From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 21 Jul 2022 14:22:15 +0200 Subject: Add the $anyinit cell and the formalff pass These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. --- CHANGELOG | 6 ++ kernel/celltypes.h | 6 ++ kernel/ff.cc | 19 ++++- kernel/ff.h | 8 +- kernel/rtlil.cc | 17 ++++ kernel/rtlil.h | 2 + kernel/satgen.cc | 2 +- manual/CHAPTER_CellLib.tex | 2 +- passes/cmds/show.cc | 1 + passes/fsm/fsm_detect.cc | 1 + passes/hierarchy/submod.cc | 1 + passes/opt/opt_clean.cc | 2 + passes/sat/Makefile.inc | 1 + passes/sat/formalff.cc | 192 +++++++++++++++++++++++++++++++++++++++++++++ passes/sat/sim.cc | 2 +- techlibs/common/simlib.v | 17 ++++ 16 files changed, 271 insertions(+), 8 deletions(-) create mode 100644 passes/sat/formalff.cc diff --git a/CHANGELOG b/CHANGELOG index 434872248..199d6a61a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -4,6 +4,12 @@ List of major changes and improvements between releases Yosys 0.20 .. Yosys 0.20-dev -------------------------- + * New commands and options + - Added "formalff" pass - transforms FFs for formal verification + + * Formal Verification + - Added $anyinit cell to directly represent FFs with an unconstrained + initialization value. These can be generated by the new formalff pass. Yosys 0.19 .. Yosys 0.20 -------------------------- diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 7e9cfb38d..d62ba1506 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -51,6 +51,7 @@ struct CellTypes setup_internals(); setup_internals_mem(); + setup_internals_anyinit(); setup_stdcells(); setup_stdcells_mem(); } @@ -155,6 +156,11 @@ struct CellTypes setup_type(ID($dlatchsr), {ID::EN, ID::SET, ID::CLR, ID::D}, {ID::Q}); } + void setup_internals_anyinit() + { + setup_type(ID($anyinit), {ID::D}, {ID::Q}); + } + void setup_internals_mem() { setup_internals_ff(); diff --git a/kernel/ff.cc b/kernel/ff.cc index b0f1a924f..697ba7342 100644 --- a/kernel/ff.cc +++ b/kernel/ff.cc @@ -33,10 +33,14 @@ FfData::FfData(FfInitVals *initvals, Cell *cell_) : FfData(cell_->module, initva std::string type_str = cell->type.str(); - if (cell->type.in(ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) { - if (cell->type == ID($ff)) { + if (cell->type.in(ID($anyinit), ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) { + if (cell->type.in(ID($anyinit), ID($ff))) { has_gclk = true; sig_d = cell->getPort(ID::D); + if (cell->type == ID($anyinit)) { + is_anyinit = true; + log_assert(val_init.is_fully_undef()); + } } else if (cell->type == ID($sr)) { // No data input at all. } else if (cell->type.in(ID($dlatch), ID($adlatch), ID($dlatchsr))) { @@ -274,6 +278,7 @@ FfData FfData::slice(const std::vector &bits) { res.has_sr = has_sr; res.ce_over_srst = ce_over_srst; res.is_fine = is_fine; + res.is_anyinit = is_anyinit; res.pol_clk = pol_clk; res.pol_ce = pol_ce; res.pol_aload = pol_aload; @@ -542,7 +547,7 @@ Cell *FfData::emit() { return nullptr; } } - if (initvals) + if (initvals && !is_anyinit) initvals->set_init(sig_q, val_init); if (!is_fine) { if (has_gclk) { @@ -552,7 +557,12 @@ Cell *FfData::emit() { log_assert(!has_arst); log_assert(!has_srst); log_assert(!has_sr); - cell = module->addFf(name, sig_d, sig_q); + if (is_anyinit) { + cell = module->addAnyinit(name, sig_d, sig_q); + log_assert(val_init.is_fully_undef()); + } else { + cell = module->addFf(name, sig_d, sig_q); + } } else if (!has_aload && !has_clk) { log_assert(has_sr); cell = module->addSr(name, sig_set, sig_clr, sig_q, pol_set, pol_clr); @@ -603,6 +613,7 @@ Cell *FfData::emit() { log_assert(!has_arst); log_assert(!has_srst); log_assert(!has_sr); + log_assert(!is_anyinit); cell = module->addFfGate(name, sig_d, sig_q); } else if (!has_aload && !has_clk) { log_assert(has_sr); diff --git a/kernel/ff.h b/kernel/ff.h index 41721b4a1..e684d3c43 100644 --- a/kernel/ff.h +++ b/kernel/ff.h @@ -28,7 +28,10 @@ YOSYS_NAMESPACE_BEGIN // Describes a flip-flop or a latch. // // If has_gclk, this is a formal verification FF with implicit global clock: -// Q is simply previous cycle's D. +// Q is simply previous cycle's D. Additionally if is_anyinit is true, this is +// an $anyinit cell which always has an undefined initialization value. Note +// that $anyinit is not considered to be among the FF celltypes, so a pass has +// to explicitly opt-in to process $anyinit cells with FfData. // // Otherwise, the FF/latch can have any number of features selected by has_* // attributes that determine Q's value (in order of decreasing priority): @@ -126,6 +129,8 @@ struct FfData { // True if this FF is a fine cell, false if it is a coarse cell. // If true, width must be 1. bool is_fine; + // True if this FF is an $anyinit cell. Depends on has_gclk. + bool is_anyinit; // Polarities, corresponding to sig_*. True means active-high, false // means active-low. bool pol_clk; @@ -156,6 +161,7 @@ struct FfData { has_sr = false; ce_over_srst = false; is_fine = false; + is_anyinit = false; pol_clk = false; pol_aload = false; pol_ce = false; diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index b274bba78..5211c3b3f 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1632,6 +1632,13 @@ namespace { return; } + if (cell->type.in(ID($anyinit))) { + port(ID::D, param(ID::WIDTH)); + port(ID::Q, param(ID::WIDTH)); + check_expected(); + return; + } + if (cell->type == ID($equiv)) { port(ID::A, 1); port(ID::B, 1); @@ -3120,6 +3127,16 @@ RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, const RTLIL::S return cell; } +RTLIL::Cell* RTLIL::Module::addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src) +{ + RTLIL::Cell *cell = addCell(name, ID($anyinit)); + cell->parameters[ID::WIDTH] = sig_q.size(); + cell->setPort(ID::D, sig_d); + cell->setPort(ID::Q, sig_q); + cell->set_src_attribute(src); + return cell; +} + RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width, const std::string &src) { RTLIL::SigSpec sig = addWire(NEW_ID, width); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index db175d7e9..27ffdff1f 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1375,6 +1375,8 @@ public: RTLIL::Cell* addDlatchsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = ""); + RTLIL::Cell* addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src = ""); + // The methods without the add* prefix create a cell and an output signal. They return the newly created output signal. RTLIL::SigSpec Not (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, bool is_signed = false, const std::string &src = ""); diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 9c40ec66d..05eeca76e 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1176,7 +1176,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type)) + if (timestep > 0 && (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit))) { FfData ff(nullptr, cell); diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 3c9fb31cc..86b1f6a9a 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -603,7 +603,7 @@ Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} c \begin{fixme} Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv}, -{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells. +{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$anyinit}, {\tt \$allconst}, {\tt \$allseq} cells. \end{fixme} \begin{fixme} diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 43deba47b..4d5605932 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -574,6 +574,7 @@ struct ShowWorker { ct.setup_internals(); ct.setup_internals_mem(); + ct.setup_internals_anyinit(); ct.setup_stdcells(); ct.setup_stdcells_mem(); ct.setup_design(design); diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc index a2d38a0bd..f829714c4 100644 --- a/passes/fsm/fsm_detect.cc +++ b/passes/fsm/fsm_detect.cc @@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass { CellTypes ct; ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc index 845dc850f..c0c40671d 100644 --- a/passes/hierarchy/submod.cc +++ b/passes/hierarchy/submod.cc @@ -260,6 +260,7 @@ struct SubmodWorker } ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index cb2c261c4..dde7c5299 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -633,6 +633,7 @@ struct OptCleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); @@ -694,6 +695,7 @@ struct CleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index da6d49433..ebe3dc536 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o +OBJS += passes/sat/formalff.o OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc new file mode 100644 index 000000000..fe6f98c16 --- /dev/null +++ b/passes/sat/formalff.cc @@ -0,0 +1,192 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/ffinit.h" +#include "kernel/ff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct FormalFfPass : public Pass { + FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" formalff [options] [selection]\n"); + log("\n"); + log("This pass transforms clocked flip-flops to prepare a design for formal\n"); + log("verification. If a design contains latches and/or multiple different clocks run\n"); + log("the async2sync or clk2fflogic passes before using this pass.\n"); + log("\n"); + log(" -clk2ff\n"); + log(" Replace all clocked flip-flops with $ff cells that use the implicit\n"); + log(" global clock. This assumes, without checking, that the design uses a\n"); + log(" single global clock. If that is not the case, the clk2fflogic pass\n"); + log(" should be used instead.\n"); + log("\n"); + log(" -ff2anyinit\n"); + log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n"); + log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n"); + log(" initialization value. The difference is that $anyinit inhibits\n"); + log(" don't-care optimizations and is used to track solver-provided values\n"); + log(" in witness traces.\n"); + log("\n"); + log(" If combined with -clk2ff this also affects newly created $ff cells.\n"); + log("\n"); + log(" -anyinit2ff\n"); + log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n"); + log(" reverse of -ff2anyinit and can be used, before running a backend pass\n"); + log(" (or similar) that is not yet aware of $anyinit cells.\n"); + log("\n"); + log(" Note that after running -anyinit2ff, in general, performing don't-care\n"); + log(" optimizations is not sound in a formal verification setting.\n"); + log("\n"); + log(" -fine\n"); + log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n"); + log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n"); + log("\n"); + + // TODO: An option to check whether all FFs use the same clock before changing it to the global clock + } + void execute(std::vector args, RTLIL::Design *design) override + { + bool flag_clk2ff = false; + bool flag_ff2anyinit = false; + bool flag_anyinit2ff = false; + bool flag_fine = false; + + log_header(design, "Executing FORMALFF pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-clk2ff") { + flag_clk2ff = true; + continue; + } + if (args[argidx] == "-ff2anyinit") { + flag_ff2anyinit = true; + continue; + } + if (args[argidx] == "-anyinit2ff") { + flag_anyinit2ff = true; + continue; + } + if (args[argidx] == "-fine") { + flag_fine = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n"); + + if (flag_ff2anyinit && flag_anyinit2ff) + log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n"); + + if (flag_fine && !flag_anyinit2ff) + log_cmd_error("The option -fine requries the -anyinit2ff option.\n"); + + if (flag_fine && flag_clk2ff) + log_cmd_error("The options -fine and -clk2ff are exclusive.\n"); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + FfInitVals initvals(&sigmap, module); + + + for (auto cell : module->selected_cells()) + { + if (flag_anyinit2ff && cell->type == ID($anyinit)) + { + FfData ff(&initvals, cell); + ff.remove(); + ff.is_anyinit = false; + ff.is_fine = flag_fine; + if (flag_fine) + for (int i = 0; i < ff.width; i++) + ff.slice({i}).emit(); + else + ff.emit(); + + continue; + } + + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; + + FfData ff(&initvals, cell); + bool emit = false; + + if (flag_clk2ff && ff.has_clk) { + if (ff.sig_clk.is_fully_const()) + log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", + log_id(cell), log_id(cell->type), log_id(module)); + + ff.unmap_ce_srst(); + ff.has_clk = false; + ff.has_gclk = true; + emit = true; + } + + if (!ff.has_gclk) { + continue; + } + + if (flag_ff2anyinit && !ff.val_init.is_fully_def()) + { + ff.remove(); + emit = false; + + int cursor = 0; + while (cursor < ff.val_init.size()) + { + bool is_anyinit = ff.val_init[cursor] == State::Sx; + std::vector bits; + bits.push_back(cursor++); + while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit) + bits.push_back(cursor++); + + if ((int)bits.size() == ff.val_init.size()) { + // This check is only to make the private names more helpful for debugging + ff.is_anyinit = true; + emit = true; + break; + } + + auto slice = ff.slice(bits); + slice.is_anyinit = is_anyinit; + slice.emit(); + } + } + + if (emit) + ff.emit(); + } + } + } +} FormalFfPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 53644c6b7..ea64dce06 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -231,7 +231,7 @@ struct SimInstance } } - if (RTLIL::builtin_ff_cell_types().count(cell->type)) { + if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) { FfData ff_data(nullptr, cell); ff_state_t ff; ff.past_d = Const(State::Sx, ff_data.width); diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index b14488ff4..ab9bd7e1d 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1696,6 +1696,23 @@ assign Y = 'bx; endmodule +// -------------------------------------------------------- +`ifdef SIMLIB_FF +module \$anyinit (D, Q); + +parameter WIDTH = 0; + +input [WIDTH-1:0] D; +output reg [WIDTH-1:0] Q; + +initial Q <= 'bx; + +always @($global_clk) begin + Q <= D; +end + +endmodule +`endif // -------------------------------------------------------- module \$allconst (Y); -- cgit v1.2.3 From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:49:51 +0200 Subject: formalff: Set new replaced_by_gclk attribute on removed dff's clks This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute. --- backends/btor/btor.cc | 10 ++++++++++ backends/smt2/smt2.cc | 11 +++++++++++ kernel/constids.inc | 1 + passes/sat/formalff.cc | 22 ++++++++++++++++++++++ 4 files changed, 44 insertions(+) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 831a3ada2..6dae7156a 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1112,6 +1112,16 @@ struct BtorWorker btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str()); add_nid_sig(nid, sig); + + if (!info_filename.empty()) { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + if (gclk_attr->second == State::S1) + info_clocks[nid] |= 1; + else if (gclk_attr->second == State::S0) + info_clocks[nid] |= 2; + } + } } btorf_pop("inputs"); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index f6c3560c1..126ee1175 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -239,6 +239,17 @@ struct Smt2Worker clock_negedge.erase(bit); } + for (auto wire : module->wires()) + { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + if (gclk_attr->second == State::S1) + clock_posedge.insert(sigmap(wire)); + else if (gclk_attr->second == State::S0) + clock_negedge.insert(sigmap(wire)); + } + } + for (auto wire : module->wires()) { if (!wire->port_input || GetSize(wire) != 1) diff --git a/kernel/constids.inc b/kernel/constids.inc index 0f6dfc29b..239381f85 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -171,6 +171,7 @@ X(RD_TRANSPARENCY_MASK) X(RD_TRANSPARENT) X(RD_WIDE_CONTINUATION) X(reg) +X(replaced_by_gclk) X(reprocess_after) X(rom_block) X(rom_style) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index fe6f98c16..0c85c3442 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -145,6 +145,28 @@ struct FormalFfPass : public Pass { log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", log_id(cell), log_id(cell->type), log_id(module)); + auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr; + + if (clk_wire == nullptr) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), ff.sig_clk); + } + + auto clk_polarity = ff.pol_clk ? State::S1 : State::S0; + + std::string attribute = clk_wire->get_string_attribute(ID::replaced_by_gclk); + + auto &attr = clk_wire->attributes[ID::replaced_by_gclk]; + + if (!attr.empty() && attr != clk_polarity) + log_error("CLK %s on %s (%s) from module %s also used with opposite polarity, run clk2fflogic instead.\n", + log_id(clk_wire), log_id(cell), log_id(cell->type), log_id(module)); + + attr = clk_polarity; + clk_wire->set_bool_attribute(ID::keep); + + // TODO propagate the replaced_by_gclk attribute upwards throughout the hierarchy + ff.unmap_ce_srst(); ff.has_clk = false; ff.has_gclk = true; -- cgit v1.2.3 From 95db5a9d3899973c0c7bcfa887f8404ac017d53f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:43:08 +0200 Subject: formalff: New -setundef option Find FFs with undefined initialization values for which changing the initialization does not change the observable behavior and initialize them. For -ff2anyinit, this reduces the number of generated $anyinit cells that drive wires with private names. --- passes/sat/formalff.cc | 335 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 335 insertions(+) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index 0c85c3442..209486a37 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -21,10 +21,302 @@ #include "kernel/sigtools.h" #include "kernel/ffinit.h" #include "kernel/ff.h" +#include "kernel/modtools.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN + +// Finds signal values with known constant or known unused values in the initial state +struct InitValWorker +{ + Module *module; + + ModWalker modwalker; + SigMap &sigmap; + FfInitVals initvals; + + dict initconst_bits; + dict used_bits; + + InitValWorker(Module *module) : module(module), modwalker(module->design), sigmap(modwalker.sigmap) + { + modwalker.setup(module); + initvals.set(&modwalker.sigmap, module); + + for (auto wire : module->wires()) + if (wire->name.isPublic() || wire->get_bool_attribute(ID::keep)) + for (auto bit : SigSpec(wire)) + used_bits[sigmap(bit)] = true; + } + + // Sign/Zero-extended indexing of individual port bits + static SigBit bit_in_port(RTLIL::Cell *cell, RTLIL::IdString port, RTLIL::IdString sign, int index) + { + auto sig_port = cell->getPort(port); + if (index < GetSize(sig_port)) + return sig_port[index]; + else if (cell->getParam(sign).as_bool()) + return GetSize(sig_port) > 0 ? sig_port[GetSize(sig_port) - 1] : State::Sx; + else + return State::S0; + } + + // Has the signal a known constant value in the initial state? + // + // For sync-only FFs outputs, this is their initval. For logic loops, + // multiple drivers or unknown cells this is Sx. For a small number of + // handled cells we recurse through their inputs. All results are cached. + RTLIL::State initconst(SigBit bit) + { + sigmap.apply(bit); + + if (!bit.is_wire()) + return bit.data; + + auto it = initconst_bits.find(bit); + if (it != initconst_bits.end()) + return it->second; + + // Setting this temporarily to x takes care of any logic loops + initconst_bits[bit] = State::Sx; + + pool portbits; + modwalker.get_drivers(portbits, {bit}); + + if (portbits.size() != 1) + return State::Sx; + + ModWalker::PortBit portbit = *portbits.begin(); + RTLIL::Cell *cell = portbit.cell; + + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&initvals, cell); + + if (ff.has_aload || ff.has_sr || ff.has_arst || (!ff.has_clk && !ff.has_gclk)) { + for (auto bit_q : ff.sig_q) { + initconst_bits[sigmap(bit_q)] = State::Sx; + } + return State::Sx; + } + + for (int i = 0; i < ff.width; i++) { + initconst_bits[sigmap(ff.sig_q[i])] = ff.val_init[i]; + } + + return ff.val_init[portbit.offset]; + } + + if (cell->type.in(ID($mux), ID($and), ID($or), ID($eq), ID($eqx), ID($initstate))) + { + if (cell->type == ID($mux)) + { + SigBit sig_s = sigmap(cell->getPort(ID::S)); + State init_s = initconst(sig_s); + State init_y; + + if (init_s == State::S0) { + init_y = initconst(cell->getPort(ID::A)[portbit.offset]); + } else if (init_s == State::S1) { + init_y = initconst(cell->getPort(ID::B)[portbit.offset]); + } else { + State init_a = initconst(cell->getPort(ID::A)[portbit.offset]); + State init_b = initconst(cell->getPort(ID::B)[portbit.offset]); + init_y = init_a == init_b ? init_a : State::Sx; + } + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type.in(ID($and), ID($or))) + { + State init_a = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, portbit.offset)); + State init_b = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, portbit.offset)); + State init_y; + if (init_a == init_b) + init_y = init_a; + else if (cell->type == ID($and) && (init_a == State::S0 || init_b == State::S0)) + init_y = State::S0; + else if (cell->type == ID($or) && (init_a == State::S1 || init_b == State::S1)) + init_y = State::S1; + else + init_y = State::Sx; + + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type.in(ID($eq), ID($eqx))) // Treats $eqx as $eq + { + if (portbit.offset > 0) { + initconst_bits[bit] = State::S0; + return State::S0; + } + + SigSpec sig_a = cell->getPort(ID::A); + SigSpec sig_b = cell->getPort(ID::B); + + State init_y = State::S1; + + for (int i = 0; init_y != State::S0 && i < GetSize(sig_a); i++) { + State init_ai = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, i)); + if (init_ai == State::Sx) { + init_y = State::Sx; + continue; + } + State init_bi = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, i)); + if (init_bi == State::Sx) + init_y = State::Sx; + else if (init_ai != init_bi) + init_y = State::S0; + } + + initconst_bits[bit] = init_y; + return init_y; + } + + if (cell->type == ID($initstate)) + { + initconst_bits[bit] = State::S1; + return State::S1; + } + + log_assert(false); + } + + return State::Sx; + } + + RTLIL::Const initconst(SigSpec sig) + { + std::vector bits; + for (auto bit : sig) + bits.push_back(initconst(bit)); + return bits; + } + + // Is the initial value of this signal used? + // + // An initial value of a signal is considered as used if it a) aliases a + // wire with a public name, an output wire or with a keep attribute b) + // combinationally drives such a wire or c) drive an input to an unknown + // cell. + // + // This recurses into driven cells for a small number of known handled + // celltypes. Results are cached and initconst is used to detect unused + // inputs for the handled celltypes. + bool is_initval_used(SigBit bit) + { + if (!bit.is_wire()) + return false; + + auto it = used_bits.find(bit); + if (it != used_bits.end()) + return it->second; + + used_bits[bit] = true; // Temporarily set to guard against logic loops + + pool portbits; + modwalker.get_consumers(portbits, {bit}); + + for (auto portbit : portbits) { + RTLIL::Cell *cell = portbit.cell; + if (!cell->type.in(ID($mux), ID($and), ID($or), ID($mem_v2)) && !RTLIL::builtin_ff_cell_types().count(cell->type)) { + return true; + } + } + + for (auto portbit : portbits) + { + RTLIL::Cell *cell = portbit.cell; + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&initvals, cell); + if (ff.has_aload || ff.has_sr || ff.has_arst || ff.has_gclk || !ff.has_clk) + return true; + if (ff.has_ce && initconst(ff.sig_ce.as_bit()) == (ff.pol_ce ? State::S0 : State::S1)) + continue; + if (ff.has_srst && initconst(ff.sig_ce.as_bit()) == (ff.pol_srst ? State::S1 : State::S0)) + continue; + + return true; + } + else if (cell->type == ID($mux)) + { + State init_s = initconst(cell->getPort(ID::S).as_bit()); + if (init_s == State::S0 && portbit.port == ID::B) + continue; + if (init_s == State::S1 && portbit.port == ID::A) + continue; + auto sig_y = cell->getPort(ID::Y); + + if (is_initval_used(sig_y[portbit.offset])) + return true; + } + else if (cell->type.in(ID($and), ID($or))) + { + auto sig_a = cell->getPort(ID::A); + auto sig_b = cell->getPort(ID::B); + auto sig_y = cell->getPort(ID::Y); + if (GetSize(sig_y) != GetSize(sig_a) || GetSize(sig_y) != GetSize(sig_b)) + return true; // TODO handle more of this + State absorbing = cell->type == ID($and) ? State::S0 : State::S1; + if (portbit.port == ID::A && initconst(sig_b[portbit.offset]) == absorbing) + continue; + if (portbit.port == ID::B && initconst(sig_a[portbit.offset]) == absorbing) + continue; + + if (is_initval_used(sig_y[portbit.offset])) + return true; + } + else if (cell->type == ID($mem_v2)) + { + // TODO Use mem.h instead to uniformily cover all cases, most + // likely requires processing all memories when initializing + // the worker + if (!portbit.port.in(ID::WR_DATA, ID::WR_ADDR, ID::RD_ADDR)) + return true; + + if (portbit.port == ID::WR_DATA) + { + if (initconst(cell->getPort(ID::WR_EN)[portbit.offset]) == State::S0) + continue; + } + else if (portbit.port == ID::WR_ADDR) + { + int port = portbit.offset / cell->getParam(ID::ABITS).as_int(); + auto sig_en = cell->getPort(ID::WR_EN); + int width = cell->getParam(ID::WIDTH).as_int(); + + for (int i = port * width; i < (port + 1) * width; i++) + if (initconst(sig_en[i]) != State::S0) + return true; + + continue; + } + else if (portbit.port == ID::RD_ADDR) + { + int port = portbit.offset / cell->getParam(ID::ABITS).as_int(); + auto sig_en = cell->getPort(ID::RD_EN); + + if (initconst(sig_en[port]) != State::S0) + return true; + + continue; + } + else + return true; + } + else + log_assert(false); + } + + used_bits[bit] = false; + return false; + } +}; + struct FormalFfPass : public Pass { FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } void help() override @@ -64,6 +356,12 @@ struct FormalFfPass : public Pass { log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n"); log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n"); log("\n"); + log(" -setundef\n"); + log(" Find FFs with undefined initialization values for which changing the\n"); + log(" initialization does not change the observable behavior and initialize\n"); + log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n"); + log(" cells that drive wires with private names.\n"); + log("\n"); // TODO: An option to check whether all FFs use the same clock before changing it to the global clock } @@ -73,6 +371,7 @@ struct FormalFfPass : public Pass { bool flag_ff2anyinit = false; bool flag_anyinit2ff = false; bool flag_fine = false; + bool flag_setundef = false; log_header(design, "Executing FORMALFF pass.\n"); @@ -95,6 +394,10 @@ struct FormalFfPass : public Pass { flag_fine = true; continue; } + if (args[argidx] == "-setundef") { + flag_setundef = true; + continue; + } break; } extra_args(args, argidx, design); @@ -113,6 +416,38 @@ struct FormalFfPass : public Pass { for (auto module : design->selected_modules()) { + if (flag_setundef) + { + InitValWorker worker(module); + + for (auto cell : module->selected_cells()) + { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) + { + FfData ff(&worker.initvals, cell); + if (ff.has_aload || ff.has_sr || ff.has_arst || ff.val_init.is_fully_def()) + continue; + + if (ff.has_ce && // CE can make the initval stick around + worker.initconst(ff.sig_ce.as_bit()) != (ff.pol_ce ? State::S1 : State::S0) && // unless it's known active + (!ff.has_srst || ff.ce_over_srst || + worker.initconst(ff.sig_srst.as_bit()) != (ff.pol_srst ? State::S1 : State::S0))) // or a srst with priority is known active + continue; + + auto before = ff.val_init; + for (int i = 0; i < ff.width; i++) + if (ff.val_init[i] == State::Sx && !worker.is_initval_used(ff.sig_q[i])) + ff.val_init[i] = State::S0; + + if (ff.val_init != before) { + log("Setting unused undefined initial value of %s.%s (%s) from %s to %s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_const(before), log_const(ff.val_init)); + worker.initvals.set_init(ff.sig_q, ff.val_init); + } + } + } + } SigMap sigmap(module); FfInitVals initvals(&sigmap, module); -- cgit v1.2.3 From 428ad5b9fd1861d7943c29e7927969a02b14926b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 20 Jul 2022 11:31:06 +0200 Subject: wreduce: Keep more x-bits with -keepdc --- passes/opt/wreduce.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc index 08ab6de6f..8fd4c788c 100644 --- a/passes/opt/wreduce.cc +++ b/passes/opt/wreduce.cc @@ -166,8 +166,8 @@ struct WreduceWorker for (int i = GetSize(sig_q)-1; i >= 0; i--) { - if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || initval[i] == State::Sx) && - (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || rst_value[i] == State::Sx)) { + if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || (!config->keepdc && initval[i] == State::Sx)) && + (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || (!config->keepdc && rst_value[i] == State::Sx))) { module->connect(sig_q[i], State::S0); initvals.remove_init(sig_q[i]); sig_d.remove(i); @@ -175,8 +175,8 @@ struct WreduceWorker continue; } - if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && - (!has_reset || i >= GetSize(rst_value) || rst_value[i] == rst_value[i-1])) { + if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && (!config->keepdc || initval[i] != State::Sx) && + (!has_reset || i >= GetSize(rst_value) || (rst_value[i] == rst_value[i-1] && (!config->keepdc || rst_value[i] != State::Sx)))) { module->connect(sig_q[i], sig_q[i-1]); initvals.remove_init(sig_q[i]); sig_d.remove(i); -- cgit v1.2.3 From 0cdb14df41be53f770390d6ad01cf650f1bc49da Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:36:29 +0200 Subject: setundef: Do not add anyseq / anyconst to unused memory port clocks Instead set those unused clocks to zero. --- passes/cmds/setundef.cc | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index a078b0b1c..590a7eb1d 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -20,6 +20,7 @@ #include "kernel/register.h" #include "kernel/celltypes.h" #include "kernel/sigtools.h" +#include "kernel/mem.h" #include "kernel/rtlil.h" #include "kernel/log.h" @@ -478,6 +479,29 @@ struct SetundefPass : public Pass { log_assert(ffbits.empty()); } + if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) + { + // Do not add anyseq / anyconst to unused memory port clocks + std::vector memories = Mem::get_selected_memories(module); + for (auto &mem : memories) { + bool changed = false; + for (auto &rd_port : mem.rd_ports) { + if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) { + changed = true; + rd_port.clk = State::S0; + } + } + for (auto &wr_port : mem.rd_ports) { + if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) { + changed = true; + wr_port.clk = State::S0; + } + } + if (changed) + mem.emit(); + } + } + module->rewrite_sigspecs(worker); if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) -- cgit v1.2.3 From a2f9ebe43a287233917947851e0d0dff803a4675 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:07:28 +0200 Subject: memory_map: Add -formal option This maps memories for a global clock based formal verification flow. This implies -keepdc, uses $ff cells for ROMs and sets hdlname attributes. --- CHANGELOG | 1 + passes/memory/memory_map.cc | 84 ++++++++++++++++++++++++++++++++++++--------- 2 files changed, 68 insertions(+), 17 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 199d6a61a..5ee3e3cc0 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ Yosys 0.20 .. Yosys 0.20-dev -------------------------- * New commands and options - Added "formalff" pass - transforms FFs for formal verification + - Added option "-formal" to "memory_map" pass * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc index fd5b1f1ad..e2f74c2e1 100644 --- a/passes/memory/memory_map.cc +++ b/passes/memory/memory_map.cc @@ -32,6 +32,7 @@ struct MemoryMapWorker bool attr_icase = false; bool rom_only = false; bool keepdc = false; + bool formal = false; dict> attributes; RTLIL::Design *design; @@ -151,6 +152,8 @@ struct MemoryMapWorker // all write ports must share the same clock RTLIL::SigSpec refclock; bool refclock_pol = false; + bool async_wr = false; + bool static_only = true; for (int i = 0; i < GetSize(mem.wr_ports); i++) { auto &port = mem.wr_ports[i]; if (port.en.is_fully_const() && !port.en.as_bool()) { @@ -164,10 +167,20 @@ struct MemoryMapWorker static_ports.insert(i); continue; } - log("Not mapping memory %s in module %s (write port %d has no clock).\n", - mem.memid.c_str(), module->name.c_str(), i); - return; + static_only = false; + if (GetSize(refclock) != 0) + log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n", + mem.memid.c_str(), module->name.c_str()); + if (!formal) + log("Not mapping memory %s in module %s (write port %d has no clock).\n", + mem.memid.c_str(), module->name.c_str(), i); + async_wr = true; + continue; } + static_only = false; + if (async_wr) + log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n", + mem.memid.c_str(), module->name.c_str()); if (refclock.size() == 0) { refclock = port.clk; refclock_pol = port.clk_polarity; @@ -185,6 +198,8 @@ struct MemoryMapWorker std::vector data_reg_in(1 << abits); std::vector data_reg_out(1 << abits); + std::vector &data_read = async_wr ? data_reg_in : data_reg_out; + int count_static = 0; for (int i = 0; i < mem.size; i++) @@ -194,24 +209,36 @@ struct MemoryMapWorker SigSpec w_init = init_data.extract(i*mem.width, mem.width); if (static_cells_map.count(addr) > 0) { - data_reg_out[idx] = static_cells_map[addr]; + data_read[idx] = static_cells_map[addr]; count_static++; } - else if (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def())) + else if (static_only && (!keepdc || w_init.is_fully_def())) { - data_reg_out[idx] = w_init; + data_read[idx] = w_init; } else { - RTLIL::Cell *c = module->addCell(genid(mem.memid, "", addr), ID($dff)); - c->parameters[ID::WIDTH] = mem.width; - if (GetSize(refclock) != 0) { + RTLIL::Cell *c; + auto ff_id = genid(mem.memid, "", addr); + + if (static_only) { + // non-static part is a ROM, we only reach this with keepdc + if (formal) { + c = module->addCell(ff_id, ID($ff)); + } else { + c = module->addCell(ff_id, ID($dff)); + c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1); + c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0)); + } + } else if (async_wr) { + log_assert(formal); // General async write not implemented yet, checked against above + c = module->addCell(ff_id, ID($ff)); + } else { + c = module->addCell(ff_id, ID($dff)); c->parameters[ID::CLK_POLARITY] = RTLIL::Const(refclock_pol); c->setPort(ID::CLK, refclock); - } else { - c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1); - c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0)); } + c->parameters[ID::WIDTH] = mem.width; RTLIL::Wire *w_in = module->addWire(genid(mem.memid, "", addr, "$d"), mem.width); data_reg_in[idx] = w_in; @@ -223,18 +250,27 @@ struct MemoryMapWorker RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width); + if (formal && mem.packed && mem.cell->name.c_str()[0] == '\\') { + auto hdlname = mem.cell->get_hdlname_attribute(); + if (hdlname.empty()) + hdlname.push_back(mem.cell->name.c_str() + 1); + hdlname.push_back(stringf("[%d]", addr)); + w_out->set_hdlname_attribute(hdlname); + } + if (!w_init.is_fully_undef()) w_out->attributes[ID::init] = w_init.as_const(); data_reg_out[idx] = w_out; c->setPort(ID::Q, w_out); - if (mem.wr_ports.empty()) + if (static_only) module->connect(RTLIL::SigSig(w_in, w_out)); } } - log(" created %d $dff cells and %d static cells of width %d.\n", mem.size-count_static, count_static, mem.width); + log(" created %d %s cells and %d static cells of width %d.\n", + mem.size-count_static, formal && (static_only || async_wr) ? "$ff" : "$dff", count_static, mem.width); int count_dff = 0, count_mux = 0, count_wrmux = 0; @@ -272,13 +308,13 @@ struct MemoryMapWorker } for (int j = 0; j < (1 << abits); j++) - if (data_reg_out[j] != SigSpec()) - module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_reg_out[j])); + if (data_read[j] != SigSpec()) + module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_read[j])); } log(" read interface: %d $dff and %d $mux cells.\n", count_dff, count_mux); - if (!mem.wr_ports.empty()) + if (!static_only) { for (int i = 0; i < mem.size; i++) { @@ -387,12 +423,19 @@ struct MemoryMapPass : public Pass { log(" -keepdc\n"); log(" when mapping ROMs, keep x-bits shared across read ports.\n"); log("\n"); + log(" -formal\n"); + log(" map memories for a global clock based formal verification flow.\n"); + log(" This implies -keepdc, uses $ff cells for ROMs and sets hdlname\n"); + log(" attributes. It also has limited support for async write ports\n"); + log(" as generated by clk2fflogic.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { bool attr_icase = false; bool rom_only = false; bool keepdc = false; + bool formal = false; dict> attributes; log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n"); @@ -439,6 +482,12 @@ struct MemoryMapPass : public Pass { keepdc = true; continue; } + if (args[argidx] == "-formal") + { + formal = true; + keepdc = true; + continue; + } break; } extra_args(args, argidx, design); @@ -449,6 +498,7 @@ struct MemoryMapPass : public Pass { worker.attributes = attributes; worker.rom_only = rom_only; worker.keepdc = keepdc; + worker.formal = formal; worker.run(); } } -- cgit v1.2.3 From 021c3c8da52ebaf6088ea740fdc12b496bfc338a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:53:47 +0200 Subject: smt2: Support $anyinit cells --- backends/smt2/smt2.cc | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 126ee1175..e6729aade 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -594,25 +594,26 @@ struct Smt2Worker return; } - if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq))) + if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { + auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y; registers.insert(cell); string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell); if (cell->attributes.count(ID::reg)) infostr += " " + cell->attributes.at(ID::reg).decode_string(); - decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str())); - if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){ + decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(QY)), infostr.c_str())); + if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::maximize)){ decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter)); - log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); + log("Wire %s is maximized\n", cell->getPort(QY).as_wire()->name.str().c_str()); } - else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){ + else if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::minimize)){ decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); - log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str()); + log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str()); } - makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y))); + makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY))); if (cell->type == ID($anyseq)) ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); - register_bv(cell->getPort(ID::Y), idcounter++); + register_bv(cell->getPort(QY), idcounter++); recursive_cells.erase(cell); return; } @@ -931,7 +932,7 @@ struct Smt2Worker pool reg_bits; for (auto cell : module->cells()) - if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { + if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_), ID($anyinit))) { // not using sigmap -- we want the net directly at the dff output for (auto bit : cell->getPort(ID::Q)) reg_bits.insert(bit); @@ -1147,7 +1148,7 @@ struct Smt2Worker ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str())); } - if (cell->type.in(ID($ff), ID($dff))) + if (cell->type.in(ID($ff), ID($dff), ID($anyinit))) { std::string expr_d = get_bv(cell->getPort(ID::D)); std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state"); -- cgit v1.2.3 From 5893cae6472727a71573cb0826158125a6aa04af Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:55:54 +0200 Subject: aiger: Support $anyinit cells --- backends/aiger/aiger.cc | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 547d131ee..800743b22 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -189,6 +189,17 @@ struct AigerWriter continue; } + if (cell->type == ID($anyinit)) + { + auto sig_d = sigmap(cell->getPort(ID::D)); + auto sig_q = sigmap(cell->getPort(ID::Q)); + for (int i = 0; i < sig_d.size(); i++) { + undriven_bits.erase(sig_q[i]); + ff_map[sig_q[i]] = sig_d[i]; + } + continue; + } + if (cell->type == ID($_AND_)) { SigBit A = sigmap(cell->getPort(ID::A).as_bit()); -- cgit v1.2.3 From 96a1173598ec1bf93670b2de3c8bb087f03a8528 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:59:39 +0200 Subject: btor: Support $anyinit cells --- backends/btor/btor.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 6dae7156a..06de71018 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -612,7 +612,7 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) + if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) { SigSpec sig_d = sigmap(cell->getPort(ID::D)); SigSpec sig_q = sigmap(cell->getPort(ID::Q)); -- cgit v1.2.3 From f041e36c6e142878c5bca4da5b459177c4f75e07 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:49:36 +0200 Subject: smtbmc: Add native json based witness format + smt2 backend support This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication. --- .gitignore | 3 + CHANGELOG | 4 + backends/smt2/Makefile.inc | 16 +- backends/smt2/smt2.cc | 120 ++++++++- backends/smt2/smtbmc.py | 400 +++++++++++++++++++++-------- backends/smt2/smtio.py | 63 ++++- backends/smt2/witness.py | 90 +++++++ backends/smt2/ywio.py | 392 ++++++++++++++++++++++++++++ tests/various/smtlib2_module-expected.smt2 | 8 + 9 files changed, 983 insertions(+), 113 deletions(-) create mode 100644 backends/smt2/witness.py create mode 100644 backends/smt2/ywio.py diff --git a/.gitignore b/.gitignore index 0460c7c13..49b886e7e 100644 --- a/.gitignore +++ b/.gitignore @@ -28,6 +28,9 @@ __pycache__ /yosys-smtbmc /yosys-smtbmc.exe /yosys-smtbmc-script.py +/yosys-witness +/yosys-witness.exe +/yosys-witness-script.py /yosys-filterlib /yosys-filterlib.exe /kernel/*.pyh diff --git a/CHANGELOG b/CHANGELOG index 5ee3e3cc0..cf2a46bd3 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -11,6 +11,10 @@ Yosys 0.20 .. Yosys 0.20-dev * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained initialization value. These can be generated by the new formalff pass. + - New JSON based yosys witness format for formal verification traces. + - yosys-smtbmc: Reading and writing of yosys witness traces. + - write_smt2: Emit inline metadata to support yosys witness trace. + - yosys-witness is a new tool to inspect and convert yosys witness traces. Yosys 0.19 .. Yosys 0.20 -------------------------- diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc index fb01308bd..3afe990e7 100644 --- a/backends/smt2/Makefile.inc +++ b/backends/smt2/Makefile.inc @@ -7,6 +7,7 @@ ifneq ($(CONFIG),emcc) # MSYS targets support yosys-smtbmc, but require a launcher script ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64)) TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc.exe $(PROGRAM_PREFIX)yosys-smtbmc-script.py +TARGETS += $(PROGRAM_PREFIX)yosys-witness.exe $(PROGRAM_PREFIX)yosys-witness-script.py # Needed to find the Python interpreter for yosys-smtbmc scripts. # Override if necessary, it is only used for msys2 targets. PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3) @@ -15,18 +16,31 @@ $(PROGRAM_PREFIX)yosys-smtbmc-script.py: backends/smt2/smtbmc.py $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \ -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@ +$(PROGRAM_PREFIX)yosys-witness-script.py: backends/smt2/witness.py + $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \ + -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@ + $(PROGRAM_PREFIX)yosys-smtbmc.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-smtbmc-script.py $(P) $(CXX) -DGUI=0 -O -s -o $@ $< + +$(PROGRAM_PREFIX)yosys-witness.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-witness-script.py + $(P) $(CXX) -DGUI=0 -O -s -o $@ $< # Other targets else -TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc +TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc $(PROGRAM_PREFIX)yosys-witness $(PROGRAM_PREFIX)yosys-smtbmc: backends/smt2/smtbmc.py $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new $(Q) chmod +x $@.new $(Q) mv $@.new $@ + +$(PROGRAM_PREFIX)yosys-witness: backends/smt2/witness.py + $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new + $(Q) chmod +x $@.new + $(Q) mv $@.new $@ endif $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py)) +$(eval $(call add_share_file,share/python3,backends/smt2/ywio.py)) endif endif diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e6729aade..54783cf1b 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -23,6 +23,7 @@ #include "kernel/celltypes.h" #include "kernel/log.h" #include "kernel/mem.h" +#include "libs/json11/json11.hpp" #include USING_YOSYS_NAMESPACE @@ -588,6 +589,9 @@ struct Smt2Worker if (cell->type.in(ID($ff), ID($dff))) { registers.insert(cell); + for (auto chunk : cell->getPort(ID::Q).chunks()) + if (chunk.is_wire()) + decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire)); makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); register_bv(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -610,6 +614,12 @@ struct Smt2Worker decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str()); } + + bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst)); + for (auto chunk : cell->getPort(QY).chunks()) + if (chunk.is_wire()) + decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire)); + makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY))); if (cell->type == ID($anyseq)) ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); @@ -760,6 +770,7 @@ struct Smt2Worker log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync")); + decls.push_back(witness_memory(get_id(mem->memid), cell, mem)); string memstate; if (has_async_wr) { @@ -852,6 +863,7 @@ struct Smt2Worker if (m != nullptr) { decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name))); + decls.push_back(witness_cell(get_id(cell->name), cell)); string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name)); for (auto &conn : cell->connections()) @@ -950,14 +962,19 @@ struct Smt2Worker for (auto wire : module->wires()) { bool is_register = false; - for (auto bit : SigSpec(wire)) + bool contains_clock = false; + for (auto bit : SigSpec(wire)) { if (reg_bits.count(bit)) is_register = true; + auto sig_bit = sigmap(bit); + if (clock_posedge.count(sig_bit) || clock_negedge.count(sig_bit)) + contains_clock = true; + } bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr); if (is_smtlib2_comb_expr && !is_smtlib2_module) log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module), log_id(wire)); - if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) { + if (wire->port_id || is_register || contains_clock || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) { RTLIL::SigSpec sig = sigmap(wire); std::vector comments; if (wire->port_input) @@ -968,9 +985,20 @@ struct Smt2Worker comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); - if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) + if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); + if (contains_clock) { + for (int i = 0; i < GetSize(sig); i++) { + bool is_posedge = clock_posedge.count(sig[i]); + bool is_negedge = clock_negedge.count(sig[i]); + if (is_posedge != is_negedge) + comments.push_back(witness_signal( + is_posedge ? "posedge" : "negedge", 1, i, get_id(wire), -1, wire)); + } + } + if (wire->port_input) + comments.push_back(witness_signal("input", wire->width, 0, get_id(wire), -1, wire)); std::string smtlib2_comb_expr; if (is_smtlib2_comb_expr) { smtlib2_comb_expr = @@ -980,6 +1008,8 @@ struct Smt2Worker if (!bvmode && GetSize(sig) > 1) log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s", log_id(module), log_id(wire)); + + comments.push_back(witness_signal("blackbox", wire->width, 0, get_id(wire), -1, wire)); } auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls; if (bvmode && GetSize(sig) > 1) { @@ -1447,6 +1477,90 @@ struct Smt2Worker f << "true)"; f << stringf(" ; end of module %s\n", get_id(module)); } + + template static std::vector witness_path(T *obj) { + std::vector path; + if (obj->name.isPublic()) { + auto hdlname = obj->get_string_attribute(ID::hdlname); + for (auto token : split_tokens(hdlname)) + path.push_back("\\" + token); + } + if (path.empty()) + path.push_back(obj->name.str()); + return path; + } + + std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire) + { + std::vector hiername; + const char *wire_name = wire->name.c_str(); + if (wire_name[0] == '\\') { + auto hdlname = wire->get_string_attribute(ID::hdlname); + for (auto token : split_tokens(hdlname)) + hiername.push_back("\\" + token); + } + if (hiername.empty()) + hiername.push_back(wire->name.str()); + + std::string line = "; yosys-smt2-witness "; + (json11::Json { json11::Json::object { + { "type", type }, + { "offset", offset }, + { "width", width }, + { "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) }, + { "path", witness_path(wire) }, + }}).dump(line); + line += "\n"; + return line; + } + + std::string witness_cell(const char *smtname, RTLIL::Cell *cell) + { + std::string line = "; yosys-smt2-witness "; + (json11::Json {json11::Json::object { + { "type", "cell" }, + { "smtname", smtname }, + { "path", witness_path(cell) }, + }}).dump(line); + line += "\n"; + return line; + } + + std::string witness_memory(const char *smtname, RTLIL::Cell *cell, Mem *mem) + { + json11::Json::array uninitialized; + auto init_data = mem->get_init_data(); + + int cursor = 0; + + while (cursor < init_data.size()) { + while (cursor < init_data.size() && init_data[cursor] != State::Sx) + cursor++; + int offset = cursor; + while (cursor < init_data.size() && init_data[cursor] == State::Sx) + cursor++; + int width = cursor - offset; + if (width) + uninitialized.push_back(json11::Json::object { + {"width", width}, + {"offset", offset}, + }); + } + + std::string line = "; yosys-smt2-witness "; + (json11::Json { json11::Json::object { + { "type", "mem" }, + { "width", mem->width }, + { "size", mem->size }, + { "rom", mem->wr_ports.empty() }, + { "statebv", statebv }, + { "smtname", smtname }, + { "uninitialized", uninitialized }, + { "path", witness_path(cell) }, + }}).dump(line); + line += "\n"; + return line; + } }; struct Smt2Backend : public Backend { diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 137182f33..b8ea22aaf 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -17,9 +17,10 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import os, sys, getopt, re +import os, sys, getopt, re, bisect ##yosys-sys-path## from smtio import SmtIo, SmtOpts, MkVcd +from ywio import ReadWitness, WriteWitness, WitnessValues from collections import defaultdict got_topt = False @@ -28,6 +29,8 @@ step_size = 1 num_steps = 20 append_steps = 0 vcdfile = None +inywfile = None +outywfile = None cexfile = None aimfile = None aiwfile = None @@ -94,6 +97,9 @@ def usage(): the AIGER witness file does not include the status and properties lines. + --yw + read a Yosys witness. + --btorwit read a BTOR witness. @@ -121,6 +127,9 @@ def usage(): (hint: use 'write_smt2 -wires' for maximum coverage of signals in generated VCD file) + --dump-yw + write trace as a Yosys witness trace + --dump-vlogtb write trace as Verilog test bench @@ -167,8 +176,8 @@ def usage(): try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat", - "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", + "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"]) except: usage() @@ -204,10 +213,14 @@ for o, a in opts: aiwfile = a + ".aiw" elif o == "--aig-noheader": aigheader = False + elif o == "--yw": + inywfile = a elif o == "--btorwit": btorwitfile = a elif o == "--dump-vcd": vcdfile = a + elif o == "--dump-yw": + outywfile = a elif o == "--dump-vlogtb": vlogtbfile = a elif o == "--vlogtb-top": @@ -602,6 +615,101 @@ if aimfile is not None: num_steps = max(num_steps, step+2) step += 1 +if inywfile is not None: + with open(inywfile, "r") as f: + inyw = ReadWitness(f) + + inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True) + + smt_wires = defaultdict(list) + smt_mems = defaultdict(list) + + for wire in inits + seqs: + smt_wires[wire["path"]].append(wire) + + for mem in mems: + smt_mems[mem["path"]].append(mem) + + addr_re = re.compile(r'\\\[[0-9]+\]$') + bits_re = re.compile(r'[01?]*$') + + for t, step in inyw.steps(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") + + 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"] + + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + + offset = max(offset, 0) + + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue + + smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"]) + + 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) + + bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] + + if bit_slice.count("?") == len(bit_slice): + continue + + 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) + + smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + + constr_assumes[t].append((inywfile, smt_constr)) + + 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{t}", 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 len(bits) < width: + slice_high = sig.offset + len(bits) - 1 + smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + + bit_slice = bits + + 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) + + smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + constr_assumes[t].append((inywfile, smt_constr)) + if btorwitfile is not None: with open(btorwitfile, "r") as f: step = None @@ -699,128 +807,137 @@ if btorwitfile is not None: skip_steps = step num_steps = step+1 -def write_vcd_trace(steps_start, steps_stop, index): - filename = vcdfile.replace("%", index) - print_msg("Writing trace to VCD file: %s" % (filename)) +def collect_mem_trace_data(steps_start, steps_stop, vcd=None): + mem_trace_data = dict() - with open(filename, "w") as vcd_file: - vcd = MkVcd(vcd_file) - path_list = list() + for mempath in sorted(smt.hiermems(topmod)): + abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath) - for netpath in sorted(smt.hiernets(topmod)): - hidden_net = False - for n in netpath: - if n.startswith("$"): - hidden_net = True - if not hidden_net: - edge = smt.net_clock(topmod, netpath) - if edge is None: - vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath)) - else: - vcd.add_clock([topmod] + netpath, edge) - path_list.append(netpath) - - mem_trace_data = dict() - for mempath in sorted(smt.hiermems(topmod)): - abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath) + expr_id = list() + expr_list = list() + for i in range(steps_start, steps_stop): + for j in range(rports): + expr_id.append(('R', i-steps_start, j, 'A')) + expr_id.append(('R', i-steps_start, j, 'D')) + expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j)) + expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j)) + for j in range(wports): + expr_id.append(('W', i-steps_start, j, 'A')) + expr_id.append(('W', i-steps_start, j, 'D')) + expr_id.append(('W', i-steps_start, j, 'M')) + expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j)) + expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j)) + expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j)) + + rdata = list() + wdata = list() + addrs = set() + + for eid, edat in zip(expr_id, smt.get_list(expr_list)): + t, i, j, f = eid + + if t == 'R': + c = rdata + elif t == 'W': + c = wdata + else: + assert False - expr_id = list() - expr_list = list() - for i in range(steps_start, steps_stop): - for j in range(rports): - expr_id.append(('R', i-steps_start, j, 'A')) - expr_id.append(('R', i-steps_start, j, 'D')) - expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j)) - expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j)) - for j in range(wports): - expr_id.append(('W', i-steps_start, j, 'A')) - expr_id.append(('W', i-steps_start, j, 'D')) - expr_id.append(('W', i-steps_start, j, 'M')) - expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j)) - expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j)) - expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j)) - - rdata = list() - wdata = list() - addrs = set() - - for eid, edat in zip(expr_id, smt.get_list(expr_list)): - t, i, j, f = eid - - if t == 'R': - c = rdata - elif t == 'W': - c = wdata - else: - assert False + while len(c) <= i: + c.append(list()) + c = c[i] - while len(c) <= i: - c.append(list()) - c = c[i] + while len(c) <= j: + c.append(dict()) + c = c[j] - while len(c) <= j: - c.append(dict()) - c = c[j] + c[f] = smt.bv2bin(edat) - c[f] = smt.bv2bin(edat) + if f == 'A': + addrs.add(c[f]) - if f == 'A': - addrs.add(c[f]) + for addr in addrs: + tdata = list() + data = ["x"] * width + gotread = False - for addr in addrs: - tdata = list() - data = ["x"] * width - gotread = False + if len(wdata) == 0 and len(rdata) != 0: + wdata = [[]] * len(rdata) - if len(wdata) == 0 and len(rdata) != 0: - wdata = [[]] * len(rdata) + assert len(rdata) == len(wdata) - assert len(rdata) == len(wdata) + for i in range(len(wdata)): + if not gotread: + for j_data in rdata[i]: + if j_data["A"] == addr: + data = list(j_data["D"]) + gotread = True + break - for i in range(len(wdata)): - if not gotread: - for j_data in rdata[i]: - if j_data["A"] == addr: - data = list(j_data["D"]) - gotread = True - break + if gotread: + buf = data[:] + for ii in reversed(range(len(tdata))): + for k in range(width): + if tdata[ii][k] == "x": + tdata[ii][k] = buf[k] + else: + buf[k] = tdata[ii][k] - if gotread: - buf = data[:] - for ii in reversed(range(len(tdata))): - for k in range(width): - if tdata[ii][k] == "x": - tdata[ii][k] = buf[k] - else: - buf[k] = tdata[ii][k] + if not asyncwr: + tdata.append(data[:]) - if not asyncwr: - tdata.append(data[:]) + for j_data in wdata[i]: + if j_data["A"] != addr: + continue - for j_data in wdata[i]: - if j_data["A"] != addr: - continue + D = j_data["D"] + M = j_data["M"] - D = j_data["D"] - M = j_data["M"] + for k in range(width): + if M[k] == "1": + data[k] = D[k] - for k in range(width): - if M[k] == "1": - data[k] = D[k] + if asyncwr: + tdata.append(data[:]) - if asyncwr: - tdata.append(data[:]) + assert len(tdata) == len(rdata) - assert len(tdata) == len(rdata) + int_addr = int(addr, 2) - netpath = mempath[:] - netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2)) + netpath = mempath[:] + if vcd: + netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int_addr) vcd.add_net([topmod] + netpath, width) - for i in range(steps_start, steps_stop): - if i not in mem_trace_data: - mem_trace_data[i] = list() - mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start]))) + for i in range(steps_start, steps_stop): + if i not in mem_trace_data: + mem_trace_data[i] = list() + mem_trace_data[i].append((netpath, int_addr, "".join(tdata[i-steps_start]))) + + return mem_trace_data + +def write_vcd_trace(steps_start, steps_stop, index): + filename = vcdfile.replace("%", index) + print_msg("Writing trace to VCD file: %s" % (filename)) + + with open(filename, "w") as vcd_file: + vcd = MkVcd(vcd_file) + path_list = list() + + for netpath in sorted(smt.hiernets(topmod)): + hidden_net = False + for n in netpath: + if n.startswith("$"): + hidden_net = True + if not hidden_net: + edge = smt.net_clock(topmod, netpath) + if edge is None: + vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath)) + else: + vcd.add_clock([topmod] + netpath, edge) + path_list.append(netpath) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop, vcd) for i in range(steps_start, steps_stop): vcd.set_time(i) @@ -828,7 +945,7 @@ def write_vcd_trace(steps_start, steps_stop, index): for path, value in zip(path_list, value_list): vcd.set_net([topmod] + path, value) if i in mem_trace_data: - for path, value in mem_trace_data[i]: + for path, addr, value in mem_trace_data[i]: vcd.set_net([topmod] + path, value) vcd.set_time(steps_stop) @@ -1072,8 +1189,72 @@ def write_constr_trace(steps_start, steps_stop, index): for name, val in zip(pi_names, pi_values): print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f) +def write_yw_trace(steps_start, steps_stop, index, allregs=False): + filename = outywfile.replace("%", index) + print_msg("Writing trace to Yosys witness file: %s" % (filename)) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + + with open(filename, "w") as f: + inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs) + + yw = WriteWitness(f, "smtbmc") + + for clock in clocks: + yw.add_clock(clock["path"], clock["offset"], clock["type"]) + + for seq in seqs: + seq["sig"] = yw.add_sig(seq["path"], seq["offset"], seq["width"]) + + for init in inits: + init["sig"] = yw.add_sig(init["path"], init["offset"], init["width"], True) + + inits = seqs + inits + + mem_dict = {tuple(mem["smtpath"]): mem for mem in mems} + mem_init_values = [] + + for path, addr, value in mem_trace_data.get(0, ()): + json_mem = mem_dict.get(tuple(path)) + if not json_mem: + continue + + bit_addr = addr * json_mem["width"] + uninit_chunks = [(chunk["width"] + chunk["offset"], chunk["offset"]) for chunk in json_mem["uninitialized"]] + first_chunk_nr = bisect.bisect_left(uninit_chunks, (bit_addr + 1,)) -def write_trace(steps_start, steps_stop, index): + for uninit_end, uninit_offset in uninit_chunks[first_chunk_nr:]: + assert uninit_end > bit_addr + if uninit_offset > bit_addr + json_mem["width"]: + break + + word_path = (*json_mem["path"], f"\\[{addr}]") + + overlap_start = max(uninit_offset - bit_addr, 0) + overlap_end = min(uninit_end - bit_addr, json_mem["width"]) + overlap_bits = value[len(value)-overlap_end:len(value)-overlap_start] + + sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True) + mem_init_values.append((sig, overlap_bits.replace("x", "?"))) + + for k in range(steps_start, steps_stop): + step_values = WitnessValues() + + if k == steps_start: + for sig, value in mem_init_values: + step_values[sig] = value + sigs = inits + seqs + else: + sigs = seqs + + for sig in sigs: + step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"]))) + yw.step(step_values) + + yw.end_trace() + + +def write_trace(steps_start, steps_stop, index, allregs=False): if vcdfile is not None: write_vcd_trace(steps_start, steps_stop, index) @@ -1083,6 +1264,9 @@ def write_trace(steps_start, steps_stop, index): if outconstr is not None: write_constr_trace(steps_start, steps_stop, index) + if outywfile is not None: + write_yw_trace(steps_start, steps_stop, index, allregs) + def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()): assert mod in smt.modinfo @@ -1392,12 +1576,12 @@ if tempind: print_msg("Temporal induction failed!") print_anyconsts(num_steps) print_failed_asserts(num_steps) - write_trace(step, num_steps+1, '%') + write_trace(step, num_steps+1, '%', allregs=True) elif dumpall: print_anyconsts(num_steps) print_failed_asserts(num_steps) - write_trace(step, num_steps+1, "%d" % step) + write_trace(step, num_steps+1, "%d" % step, allregs=True) else: print_msg("Temporal induction successful.") diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3ba43825c..de09c040e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, re, os, signal +import sys, re, os, signal, json import subprocess if os.name == "posix": import resource @@ -108,6 +108,7 @@ class SmtModInfo: self.allconsts = dict() self.allseqs = dict() self.asize = dict() + self.witness = [] class SmtIo: @@ -587,6 +588,11 @@ class SmtIo: self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) + if fields[1] == "yosys-smt2-witness": + data = json.loads(stmt.split(None, 2)[2]) + if data.get("type") in ["cell", "mem", "posedge", "negedge", "input", "reg", "init", "seq", "blackbox"]: + self.modinfo[self.curmod].witness.append(data) + def hiernets(self, top, regs_only=False): def hiernets_worker(nets, mod, cursor): for netname in sorted(self.modinfo[mod].wsize.keys()): @@ -658,6 +664,57 @@ class SmtIo: hiermems_worker(mems, top, []) return mems + def hierwitness(self, top, allregs=False, blackbox=True): + init_witnesses = [] + seq_witnesses = [] + clk_witnesses = [] + mem_witnesses = [] + + def absolute(path, cursor, witness): + return { + **witness, + "path": path + tuple(witness["path"]), + "smtpath": cursor + [witness["smtname"]], + } + + for witness in self.modinfo[top].witness: + if witness["type"] == "input": + seq_witnesses.append(absolute((), [], witness)) + if witness["type"] in ("posedge", "negedge"): + clk_witnesses.append(absolute((), [], witness)) + + init_types = ["init"] + if allregs: + init_types.append("reg") + + seq_types = ["seq"] + if blackbox: + seq_types.append("blackbox") + + def worker(mod, path, cursor): + cell_paths = {} + for witness in self.modinfo[mod].witness: + if witness["type"] in init_types: + init_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] in seq_types: + seq_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] == "mem": + if allregs and not witness["rom"]: + width, size = witness["width"], witness["size"] + witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}} + if not witness["uninitialized"]: + continue + + mem_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] == "cell": + cell_paths[witness["smtname"]] = tuple(witness["path"]) + + for cellname, celltype in sorted(self.modinfo[mod].cells.items()): + worker(celltype, path + cell_paths.get(cellname, ("?" + cellname,)), cursor + [cellname]) + + worker(top, (), []) + return init_witnesses, seq_witnesses, clk_witnesses, mem_witnesses + def read(self): stmt = [] count_brackets = 0 @@ -887,6 +944,8 @@ class SmtIo: assert mod in self.modinfo if path[0] == "": return base + if isinstance(path[0], int): + return "(|%s#%d| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].cells: return "(|%s_h %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].wsize: @@ -909,6 +968,8 @@ class SmtIo: mod = self.modinfo[mod].cells[net_path[i]] assert mod in self.modinfo + if isinstance(net_path[-1], int): + return None assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py new file mode 100644 index 000000000..1105d9ed0 --- /dev/null +++ b/backends/smt2/witness.py @@ -0,0 +1,90 @@ +#!/usr/bin/env python3 +# +# yosys -- Yosys Open SYnthesis Suite +# +# Copyright (C) 2022 Jannis Harder +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import os, sys +##yosys-sys-path## +import click + +from ywio import ReadWitness, WriteWitness, WitnessSig + +@click.group() +def cli(): + pass + + +@cli.command(help=""" +Display a Yosys witness trace in a human readable format. +""") +@click.argument("input", type=click.File("r")) +def display(input): + click.echo(f"Reading Yosys witness trace {input.name!r}...") + inyw = ReadWitness(input) + + def output(): + + yield click.style("*** RTLIL bit-order below may differ from source level declarations ***", fg="red") + if inyw.clocks: + yield click.style("=== Clock Signals ===", fg="blue") + for clock in inyw.clocks: + yield f" {clock['edge']} {WitnessSig(clock['path'], clock['offset']).pretty()}" + + for t, values in inyw.steps(): + if t: + yield click.style(f"=== Step {t} ===", fg="blue") + else: + yield click.style("=== Initial State ===", fg="blue") + + step_prefix = click.style(f"#{t}", fg="bright_black") + + signals, missing = values.present_signals(inyw.sigmap) + + assert not missing + + for sig in signals: + display_bits = values[sig].replace("?", click.style("?", fg="bright_black")) + yield f" {step_prefix} {sig.pretty()} = {display_bits}" + click.echo_via_pager([line + "\n" for line in output()]) + +@cli.command(help=""" +Transform a Yosys witness trace. + +Currently no transformations are implemented, so it is only useful for testing. +""") +@click.argument("input", type=click.File("r")) +@click.argument("output", type=click.File("w")) +def yw2yw(input, output): + click.echo(f"Copying yosys witness trace from {input.name!r} to {output.name!r}...") + inyw = ReadWitness(input) + outyw = WriteWitness(output, "yosys-witness yw2yw") + + for clock in inyw.clocks: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + + for sig in inyw.signals: + outyw.add_sig(sig.path, sig.offset, sig.width, sig.init_only) + + for t, values in inyw.steps(): + outyw.step(values) + + outyw.end_trace() + + click.echo(f"Copied {outyw.t + 1} time steps.") + +if __name__ == "__main__": + cli() diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py new file mode 100644 index 000000000..8469b4162 --- /dev/null +++ b/backends/smt2/ywio.py @@ -0,0 +1,392 @@ +# +# yosys -- Yosys Open SYnthesis Suite +# +# Copyright (C) 2022 Jannis Harder +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import json, re + +from functools import total_ordering + + +class PrettyJson: + def __init__(self, f): + self.f = f + self.indent = 0 + self.state = ["value"] + + def line(self): + indent = len(self.state) - bool(self.state and self.state[-1] == "value") + print("\n", end=" " * (2 * indent), file=self.f) + + def raw(self, str): + print(end=str, file=self.f) + + def begin_object(self): + self.begin_value() + self.raw("{") + self.state.append("object_first") + + def begin_array(self): + self.begin_value() + self.raw("[") + self.state.append("array_first") + + def end_object(self): + state = self.state.pop() + if state == "object": + self.line() + else: + assert state == "object_first" + self.raw("}") + self.end_value() + + def end_array(self): + state = self.state.pop() + if state == "array": + self.line() + else: + assert state == "array_first" + self.raw("]") + self.end_value() + + def name(self, name): + if self.state[-1] == "object_first": + self.state[-1] = "object" + else: + self.raw(",") + self.line() + json.dump(str(name), self.f) + self.raw(": ") + self.state.append("value") + + def begin_value(self): + if self.state[-1] == "array_first": + self.line() + self.state[-1] = "array" + elif self.state[-1] == "array": + self.raw(",") + self.line() + else: + assert self.state.pop() == "value" + + def end_value(self): + if not self.state: + print(file=self.f, flush=True) + + def value(self, value): + self.begin_value() + json.dump(value, self.f) + self.end_value() + + def entry(self, name, value): + self.name(name) + self.value(value) + + def object(self, entries=None): + if isinstance(entries, dict): + entries = dict.items() + self.begin_object() + for name, value in entries: + self.entry(name, value) + self.end_object() + + def array(self, values=None): + self.begin_array() + for value in values: + self.value(value) + self.end_array() + + +addr_re = re.compile(r'\\\[[0-9]+\]$') +public_name_re = re.compile(r"\\([a-zA-Z_][a-zA-Z0-9_]*(\[[0-9]+\])?|\[[0-9]+\])$") + +def pretty_name(id): + if public_name_re.match(id): + return id.lstrip("\\") + else: + return id + +def pretty_path(path): + out = "" + for name in path: + name = pretty_name(name) + if name.startswith("["): + out += name + continue + if out: + out += "." + if name.startswith("\\") or name.startswith("$"): + out += name + " " + else: + out += name + + return out + +@total_ordering +class WitnessSig: + def __init__(self, path, offset, width=1, init_only=False): + path = tuple(path) + self.path, self.width, self.offset, self.init_only = path, width, offset, init_only + + self.memory_path = None + self.memory_addr = None + + sort_path = path + sort_id = -1 + if path and addr_re.match(path[-1]): + self.memory_path = sort_path = path[:-1] + self.memory_addr = sort_id = int(path[-1][2:-1]) + + self.sort_key = (init_only, sort_path, sort_id, offset, width) + + def bits(self): + return ((self.path, i) for i in range(self.offset, self.offset + self.width)) + + def rev_bits(self): + return ((self.path, i) for i in reversed(range(self.offset, self.offset + self.width))) + + def pretty(self): + if self.width > 1: + last_offset = self.offset + self.width - 1 + return f"{pretty_path(self.path)}[{last_offset}:{self.offset}]" + else: + return f"{pretty_path(self.path)}[{self.offset}]" + + def __eq__(self): + return self.sort_key + + def __hash__(self): + return hash(self.sort_key) + + def __lt__(self, other): + return self.sort_key < other.sort_key + + +def coalesce_signals(signals): + bits = {} + for sig in signals: + for bit in sig.bits(): + if sig.init_only: + bits.setdefault(bit, False) + else: + bits[bit] = True + + active = None + + out = [] + + for bit, not_init in sorted(bits.items()): + if active: + if active[0] == bit[0] and active[2] == bit[1] and active[3] == not_init: + active[2] += 1 + else: + out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3])) + active = None + + if active is None: + active = [bit[0], bit[1], bit[1] + 1, not_init] + + if active: + out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3])) + + return sorted(out) + + +class WitnessSigMap: + def __init__(self, signals=[]): + self.signals = [] + + self.id_to_bit = [] + self.bit_to_id = {} + self.bit_to_sig = {} + + for sig in signals: + self.add_signal(sig) + + def add_signal(self, sig): + self.signals.append(sig) + for bit in sig.bits(): + self.add_bit(bit) + self.bit_to_sig[bit] = sig + + def add_bit(self, bit, id=None): + if id is None: + id = len(self.id_to_bit) + self.id_to_bit.append(bit) + else: + if len(self.id_to_bit) <= id: + self.id_to_bit += [None] * (id - len(self.id_to_bit) + 1) + self.id_to_bit[id] = bit + self.bit_to_id[bit] = id + + +class WitnessValues: + def __init__(self): + self.values = {} + + def __setitem__(self, key, value): + if isinstance(key, tuple) and len(key) == 2: + if value != "?": + assert isinstance(value, str) + assert len(value) == 1 + self.values[key] = value + else: + assert isinstance(key, WitnessSig) + assert key.width == len(value) + if isinstance(value, str): + value = reversed(value) + for bit, bit_value in zip(key.bits(), value): + if bit_value != "?": + self.values[bit] = bit_value + + def __getitem__(self, key): + if isinstance(key, tuple) and len(key) == 2: + return self.values.get(key, "?") + else: + assert isinstance(key, WitnessSig) + return "".join([self.values.get(bit, "?") for bit in key.rev_bits()]) + + def pack_present(self, sigmap): + missing = [] + + max_id = max((sigmap.bit_to_id.get(bit, -1) for bit in self.values), default=-1) + + vector = ["?"] * (max_id + 1) + for bit, bit_value in self.values.items(): + id = sigmap.bit_to_id.get(bit, - 1) + if id < 0: + missing.append(bit) + else: + vector[max_id - sigmap.bit_to_id[bit]] = bit_value + + return "".join(vector), missing + + def pack(self, sigmap): + packed, missing = self.pack_present(sigmap) + if missing: + raise RuntimeError(f"Cannot pack bits {missing!r}") + return packed + + def unpack(self, sigmap, bits): + for i, bit_value in enumerate(reversed(bits)): + if bit_value != "?": + self.values[sigmap.id_to_bit[i]] = bit_value + + def present_signals(self, sigmap): + signals = set(sigmap.bit_to_sig.get(bit) for bit in self.values) + missing_signals = None in signals + if missing_signals: + signals.discard(None) + + return sorted(signals), missing_signals + + +class WriteWitness: + def __init__(self, f, generator): + self.out = PrettyJson(f) + self.t = 0 + self.header_written = False + self.clocks = [] + self.signals = [] + + self.out.begin_object() + self.out.entry("format", "Yosys Witness Trace") + self.out.entry("generator", generator) + + def add_clock(self, path, offset, edge): + assert not self.header_written + self.clocks.append({ + "path": path, + "edge": edge, + "offset": offset, + }) + + def add_sig(self, path, offset, width=1, init_only=False): + assert not self.header_written + sig = WitnessSig(path, offset, width, init_only) + self.signals.append(sig) + return sig + + def write_header(self): + assert not self.header_written + self.header_written = True + self.out.name("clocks") + self.out.array(self.clocks) + + self.signals = coalesce_signals(self.signals) + self.sigmap = WitnessSigMap(self.signals) + + self.out.name("signals") + self.out.array({ + "path": sig.path, + "width": sig.width, + "offset": sig.offset, + "init_only": sig.init_only, + } for sig in self.signals) + + self.out.name("steps") + self.out.begin_array() + + def step(self, values): + if not self.header_written: + self.write_header() + + self.out.value({"bits": values.pack(self.sigmap)}) + + self.t += 1 + + def end_trace(self): + if not self.header_written: + self.write_header() + self.out.end_array() + self.out.end_object() + + +class ReadWitness: + def __init__(self, f): + data = json.load(f) + if not isinstance(data, dict): + data = {} + + data_format = data.get("format", "Unknown Format") + + if data_format != "Yosys Witness Trace": + raise ValueError(f"unsupported format {data_format!r}") + + self.clocks = data["clocks"] + for clock in self.clocks: + clock["path"] = tuple(clock["path"]) + + self.signals = [ + WitnessSig(sig["path"], sig["offset"], sig["width"], sig["init_only"]) + for sig in data["signals"] + ] + + self.sigmap = WitnessSigMap(self.signals) + + self.bits = [step["bits"] for step in data["steps"]] + + def step(self, t): + values = WitnessValues() + values.unpack(self.sigmap, self.bits[t]) + return values + + def steps(self): + for i in range(len(self.bits)): + yield i, self.step(i) + + def __len__(self): + return len(self.bits) diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 index ace858ca8..74e2f3fca 100644 --- a/tests/various/smtlib2_module-expected.smt2 +++ b/tests/various/smtlib2_module-expected.smt2 @@ -4,11 +4,14 @@ (declare-fun |smtlib2_is| (|smtlib2_s|) Bool) (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a ; yosys-smt2-input a 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8} (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b ; yosys-smt2-input b 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8} (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state)) ; yosys-smt2-output add 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8} (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -16,6 +19,7 @@ (bvadd a b) )) ; yosys-smt2-output eq 1 +; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1} (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -23,6 +27,7 @@ (= a b) )) ; yosys-smt2-output sub 8 +; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8} (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -38,13 +43,16 @@ (declare-sort |uut_s| 0) (declare-fun |uut_is| (|uut_s|) Bool) ; yosys-smt2-cell smtlib2 s +; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"} (declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add (declare-fun |uut#1| (|uut_s|) Bool) ; \eq (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|) ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26 +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8} (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41 +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8} (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9 -- cgit v1.2.3 From efd5b86eb9c56d293c608d378ee90beea53784b5 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 17:02:39 +0200 Subject: aiger: Add yosys-witness support Adds a new json based aiger map file and yosys-witness converters to us this to convert between native and AIGER witness files. --- CHANGELOG | 3 + backends/aiger/aiger.cc | 169 +++++++++++++++++++++++++++++++++++++++++++++++ backends/smt2/witness.py | 150 ++++++++++++++++++++++++++++++++++++++++- 3 files changed, 320 insertions(+), 2 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index cf2a46bd3..a9144facf 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -15,6 +15,9 @@ Yosys 0.20 .. Yosys 0.20-dev - yosys-smtbmc: Reading and writing of yosys witness traces. - write_smt2: Emit inline metadata to support yosys witness trace. - yosys-witness is a new tool to inspect and convert yosys witness traces. + - write_aiger: Option to write a map file for yosys witness trace + conversion. + - yosys-witness: Conversion from and to AIGER witness traces. Yosys 0.19 .. Yosys 0.20 -------------------------- diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 800743b22..2ea999dc0 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -19,6 +19,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -61,6 +62,8 @@ struct AigerWriter dict init_inputs; int initstate_ff = 0; + dict ywmap_clocks; + int mkgate(int a0, int a1) { aig_m++, aig_a++; @@ -159,6 +162,17 @@ struct AigerWriter output_bits.insert(wirebit); } } + + if (wire->width == 1) { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + SigBit bit = sigmap(wire); + if (gclk_attr->second == State::S1) + ywmap_clocks[bit] |= 1; + else if (gclk_attr->second == State::S0) + ywmap_clocks[bit] |= 2; + } + } } for (auto bit : input_bits) @@ -186,6 +200,11 @@ struct AigerWriter unused_bits.erase(D); undriven_bits.erase(Q); ff_map[Q] = D; + + if (cell->type != ID($_FF_)) { + auto sig_clk = sigmap(cell->getPort(ID::CLK).as_bit()); + ywmap_clocks[sig_clk] |= cell->type == ID($_DFF_N_) ? 2 : 1; + } continue; } @@ -689,6 +708,137 @@ struct AigerWriter for (auto &it : wire_lines) f << it.second; } + + template static std::vector witness_path(T *obj) { + std::vector path; + if (obj->name.isPublic()) { + auto hdlname = obj->get_string_attribute(ID::hdlname); + for (auto token : split_tokens(hdlname)) + path.push_back("\\" + token); + } + if (path.empty()) + path.push_back(obj->name.str()); + return path; + } + + void write_ywmap(std::ostream &f) + { + f << "{\n"; + f << " \"version\": \"Yosys Witness Aiger Map\",\n"; + f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str()); + f << stringf(" \"latch_count\": %d,\n", aig_l); + f << stringf(" \"input_count\": %d,\n", aig_i); + + dict clock_lines; + dict input_lines; + dict init_lines; + dict seq_lines; + + for (auto cell : module->cells()) + { + if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_), ID($anyinit), ID($anyconst), ID($anyseq))) + { + // Use sig_q to get the FF output name, but sig to lookup aiger bits + auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q); + SigSpec sig = sigmap(sig_qy); + + for (int i = 0; i < GetSize(sig_qy); i++) { + if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr) + continue; + + auto wire = sig_qy[i].wire; + + if (init_inputs.count(sig[i])) { + int a = init_inputs.at(sig[i]); + log_assert((a & 1) == 0); + init_lines[a] += json11::Json(json11::Json::object { + { "path", witness_path(wire) }, + { "input", (a >> 1) - 1 }, + { "offset", sig_qy[i].offset }, + }).dump(); + } + + if (input_bits.count(sig[i])) { + int a = aig_map.at(sig[i]); + log_assert((a & 1) == 0); + seq_lines[a] += json11::Json(json11::Json::object { + { "path", witness_path(wire) }, + { "input", (a >> 1) - 1 }, + { "offset", sig_qy[i].offset }, + }).dump(); + } + } + } + } + + for (auto wire : module->wires()) + { + SigSpec sig = sigmap(wire); + if (wire->port_input) + { + auto path = witness_path(wire); + for (int i = 0; i < GetSize(wire); i++) { + if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr) + continue; + + int a = aig_map.at(sig[i]); + log_assert((a & 1) == 0); + input_lines[a] += json11::Json(json11::Json::object { + { "path", path }, + { "input", (a >> 1) - 1 }, + { "offset", i }, + }).dump(); + + if (ywmap_clocks.count(sig[i])) { + int clock_mode = ywmap_clocks[sig[i]]; + if (clock_mode != 3) { + clock_lines[a] += json11::Json(json11::Json::object { + { "path", path }, + { "input", (a >> 1) - 1 }, + { "offset", i }, + { "edge", clock_mode == 1 ? "posedge" : "negedge" }, + }).dump(); + } + } + } + } + } + + f << " \"clocks\": ["; + clock_lines.sort(); + const char *sep = "\n "; + for (auto &it : clock_lines) { + f << sep << it.second; + sep = ",\n "; + } + f << "\n ],\n"; + + f << " \"inputs\": ["; + input_lines.sort(); + sep = "\n "; + for (auto &it : input_lines) { + f << sep << it.second; + sep = ",\n "; + } + f << "\n ],\n"; + + f << " \"seqs\": ["; + sep = "\n "; + for (auto &it : seq_lines) { + f << sep << it.second; + sep = ",\n "; + } + f << "\n ],\n"; + + f << " \"inits\": ["; + sep = "\n "; + for (auto &it : init_lines) { + f << sep << it.second; + sep = ",\n "; + } + f << "\n ]\n}\n"; + } + }; struct AigerBackend : public Backend { @@ -728,6 +878,9 @@ struct AigerBackend : public Backend { log(" -no-startoffset\n"); log(" make indexes zero based, enable using map files with smt solvers.\n"); log("\n"); + log(" -ywmap \n"); + log(" write a map file for conversion to and from yosys witness traces.\n"); + log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n"); @@ -747,6 +900,7 @@ struct AigerBackend : public Backend { bool lmode = false; bool no_startoffset = false; std::string map_filename; + std::string yw_map_filename; log_header(design, "Executing AIGER backend.\n"); @@ -778,6 +932,10 @@ struct AigerBackend : public Backend { verbose_map = true; continue; } + if (yw_map_filename.empty() && args[argidx] == "-ywmap" && argidx+1 < args.size()) { + yw_map_filename = args[++argidx]; + continue; + } if (args[argidx] == "-no-startoffset") { no_startoffset = true; continue; @@ -802,6 +960,9 @@ struct AigerBackend : public Backend { } extra_args(f, filename, args, argidx, !ascii_mode); + if (!yw_map_filename.empty() && !zinit_mode) + log_error("Currently -ywmap requires -zinit.\n"); + Module *top_module = design->top_module(); if (top_module == nullptr) @@ -826,6 +987,14 @@ struct AigerBackend : public Backend { log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno)); writer.write_map(mapf, verbose_map, no_startoffset); } + + if (!yw_map_filename.empty()) { + std::ofstream mapf; + mapf.open(yw_map_filename.c_str(), std::ofstream::trunc); + if (mapf.fail()) + log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno)); + writer.write_ywmap(mapf); + } } } AigerBackend; diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index 1105d9ed0..03d72a17b 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -17,11 +17,12 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import os, sys +import os, sys, itertools, re ##yosys-sys-path## +import json import click -from ywio import ReadWitness, WriteWitness, WitnessSig +from ywio import ReadWitness, WriteWitness, WitnessSig, WitnessSigMap, WitnessValues, coalesce_signals @click.group() def cli(): @@ -86,5 +87,150 @@ def yw2yw(input, output): click.echo(f"Copied {outyw.t + 1} time steps.") + +class AigerMap: + def __init__(self, mapfile): + data = json.load(mapfile) + + self.latch_count = data["latch_count"] + self.input_count = data["input_count"] + + self.clocks = data["clocks"] + + self.sigmap = WitnessSigMap() + self.init_inputs = set(init["input"] for init in data["inits"]) + + for bit in data["inputs"] + data["seqs"] + data["inits"]: + self.sigmap.add_bit((tuple(bit["path"]), bit["offset"]), bit["input"]) + + + +@cli.command(help=""" +Convert an AIGER witness trace into a Yosys witness trace. + +This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'. +""") +@click.argument("input", type=click.File("r")) +@click.argument("mapfile", type=click.File("r")) +@click.argument("output", type=click.File("w")) +def aiw2yw(input, mapfile, output): + input_name = input.name + click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...") + click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}") + aiger_map = AigerMap(mapfile) + + header_lines = list(itertools.islice(input, 0, 2)) + + if len(header_lines) == 2 and header_lines[1][0] in ".bcjf": + status = header_lines[0].strip() + if status == "0": + raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is unsat") + elif status == "2": + raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is sat") + elif status != "1": + raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file") + else: + input = itertools.chain(header_lines, input) + + ffline = next(input, None) + if ffline is None: + raise click.ClickException(f"{input_name}: unexpected end of file") + ffline = ffline.strip() + if not re.match(r'[01x]*$', ffline): + raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file") + if not re.match(r'[0]*$', ffline): + raise click.ClickException(f"{input_name}: non-default initial state not supported") + + outyw = WriteWitness(output, 'yosys-witness aiw2yw') + + for clock in aiger_map.clocks: + outyw.add_clock(clock["path"], clock["offset"], clock["edge"]) + + for (path, offset), id in aiger_map.sigmap.bit_to_id.items(): + outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs) + + missing = set() + + while True: + inline = next(input, None) + if inline is None: + click.echo(f"Warning: {input_name}: file may be incomplete") + break + inline = inline.strip() + if inline in [".", "# DONE"]: + break + if inline.startswith("#"): + continue + + if not re.match(r'[01x]*$', ffline): + raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file") + + if len(inline) != aiger_map.input_count: + raise click.ClickException( + f"{input_name}: {mapfile.name}: number of inputs does not match, " + f"{len(inline)} in witness, {aiger_map.input_count} in map file") + + values = WitnessValues() + for i, v in enumerate(inline): + if v == "x" or outyw.t > 0 and i in aiger_map.init_inputs: + continue + + try: + bit = aiger_map.sigmap.id_to_bit[i] + except IndexError: + bit = None + if bit is None: + missing.insert(i) + + values[bit] = v + + outyw.step(values) + + outyw.end_trace() + + if missing: + click.echo("The following AIGER inputs belong to unknown signals:") + click.echo(" " + " ".join(str(id) for id in sorted(missing))) + + click.echo(f"Converted {outyw.t} time steps.") + +@cli.command(help=""" +Convert a Yosys witness trace into an AIGER witness trace. + +This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'. +""") +@click.argument("input", type=click.File("r")) +@click.argument("mapfile", type=click.File("r")) +@click.argument("output", type=click.File("w")) +def yw2aiw(input, mapfile, output): + click.echo(f"Converting Yosys witness trace {input.name!r} to AIGER witness trace {output.name!r}...") + click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}") + aiger_map = AigerMap(mapfile) + inyw = ReadWitness(input) + + print("1", file=output) + print("b0", file=output) + # TODO the b0 status isn't really accurate, but we don't have any better info here + print("0" * aiger_map.latch_count, file=output) + + all_missing = set() + + for t, step in inyw.steps(): + bits, missing = step.pack_present(aiger_map.sigmap) + bits = bits[::-1].replace('?', 'x') + all_missing.update(missing) + bits += 'x' * (aiger_map.input_count - len(bits)) + print(bits, file=output) + + print(".", file=output) + + if all_missing: + click.echo("The following signals are missing in the AIGER map file and will be dropped:") + for sig in coalesce_signals(WitnessSig(*bit) for bit in all_missing): + click.echo(" " + sig.pretty()) + + + click.echo(f"Converted {len(inyw)} time steps.") + if __name__ == "__main__": cli() -- cgit v1.2.3 From 475267ac254f6f5ec2202b58c26d8ea82c9d2e4a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 17:04:34 +0200 Subject: smtbmc: Add --check-witness mode This verifies that the given constraints force an assertion failure. This is useful to debug witness trace conversion (and minimization). --- backends/smt2/smtbmc.py | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index b8ea22aaf..3714e2918 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -54,6 +54,7 @@ smtctop = None noinit = False binarymode = False keep_going = False +check_witness = False so = SmtOpts() @@ -170,6 +171,10 @@ def usage(): covering all found failed assertions, the character '%' is replaced in all dump filenames with an increasing number. + --check-witness + check that the used witness file contains sufficient + constraints to force an assertion failure. + """ + so.helpmsg()) sys.exit(1) @@ -178,7 +183,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"]) except: usage() @@ -257,6 +262,8 @@ for o, a in opts: binarymode = True elif o == "--keep-going": keep_going = True + elif o == "--check-witness": + check_witness = True elif so.handle(o, a): pass else: @@ -1774,6 +1781,7 @@ else: # not tempind, covermode smt_assert("(not %s)" % active_assert_expr) else: + active_assert_expr = "true" smt_assert("false") @@ -1781,6 +1789,17 @@ else: # not tempind, covermode if retstatus != "FAILED": print("%s BMC failed!" % smt.timestamp()) + if check_witness: + print_msg("Checking witness constraints...") + smt_pop() + smt_push() + smt_assert(active_assert_expr) + if smt_check_sat() != "sat": + retstatus = "PASSED" + check_witness = False + num_steps = -1 + break + if append_steps > 0: for i in range(last_check_step+1, last_check_step+1+append_steps): print_msg("Appending additional step %d." % i) @@ -1873,6 +1892,8 @@ else: # not tempind, covermode print_anyconsts(0) write_trace(0, num_steps, '%') + if check_witness: + retstatus = "FAILED" smt.write("(exit)") smt.wait() -- cgit v1.2.3 From b156fe903f75b589cb270c062a5cbd65f55e5cf6 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:24:28 +0200 Subject: yosys-witness: Add stats command --- backends/smt2/witness.py | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index 03d72a17b..a1e65569d 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -62,6 +62,24 @@ def display(input): yield f" {step_prefix} {sig.pretty()} = {display_bits}" click.echo_via_pager([line + "\n" for line in output()]) + +@cli.command(help=""" +Display statistics of a Yosys witness trace. +""") +@click.argument("input", type=click.File("r")) +def stats(input): + click.echo(f"Reading Yosys witness trace {input.name!r}...") + inyw = ReadWitness(input) + + total = 0 + + for t, values in inyw.steps(): + click.echo(f"{t:5}: {len(values.values):8} bits") + total += len(values.values) + + click.echo(f"total: {total:8} bits") + + @cli.command(help=""" Transform a Yosys witness trace. -- cgit v1.2.3 From 65145db7e7bec998a194aa0f6335de50df00e550 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 3 Aug 2022 17:27:06 +0200 Subject: rename: Add -witness mode --- CHANGELOG | 2 ++ passes/cmds/rename.cc | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 83 insertions(+) diff --git a/CHANGELOG b/CHANGELOG index a9144facf..6403c5b9a 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -7,6 +7,8 @@ Yosys 0.20 .. Yosys 0.20-dev * New commands and options - Added "formalff" pass - transforms FFs for formal verification - Added option "-formal" to "memory_map" pass + - Added option "-witness" to "rename" - give public names to all signals + present in yosys witness traces * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index b49d5cdc2..45576c91c 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -106,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin return name + suffix; } +static bool rename_witness(RTLIL::Design *design, dict &cache, RTLIL::Module *module) +{ + auto cached = cache.find(module); + if (cached != cache.end()) { + if (cached->second == -1) + log_error("Cannot rename witness signals in a design containing recursive instantiations.\n"); + return cached->second; + } + cache.emplace(module, -1); + + bool has_witness_signals = false; + for (auto cell : module->cells()) + { + RTLIL::Module *impl = design->module(cell->type); + if (impl != nullptr) { + bool witness_in_cell = rename_witness(design, cache, impl); + has_witness_signals |= witness_in_cell; + if (witness_in_cell && !cell->name.isPublic()) { + std::string name = cell->name.c_str() + 1; + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->rename(cell, new_id); + } + } + + if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) { + has_witness_signals = true; + auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y; + auto sig_out = cell->getPort(QY); + + for (auto chunk : sig_out.chunks()) { + if (chunk.is_wire() && !chunk.wire->name.isPublic()) { + std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1); + for (auto &c : name) + if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_') + c = '_'; + auto new_id = module->uniquify("\\_witness_." + name); + auto new_wire = module->addWire(new_id, GetSize(sig_out)); + new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 }); + module->connect({sig_out, new_wire}); + cell->setPort(QY, new_wire); + break; + } + } + } + } + + cache[module] = has_witness_signals; + return has_witness_signals; +} + struct RenamePass : public Pass { RenamePass() : Pass("rename", "rename object in the design") { } void help() override @@ -147,6 +201,14 @@ struct RenamePass : public Pass { log("pattern is '_%%_'.\n"); log("\n"); log("\n"); + log(" rename -witness\n"); + log("\n"); + log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); + log("cells that do not have a public name. This ensures that, during formal\n"); + log("verification, a solver-found trace can be fully specified using a public\n"); + log("hierarchical names.\n"); + log("\n"); + log("\n"); log(" rename -hide [selection]\n"); log("\n"); log("Assign private names (the ones with $-prefix) to all selected wires and cells\n"); @@ -172,6 +234,7 @@ struct RenamePass : public Pass { bool flag_src = false; bool flag_wire = false; bool flag_enumerate = false; + bool flag_witness = false; bool flag_hide = false; bool flag_top = false; bool flag_output = false; @@ -203,6 +266,11 @@ struct RenamePass : public Pass { got_mode = true; continue; } + if (arg == "-witness" && !got_mode) { + flag_witness = true; + got_mode = true; + continue; + } if (arg == "-hide" && !got_mode) { flag_hide = true; got_mode = true; @@ -309,6 +377,19 @@ struct RenamePass : public Pass { } } else + if (flag_witness) + { + extra_args(args, argidx, design, false); + + RTLIL::Module *module = design->top_module(); + + if (module == nullptr) + log_cmd_error("No top module found!\n"); + + dict cache; + rename_witness(design, cache, module); + } + else if (flag_hide) { extra_args(args, argidx, design); -- cgit v1.2.3 From 4ad13c647e2789268aed06d528bc2a40c6196133 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:34:14 +0200 Subject: clk2fflogic: Generate less unused logic when using verific Verific generates a lot of FFs with an unused async load and we cannot always optimize that away before running clk2fflogic, so check for that special case here. --- passes/sat/clk2fflogic.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index b1b0567a0..2384ffced 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -233,7 +233,10 @@ struct Clk2fflogicPass : public Pass { qval = past_q; } - if (ff.has_aload) { + // The check for a constant sig_aload is also done by opt_dff, but when using verific and running + // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids + // generating a lot of extra logic. + if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) { SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID); if (!ff.is_fine) -- cgit v1.2.3 From 927af914f11f895d10475917d5c0b06261703362 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 5 Aug 2022 15:22:56 +0200 Subject: Update CEX minimization patches for abc --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b3a466a5e..4342882c3 100644 --- a/Makefile +++ b/Makefile @@ -155,7 +155,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 = 7cc11f7 +ABCREV = 20f970f ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) -- cgit v1.2.3 From 66f761a8c54b66b8e6b4667cfb54072ad76952e0 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 8 Aug 2022 15:33:47 +0200 Subject: smtbmc: Set step range for --yw and dont skip steps for --check-witness --- backends/smt2/smtbmc.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3714e2918..5f05287de 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -482,7 +482,8 @@ if cexfile is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = max(skip_steps, step) + if not check_witness: + skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) if aimfile is not None: @@ -615,7 +616,8 @@ if aimfile is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = max(skip_steps, step) + if not check_witness: + skip_steps = max(skip_steps, step) # some solvers optimize the properties so that they fail one cycle early, # thus we check the properties in the cycle the aiger witness ends, and # if that doesn't work, we check the cycle after that as well. @@ -623,6 +625,11 @@ if aimfile is not None: step += 1 if inywfile is not None: + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(inywfile, "r") as f: inyw = ReadWitness(f) @@ -717,6 +724,11 @@ if inywfile is not None: smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) constr_assumes[t].append((inywfile, smt_constr)) + if not got_topt: + if not check_witness: + skip_steps = max(skip_steps, t) + num_steps = max(num_steps, t+1) + if btorwitfile is not None: with open(btorwitfile, "r") as f: step = None -- cgit v1.2.3 From f7023d06a2bda56467c8f07cc44d3b92f0eab2ba Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 9 Aug 2022 15:43:26 +0200 Subject: sim: -hdlname option to preserve flattened hierarchy in sim output --- CHANGELOG | 2 ++ passes/sat/sim.cc | 50 +++++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 43 insertions(+), 9 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 6403c5b9a..a1f4624ee 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -9,6 +9,8 @@ Yosys 0.20 .. Yosys 0.20-dev - Added option "-formal" to "memory_map" pass - Added option "-witness" to "rename" - give public names to all signals present in yosys witness traces + - Added option "-hdlname" to "sim" pass - preserves hiearachy when writing + simulation output for a flattened design * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index ea64dce06..18a25a097 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -81,6 +81,7 @@ struct SimShared bool hide_internal = true; bool writeback = false; bool zinit = false; + bool hdlname = false; int rstlen = 1; FstData *fst = nullptr; double start_time = 0; @@ -738,9 +739,17 @@ struct SimInstance child.second->register_signals(id); } - void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) + void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) { - enter_scope(name()); + int exit_scopes = 1; + if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) { + auto hdlname = instance->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + for (auto name : hdlname) + enter_scope("\\" + name); + exit_scopes = hdlname.size(); + } else + enter_scope(name()); dict registers; for (auto cell : module->cells()) @@ -756,13 +765,25 @@ struct SimInstance for (auto signal : signal_database) { - register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0); + if (shared->hdlname && signal.first->name.isPublic() && signal.first->has_attribute(ID::hdlname)) { + auto hdlname = signal.first->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + auto signal_name = std::move(hdlname.back()); + hdlname.pop_back(); + for (auto name : hdlname) + enter_scope("\\" + name); + register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0); + for (auto name : hdlname) + exit_scope(); + } else + register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0); } for (auto child : children) child.second->write_output_header(enter_scope, exit_scope, register_signal); - exit_scope(); + for (int i = 0; i < exit_scopes; i++) + exit_scope(); } void register_output_step_values(std::map *data) @@ -1712,7 +1733,11 @@ struct VCDWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); }, [this]() { vcdfile << stringf("$upscope $end\n");}, - [this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); } + [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + if (use_signal.at(id)) { + vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name); + } + } ); vcdfile << stringf("$enddefinitions $end\n"); @@ -1770,11 +1795,10 @@ struct FSTWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); }, [this]() { fstWriterSetUpscope(fstfile); }, - [this,use_signal](Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { if (!use_signal.at(id)) return; fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), - stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0); - + name, 0); mapping.emplace(id, fst_id); } ); @@ -1856,7 +1880,7 @@ struct AIWWriter : public OutputWriter worker->top->write_output_header( [](IdString) {}, []() {}, - [this](Wire *wire, int id, bool) { mapping[wire] = id; } + [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; } ); std::map current; @@ -1945,6 +1969,10 @@ struct SimPass : public Pass { log(" write the simulation results to an AIGER witness file\n"); log(" (requires a *.aim file via -map)\n"); log("\n"); + log(" -hdlname\n"); + log(" use the hdlname attribute when writing simulation results\n"); + log(" (preserves hierarchy in a flattened design)\n"); + log("\n"); log(" -x\n"); log(" ignore constant x outputs in simulation file.\n"); log("\n"); @@ -2057,6 +2085,10 @@ struct SimPass : public Pass { worker.outputfiles.emplace_back(std::unique_ptr(new AIWWriter(&worker, aiw_filename.c_str()))); continue; } + if (args[argidx] == "-hdlname") { + worker.hdlname = true; + continue; + } if (args[argidx] == "-n" && argidx+1 < args.size()) { numcycles = atoi(args[++argidx].c_str()); worker.cycles_set = true; -- cgit v1.2.3