Separated Modelsim tcl script generation
This commit is contained in:
parent
bcbcd463fe
commit
d64bb18346
|
@ -0,0 +1,8 @@
|
||||||
|
read_verilog -container r -libname WORK -05 { ${SOURCE_DESIGN} }
|
||||||
|
set_top r:${SOURCE_TOP_DIR}
|
||||||
|
read_verilog -container i -libname WORK -05 { ${IMPL_DESIGN} }
|
||||||
|
|
||||||
|
set_top i:${IMPL_TOP_DIR}
|
||||||
|
match
|
||||||
|
${MATCH_MODUEL_LIST}
|
||||||
|
verify
|
|
@ -0,0 +1,86 @@
|
||||||
|
from string import Template
|
||||||
|
import sys
|
||||||
|
import os
|
||||||
|
import argparse
|
||||||
|
import subprocess
|
||||||
|
import logging
|
||||||
|
from pprint import pprint
|
||||||
|
|
||||||
|
# = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
|
||||||
|
# Configure logging system
|
||||||
|
# = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =
|
||||||
|
logging.basicConfig(level=logging.INFO, stream=sys.stdout,
|
||||||
|
format='%(levelname)s (%(threadName)10s) - %(message)s')
|
||||||
|
logger = logging.getLogger('Modelsim_run_log')
|
||||||
|
|
||||||
|
parser = argparse.ArgumentParser()
|
||||||
|
parser.add_argument('files', nargs='+')
|
||||||
|
parser.add_argument('--modelsim_template', type=str,
|
||||||
|
help="Modelsim verification template file")
|
||||||
|
parser.add_argument('--run_sim', action="store_true",
|
||||||
|
help="Execute generated script in formality")
|
||||||
|
args = parser.parse_args()
|
||||||
|
|
||||||
|
|
||||||
|
if not args.modelsim_template:
|
||||||
|
task_script_dir = os.path.dirname(os.path.abspath(__file__))
|
||||||
|
args.modelsim_template = os.path.join(task_script_dir, os.pardir,
|
||||||
|
"misc", "modelsim_template.j2")
|
||||||
|
|
||||||
|
args.modelsim_template = os.path.abspath(args.modelsim_template)
|
||||||
|
|
||||||
|
|
||||||
|
def main():
|
||||||
|
for eachFile in args.files:
|
||||||
|
eachFile = os.path.abspath(eachFile)
|
||||||
|
directory = os.path.dirname(eachFile)
|
||||||
|
os.chdir(directory)
|
||||||
|
with open(eachFile, 'r') as fp:
|
||||||
|
lines = fp.read().split("\n")
|
||||||
|
SplitL = [indx for indx, eachL in enumerate(lines) if eachL == ""]
|
||||||
|
SplitL = list(zip([0] + SplitL[:-1], SplitL))
|
||||||
|
for indx, eachSection in enumerate(SplitL):
|
||||||
|
SplitL[indx] = list(filter(None, lines[slice(*eachSection)]))
|
||||||
|
|
||||||
|
match_str = "set_user_match r:%s i:%s -type port -noninverted"
|
||||||
|
lables = {"SOURCE_DESIGN": " ".join(SplitL[0]),
|
||||||
|
"SOURCE_TOP_DIR": "/WORK/" + " ".join(SplitL[1]),
|
||||||
|
"IMPL_DESIGN": " ".join(SplitL[2]),
|
||||||
|
"IMPL_TOP_DIR": "/WORK/" + " ".join(SplitL[3]),
|
||||||
|
"MATCH_MODUEL_LIST": "\n".join([match_str % tuple(eachPort.split()) for eachPort in SplitL[4]])
|
||||||
|
}
|
||||||
|
|
||||||
|
tmpl = Template(open(args.modelsim_template, encoding='utf-8').read())
|
||||||
|
with open("Output.tcl", 'w', encoding='utf-8') as tclout:
|
||||||
|
tclout.write(tmpl.substitute(lables))
|
||||||
|
if args.run_sim:
|
||||||
|
formality_run_string = ["formality", "-file", "Output.tcl"]
|
||||||
|
run_command("Modelsim run", "modelsim_run.log", formality_run_string)
|
||||||
|
else:
|
||||||
|
with open("Output.tcl", 'r', encoding='utf-8') as tclout:
|
||||||
|
print(tclout.read())
|
||||||
|
|
||||||
|
|
||||||
|
def run_command(taskname, logfile, command, exit_if_fail=True):
|
||||||
|
logger.info("Launching %s " % taskname)
|
||||||
|
with open(logfile, 'w+') as output:
|
||||||
|
try:
|
||||||
|
output.write(" ".join(command)+"\n")
|
||||||
|
process = subprocess.run(command,
|
||||||
|
check=True,
|
||||||
|
stdout=subprocess.PIPE,
|
||||||
|
stderr=subprocess.PIPE,
|
||||||
|
universal_newlines=True)
|
||||||
|
output.write(process.stdout)
|
||||||
|
if process.returncode:
|
||||||
|
logger.error("%s run failed with returncode %d" %
|
||||||
|
(taskname, process.returncode))
|
||||||
|
except (Exception, subprocess.CalledProcessError) as e:
|
||||||
|
logger.exception("failed to execute %s" % taskname)
|
||||||
|
return None
|
||||||
|
logger.info("%s is written in file %s" % (taskname, logfile))
|
||||||
|
return process.stdout
|
||||||
|
|
||||||
|
|
||||||
|
if __name__ == "__main__":
|
||||||
|
main()
|
|
@ -39,105 +39,99 @@
|
||||||
#include "verilog_routing.h"
|
#include "verilog_routing.h"
|
||||||
#include "verilog_tcl_utils.h"
|
#include "verilog_tcl_utils.h"
|
||||||
|
|
||||||
|
static void searching_used_latch(FILE *fp, t_pb *pb, int pb_index, char *chomped_circuit_name, char *inst_name)
|
||||||
|
{
|
||||||
|
int i, j;
|
||||||
|
// char* tmp = NULL;
|
||||||
|
const t_pb_type *pb_type;
|
||||||
|
t_mode *mode;
|
||||||
|
t_pb_graph_node *node;
|
||||||
|
// char* index = NULL;
|
||||||
|
|
||||||
static void searching_used_latch(FILE *fp, t_pb * pb, int pb_index, char* chomped_circuit_name, char* inst_name){
|
pb_type = pb->pb_graph_node->pb_type;
|
||||||
int i, j;
|
node = pb->pb_graph_node->physical_pb_graph_node;
|
||||||
// char* tmp = NULL;
|
mode = &pb_type->modes[pb->mode];
|
||||||
const t_pb_type *pb_type;
|
|
||||||
t_mode *mode;
|
|
||||||
t_pb_graph_node * node;
|
|
||||||
// char* index = NULL;
|
|
||||||
|
|
||||||
pb_type = pb->pb_graph_node->pb_type;
|
// tmp = (char*) my_malloc(sizeof(1 + (strlen(ff_hierarchy) + 1 + strlen(my_strcat(pb_type->name, index)))));
|
||||||
node = pb->pb_graph_node->physical_pb_graph_node;
|
// tmp = ff_hierarchy;
|
||||||
mode = &pb_type->modes[pb->mode];
|
// index = my_strcat("_", my_strcat(my_itoa(pb_index), "_"));
|
||||||
|
|
||||||
// tmp = (char*) my_malloc(sizeof(1 + (strlen(ff_hierarchy) + 1 + strlen(my_strcat(pb_type->name, index)))));
|
if (pb_type->num_modes > 0)
|
||||||
// tmp = ff_hierarchy;
|
{
|
||||||
// index = my_strcat("_", my_strcat(my_itoa(pb_index), "_"));
|
for (i = 0; i < mode->num_pb_type_children; i++)
|
||||||
|
{
|
||||||
if (pb_type->num_modes > 0) {
|
for (j = 0; j < mode->pb_type_children[i].num_pb; j++)
|
||||||
for (i = 0; i < mode->num_pb_type_children; i++) {
|
{
|
||||||
for (j = 0; j < mode->pb_type_children[i].num_pb; j++) {
|
// if(strcmp(pb_type->name, mode->name) != 0)
|
||||||
// if(strcmp(pb_type->name, mode->name) != 0)
|
// tmp = my_strcat(tmp, my_strcat("/", my_strcat(pb_type->name, index)));
|
||||||
// tmp = my_strcat(tmp, my_strcat("/", my_strcat(pb_type->name, index)));
|
if (pb->child_pbs[i][j].name != NULL)
|
||||||
if(pb->child_pbs[i][j].name != NULL)
|
searching_used_latch(fp, &pb->child_pbs[i][j], j, chomped_circuit_name, inst_name);
|
||||||
searching_used_latch(fp, &pb->child_pbs[i][j], j, chomped_circuit_name, inst_name);
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} else if((pb_type->class_type == LATCH_CLASS) && (pb->name)){
|
else if ((pb_type->class_type == LATCH_CLASS) && (pb->name))
|
||||||
// tmp = my_strcat(tmp, my_strcat("/", my_strcat(pb_type->physical_pb_type_name, my_strcat(index, "/dff_0_"))));
|
{
|
||||||
fprintf(fp, "set_user_match r:/WORK/%s/%s_reg i:/WORK/%s/%sdff_0 -type cell -noninverted\n", chomped_circuit_name,
|
// tmp = my_strcat(tmp, my_strcat("/", my_strcat(pb_type->physical_pb_type_name, my_strcat(index, "/dff_0_"))));
|
||||||
pb->name,
|
fprintf(fp, "set_user_match r:/WORK/%s/%s_reg i:/WORK/%s/%sdff_0 -type cell -noninverted\n", chomped_circuit_name,
|
||||||
inst_name,
|
pb->name,
|
||||||
gen_verilog_one_pb_graph_node_full_name_in_hierarchy(node) );
|
inst_name,
|
||||||
}
|
gen_verilog_one_pb_graph_node_full_name_in_hierarchy(node));
|
||||||
//free(tmp); //Looks like is the cause of a double free, once free executated next iteration as no value in tmp
|
}
|
||||||
return;
|
//free(tmp); //Looks like is the cause of a double free, once free executated next iteration as no value in tmp
|
||||||
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
static void clb_iteration(FILE *fp, char* chomped_circuit_name, int h){
|
static void clb_iteration(FILE *fp, char *chomped_circuit_name, int h)
|
||||||
t_pb* pb;
|
{
|
||||||
char* inst_name = NULL;
|
t_pb *pb;
|
||||||
const t_pb_type *pb_type;
|
char *inst_name = NULL;
|
||||||
t_mode *mode;
|
const t_pb_type *pb_type;
|
||||||
int i, j, x_pos, y_pos;
|
t_mode *mode;
|
||||||
char* grid_x = NULL;
|
int i, j, x_pos, y_pos;
|
||||||
char* grid_y = NULL;
|
char *grid_x = NULL;
|
||||||
|
char *grid_y = NULL;
|
||||||
|
|
||||||
x_pos = block[h].x;
|
x_pos = block[h].x;
|
||||||
y_pos = block[h].y;
|
y_pos = block[h].y;
|
||||||
|
|
||||||
pb = (t_pb*) block[h].pb;
|
pb = (t_pb *)block[h].pb;
|
||||||
|
|
||||||
pb_type = pb->pb_graph_node->pb_type;
|
pb_type = pb->pb_graph_node->pb_type;
|
||||||
mode = &pb_type->modes[pb->mode];
|
mode = &pb_type->modes[pb->mode];
|
||||||
|
|
||||||
grid_x = my_strcat("_", my_strcat(my_itoa(x_pos), "_"));
|
grid_x = my_strcat("_", my_strcat(my_itoa(x_pos), "_"));
|
||||||
grid_y = my_strcat("_", my_strcat(my_itoa(y_pos), "_"));
|
grid_y = my_strcat("_", my_strcat(my_itoa(y_pos), "_"));
|
||||||
|
|
||||||
|
if (strcmp(pb_type->name, FILL_TYPE->name) == 0)
|
||||||
if (strcmp(pb_type->name, FILL_TYPE->name) == 0) {
|
{
|
||||||
inst_name = my_strcat(chomped_circuit_name, my_strcat(formal_verification_top_postfix, my_strcat("/", my_strcat(formal_verification_top_module_uut_name, my_strcat("/grid",my_strcat(grid_x, my_strcat(grid_y, "/" )))))));
|
inst_name = my_strcat(chomped_circuit_name, my_strcat(formal_verification_top_postfix, my_strcat("/", my_strcat(formal_verification_top_module_uut_name, my_strcat("/grid", my_strcat(grid_x, my_strcat(grid_y, "/")))))));
|
||||||
if (pb_type->num_modes > 0) {
|
if (pb_type->num_modes > 0)
|
||||||
for (i = 0; i < mode->num_pb_type_children; i++) {
|
{
|
||||||
inst_name = my_strcat(inst_name, my_strcat("grid_", my_strcat(pb_type->name, my_strcat("_", my_strcat(my_itoa(i), "_")))));
|
for (i = 0; i < mode->num_pb_type_children; i++)
|
||||||
for (j = 0; j < mode->pb_type_children[i].num_pb; j++) {
|
{
|
||||||
/* If child pb is not used but routing is used, I must print things differently */
|
inst_name = my_strcat(inst_name, my_strcat("grid_", my_strcat(pb_type->name, my_strcat("_", my_strcat(my_itoa(i), "_")))));
|
||||||
if ((pb->child_pbs[i] != NULL)
|
for (j = 0; j < mode->pb_type_children[i].num_pb; j++)
|
||||||
&& (pb->child_pbs[i][j].name != NULL)) {
|
{
|
||||||
searching_used_latch(fp, &pb->child_pbs[i][j], j, chomped_circuit_name, inst_name);
|
/* If child pb is not used but routing is used, I must print things differently */
|
||||||
}
|
if ((pb->child_pbs[i] != NULL) && (pb->child_pbs[i][j].name != NULL))
|
||||||
}
|
{
|
||||||
}
|
searching_used_latch(fp, &pb->child_pbs[i][j], j, chomped_circuit_name, inst_name);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return;
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
static void match_registers(FILE *fp, char* chomped_circuit_name) {
|
static void formality_include_user_defined_verilog_netlists(FILE *fp,
|
||||||
int h;
|
t_spice spice)
|
||||||
|
{
|
||||||
for(h = 0; h < copy_nb_clusters; h++)
|
|
||||||
clb_iteration(fp, chomped_circuit_name, h);
|
|
||||||
/* for(h = 0; h < copy_nb_clusters; h++){
|
|
||||||
free_cb(copy_clb[h].pb);
|
|
||||||
free(copy_clb[h].name);
|
|
||||||
free(copy_clb[h].nets);
|
|
||||||
free(copy_clb[h].pb);
|
|
||||||
}*/
|
|
||||||
// free(copy_clb);
|
|
||||||
// free(block);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
|
|
||||||
static
|
|
||||||
void formality_include_user_defined_verilog_netlists(FILE* fp,
|
|
||||||
t_spice spice) {
|
|
||||||
int i;
|
int i;
|
||||||
|
|
||||||
/* A valid file handler*/
|
/* A valid file handler*/
|
||||||
if (NULL == fp) {
|
if (NULL == fp)
|
||||||
|
{
|
||||||
vpr_printf(TIO_MESSAGE_ERROR,
|
vpr_printf(TIO_MESSAGE_ERROR,
|
||||||
"(File:%s, [LINE%d])Invalid File Handler!\n",
|
"(File:%s, [LINE%d])Invalid File Handler!\n",
|
||||||
__FILE__, __LINE__);
|
__FILE__, __LINE__);
|
||||||
|
@ -145,12 +139,16 @@ void formality_include_user_defined_verilog_netlists(FILE* fp,
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Include user-defined sub-circuit netlist */
|
/* Include user-defined sub-circuit netlist */
|
||||||
for (i = 0; i < spice.num_include_netlist; i++) {
|
for (i = 0; i < spice.num_include_netlist; i++)
|
||||||
if (0 == spice.include_netlists[i].included) {
|
{
|
||||||
|
if (0 == spice.include_netlists[i].included)
|
||||||
|
{
|
||||||
assert(NULL != spice.include_netlists[i].path);
|
assert(NULL != spice.include_netlists[i].path);
|
||||||
fprintf(fp, "%s ", spice.include_netlists[i].path);
|
fprintf(fp, "%s \n", spice.include_netlists[i].path);
|
||||||
spice.include_netlists[i].included = 1;
|
spice.include_netlists[i].included = 1;
|
||||||
} else {
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
assert(1 == spice.include_netlists[i].included);
|
assert(1 == spice.include_netlists[i].included);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -158,84 +156,100 @@ void formality_include_user_defined_verilog_netlists(FILE* fp,
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
void write_formality_script (t_syn_verilog_opts fpga_verilog_opts,
|
void write_formality_script(t_syn_verilog_opts fpga_verilog_opts,
|
||||||
char* fm_dir_formatted,
|
char *fm_dir_formatted,
|
||||||
char* src_dir_formatted,
|
char *src_dir_formatted,
|
||||||
char* chomped_circuit_name,
|
char *chomped_circuit_name,
|
||||||
t_spice spice){
|
t_spice spice)
|
||||||
int iblock;
|
{
|
||||||
char* formality_script_file_name = NULL;
|
int iblock, h;
|
||||||
char* benchmark_path = NULL;
|
char *formScriptfp = NULL;
|
||||||
char* original_output_name = NULL;
|
char *benchmark_path = NULL;
|
||||||
/* int output_length; */
|
char *original_output_name = NULL;
|
||||||
/* int pos; */
|
/* int output_length; */
|
||||||
FILE* fp = NULL;
|
/* int pos; */
|
||||||
|
FILE *fp = NULL;
|
||||||
|
|
||||||
if(TRUE == fpga_verilog_opts.print_autocheck_top_testbench){
|
if (TRUE == fpga_verilog_opts.print_autocheck_top_testbench)
|
||||||
|
{
|
||||||
benchmark_path = fpga_verilog_opts.reference_verilog_benchmark_file;
|
benchmark_path = fpga_verilog_opts.reference_verilog_benchmark_file;
|
||||||
} else {
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
benchmark_path = "Insert verilog benchmark path";
|
benchmark_path = "Insert verilog benchmark path";
|
||||||
}
|
}
|
||||||
|
|
||||||
formality_script_file_name = my_strcat(fm_dir_formatted, my_strcat(chomped_circuit_name, formality_script_name_postfix));
|
formScriptfp = my_strcat(fm_dir_formatted,
|
||||||
fp = fopen(formality_script_file_name, "w");
|
my_strcat(chomped_circuit_name,
|
||||||
if (NULL == fp) {
|
formality_script_name_postfix));
|
||||||
vpr_printf(TIO_MESSAGE_ERROR,
|
fp = fopen(formScriptfp, "w");
|
||||||
"(FILE:%s,LINE[%d])Failure in create formality script %s",
|
if (NULL == fp)
|
||||||
__FILE__, __LINE__, formality_script_file_name);
|
{
|
||||||
exit(1);
|
vpr_printf(TIO_MESSAGE_ERROR,
|
||||||
}
|
"(FILE:%s,LINE[%d])Failure in create formality script %s",
|
||||||
|
__FILE__, __LINE__, formScriptfp);
|
||||||
|
exit(1);
|
||||||
|
}
|
||||||
|
|
||||||
/* Load Verilog benchmark as reference */
|
/* Load Verilog benchmark as reference */
|
||||||
fprintf(fp, "read_verilog -container r -libname WORK -05 { %s }\n", benchmark_path);
|
fprintf(fp, "%s\n\n", benchmark_path);
|
||||||
|
|
||||||
/* Set reference top */
|
/* Set reference top */
|
||||||
fprintf(fp, "set_top r:/WORK/%s\n", chomped_circuit_name);
|
fprintf(fp, "%s\n\n", chomped_circuit_name);
|
||||||
|
|
||||||
/* Load generated verilog as implemnetation */
|
/* Load generated verilog as implemnetation */
|
||||||
fprintf(fp, "read_verilog -container i -libname WORK -05 { ");
|
fprintf(fp, "%s%s%s\n", src_dir_formatted, chomped_circuit_name,
|
||||||
fprintf(fp, "%s%s%s ", src_dir_formatted,
|
verilog_top_postfix);
|
||||||
chomped_circuit_name,
|
|
||||||
verilog_top_postfix);
|
fprintf(fp, "%s%s%s\n", src_dir_formatted,
|
||||||
fprintf(fp, "%s%s%s ", src_dir_formatted,
|
chomped_circuit_name,
|
||||||
chomped_circuit_name,
|
formal_verification_verilog_file_postfix);
|
||||||
formal_verification_verilog_file_postfix);
|
|
||||||
init_include_user_defined_verilog_netlists(spice);
|
init_include_user_defined_verilog_netlists(spice);
|
||||||
formality_include_user_defined_verilog_netlists(fp, spice);
|
formality_include_user_defined_verilog_netlists(fp, spice);
|
||||||
fprintf(fp, "%s%s%s ", src_dir_formatted,
|
fprintf(fp, "%s%s%s\n", src_dir_formatted,
|
||||||
default_rr_dir_name,
|
default_rr_dir_name,
|
||||||
routing_verilog_file_name);
|
routing_verilog_file_name);
|
||||||
fprintf(fp, "%s%s%s ", src_dir_formatted,
|
fprintf(fp, "%s%s%s\n", src_dir_formatted,
|
||||||
default_lb_dir_name,
|
default_lb_dir_name,
|
||||||
logic_block_verilog_file_name);
|
logic_block_verilog_file_name);
|
||||||
fprintf(fp, "%s%s%s ", src_dir_formatted,
|
fprintf(fp, "%s%s%s\n", src_dir_formatted,
|
||||||
default_submodule_dir_name,
|
default_submodule_dir_name,
|
||||||
submodule_verilog_file_name);
|
submodule_verilog_file_name);
|
||||||
fprintf(fp, "}\n");
|
fprintf(fp, "\n");
|
||||||
|
|
||||||
/* Set implementation top */
|
/* Set implementation top */
|
||||||
fprintf(fp, "set_top i:/WORK/%s\n", my_strcat(chomped_circuit_name, formal_verification_top_postfix));
|
fprintf(fp, "%s\n", my_strcat(chomped_circuit_name, formal_verification_top_postfix));
|
||||||
/* Run matching */
|
/* Run matching */
|
||||||
fprintf(fp, "match\n");
|
fprintf(fp, "\n");
|
||||||
/* Add manual matching for the outputs */
|
/* Add manual matching for the outputs */
|
||||||
for (iblock = 0; iblock < num_logical_blocks; iblock++) {
|
for (iblock = 0; iblock < num_logical_blocks; iblock++)
|
||||||
|
{
|
||||||
original_output_name = NULL;
|
original_output_name = NULL;
|
||||||
if (iopad_verilog_model == logical_block[iblock].mapped_spice_model) {
|
if (iopad_verilog_model == logical_block[iblock].mapped_spice_model)
|
||||||
|
{
|
||||||
/* Make sure We find the correct logical block !*/
|
/* Make sure We find the correct logical block !*/
|
||||||
assert((VPACK_INPAD == logical_block[iblock].type)
|
assert((VPACK_INPAD == logical_block[iblock].type) || (VPACK_OUTPAD == logical_block[iblock].type));
|
||||||
||(VPACK_OUTPAD == logical_block[iblock].type));
|
if (VPACK_OUTPAD == logical_block[iblock].type)
|
||||||
if(VPACK_OUTPAD == logical_block[iblock].type){
|
{
|
||||||
/* output_length = strlen(logical_block[iblock].name); */
|
/* output_length = strlen(logical_block[iblock].name); */
|
||||||
original_output_name = logical_block[iblock].name + 4;
|
original_output_name = logical_block[iblock].name + 4;
|
||||||
/* printf("%s", original_output_name); */
|
/* printf("%s", original_output_name); */
|
||||||
fprintf(fp, "set_user_match r:/WORK/%s/%s i:/WORK/%s/%s[0] -type port -noninverted\n",
|
// fprintf(fp, "set_user_match r:/WORK/%s/%s i:/WORK/%s/%s[0] -type port -noninverted\n",
|
||||||
|
fprintf(fp, "/WORK/%s/%s /WORK/%s/%s[0]\n",
|
||||||
chomped_circuit_name,
|
chomped_circuit_name,
|
||||||
original_output_name,
|
original_output_name,
|
||||||
my_strcat(chomped_circuit_name, formal_verification_top_postfix),
|
my_strcat(chomped_circuit_name, formal_verification_top_postfix),
|
||||||
my_strcat(logical_block[iblock].name, formal_verification_top_module_port_postfix));
|
my_strcat(logical_block[iblock].name, formal_verification_top_module_port_postfix));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
match_registers(fp, chomped_circuit_name);
|
|
||||||
|
for (h = 0; h < copy_nb_clusters; h++)
|
||||||
|
clb_iteration(fp, chomped_circuit_name, h);
|
||||||
|
|
||||||
/* Run verification */
|
/* Run verification */
|
||||||
fprintf(fp, "verify\n");
|
fprintf(fp, "\n");
|
||||||
/* Script END */
|
/* Script END */
|
||||||
fclose(fp);
|
fclose(fp);
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue