verific: Improve logic generated for SVA value change expressions

The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

	a) provides the expected behavior in a 2-valued logic setting, not
	   depending on any dont-care optimizations, and

	b) properly handles 'x values in yosys simulation

1 files changed, 25 insertions, 10 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index d19d837ff..145a5acf2 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1557,17 +1557,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 
 			SigSpec sig_d = net_map_at(inst->GetInput1());
 			SigSpec sig_o = net_map_at(inst->GetOutput());
-			SigSpec sig_q = module->addWire(new_verific_id(inst));
+			SigSpec sig_dx = module->addWire(new_verific_id(inst), 2);
+			SigSpec sig_qx = module->addWire(new_verific_id(inst), 2);
 
 			if (verific_verbose) {
+				log("    NEX with A=%s, B=0, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_dx[0]));
+				log("    EQX with A=%s, B=1, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_dx[1]));
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
-						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
-				log("    XNOR with A=%s, B=%s, Y=%s.\n",
-						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+						log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig));
+				log("    EQ with A=%s, B=%s, Y=%s.\n",
+						log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_o));
 			}
 
-			clocking.addDff(new_verific_id(inst), sig_d, sig_q);
-			module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
+			module->addNex(new_verific_id(inst), sig_d, State::S0, sig_dx[0]);
+			module->addEqx(new_verific_id(inst), sig_d, State::S1, sig_dx[1]);
+
+			clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, Const(1, 2));
+			module->addEq(new_verific_id(inst), sig_dx, sig_qx, sig_o);
 
 			if (!mode_keep)
 				continue;
@@ -1601,13 +1609,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 			SigBit sig_d = net_map_at(inst->GetInput1());
 			SigBit sig_o = net_map_at(inst->GetOutput());
 			SigBit sig_q = module->addWire(new_verific_id(inst));
+			SigBit sig_d_no_x = module->addWire(new_verific_id(inst));
 
-			if (verific_verbose)
+			if (verific_verbose) {
+				log("    EQX with A=%s, B=%d, Y=%s.\n",
+						log_signal(sig_d), inst->Type() == PRIM_SVA_ROSE, log_signal(sig_d_no_x));
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
-						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+						log_signal(sig_d_no_x), log_signal(sig_q), log_signal(clocking.clock_sig));
+				log("    EQ with A={%s, %s}, B={0, 1}, Y=%s.\n",
+						log_signal(sig_q), log_signal(sig_d_no_x), log_signal(sig_o));
+			}
 
-			clocking.addDff(new_verific_id(inst), sig_d, sig_q);
-			module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
+			module->addEqx(new_verific_id(inst), sig_d, inst->Type() == PRIM_SVA_ROSE ? State::S1 : State::S0, sig_d_no_x);
+			clocking.addDff(new_verific_id(inst), sig_d_no_x, sig_q, State::S0);
+			module->addEq(new_verific_id(inst), {sig_q, sig_d_no_x}, Const(1, 2), sig_o);
 
 			if (!mode_keep)
 				continue;