Add the user matching for internal register in formal verification script generation

This commit is contained in:
AurelienUoU 2019-05-03 10:24:02 -06:00
parent 974af5a2ae
commit 42f20eda60
7 changed files with 149 additions and 10 deletions

View File

@ -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;

View File

@ -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
*********************************************************************/

View File

@ -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 <stdio.h>
#include <stdlib.h>
#include <string.h>
@ -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 */

View File

@ -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;
}

View File

@ -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);

View File

@ -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);

View File

@ -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