Now calls Tcl_Init after creating the interp, fixes clock format.
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
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;
}
}
-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]);
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));
// 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
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) {
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
--- /dev/null
+/*
+ * 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
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
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");
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");
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();
noopt = true;
continue;
}
+ if (args[argidx] == "-norom") {
+ norom = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
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");
--- /dev/null
+/*
+ * 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
--- /dev/null
+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
--- /dev/null
+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
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));
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;
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
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
projects / yosys.git / commitdiff