Merge d1eb2e518d into 29e8812bab

verific: fix blackbox regression and add test case

frontends/verific/verific.cc

@@ -2126,12 +2126,6 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 				log("    assert condition %s.\n", log_signal(cond));
 
 			Cell *cell = module->addAssert(new_verific_id(inst), cond, State::S1);
-			// Initialize FF feeding condition  to 1, in case it is not
-			// used by rest of design logic, to prevent failing on
-			// initial uninitialized state
-			if (cond.is_wire() && !cond.wire->name.isPublic())
-				cond.wire->attributes[ID::init] = Const(1,1);
-
 			import_attributes(cell->attributes, inst);
 			continue;
 		}
@@ -3428,6 +3422,7 @@ struct VerificPass : public Pass {
 			RuntimeFlags::SetVar("veri_preserve_assignments", 1);
 			RuntimeFlags::SetVar("veri_preserve_comments", 1);
 			RuntimeFlags::SetVar("veri_preserve_drivers", 1);
+			RuntimeFlags::SetVar("veri_create_empty_box", 1);
 
 			// Workaround for VIPER #13851
 			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);

tests/arch/common/blockram.v

@@ -32,6 +32,8 @@ module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
   localparam DEPTH = (2**ADDRESS_WIDTH-1);
 
   reg [WORD:0] data_out_r;
+
+  (* no_rw_check *)
   reg [WORD:0] memory [0:DEPTH];
 
   always @(posedge clk) begin

tests/arch/ecp5/memories.ys

@@ -6,6 +6,7 @@ chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
 hierarchy -top sync_ram_sdp
 synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp
 select -assert-count 1 t:DP16KD
+select -assert-none t:LUT4
 
 ## With parameters
 

tests/arch/gatemate/memory.ys

@@ -5,6 +5,9 @@ synth_gatemate -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:CC_BUFG
 select -assert-count 1 t:CC_BRAM_20K
+select -assert-none t:CC_LUT3
+select -assert-none t:CC_LUT4
+select -assert-none t:CC_DFF
 
 # 512 x 20 bit x 2 -> CC_BRAM_20K TDP RAM
 design -reset

tests/arch/ice40/memories.ys

@@ -6,6 +6,8 @@ chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 2 sync_ram_sdp
 hierarchy -top sync_ram_sdp
 synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp
 select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_LUT4
+select -assert-none t:SB_DFF
 
 design -reset; read_verilog -defer ../common/blockram.v
 chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 4 sync_ram_sdp

tests/verific/blackbox.ys

@@ -0,0 +1,24 @@
+verific -sv -lib <<EOF
+module TEST_CELL(input clk, input a, input b, output reg c);
+parameter PATH = "DEFAULT";
+always @(posedge clk) begin
+    if (PATH=="DEFAULT")
+		c <= a;
+	else 
+		c <= b;
+end
+
+endmodule
+EOF
+
+verific -sv <<EOF
+module top(input clk, input a, input b, output c, output d);
+	TEST_CELL  #(.PATH("TEST")) test1(.clk(clk),.a(a),.b(1'b1),.c(c));
+	TEST_CELL  #(.PATH("DEFAULT")) test2(.clk(clk),.a(a),.b(1'bx),.c(d));
+endmodule
+EOF
+
+verific -import top
+hierarchy -top top
+stat
+select -assert-count 2 t:TEST_CELL