diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/Makefile.inc | 1 | ||||
| -rw-r--r-- | passes/sat/async2sync.cc | 3 | ||||
| -rw-r--r-- | passes/sat/clk2fflogic.cc | 193 | ||||
| -rw-r--r-- | passes/sat/formalff.cc | 766 | ||||
| -rw-r--r-- | passes/sat/miter.cc | 58 | ||||
| -rw-r--r-- | passes/sat/mutate.cc | 2 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 63 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 50 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 29 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 623 |
10 files changed, 1542 insertions, 246 deletions
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/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) { diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index b1b0567a0..bba2cbbec 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -26,6 +26,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct SampledSig { + SigSpec sampled, current; + SigSpec &operator[](bool get_current) { return get_current ? current : sampled; } +}; + struct Clk2fflogicPass : public Pass { Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } void help() override @@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass { log("implicit global clock. This is useful for formal verification of designs with\n"); log("multiple clocks.\n"); log("\n"); + log("This pass assumes negative hold time for the async FF inputs. For example when\n"); + log("a reset deasserts with the clock edge, then the FF output will still drive the\n"); + log("reset value in the next cycle regardless of the data-in value at the time of\n"); + log("the clock edge.\n"); + log("\n"); } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) { - if (!is_fine) - return wrap_async_control(module, sig, polarity, past_sig_id); - return wrap_async_control_gate(module, sig, polarity, past_sig_id); + // Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted. + SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) { + if (!polarity) { + if (is_fine) + sig = module->NotGate(NEW_ID, sig); + else + sig = module->Not(NEW_ID, sig); + } + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); + else + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id, GetSize(sig)); - past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig)); - module->addFf(NEW_ID, sig, past_sig); - if (polarity) - sig = module->Or(NEW_ID, sig, past_sig); + // Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge. + SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - sig = module->And(NEW_ID, sig, past_sig); - if (polarity) - return sig; + module->addFf(NEW_ID, sig, sampled_sig); + return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0}); + } + // Sampled and current value of a data signal. + SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = init; + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - return module->Not(NEW_ID, sig); + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id); - past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1; - module->addFfGate(NEW_ID, sig, past_sig); - if (polarity) - sig = module->OrGate(NEW_ID, sig, past_sig); + SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) { + if (is_fine) + return module->MuxGate(NEW_ID, a, b, s); else - sig = module->AndGate(NEW_ID, sig, past_sig); - if (polarity) - return sig; + return module->Mux(NEW_ID, a, b, s); + } + SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) { + if (is_fine) + return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)); else - return module->NotGate(NEW_ID, sig); + return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r)); } void execute(std::vector<std::string> args, RTLIL::Design *design) override { @@ -177,93 +210,47 @@ struct Clk2fflogicPass : public Pass { ff.remove(); - // Strip spaces from signal name, since Yosys IDs can't contain spaces - // Spaces only occur when we have a signal that's a slice of a larger bus, - // e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness - std::string sig_q_str = log_signal(ff.sig_q); - sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end()); - - Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width); - - if (!ff.is_fine) { - module->addFf(NEW_ID, ff.sig_q, past_q); - } else { - module->addFfGate(NEW_ID, ff.sig_q, past_q); - } - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_q, ff.val_init); - - if (ff.has_clk) { + if (ff.has_clk) ff.unmap_ce_srst(); - Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk)))); - initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0); - - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_clk, past_clk); - else - module->addFfGate(NEW_ID, ff.sig_clk, past_clk); + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled; - SigSpec clock_edge_pattern; - - if (ff.pol_clk) { - clock_edge_pattern.append(State::S0); - clock_edge_pattern.append(State::S1); - } else { - clock_edge_pattern.append(State::S1); - clock_edge_pattern.append(State::S0); - } - - SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern); - - Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width); - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_d, past_d); - else - module->addFfGate(NEW_ID, ff.sig_d, past_d); - - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_d, ff.val_init); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); - else - qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); - } else { - qval = past_q; + if (ff.has_clk) { + // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs + auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine); + auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine); + next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine); } - if (ff.has_aload) { - SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload); - else - qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload); + SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst; + // 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. + bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1); + if (has_nonconst_aload) { + sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine); + // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs + sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine); } - if (ff.has_sr) { - SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID); - SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID); - if (!ff.is_fine) { - clrval = module->Not(NEW_ID, clrval); - qval = module->Or(NEW_ID, qval, setval); - module->addAnd(NEW_ID, qval, clrval, ff.sig_q); - } else { - clrval = module->NotGate(NEW_ID, clrval); - qval = module->OrGate(NEW_ID, qval, setval); - module->addAndGate(NEW_ID, qval, clrval, ff.sig_q); - } - } else if (ff.has_arst) { - IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst))); - SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id); - if (!ff.is_fine) - module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q); - else - module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q); - } else { - module->connect(ff.sig_q, qval); + sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine); + sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine); + } + if (ff.has_arst) + sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine); + + // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous + // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously. + for (int current = 0; current < 2; current++) { + if (has_nonconst_aload) + next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine); + if (ff.has_sr) + next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine); + if (ff.has_arst) + next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine); } + + module->connect(ff.sig_q, next_q); } } } diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc new file mode 100644 index 000000000..264a9fb3b --- /dev/null +++ b/passes/sat/formalff.cc @@ -0,0 +1,766 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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" +#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<RTLIL::SigBit, RTLIL::State> initconst_bits; + dict<RTLIL::SigBit, bool> 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<ModWalker::PortBit> 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<RTLIL::State> 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<ModWalker::PortBit> 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 ReplacedPort { + IdString name; + int offset; + bool clk_pol; +}; + +struct HierarchyWorker +{ + Design *design; + pool<Module *> pending; + + dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs; + + HierarchyWorker(Design *design) : + design(design) + { + for (auto module : design->modules()) + pending.insert(module); + } + + void propagate(); + + const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type); +}; + +// Propagates replaced clock signals +struct PropagateWorker +{ + HierarchyWorker &hierarchy; + + Module *module; + SigMap sigmap; + + dict<SigBit, bool> replaced_clk_bits; + dict<SigBit, SigBit> not_drivers; + + std::vector<ReplacedPort> replaced_clk_inputs; + std::vector<std::pair<SigBit, bool>> pending; + + PropagateWorker(Module *module, HierarchyWorker &hierarchy) : + hierarchy(hierarchy), module(module), sigmap(module) + { + hierarchy.pending.erase(module); + + for (auto wire : module->wires()) + if (wire->has_attribute(ID::replaced_by_gclk)) + replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false); + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) { + auto sig_a = cell->getPort(ID::A); + auto &sig_y = cell->getPort(ID::Y); + sig_a.extend_u0(GetSize(sig_y), cell->hasParam(ID::A_SIGNED) && cell->parameters.at(ID::A_SIGNED).as_bool()); + + for (int i = 0; i < GetSize(sig_a); i++) + if (sig_a[i].is_wire()) + not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i])); + } else { + for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type)) + replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true); + } + } + + while (!pending.empty()) { + auto current = pending.back(); + pending.pop_back(); + auto it = not_drivers.find(current.first); + if (it == not_drivers.end()) + continue; + + replace_clk_bit(it->second, !current.second, true); + } + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) + continue; + for (auto &conn : cell->connections()) { + if (!cell->output(conn.first)) + continue; + for (SigBit bit : conn.second) { + sigmap.apply(bit); + if (replaced_clk_bits.count(bit)) + log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n", + log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module)); + } + } + } + + for (auto port : module->ports) { + auto wire = module->wire(port); + if (!wire->port_input) + continue; + for (int i = 0; i < GetSize(wire); i++) { + SigBit bit(wire, i); + sigmap.apply(bit); + auto it = replaced_clk_bits.find(bit); + if (it == replaced_clk_bits.end()) + continue; + replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second}); + + if (it->second) { + bit = module->Not(NEW_ID, bit); + } + } + } + } + + void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute) + { + sigmap.apply(bit); + if (!bit.is_wire()) + log_error("XXX todo\n"); + + auto it = replaced_clk_bits.find(bit); + if (it != replaced_clk_bits.end()) { + if (it->second != polarity) + log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n", + log_signal(bit), log_id(module)); + return; + } + + replaced_clk_bits.emplace(bit, polarity); + + if (add_attribute) { + Wire *clk_wire = bit.wire; + if (bit.offset != 0 || GetSize(bit.wire) != 1) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), bit); + } + clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0; + clk_wire->set_bool_attribute(ID::keep); + } + + pending.emplace_back(bit, polarity); + } +}; + +const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type) +{ + static const std::vector<ReplacedPort> empty; + if (!cell_type.isPublic()) + return empty; + + Module *module = design->module(cell_type); + if (module == nullptr) + return empty; + + auto it = replaced_clk_inputs.find(module); + if (it != replaced_clk_inputs.end()) + return it->second; + + if (pending.count(module)) { + PropagateWorker worker(module, *this); + return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second; + } + + return empty; +} + + +void HierarchyWorker::propagate() +{ + while (!pending.empty()) + PropagateWorker worker(pending.pop(), *this); +} + +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"); + 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"); + log(" -hierarchy\n"); + log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n"); + log(" through the design hierarchy towards the toplevel inputs. This option\n"); + log(" works on the whole design and ignores the selection.\n"); + log("\n"); + log(" -assume\n"); + log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n"); + log(" attribute to the value they would have before an active clock edge.\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<std::string> args, RTLIL::Design *design) override + { + bool flag_clk2ff = false; + bool flag_ff2anyinit = false; + bool flag_anyinit2ff = false; + bool flag_fine = false; + bool flag_setundef = false; + bool flag_hierarchy = false; + bool flag_assume = 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; + } + if (args[argidx] == "-setundef") { + flag_setundef = true; + continue; + } + if (args[argidx] == "-hierarchy") { + flag_hierarchy = true; + continue; + } + if (args[argidx] == "-assume") { + flag_assume = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume 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()) + { + 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); + + + 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)); + if (ff.has_aload || ff.has_arst || ff.has_sr) + log_error("Async inputs 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; + 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<int> 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; + ff.is_fine = false; + emit = true; + break; + } + + auto slice = ff.slice(bits); + slice.is_anyinit = is_anyinit; + slice.is_fine = false; + slice.emit(); + } + } + + if (emit) + ff.emit(); + } + } + + if (flag_hierarchy) { + HierarchyWorker worker(design); + worker.propagate(); + } + + if (flag_assume) { + for (auto module : design->selected_modules()) { + std::vector<pair<SigBit, bool>> found; + for (auto wire : module->wires()) { + if (!wire->has_attribute(ID::replaced_by_gclk)) + continue; + bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1; + + found.emplace_back(SigSpec(wire), clk_pol); + } + for (auto pair : found) { + SigBit clk = pair.first; + + if (pair.second) + clk = module->Not(NEW_ID, clk); + + module->addAssume(NEW_ID, clk, State::S1); + + } + } + } + } +} FormalFfPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 37efadfbd..8f27c4c6f 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -30,7 +30,9 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: bool flag_make_outputs = false; bool flag_make_outcmp = false; bool flag_make_assert = false; + bool flag_make_cover = false; bool flag_flatten = false; + bool flag_cross = false; log_header(design, "Executing MITER pass (creating miter circuit).\n"); @@ -53,10 +55,18 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: flag_make_assert = true; continue; } + if (args[argidx] == "-make_cover") { + flag_make_cover = true; + continue; + } if (args[argidx] == "-flatten") { flag_flatten = true; continue; } + if (args[argidx] == "-cross") { + flag_cross = true; + continue; + } break; } if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0) @@ -75,6 +85,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: RTLIL::Module *gold_module = design->module(gold_name); RTLIL::Module *gate_module = design->module(gate_name); + pool<Wire*> gold_cross_ports; for (auto gold_wire : gold_module->wires()) { if (gold_wire->port_id == 0) @@ -82,12 +93,17 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name); if (gate_wire == nullptr) goto match_gold_port_error; + if (gold_wire->width != gate_wire->width) + goto match_gold_port_error; + if (flag_cross && !gold_wire->port_input && gold_wire->port_output && + gate_wire->port_input && !gate_wire->port_output) { + gold_cross_ports.insert(gold_wire); + continue; + } if (gold_wire->port_input != gate_wire->port_input) goto match_gold_port_error; if (gold_wire->port_output != gate_wire->port_output) goto match_gold_port_error; - if (gold_wire->width != gate_wire->width) - goto match_gold_port_error; continue; match_gold_port_error: log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str()); @@ -99,12 +115,15 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name); if (gold_wire == nullptr) goto match_gate_port_error; + if (gate_wire->width != gold_wire->width) + goto match_gate_port_error; + if (flag_cross && !gold_wire->port_input && gold_wire->port_output && + gate_wire->port_input && !gate_wire->port_output) + continue; if (gate_wire->port_input != gold_wire->port_input) goto match_gate_port_error; if (gate_wire->port_output != gold_wire->port_output) goto match_gate_port_error; - if (gate_wire->width != gold_wire->width) - goto match_gate_port_error; continue; match_gate_port_error: log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str()); @@ -123,6 +142,22 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: for (auto gold_wire : gold_module->wires()) { + if (gold_cross_ports.count(gold_wire)) + { + SigSpec w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width); + gold_cell->setPort(gold_wire->name, w); + if (flag_ignore_gold_x) { + RTLIL::SigSpec w_x = miter_module->addWire(NEW_ID, GetSize(w)); + for (int i = 0; i < GetSize(w); i++) + miter_module->addEqx(NEW_ID, w[i], State::Sx, w_x[i]); + RTLIL::SigSpec w_any = miter_module->And(NEW_ID, miter_module->Anyseq(NEW_ID, GetSize(w)), w_x); + RTLIL::SigSpec w_masked = miter_module->And(NEW_ID, w, miter_module->Not(NEW_ID, w_x)); + w = miter_module->And(NEW_ID, w_any, w_masked); + } + gate_cell->setPort(gold_wire->name, w); + continue; + } + if (gold_wire->port_input) { RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width); @@ -215,6 +250,12 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: miter_module->connect(RTLIL::SigSig(w_cmp, this_condition)); } + if (flag_make_cover) + { + auto cover_condition = miter_module->Not(NEW_ID, this_condition); + miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1); + } + all_conditions.append(this_condition); } } @@ -380,10 +421,19 @@ struct MiterPass : public Pass { log(" -make_assert\n"); log(" also create an 'assert' cell that checks if trigger is always low.\n"); log("\n"); + log(" -make_cover\n"); + log(" also create a 'cover' cell for each gold/gate output pair.\n"); + log("\n"); log(" -flatten\n"); log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); log("\n"); log("\n"); + log(" -cross\n"); + log(" allow output ports on the gold module to match input ports on the\n"); + log(" gate module. This is useful when the gold module contains additional\n"); + log(" logic to drive some of the gate module inputs.\n"); + log("\n"); + log("\n"); log(" miter -assert [options] module [miter_name]\n"); log("\n"); log("Creates a miter circuit for property checking. All input ports are kept,\n"); diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 42eb0c6d0..02174be53 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -527,6 +527,8 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena } log("Raw database size: %d\n", GetSize(database)); + if (N > GetSize(database)) + log_warning("%d mutations requested but only %d could be created!\n", N, GetSize(database)); if (N != 0) { database_reduce(database, opts, opts.none ? N-1 : N, rng); log("Reduced database size: %d\n", GetSize(database)); diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 864d6f05d..db6836ea1 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -66,9 +66,9 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool ass } void specialize_from_file(RTLIL::Module *module, const std::string &file) { - YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); - YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified - YS_REGEX_MATCH_TYPE bit_m, m; + std::regex hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); + std::regex hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified + std::smatch bit_m, m; dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell; dict<RTLIL::SigBit, RTLIL::State> hole_assignments; @@ -83,9 +83,9 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::string buf; while (std::getline(fin, buf)) { bool bit_assn = true; - if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { + if (!std::regex_search(buf, bit_m, hole_bit_assn_regex)) { bit_assn = false; - if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)) + if (!std::regex_search(buf, m, hole_assn_regex)) log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str()); } @@ -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(), @@ -416,6 +416,8 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.solver = opt.Solver::Yices; else if (args[opt.argidx+1] == "cvc4") opt.solver = opt.Solver::CVC4; + else if (args[opt.argidx+1] == "cvc5") + opt.solver = opt.Solver::CVC5; else log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str()); opt.argidx++; @@ -508,11 +510,11 @@ struct QbfSatPass : public Pass { log("\n"); log(" qbfsat [options] [selection]\n"); log("\n"); - log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n"); - log("selected module. Existentially-quantified variables are declared by assigning a wire\n"); - log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n"); - log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n"); - log("variables by default.\n"); + log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the\n"); + log("currently selected module. Existentially-quantified variables are declared by\n"); + log("assigning a wire \"$anyconst\". Universally-quantified variables may be\n"); + log("explicitly declared by assigning a wire \"$allconst\", but module inputs will be\n"); + log("treated as universally-quantified variables by default.\n"); log("\n"); log(" -nocleanup\n"); log(" Do not delete temporary files and directories. Useful for debugging.\n"); @@ -521,27 +523,29 @@ struct QbfSatPass : public Pass { log(" Pass the --dump-smt2 option to yosys-smtbmc.\n"); log("\n"); log(" -assume-outputs\n"); - log(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n"); + log(" Add an \"$assume\" cell for the conjunction of all one-bit module output\n"); + log(" wires.\n"); log("\n"); log(" -assume-negative-polarity\n"); - log(" When adding $assume cells for one-bit module output wires, assume they are\n"); - log(" negative polarity signals and should always be low, for example like the\n"); - log(" miters created with the `miter` command.\n"); + log(" When adding $assume cells for one-bit module output wires, assume they\n"); + log(" are negative polarity signals and should always be low, for example like\n"); + log(" the miters created with the `miter` command.\n"); log("\n"); log(" -nooptimize\n"); - log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n"); - log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n"); + log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit\n"); + log(" \"(maximize)\" or \"(minimize)\" in the SMT-LIBv2, and generally make no\n"); + log(" attempt to optimize anything.\n"); log("\n"); log(" -nobisection\n"); - log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n"); - log(" attempt to optimize that value with the default iterated solving and threshold\n"); - log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n"); - log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n"); - log(" quantified bitvector problems.\n"); + log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute,\n"); + log(" do not attempt to optimize that value with the default iterated solving\n"); + log(" and threshold bisection approach. Instead, have yosys-smtbmc emit a\n"); + log(" \"(minimize)\" or \"(maximize)\" command in the SMT-LIBv2 output and\n"); + log(" hope that the solver supports optimizing quantified bitvector problems.\n"); log("\n"); log(" -solver <solver>\n"); - log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); - log(" (default: yices)\n"); + log(" Use a particular solver. Choose one of: \"z3\", \"yices\", \"cvc4\"\n"); + log(" and \"cvc5\". (default: yices)\n"); log("\n"); log(" -solver-option <name> <value>\n"); log(" Set the specified solver option in the SMT-LIBv2 problem file.\n"); @@ -567,13 +571,14 @@ struct QbfSatPass : public Pass { log(" corresponding constant value from the model produced by the solver.\n"); log("\n"); log(" -specialize-from-file <solution file>\n"); - log(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n"); - log(" cell in the current module with a constant value provided by the specified file.\n"); + log(" Do not run the solver, but instead only attempt to replace each\n"); + log(" \"$anyconst\" cell in the current module with a constant value provided\n"); + log(" by the specified file.\n"); log("\n"); log(" -write-solution <solution file>\n"); - log(" If the problem is satisfiable, write the corresponding constant value for each\n"); - log(" \"$anyconst\" cell from the model produced by the solver to the specified file."); - log("\n"); + log(" If the problem is satisfiable, write the corresponding constant value\n"); + log(" for each \"$anyconst\" cell from the model produced by the solver to the\n"); + log(" specified file.\n"); log("\n"); } diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h index c96c6f818..253cecce4 100644 --- a/passes/sat/qbfsat.h +++ b/passes/sat/qbfsat.h @@ -29,7 +29,7 @@ struct QbfSolveOptions { bool specialize = false, specialize_from_file = false, write_solution = false, nocleanup = false; bool dump_final_smt2 = false, assume_outputs = false, assume_neg = false, nooptimize = false; bool nobisection = false, sat = false, unsat = false, show_smtbmc = false; - enum Solver{Z3, Yices, CVC4} solver = Yices; + enum Solver{Z3, Yices, CVC4, CVC5} solver = Yices; enum OptimizationLevel{O0, O1, O2} oflag = O0; dict<std::string, std::string> solver_options; int timeout = 0; @@ -45,6 +45,8 @@ struct QbfSolveOptions { return "yices"; else if (solver == Solver::CVC4) return "cvc4"; + else if (solver == Solver::CVC5) + return "cvc5"; log_cmd_error("unknown solver specified.\n"); return ""; @@ -152,67 +154,67 @@ struct QbfSolutionType { } void recover_solution() { - YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED"); - YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); - YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); - YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); - YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); - YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); - YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); - YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); - YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); + std::regex sat_regex = YS_REGEX_COMPILE("Status: PASSED"); + std::regex unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available"); + std::regex unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED"); + std::regex timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)"); + std::regex timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)"); + std::regex unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)"); + std::regex unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver"); + std::regex memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\""); + std::regex hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)"); #ifndef NDEBUG - YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); - YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); + std::regex hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); + std::regex hole_val_regex = YS_REGEX_COMPILE("[0-9]+"); #endif - YS_REGEX_MATCH_TYPE m; + std::smatch m; bool sat_regex_found = false; bool unsat_regex_found = false; dict<std::string, bool> hole_value_recovered; for (const std::string &x : stdout_lines) { - if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { + if(std::regex_search(x, m, hole_value_regex)) { std::string loc = m[1].str(); std::string val = m[2].str(); #ifndef NDEBUG - log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex)); - log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex)); + log_assert(std::regex_search(loc, hole_loc_regex)); + log_assert(std::regex_search(val, hole_val_regex)); #endif auto locs = split_tokens(loc, "|"); pool<std::string> loc_pool(locs.begin(), locs.end()); hole_to_value[loc_pool] = val; } - else if (YS_REGEX_NS::regex_search(x, sat_regex)) { + else if (std::regex_search(x, sat_regex)) { sat_regex_found = true; sat = true; unknown = false; } - else if (YS_REGEX_NS::regex_search(x, unsat_regex)) { + else if (std::regex_search(x, unsat_regex)) { unsat_regex_found = true; sat = false; unknown = false; } - else if (YS_REGEX_NS::regex_search(x, memout_regex)) { + else if (std::regex_search(x, memout_regex)) { unknown = true; log_warning("solver ran out of memory\n"); } - else if (YS_REGEX_NS::regex_search(x, timeout_regex)) { + else if (std::regex_search(x, timeout_regex)) { unknown = true; log_warning("solver timed out\n"); } - else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) { + else if (std::regex_search(x, timeout_regex2)) { unknown = true; log_warning("solver timed out\n"); } - else if (YS_REGEX_NS::regex_search(x, unknown_regex)) { + else if (std::regex_search(x, unknown_regex)) { unknown = true; log_warning("solver returned \"unknown\"\n"); } - else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) { + else if (std::regex_search(x, unsat_regex2)) { unsat_regex_found = true; sat = false; unknown = false; } - else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) { + else if (std::regex_search(x, unknown_regex2)) { unknown = true; } } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index df2725b3c..69f81e3df 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -65,11 +65,12 @@ struct SatHelper int max_timestep, timeout; bool gotTimeout; - SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) : + SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) : design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap) { this->enable_undef = enable_undef; satgen.model_undef = enable_undef; + satgen.def_formal = set_def_formal; set_init_def = false; set_init_undef = false; set_init_zero = false; @@ -254,7 +255,13 @@ struct SatHelper if (initstate) { - RTLIL::SigSpec big_lhs, big_rhs; + RTLIL::SigSpec big_lhs, big_rhs, forced_def; + + // Check for $anyinit cells that are forced to be defined + if (set_init_undef && satgen.def_formal) + for (auto cell : module->cells()) + if (cell->type == ID($anyinit)) + forced_def.append(sigmap(cell->getPort(ID::Q))); for (auto wire : module->wires()) { @@ -323,6 +330,7 @@ struct SatHelper if (set_init_undef) { RTLIL::SigSpec rem = satgen.initial_state.export_all(); rem.remove(big_lhs); + rem.remove(forced_def); big_lhs.append(rem); big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size())); } @@ -758,6 +766,7 @@ struct SatHelper if (last_timestep == -2) log(" no model variables selected for display.\n"); + fprintf(f, "#%d\n", last_timestep+1); fclose(f); } @@ -932,6 +941,9 @@ struct SatPass : public Pass { log(" -set-def-inputs\n"); log(" add -set-def constraints for all module inputs\n"); log("\n"); + log(" -set-def-formal\n"); + log(" add -set-def constraints for formal $anyinit, $anyconst, $anyseq cells\n"); + log("\n"); log(" -show <signal>\n"); log(" show the model for the specified signal. if no -show option is\n"); log(" passed then a set of signals to be shown is automatically selected.\n"); @@ -1067,7 +1079,7 @@ struct SatPass : public Pass { std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at; std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef; int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0; - bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false; + bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false, set_def_formal = false; bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false; bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false; bool show_regs = false, show_public = false, show_all = false; @@ -1140,6 +1152,11 @@ struct SatPass : public Pass { set_def_inputs = true; continue; } + if (args[argidx] == "-set-def-formal") { + enable_undef = true; + set_def_formal = true; + continue; + } if (args[argidx] == "-set" && argidx+2 < args.size()) { std::string lhs = args[++argidx]; std::string rhs = args[++argidx]; @@ -1379,8 +1396,8 @@ struct SatPass : public Pass { if (loopcount > 0 || max_undef) log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n"); - SatHelper basecase(design, module, enable_undef); - SatHelper inductstep(design, module, enable_undef); + SatHelper basecase(design, module, enable_undef, set_def_formal); + SatHelper inductstep(design, module, enable_undef, set_def_formal); basecase.sets = sets; basecase.set_assumes = set_assumes; @@ -1569,7 +1586,7 @@ struct SatPass : public Pass { if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); - SatHelper sathelper(design, module, enable_undef); + SatHelper sathelper(design, module, enable_undef, set_def_formal); sathelper.sets = sets; sathelper.set_assumes = set_assumes; diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index d085fab2d..cfe31968d 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -23,6 +23,8 @@ #include "kernel/mem.h" #include "kernel/fstdata.h" #include "kernel/ff.h" +#include "kernel/yw.h" +#include "kernel/json.h" #include <ctime> @@ -74,6 +76,17 @@ struct OutputWriter SimWorker *worker; }; +struct SimInstance; +struct TriggeredAssertion { + int step; + SimInstance *instance; + Cell *cell; + + TriggeredAssertion(int step, SimInstance *instance, Cell *cell) : + step(step), instance(instance), cell(cell) + { } +}; + struct SimShared { bool debug = false; @@ -81,6 +94,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; @@ -92,6 +106,9 @@ struct SimShared bool ignore_x = false; bool date = false; bool multiclock = false; + int next_output_id = 0; + int step = 0; + std::vector<TriggeredAssertion> triggered_assertions; }; void zinit(State &v) @@ -151,12 +168,16 @@ struct SimInstance dict<Cell*, ff_state_t> ff_database; dict<IdString, mem_state_t> mem_database; pool<Cell*> formal_database; + pool<Cell*> initstate_database; dict<Cell*, IdString> mem_cells; std::vector<Mem> memories; dict<Wire*, pair<int, Const>> signal_database; + dict<IdString, std::map<int, pair<int, Const>>> trace_mem_database; + dict<std::pair<IdString, int>, Const> trace_mem_init_database; dict<Wire*, fstHandle> fst_handles; + dict<Wire*, fstHandle> fst_inputs; dict<IdString, dict<int,fstHandle>> fst_memories; SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) : @@ -230,7 +251,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); @@ -252,6 +273,8 @@ struct SimInstance if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } + if (cell->type == ID($initstate)) + initstate_database.insert(cell); } if (shared->zinit) @@ -298,6 +321,21 @@ struct SimInstance return log_id(module->name); } + vector<std::string> witness_full_path() const + { + if (instance != nullptr) + return parent->witness_full_path(instance); + return vector<std::string>(); + } + + vector<std::string> witness_full_path(Cell *cell) const + { + auto result = witness_full_path(); + auto cell_path = witness_path(cell); + result.insert(result.end(), cell_path.begin(), cell_path.end()); + return result; + } + Const get_state(SigSpec sig) { Const value; @@ -323,7 +361,7 @@ struct SimInstance log_assert(GetSize(sig) <= GetSize(value)); for (int i = 0; i < GetSize(sig); i++) - if (state_nets.at(sig[i]) != value[i]) { + if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) { state_nets.at(sig[i]) = value[i]; dirty_bits.insert(sig[i]); did_something = true; @@ -336,12 +374,23 @@ struct SimInstance void set_memory_state(IdString memid, Const addr, Const data) { + set_memory_state(memid, addr.as_int(), data); + } + + void set_memory_state(IdString memid, int addr, Const data) + { auto &state = mem_database[memid]; - int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width; + bool dirty = false; + + int offset = (addr - state.mem->start_offset) * state.mem->width; for (int i = 0; i < GetSize(data); i++) - if (0 <= i+offset && i+offset < state.mem->size * state.mem->width) - state.data.bits[i+offset] = data.bits[i]; + if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa) + if (state.data.bits[i+offset] != data.bits[i]) + dirty = true, state.data.bits[i+offset] = data.bits[i]; + + if (dirty) + dirty_memories.insert(memid); } void set_memory_state_bit(IdString memid, int offset, State data) @@ -349,7 +398,10 @@ struct SimInstance auto &state = mem_database[memid]; if (offset >= state.mem->size * state.mem->width) log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid)); - state.data.bits[offset] = data; + if (state.data.bits[offset] != data) { + state.data.bits[offset] = data; + dirty_memories.insert(memid); + } } void update_cell(Cell *cell) @@ -445,9 +497,14 @@ struct SimInstance log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid)); if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2); + + for (int offset = 0; offset < 1 << port.wide_log2; offset++) { + register_memory_addr(id, addr_int + offset); + } } set_state(port.data, data); @@ -507,7 +564,7 @@ struct SimInstance } } - bool update_ph2() + bool update_ph2(bool gclk) { bool did_something = false; @@ -565,7 +622,8 @@ struct SimInstance } if (ff_data.has_gclk) { // $ff - current_q = ff.past_d; + if (gclk) + current_q = ff.past_d; } if (set_state(ff_data.sig_q, current_q)) did_something = true; @@ -601,7 +659,8 @@ struct SimInstance if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) for (int i = 0; i < (mem.width << port.wide_log2); i++) if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) { @@ -609,12 +668,15 @@ struct SimInstance dirty_memories.insert(mem.memid); did_something = true; } + + for (int i = 0; i < 1 << port.wide_log2; i++) + register_memory_addr(it.first, addr_int + i); } } } for (auto it : children) - if (it.second->update_ph2()) { + if (it.second->update_ph2(gclk)) { dirty_children.insert(it.second); did_something = true; } @@ -622,7 +684,7 @@ struct SimInstance return did_something; } - void update_ph3() + void update_ph3(bool check_assertions) { for (auto &it : ff_database) { @@ -657,35 +719,51 @@ struct SimInstance } } - for (auto cell : formal_database) + if (check_assertions) { - string label = log_id(cell); - if (cell->attributes.count(ID::src)) - label = cell->attributes.at(ID::src).decode_string(); + for (auto cell : formal_database) + { + string label = log_id(cell); + if (cell->attributes.count(ID::src)) + label = cell->attributes.at(ID::src).decode_string(); - State a = get_state(cell->getPort(ID::A))[0]; - State en = get_state(cell->getPort(ID::EN))[0]; + State a = get_state(cell->getPort(ID::A))[0]; + State en = get_state(cell->getPort(ID::EN))[0]; - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) - log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) { + shared->triggered_assertions.emplace_back(shared->step, this, cell); + } + + if (cell->type == ID($cover) && en == State::S1 && a == State::S1) + log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assume) && en == State::S1 && a != State::S1) - log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assume) && en == State::S1 && a != State::S1) + log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assert) && en == State::S1 && a != State::S1) - log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assert) && en == State::S1 && a != State::S1) + log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + } } for (auto it : children) - it.second->update_ph3(); + it.second->update_ph3(check_assertions); } - void writeback(pool<Module*> &wbmods) + void set_initstate_outputs(State state) { - if (wbmods.count(module)) - log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module)); + for (auto cell : initstate_database) + set_state(cell->getPort(ID::Y), state); + for (auto child : children) + child.second->set_initstate_outputs(state); + } - wbmods.insert(module); + void writeback(pool<Module*> &wbmods) + { + if (!ff_database.empty() || !mem_database.empty()) { + if (wbmods.count(module)) + log_error("Instance %s of module %s is not unique: Writeback not possible. (Fix by running 'uniquify'.)\n", hiername().c_str(), log_id(module)); + wbmods.insert(module); + } for (auto wire : module->wires()) wire->attributes.erase(ID::init); @@ -737,9 +815,17 @@ struct SimInstance child.second->register_signals(id); } - void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int, bool)> register_signal) + void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, int, Wire*, int, bool)> 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<Wire*,bool> registers; for (auto cell : module->cells()) @@ -755,13 +841,83 @@ 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(), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); + for (auto name : hdlname) + exit_scope(); + } else + register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); + } + + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + Cell *cell = mdb.mem->cell; + + std::vector<std::string> hdlname; + std::string signal_name; + bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname); + + if (has_hdlname) { + hdlname = cell->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + signal_name = std::move(hdlname.back()); + hdlname.pop_back(); + for (auto name : hdlname) + enter_scope("\\" + name); + } else { + signal_name = log_id(memid); + } + + for (auto &trace_index : trace_mem.second) { + int output_id = trace_index.second.first; + int index = trace_index.first; + register_signal( + stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(), + mdb.mem->width, nullptr, output_id, true); + } + + if (has_hdlname) + for (auto name : hdlname) + exit_scope(); } 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_memory_addr(IdString memid, int addr) + { + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + int index = addr - mem.start_offset; + if (index < 0 || index >= mem.size) + return; + auto it = trace_mem_database.find(memid); + if (it != trace_mem_database.end() && it->second.count(index)) + return; + int output_id = shared->next_output_id++; + Const data; + if (!shared->output_data.empty()) { + auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr)); + if (init_it != trace_mem_init_database.end()) + data = init_it->second; + else + data = mem.get_init_data().extract(index * mem.width, mem.width); + shared->output_data.front().second.emplace(output_id, data); + } + trace_mem_database[memid].emplace(index, make_pair(output_id, data)); + } void register_output_step_values(std::map<int,Const> *data) @@ -779,6 +935,26 @@ struct SimInstance data->emplace(id, value); } + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + for (auto &trace_index : trace_mem.second) + { + int output_id = trace_index.second.first; + int index = trace_index.first; + + auto value = mdb.data.extract(index * mem.width, mem.width); + + if (trace_index.second.second == value) + continue; + + trace_index.second.second = value; + data->emplace(output_id, value); + } + } + for (auto child : children) child.second->register_output_step_values(data); } @@ -791,18 +967,6 @@ struct SimInstance std::string v = shared->fst->valueOf(item.second); did_something |= set_state(item.first, Const::from_string(v)); } - for (auto &it : ff_database) - { - ff_state_t &ff = it.second; - SigSpec dsig = it.second.data.sig_d; - Const value = get_state(dsig); - if (dsig.is_wire()) { - ff.past_d = value; - if (ff.data.has_aload) - ff.past_ad = value; - did_something |= true; - } - } for (auto cell : module->cells()) { if (cell->is_mem_cell()) { @@ -820,7 +984,7 @@ struct SimInstance return did_something; } - void addAdditionalInputs(std::map<Wire*,fstHandle> &inputs) + void addAdditionalInputs() { for (auto cell : module->cells()) { @@ -831,7 +995,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 +1006,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<int, std::pair<SigBit,bool>> bits, std::string values) @@ -920,6 +1098,7 @@ struct SimWorker : SimShared std::string timescale; std::string sim_filename; std::string map_filename; + std::string summary_filename; std::string scope; ~SimWorker() @@ -930,8 +1109,8 @@ struct SimWorker : SimShared void register_signals() { - int id = 1; - top->register_signals(id); + next_output_id = 1; + top->register_signals(top->shared->next_output_id); } void register_output_step(int t) @@ -961,8 +1140,11 @@ struct SimWorker : SimShared writer->write(use_signal); } - void update() + void update(bool gclk) { + if (gclk) + step += 1; + while (1) { if (debug) @@ -973,14 +1155,24 @@ struct SimWorker : SimShared if (debug) log("\n-- ph2 --\n"); - if (!top->update_ph2()) + if (!top->update_ph2(gclk)) break; } if (debug) log("\n-- ph3 --\n"); - top->update_ph3(); + top->update_ph3(gclk); + } + + void initialize_stable_past() + { + if (debug) + log("\n-- ph1 (initialize) --\n"); + top->update_ph1(); + if (debug) + log("\n-- ph3 (initialize) --\n"); + top->update_ph3(true); } void set_inports(pool<IdString> ports, State value) @@ -1013,7 +1205,7 @@ struct SimWorker : SimShared set_inports(clock, State::Sx); set_inports(clockn, State::Sx); - update(); + update(false); register_output_step(0); @@ -1026,7 +1218,7 @@ struct SimWorker : SimShared set_inports(clock, State::S0); set_inports(clockn, State::S1); - update(); + update(true); register_output_step(10*cycle + 5); if (debug) @@ -1042,7 +1234,7 @@ struct SimWorker : SimShared set_inports(resetn, State::S1); } - update(); + update(true); register_output_step(10*cycle + 10); } @@ -1095,18 +1287,17 @@ struct SimWorker : SimShared } SigMap sigmap(topmod); - std::map<Wire*,fstHandle> 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,18 +1343,15 @@ 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(); + initialize_stable_past(); initial = false; } if (did_something) - update(); + update(true); register_output_step(time); bool status = top->checkSignals(); @@ -1312,12 +1500,12 @@ struct SimWorker : SimShared set_inports(clock, State::S0); set_inports(clockn, State::S1); } - update(); + update(true); register_output_step(10*cycle); if (!multiclock && cycle) { set_inports(clock, State::S0); set_inports(clockn, State::S1); - update(); + update(true); register_output_step(10*cycle + 5); } cycle++; @@ -1389,12 +1577,12 @@ struct SimWorker : SimShared log("Simulating cycle %d.\n", cycle); set_inports(clock, State::S1); set_inports(clockn, State::S0); - update(); + update(true); register_output_step(10*cycle+0); if (!multiclock) { set_inports(clock, State::S0); set_inports(clockn, State::S1); - update(); + update(true); register_output_step(10*cycle+5); } cycle++; @@ -1458,6 +1646,242 @@ struct SimWorker : SimShared write_output_files(); } + struct FoundYWPath + { + SimInstance *instance; + Wire *wire; + IdString memid; + int addr; + }; + + struct YwHierarchy { + dict<IdPath, FoundYWPath> paths; + }; + + YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw) + { + YwHierarchy hierarchy; + pool<IdPath> paths; + dict<IdPath, pool<IdString>> mem_paths; + + for (auto &signal : yw.signals) + paths.insert(signal.path); + + for (auto &clock : yw.clocks) + paths.insert(clock.path); + + for (auto &path : paths) + if (path.has_address()) + mem_paths[path.prefix()].insert(path.back()); + + witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) { + if (item.cell != nullptr) + return instance->children.at(item.cell); + if (item.wire != nullptr) { + if (paths.count(path)) { + if (debug) + log("witness hierarchy: found wire %s\n", path.str().c_str()); + bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } else if (item.mem) { + auto it = mem_paths.find(path); + if (it != mem_paths.end()) { + if (debug) + log("witness hierarchy: found mem %s\n", path.str().c_str()); + IdPath word_path = path; + word_path.emplace_back(); + for (auto addr_part : it->second) { + word_path.back() = addr_part; + int addr; + word_path.get_address(addr); + if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size) + continue; + bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } + } + return instance; + }); + + for (auto &path : paths) + if (!hierarchy.paths.count(path)) + log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str()); + + dict<IdPath, dict<int, bool>> clock_inputs; + + for (auto &clock : yw.clocks) { + if (clock.is_negedge == clock.is_posedge) + continue; + clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge); + } + for (auto &signal : yw.signals) { + auto it = clock_inputs.find(signal.path); + if (it == clock_inputs.end()) + continue; + + for (auto &clock_input : it->second) { + int offset = clock_input.first; + if (offset >= signal.offset && (offset - signal.offset) < signal.width) { + int clock_bits_offset = signal.bits_offset + (offset - signal.offset); + + State expected = clock_input.second ? State::S0 : State::S1; + + for (int t = 0; t < GetSize(yw.steps); t++) { + if (yw.get_bits(t, clock_bits_offset, 1) != expected) + log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t); + } + } + } + } + // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file + + return hierarchy; + } + + void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t) + { + log_assert(t >= 0 && t < GetSize(yw.steps)); + + for (auto &signal : yw.signals) { + if (signal.init_only && t >= 1) + continue; + auto found_path_it = hierarchy.paths.find(signal.path); + if (found_path_it == hierarchy.paths.end()) + continue; + auto &found_path = found_path_it->second; + + Const value = yw.get_bits(t, signal.bits_offset, signal.width); + + if (debug) + log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value)); + + if (found_path.wire != nullptr) { + found_path.instance->set_state( + SigChunk(found_path.wire, signal.offset, signal.width), + value); + } else if (!found_path.memid.empty()) { + if (t >= 1) + found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + else + found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value); + found_path.instance->set_memory_state( + found_path.memid, found_path.addr, + value); + } + } + } + + void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge) + { + for (auto &clock : yw.clocks) { + if (clock.is_negedge == clock.is_posedge) + continue; + auto found_path_it = hierarchy.paths.find(clock.path); + if (found_path_it == hierarchy.paths.end()) + continue; + auto &found_path = found_path_it->second; + + if (found_path.wire != nullptr) { + found_path.instance->set_state( + SigChunk(found_path.wire, clock.offset, 1), + active_edge == clock.is_posedge ? State::S1 : State::S0); + } + } + } + + void run_cosim_yw_witness(Module *topmod, int append) + { + if (!clock.empty()) + log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n"); + if (!reset.empty()) + log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n"); + if (multiclock) + log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n"); + + ReadWitness yw(sim_filename); + + top = new SimInstance(this, scope, topmod); + register_signals(); + + YwHierarchy hierarchy = prepare_yw_hierarchy(yw); + + if (yw.steps.empty()) { + log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str()); + } else { + top->set_initstate_outputs(State::S1); + set_yw_state(yw, hierarchy, 0); + set_yw_clocks(yw, hierarchy, true); + initialize_stable_past(); + register_output_step(0); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5); + } + top->set_initstate_outputs(State::S0); + } + + for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++) + { + if (verbose) + log("Simulating cycle %d.\n", cycle); + if (cycle < GetSize(yw.steps)) + set_yw_state(yw, hierarchy, cycle); + set_yw_clocks(yw, hierarchy, true); + update(true); + register_output_step(10 * cycle); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5 + 10 * cycle); + } + } + + register_output_step(10 * (GetSize(yw.steps) + append)); + write_output_files(); + } + + void write_summary() + { + if (summary_filename.empty()) + return; + + PrettyJson json; + if (!json.write_to_file(summary_filename)) + log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno)); + + json.begin_object(); + json.entry("version", "Yosys sim summary"); + json.entry("generator", yosys_version_str); + json.entry("steps", step); + json.entry("top", log_id(top->module->name)); + json.name("assertions"); + json.begin_array(); + for (auto &assertion : triggered_assertions) { + json.begin_object(); + json.entry("step", assertion.step); + json.entry("type", log_id(assertion.cell->type)); + json.entry("path", assertion.instance->witness_full_path(assertion.cell)); + auto src = assertion.cell->get_string_attribute(ID::src); + if (!src.empty()) { + json.entry("src", src); + } + json.end_object(); + } + json.end_array(); + json.end_object(); + } + std::string define_signal(Wire *wire) { std::stringstream f; @@ -1702,7 +2126,17 @@ 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, int size, Wire *, int id, bool is_reg) { + if (use_signal.at(id)) { + // Works around gtkwave trying to parse everything past the last [ in a signal + // name. While the emitted range doesn't necessarily match the wire's range, + // this is consistent with the range gtkwave makes up if it doesn't find a + // range + std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string(); + vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str()); + + } + } ); vcdfile << stringf("$enddefinitions $end\n"); @@ -1760,11 +2194,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, int size, 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); - + fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size, + name, 0); mapping.emplace(id, fst_id); } ); @@ -1846,7 +2279,7 @@ struct AIWWriter : public OutputWriter worker->top->write_output_header( [](IdString) {}, []() {}, - [this](Wire *wire, int id, bool) { mapping[wire] = id; } + [this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; } ); std::map<int, Yosys::RTLIL::Const> current; @@ -1935,6 +2368,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"); @@ -1974,9 +2411,16 @@ struct SimPass : public Pass { log(" -w\n"); log(" writeback mode: use final simulation state as new init state\n"); log("\n"); - log(" -r\n"); - log(" read simulation results file (file formats supported: FST, VCD, AIW and WIT)\n"); - log(" VCD support requires vcd2fst external tool to be present\n"); + log(" -r <filename>\n"); + log(" read simulation or formal results file\n"); + log(" File formats supported: FST, VCD, AIW, WIT and .yw\n"); + log(" VCD support requires vcd2fst external tool to be present\n"); + log("\n"); + log(" -append <integer>\n"); + log(" number of extra clock cycles to simulate for a Yosys witness input\n"); + log("\n"); + log(" -summary <filename>\n"); + log(" write a JSON summary to the given file\n"); log("\n"); log(" -map <filename>\n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); @@ -2023,6 +2467,7 @@ struct SimPass : public Pass { { SimWorker worker; int numcycles = 20; + int append = 0; bool start_set = false, stop_set = false, at_set = false; log_header(design, "Executing SIM pass (simulate the circuit).\n"); @@ -2047,6 +2492,10 @@ struct SimPass : public Pass { worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(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; @@ -2102,12 +2551,22 @@ struct SimPass : public Pass { worker.sim_filename = sim_filename; continue; } + if (args[argidx] == "-append" && argidx+1 < args.size()) { + append = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-map" && argidx+1 < args.size()) { std::string map_filename = args[++argidx]; rewrite_filename(map_filename); worker.map_filename = map_filename; continue; } + if (args[argidx] == "-summary" && argidx+1 < args.size()) { + std::string summary_filename = args[++argidx]; + rewrite_filename(summary_filename); + worker.summary_filename = summary_filename; + continue; + } if (args[argidx] == "-scope" && argidx+1 < args.size()) { worker.scope = args[++argidx]; continue; @@ -2191,10 +2650,14 @@ struct SimPass : public Pass { worker.run_cosim_aiger_witness(top_mod); } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) { worker.run_cosim_btor2_witness(top_mod); + } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) { + worker.run_cosim_yw_witness(top_mod, append); } else { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } } + + worker.write_summary(); } } SimPass; @@ -2206,8 +2669,8 @@ struct Fst2TbPass : public Pass { log("\n"); log(" fst2tb [options] [top-level]\n"); log("\n"); - log("This command generates testbench for the circuit using the given top-level module\n"); - log("and simulus signal from FST file\n"); + log("This command generates testbench for the circuit using the given top-level\n"); + log("module and simulus signal from FST file\n"); log("\n"); log(" -tb <name>\n"); log(" generated testbench name.\n"); |