From 5db542742b8f69405417e5a715b4b72ce4c78534 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 17:53:58 +0200 Subject: async2sync: turn FFs with const clks into gclk FFs with feedback The formal backends do not support multiple clocks. This includes constant clocks. Constant clocks do appear in what isn't a proper multiclock design, for example when mapping not fully initialized ROMs. As converting FFs with constant clocks to FFs using the global is doable even in a single clock flow, make async2sync do this. --- passes/sat/async2sync.cc | 3 +++ 1 file changed, 3 insertions(+) (limited to 'passes/sat') diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 46c76eba9..6fdf470b1 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -75,6 +75,9 @@ struct Async2syncPass : public Pass { if (ff.has_gclk) continue; + if (ff.has_clk && ff.sig_clk.is_fully_const()) + ff.has_ce = ff.has_clk = ff.has_srst = false; + if (ff.has_clk) { if (ff.has_sr) { -- cgit v1.2.3 From 14ba50908bd53186b13845499635fb3f9ddc60c1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 22 Jul 2022 14:47:00 +0200 Subject: sim: Fix $anyseq in nested modules --- passes/sat/sim.cc | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) (limited to 'passes/sat') diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index d085fab2d..53644c6b7 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -157,6 +157,7 @@ struct SimInstance dict> signal_database; dict fst_handles; + dict fst_inputs; dict> fst_memories; SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) : @@ -820,7 +821,7 @@ struct SimInstance return did_something; } - void addAdditionalInputs(std::map &inputs) + void addAdditionalInputs() { for (auto cell : module->cells()) { @@ -831,7 +832,7 @@ struct SimInstance for(auto &item : fst_handles) { if (item.second==0) continue; // Ignore signals not found if (sig_y == sigmap(item.first)) { - inputs[sig_y.as_wire()] = item.second; + fst_inputs[sig_y.as_wire()] = item.second; found = true; break; } @@ -842,7 +843,21 @@ struct SimInstance } } for (auto child : children) - child.second->addAdditionalInputs(inputs); + child.second->addAdditionalInputs(); + } + + bool setInputs() + { + bool did_something = false; + for(auto &item : fst_inputs) { + std::string v = shared->fst->valueOf(item.second); + did_something |= set_state(item.first, Const::from_string(v)); + } + + for (auto child : children) + did_something |= child.second->setInputs(); + + return did_something; } void setState(dict> bits, std::string values) @@ -1095,18 +1110,17 @@ struct SimWorker : SimShared } SigMap sigmap(topmod); - std::map inputs; for (auto wire : topmod->wires()) { if (wire->port_input) { fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name)); if (id==0) log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str()); - inputs[wire] = id; + top->fst_inputs[wire] = id; } } - top->addAdditionalInputs(inputs); + top->addAdditionalInputs(); uint64_t startCount = 0; uint64_t stopCount = 0; @@ -1152,11 +1166,7 @@ struct SimWorker : SimShared fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) { if (verbose) log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString()); - bool did_something = false; - for(auto &item : inputs) { - std::string v = fst->valueOf(item.second); - did_something |= top->set_state(item.first, Const::from_string(v)); - } + bool did_something = top->setInputs(); if (initial) { did_something |= top->setInitState(); -- cgit v1.2.3 From f4a1906721507c512050f62080a999c4147d92d6 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 8 Aug 2022 20:30:50 +0200 Subject: support file locations containing spaces --- passes/sat/qbfsat.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'passes/sat') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 864d6f05d..1302b3383 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -216,7 +216,7 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, QbfSolutionType ret; const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc"; const std::string smtbmc_warning = "z3: WARNING:"; - const std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", + const std::string smtbmc_cmd = stringf("\"%s\" -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1", yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(), (opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(), (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(), -- cgit v1.2.3 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. --- passes/sat/Makefile.inc | 1 + passes/sat/formalff.cc | 192 ++++++++++++++++++++++++++++++++++++++++++++++++ passes/sat/sim.cc | 2 +- 3 files changed, 194 insertions(+), 1 deletion(-) create mode 100644 passes/sat/formalff.cc (limited to 'passes/sat') 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); -- 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. --- passes/sat/formalff.cc | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'passes/sat') 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(+) (limited to 'passes/sat') 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 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(-) (limited to 'passes/sat') 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 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 --- passes/sat/sim.cc | 50 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 9 deletions(-) (limited to 'passes/sat') 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