From 3eeefd23e38a53b28923749feaa9f57670e07d5c Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 18 Mar 2024 11:08:13 +1300 Subject: [PATCH 01/44] Typo fixup(s) --- frontends/ast/genrtlil.cc | 2 +- kernel/driver.cc | 2 +- passes/pmgen/ice40_dsp.cc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index fe67f00c692..e1cf6fb573a 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -2224,7 +2224,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) else input_error("FATAL.\n"); } else { - input_error("Unknown elabortoon system task '%s'.\n", str.c_str()); + input_error("Unknown elaboration system task '%s'.\n", str.c_str()); } } break; diff --git a/kernel/driver.cc b/kernel/driver.cc index 58da1bc32e3..79dff7ddabe 100644 --- a/kernel/driver.cc +++ b/kernel/driver.cc @@ -356,7 +356,7 @@ int main(int argc, char **argv) printf(" -V\n"); printf(" print version information and exit\n"); printf("\n"); - printf("The option -S is an shortcut for calling the \"synth\" command, a default\n"); + printf("The option -S is a shortcut for calling the \"synth\" command, a default\n"); printf("script for transforming the Verilog input to a gate-level netlist. For example:\n"); printf("\n"); printf(" yosys -o output.blif -S input.v\n"); diff --git a/passes/pmgen/ice40_dsp.cc b/passes/pmgen/ice40_dsp.cc index 24134b1fb1f..5720c9b1e7a 100644 --- a/passes/pmgen/ice40_dsp.cc +++ b/passes/pmgen/ice40_dsp.cc @@ -289,7 +289,7 @@ struct Ice40DspPass : public Pass { log("\n"); log("Pack input registers (A, B, {C,D}; with optional hold), pipeline registers\n"); log("({F,J,K,G}, H), output registers (O -- full 32-bits or lower 16-bits only; with\n"); - log("optional hold), and post-adder into into the SB_MAC16 resource.\n"); + log("optional hold), and post-adder into the SB_MAC16 resource.\n"); log("\n"); log("Multiply-accumulate operations using the post-adder with feedback on the {C,D}\n"); log("input will be folded into the DSP. In this scenario only, resetting the\n"); From ff10aeebd68a1906703cc4a63b70ca0f30474c0d Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 18 Mar 2024 11:33:18 +1300 Subject: [PATCH 02/44] Fix some synth_* help messages Mostly memory_libmap arg checks; puts the checks into an else block on the `if (help_mode)` check to avoid cases like `synth_ice40` listing `-no-auto-huge [-no-auto-huge]`. Also fix `map_iopad` section being empty in `synth_fabulous`. --- techlibs/anlogic/synth_anlogic.cc | 10 ++++++---- techlibs/ecp5/synth_ecp5.cc | 10 ++++++---- techlibs/efinix/synth_efinix.cc | 10 +++++++--- techlibs/fabulous/synth_fabulous.cc | 4 ++-- techlibs/gowin/synth_gowin.cc | 10 ++++++---- techlibs/ice40/synth_ice40.cc | 10 ++++++---- techlibs/lattice/synth_lattice.cc | 10 ++++++---- techlibs/nexus/synth_nexus.cc | 10 ++++++---- 8 files changed, 45 insertions(+), 29 deletions(-) diff --git a/techlibs/anlogic/synth_anlogic.cc b/techlibs/anlogic/synth_anlogic.cc index a3c1e0434f2..c72e7f2a183 100644 --- a/techlibs/anlogic/synth_anlogic.cc +++ b/techlibs/anlogic/synth_anlogic.cc @@ -169,12 +169,14 @@ struct SynthAnlogicPass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (nobram) - args += " -no-auto-block"; - if (nolutram) - args += " -no-auto-distributed"; if (help_mode) args += " [-no-auto-block] [-no-auto-distributed]"; + else { + if (nobram) + args += " -no-auto-block"; + if (nolutram) + args += " -no-auto-distributed"; + } run("memory_libmap -lib +/anlogic/lutrams.txt -lib +/anlogic/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run("techmap -map +/anlogic/lutrams_map.v -map +/anlogic/brams_map.v"); } diff --git a/techlibs/ecp5/synth_ecp5.cc b/techlibs/ecp5/synth_ecp5.cc index f6215987f7f..6e518f5d183 100644 --- a/techlibs/ecp5/synth_ecp5.cc +++ b/techlibs/ecp5/synth_ecp5.cc @@ -308,12 +308,14 @@ struct SynthEcp5Pass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (nobram) - args += " -no-auto-block"; - if (nolutram) - args += " -no-auto-distributed"; if (help_mode) args += " [-no-auto-block] [-no-auto-distributed]"; + else { + if (nobram) + args += " -no-auto-block"; + if (nolutram) + args += " -no-auto-distributed"; + } run("memory_libmap -lib +/ecp5/lutrams.txt -lib +/ecp5/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run("techmap -map +/ecp5/lutrams_map.v -map +/ecp5/brams_map.v"); } diff --git a/techlibs/efinix/synth_efinix.cc b/techlibs/efinix/synth_efinix.cc index bbc38944488..419bc2f884c 100644 --- a/techlibs/efinix/synth_efinix.cc +++ b/techlibs/efinix/synth_efinix.cc @@ -161,9 +161,13 @@ struct SynthEfinixPass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (nobram) - args += " -no-auto-block"; - run("memory_libmap -lib +/efinix/brams.txt" + args); + if (help_mode) + args += " [-no-auto-block]"; + else { + if (nobram) + args += " -no-auto-block"; + } + run("memory_libmap -lib +/efinix/brams.txt" + args, "(-no-auto-block if -nobram)"); run("techmap -map +/efinix/brams_map.v"); } diff --git a/techlibs/fabulous/synth_fabulous.cc b/techlibs/fabulous/synth_fabulous.cc index b4a7ab2dc6f..8d2fb1471a9 100644 --- a/techlibs/fabulous/synth_fabulous.cc +++ b/techlibs/fabulous/synth_fabulous.cc @@ -320,7 +320,7 @@ struct SynthPass : public ScriptPass run("opt_clean"); } - if (check_label("map_ram")) { + if (check_label("map_ram", "(unless -noregfile)")) { // RegFile extraction if (!noregfile) { run("memory_libmap -lib +/fabulous/ram_regfile.txt"); @@ -342,7 +342,7 @@ struct SynthPass : public ScriptPass } if (check_label("map_iopad", "(if -iopad)")) { - if (iopad) { + if (iopad || help_mode) { run("opt -full"); run("iopadmap -bits -outpad $__FABULOUS_OBUF I:PAD -inpad $__FABULOUS_IBUF O:PAD " "-toutpad IO_1_bidirectional_frame_config_pass ~T:I:PAD " diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index 85022c1cfa2..48b7563b1ec 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -230,12 +230,14 @@ struct SynthGowinPass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (nobram) - args += " -no-auto-block"; - if (nolutram) - args += " -no-auto-distributed"; if (help_mode) args += " [-no-auto-block] [-no-auto-distributed]"; + else { + if (nobram) + args += " -no-auto-block"; + if (nolutram) + args += " -no-auto-distributed"; + } run("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run("techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map.v"); } diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index 4c691c7a5aa..81832389269 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -353,12 +353,14 @@ struct SynthIce40Pass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (!spram) - args += " -no-auto-huge"; - if (nobram) - args += " -no-auto-block"; if (help_mode) args += " [-no-auto-huge] [-no-auto-block]"; + else { + if (!spram) + args += " -no-auto-huge"; + if (nobram) + args += " -no-auto-block"; + } run("memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt" + args, "(-no-auto-huge unless -spram, -no-auto-block if -nobram)"); run("techmap -map +/ice40/brams_map.v -map +/ice40/spram_map.v"); run("ice40_braminit"); diff --git a/techlibs/lattice/synth_lattice.cc b/techlibs/lattice/synth_lattice.cc index cc5821ad832..16a068b0741 100644 --- a/techlibs/lattice/synth_lattice.cc +++ b/techlibs/lattice/synth_lattice.cc @@ -373,12 +373,14 @@ struct SynthLatticePass : public ScriptPass if (check_label("map_ram")) { std::string args = ""; - if (nobram) - args += " -no-auto-block"; - if (nolutram) - args += " -no-auto-distributed"; if (help_mode) args += " [-no-auto-block] [-no-auto-distributed]"; + else { + if (nobram) + args += " -no-auto-block"; + if (nolutram) + args += " -no-auto-distributed"; + } run("memory_libmap -lib +/lattice/lutrams.txt -lib +/lattice/brams" + brams_map + ".txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run("techmap -map +/lattice/lutrams_map.v -map +/lattice/brams_map" + brams_map + ".v"); } diff --git a/techlibs/nexus/synth_nexus.cc b/techlibs/nexus/synth_nexus.cc index 6fd15ba5577..2935fbd3bca 100644 --- a/techlibs/nexus/synth_nexus.cc +++ b/techlibs/nexus/synth_nexus.cc @@ -300,12 +300,14 @@ struct SynthNexusPass : public ScriptPass { std::string args = ""; args += " -no-auto-huge"; - if (nobram) - args += " -no-auto-block"; - if (nolutram) - args += " -no-auto-distributed"; if (help_mode) args += " [-no-auto-block] [-no-auto-distributed]"; + else { + if (nobram) + args += " -no-auto-block"; + if (nolutram) + args += " -no-auto-distributed"; + } run("memory_libmap -lib +/nexus/lutrams.txt -lib +/nexus/brams.txt -lib +/nexus/lrams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run("techmap -map +/nexus/lutrams_map.v -map +/nexus/brams_map.v -map +/nexus/lrams_map.v"); } From b87327d1b9a0ec0c8b62694cb3697dcda1665ee2 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Fri, 12 Apr 2024 13:38:33 +0200 Subject: [PATCH 03/44] fix hierarchy -generate mode handling of cells --- passes/hierarchy/hierarchy.cc | 2 +- tests/various/hierarchy_generate.ys | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 tests/various/hierarchy_generate.ys diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index 6fcda5d7644..3ef04616fcb 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -47,7 +47,7 @@ void generate(RTLIL::Design *design, const std::vector &celltypes, { if (design->module(cell->type) != nullptr) continue; - if (cell->type.begins_with("$__")) + if (cell->type.begins_with("$") && !cell->type.begins_with("$__")) continue; for (auto &pattern : celltypes) if (patmatch(pattern.c_str(), RTLIL::unescape_id(cell->type).c_str())) diff --git a/tests/various/hierarchy_generate.ys b/tests/various/hierarchy_generate.ys new file mode 100644 index 00000000000..a4dc87a865f --- /dev/null +++ b/tests/various/hierarchy_generate.ys @@ -0,0 +1,19 @@ +read_verilog -icells < Date: Fri, 12 Apr 2024 13:51:06 +0200 Subject: [PATCH 04/44] add command that should not have any effect to hierarchy -generate test (this documents the current behavior, not sure if it is desired functionality) --- tests/various/hierarchy_generate.ys | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/various/hierarchy_generate.ys b/tests/various/hierarchy_generate.ys index a4dc87a865f..9c01afb6499 100644 --- a/tests/various/hierarchy_generate.ys +++ b/tests/various/hierarchy_generate.ys @@ -15,5 +15,6 @@ endmodule EOF hierarchy -generate unknown_sub i:a i:b o:y hierarchy -generate $__dunder_sub i:a i:b o:y +hierarchy -generate $xor i:A i:B o:Y # this one is ignored hierarchy -top top -check check -assert From 0d30a4d479b4c5ac931610d019b053815e943cca Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 22 Apr 2024 13:26:17 +0200 Subject: [PATCH 05/44] rtlil: Add packed `extract` implementation for `SigSpec` Previously `extract` on a `SigSpec` would always unpack it. Since a significant amount of `SigSpec`s have one or few chunks, it's worth having a dedicated implementation. This is especially true, since the RTLIL frontend calls into this for every `wire [lhs:rhs]` slice, making this `extract` take up 40% when profiling `read_rtlil` with one of the largest coarse grained RTLIL designs I had on hand. With this change the `read_rtlil` profile looks like I would expect it to look like, but I noticed that a lot of the other core RTLIL methods also are a bit too eager with unpacking or implementing `SigChunk`/`Const` overloads that just convert to a single chunk `SigSpec` and forward to the implementation for that, when a direct implementation would avoid temporary std::vector allocations. While not relevant for `read_rtlil`, to me it looks like there might be a few easy overall performance gains to be had by addressing this more generally. --- kernel/rtlil.cc | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 8781b6a8946..bafafb57b9b 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -4435,8 +4435,39 @@ RTLIL::SigSpec RTLIL::SigSpec::extract(int offset, int length) const log_assert(offset >= 0); log_assert(length >= 0); log_assert(offset + length <= width_); - unpack(); + cover("kernel.rtlil.sigspec.extract_pos"); + + if (packed()) + { + if (chunks_.size() == 1) + return chunks_[0].extract(offset, length); + + SigSpec extracted; + int end = offset + length; + int chunk_end = 0; + + for (auto const &chunk : chunks_) + { + int chunk_begin = chunk_end; + chunk_end += chunk.width; + int extract_begin = std::max(chunk_begin, offset); + int extract_end = std::min(chunk_end, end); + if (extract_begin >= extract_end) + continue; + int extract_offset = extract_begin - chunk_begin; + int extract_len = extract_end - extract_begin; + if (extract_offset == 0 && extract_len == chunk.width) + extracted.chunks_.emplace_back(chunk); + else + extracted.chunks_.emplace_back( + chunk.extract(extract_offset, extract_len)); + } + + extracted.width_ = length; + return extracted; + } + return std::vector(bits_.begin() + offset, bits_.begin() + offset + length); } From 178eceb32d9e6d5e36077347ac452f6e10ae7aab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 22 Apr 2024 16:23:51 +0200 Subject: [PATCH 06/44] rtlil: Replace the packed `SigSpec::extract` impl --- kernel/rtlil.cc | 46 +++++++++++++++++++++------------------------- 1 file changed, 21 insertions(+), 25 deletions(-) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index bafafb57b9b..a6aebaa4258 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -4438,37 +4438,33 @@ RTLIL::SigSpec RTLIL::SigSpec::extract(int offset, int length) const cover("kernel.rtlil.sigspec.extract_pos"); - if (packed()) - { - if (chunks_.size() == 1) - return chunks_[0].extract(offset, length); - + if (packed()) { SigSpec extracted; - int end = offset + length; - int chunk_end = 0; + extracted.width_ = length; - for (auto const &chunk : chunks_) - { - int chunk_begin = chunk_end; - chunk_end += chunk.width; - int extract_begin = std::max(chunk_begin, offset); - int extract_end = std::min(chunk_end, end); - if (extract_begin >= extract_end) - continue; - int extract_offset = extract_begin - chunk_begin; - int extract_len = extract_end - extract_begin; - if (extract_offset == 0 && extract_len == chunk.width) - extracted.chunks_.emplace_back(chunk); - else - extracted.chunks_.emplace_back( - chunk.extract(extract_offset, extract_len)); + auto it = chunks_.begin(); + for (; offset; offset -= it->width, it++) { + if (offset < it->width) { + int chunk_length = min(it->width - offset, length); + extracted.chunks_.emplace_back(it->extract(offset, chunk_length)); + length -= chunk_length; + it++; + break; + } + } + for (; length; length -= it->width, it++) { + if (length >= it->width) { + extracted.chunks_.emplace_back(*it); + } else { + extracted.chunks_.emplace_back(it->extract(0, length)); + break; + } } - extracted.width_ = length; return extracted; + } else { + return std::vector(bits_.begin() + offset, bits_.begin() + offset + length); } - - return std::vector(bits_.begin() + offset, bits_.begin() + offset + length); } void RTLIL::SigSpec::append(const RTLIL::SigSpec &signal) From 4a666d3ba860f5d43f118c058b79a4ed6fce5b1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 22 Apr 2024 16:36:47 +0200 Subject: [PATCH 07/44] Bump abc --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 95a982874d4..72adfe97240 100644 --- a/Makefile +++ b/Makefile @@ -166,7 +166,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 0cd90d0 +ABCREV = 208b486 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From 6d6aa4d35e43ac58cedef07326e45eb63890bf2e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 22 Apr 2024 17:43:41 +0200 Subject: [PATCH 08/44] Bump abc to cherry-pick a WASM build fix --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 72adfe97240..b426522b8aa 100644 --- a/Makefile +++ b/Makefile @@ -166,7 +166,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = 208b486 +ABCREV = b502f00 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From c167d9b76ec1f5cdacad0675185dad8d05a98fcc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Tue, 23 Apr 2024 11:41:20 +0200 Subject: [PATCH 09/44] Bump abc for one more fix --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b426522b8aa..afa76b6c945 100644 --- a/Makefile +++ b/Makefile @@ -166,7 +166,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = b502f00 +ABCREV = bc45604 ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From 67c7062fb8d6e90e38954324c616d17d3b1d638f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Tue, 23 Apr 2024 13:50:45 +0200 Subject: [PATCH 10/44] Bump abc for a fix once more --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index afa76b6c945..f19ac04b5b3 100644 --- a/Makefile +++ b/Makefile @@ -166,7 +166,7 @@ bumpversion: # is just a symlink to your actual ABC working directory, as 'make mrproper' # will remove the 'abc' directory and you do not want to accidentally # delete your work on ABC.. -ABCREV = bc45604 +ABCREV = 03da96f ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) From cf02f86c28ceb7f9bba041493663da3198c0fabc Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Wed, 24 Apr 2024 00:16:06 +0000 Subject: [PATCH 11/44] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index f19ac04b5b3..22fe373a68a 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+25 +YOSYS_VER := 0.40+33 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 4e6deb53b64d4acd2046d2826ede02c5cd35d22f Mon Sep 17 00:00:00 2001 From: George Rennie Date: Fri, 26 Apr 2024 19:16:01 +0100 Subject: [PATCH 12/44] read_aiger: Fix incorrect read of binary Aiger without outputs * Also makes all ascii parsing finish reading lines and adds a small test --- frontends/aiger/aigerparse.cc | 12 +++++------- tests/aiger/and_to_bad_out.aag | 8 ++++++++ tests/aiger/and_to_bad_out.aig | 5 +++++ 3 files changed, 18 insertions(+), 7 deletions(-) create mode 100644 tests/aiger/and_to_bad_out.aag create mode 100644 tests/aiger/and_to_bad_out.aig diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index cb19b8413a5..0178514e1cd 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -590,6 +590,7 @@ void AigerReader::parse_aiger_ascii() for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is an output\n", l1); RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); @@ -597,20 +598,18 @@ void AigerReader::parse_aiger_ascii() module->connect(wire, createWireIfNotExists(module, l1)); outputs.push_back(wire); } - //std::getline(f, line); // Ignore up to start of next line // Parse bad properties for (unsigned i = 0; i < B; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is a bad state property\n", l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_output = true; bad_properties.push_back(wire); } - //if (B > 0) - // std::getline(f, line); // Ignore up to start of next line // TODO: Parse invariant constraints for (unsigned i = 0; i < C; ++i, ++line_count) @@ -628,6 +627,7 @@ void AigerReader::parse_aiger_ascii() for (unsigned i = 0; i < A; ++i) { if (!(f >> l1 >> l2 >> l3)) log_error("Line %u cannot be interpreted as an AND!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d %d %d is an AND\n", l1, l2, l3); log_assert(!(l1 & 1)); @@ -636,7 +636,6 @@ void AigerReader::parse_aiger_ascii() RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3); module->addAndGate("$and" + o_wire->name.str(), i1_wire, i2_wire, o_wire); } - std::getline(f, line); // Ignore up to start of next line } static unsigned parse_next_delta_literal(std::istream &f, unsigned ref) @@ -715,6 +714,7 @@ void AigerReader::parse_aiger_binary() for (unsigned i = 0; i < O; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as an output!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is an output\n", l1); RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i)); @@ -722,20 +722,18 @@ void AigerReader::parse_aiger_binary() module->connect(wire, createWireIfNotExists(module, l1)); outputs.push_back(wire); } - std::getline(f, line); // Ignore up to start of next line // Parse bad properties for (unsigned i = 0; i < B; ++i, ++line_count) { if (!(f >> l1)) log_error("Line %u cannot be interpreted as a bad state property!\n", line_count); + std::getline(f, line); // Ignore up to start of next line log_debug2("%d is a bad state property\n", l1); RTLIL::Wire *wire = createWireIfNotExists(module, l1); wire->port_output = true; bad_properties.push_back(wire); } - if (B > 0) - std::getline(f, line); // Ignore up to start of next line // TODO: Parse invariant constraints for (unsigned i = 0; i < C; ++i, ++line_count) diff --git a/tests/aiger/and_to_bad_out.aag b/tests/aiger/and_to_bad_out.aag new file mode 100644 index 00000000000..96f1e7cad12 --- /dev/null +++ b/tests/aiger/and_to_bad_out.aag @@ -0,0 +1,8 @@ +aag 3 2 0 0 1 1 0 0 0 +2 +4 +6 +6 2 4 +i0 pi0 +i1 pi1 +b0 b0 diff --git a/tests/aiger/and_to_bad_out.aig b/tests/aiger/and_to_bad_out.aig new file mode 100644 index 00000000000..3be65ae895b --- /dev/null +++ b/tests/aiger/and_to_bad_out.aig @@ -0,0 +1,5 @@ +aig 3 2 0 0 1 1 +6 +i0 pi0 +i1 pi1 +b0 b0 From dd2195543b095cce108dcd9b94fe2f0a80660491 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Apr 2024 00:17:14 +0000 Subject: [PATCH 13/44] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 22fe373a68a..2dbce272dc6 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+33 +YOSYS_VER := 0.40+45 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From fc82251105324ea14e10b6738cbaffe5e68c3588 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 10 Apr 2024 14:17:57 +0200 Subject: [PATCH 14/44] techmap: Support dynamic cell types --- kernel/constids.inc | 2 ++ passes/techmap/techmap.cc | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/kernel/constids.inc b/kernel/constids.inc index 7db21debb0e..00db94af441 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -222,6 +222,8 @@ X(_TECHMAP_REPLACE_) X(techmap_simplemap) X(_techmap_special_) X(techmap_wrap) +X(_TECHMAP_PLACEHOLDER_) +X(techmap_chtype) X(T_FALL_MAX) X(T_FALL_MIN) X(T_FALL_TYP) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index db395315ce6..eda7c2f6c3b 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -336,6 +336,9 @@ struct TechmapWorker if (c->type.begins_with("\\$")) c->type = c->type.substr(1); + + if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) + c->type = RTLIL::escape_id(tpl_cell->get_string_attribute(ID::techmap_chtype)); vector autopurge_ports; @@ -1135,6 +1138,10 @@ struct TechmapPass : public Pass { log("new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'\n"); log("prefix also substituted.\n"); log("\n"); + log("A cell with the type _TECHMAP_PLACEHOLDER_ in the map file will have its type\n"); + log("changed to the content of the techmap_chtype attribute. This allows for choosing\n"); + log("the cell type dynamically.\n"); + log("\n"); log("See 'help extract' for a pass that does the opposite thing.\n"); log("\n"); log("See 'help flatten' for a pass that does flatten the design (which is\n"); From 6ff4ecb2b42b8df40c2c44051159d53bf9eea65b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 10 Apr 2024 18:32:27 +0200 Subject: [PATCH 15/44] techmap: Remove `techmap_chtype` from the result --- passes/techmap/techmap.cc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index eda7c2f6c3b..64de3a1cac0 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -337,8 +337,10 @@ struct TechmapWorker if (c->type.begins_with("\\$")) c->type = c->type.substr(1); - if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) + if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) { c->type = RTLIL::escape_id(tpl_cell->get_string_attribute(ID::techmap_chtype)); + c->attributes.erase(ID::techmap_chtype); + } vector autopurge_ports; From a833f050364c959c2eebc039c019a3df8d420825 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 2 May 2024 23:49:50 +0200 Subject: [PATCH 16/44] techmap: add dynamic cell type test --- tests/techmap/techmap_chtype.ys | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/techmap/techmap_chtype.ys diff --git a/tests/techmap/techmap_chtype.ys b/tests/techmap/techmap_chtype.ys new file mode 100644 index 00000000000..7c339842013 --- /dev/null +++ b/tests/techmap/techmap_chtype.ys @@ -0,0 +1,33 @@ +read_verilog < Date: Wed, 27 Mar 2024 23:54:51 +0100 Subject: [PATCH 17/44] cellmatch: New pass --- passes/techmap/Makefile.inc | 1 + passes/techmap/cellmatch.cc | 340 ++++++++++++++++++++++++++++++++++++ 2 files changed, 341 insertions(+) create mode 100644 passes/techmap/cellmatch.cc diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 9d57e3d71af..74813bca93f 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -48,6 +48,7 @@ OBJS += passes/techmap/dfflegalize.o OBJS += passes/techmap/dffunmap.o OBJS += passes/techmap/flowmap.o OBJS += passes/techmap/extractinv.o +OBJS += passes/techmap/cellmatch.o endif ifeq ($(DISABLE_SPAWN),0) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc new file mode 100644 index 00000000000..7c75418e3bc --- /dev/null +++ b/passes/techmap/cellmatch.cc @@ -0,0 +1,340 @@ +#include "kernel/celltypes.h" +#include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/sigtools.h" +#include "kernel/utils.h" + +#include + +USING_YOSYS_NAMESPACE +YOSYS_NAMESPACE_BEGIN + +// return module's inputs in canonical order +SigSpec module_inputs(Module *m) +{ + SigSpec ret; + for (auto port : m->ports) { + Wire *w = m->wire(port); + if (!w->port_input) + continue; + if (w->width != 1) + log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n", + log_id(w), log_id(m)); + ret.append(w); + } + return ret; +} + +// return module's outputs in canonical order +SigSpec module_outputs(Module *m) +{ + SigSpec ret; + for (auto port : m->ports) { + Wire *w = m->wire(port); + if (!w->port_output) + continue; + if (w->width != 1) + log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n", + log_id(w), log_id(m)); + ret.append(w); + } + return ret; +} + +uint64_t permute_lut(uint64_t lut, const std::vector &varmap) +{ + int k = varmap.size(); + uint64_t ret = 0; + for (int j = 0; j < 1 << k; j++) { + int m = 0; + for (int l = 0; l < k; l++) + if (j & 1 << l) + m |= 1 << varmap[l]; + if (lut & 1 << m) + ret |= 1 << j; + } + return ret; +} + +uint64_t p_class(int k, uint64_t lut) +{ + std::vector map; + for (int j = 0; j < k; j++) + map.push_back(j); + + uint64_t repr = ~(uint64_t) 0; + std::vector repr_vars; + while (true) { + uint64_t perm = permute_lut(lut, map); + if (perm <= repr) { + repr = perm; + repr_vars = map; + } + if (!std::next_permutation(map.begin(), map.end())) + break; + } + return repr; +} + +bool derive_module_luts(Module *m, std::vector &luts) +{ + SigMap sigmap(m); + CellTypes ff_types; + ff_types.setup_stdcells_mem(); + + dict driver; + for (auto cell : m->selected_cells()) { + if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) + continue; + + if (ff_types.cell_known(cell->type)) { + log("Ignoring module '%s' which isn't purely combinational.\n", log_id(m)); + return false; + } + + if (!cell->type.in(ID($_NOT_), ID($_AND_))) + log_error("Unsupported cell in module '%s': %s of type %s\n", + log_id(m), log_id(cell), log_id(cell->type)); + + driver[sigmap(cell->getPort(ID::Y))] = cell; + } + + TopoSort sort; + for (auto cell : m->cells()) + if (cell->type.in(ID($_NOT_), ID($_AND_))) { + sort.node(cell); + SigSpec inputs = cell->type == ID($_AND_) + ? SigSpec({cell->getPort(ID::B), cell->getPort(ID::A)}) + : cell->getPort(ID::A); + for (auto bit : sigmap(inputs)) + if (driver.count(bit)) + sort.edge(driver.at(bit), cell); + } + + if (!sort.sort()) + log_error("Module %s contains combinational loops.\n", log_id(m)); + + dict states; + states[State::S0] = 0; + states[State::S1] = ~(uint64_t) 1; + + { + uint64_t sieves[6] = { + 0xaaaaaaaaaaaaaaaa, + 0xcccccccccccccccc, + 0xf0f0f0f0f0f0f0f0, + 0xff00ff00ff00ff00, + 0xffff0000ffff0000, + 0xffffffff00000000, + }; + + SigSpec inputs = sigmap(module_inputs(m)); + if (inputs.size() > 6) { + log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); + return false; + } + + for (int i = 0; i < inputs.size(); i++) + states[inputs[i]] = sieves[i] & ((((uint64_t) 1) << (1 << inputs.size())) - 1); + } + + for (auto cell : sort.sorted) { + if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) + continue; + + if (cell->type == ID($_AND_)) { + SigSpec a = sigmap(cell->getPort(ID::A)); + SigSpec b = sigmap(cell->getPort(ID::B)); + if (!states.count(a) || !states.count(b)) + log_error("Cell %s in module %s sources an undriven wire!", + log_id(cell), log_id(m)); + states[sigmap(cell->getPort(ID::Y))] = \ + states.at(a) & states.at(b); + } else if (cell->type == ID($_NOT_)) { + SigSpec a = sigmap(cell->getPort(ID::A)); + if (!states.count(a)) + log_error("Cell %s in module %s sources an undriven wire!", + log_id(cell), log_id(m)); + states[sigmap(cell->getPort(ID::Y))] = ~states.at(a); + } else { + log_abort(); + } + } + + for (auto bit : module_outputs(m)) { + if (!states.count(sigmap(bit))) + log_error("Output port %s in module %s is undriven!", + log_signal(bit), log_id(m)); + luts.push_back(states.at(sigmap(bit))); + } + return true; +} + +struct CellmatchPass : Pass { + CellmatchPass() : Pass("cellmatch", "match cells to their targets in cell library") {} + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" cellmatch -lib [module selection]\n"); + log("\n"); + log("This pass identifies functionally equivalent counterparts between each of the\n"); + log("selected modules and a module from the secondary design . For every such\n"); + log("correspondence found, a techmap rule is generated for mapping instances of the\n"); + log("former to instances of the latter. This techmap rule is saved in yet another\n"); + log("design called '$cellmatch_map', which is created if non-existent.\n"); + log("\n"); + log("This pass restricts itself to combinational modules which must be modeled with an\n"); + log("and-inverter graph. Run 'aigmap' first if necessary. Modules are functionally\n"); + log("equivalent as long as their truth tables are identical upto a permutation of\n"); + log("inputs and outputs. The number of inputs is limited to 6.\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *d) override + { + log_header(d, "Executing CELLMATCH pass. (match cells)\n"); + + size_t argidx; + bool lut_attrs = false; + Design *lib = NULL; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-lut_attrs") { + // an undocumented debugging option + lut_attrs = true; + } else if (args[argidx] == "-lib" && argidx + 1 < args.size()) { + if (!saved_designs.count(args[++argidx])) + log_cmd_error("No design '%s' found!\n", args[argidx].c_str()); + lib = saved_designs.at(args[argidx]); + } else { + break; + } + } + extra_args(args, argidx, d); + + if (!lib && !lut_attrs) + log_cmd_error("Missing required -lib option.\n"); + + struct Target { + Module *module; + std::vector luts; + }; + + dict, std::vector> targets; + + if (lib) + for (auto m : lib->modules()) { + pool p_classes; + + // produce a fingerprint in p_classes + int ninputs = module_inputs(m).size(); + std::vector luts; + if (!derive_module_luts(m, luts)) + continue; + for (auto lut : luts) + p_classes.insert(p_class(ninputs, lut)); + + // save as a viable target + targets[p_classes].push_back(Target{m, luts}); + } + + auto r = saved_designs.emplace("$cellmatch_map", nullptr); + if (r.second) + r.first->second = new Design; + Design *map_design = r.first->second; + + for (auto m : d->selected_whole_modules_warn()) { + std::vector luts; + if (!derive_module_luts(m, luts)) + continue; + + SigSpec inputs = module_inputs(m); + SigSpec outputs = module_outputs(m); + + if (lut_attrs) { + int no = 0; + for (auto bit : outputs) { + log_assert(bit.is_wire()); + bit.wire->attributes[ID(p_class)] = p_class(inputs.size(), luts[no]); + bit.wire->attributes[ID(lut)] = luts[no++]; + } + } + + // fingerprint + pool p_classes; + for (auto lut : luts) + p_classes.insert(p_class(inputs.size(), lut)); + + for (auto target : targets[p_classes]) { + log_debug("Candidate %s for matching to %s\n", log_id(target.module), log_id(m)); + + SigSpec target_inputs = module_inputs(target.module); + SigSpec target_outputs = module_outputs(target.module); + + if (target_inputs.size() != inputs.size()) + continue; + + if (target_outputs.size() != outputs.size()) + continue; + + std::vector input_map; + for (int i = 0; i < inputs.size(); i++) + input_map.push_back(i); + + bool found_match = false; + while (!found_match) { + std::vector output_map; + for (int i = 0; i < outputs.size(); i++) + output_map.push_back(i); + + while (!found_match) { + int out_no = 0; + bool match = true; + for (auto lut : luts) { + if (permute_lut(target.luts[output_map[out_no++]], input_map) != lut) { + match = false; + break; + } + } + + if (match) { + log("Module %s matches %s\n", log_id(m), log_id(target.module)); + Module *map = map_design->addModule(stringf("\\_60_%s_%s", log_id(m), log_id(target.module))); + Cell *cell = map->addCell(ID::_TECHMAP_REPLACE_, target.module->name); + + map->attributes[ID(techmap_celltype)] = m->name.str(); + + for (int i = 0; i < outputs.size(); i++) { + log_assert(outputs[i].is_wire()); + Wire *w = map->addWire(outputs[i].wire->name, 1); + w->port_id = outputs[i].wire->port_id; + w->port_output = true; + log_assert(target_outputs[output_map[i]].is_wire()); + cell->setPort(target_outputs[output_map[i]].wire->name, w); + } + + for (int i = 0; i < inputs.size(); i++) { + log_assert(inputs[i].is_wire()); + Wire *w = map->addWire(inputs[i].wire->name, 1); + w->port_id = inputs[i].wire->port_id; + w->port_input = true; + log_assert(target_inputs[input_map[i]].is_wire()); + cell->setPort(target_inputs[input_map[i]].wire->name, w); + } + + map->fixup_ports(); + found_match = true; + } + + if (!std::next_permutation(output_map.begin(), output_map.end())) + break; + } + + if (!std::next_permutation(input_map.begin(), input_map.end())) + break; + } + } + } + } +} CellmatchPass; + +YOSYS_NAMESPACE_END From 6a9858cdad96322ddca73d50602ce643c82edc04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 16:56:36 +0200 Subject: [PATCH 18/44] cellmatch: Delegate evaluation to `ConstEval` --- passes/techmap/cellmatch.cc | 107 ++++++++++-------------------------- 1 file changed, 30 insertions(+), 77 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 7c75418e3bc..9459c112fe7 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -2,6 +2,7 @@ #include "kernel/register.h" #include "kernel/rtlil.h" #include "kernel/sigtools.h" +#include "kernel/consteval.h" #include "kernel/utils.h" #include @@ -78,95 +79,48 @@ uint64_t p_class(int k, uint64_t lut) bool derive_module_luts(Module *m, std::vector &luts) { - SigMap sigmap(m); CellTypes ff_types; ff_types.setup_stdcells_mem(); - - dict driver; - for (auto cell : m->selected_cells()) { - if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) - continue; - + for (auto cell : m->cells()) { if (ff_types.cell_known(cell->type)) { log("Ignoring module '%s' which isn't purely combinational.\n", log_id(m)); return false; } - - if (!cell->type.in(ID($_NOT_), ID($_AND_))) - log_error("Unsupported cell in module '%s': %s of type %s\n", - log_id(m), log_id(cell), log_id(cell->type)); - - driver[sigmap(cell->getPort(ID::Y))] = cell; } - TopoSort sort; - for (auto cell : m->cells()) - if (cell->type.in(ID($_NOT_), ID($_AND_))) { - sort.node(cell); - SigSpec inputs = cell->type == ID($_AND_) - ? SigSpec({cell->getPort(ID::B), cell->getPort(ID::A)}) - : cell->getPort(ID::A); - for (auto bit : sigmap(inputs)) - if (driver.count(bit)) - sort.edge(driver.at(bit), cell); - } - - if (!sort.sort()) - log_error("Module %s contains combinational loops.\n", log_id(m)); - - dict states; - states[State::S0] = 0; - states[State::S1] = ~(uint64_t) 1; - - { - uint64_t sieves[6] = { - 0xaaaaaaaaaaaaaaaa, - 0xcccccccccccccccc, - 0xf0f0f0f0f0f0f0f0, - 0xff00ff00ff00ff00, - 0xffff0000ffff0000, - 0xffffffff00000000, - }; - - SigSpec inputs = sigmap(module_inputs(m)); - if (inputs.size() > 6) { - log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); - return false; - } + SigSpec inputs = module_inputs(m); + SigSpec outputs = module_outputs(m); + int ninputs = inputs.size(), noutputs = outputs.size(); - for (int i = 0; i < inputs.size(); i++) - states[inputs[i]] = sieves[i] & ((((uint64_t) 1) << (1 << inputs.size())) - 1); + if (ninputs > 6) { + log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); + return false; } - for (auto cell : sort.sorted) { - if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) - continue; + luts.clear(); + luts.resize(noutputs); + + ConstEval ceval(m); + for (int i = 0; i < 1 << ninputs; i++) { + ceval.clear(); + for (int j = 0; j < ninputs; j++) + ceval.set(inputs[j], (i & (1 << j)) ? State::S1 : State::S0); + for (int j = 0; j < noutputs; j++) { + SigSpec bit = outputs[j]; + + if (!ceval.eval(bit)) { + log("Failed to evaluate output '%s' in module '%s'.\n", + log_signal(outputs[j]), log_id(m)); + return false; + } - if (cell->type == ID($_AND_)) { - SigSpec a = sigmap(cell->getPort(ID::A)); - SigSpec b = sigmap(cell->getPort(ID::B)); - if (!states.count(a) || !states.count(b)) - log_error("Cell %s in module %s sources an undriven wire!", - log_id(cell), log_id(m)); - states[sigmap(cell->getPort(ID::Y))] = \ - states.at(a) & states.at(b); - } else if (cell->type == ID($_NOT_)) { - SigSpec a = sigmap(cell->getPort(ID::A)); - if (!states.count(a)) - log_error("Cell %s in module %s sources an undriven wire!", - log_id(cell), log_id(m)); - states[sigmap(cell->getPort(ID::Y))] = ~states.at(a); - } else { - log_abort(); + log_assert(ceval.eval(bit)); + + if (bit[0] == State::S1) + luts[j] |= 1 << i; } } - for (auto bit : module_outputs(m)) { - if (!states.count(sigmap(bit))) - log_error("Output port %s in module %s is undriven!", - log_signal(bit), log_id(m)); - luts.push_back(states.at(sigmap(bit))); - } return true; } @@ -184,10 +138,9 @@ struct CellmatchPass : Pass { log("former to instances of the latter. This techmap rule is saved in yet another\n"); log("design called '$cellmatch_map', which is created if non-existent.\n"); log("\n"); - log("This pass restricts itself to combinational modules which must be modeled with an\n"); - log("and-inverter graph. Run 'aigmap' first if necessary. Modules are functionally\n"); + log("This pass restricts itself to combinational modules. Modules are functionally\n"); log("equivalent as long as their truth tables are identical upto a permutation of\n"); - log("inputs and outputs. The number of inputs is limited to 6.\n"); + log("inputs and outputs. The supported number of inputs is limited to 6.\n"); log("\n"); } void execute(std::vector args, RTLIL::Design *d) override From c0e68dcc4d232542272d1ad436767175a6f04481 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 16:56:44 +0200 Subject: [PATCH 19/44] cellmatch: Add debug print --- passes/techmap/cellmatch.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 9459c112fe7..5301cc99bfd 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -185,6 +185,8 @@ struct CellmatchPass : Pass { continue; for (auto lut : luts) p_classes.insert(p_class(ninputs, lut)); + + log_debug("Registered %s\n", log_id(m)); // save as a viable target targets[p_classes].push_back(Target{m, luts}); From 913bc87c4419303e32f4ca86ed437fe1e8ee015e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 17:12:53 +0200 Subject: [PATCH 20/44] cellmatch: Add test --- tests/techmap/cellmatch.ys | 79 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 tests/techmap/cellmatch.ys diff --git a/tests/techmap/cellmatch.ys b/tests/techmap/cellmatch.ys new file mode 100644 index 00000000000..46960fc1430 --- /dev/null +++ b/tests/techmap/cellmatch.ys @@ -0,0 +1,79 @@ +read_verilog < Date: Sat, 13 Apr 2024 17:20:32 +0200 Subject: [PATCH 21/44] cellmatch: Rename the special design to `$cellmatch` --- passes/techmap/cellmatch.cc | 4 ++-- tests/techmap/cellmatch.ys | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 5301cc99bfd..d1da6babd63 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -136,7 +136,7 @@ struct CellmatchPass : Pass { log("selected modules and a module from the secondary design . For every such\n"); log("correspondence found, a techmap rule is generated for mapping instances of the\n"); log("former to instances of the latter. This techmap rule is saved in yet another\n"); - log("design called '$cellmatch_map', which is created if non-existent.\n"); + log("design called '$cellmatch', which is created if non-existent.\n"); log("\n"); log("This pass restricts itself to combinational modules. Modules are functionally\n"); log("equivalent as long as their truth tables are identical upto a permutation of\n"); @@ -192,7 +192,7 @@ struct CellmatchPass : Pass { targets[p_classes].push_back(Target{m, luts}); } - auto r = saved_designs.emplace("$cellmatch_map", nullptr); + auto r = saved_designs.emplace("$cellmatch", nullptr); if (r.second) r.first->second = new Design; Design *map_design = r.first->second; diff --git a/tests/techmap/cellmatch.ys b/tests/techmap/cellmatch.ys index 46960fc1430..bea2f598d94 100644 --- a/tests/techmap/cellmatch.ys +++ b/tests/techmap/cellmatch.ys @@ -61,7 +61,7 @@ prep cellmatch -lib gatelib FA A:gate design -save gold -techmap -map %$cellmatch_map +techmap -map %$cellmatch design -save gate select -assert-none ripple_carry/t:FA From e939182e68edc26b4267f011f644067e29c7c25a Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 3 May 2024 12:11:55 +0200 Subject: [PATCH 22/44] cellmatch: add comments --- passes/techmap/cellmatch.cc | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index d1da6babd63..a21a4fbadc2 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -42,10 +42,16 @@ SigSpec module_outputs(Module *m) return ret; } +// Permute the inputs of a single-output k-LUT according to varmap uint64_t permute_lut(uint64_t lut, const std::vector &varmap) { int k = varmap.size(); uint64_t ret = 0; + // Index j iterates over all bits in lut. + // When (j & 1 << n) is true, + // (lut & 1 << j) represents an output value where input var n is set. + // We use this fact to permute the LUT such that + // every variable n is remapped to varmap[n]. for (int j = 0; j < 1 << k; j++) { int m = 0; for (int l = 0; l < k; l++) @@ -57,6 +63,10 @@ uint64_t permute_lut(uint64_t lut, const std::vector &varmap) return ret; } +// Find the LUT with the minimum integer representation +// such that it is a permutation of the given lut. +// The resulting LUT becomes the "fingerprint" of the "permutation class". +// This function checks all possible input permutations. uint64_t p_class(int k, uint64_t lut) { std::vector map; @@ -77,6 +87,9 @@ uint64_t p_class(int k, uint64_t lut) return repr; } +// Represent module m as N single-output k-LUTs +// where k is the number of module inputs, +// and N is the number of module outputs. bool derive_module_luts(Module *m, std::vector &luts) { CellTypes ff_types; @@ -185,7 +198,7 @@ struct CellmatchPass : Pass { continue; for (auto lut : luts) p_classes.insert(p_class(ninputs, lut)); - + log_debug("Registered %s\n", log_id(m)); // save as a viable target @@ -210,7 +223,7 @@ struct CellmatchPass : Pass { for (auto bit : outputs) { log_assert(bit.is_wire()); bit.wire->attributes[ID(p_class)] = p_class(inputs.size(), luts[no]); - bit.wire->attributes[ID(lut)] = luts[no++]; + bit.wire->attributes[ID(lut)] = luts[no++]; } } @@ -236,11 +249,13 @@ struct CellmatchPass : Pass { input_map.push_back(i); bool found_match = false; + // For each input_map while (!found_match) { std::vector output_map; for (int i = 0; i < outputs.size(); i++) output_map.push_back(i); + // For each output_map while (!found_match) { int out_no = 0; bool match = true; @@ -253,6 +268,8 @@ struct CellmatchPass : Pass { if (match) { log("Module %s matches %s\n", log_id(m), log_id(target.module)); + // Add target.module to map_design ("$cellmatch") + // as a techmap rule to match m and replace it with target.module Module *map = map_design->addModule(stringf("\\_60_%s_%s", log_id(m), log_id(target.module))); Cell *cell = map->addCell(ID::_TECHMAP_REPLACE_, target.module->name); @@ -281,7 +298,7 @@ struct CellmatchPass : Pass { } if (!std::next_permutation(output_map.begin(), output_map.end())) - break; + break; } if (!std::next_permutation(input_map.begin(), input_map.end())) From 0f9ee20ea2c9b377f9b28b862f77b197e6485e00 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 4 May 2024 00:16:00 +0000 Subject: [PATCH 23/44] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 2dbce272dc6..56efaf5eb0f 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+45 +YOSYS_VER := 0.40+50 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From bb0be8c7a20335f8e03597cfcf052609f8a1f4a4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 4 May 2024 16:51:29 +1200 Subject: [PATCH 24/44] Docs: Set release to YOSYS_VER If building from read the docs, and the current build is "latest", add `-dev` to the version string. Requires `YOSYS_VER` to be exported by .readthedocs.yaml. --- docs/source/conf.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/docs/source/conf.py b/docs/source/conf.py index 29d36d9c45f..aed3fddff7c 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -63,6 +63,14 @@ extensions.append('sphinx.ext.todo') todo_include_todos = False +# attempt to get version +env_yosys_ver = os.getenv("YOSYS_VER") +if env_yosys_ver: + if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": + release = env_yosys_ver + "-dev" + else: + release = env_yosys_ver + # custom cmd-ref parsing/linking sys.path += [os.path.dirname(__file__) + "/../"] extensions.append('util.cmdref') From fe27240b3a9c0be98dd16b3fc27cef61ddb50946 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 4 May 2024 16:51:38 +1200 Subject: [PATCH 25/44] Makefile: Export YOSYS_VER --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 56efaf5eb0f..2e93bcc8dc3 100644 --- a/Makefile +++ b/Makefile @@ -143,6 +143,7 @@ endif endif YOSYS_VER := 0.40+50 +export YOSYS_VER # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 6eb49ee9e830545e212f9aefe90d5bd130afa7a4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 7 May 2024 10:23:22 +1200 Subject: [PATCH 26/44] Makefile: Export YOSYS_VER only for make docs --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 2e93bcc8dc3..6711751b62d 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,6 @@ endif endif YOSYS_VER := 0.40+50 -export YOSYS_VER # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -1013,7 +1012,7 @@ docs/reqs: DOC_TARGET ?= html docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs - $(Q) $(MAKE) -C docs $(DOC_TARGET) + $(Q) YOSYS_VER=$(YOSYS_VER) $(MAKE) -C docs $(DOC_TARGET) clean: rm -rf share From b4034a881e0cf476bbdc19e984a9762bb260ad39 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 7 May 2024 15:35:25 +0200 Subject: [PATCH 27/44] Keep docs version in conf.py --- Makefile | 2 +- docs/source/conf.py | 19 +++++++++---------- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Makefile b/Makefile index 6711751b62d..56efaf5eb0f 100644 --- a/Makefile +++ b/Makefile @@ -1012,7 +1012,7 @@ docs/reqs: DOC_TARGET ?= html docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs - $(Q) YOSYS_VER=$(YOSYS_VER) $(MAKE) -C docs $(DOC_TARGET) + $(Q) $(MAKE) -C docs $(DOC_TARGET) clean: rm -rf share diff --git a/docs/source/conf.py b/docs/source/conf.py index aed3fddff7c..4e46cfad1b8 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -4,7 +4,8 @@ project = 'YosysHQ Yosys' author = 'YosysHQ GmbH' -copyright ='2022 YosysHQ GmbH' +copyright ='2024 YosysHQ GmbH' +yosys_ver = "0.40" # select HTML theme html_theme = 'furo' @@ -46,12 +47,18 @@ autosectionlabel_prefix_document = True autosectionlabel_maxdepth = 1 +# set version +if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": + release = yosys_ver + "-dev" +else: + release = yosys_ver + # assign figure numbers numfig = True bibtex_bibfiles = ['literature.bib'] - latex_elements = { + 'releasename': ' ', 'preamble': r''' \usepackage{lmodern} \usepackage{comment} @@ -63,14 +70,6 @@ extensions.append('sphinx.ext.todo') todo_include_todos = False -# attempt to get version -env_yosys_ver = os.getenv("YOSYS_VER") -if env_yosys_ver: - if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": - release = env_yosys_ver + "-dev" - else: - release = env_yosys_ver - # custom cmd-ref parsing/linking sys.path += [os.path.dirname(__file__) + "/../"] extensions.append('util.cmdref') From 71f2540cd840046499e1dd84c76ea64c437140d3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 7 May 2024 15:55:52 +0200 Subject: [PATCH 28/44] docs conf.py change Release -> Version --- docs/source/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 4e46cfad1b8..182d033f8ce 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -58,7 +58,7 @@ bibtex_bibfiles = ['literature.bib'] latex_elements = { - 'releasename': ' ', + 'releasename': 'Version', 'preamble': r''' \usepackage{lmodern} \usepackage{comment} From a52088b6af5c4467835de173d83a00645546eddf Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 7 May 2024 17:57:37 +0200 Subject: [PATCH 29/44] smtbmc: Improvements for --incremental and .yw fixes This extends the experimental incremental JSON API to allow arbitrary smtlib subexpressions, defining smtlib constants and to allow access of signals by their .yw path. It also fixes a bug during .yw writing where values would be re-emitted in later cycles if they have no newer defined value and a potential crash when using --track-assumes. --- backends/smt2/smtbmc.py | 203 +++++++++++++++++----------- backends/smt2/smtbmc_incremental.py | 147 ++++++++++++++++++-- backends/smt2/smtio.py | 21 ++- 3 files changed, 279 insertions(+), 92 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e6b4088dbd7..995a714c926 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -199,7 +199,6 @@ def help(): --minimize-assumes when using --track-assumes, solve for a minimal set of sufficient assumptions. - """ + so.helpmsg()) def usage(): @@ -670,18 +669,12 @@ def print_msg(msg): ywfile_hierwitness_cache = None -def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): +def ywfile_hierwitness(): global ywfile_hierwitness_cache - if map_steps is None: - map_steps = {} - - with open(inywfile, "r") as f: - inyw = ReadWitness(f) - - if ywfile_hierwitness_cache is None: - ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness = smt.hierwitness(topmod, allregs=True, blackbox=True) - inits, seqs, clocks, mems = ywfile_hierwitness_cache + inits, seqs, clocks, mems = ywfile_hierwitness smt_wires = defaultdict(list) smt_mems = defaultdict(list) @@ -692,91 +685,147 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): for mem in mems: smt_mems[mem["path"]].append(mem) - addr_re = re.compile(r'\\\[[0-9]+\]$') - bits_re = re.compile(r'[01?]*$') + ywfile_hierwitness_cache = inits, seqs, clocks, mems, smt_wires, smt_mems - max_t = -1 + return ywfile_hierwitness_cache - for t, step in inyw.steps(): - present_signals, missing = step.present_signals(inyw.sigmap) - for sig in present_signals: - bits = step[sig] - if skip_x: - bits = bits.replace('x', '?') - if not bits_re.match(bits): - raise ValueError("unsupported bit value in Yosys witness file") +def_bits_re = re.compile(r'([01]+)') - sig_end = sig.offset + len(bits) - if sig.path in smt_wires: - for wire in smt_wires[sig.path]: - width, offset = wire["width"], wire["offset"] +def smt_extract_mask(smt_expr, mask): + chunks = [] + def_bits = '' - smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + mask_index_order = mask[::-1] - offset = max(offset, 0) + for matched in def_bits_re.finditer(mask_index_order): + chunks.append(matched.span()) + def_bits += matched[0] - end = width + offset - common_offset = max(sig.offset, offset) - common_end = min(sig_end, end) - if common_end <= common_offset: - continue + if not chunks: + return - smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire) + if len(chunks) == 1: + start, end = chunks[0] + if start == 0 and end == len(mask_index_order): + combined_chunks = smt_expr + else: + combined_chunks = '((_ extract %d %d) %s)' % (end - 1, start, smt_expr) + else: + combined_chunks = '(let ((x %s)) (concat %s))' % (smt_expr, ' '.join( + '((_ extract %d %d) x)' % (end - 1, start) + for start, end in reversed(chunks) + )) - if not smt_bool: - slice_high = common_end - offset - 1 - slice_low = common_offset - offset - smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] - bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] +def smt_concat(exprs): + if not exprs: + return "" + if len(exprs) == 1: + return exprs[1] + return "(concat %s)" % ' '.join(exprs) - if bit_slice.count("?") == len(bit_slice): - continue +def ywfile_signal(sig, step, mask=None): + assert sig.width > 0 - if smt_bool: - assert width == 1 - smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false") - else: - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + sig_end = sig.offset + sig.width - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + output = [] - constr_assumes[t].append((inywfile, smt_constr)) + if sig.path in smt_wires: + for wire in smt_wires[sig.path]: + width, offset = wire["width"], wire["offset"] - if sig.memory_path: - if sig.memory_path in smt_mems: - for mem in smt_mems[sig.memory_path]: - width, size, bv = mem["width"], mem["size"], mem["statebv"] + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 - smt_expr = smt.net_expr(topmod, f"s{map_steps.get(t, t)}", mem["smtpath"]) + offset = max(offset, 0) - if bv: - word_low = sig.memory_addr * width - word_high = word_low + width - 1 - smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) - else: - addr_width = (size - 1).bit_length() - addr_bits = f"{sig.memory_addr:0{addr_width}b}" - smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue - if len(bits) < width: - slice_high = sig.offset + len(bits) - 1 - smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire) - bit_slice = bits + if not smt_bool: + slice_high = common_end - offset - 1 + slice_low = common_offset - offset + smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + else: + smt_expr = "(ite %s #b1 #b0)" % smt_expr - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr)) - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - constr_assumes[t].append((inywfile, smt_constr)) - max_t = t + if sig.memory_path: + if sig.memory_path in smt_mems: + for mem in smt_mems[sig.memory_path]: + width, size, bv = mem["width"], mem["size"], mem["statebv"] + + smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"]) + + if bv: + word_low = sig.memory_addr * width + word_high = word_low + width - 1 + smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) + else: + addr_width = (size - 1).bit_length() + addr_bits = f"{sig.memory_addr:0{addr_width}b}" + smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + + if sig.width < width: + slice_high = sig.offset + sig.width - 1 + smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + output.append((0, sig.width, smt_expr)) + + output.sort() + + output = [chunk for chunk in output if chunk[0] != chunk[1]] + + pos = 0 + + for start, end, smt_expr in output: + assert start == pos + pos = end + + assert pos == sig.width + + if len(output) == 1: + return output[0][-1] + return smt_concat(smt_expr for start, end, smt_expr in reversed(output)) + +def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache + if map_steps is None: + map_steps = {} + + with open(inywfile, "r") as f: + inyw = ReadWitness(f) + + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + + bits_re = re.compile(r'[01?]*$') + max_t = -1 + + for t, step in inyw.steps(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if skip_x: + bits = bits.replace('x', '?') + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") + + smt_expr = ywfile_signal(sig, map_steps.get(t, t)) + + smt_expr, bits = smt_extract_mask(smt_expr, bits) + + smt_constr = "(= %s #b%s)" % (smt_expr, bits) + constr_assumes[t].append((inywfile, smt_constr)) + + max_t = t return max_t if inywfile is not None: @@ -1367,11 +1416,11 @@ def write_yw_trace(steps, index, allregs=False, filename=None): exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) - all_sigs.append(sigs) + all_sigs.append((step_values, sigs)) bvs = iter(smt.get_list(exprs)) - for sigs in all_sigs: + for (step_values, sigs) in all_sigs: for sig in sigs: value = smt.bv2bin(next(bvs)) step_values[sig["sig"]] = value diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index f43e878f31c..0bd280b4a48 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -1,7 +1,7 @@ from collections import defaultdict import json import typing -from functools import partial +import ywio if typing.TYPE_CHECKING: import smtbmc @@ -34,6 +34,7 @@ def __init__(self): self._witness_index = None self._yw_constraints = {} + self._define_sorts = {} def setup(self): generic_assert_map = smtbmc.get_assert_map( @@ -175,11 +176,7 @@ def expr_andor(self, expr, smt_out): if len(expr) == 1: smt_out.push({"and": "true", "or": "false"}[expr[0]]) elif len(expr) == 2: - arg_sort = self.expr(expr[1], smt_out) - if arg_sort != "Bool": - raise InteractiveError( - f"arguments of {json.dumps(expr[0])} must have sort Bool" - ) + self.expr(expr[1], smt_out, required_sort="Bool") else: sep = f"({expr[0]} " for arg in expr[1:]: @@ -189,7 +186,51 @@ def expr_andor(self, expr, smt_out): smt_out.append(")") return "Bool" + def expr_bv_binop(self, expr, smt_out): + self.expr_arg_len(expr, 2) + + smt_out.append(f"({expr[0]} ") + arg_sort = self.expr(expr[1], smt_out, required_sort=("BitVec", None)) + smt_out.append(" ") + self.expr(expr[2], smt_out, required_sort=arg_sort) + smt_out.append(")") + return arg_sort + + def expr_extract(self, expr, smt_out): + self.expr_arg_len(expr, 3) + + hi = expr[1] + lo = expr[2] + + smt_out.append(f"((_ extract {hi} {lo}) ") + + arg_sort = self.expr(expr[3], smt_out, required_sort=("BitVec", None)) + smt_out.append(")") + + if not (isinstance(hi, int) and 0 <= hi < arg_sort[1]): + raise InteractiveError( + f"high bit index must be 0 <= index < {arg_sort[1]}, is {hi!r}" + ) + if not (isinstance(lo, int) and 0 <= lo <= hi): + raise InteractiveError( + f"low bit index must be 0 <= index < {hi}, is {lo!r}" + ) + + return "BitVec", hi - lo + 1 + + def expr_bv(self, expr, smt_out): + self.expr_arg_len(expr, 1) + + arg = expr[1] + if not isinstance(arg, str) or arg.count("0") + arg.count("1") != len(arg): + raise InteractiveError("bv argument must contain only 0 or 1 bits") + + smt_out.append("#b" + arg) + + return "BitVec", len(arg) + def expr_yw(self, expr, smt_out): + self.expr_arg_len(expr, 1, 2) if len(expr) == 2: name = None step = expr[1] @@ -219,6 +260,40 @@ def expr_yw(self, expr, smt_out): return "Bool" + def expr_yw_sig(self, expr, smt_out): + self.expr_arg_len(expr, 3, 4) + + step = expr[1] + path = expr[2] + offset = expr[3] + width = expr[4] if len(expr) == 5 else 1 + + if not isinstance(offset, int) or offset < 0: + raise InteractiveError( + f"offset must be a non-negative integer, got {json.dumps(offset)}" + ) + + if not isinstance(width, int) or width <= 0: + raise InteractiveError( + f"width must be a positive integer, got {json.dumps(width)}" + ) + + if not isinstance(path, list) or not all(isinstance(s, str) for s in path): + raise InteractiveError( + f"path must be a string list, got {json.dumps(path)}" + ) + + if step not in self.state_set: + raise InteractiveError(f"step {step} not declared") + + smt_expr = smtbmc.ywfile_signal( + ywio.WitnessSig(path=path, offset=offset, width=width), step + ) + + smt_out.append(smt_expr) + + return "BitVec", width + def expr_smtlib(self, expr, smt_out): self.expr_arg_len(expr, 2) @@ -231,10 +306,15 @@ def expr_smtlib(self, expr, smt_out): f"got {json.dumps(smtlib_expr)}" ) - if not isinstance(sort, str): - raise InteractiveError( - f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}" - ) + if ( + isinstance(sort, list) + and len(sort) == 2 + and sort[0] == "BitVec" + and (sort[1] is None or isinstance(sort[1], int)) + ): + sort = tuple(sort) + elif not isinstance(sort, str): + raise InteractiveError(f"unsupported raw SMT-LIB sort {json.dumps(sort)}") smt_out.append(smtlib_expr) return sort @@ -258,6 +338,14 @@ def expr_label(self, expr, smt_out): return sort + def expr_def(self, expr, smt_out): + self.expr_arg_len(expr, 1) + sort = self._define_sorts.get(expr[1]) + if sort is None: + raise InteractiveError(f"unknown definition {json.dumps(expr)}") + smt_out.append(expr[1]) + return sort + expr_handlers = { "step": expr_step, "cell": expr_cell, @@ -270,8 +358,15 @@ def expr_label(self, expr, smt_out): "not": expr_not, "and": expr_andor, "or": expr_andor, + "bv": expr_bv, + "bvand": expr_bv_binop, + "bvor": expr_bv_binop, + "bvxor": expr_bv_binop, + "extract": expr_extract, + "def": expr_def, "=": expr_eq, "yw": expr_yw, + "yw_sig": expr_yw_sig, "smtlib": expr_smtlib, "!": expr_label, } @@ -305,10 +400,13 @@ def expr(self, expr, smt_out, required_sort=None): raise InteractiveError(f"unknown expression {json.dumps(expr[0])}") def expr_smt(self, expr, required_sort): + return self.expr_smt_and_sort(expr, required_sort)[0] + + def expr_smt_and_sort(self, expr, required_sort=None): smt_out = [] - self.expr(expr, smt_out, required_sort=required_sort) + output_sort = self.expr(expr, smt_out, required_sort=required_sort) out = "".join(smt_out) - return out + return out, output_sort def cmd_new_step(self, cmd): step = self.arg_step(cmd, declare=True) @@ -338,7 +436,6 @@ def cmd_update_assumptions(self, cmd): expr = cmd.get("expr") key = cmd.get("key") - key = mkkey(key) result = smtbmc.smt.smt2_assumptions.pop(key, None) @@ -348,7 +445,7 @@ def cmd_update_assumptions(self, cmd): return result def cmd_get_unsat_assumptions(self, cmd): - return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize'))) + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get("minimize"))) def cmd_push(self, cmd): smtbmc.smt_push() @@ -370,6 +467,27 @@ def cmd_smtlib(self, cmd): if response: return smtbmc.smt.read() + def cmd_define(self, cmd): + expr = cmd.get("expr") + if expr is None: + raise InteractiveError("'define' copmmand requires 'expr' parameter") + + expr, sort = self.expr_smt_and_sort(expr) + + if isinstance(sort, tuple) and sort[0] == "module": + raise InteractiveError("'define' does not support module sorts") + + define_name = f"|inc def {len(self._define_sorts)}|" + + self._define_sorts[define_name] = sort + + if isinstance(sort, tuple): + sort = f"(_ {' '.join(map(str, sort))})" + + smtbmc.smt.write(f"(define-const {define_name} {sort} {expr})") + + return {"name": define_name} + def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) if self._cached_hierwitness[allregs] is not None: @@ -451,6 +569,7 @@ def cmd_ping(self, cmd): "pop": cmd_pop, "check": cmd_check, "smtlib": cmd_smtlib, + "define": cmd_define, "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e32f43c60a0..5fc3ab5a424 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -160,6 +160,7 @@ def __init__(self, opts=None): self.noincr = opts.noincr self.info_stmts = opts.info_stmts self.nocomments = opts.nocomments + self.smt2_options.update(opts.smt2_options) else: self.solver = "yices" @@ -959,6 +960,8 @@ def bv2int(self, v): return int(self.bv2bin(v), 2) def get_raw_unsat_assumptions(self): + if not self.smt2_assumptions: + return [] self.write("(get-unsat-assumptions)") exprs = set(self.unparse(part) for part in self.parse(self.read())) unsat_assumptions = [] @@ -973,6 +976,10 @@ def get_raw_unsat_assumptions(self): def get_unsat_assumptions(self, minimize=False): if not minimize: return self.get_raw_unsat_assumptions() + orig_assumptions = self.smt2_assumptions + + self.smt2_assumptions = dict(orig_assumptions) + required_assumptions = {} while True: @@ -998,6 +1005,7 @@ def get_unsat_assumptions(self, minimize=False): required_assumptions[candidate_key] = candidate_assume if candidate_assumptions is not None: + self.smt2_assumptions = orig_assumptions return list(required_assumptions) def get(self, expr): @@ -1146,7 +1154,7 @@ def wait(self): class SmtOpts: def __init__(self): self.shortopts = "s:S:v" - self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] + self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments", "smt2-option="] self.solver = "yices" self.solver_opts = list() self.debug_print = False @@ -1159,6 +1167,7 @@ def __init__(self): self.logic = None self.info_stmts = list() self.nocomments = False + self.smt2_options = {} def handle(self, o, a): if o == "-s": @@ -1185,6 +1194,13 @@ def handle(self, o, a): self.info_stmts.append(a) elif o == "--nocomments": self.nocomments = True + elif o == "--smt2-option": + args = a.split('=', 1) + if len(args) != 2: + print("--smt2-option expects an