From 42f20eda60bbc8ca8ab3a7789e21b09c3ae29f25 Mon Sep 17 00:00:00 2001 From: AurelienUoU Date: Fri, 3 May 2019 10:24:02 -0600 Subject: [PATCH] Add the user matching for internal register in formal verification script generation --- vpr7_x2p/vpr/SRC/base/globals.c | 2 + vpr7_x2p/vpr/SRC/base/globals.h | 2 + .../verilog/verilog_formality_autodeck.c | 120 +++++++++++++++++- .../vpr/SRC/fpga_x2p/verilog/verilog_utils.c | 24 ++++ .../vpr/SRC/fpga_x2p/verilog/verilog_utils.h | 1 + vpr7_x2p/vpr/SRC/pack/cluster.c | 2 + vpr7_x2p/vpr/go_fpga_verilog.sh | 8 +- 7 files changed, 149 insertions(+), 10 deletions(-) diff --git a/vpr7_x2p/vpr/SRC/base/globals.c b/vpr7_x2p/vpr/SRC/base/globals.c index 022e64db3..f0ef6bc6d 100644 --- a/vpr7_x2p/vpr/SRC/base/globals.c +++ b/vpr7_x2p/vpr/SRC/base/globals.c @@ -13,6 +13,8 @@ int binary_search = -1; float grid_logic_tile_area = 0; float ipin_mux_trans_size = 0; +int copy_nb_clusters = 0; + /* User netlist information begin */ int num_logical_nets = 0, num_logical_blocks = 0; int num_p_inputs = 0, num_p_outputs = 0; diff --git a/vpr7_x2p/vpr/SRC/base/globals.h b/vpr7_x2p/vpr/SRC/base/globals.h index 5589116a0..47e993e76 100644 --- a/vpr7_x2p/vpr/SRC/base/globals.h +++ b/vpr7_x2p/vpr/SRC/base/globals.h @@ -38,6 +38,8 @@ extern struct s_net *clb_net; extern int num_blocks; extern struct s_block *block; +extern int copy_nb_clusters; + /******************************************************************** Physical FPGA architecture globals *********************************************************************/ diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formality_autodeck.c b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formality_autodeck.c index 56eb60497..569d6cac2 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formality_autodeck.c +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formality_autodeck.c @@ -1,5 +1,7 @@ -// Formality runsim -// Need to declare formality_script_name_postfix = "formality_script.tcl"; +/***********************************/ +/* SPICE Modeling for VPR */ +/* Xifan TANG, EPFL/LSI */ +/***********************************/ #include #include #include @@ -14,19 +16,124 @@ #include "physical_types.h" #include "vpr_types.h" #include "globals.h" +#include "rr_graph_util.h" #include "rr_graph.h" +#include "rr_graph2.h" +#include "route_common.h" #include "vpr_utils.h" -#include "path_delay.h" -#include "stats.h" -/* Include FPGA-SPICE utils */ +/* Include SPICE support headers*/ #include "linkedlist.h" +#include "fpga_x2p_types.h" #include "fpga_x2p_utils.h" +#include "fpga_x2p_backannotate_utils.h" +#include "fpga_x2p_mux_utils.h" +#include "fpga_x2p_pbtypes_utils.h" +#include "fpga_x2p_bitstream_utils.h" +#include "fpga_x2p_rr_graph_utils.h" #include "fpga_x2p_globals.h" -/* Include verilog utils */ +/* Include Verilog support headers*/ #include "verilog_global.h" #include "verilog_utils.h" +#include "verilog_routing.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; + + pb_type = pb->pb_graph_node->pb_type; + node = pb->pb_graph_node->physical_pb_graph_node; + mode = &pb_type->modes[pb->mode]; + +// tmp = (char*) my_malloc(sizeof(1 + (strlen(ff_hierarchy) + 1 + strlen(my_strcat(pb_type->name, index))))); +// tmp = ff_hierarchy; +// index = my_strcat("_", my_strcat(my_itoa(pb_index), "_")); + + if (pb_type->num_modes > 0) { + 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) +// tmp = my_strcat(tmp, my_strcat("/", my_strcat(pb_type->name, index))); + if(pb->child_pbs[i][j].name != NULL) + 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)){ +// 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, + pb->name, + 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; +} + +static void clb_iteration(FILE *fp, char* chomped_circuit_name, int h){ + t_phy_pb* cur_phy_pb; + t_pb* pb; + char* inst_name = NULL; + const t_pb_type *pb_type; + t_pb_graph_node *pb_graph_node; + t_mode *mode; + int i, j, x_pos, y_pos; + char* grid_x = NULL; + char* grid_y = NULL; + + x_pos = block[h].x; + y_pos = block[h].y; + + cur_phy_pb = (t_phy_pb*) block[h].phy_pb; + pb = (t_pb*) block[h].pb; + + pb_type = pb->pb_graph_node->pb_type; + pb_graph_node = pb->pb_graph_node; + mode = &pb_type->modes[pb->mode]; + + grid_x = my_strcat("_", my_strcat(my_itoa(x_pos), "_")); + grid_y = my_strcat("_", my_strcat(my_itoa(y_pos), "_")); + + + 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, "/" ))))))); + 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 (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 */ + 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; +} + +static void match_registers(FILE *fp, char* chomped_circuit_name) { + int h; + + 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, @@ -130,6 +237,7 @@ void write_formality_script (t_syn_verilog_opts fpga_verilog_opts, } } } + match_registers(fp, chomped_circuit_name); /* Run verification */ fprintf(fp, "verify\n"); /* Script END */ diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.c b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.c index 5e1f476c7..c6abe57c9 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.c +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.c @@ -3436,3 +3436,27 @@ char* gen_verilog_one_pb_graph_pin_full_name_in_hierarchy_grand_parent_node(t_pb return full_name; } +char* gen_verilog_one_pb_graph_node_full_name_in_hierarchy(t_pb_graph_node* cur_pb_graph_node) { + char* full_name = NULL; + char* cur_name = NULL; + t_pb_graph_node* temp = cur_pb_graph_node; + + full_name = ""; + /* The instance name of the top-level graph node is very special + * we output it in another function + */ + while (NULL != temp->parent_pb_graph_node) { + /* Generate the instance name of current pb_graph_node + * and add a slash to separate the upper level + */ + cur_name = gen_verilog_one_pb_graph_node_instance_name(temp); + cur_name = my_strcat(cur_name, "/"); + full_name = my_strcat(cur_name, full_name); + /* Go to upper level */ + temp = temp->parent_pb_graph_node; + my_free(cur_name); + } + + return full_name; +} + diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.h b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.h index 9c552cfb0..35edb02c3 100644 --- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.h +++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_utils.h @@ -280,3 +280,4 @@ char* gen_verilog_one_pb_graph_pin_full_name_in_hierarchy_grand_parent_node(t_pb char* gen_verilog_top_module_io_port_prefix(char* global_prefix, char* io_port_prefix); +char* gen_verilog_one_pb_graph_node_full_name_in_hierarchy(t_pb_graph_node* cur_pb_graph_node); diff --git a/vpr7_x2p/vpr/SRC/pack/cluster.c b/vpr7_x2p/vpr/SRC/pack/cluster.c index ee95f08da..8517568cc 100755 --- a/vpr7_x2p/vpr/SRC/pack/cluster.c +++ b/vpr7_x2p/vpr/SRC/pack/cluster.c @@ -576,6 +576,8 @@ void do_clustering(const t_arch *arch, t_pack_molecule *molecule_head, output_clustering(clb, num_clb, global_clocks, is_clock, out_fname, FALSE); + copy_nb_clusters = num_clb; + if (getEchoEnabled() && isEchoFileEnabled(E_ECHO_POST_PACK_NETLIST)) { output_blif (clb, num_clb, global_clocks, is_clock, getEchoFileName(E_ECHO_POST_PACK_NETLIST), FALSE); diff --git a/vpr7_x2p/vpr/go_fpga_verilog.sh b/vpr7_x2p/vpr/go_fpga_verilog.sh index 0226049e9..cabfbd6d8 100755 --- a/vpr7_x2p/vpr/go_fpga_verilog.sh +++ b/vpr7_x2p/vpr/go_fpga_verilog.sh @@ -3,8 +3,8 @@ # Set variables # For FPGA-Verilog ONLY -set verilog_output_dirname = sram_fpga_hetero -set verilog_output_dirpath = /var/tmp/xtang/vpr7 +set verilog_output_dirname = OpenFPGA_Branch +set verilog_output_dirpath = /var/tmp/AA_simu/ set modelsim_ini_file = /uusoc/facility/cad_tools/Mentor/modelsim10.7b/modeltech/modelsim.ini # VPR critical inputs #set arch_xml_file = ARCH/k6_N10_MD_tsmc40nm_chain_TT.xml @@ -18,8 +18,8 @@ set arch_xml_file = ARCH/k8_N10_sram_chain_FC_tsmc40_stratix4_auto.xml #set verilog_reference = ${PWD}/Circuits/alu4_K6_N10_ace.v #set blif_file = Circuits/shiftReg.blif #set act_file = Circuits/shiftReg.act -set blif_file = Circuits/simple_gates_prevpr.blif -set act_file = Circuits/simple_gates_prevpr.act +set blif_file = Circuits/s298_prevpr.blif +set act_file = Circuits/s298_prevpr.act set verilog_reference = ${PWD}/Circuits/s298_prevpr.v #set blif_file = Circuits/frisc.blif #set act_file = Circuits/frisc.act