diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 36 | ||||
| -rw-r--r-- | kernel/ff.cc | 13 | ||||
| -rw-r--r-- | kernel/ff.h | 2 | ||||
| -rw-r--r-- | kernel/mem.h | 2 | ||||
| -rw-r--r-- | passes/opt/Makefile.inc | 1 | ||||
| -rw-r--r-- | passes/opt/opt_ffinv.cc | 258 | ||||
| -rw-r--r-- | passes/proc/Makefile.inc | 1 | ||||
| -rw-r--r-- | passes/proc/proc.cc | 11 | ||||
| -rw-r--r-- | passes/proc/proc_rom.cc | 227 | ||||
| -rw-r--r-- | tests/proc/proc_rom.ys | 43 | ||||
| -rw-r--r-- | tests/sva/sva_value_change_changed_wide.sv | 22 | ||||
| -rw-r--r-- | tests/sva/sva_value_change_sim.sv | 23 |
13 files changed, 627 insertions, 14 deletions
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.17+5 +YOSYS_VER := 0.17+9 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index fd8bbc3f1..b130edbdc 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1527,23 +1527,45 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma log_assert(inst->Input1Size() == inst->OutputSize()); - SigSpec sig_d, sig_q, sig_o; - sig_q = module->addWire(new_verific_id(inst), inst->Input1Size()); + unsigned width = inst->Input1Size(); - for (int i = int(inst->Input1Size())-1; i >= 0; i--){ + SigSpec sig_d, sig_dx, sig_qx, sig_o, sig_ox; + sig_dx = module->addWire(new_verific_id(inst), width * 2); + sig_qx = module->addWire(new_verific_id(inst), width * 2); + sig_ox = module->addWire(new_verific_id(inst), width * 2); + + for (int i = int(width)-1; i >= 0; i--){ sig_d.append(net_map_at(inst->GetInput1Bit(i))); sig_o.append(net_map_at(inst->GetOutputBit(i))); } if (verific_verbose) { + for (unsigned i = 0; i < width; i++) { + log(" NEX with A=%s, B=0, Y=%s.\n", + log_signal(sig_d[i]), log_signal(sig_dx[i])); + log(" EQX with A=%s, B=1, Y=%s.\n", + log_signal(sig_d[i]), log_signal(sig_dx[i + width])); + } log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", - log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_ox)); + log(" AND with A=%s, B=%s, Y=%s.\n", + log_signal(sig_ox.extract(0, width)), log_signal(sig_ox.extract(width, width)), log_signal(sig_o)); } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); + for (unsigned i = 0; i < width; i++) { + module->addNex(new_verific_id(inst), sig_d[i], State::S0, sig_dx[i]); + module->addEqx(new_verific_id(inst), sig_d[i], State::S1, sig_dx[i + width]); + } + + Const qx_init = Const(State::S1, width); + qx_init.bits.resize(2 * width, State::S0); + + clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, qx_init); + module->addXnor(new_verific_id(inst), sig_dx, sig_qx, sig_ox); + + module->addAnd(new_verific_id(inst), sig_ox.extract(0, width), sig_ox.extract(width, width), sig_o); if (!mode_keep) continue; diff --git a/kernel/ff.cc b/kernel/ff.cc index c43482bd2..b0f1a924f 100644 --- a/kernel/ff.cc +++ b/kernel/ff.cc @@ -669,14 +669,12 @@ namespace { } } -void FfData::flip_bits(const pool<int> &bits) { +void FfData::flip_rst_bits(const pool<int> &bits) { if (!bits.size()) return; remove_init(); - Wire *new_q = module->addWire(NEW_ID, width); - for (auto bit: bits) { if (has_arst) val_arst[bit] = invert(val_arst[bit]); @@ -684,6 +682,15 @@ void FfData::flip_bits(const pool<int> &bits) { val_srst[bit] = invert(val_srst[bit]); val_init[bit] = invert(val_init[bit]); } +} + +void FfData::flip_bits(const pool<int> &bits) { + if (!bits.size()) + return; + + flip_rst_bits(bits); + + Wire *new_q = module->addWire(NEW_ID, width); if (has_sr && cell) { log_warning("Flipping D/Q/init and inserting priority fixup to legalize %s.%s [%s].\n", log_id(module->name), log_id(cell->name), log_id(cell->type)); diff --git a/kernel/ff.h b/kernel/ff.h index 5a629d5dd..41721b4a1 100644 --- a/kernel/ff.h +++ b/kernel/ff.h @@ -209,6 +209,8 @@ struct FfData { // inputs and output, flip the corresponding init/reset bits, swap clr/set // inputs with proper priority fix. void flip_bits(const pool<int> &bits); + + void flip_rst_bits(const pool<int> &bits); }; YOSYS_NAMESPACE_END diff --git a/kernel/mem.h b/kernel/mem.h index ae87b1285..8c484274c 100644 --- a/kernel/mem.h +++ b/kernel/mem.h @@ -46,7 +46,7 @@ struct MemRd : RTLIL::AttrObject { std::vector<bool> collision_x_mask; SigSpec clk, en, arst, srst, addr, data; - MemRd() : removed(false), cell(nullptr) {} + MemRd() : removed(false), cell(nullptr), wide_log2(0), clk_enable(false), clk_polarity(true), ce_over_srst(false), clk(State::Sx), en(State::S1), arst(State::S0), srst(State::S0) {} // Returns the address of given subword index accessed by this port. SigSpec sub_addr(int sub) { diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc index 4e52ad8da..76bf8a84e 100644 --- a/passes/opt/Makefile.inc +++ b/passes/opt/Makefile.inc @@ -19,6 +19,7 @@ OBJS += passes/opt/opt_demorgan.o OBJS += passes/opt/rmports.o OBJS += passes/opt/opt_lut.o OBJS += passes/opt/opt_lut_ins.o +OBJS += passes/opt/opt_ffinv.o OBJS += passes/opt/pmux2shiftx.o OBJS += passes/opt/muxpack.o endif diff --git a/passes/opt/opt_ffinv.cc b/passes/opt/opt_ffinv.cc new file mode 100644 index 000000000..fd76dd2be --- /dev/null +++ b/passes/opt/opt_ffinv.cc @@ -0,0 +1,258 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Marcelina Kościelnicka <mwk@0x04.net> + * + * 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/modtools.h" +#include "kernel/ffinit.h" +#include "kernel/ff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct OptFfInvWorker +{ + int count = 0; + RTLIL::Module *module; + ModIndex index; + FfInitVals initvals; + + // Case 1: + // - FF is driven by inverter + // - ... which has no other users + // - all users of FF are LUTs + bool push_d_inv(FfData &ff) { + if (index.query_is_input(ff.sig_d)) + return false; + if (index.query_is_output(ff.sig_d)) + return false; + auto d_ports = index.query_ports(ff.sig_d); + if (d_ports.size() != 2) + return false; + Cell *d_inv = nullptr; + for (auto &port: d_ports) { + if (port.cell == ff.cell && port.port == ID::D) + continue; + if (port.port != ID::Y) + return false; + if (port.cell->type.in(ID($not), ID($_NOT_))) { + // OK + } else if (port.cell->type.in(ID($lut))) { + if (port.cell->getParam(ID::WIDTH) != 1) + return false; + if (port.cell->getParam(ID::LUT).as_int() != 1) + return false; + } else { + return false; + } + log_assert(d_inv == nullptr); + d_inv = port.cell; + } + + if (index.query_is_output(ff.sig_q)) + return false; + auto q_ports = index.query_ports(ff.sig_q); + pool<Cell *> q_luts; + for (auto &port: q_ports) { + if (port.cell == ff.cell && port.port == ID::Q) + continue; + if (port.port != ID::A) + return false; + if (!port.cell->type.in(ID($not), ID($_NOT_), ID($lut))) + return false; + q_luts.insert(port.cell); + } + + ff.flip_rst_bits({0}); + ff.sig_d = d_inv->getPort(ID::A); + + for (Cell *lut: q_luts) { + if (lut->type == ID($lut)) { + int flip_mask = 0; + SigSpec sig_a = lut->getPort(ID::A); + for (int i = 0; i < GetSize(sig_a); i++) { + if (index.sigmap(sig_a[i]) == index.sigmap(ff.sig_q)) { + flip_mask |= 1 << i; + } + } + Const mask = lut->getParam(ID::LUT); + Const new_mask; + for (int j = 0; j < (1 << GetSize(sig_a)); j++) { + new_mask.bits.push_back(mask.bits[j ^ flip_mask]); + } + if (GetSize(sig_a) == 1 && new_mask.as_int() == 2) { + module->connect(lut->getPort(ID::Y), ff.sig_q); + module->remove(lut); + } else { + lut->setParam(ID::LUT, new_mask); + } + } else { + // it was an inverter + module->connect(lut->getPort(ID::Y), ff.sig_q); + module->remove(lut); + } + } + + ff.emit(); + return true; + } + + // Case 2: + // - FF is driven by LUT + // - ... which has no other users + // - FF has one user + // - ... which is an inverter + bool push_q_inv(FfData &ff) { + if (index.query_is_input(ff.sig_d)) + return false; + if (index.query_is_output(ff.sig_d)) + return false; + + Cell *d_lut = nullptr; + auto d_ports = index.query_ports(ff.sig_d); + if (d_ports.size() != 2) + return false; + for (auto &port: d_ports) { + if (port.cell == ff.cell && port.port == ID::D) + continue; + if (port.port != ID::Y) + return false; + if (!port.cell->type.in(ID($not), ID($_NOT_), ID($lut))) + return false; + log_assert(d_lut == nullptr); + d_lut = port.cell; + } + + if (index.query_is_output(ff.sig_q)) + return false; + auto q_ports = index.query_ports(ff.sig_q); + if (q_ports.size() != 2) + return false; + Cell *q_inv = nullptr; + for (auto &port: q_ports) { + if (port.cell == ff.cell && port.port == ID::Q) + continue; + if (port.port != ID::A) + return false; + if (port.cell->type.in(ID($not), ID($_NOT_))) { + // OK + } else if (port.cell->type.in(ID($lut))) { + if (port.cell->getParam(ID::WIDTH) != 1) + return false; + if (port.cell->getParam(ID::LUT).as_int() != 1) + return false; + } else { + return false; + } + log_assert(q_inv == nullptr); + q_inv = port.cell; + } + + ff.flip_rst_bits({0}); + ff.sig_q = q_inv->getPort(ID::Y); + module->remove(q_inv); + + if (d_lut->type == ID($lut)) { + Const mask = d_lut->getParam(ID::LUT); + Const new_mask; + for (int i = 0; i < GetSize(mask); i++) { + if (mask.bits[i] == State::S0) + new_mask.bits.push_back(State::S1); + else + new_mask.bits.push_back(State::S0); + } + d_lut->setParam(ID::LUT, new_mask); + if (d_lut->getParam(ID::WIDTH) == 1 && new_mask.as_int() == 2) { + module->connect(ff.sig_d, d_lut->getPort(ID::A)); + module->remove(d_lut); + } + } else { + // it was an inverter + module->connect(ff.sig_d, d_lut->getPort(ID::A)); + module->remove(d_lut); + } + + ff.emit(); + return true; + } + + OptFfInvWorker(RTLIL::Module *module) : + module(module), index(module), initvals(&index.sigmap, module) + { + log("Discovering LUTs.\n"); + + for (Cell *cell : module->selected_cells()) { + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; + + FfData ff(&initvals, cell); + if (ff.has_sr) + continue; + if (!ff.has_clk) + continue; + if (ff.has_aload) + continue; + if (ff.width != 1) + continue; + + if (push_d_inv(ff)) { + count++; + } else if (push_q_inv(ff)) { + count++; + } + } + } +}; + +struct OptFfInvPass : public Pass { + OptFfInvPass() : Pass("opt_ffinv", "push inverters through FFs") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" opt_ffinv [selection]\n"); + log("\n"); + log("This pass pushes inverters to the other side of a FF when they can be merged\n"); + log("into LUTs on the other side.\n"); + log("\n"); + } + void execute(std::vector<std::string> args, RTLIL::Design *design) override + { + log_header(design, "Executing OPT_FFINV pass (push inverters through FFs).\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + break; + } + extra_args(args, argidx, design); + + int total_count = 0; + for (auto module : design->selected_modules()) + { + OptFfInvWorker worker(module); + total_count += worker.count; + } + if (total_count) + design->scratchpad_set_bool("opt.did_something", true); + log("Pushed %d inverters.\n", total_count); + } +} OptFfInvPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/proc/Makefile.inc b/passes/proc/Makefile.inc index 50244bf33..21e169a34 100644 --- a/passes/proc/Makefile.inc +++ b/passes/proc/Makefile.inc @@ -5,6 +5,7 @@ OBJS += passes/proc/proc_clean.o OBJS += passes/proc/proc_rmdead.o OBJS += passes/proc/proc_init.o OBJS += passes/proc/proc_arst.o +OBJS += passes/proc/proc_rom.o OBJS += passes/proc/proc_mux.o OBJS += passes/proc/proc_dlatch.o OBJS += passes/proc/proc_dff.o diff --git a/passes/proc/proc.cc b/passes/proc/proc.cc index d7aac57b6..c18651d5e 100644 --- a/passes/proc/proc.cc +++ b/passes/proc/proc.cc @@ -40,6 +40,7 @@ struct ProcPass : public Pass { log(" proc_prune\n"); log(" proc_init\n"); log(" proc_arst\n"); + log(" proc_rom\n"); log(" proc_mux\n"); log(" proc_dlatch\n"); log(" proc_dff\n"); @@ -55,6 +56,9 @@ struct ProcPass : public Pass { log(" -nomux\n"); log(" Will omit the proc_mux pass.\n"); log("\n"); + log(" -norom\n"); + log(" Will omit the proc_rom pass.\n"); + log("\n"); log(" -global_arst [!]<netname>\n"); log(" This option is passed through to proc_arst.\n"); log("\n"); @@ -72,6 +76,7 @@ struct ProcPass : public Pass { bool ifxmode = false; bool nomux = false; bool noopt = false; + bool norom = false; log_header(design, "Executing PROC pass (convert processes to netlists).\n"); log_push(); @@ -95,6 +100,10 @@ struct ProcPass : public Pass { noopt = true; continue; } + if (args[argidx] == "-norom") { + norom = true; + continue; + } break; } extra_args(args, argidx, design); @@ -108,6 +117,8 @@ struct ProcPass : public Pass { Pass::call(design, "proc_arst"); else Pass::call(design, "proc_arst -global_arst " + global_arst); + if (!norom) + Pass::call(design, "proc_rom"); if (!nomux) Pass::call(design, ifxmode ? "proc_mux -ifx" : "proc_mux"); Pass::call(design, "proc_dlatch"); diff --git a/passes/proc/proc_rom.cc b/passes/proc/proc_rom.cc new file mode 100644 index 000000000..4fd611518 --- /dev/null +++ b/passes/proc/proc_rom.cc @@ -0,0 +1,227 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Marcelina Kościelnicka <mwk@0x04.net> + * + * 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/register.h" +#include "kernel/sigtools.h" +#include "kernel/log.h" +#include "kernel/mem.h" +#include <stdlib.h> +#include <stdio.h> + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct RomWorker +{ + RTLIL::Module *module; + SigMap sigmap; + + int count = 0; + + RomWorker(RTLIL::Module *mod) : module(mod), sigmap(mod) {} + + void do_switch(RTLIL::SwitchRule *sw) + { + for (auto cs : sw->cases) { + do_case(cs); + } + + if (sw->cases.empty()) { + log_debug("rejecting switch: no cases\n"); + return; + } + if (GetSize(sw->signal) > 30) { + log_debug("rejecting switch: address too wide\n"); + return; + } + + // A switch can be converted into ROM when: + // + // 1. No case contains a nested switch + // 2. All cases have the same set of assigned signals + // 3. All right-hand values in cases are constants + // 4. All compare values used in cases are fully-defined constants + // 5. The cases must cover all possible values (possibly by using default case) + + SigSpec lhs; + dict<SigBit, int> lhs_lookup; + for (auto &it: sw->cases[0]->actions) { + for (auto bit: it.first) { + if (!lhs_lookup.count(bit)) { + lhs_lookup[bit] = GetSize(lhs); + lhs.append(bit); + } + } + } + + dict<int, Const> vals; + Const default_val; + bool got_default = false; + for (auto cs : sw->cases) { + if (!cs->switches.empty()) { + log_debug("rejecting switch: has nested switches\n"); + return; + } + Const val = Const(State::Sm, GetSize(lhs)); + for (auto &it: cs->actions) { + if (!it.second.is_fully_const()) { + log_debug("rejecting switch: rhs not const\n"); + return; + } + for (int i = 0; i < GetSize(it.first); i++) { + auto it2 = lhs_lookup.find(it.first[i]); + if (it2 == lhs_lookup.end()) { + log_debug("rejecting switch: lhs not uniform\n"); + return; + } + val[it2->second] = it.second[i].data; + } + } + for (auto bit: val.bits) { + if (bit == State::Sm) { + log_debug("rejecting switch: lhs not uniform\n"); + return; + } + } + + for (auto &addr: cs->compare) { + if (!addr.is_fully_def()) { + log_debug("rejecting switch: case value has undef bits\n"); + return; + } + int a = addr.as_int(); + if (vals.count(a)) + continue; + vals[a] = val; + } + if (cs->compare.empty()) { + default_val = val; + got_default = true; + break; + } + } + int total = 1 << GetSize(sw->signal); + if (!got_default && GetSize(vals) != total) { + log_debug("rejecting switch: not all values are covered\n"); + return; + } + + // TODO: better density heuristic? + if (GetSize(vals) < 8) { + log_debug("rejecting switch: not enough values\n"); + return; + } + if (total / GetSize(vals) > 4) { + log_debug("rejecting switch: not enough density\n"); + return; + } + + // Ok, let's do it. + SigSpec rdata = module->addWire(NEW_ID, GetSize(lhs)); + Mem mem(module, NEW_ID, GetSize(lhs), 0, total); + mem.attributes = sw->attributes; + + Const init_data; + for (int i = 0; i < total; i++) { + auto it = vals.find(i); + if (it == vals.end()) { + log_assert(got_default); + for (auto bit: default_val.bits) + init_data.bits.push_back(bit); + } else { + for (auto bit: it->second.bits) + init_data.bits.push_back(bit); + } + } + + MemInit init; + init.addr = 0; + init.data = init_data; + init.en = Const(State::S1, GetSize(lhs)); + mem.inits.push_back(std::move(init)); + + MemRd rd; + rd.addr = sw->signal; + rd.data = rdata; + rd.init_value = Const(State::Sx, GetSize(lhs)); + rd.arst_value = Const(State::Sx, GetSize(lhs)); + rd.srst_value = Const(State::Sx, GetSize(lhs)); + mem.rd_ports.push_back(std::move(rd)); + + mem.emit(); + for (auto cs: sw->cases) + delete cs; + sw->cases.clear(); + sw->signal = SigSpec(); + RTLIL::CaseRule *cs = new RTLIL::CaseRule; + cs->actions.push_back(SigSig(lhs, rdata)); + sw->cases.push_back(cs); + + count += 1; + } + + void do_case(RTLIL::CaseRule *cs) + { + for (auto sw: cs->switches) { + do_switch(sw); + } + } + + void do_process(RTLIL::Process *pr) + { + do_case(&pr->root_case); + } +}; + +struct ProcRomPass : public Pass { + ProcRomPass() : Pass("proc_rom", "convert switches to ROMs") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" proc_rom [selection]\n"); + log("\n"); + log("This pass converts switches into read-only memories when appropriate.\n"); + log("\n"); + } + void execute(std::vector<std::string> args, RTLIL::Design *design) override + { + int total_count = 0; + log_header(design, "Executing PROC_ROM pass (convert switches to ROMs).\n"); + + extra_args(args, 1, design); + + for (auto mod : design->modules()) { + if (!design->selected(mod)) + continue; + RomWorker worker(mod); + for (auto &proc_it : mod->processes) { + if (!design->selected(mod, proc_it.second)) + continue; + worker.do_process(proc_it.second); + } + total_count += worker.count; + } + + log("Converted %d switch%s.\n", + total_count, total_count == 1 ? "" : "es"); + } +} ProcRomPass; + +PRIVATE_NAMESPACE_END diff --git a/tests/proc/proc_rom.ys b/tests/proc/proc_rom.ys new file mode 100644 index 000000000..c854e732f --- /dev/null +++ b/tests/proc/proc_rom.ys @@ -0,0 +1,43 @@ +read_verilog << EOT + +module top(input [3:0] a, input en, output [7:0] d); + +always @* + if (en) + case(a) + 4'h0: d <= 8'h12; + 4'h1: d <= 8'h34; + 4'h2: d <= 8'h56; + 4'h3: d <= 8'h78; + 4'h4: d <= 8'h9a; + 4'h5: d <= 8'hbc; + 4'h6: d <= 8'hde; + 4'h7: d <= 8'hff; + 4'h8: d <= 8'h61; + 4'h9: d <= 8'h49; + 4'ha: d <= 8'h36; + 4'hb: d <= 8'h81; + 4'hc: d <= 8'h8c; + 4'hd: d <= 8'ha9; + 4'he: d <= 8'h99; + 4'hf: d <= 8'h51; + endcase + else + d <= 0; + +endmodule + +EOT + +hierarchy -auto-top + +design -save orig +proc +memory +opt_dff +design -stash postopt +design -load orig +proc -norom +design -stash preopt + +equiv_opt -assert -run prepare: dummy diff --git a/tests/sva/sva_value_change_changed_wide.sv b/tests/sva/sva_value_change_changed_wide.sv new file mode 100644 index 000000000..c9147c4f3 --- /dev/null +++ b/tests/sva/sva_value_change_changed_wide.sv @@ -0,0 +1,22 @@ +module top ( + input clk, + input [2:0] a, + input [2:0] b +); + default clocking @(posedge clk); endclocking + + assert property ( + $changed(a) + ); + + assert property ( + $changed(b) == ($changed(b[0]) || $changed(b[1]) || $changed(b[2])) + ); + +`ifndef FAIL + assume property ( + a !== 'x ##1 $changed(a) + ); +`endif + +endmodule diff --git a/tests/sva/sva_value_change_sim.sv b/tests/sva/sva_value_change_sim.sv index 80ff309cd..92fe30b23 100644 --- a/tests/sva/sva_value_change_sim.sv +++ b/tests/sva/sva_value_change_sim.sv @@ -7,6 +7,8 @@ reg [7:0] counter = 0; reg a = 0; reg b = 1; reg c; +reg [2:0] wide_a = 3'b10x; +reg [2:0] wide_b = 'x; wire a_fell; assign a_fell = $fell(a, @(posedge clk)); wire a_rose; assign a_rose = $rose(a, @(posedge clk)); @@ -20,6 +22,9 @@ wire c_fell; assign c_fell = $fell(c, @(posedge clk)); wire c_rose; assign c_rose = $rose(c, @(posedge clk)); wire c_stable; assign c_stable = $stable(c, @(posedge clk)); +wire wide_a_stable; assign wide_a_stable = $stable(wide_a, @(posedge clk)); +wire wide_b_stable; assign wide_b_stable = $stable(wide_b, @(posedge clk)); + always @(posedge clk) begin counter <= counter + 1; @@ -28,13 +33,20 @@ always @(posedge clk) begin assert property ( $fell(a) && !$rose(a) && !$stable(a)); assert property (!$fell(b) && $rose(b) && !$stable(b)); assert property (!$fell(c) && !$rose(c) && $stable(c)); + assert property (!$stable(wide_a)); + assert property ($stable(wide_b)); a <= 1; b <= 1; c <= 1; end - 1: begin a <= 0; b <= 1; c <= 'x; end + 1: begin + a <= 0; b <= 1; c <= 'x; + wide_a <= 3'b101; wide_b <= 3'bxx0; + end 2: begin assert property ( $fell(a) && !$rose(a) && !$stable(a)); assert property (!$fell(b) && !$rose(b) && $stable(b)); assert property (!$fell(c) && !$rose(c) && !$stable(c)); + assert property (!$stable(wide_a)); + assert property (!$stable(wide_b)); a <= 0; b <= 0; c <= 0; end 3: begin a <= 0; b <= 1; c <= 'x; end @@ -42,9 +54,16 @@ always @(posedge clk) begin assert property (!$fell(a) && !$rose(a) && $stable(a)); assert property (!$fell(b) && $rose(b) && !$stable(b)); assert property (!$fell(c) && !$rose(c) && !$stable(c)); + assert property ($stable(wide_a)); + assert property ($stable(wide_b)); a <= 'x; b <= 'x; c <= 'x; + wide_a <= 'x; wide_b <= 'x; + end + 5: begin + a <= 0; b <= 1; c <= 'x; + wide_a <= 3'b10x; wide_b <= 'x; + counter <= 0; end - 5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end endcase; end |