diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index c3637bc8f..43d189679 100644 --- a/backends/btor/btor.cc +++ b/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)); diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index a56bfc036..1c22e7ae9 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/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 { diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 55c5c03f5..a6e1965ba 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -329,13 +329,14 @@ struct Smt2Worker { sigmap.apply(bit); + 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 (bit_driver.count(bit)) - export_cell(bit_driver.at(bit)); - sigmap.apply(bit); - if (fcache.count(bit) == 0) { if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "", log_signal(bit)); diff --git a/kernel/fmt.cc b/kernel/fmt.cc index d1c6b8ac9..6ba1150ce 100644 --- a/kernel/fmt.cc +++ b/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 { diff --git a/misc/py_wrap_generator.py b/misc/py_wrap_generator.py index c49c375cd..4e7d83922 100644 --- a/misc/py_wrap_generator.py +++ b/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): @@ -536,13 +540,14 @@ class TupleTranslator(PythonDictTranslator): #Associate the Translators with their c++ type known_containers = { - "std::set" : SetTranslator, - "std::vector" : VectorTranslator, - "pool" : PoolTranslator, - "idict" : IDictTranslator, - "dict" : DictTranslator, - "std::pair" : TupleTranslator, - "std::map" : MapTranslator + "std::set" : SetTranslator, + "std::vector" : VectorTranslator, + "pool" : PoolTranslator, + "idict" : IDictTranslator, + "dict" : DictTranslator, + "std::pair" : TupleTranslator, + "std::map" : MapTranslator, + "RTLIL::ObjRange" : ObjRangeTranslator } class Attribute: diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc index 4b712aec9..c2cd8b9e9 100644 --- a/passes/pmgen/Makefile.inc +++ b/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 $<,$^) diff --git a/passes/pmgen/peepopt.cc b/passes/pmgen/peepopt.cc index bfaf4961e..e7a729ecb 100644 --- a/passes/pmgen/peepopt.cc +++ b/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 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,12 +102,16 @@ struct PeepoptPass : public Pass { pm.setup(module->selected_cells()); - pm.run_shiftadd(); - pm.run_shiftmul_right(); - pm.run_shiftmul_left(); - pm.run_muldiv(); - pm.run_muldiv_c(); - pm.run_muxadd(); + if (formalclk) { + pm.run_formal_clockgateff(); + } else { + pm.run_shiftadd(); + pm.run_shiftmul_right(); + pm.run_shiftmul_left(); + pm.run_muldiv(); + pm.run_muldiv_c(); + pm.run_muxadd(); + } } } } diff --git a/passes/pmgen/peepopt_formal_clockgateff.pmg b/passes/pmgen/peepopt_formal_clockgateff.pmg new file mode 100644 index 000000000..835f68bd8 --- /dev/null +++ b/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 clk en latched_en gated_clk +state 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 clk_port {\A, \B} + define latch_port {clk_port == \A ? \B : \A} + index port(and_gate, clk_port) === clk + index 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 diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index bcefa7d8f..348bab727 100644 --- a/passes/sat/clk2fflogic.cc +++ b/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 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()) diff --git a/tests/various/peepopt_formal.ys b/tests/various/peepopt_formal.ys new file mode 100644 index 000000000..52bf3c67f --- /dev/null +++ b/tests/various/peepopt_formal.ys @@ -0,0 +1,45 @@ +read_verilog -sv <