From f6f85f475ba2abd186ddda10d0099750e28231ca Mon Sep 17 00:00:00 2001 From: George Rennie Date: Sun, 24 Sep 2023 12:40:41 +0100 Subject: [PATCH 1/8] smt2: Check for constant bool after fully resolving signal * This fixes #3769 --- backends/smt2/smt2.cc | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 5e63e6237..703628b73 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)); From 2cb3b6e9b8f59936524729af591d1cfbcec0e461 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Tue, 6 Aug 2024 16:32:26 +0100 Subject: [PATCH 2/8] peepopt: add formal only peepopt to rewrite latches to ffs in clock gates * this is gated behind the -formalclk flag, which also disables the other synthesis focused optimizations --- passes/pmgen/Makefile.inc | 1 + passes/pmgen/peepopt.cc | 26 +++++++-- passes/pmgen/peepopt_formal_clockgateff.pmg | 59 +++++++++++++++++++++ 3 files changed, 81 insertions(+), 5 deletions(-) create mode 100644 passes/pmgen/peepopt_formal_clockgateff.pmg diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc index 84d9ebaf1..6fa7d1fd7 100644 --- a/passes/pmgen/Makefile.inc +++ b/passes/pmgen/Makefile.inc @@ -57,6 +57,7 @@ PEEPOPT_PATTERN = passes/pmgen/peepopt_shiftmul_right.pmg PEEPOPT_PATTERN += passes/pmgen/peepopt_shiftmul_left.pmg PEEPOPT_PATTERN += passes/pmgen/peepopt_shiftadd.pmg PEEPOPT_PATTERN += passes/pmgen/peepopt_muldiv.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 5638ec3c2..5b678ee55 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(" * muldiv - Replace (A*B)/B with A\n"); log("\n"); @@ -57,14 +57,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); @@ -86,10 +98,14 @@ struct PeepoptPass : public Pass { pm.setup(module->selected_cells()); - pm.run_shiftadd(); - pm.run_shiftmul_right(); - pm.run_shiftmul_left(); - pm.run_muldiv(); + if (formalclk) { + pm.run_formal_clockgateff(); + } else { + pm.run_shiftadd(); + pm.run_shiftmul_right(); + pm.run_shiftmul_left(); + pm.run_muldiv(); + } } } } 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 From 236c69bed440ca9456c0c9c609e5ee6839322be8 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 7 Aug 2024 09:59:44 +0100 Subject: [PATCH 3/8] clk2fflogic: run peepopt -formalclk before processing design * this attempts to rewrite clock gating patterns into a form that is less likely to introduce combinational loops with clk2fflogic * can be disabled with -nopeepopt which is useful for testing clk2fflogic --- passes/sat/clk2fflogic.cc | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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()) From b6ceff2aab27c988b7de8e072eb4bc07d1637e75 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 7 Aug 2024 09:59:18 +0100 Subject: [PATCH 4/8] peepopt clockgateff: add testcase --- tests/various/peepopt_formal.ys | 45 +++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 tests/various/peepopt_formal.ys 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 < Date: Tue, 8 Oct 2024 14:34:17 +0200 Subject: [PATCH 5/8] write_btor: don't emit undriven bits multiple times * Fixes #4640 --- backends/btor/btor.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9cfd967e5..81402fa49 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1077,6 +1077,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)); From 6ab39319647009def8926da4c82ca340790fa4b9 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 9 Oct 2024 13:48:26 +0200 Subject: [PATCH 6/8] write_btor: only initialize array with const value when it is fully def * If all addresses of an array have the same initial value, they can be initialized in one go in btor with the constraint that the initial value must be fully const and thus can't have undef bits in --- backends/btor/btor.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9cfd967e5..1c2d5132e 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)); From 84ee345071d0c46b24f14e944d8c175c8831ea48 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Mon, 4 Nov 2024 15:56:33 +0100 Subject: [PATCH 7/8] pyosys: support ObjRange * this adds support for cells(), modules() and wires() that all return ObjRanges, converting them into lists for python --- misc/py_wrap_generator.py | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/misc/py_wrap_generator.py b/misc/py_wrap_generator.py index 91a82081a..b0ac1e82e 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: From 8bc4bd8a203f7847925c01659aa1af6487616cfb Mon Sep 17 00:00:00 2001 From: Robin Ole Heinemann Date: Mon, 11 Nov 2024 18:43:46 +0100 Subject: [PATCH 8/8] cxxrtl, fmt: escape double quotes in c strings --- backends/cxxrtl/cxxrtl_backend.cc | 2 +- kernel/fmt.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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/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 {