Merge 884f40df11 into 4b3c03dabc

frontends/verific/verific.cc

@@ -2126,6 +2126,12 @@ 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;
 		}
@@ -3422,7 +3428,6 @@ 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/verific/blackbox.ys

@@ -1,24 +0,0 @@
-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