Merge pull request #2131 from YosysHQ/claire/preserveffs

Do not optimize away FFs in "prep" and Verific front-end

6 files changed, 50 insertions, 33 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 65e71876a..a22a8a93d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -2180,6 +2180,9 @@ struct VerificPass : public Pass {
 			RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
 			RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
 
+			RuntimeFlags::SetVar("veri_preserve_assignments", 1);
+			RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
+
 			// Workaround for VIPER #13851
 			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
 
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index 396819883..b852e6ae8 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,8 +44,8 @@ struct OptPass : public Pass {
 		log("        opt_muxtree\n");
 		log("        opt_reduce [-fine] [-full]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_share (-full only)\n");
-		log("        opt_rmdff [-keepdc] [-sat]\n");
+		log("        opt_share  (-full only)\n");
+		log("        opt_rmdff [-keepdc] [-sat]  (except when called with -noff)\n");
 		log("        opt_clean [-purge]\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("    while <changed design>\n");
@@ -55,7 +55,7 @@ struct OptPass : public Pass {
 		log("    do\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff [-keepdc] [-sat]\n");
+		log("        opt_rmdff [-keepdc] [-sat]  (except when called with -noff)\n");
 		log("        opt_clean [-purge]\n");
 		log("    while <changed design in opt_rmdff>\n");
 		log("\n");
@@ -73,6 +73,7 @@ struct OptPass : public Pass {
 		std::string opt_rmdff_args;
 		bool opt_share = false;
 		bool fast_mode = false;
+		bool noff_mode = false;
 
 		log_header(design, "Executing OPT pass (performing simple optimizations).\n");
 		log_push();
@@ -127,6 +128,10 @@ struct OptPass : public Pass {
 				fast_mode = true;
 				continue;
 			}
+			if (args[argidx] == "-noff") {
+				noff_mode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -137,7 +142,8 @@ struct OptPass : public Pass {
 				Pass::call(design, "opt_expr" + opt_expr_args);
 				Pass::call(design, "opt_merge" + opt_merge_args);
 				design->scratchpad_unset("opt.did_something");
-				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
+				if (!noff_mode)
+					Pass::call(design, "opt_rmdff" + opt_rmdff_args);
 				if (design->scratchpad_get_bool("opt.did_something") == false)
 					break;
 				Pass::call(design, "opt_clean" + opt_clean_args);
@@ -156,7 +162,8 @@ struct OptPass : public Pass {
 				Pass::call(design, "opt_merge" + opt_merge_args);
 				if (opt_share)
 					Pass::call(design, "opt_share");
-				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
+				if (!noff_mode)
+					Pass::call(design, "opt_rmdff" + opt_rmdff_args);
 				Pass::call(design, "opt_clean" + opt_clean_args);
 				Pass::call(design, "opt_expr" + opt_expr_args);
 				if (design->scratchpad_get_bool("opt.did_something") == false)
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 6acdbc800..e2fe5b846 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -256,13 +256,13 @@ struct SatHelper
 		{
 			RTLIL::SigSpec big_lhs, big_rhs;
 
-			for (auto &it : module->wires_)
+			for (auto wire : module->wires())
 			{
-				if (it.second->attributes.count(ID::init) == 0)
+				if (wire->attributes.count(ID::init) == 0)
 					continue;
 
-				RTLIL::SigSpec lhs = sigmap(it.second);
-				RTLIL::SigSpec rhs = it.second->attributes.at(ID::init);
+				RTLIL::SigSpec lhs = sigmap(wire);
+				RTLIL::SigSpec rhs = wire->attributes.at(ID::init);
 				log_assert(lhs.size() == rhs.size());
 
 				RTLIL::SigSpec removed_bits;
diff --git a/techlibs/common/prep.cc b/techlibs/common/prep.cc
index cdd21c3b3..82e6126c6 100644
--- a/techlibs/common/prep.cc
+++ b/techlibs/common/prep.cc
@@ -192,7 +192,7 @@ struct PrepPass : public ScriptPass
 			run(nokeepdc ? "opt_expr" : "opt_expr -keepdc");
 			run("opt_clean");
 			run("check");
-			run(nokeepdc ? "opt" : "opt -keepdc");
+			run(nokeepdc ? "opt -noff" : "opt -noff -keepdc");
 			if (!ifxmode) {
 				if (help_mode)
 					run("wreduce -keepdc [-memx]");
@@ -208,7 +208,7 @@ struct PrepPass : public ScriptPass
 				run("opt_clean");
 				run("memory_collect");
 			}
-			run(nokeepdc ? "opt -fast" : "opt -keepdc -fast");
+			run(nokeepdc ? "opt -noff -fast" : "opt -noff -keepdc -fast");
 		}
 
 		if (check_label("check"))
diff --git a/tests/opt/opt_rmdff.v b/tests/opt/opt_rmdff.v
index b1c06703c..536bf1d4e 100644
--- a/tests/opt/opt_rmdff.v
+++ b/tests/opt/opt_rmdff.v
@@ -1,50 +1,50 @@
 module opt_rmdff_test (input C, input D, input E, output [29:0] Q);
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove0 (.CLK(C), .D(D), .EN(1'b0), .Q(Q[0])); // EN is never active
-(* init = "1'b1" *) wire Q1; assign Q[1] = Q1;
+(* init = 1'b1 *) wire Q1; assign Q[1] = Q1;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove1 (.CLK(C), .D(D), .EN(1'b0), .Q(Q1)); // EN is never active
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove2 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[2])); // EN is don't care
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep3 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[3])); // EN is always active
-(* init = "1'b0" *) wire Q4; assign Q[4] = Q4;
+(* init = 1'b0 *) wire Q4; assign Q[4] = Q4;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) keep4 (.CLK(C), .D(D), .EN(1'b1), .Q(Q4)); // EN is always active
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove5 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[5])); // EN is never active
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove6 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[6])); // EN is don't care
-(* init = "1'b0" *) wire Q7; assign Q[7] = Q7;
+(* init = 1'b0 *) wire Q7; assign Q[7] = Q7;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(0)) keep7 (.CLK(C), .D(D), .EN(E), .Q(Q7)); // EN is non constant
 
 \$_DFFE_PP_ remove8 (.C(C), .D(D), .E(1'b0), .Q(Q[8])); // EN is never active
-(* init = "1'b1" *) wire Q9; assign Q[9] = Q9;
+(* init = 1'b1 *) wire Q9; assign Q[9] = Q9;
 \$_DFFE_PP_ remove9 (.C(C), .D(D), .E(1'b0), .Q(Q9)); // EN is never active
 \$_DFFE_PP_ remove10 (.C(C), .D(D), .E(1'bx), .Q(Q[10])); // EN is don't care
 \$_DFFE_PP_ keep11 (.C(C), .D(D), .E(1'b1), .Q(Q[11])); // EN is always active
-(* init = "1'b0" *) wire Q12; assign Q[12] = Q12;
+(* init = 1'b0 *) wire Q12; assign Q[12] = Q12;
 \$_DFFE_PP_ keep12 (.C(C), .D(D), .E(1'b1), .Q(Q12)); // EN is always active
 
 \$_DFFE_NN_ remove13 (.C(C), .D(D), .E(1'b1), .Q(Q[13])); // EN is never active
-(* init = "1'b1" *) wire Q14; assign Q[14] = Q14;
+(* init = 1'b1 *) wire Q14; assign Q[14] = Q14;
 \$_DFFE_NN_ remove14 (.C(C), .D(D), .E(1'b1), .Q(Q14)); // EN is never active
 \$_DFFE_NN_ remove15 (.C(C), .D(D), .E(1'bx), .Q(Q[15])); // EN is don't care
 \$_DFFE_NN_ keep16 (.C(C), .D(D), .E(1'b0), .Q(Q[16])); // EN is always active
-(* init = "1'b0" *) wire Q17; assign Q[17] = Q17;
+(* init = 1'b0 *) wire Q17; assign Q[17] = Q17;
 \$_DFFE_NN_ keep17 (.C(C), .D(D), .E(1'b0), .Q(Q17)); // EN is always active
 
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove18 (.CLK(1'b0), .D(D), .EN(E), .Q(Q[18])); // CLK is constant
-(* init = "1'b1" *) wire Q19; assign Q[19] = Q19;
+(* init = 1'b1 *) wire Q19; assign Q[19] = Q19;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove19 (.CLK(1'b1), .D(D), .EN(E), .Q(Q19)); // CLK is constant
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove20 (.CLK(C), .D(1'bx), .EN(E), .Q(Q[20])); // D is undriven, Q has no initial value
-(* init = "1'b0" *) wire Q21; assign Q[21] = Q21;
+(* init = 1'b0 *) wire Q21; assign Q[21] = Q21;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep21 (.CLK(C), .D(1'bx), .EN(E), .Q(Q21)); // D is undriven, Q has initial value
 //\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) remove22 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q[22])); // D is constant, no initial Q value, EN is always active
 //                                                                                                           // (TODO, Q starts with 1'bx and becomes 1'b0)
-(* init = "1'b0" *) wire Q23; assign Q[23] = Q23;
+(* init = 1'b0 *) wire Q23; assign Q[23] = Q23;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) noenable23 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q23)); // D is constant, initial Q value same as D, EN is always active
-(* init = "1'b1" *) wire Q24; assign Q[24] = Q24;
+(* init = 1'b1 *) wire Q24; assign Q[24] = Q24;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) keep24 (.CLK(C), .D(1'b0), .EN(1'b0), .Q(Q24)); // D is constant, initial Q value NOT same as D, EN is always active
-(* init = "1'b1" *) wire Q25; assign Q[25] = Q25;
+(* init = 1'b1 *) wire Q25; assign Q[25] = Q25;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove25 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q25)); // D is constant, EN is never active
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove26 (.CLK(C), .D(Q[26]), .EN(1'b1), .Q(Q[26])); // D is Q, EN is always active
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove27 (.CLK(C), .D(Q[27]), .EN(1'b1), .Q(Q[27])); // D is Q, EN is never active, but no initial value
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove28 (.CLK(C), .D(Q[28]), .EN(E), .Q(Q[28])); // EN is nonconst, but no initial value
-(* init = "1'b1" *) wire Q29; assign Q[29] = Q29;
+(* init = 1'b1 *) wire Q29; assign Q[29] = Q29;
 \$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep29 (.CLK(C), .D(Q[29]), .EN(1'b1), .Q(Q29)); // EN is always active, but with initial value
 
 endmodule
diff --git a/tests/opt/opt_rmdff.ys b/tests/opt/opt_rmdff.ys
index 83a162f44..7e11bc73f 100644
--- a/tests/opt/opt_rmdff.ys
+++ b/tests/opt/opt_rmdff.ys
@@ -1,6 +1,7 @@
 read_verilog -icells opt_rmdff.v
 prep
 design -stash gold
+
 read_verilog -icells opt_rmdff.v
 proc
 opt_rmdff
@@ -14,13 +15,19 @@ design -stash gate
 design -import gold -as gold
 design -import gate -as gate
 
-equiv_make gold gate equiv
-hierarchy -top equiv
-equiv_simple -undef
-equiv_status -assert
+cd gold
+# fix up the "EN is don't care" cases, so that the gold output can't
+# become defined by using the properties of an undefined enable. (Both
+# remove6 and remove15 have active-low enables.)
+connect -port remove6 EN 1'b1
+connect -port remove15 E 1'b1
+cd ..
+
+dff2dffe -unmap
+clk2fflogic
+opt_clean
+
+miter -equiv -ignore_gold_x -make_assert -make_outputs -make_outcmp -flatten gold gate miter
+hierarchy -top miter
 
-#design -load gold
-#stat
-#
-#design -load gate
-#stat
+sat -verify -prove-asserts -enable_undef -set-init-undef -seq 10 -show-public miter