diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.c b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.c
index dd2b8faf6..1389815a8 100644
--- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.c
+++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_formal_random_top_testbench.c
@@ -222,12 +222,17 @@ void dump_verilog_top_random_testbench_check(FILE* fp){
       assert((VPACK_INPAD == logical_block[iblock].type)
            ||(VPACK_OUTPAD == logical_block[iblock].type));
       if(VPACK_OUTPAD == logical_block[iblock].type){
-        fprintf(fp, "    %s%s <= %s%s ^ %s%s ;\n", logical_block[iblock].name, 
-                									flag_postfix,
-                									logical_block[iblock].name,  
-               										gfpga_postfix,
-                									logical_block[iblock].name, 
-                									bench_postfix);
+        fprintf(fp, "    if(!(%s%s === %s%s) && !(%s%s === 1'bx)) begin\n",
+                                                        logical_block[iblock].name,  
+               									 	    gfpga_postfix,
+                									    logical_block[iblock].name, 
+                									    bench_postfix,
+                									    logical_block[iblock].name, 
+                									    bench_postfix);
+        fprintf(fp, "      %s%s <= 1'b1;\n", logical_block[iblock].name, 
+                									flag_postfix);
+        fprintf(fp, "    end else begin\n      %s%s <= 1'b0;\n    end\n", logical_block[iblock].name, 
+                									                      flag_postfix);
       }
     }
   } 
diff --git a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_submodules.c b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_submodules.c
index c63de39e4..08f53ea0f 100644
--- a/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_submodules.c
+++ b/vpr7_x2p/vpr/SRC/fpga_x2p/verilog/verilog_submodules.c
@@ -104,10 +104,17 @@ void dump_verilog_submodule_signal_init(FILE* fp,
   fprintf(fp, "initial begin\n");
 //  fprintf(fp, "`ifdef %s\n  #0.001\n`endif\n", 			// Commented, looks no longer needed
 //				icarus_simulator_flag);
+  fprintf(fp, "  `ifdef %s\n", verilog_formal_verification_preproc_flag);
+  for (iport = 0; iport < num_input_port; iport++) {
+     fprintf(fp, "  $deposit(%s, 1'b0);\n",
+                input_port[iport]->lib_name);
+  }
+  fprintf(fp, "  `else\n");
   for (iport = 0; iport < num_input_port; iport++) {
      fprintf(fp, "  $deposit(%s, $random);\n",
                 input_port[iport]->lib_name);
   }
+  fprintf(fp, "  `endif\n");
   fprintf(fp, "end\n");
   fprintf(fp, "  //------ END driver initialization -----\n");
   fprintf(fp, "`endif\n");
@@ -233,8 +240,9 @@ void dump_verilog_invbuf_module(FILE* fp,
                   output_port[0]->lib_name,
                   output_port[0]->lib_name);
     } else {
-      fprintf(fp, "assign %s = ~%s;\n",
+      fprintf(fp, "assign %s = (%s === 1'bz)? $random : ~%s;\n",
                   output_port[0]->lib_name,
+                  input_port[0]->lib_name,
                   input_port[0]->lib_name);
     }
     break;
@@ -296,13 +304,15 @@ void dump_verilog_invbuf_module(FILE* fp,
                   output_port[0]->lib_name);
 
     } else if (FALSE == invbuf_spice_model->design_tech_info.buffer_info->tapered_buf) {
-      fprintf(fp, "assign %s = %s;\n",
+      fprintf(fp, "assign %s = (%s === 1'bz)? $random : %s;\n",
                   output_port[0]->lib_name,
+                  input_port[0]->lib_name,
                   input_port[0]->lib_name);
     } else {
       assert (TRUE == invbuf_spice_model->design_tech_info.buffer_info->tapered_buf);
-      fprintf(fp, "assign %s = ",
-                  output_port[0]->lib_name);
+      fprintf(fp, "assign %s = (%s === 1'bz)? $random : ",
+                  output_port[0]->lib_name,
+                  input_port[0]->lib_name);
       /* depend on the stage, we may invert the output */
       if (1 == invbuf_spice_model->design_tech_info.buffer_info->tap_buf_level % 2) {
         fprintf(fp, "~");
diff --git a/vpr7_x2p/vpr/regression_verilog.sh b/vpr7_x2p/vpr/regression_verilog.sh
index 293d9e551..e19875026 100644
--- a/vpr7_x2p/vpr/regression_verilog.sh
+++ b/vpr7_x2p/vpr/regression_verilog.sh
@@ -33,7 +33,7 @@ perl rewrite_path_in_file.pl -i $arch_xml_file -k $arch_ff_keyword $new_ff_path
 cd -
 
 # Run VPR  
-./vpr $arch_xml_file $blif_file --full_stats --nodisp --activity_file $act_file --fpga_verilog --fpga_verilog_dir $verilog_output_dirpath/$verilog_output_dirname --fpga_x2p_rename_illegal_port --fpga_bitstream_generator --fpga_verilog_print_top_testbench --fpga_verilog_print_input_blif_testbench --fpga_verilog_include_timing --fpga_verilog_include_signal_init --fpga_verilog_print_formal_verification_top_netlist --fpga_verilog_print_autocheck_top_testbench $verilog_reference --fpga_verilog_print_user_defined_template --route_chan_width $vpr_route_chan_width --fpga_verilog_include_icarus_simulator --fpga_verilog_print_report_timing_tcl --power --tech_properties $tech_file --fpga_verilog_print_sdc_pnr --fpga_verilog_print_sdc_analysis --fpga_x2p_compact_routing_hierarchy 
+./vpr $arch_xml_file $blif_file --full_stats --nodisp --activity_file $act_file --fpga_verilog --fpga_verilog_dir $verilog_output_dirpath/$verilog_output_dirname --fpga_x2p_rename_illegal_port --fpga_bitstream_generator --fpga_verilog_print_top_testbench --fpga_verilog_print_input_blif_testbench --fpga_verilog_include_timing --fpga_verilog_include_signal_init --fpga_verilog_print_formal_verification_top_netlist --fpga_verilog_print_autocheck_top_testbench $verilog_reference --fpga_verilog_print_user_defined_template --route_chan_width $vpr_route_chan_width --fpga_verilog_include_icarus_simulator --fpga_verilog_print_report_timing_tcl --power --tech_properties $tech_file --fpga_verilog_print_sdc_pnr --fpga_verilog_print_sdc_analysis #--fpga_x2p_compact_routing_hierarchy 
 
 cd $fpga_flow_scripts
 perl rewrite_path_in_file.pl -i $ff_path -o $new_ff_path -k $ff_keyword $ff_include_path