Merge

backends/btor/btor.cc

@@ -832,7 +832,10 @@ struct BtorWorker
 					}
 				}
 
-				if (constword)
+				// If not fully defined, undef bits should be able to take a
+				// different value for each address so we can't initialise from
+				// one value (and btor2parser doesn't like it)
+				if (constword && firstword.is_fully_def())
 				{
 					if (verbose)
 						btorf("; initval = %s\n", log_signal(firstword));
@@ -1077,6 +1080,7 @@ struct BtorWorker
 							btorf("%d input %d\n", nid, sid);
 							ywmap_input(s);
 							nid_width[nid] = GetSize(s);
+							add_nid_sig(nid, s);
 
 							for (int j = 0; j < GetSize(s); j++)
 								nidbits.push_back(make_pair(nid, j));

backends/cxxrtl/cxxrtl_backend.cc

@@ -612,7 +612,7 @@ std::string escape_c_string(const std::string &input)
 	output.push_back('"');
 	for (auto c : input) {
 		if (::isprint(c)) {
-			if (c == '\\')
+			if (c == '\\' || c == '"')
 				output.push_back('\\');
 			output.push_back(c);
 		} else {

backends/smt2/smt2.cc

@@ -329,12 +329,13 @@ struct Smt2Worker
 	{
 		sigmap.apply(bit);
 
-		if (bit.wire == nullptr)
+		if (bit_driver.count(bit)) {
-			return bit == RTLIL::State::S1 ? "true" : "false";
-
-		if (bit_driver.count(bit))
 			export_cell(bit_driver.at(bit));
 			sigmap.apply(bit);
+		}
+
+		if (bit.wire == nullptr)
+			return bit == RTLIL::State::S1 ? "true" : "false";
 
 		if (fcache.count(bit) == 0) {
 			if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",

kernel/fmt.cc

@@ -630,7 +630,7 @@ std::string escape_cxx_string(const std::string &input)
 	std::string output = "\"";
 	for (auto c : input) {
 		if (::isprint(c)) {
-			if (c == '\\')
+			if (c == '\\' || c == '"')
 				output.push_back('\\');
 			output.push_back(c);
 		} else {

misc/py_wrap_generator.py

@@ -375,6 +375,10 @@ class PoolTranslator(PythonListTranslator):
 	insert_name = ".insert"
 	orig_name = "pool"
 
+#Sub-type for ObjRange
+class ObjRangeTranslator(PythonListTranslator):
+	orig_name = "RTLIL::ObjRange"
+
 #Translates dict-types (dict, std::map), that only differ in their name and
 #the name of the insertion function
 class PythonDictTranslator(Translator):
@@ -542,7 +546,8 @@ known_containers = {
 	"idict"           : IDictTranslator,
 	"dict"            : DictTranslator,
 	"std::pair"       : TupleTranslator,
-	"std::map"		:	MapTranslator
+	"std::map"        : MapTranslator,
+	"RTLIL::ObjRange" : ObjRangeTranslator
 }
 
 class Attribute:

passes/pmgen/Makefile.inc

@@ -59,6 +59,7 @@ PEEPOPT_PATTERN += passes/pmgen/peepopt_shiftadd.pmg
 PEEPOPT_PATTERN += passes/pmgen/peepopt_muldiv.pmg
 PEEPOPT_PATTERN += passes/pmgen/peepopt_muldiv_c.pmg
 PEEPOPT_PATTERN += passes/pmgen/peepopt_muxadd.pmg
+PEEPOPT_PATTERN += passes/pmgen/peepopt_formal_clockgateff.pmg
 
 passes/pmgen/peepopt_pm.h: passes/pmgen/pmgen.py $(PEEPOPT_PATTERN)
 	$(P) mkdir -p passes/pmgen && $(PYTHON_EXECUTABLE) $< -o $@ -p peepopt $(filter-out $<,$^)

passes/pmgen/peepopt.cc

@@ -40,7 +40,7 @@ struct PeepoptPass : public Pass {
 		log("\n");
 		log("This pass applies a collection of peephole optimizers to the current design.\n");
 		log("\n");
-		log("This pass employs the following rules:\n");
+		log("This pass employs the following rules by default:\n");
 		log("\n");
 		log("   * muxadd - Replace S?(A+B):A with A+(S?B:0)\n");
 		log("\n");
@@ -61,14 +61,26 @@ struct PeepoptPass : public Pass {
 		log("                limits the amount of padding to a multiple of the data, \n");
 		log("                to avoid high resource usage from large temporary MUX trees.\n");
 		log("\n");
+		log("If -formalclk is specified it instead employs the following rules:\n");
+		log("\n");
+		log("   * clockgateff - Replace latch based clock gating patterns with a flip-flop\n");
+		log("                   based pattern to prevent combinational paths from the\n");
+		log("                   output to the enable input after running clk2fflogic.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		log_header(design, "Executing PEEPOPT pass (run peephole optimizers).\n");
 
+		bool formalclk = false;
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
+			if (args[argidx] == "-formalclk") {
+				formalclk = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -90,6 +102,9 @@ struct PeepoptPass : public Pass {
 
 				pm.setup(module->selected_cells());
 
+				if (formalclk) {
+					pm.run_formal_clockgateff();
+				} else {
 					pm.run_shiftadd();
 					pm.run_shiftmul_right();
 					pm.run_shiftmul_left();
@@ -99,6 +114,7 @@ struct PeepoptPass : public Pass {
 				}
 			}
 		}
+	}
 } PeepoptPass;
 
 PRIVATE_NAMESPACE_END

passes/pmgen/peepopt_formal_clockgateff.pmg

@@ -0,0 +1,59 @@
+pattern formal_clockgateff
+
+// Detects the most common clock gating pattern using a latch and replaces it
+// with a functionally equivalent pattern based on a flip-flop. The latch
+// based pattern has a combinational path from the enable input to output after
+// clk2fflogic, but this is a stable loop and the flip-flop based pattern does
+// not exhibit this.
+//
+// This optimization is suitable for formal to prevent false comb loops, but
+// should not be used for synthesis where the latch is an intentional choice
+//
+// Latch style:
+// always @* if (!clk_i) latched_en = en;
+// assign gated_clk_o = latched_en & clk_i;
+//
+// Flip-flop style:
+// always @(posedge clk) flopped_en <= en;
+// assign gated_clk_o = flopped_en & clk_i;
+
+state <SigSpec> clk en latched_en gated_clk
+state <IdString> latched_en_port_name
+
+match latch
+	select latch->type == $dlatch
+	select param(latch, \WIDTH) == 1
+	select param(latch, \EN_POLARITY).as_bool() == false
+	set clk port(latch, \EN)
+	set en port(latch, \D)
+	set latched_en port(latch, \Q)
+endmatch
+
+match and_gate
+	select and_gate->type.in($and, $logic_and)
+	select param(and_gate, \A_WIDTH) == 1
+	select param(and_gate, \B_WIDTH) == 1
+	select param(and_gate, \Y_WIDTH) == 1
+	choice <IdString> clk_port {\A, \B}
+	define <IdString> latch_port {clk_port == \A ? \B : \A}
+	index <SigSpec> port(and_gate, clk_port) === clk
+	index <SigSpec> port(and_gate, latch_port) === latched_en
+	set gated_clk port(and_gate, \Y)
+	set latched_en_port_name latch_port
+endmatch
+
+code
+	log("replacing clock gate pattern in %s with ff: latch=%s, and=%s\n",
+		log_id(module), log_id(latch), log_id(and_gate));
+
+	// Add a flip-flop and rewire the AND gate to use the output of this flop
+	// instead of the latch. We don't delete the latch in case its output is
+	// used to drive other nodes. If it isn't, it will be trivially removed by
+	// clean
+	SigSpec flopped_en = module->addWire(NEW_ID);
+	module->addDff(NEW_ID, clk, en, flopped_en, true, latch->get_src_attribute());
+	and_gate->setPort(latched_en_port_name, flopped_en);
+	did_something = true;
+
+	accept;
+endcode

passes/sat/clk2fflogic.cc

@@ -51,6 +51,10 @@ struct Clk2fflogicPass : public Pass {
 		log("    -nolower\n");
 		log("        Do not automatically run 'chformal -lower' to lower $check cells.\n");
 		log("\n");
+		log("    -nopeepopt\n");
+		log("        Do not automatically run 'peepopt -formalclk' to rewrite clock patterns\n");
+		log("        to more formal friendly forms.\n");
+		log("\n");
 	}
 	// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
 	SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
@@ -121,6 +125,7 @@ struct Clk2fflogicPass : public Pass {
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		bool flag_nolower = false;
+		bool flag_nopeepopt = false;
 
 		log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
 
@@ -131,10 +136,20 @@ struct Clk2fflogicPass : public Pass {
 				flag_nolower = true;
 				continue;
 			}
+			if (args[argidx] == "-nopeepopt") {
+				flag_nopeepopt = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
+		if (!flag_nopeepopt) {
+			log_push();
+			Pass::call(design, "peepopt -formalclk");
+			log_pop();
+		}
+
 		bool have_check_cells = false;
 
 		for (auto module : design->selected_modules())

tests/various/peepopt_formal.ys

@@ -0,0 +1,45 @@
+read_verilog -sv <<EOT
+module peepopt_formal_clockgateff_0(
+	input  logic clk_i,
+	input  logic ena_i,
+	input  logic enb_i,
+	output logic clk_o
+);
+
+logic en_latched;
+
+always_latch
+	if (!clk_i)
+		en_latched <= ena_i | enb_i;
+
+assign clk_o = en_latched & clk_i;
+
+endmodule
+EOT
+
+# Check original design has latch
+prep -auto-top
+select -assert-count 1 t:$dlatch
+select -assert-count 0 t:$dff
+
+# Manually execute equiv_opt like pattern so clk2fflogic is called with
+# -nopeepopt, otherwise this doesn't test anything
+design -save preopt
+check -assert
+peepopt -formalclk
+check -assert
+design -stash postopt
+
+# Create miter and clk2fflogic without peepopt
+design -copy-from preopt -as gold A:top
+design -copy-from postopt -as gate A:top
+clk2fflogic -nopeepopt
+equiv_make gold gate equiv
+equiv_induct equiv
+equiv_status -assert equiv
+
+# Check final design has dff instead of latch
+design -load postopt
+clean
+select -assert-count 0 t:$dlatch
+select -assert-count 1 t:$dff