refactoring Verilog formal verification top testbench using random vectors

vpr7_x2p/vpr/SRC/base/vpr_types.h

@@ -245,6 +245,7 @@ typedef struct s_logical_block {
 
     /* Xifan TANG: SPICE model support*/
     /* For mapping */
+    CircuitModelId mapped_circuit_model;
     t_spice_model* mapped_spice_model;
     int mapped_spice_model_index; /* index of spice_model in completed FPGA netlist */
     int temp_used;

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_api.c

@@ -153,8 +153,6 @@ void vpr_fpga_verilog(ModuleManager& module_manager,
   char* formal_verification_top_netlist_file_path = NULL;
   char* autocheck_top_testbench_file_name = NULL;
   char* autocheck_top_testbench_file_path = NULL;
-  char* random_top_testbench_file_name = NULL;
-  char* random_top_testbench_file_path = NULL;
 
   char* chomped_parent_dir = NULL;
   char* chomped_circuit_name = NULL;
@@ -396,6 +394,12 @@ void vpr_fpga_verilog(ModuleManager& module_manager,
     my_free(top_testbench_file_path);
   }
 
+  /* Create vectors for logical blocks */
+  std::vector<t_logical_block> L_logical_blocks;
+  for (int i = 0; i < num_logical_blocks; ++i) {
+    L_logical_blocks.push_back(logical_block[i]);
+  }
+
   if (TRUE == vpr_setup.FPGA_SPICE_Opts.SynVerilogOpts.print_formal_verification_top_netlist) {
     formal_verification_top_netlist_file_name = my_strcat(chomped_circuit_name, formal_verification_verilog_file_postfix);
     formal_verification_top_netlist_file_path = my_strcat(src_dir_path, formal_verification_top_netlist_file_name);
@@ -407,11 +411,20 @@ void vpr_fpga_verilog(ModuleManager& module_manager,
                            src_dir_path,
                            chomped_circuit_name,
                            *(Arch.spice));
-    random_top_testbench_file_name = my_strcat(chomped_circuit_name, random_top_testbench_verilog_file_postfix);
-    random_top_testbench_file_path = my_strcat(src_dir_path, random_top_testbench_file_name);
+
+    /* Print out top-level testbench using random vectors */
+    std::string random_top_testbench_file_path = std::string(src_dir_path) 
+                                               + std::string(chomped_circuit_name) 
+                                               + std::string(random_top_testbench_verilog_file_postfix);
+    /* FIXME: old function TO BE REMOVED */
 	dump_verilog_random_top_testbench(sram_verilog_orgz_info, chomped_circuit_name, 
-                                      random_top_testbench_file_path, src_dir_path,
+                                      random_top_testbench_file_path.c_str(), src_dir_path,
                                       vpr_setup.FPGA_SPICE_Opts.SynVerilogOpts, *(Arch.spice));
+    /* TODO: remove the .bak when it is ready */
+    print_verilog_random_top_testbench(std::string(chomped_circuit_name), random_top_testbench_file_path + ".bak", 
+                                       std::string(src_dir_path), L_logical_blocks,  
+                                       vpr_setup.FPGA_SPICE_Opts.SynVerilogOpts, Arch.spice->spice_params);
+    
     /* Free */
     my_free(formal_verification_top_netlist_file_name);
     my_free(formal_verification_top_netlist_file_path);

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.c

@@ -352,11 +352,11 @@ void dump_verilog_top_random_stimuli(FILE* fp,
 }
 
 void dump_verilog_random_top_testbench(t_sram_orgz_info* cur_sram_orgz_info,
-                                          char* circuit_name,
-                                          char* top_netlist_name,
-                                          char* verilog_dir_path,
-                                          t_syn_verilog_opts fpga_verilog_opts,
-                                          t_spice verilog) {
+                                       char* circuit_name,
+                                       const char* top_netlist_name,
+                                       char* verilog_dir_path,
+                                       t_syn_verilog_opts fpga_verilog_opts,
+                                       t_spice verilog) {
   FILE* fp = NULL;
   char* title = my_strcat("FPGA Verilog Testbench for Formal Top-level netlist of Design: ", circuit_name);
   

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.cpp

@@ -0,0 +1,590 @@
+/********************************************************************
+ * This file includes functions that are used to generate a Verilog 
+ * testbench for the top-level module (FPGA fabric), in purpose of
+ * running formal verification with random input vectors 
+ *******************************************************************/
+#include <fstream>
+#include <cstring>
+#include <cmath>
+#include <ctime>
+#include <iomanip>
+
+/* Include external library headers*/
+#include "device_port.h"
+#include "vtr_assert.h"
+#include "util.h"
+
+/* Include VPR headers*/
+
+/* Include FPGA-X2P headers*/
+#include "fpga_x2p_utils.h"
+
+/* Include FPGA Verilog headers*/
+#include "verilog_global.h"
+#include "verilog_writer_utils.h"
+#include "verilog_formal_random_top_testbench.h"
+
+/********************************************************************
+ * Local variables used only in this file
+ *******************************************************************/
+constexpr char* FORMAL_RANDOM_TOP_TESTBENCH_POSTFIX = "_top_formal_verification_random_tb";
+constexpr char* FPGA_PORT_POSTFIX = "_gfpga";
+constexpr char* BENCHMARK_PORT_POSTFIX = "_bench";
+constexpr char* CHECKFLAG_PORT_POSTFIX = "_flag";
+constexpr char* DEFAULT_CLOCK_NAME = "clk";
+constexpr char* BENCHMARK_INSTANCE_NAME = "REF_DUT";
+constexpr char* FPGA_INSTANCE_NAME = "REF_DUT";
+constexpr char* ERROR_COUNTER = "nb_error";
+constexpr int MAGIC_NUMBER_FOR_SIMULATION_TIME = 200;
+
+/********************************************************************
+ * Find the clock port name to be used in this testbench
+ *******************************************************************/
+static
+std::vector<std::string> find_verilog_top_clock_port_name(const std::vector<t_logical_block>& L_logical_blocks) {
+  std::vector<std::string> clock_port_names;
+
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if ( (VPACK_INPAD != lb.type) && (VPACK_OUTPAD != lb.type) ) {
+      continue;
+    }
+
+    /* Find the clock signals */
+    if ( (VPACK_INPAD == lb.type) && (TRUE == lb.is_clock) ) {
+      clock_port_names.push_back(std::string(lb.name));
+    }
+  }
+
+  return clock_port_names;
+}
+
+/********************************************************************
+ * Generate the clock port name to be used in this testbench
+ *
+ * Restrictions:
+ * Assume this is a single clock benchmark
+ *******************************************************************/
+static 
+BasicPort generate_verilog_top_clock_port(const std::vector<std::string>& clock_port_names) {
+  if (0 == clock_port_names.size()) {
+    return BasicPort(std::string(DEFAULT_CLOCK_NAME), 1); 
+  }
+
+  VTR_ASSERT(1 == clock_port_names.size());
+  return BasicPort(clock_port_names[0], 1); 
+}
+
+/********************************************************************
+ * Print the module ports for the Verilog testbench 
+ * using random vectors 
+ * This function generates 
+ * 1. the input ports to drive both input benchmark module and FPGA fabric module
+ * 2. the output ports for input benchmark module
+ * 3. the output ports for FPGA fabric module
+ * 4. the error checking ports 
+ *******************************************************************/
+static 
+void print_verilog_top_random_testbench_ports(std::fstream& fp,
+                                              const std::string& circuit_name,
+                                              const std::vector<std::string>& clock_port_names,
+                                              const std::vector<t_logical_block>& L_logical_blocks) {
+  /* Validate the file stream */
+  check_file_handler(fp);
+ 
+  /* Print the declaration for the module */
+  fp << "module " << circuit_name << FORMAL_RANDOM_TOP_TESTBENCH_POSTFIX << ";" << std::endl;
+
+  /* Instantiate register for inputs stimulis */
+  print_verilog_comment(fp, std::string("----- Shared inputs -------"));
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* We care only those logic blocks which are input I/Os */
+    if (VPACK_INPAD != lb.type) { 
+      continue;
+    }
+   
+    /* Each logical block assumes a single-width port */
+    BasicPort input_port(std::string(lb.name), 1); 
+    fp << "\t" << generate_verilog_port(VERILOG_PORT_REG, input_port) << ";" << std::endl;
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Create a clock port if the benchmark does not have one! 
+   * The clock is used for counting and synchronizing input stimulus 
+   */
+  if (0 == clock_port_names.size()) {
+    BasicPort clock_port = generate_verilog_top_clock_port(clock_port_names);
+    print_verilog_comment(fp, std::string("----- Default clock port is added here since benchmark does not contain one -------"));
+    fp << "\t" << generate_verilog_port(VERILOG_PORT_REG, clock_port) << ";" << std::endl;
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Instantiate wires for FPGA fabric outputs */
+  print_verilog_comment(fp, std::string("----- FPGA fabric outputs -------"));
+
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* We care only those logic blocks which are input I/Os */
+    if (VPACK_OUTPAD != lb.type) { 
+      continue;
+    }
+
+    /* Each logical block assumes a single-width port */
+    BasicPort output_port(std::string(std::string(lb.name) + std::string(FPGA_PORT_POSTFIX)), 1); 
+    fp << "\t" << generate_verilog_port(VERILOG_PORT_WIRE, output_port) << ";" << std::endl;
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Benchmark is instanciated conditionally: only when a preprocessing flag is enable */
+  print_verilog_preprocessing_flag(fp, std::string(autochecked_simulation_flag)); 
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Instantiate wire for benchmark output */
+  print_verilog_comment(fp, std::string("----- Benchmark outputs -------"));
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* We care only those logic blocks which are input I/Os */
+    if (VPACK_OUTPAD != lb.type) { 
+      continue;
+    }
+
+    /* Each logical block assumes a single-width port */
+    BasicPort output_port(std::string(std::string(lb.name) + std::string(BENCHMARK_PORT_POSTFIX)), 1); 
+    fp << "\t" << generate_verilog_port(VERILOG_PORT_WIRE, output_port) << ";" << std::endl;
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Instantiate register for output comparison */
+  print_verilog_comment(fp, std::string("----- Output vectors checking flags -------"));
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* We care only those logic blocks which are input I/Os */
+    if (VPACK_OUTPAD != lb.type) { 
+      continue;
+    }
+
+    /* Each logical block assumes a single-width port */
+    BasicPort output_port(std::string(std::string(lb.name) + std::string(CHECKFLAG_PORT_POSTFIX)), 1); 
+    fp << "\t" << generate_verilog_port(VERILOG_PORT_REG, output_port) << ";" << std::endl;
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Condition ends for the benchmark instanciation */
+  print_verilog_endif(fp);
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Instantiate an integer to count the number of error 
+   * and determine if the simulation succeed or failed 
+   */
+  print_verilog_comment(fp, std::string("----- Error counter -------"));
+  fp << "\tinteger " << ERROR_COUNTER << "= 0;" << std::endl;
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/********************************************************************
+ * Instanciate the FPGA fabric module
+ *******************************************************************/
+static
+void print_verilog_random_testbench_instance(std::fstream& fp,
+                                             const std::string& module_name,
+                                             const std::string& instance_name,
+                                             const std::string& output_port_postfix,
+                                             const std::vector<t_logical_block>& L_logical_blocks) {
+
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  fp << "\t" << module_name << " " << instance_name << "(" << std::endl;
+
+  size_t port_counter = 0;
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if ( (VPACK_INPAD != lb.type) && (VPACK_OUTPAD != lb.type) ) {
+      continue;
+    }
+    /* The first port does not need a comma */
+    if(0 < port_counter){
+      fp << "," << std::endl;
+    }
+    /* Input port follows the logical block name while output port requires a special postfix */
+    if (VPACK_INPAD == lb.type){
+      fp << "\t\t" << std::string(lb.name);
+    } else {
+      VTR_ASSERT_SAFE(VPACK_OUTPAD == lb.type);
+      fp << "\t\t" << std::string(lb.name) << output_port_postfix;
+    }
+    /* Update the counter */
+    port_counter++;
+  }
+  fp << "\t);" << std::endl;
+}
+
+
+
+/********************************************************************
+ * Instanciate the input benchmark module
+ *******************************************************************/
+static
+void print_verilog_top_random_testbench_benchmark_instance(std::fstream& fp, 
+                                                           const std::string& reference_verilog_top_name,
+                                                           const std::vector<t_logical_block>& L_logical_blocks) {
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  /* Benchmark is instanciated conditionally: only when a preprocessing flag is enable */
+  print_verilog_preprocessing_flag(fp, std::string(autochecked_simulation_flag)); 
+
+  print_verilog_comment(fp, std::string("----- Reference Benchmark Instanication -------"));
+
+  print_verilog_random_testbench_instance(fp, reference_verilog_top_name,
+                                          std::string(reference_verilog_top_name + std::string(BENCHMARK_INSTANCE_NAME)),
+                                          std::string(BENCHMARK_PORT_POSTFIX), L_logical_blocks);
+
+  print_verilog_comment(fp, std::string("----- End reference Benchmark Instanication -------"));
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  /* Condition ends for the benchmark instanciation */
+  print_verilog_endif(fp);
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/********************************************************************
+ * Compute the time period for the simulation
+ *******************************************************************/
+static 
+int get_simulation_time(const int& num_op_clock_cycles,
+                        const float& op_clock_period) {
+  /* Take into account the prog_reset and reset cycles 
+   * 1e9 is to change the unit to ns rather than second 
+   */
+  return (MAGIC_NUMBER_FOR_SIMULATION_TIME * num_op_clock_cycles * op_clock_period) / verilog_sim_timescale; 
+}
+
+/********************************************************************
+ * Print Verilog codes to set up a timeout for the simulation 
+ * and dump the waveform to VCD files
+ *
+ * Note that: these codes are tuned for Icarus simulator!!!
+ *******************************************************************/
+static
+void print_verilog_timeout_and_vcd(std::fstream& fp,
+                                   const std::string& circuit_name,
+                                   const int& simulation_time) {
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  /* The following verilog codes are tuned for Icarus */
+  print_verilog_preprocessing_flag(fp, std::string(icarus_simulator_flag)); 
+
+  print_verilog_comment(fp, std::string("----- Begin Icarus requirement -------"));
+
+  fp << "\tinitial begin" << std::endl;
+  fp << "\t\t$dumpfile(\"" << circuit_name << "_formal.vcd\");" << std::endl;
+  fp << "\t\t$dumpvars(1, " << circuit_name << FORMAL_RANDOM_TOP_TESTBENCH_POSTFIX << ");" << std::endl;
+  fp << "\tend" << std::endl;
+
+  fp << "\tinitial begin" << std::endl;
+  fp << "\t\t$timeformat(-9, 2, \"ns\", 20);" << std::endl;
+  fp << "\t\t$display(\"Simulation start\");" << std::endl;
+  print_verilog_comment(fp, std::string("----- Can be changed by the user for his/her need -------"));
+  fp << "\t\t#" << simulation_time << std::endl;
+  fp << "\t\tif(" << ERROR_COUNTER << " == 0) begin" << std::endl;
+  fp << "\t\t\t$display(\"Simulation Succeed\");" << std::endl;
+  fp << "\t\tend else begin" << std::endl;
+  fp << "\t\t\t$display(\"Simulation Failed with " << std::string("%d") << " error(s)\", " << ERROR_COUNTER << ");" << std::endl;
+  fp << "\t\tend" << std::endl;
+  fp << "\t\t$finish;" << std::endl;
+  fp << "\tend" << std::endl;
+
+  print_verilog_comment(fp, std::string("----- END Icarus requirement -------"));
+
+  /* Condition ends for the Icarus requirement */
+  print_verilog_endif(fp);
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/********************************************************************
+ * Print Verilog codes to check the equivalence of output vectors 
+ *
+ * Restriction: this function only supports single clock benchmarks!
+ *******************************************************************/
+static
+void print_verilog_top_random_testbench_check(std::fstream& fp,
+                                              const std::vector<t_logical_block>& L_logical_blocks,
+                                              const std::vector<std::string>& clock_port_names) {
+
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  /* Add output autocheck conditionally: only when a preprocessing flag is enable */
+  print_verilog_preprocessing_flag(fp, std::string(autochecked_simulation_flag)); 
+
+  print_verilog_comment(fp, std::string("----- Begin checking output vectors -------"));
+
+  BasicPort clock_port = generate_verilog_top_clock_port(clock_port_names);
+
+  fp << "\talways@(negedge " << generate_verilog_port(VERILOG_PORT_CONKT, clock_port) << ") begin" << std::endl;
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if ( (VPACK_INPAD != lb.type) && (VPACK_OUTPAD != lb.type) ) {
+      continue;
+    }
+
+    if (VPACK_OUTPAD == lb.type){
+     fp << "\t\tif(!(" << std::string(lb.name) << std::string(FPGA_PORT_POSTFIX);
+     fp << " === " << std::string(lb.name) << std::string(BENCHMARK_PORT_POSTFIX);
+     fp << ") && !(" << std::string(lb.name) << std::string(BENCHMARK_PORT_POSTFIX);
+     fp << " === 1'bx)) begin" << std::endl;
+     fp << "\t\t\t" << std::string(lb.name) << std::string(CHECKFLAG_PORT_POSTFIX) << " <= 1'b1;" << std::endl;
+     fp << "\t\tend else begin" << std::endl;
+     fp << "\t\t\t" << std::string(lb.name) << std::string(CHECKFLAG_PORT_POSTFIX) << "<= 1'b0;" << std::endl;
+     fp << "\t\tend" << std::endl; 
+    }
+  } 
+  fp << "\tend" << std::endl;
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if (VPACK_OUTPAD != lb.type) {
+      continue;
+    }
+
+    fp << "\talways@(posedge " << std::string(lb.name) << std::string(CHECKFLAG_PORT_POSTFIX) << ") begin" << std::endl;
+    fp << "\t\tif(" << std::string(lb.name) << std::string(CHECKFLAG_PORT_POSTFIX) << ") begin" << std::endl;
+    fp << "\t\t\t" << ERROR_COUNTER << " = " << ERROR_COUNTER << " + 1;" << std::endl;
+    fp << "\t\t\t$display(\"Mismatch on " << std::string(lb.name) << std::string(FPGA_PORT_POSTFIX) << " at time = " << std::string("%t") << "\", $realtime);" << std::endl;
+    fp << "\t\tend" << std::endl;
+    fp << "\tend" << std::endl;
+
+    /* Add an empty line as splitter */
+    fp << std::endl;
+  }
+
+  /* Condition ends */
+  print_verilog_endif(fp);
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/********************************************************************
+ * Instanciate the FPGA fabric module
+ *******************************************************************/
+static
+void print_verilog_random_testbench_fpga_instance(std::fstream& fp,
+                                                  const std::string& circuit_name,
+                                                  const std::vector<t_logical_block>& L_logical_blocks) {
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  print_verilog_comment(fp, std::string("----- FPGA fabric instanciation -------"));
+
+
+  print_verilog_random_testbench_instance(fp, circuit_name,
+                                          std::string(circuit_name + std::string(formal_verification_top_postfix)),
+                                          std::string(FPGA_PORT_POSTFIX), L_logical_blocks);
+
+  print_verilog_comment(fp, std::string("----- End FPGA Fabric Instanication -------"));
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/********************************************************************
+ * Generate random stimulus for the input ports
+ *******************************************************************/
+static
+void print_verilog_top_random_stimuli(std::fstream& fp,
+                                      const t_spice_params& simulation_parameters,
+                                      const std::vector<t_logical_block>& L_logical_blocks,
+                                      const std::vector<std::string>& clock_port_names) {
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  print_verilog_comment(fp, std::string("----- Initialization -------"));
+
+  fp << "\tinitial begin" << std::endl;
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if ( (VPACK_INPAD != lb.type) && (VPACK_OUTPAD != lb.type) ) {
+      continue;
+    }
+
+    /* Clock ports will be initialized later */
+    if ( (VPACK_INPAD == lb.type) && (FALSE == lb.is_clock) ) {
+      fp << "\t\t" << std::string(lb.name) << " <= 1'b0;" << std::endl;
+    }
+  }
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+  
+  /* Creae clock stimuli */
+  BasicPort clock_port = generate_verilog_top_clock_port(clock_port_names);
+  fp << "\t" << generate_verilog_port(VERILOG_PORT_CONKT, clock_port) << " <= 1'b0;" << std::endl;
+  fp << "\twhile(1) begin" << std::endl;
+  fp << "\t\t#" << std::setprecision(2) << ((0.5/simulation_parameters.stimulate_params.op_clock_freq)/verilog_sim_timescale) << std::endl;
+  fp << "\t\t" << generate_verilog_port(VERILOG_PORT_CONKT, clock_port);
+  fp << " <= !";
+  fp << generate_verilog_port(VERILOG_PORT_CONKT, clock_port);
+  fp << ";" << std::endl;
+  fp << "\t\tend" << std::endl;
+  fp << "\tend" << std::endl;
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+
+  // Not ready yet to determine if input is reset
+/*
+  fprintf(fp, "//----- Reset Stimulis\n");      
+  fprintf(fp, "  initial begin\n");
+  fprintf(fp, "    #%.3f\n",(rand() % 10) + 0.001);
+  fprintf(fp, "    %s <= !%s;\n", reset_input_name, reset_input_name);
+  fprintf(fp, "    #%.3f\n",(rand() % 10) + 0.001);
+  fprintf(fp, "    %s <= !%s;\n", reset_input_name, reset_input_name);
+  fprintf(fp, "    while(1) begin\n");
+  fprintf(fp, "      #%.3f\n", (rand() % 15) + 0.5);
+  fprintf(fp, "      %s <= !%s;\n", reset_input_name, reset_input_name);
+  fprintf(fp, "      #%.3f\n", (rand() % 10000) + 200);
+  fprintf(fp, "      %s <= !%s;\n", reset_input_name, reset_input_name);
+  fprintf(fp, "    end\n");
+  fprintf(fp, "  end\n\n");  
+*/
+
+  print_verilog_comment(fp, std::string("----- Input Stimulus -------"));
+  fp << "\talways@(negedge " << generate_verilog_port(VERILOG_PORT_CONKT, clock_port) << ") begin" << std::endl;
+
+  for (const t_logical_block& lb : L_logical_blocks) {
+    /* Bypass non-I/O logical blocks ! */
+    if ( (VPACK_INPAD != lb.type) && (VPACK_OUTPAD != lb.type) ) {
+      continue;
+    }
+
+    /* Clock ports will be initialized later */
+    if ( (VPACK_INPAD == lb.type) && (FALSE == lb.is_clock) ) {
+      fp << "\t\t" << std::string(lb.name) << " <= $random;" << std::endl;
+    }
+  }
+
+  fp << "\tend" << std::endl;
+
+  /* Add an empty line as splitter */
+  fp << std::endl;
+}
+
+/*********************************************************************
+ * Top-level function in this file:
+ * Create a Verilog testbench using random input vectors 
+ * The testbench consists of two modules, i.e., Design Under Test (DUT)
+ * 1. top-level module of FPGA fabric
+ * 2. top-level module of users' benchmark, 
+ *    i.e., the input benchmark of VPR flow
+ *                                    +----------+
+ *                                    |   FPGA   |       +------------+
+ *                             +----->|  Fabric  |------>|            |
+ *                             |      |          |       |            |
+ *                             |      +----------+       |            |
+ *                             |                         | Output     | 
+ *   random_input_vectors -----+                         | Vector     |---->Functional correct?
+ *                             |                         | Comparator |    
+ *                             |      +-----------+      |            |
+ *                             |      |  Input    |      |            |
+ *                             +----->| Benchmark |----->|            |
+ *                                    +-----------+      +------------+
+ *
+ * Same input vectors are given to drive both DUTs.
+ * The output vectors of the DUTs are compared to verify if they
+ * have the same functionality.
+ * A flag will be raised to indicate the result 
+ ********************************************************************/
+void print_verilog_random_top_testbench(const std::string& circuit_name,
+                                        const std::string& verilog_fname,
+                                        const std::string& verilog_dir,
+                                        const std::vector<t_logical_block>& L_logical_blocks,
+                                        const t_syn_verilog_opts& fpga_verilog_opts,
+                                        const t_spice_params& simulation_parameters) {
+  vpr_printf(TIO_MESSAGE_INFO, 
+             "Writing Random Testbench for FPGA Top-level Verilog netlist for  %s...", 
+             circuit_name.c_str());
+
+  /* Start time count */
+  clock_t t_start = clock();
+
+  /* Create the file stream */
+  std::fstream fp;
+  fp.open(verilog_fname, std::fstream::out | std::fstream::trunc);
+
+  /* Validate the file stream */
+  check_file_handler(fp);
+
+  /* Generate a brief description on the Verilog file*/
+  std::string title = std::string("FPGA Verilog Testbench for Formal Top-level netlist of Design: ") + circuit_name;
+  print_verilog_file_header(fp, title); 
+
+  /* Print preprocessing flags and external netlists */
+  print_verilog_include_defines_preproc_file(fp, verilog_dir);
+
+  print_verilog_include_netlist(fp, std::string(verilog_dir + std::string(defines_verilog_simulation_file_name)));  
+
+  print_verilog_include_netlist(fp, std::string(fpga_verilog_opts.reference_verilog_benchmark_file));
+
+  /* Preparation: find all the clock ports */
+  std::vector<std::string> clock_port_names = find_verilog_top_clock_port_name(L_logical_blocks);
+
+  /* Start of testbench */
+  print_verilog_top_random_testbench_ports(fp, circuit_name, clock_port_names, L_logical_blocks);
+
+  /* Call defined top-level module */
+  print_verilog_random_testbench_fpga_instance(fp, circuit_name, L_logical_blocks);
+
+  /* Call defined benchmark */
+  print_verilog_top_random_testbench_benchmark_instance(fp, circuit_name, L_logical_blocks);
+
+  /* Add stimuli for reset, set, clock and iopad signals */
+  print_verilog_top_random_stimuli(fp, simulation_parameters, L_logical_blocks, clock_port_names);
+
+  print_verilog_top_random_testbench_check(fp, L_logical_blocks, clock_port_names);
+
+  int simulation_time = get_simulation_time(simulation_parameters.meas_params.sim_num_clock_cycle,
+                                            1./simulation_parameters.stimulate_params.op_clock_freq);
+
+  /* Add Icarus requirement */
+  print_verilog_timeout_and_vcd(fp, circuit_name, simulation_time);
+
+  /* Testbench ends*/
+  print_verilog_module_end(fp, std::string(circuit_name) + std::string(FORMAL_RANDOM_TOP_TESTBENCH_POSTFIX));
+
+  /* Close the file stream */
+  fp.close();
+
+  /* End time count */
+  clock_t t_end = clock();
+
+  float run_time_sec = (float)(t_end - t_start) / CLOCKS_PER_SEC;
+  vpr_printf(TIO_MESSAGE_INFO, 
+             "took %g seconds\n", 
+             run_time_sec);  
+}
+

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.h

@@ -1,8 +1,22 @@
+#ifndef VERILOG_FORMAL_RANDOME_TOP_TESTBENCH
+#define VERILOG_FORMAL_RANDOME_TOP_TESTBENCH
+
+#include <string>
+#include "vpr_types.h"
+#include "spice_types.h"
 
 void dump_verilog_random_top_testbench(t_sram_orgz_info* cur_sram_orgz_info,
-                                          char* circuit_name,
-                                          char* top_netlist_name,
-                                          char* verilog_dir_path,
-                                          t_syn_verilog_opts fpga_verilog_opts,
-                                          t_spice verilog);
+                                       char* circuit_name,
+                                       const char* top_netlist_name,
+                                       char* verilog_dir_path,
+                                       t_syn_verilog_opts fpga_verilog_opts,
+                                       t_spice verilog);
 
+void print_verilog_random_top_testbench(const std::string& circuit_name,
+                                        const std::string& verilog_fname,
+                                        const std::string& verilog_dir,
+                                        const std::vector<t_logical_block>& L_logical_blocks,
+                                        const t_syn_verilog_opts& fpga_verilog_opts,
+                                        const t_spice_params& simulation_parameters);
+
+#endif

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.cpp

@@ -43,23 +43,29 @@ void print_verilog_file_header(std::fstream& fp,
   fp << "\n";
 }
 
+/********************************************************************
+ * Print Verilog codes to include a netlist  
+ *******************************************************************/
+void print_verilog_include_netlist(std::fstream& fp, 
+                                   const std::string& netlist_name) {
+  check_file_handler(fp);
+
+  fp << "//------ Include external netlist: " << netlist_name << " -----" << std::endl;
+  fp << "`include \"" << netlist_name << "\"" << std::endl; 
+  fp << "//------ End include external netlist: " << netlist_name << " -----" << std::endl;
+}
 
 /************************************************
  * Generate include files for a Verilog netlist
  ***********************************************/
 void print_verilog_include_defines_preproc_file(std::fstream& fp, 
                                                 const std::string& verilog_dir) {
-  check_file_handler(fp);
   
   /* Generate the file name */
   std::string include_file_path = format_dir_path(verilog_dir);
   include_file_path += defines_verilog_file_name;
 
-  fp << "//------ Include defines: preproc flags -----" << std::endl;
-  fp << "`include \"" << include_file_path << "\"" << std::endl; 
-  fp << "//------ End Include defines: preproc flags -----" << std::endl << std::endl;
-
-  return;
+  print_verilog_include_netlist(fp, include_file_path); 
 }
 
 /************************************************

vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_writer_utils.h

@@ -21,6 +21,9 @@
 void print_verilog_file_header(std::fstream& fp,
                                const std::string& usage);
 
+void print_verilog_include_netlist(std::fstream& fp, 
+                                   const std::string& netlist_name);
+
 void print_verilog_include_defines_preproc_file(std::fstream& fp, 
                                                 const std::string& verilog_dir);