aboutsummaryrefslogtreecommitdiffstats
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/calc.cc60
-rw-r--r--kernel/celledges.h4
-rw-r--r--kernel/celltypes.h40
-rw-r--r--kernel/constids.inc4
-rw-r--r--kernel/ff.h486
-rw-r--r--kernel/ffinit.h141
-rw-r--r--kernel/hashlib.h2
-rw-r--r--kernel/log.cc2
-rw-r--r--kernel/log.h37
-rw-r--r--kernel/macc.h2
-rw-r--r--kernel/modtools.h8
-rw-r--r--kernel/register.cc10
-rw-r--r--kernel/register.h12
-rw-r--r--kernel/rtlil.cc502
-rw-r--r--kernel/rtlil.h55
-rw-r--r--kernel/satgen.cc1239
-rw-r--r--kernel/satgen.h1178
-rw-r--r--kernel/yosys.cc18
-rw-r--r--kernel/yosys.h27
19 files changed, 2508 insertions, 1319 deletions
diff --git a/kernel/calc.cc b/kernel/calc.cc
index ae18809d3..d54ccbc10 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -275,10 +275,15 @@ RTLIL::Const RTLIL::const_logic_or(const RTLIL::Const &arg1, const RTLIL::Const
return result;
}
-static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool sign_ext, int direction, int result_len)
+// Shift `arg1` by `arg2` bits.
+// If `direction` is +1, `arg1` is shifted right by `arg2` bits; if `direction` is -1, `arg1` is shifted left by `arg2` bits.
+// If `signed2` is true, `arg2` is interpreted as a signed integer; a negative `arg2` will cause a shift in the opposite direction.
+// Any required bits outside the bounds of `arg1` are padded with `vacant_bits` unless `sign_ext` is true, in which case any bits outside the left
+// bounds are filled with the leftmost bit of `arg1` (arithmetic shift).
+static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool sign_ext, bool signed2, int direction, int result_len, RTLIL::State vacant_bits = RTLIL::State::S0)
{
int undef_bit_pos = -1;
- BigInteger offset = const2big(arg2, false, undef_bit_pos) * direction;
+ BigInteger offset = const2big(arg2, signed2, undef_bit_pos) * direction;
if (result_len < 0)
result_len = arg1.bits.size();
@@ -290,9 +295,9 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co
for (int i = 0; i < result_len; i++) {
BigInteger pos = BigInteger(i) + offset;
if (pos < 0)
- result.bits[i] = RTLIL::State::S0;
+ result.bits[i] = vacant_bits;
else if (pos >= BigInteger(int(arg1.bits.size())))
- result.bits[i] = sign_ext ? arg1.bits.back() : RTLIL::State::S0;
+ result.bits[i] = sign_ext ? arg1.bits.back() : vacant_bits;
else
result.bits[i] = arg1.bits[pos.toInt()];
}
@@ -304,61 +309,36 @@ RTLIL::Const RTLIL::const_shl(const RTLIL::Const &arg1, const RTLIL::Const &arg2
{
RTLIL::Const arg1_ext = arg1;
extend_u0(arg1_ext, result_len, signed1);
- return const_shift_worker(arg1_ext, arg2, false, -1, result_len);
+ return const_shift_worker(arg1_ext, arg2, false, false, -1, result_len);
}
RTLIL::Const RTLIL::const_shr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
RTLIL::Const arg1_ext = arg1;
extend_u0(arg1_ext, max(result_len, GetSize(arg1)), signed1);
- return const_shift_worker(arg1_ext, arg2, false, +1, result_len);
-}
-
-RTLIL::Const RTLIL::const_sshl(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
-{
- if (!signed1)
- return const_shl(arg1, arg2, signed1, signed2, result_len);
- return const_shift_worker(arg1, arg2, true, -1, result_len);
+ return const_shift_worker(arg1_ext, arg2, false, false, +1, result_len);
}
-RTLIL::Const RTLIL::const_sshr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+RTLIL::Const RTLIL::const_sshl(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
- if (!signed1)
- return const_shr(arg1, arg2, signed1, signed2, result_len);
- return const_shift_worker(arg1, arg2, true, +1, result_len);
+ return const_shift_worker(arg1, arg2, signed1, false, -1, result_len);
}
-static RTLIL::Const const_shift_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool, bool signed2, int result_len, RTLIL::State other_bits)
+RTLIL::Const RTLIL::const_sshr(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool, int result_len)
{
- int undef_bit_pos = -1;
- BigInteger offset = const2big(arg2, signed2, undef_bit_pos);
-
- if (result_len < 0)
- result_len = arg1.bits.size();
-
- RTLIL::Const result(RTLIL::State::Sx, result_len);
- if (undef_bit_pos >= 0)
- return result;
-
- for (int i = 0; i < result_len; i++) {
- BigInteger pos = BigInteger(i) + offset;
- if (pos < 0 || pos >= BigInteger(int(arg1.bits.size())))
- result.bits[i] = other_bits;
- else
- result.bits[i] = arg1.bits[pos.toInt()];
- }
-
- return result;
+ return const_shift_worker(arg1, arg2, signed1, false, +1, result_len);
}
RTLIL::Const RTLIL::const_shift(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
{
- return const_shift_shiftx(arg1, arg2, signed1, signed2, result_len, RTLIL::State::S0);
+ RTLIL::Const arg1_ext = arg1;
+ extend_u0(arg1_ext, max(result_len, GetSize(arg1)), signed1);
+ return const_shift_worker(arg1_ext, arg2, false, signed2, +1, result_len);
}
-RTLIL::Const RTLIL::const_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+RTLIL::Const RTLIL::const_shiftx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool, bool signed2, int result_len)
{
- return const_shift_shiftx(arg1, arg2, signed1, signed2, result_len, RTLIL::State::Sx);
+ return const_shift_worker(arg1, arg2, false, signed2, +1, result_len, RTLIL::State::Sx);
}
RTLIL::Const RTLIL::const_lt(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
diff --git a/kernel/celledges.h b/kernel/celledges.h
index 2cc297cb2..d105e4009 100644
--- a/kernel/celledges.h
+++ b/kernel/celledges.h
@@ -38,7 +38,7 @@ struct FwdCellEdgesDatabase : AbstractCellEdgesDatabase
dict<SigBit, pool<SigBit>> db;
FwdCellEdgesDatabase(SigMap &sigmap) : sigmap(sigmap) { }
- void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) YS_OVERRIDE {
+ void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) override {
SigBit from_sigbit = sigmap(cell->getPort(from_port)[from_bit]);
SigBit to_sigbit = sigmap(cell->getPort(to_port)[to_bit]);
db[from_sigbit].insert(to_sigbit);
@@ -51,7 +51,7 @@ struct RevCellEdgesDatabase : AbstractCellEdgesDatabase
dict<SigBit, pool<SigBit>> db;
RevCellEdgesDatabase(SigMap &sigmap) : sigmap(sigmap) { }
- void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) YS_OVERRIDE {
+ void add_edge(RTLIL::Cell *cell, RTLIL::IdString from_port, int from_bit, RTLIL::IdString to_port, int to_bit, int) override {
SigBit from_sigbit = sigmap(cell->getPort(from_port)[from_bit]);
SigBit to_sigbit = sigmap(cell->getPort(to_port)[to_bit]);
db[to_sigbit].insert(from_sigbit);
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index db54436cb..944cb301a 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -139,8 +139,14 @@ struct CellTypes
setup_type(ID($dff), {ID::CLK, ID::D}, {ID::Q});
setup_type(ID($dffe), {ID::CLK, ID::EN, ID::D}, {ID::Q});
setup_type(ID($dffsr), {ID::CLK, ID::SET, ID::CLR, ID::D}, {ID::Q});
+ setup_type(ID($dffsre), {ID::CLK, ID::SET, ID::CLR, ID::D, ID::EN}, {ID::Q});
setup_type(ID($adff), {ID::CLK, ID::ARST, ID::D}, {ID::Q});
+ setup_type(ID($adffe), {ID::CLK, ID::ARST, ID::D, ID::EN}, {ID::Q});
+ setup_type(ID($sdff), {ID::CLK, ID::SRST, ID::D}, {ID::Q});
+ setup_type(ID($sdffe), {ID::CLK, ID::SRST, ID::D, ID::EN}, {ID::Q});
+ setup_type(ID($sdffce), {ID::CLK, ID::SRST, ID::D, ID::EN}, {ID::Q});
setup_type(ID($dlatch), {ID::EN, ID::D}, {ID::Q});
+ setup_type(ID($adlatch), {ID::EN, ID::D, ID::ARST}, {ID::Q});
setup_type(ID($dlatchsr), {ID::EN, ID::SET, ID::CLR, ID::D}, {ID::Q});
}
@@ -210,14 +216,48 @@ struct CellTypes
for (auto c1 : list_np)
for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_DFFE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
for (auto c3 : list_np)
setup_type(stringf("$_DFFSR_%c%c%c_", c1, c2, c3), {ID::C, ID::S, ID::R, ID::D}, {ID::Q});
for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_np)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_DFFSRE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::S, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ setup_type(stringf("$_SDFF_%c%c%c_", c1, c2, c3), {ID::C, ID::R, ID::D}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_SDFFE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ for (auto c4 : list_np)
+ setup_type(stringf("$_SDFFCE_%c%c%c%c_", c1, c2, c3, c4), {ID::C, ID::R, ID::D, ID::E}, {ID::Q});
+
+ for (auto c1 : list_np)
setup_type(stringf("$_DLATCH_%c_", c1), {ID::E, ID::D}, {ID::Q});
for (auto c1 : list_np)
for (auto c2 : list_np)
+ for (auto c3 : list_01)
+ setup_type(stringf("$_DLATCH_%c%c%c_", c1, c2, c3), {ID::E, ID::R, ID::D}, {ID::Q});
+
+ for (auto c1 : list_np)
+ for (auto c2 : list_np)
for (auto c3 : list_np)
setup_type(stringf("$_DLATCHSR_%c%c%c_", c1, c2, c3), {ID::E, ID::S, ID::R, ID::D}, {ID::Q});
}
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 383d7c615..3c2ff9beb 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -158,6 +158,9 @@ X(SRC_EN)
X(SRC_PEN)
X(SRC_POL)
X(SRC_WIDTH)
+X(SRST)
+X(SRST_POLARITY)
+X(SRST_VALUE)
X(STATE_BITS)
X(STATE_NUM)
X(STATE_NUM_LOG2)
@@ -169,6 +172,7 @@ X(T)
X(TABLE)
X(techmap_autopurge)
X(_TECHMAP_BITS_CONNMAP_)
+X(_TECHMAP_CELLNAME_)
X(_TECHMAP_CELLTYPE_)
X(techmap_celltype)
X(_TECHMAP_FAIL_)
diff --git a/kernel/ff.h b/kernel/ff.h
new file mode 100644
index 000000000..0aecbaa2a
--- /dev/null
+++ b/kernel/ff.h
@@ -0,0 +1,486 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 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.
+ *
+ */
+
+#ifndef FF_H
+#define FF_H
+
+#include "kernel/yosys.h"
+#include "kernel/ffinit.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct FfData {
+ FfInitVals *initvals;
+ SigSpec sig_q;
+ SigSpec sig_d;
+ SigSpec sig_clk;
+ SigSpec sig_en;
+ SigSpec sig_arst;
+ SigSpec sig_srst;
+ SigSpec sig_clr;
+ SigSpec sig_set;
+ bool has_d;
+ bool has_clk;
+ bool has_en;
+ bool has_srst;
+ bool has_arst;
+ bool has_sr;
+ bool ce_over_srst;
+ bool is_fine;
+ bool pol_clk;
+ bool pol_en;
+ bool pol_arst;
+ bool pol_srst;
+ bool pol_clr;
+ bool pol_set;
+ Const val_arst;
+ Const val_srst;
+ Const val_init;
+ Const val_d;
+ bool d_is_const;
+ int width;
+ dict<IdString, Const> attributes;
+
+ FfData(FfInitVals *initvals, Cell *cell = nullptr) : initvals(initvals) {
+ width = 0;
+ has_d = true;
+ has_clk = false;
+ has_en = false;
+ has_srst = false;
+ has_arst = false;
+ has_sr = false;
+ ce_over_srst = false;
+ is_fine = false;
+ pol_clk = false;
+ pol_en = false;
+ pol_arst = false;
+ pol_srst = false;
+ pol_clr = false;
+ pol_set = false;
+ d_is_const = false;
+
+ if (!cell)
+ return;
+
+ sig_q = cell->getPort(ID::Q);
+ width = GetSize(sig_q);
+ attributes = cell->attributes;
+
+ if (initvals)
+ val_init = (*initvals)(sig_q);
+
+ std::string type_str = cell->type.str();
+
+ if (cell->type.in(ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
+ if (cell->type == ID($sr)) {
+ has_d = false;
+ } else {
+ sig_d = cell->getPort(ID::D);
+ }
+ if (!cell->type.in(ID($ff), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) {
+ has_clk = true;
+ sig_clk = cell->getPort(ID::CLK);
+ pol_clk = cell->getParam(ID::CLK_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($dffe), ID($dffsre), ID($adffe), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr))) {
+ has_en = true;
+ sig_en = cell->getPort(ID::EN);
+ pol_en = cell->getParam(ID::EN_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($dffsr), ID($dffsre), ID($dlatchsr), ID($sr))) {
+ has_sr = true;
+ sig_clr = cell->getPort(ID::CLR);
+ sig_set = cell->getPort(ID::SET);
+ pol_clr = cell->getParam(ID::CLR_POLARITY).as_bool();
+ pol_set = cell->getParam(ID::SET_POLARITY).as_bool();
+ }
+ if (cell->type.in(ID($adff), ID($adffe), ID($adlatch))) {
+ has_arst = true;
+ sig_arst = cell->getPort(ID::ARST);
+ pol_arst = cell->getParam(ID::ARST_POLARITY).as_bool();
+ val_arst = cell->getParam(ID::ARST_VALUE);
+ }
+ if (cell->type.in(ID($sdff), ID($sdffe), ID($sdffce))) {
+ has_srst = true;
+ sig_srst = cell->getPort(ID::SRST);
+ pol_srst = cell->getParam(ID::SRST_POLARITY).as_bool();
+ val_srst = cell->getParam(ID::SRST_VALUE);
+ ce_over_srst = cell->type == ID($sdffce);
+ }
+ } else if (cell->type == ID($_FF_)) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ } else if (type_str.substr(0, 5) == "$_SR_") {
+ is_fine = true;
+ has_d = false;
+ has_sr = true;
+ pol_set = type_str[5] == 'P';
+ pol_clr = type_str[6] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else if (type_str.substr(0, 6) == "$_DFF_" && type_str.size() == 8) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[6] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ } else if (type_str.substr(0, 7) == "$_DFFE_" && type_str.size() == 10) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_en = true;
+ pol_en = type_str[8] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 6) == "$_DFF_" && type_str.size() == 10) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[6] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_arst = true;
+ pol_arst = type_str[7] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[8] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 7) == "$_DFFE_" && type_str.size() == 12) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_arst = true;
+ pol_arst = type_str[8] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[9] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[10] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 8) == "$_DFFSR_" && type_str.size() == 12) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[8] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_sr = true;
+ pol_set = type_str[9] == 'P';
+ pol_clr = type_str[10] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else if (type_str.substr(0, 9) == "$_DFFSRE_" && type_str.size() == 14) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[9] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_sr = true;
+ pol_set = type_str[10] == 'P';
+ pol_clr = type_str[11] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ has_en = true;
+ pol_en = type_str[12] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 7) == "$_SDFF_" && type_str.size() == 11) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[7] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[8] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[9] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 8) == "$_SDFFE_" && type_str.size() == 13) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[8] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[9] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[10] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[11] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 9) == "$_SDFFCE_" && type_str.size() == 14) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_clk = true;
+ pol_clk = type_str[9] == 'P';
+ sig_clk = cell->getPort(ID::C);
+ has_srst = true;
+ pol_srst = type_str[10] == 'P';
+ sig_srst = cell->getPort(ID::R);
+ val_srst = type_str[11] == '1' ? State::S1 : State::S0;
+ has_en = true;
+ pol_en = type_str[12] == 'P';
+ sig_en = cell->getPort(ID::E);
+ ce_over_srst = true;
+ } else if (type_str.substr(0, 9) == "$_DLATCH_" && type_str.size() == 11) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[9] == 'P';
+ sig_en = cell->getPort(ID::E);
+ } else if (type_str.substr(0, 9) == "$_DLATCH_" && type_str.size() == 13) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[9] == 'P';
+ sig_en = cell->getPort(ID::E);
+ has_arst = true;
+ pol_arst = type_str[10] == 'P';
+ sig_arst = cell->getPort(ID::R);
+ val_arst = type_str[11] == '1' ? State::S1 : State::S0;
+ } else if (type_str.substr(0, 11) == "$_DLATCHSR_" && type_str.size() == 15) {
+ is_fine = true;
+ sig_d = cell->getPort(ID::D);
+ has_en = true;
+ pol_en = type_str[11] == 'P';
+ sig_en = cell->getPort(ID::E);
+ has_sr = true;
+ pol_set = type_str[12] == 'P';
+ pol_clr = type_str[13] == 'P';
+ sig_set = cell->getPort(ID::S);
+ sig_clr = cell->getPort(ID::R);
+ } else {
+ log_assert(0);
+ }
+ if (has_d && sig_d.is_fully_const()) {
+ d_is_const = true;
+ val_d = sig_d.as_const();
+ if (has_en && !has_clk && !has_sr && !has_arst) {
+ // Plain D latches with const D treated specially.
+ has_en = has_d = false;
+ has_arst = true;
+ sig_arst = sig_en;
+ pol_arst = pol_en;
+ val_arst = val_d;
+ }
+ }
+ }
+
+ // Returns a FF identical to this one, but only keeping bit indices from the argument.
+ FfData slice(const std::vector<int> &bits) {
+ FfData res(initvals);
+ res.sig_clk = sig_clk;
+ res.sig_en = sig_en;
+ res.sig_arst = sig_arst;
+ res.sig_srst = sig_srst;
+ res.has_d = has_d;
+ res.has_clk = has_clk;
+ res.has_en = has_en;
+ res.has_arst = has_arst;
+ res.has_srst = has_srst;
+ res.has_sr = has_sr;
+ res.ce_over_srst = ce_over_srst;
+ res.is_fine = is_fine;
+ res.pol_clk = pol_clk;
+ res.pol_en = pol_en;
+ res.pol_arst = pol_arst;
+ res.pol_srst = pol_srst;
+ res.pol_clr = pol_clr;
+ res.pol_set = pol_set;
+ res.attributes = attributes;
+ for (int i : bits) {
+ res.sig_q.append(sig_q[i]);
+ if (has_d)
+ res.sig_d.append(sig_d[i]);
+ if (has_sr) {
+ res.sig_clr.append(sig_clr[i]);
+ res.sig_set.append(sig_set[i]);
+ }
+ if (has_arst)
+ res.val_arst.bits.push_back(val_arst[i]);
+ if (has_srst)
+ res.val_srst.bits.push_back(val_srst[i]);
+ res.val_init.bits.push_back(val_init[i]);
+ }
+ res.width = GetSize(res.sig_q);
+ // Slicing bits out may cause D to become const.
+ if (has_d && res.sig_d.is_fully_const()) {
+ res.d_is_const = true;
+ res.val_d = res.sig_d.as_const();
+ }
+ return res;
+ }
+
+ void unmap_ce(Module *module) {
+ if (!has_en)
+ return;
+ log_assert(has_clk);
+ if (has_srst && ce_over_srst)
+ unmap_srst(module);
+
+ if (!is_fine) {
+ if (pol_en)
+ sig_d = module->Mux(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->Mux(NEW_ID, sig_d, sig_q, sig_en);
+ } else {
+ if (pol_en)
+ sig_d = module->MuxGate(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->MuxGate(NEW_ID, sig_d, sig_q, sig_en);
+ }
+ has_en = false;
+ }
+
+ void unmap_srst(Module *module) {
+ if (!has_srst)
+ return;
+ if (has_en && !ce_over_srst)
+ unmap_ce(module);
+
+ if (!is_fine) {
+ if (pol_srst)
+ sig_d = module->Mux(NEW_ID, sig_d, val_srst, sig_srst);
+ else
+ sig_d = module->Mux(NEW_ID, val_srst, sig_d, sig_srst);
+ } else {
+ if (pol_srst)
+ sig_d = module->MuxGate(NEW_ID, sig_d, val_srst[0], sig_srst);
+ else
+ sig_d = module->MuxGate(NEW_ID, val_srst[0], sig_d, sig_srst);
+ }
+ has_srst = false;
+ }
+
+ void unmap_ce_srst(Module *module) {
+ unmap_ce(module);
+ unmap_srst(module);
+ }
+
+ Cell *emit(Module *module, IdString name) {
+ if (!width)
+ return nullptr;
+ if (!has_d && !has_sr) {
+ if (has_arst) {
+ // Convert this case to a D latch.
+ has_d = has_en = true;
+ has_arst = false;
+ sig_d = val_arst;
+ sig_en = sig_arst;
+ pol_en = pol_arst;
+ } else {
+ // No control inputs left. Turn into a const driver.
+ initvals->remove_init(sig_q);
+ module->connect(sig_q, val_init);
+ return nullptr;
+ }
+ }
+ initvals->set_init(sig_q, val_init);
+ Cell *cell;
+ if (!is_fine) {
+ if (!has_d) {
+ log_assert(has_sr);
+ cell = module->addSr(name, sig_set, sig_clr, sig_q, pol_set, pol_clr);
+ } else if (!has_clk && !has_en) {
+ log_assert(!has_arst);
+ log_assert(!has_srst);
+ log_assert(!has_sr);
+ cell = module->addFf(name, sig_d, sig_q);
+ } else if (!has_clk) {
+ log_assert(!has_srst);
+ if (has_sr)
+ cell = module->addDlatchsr(name, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_en, pol_set, pol_clr);
+ else if (has_arst)
+ cell = module->addAdlatch(name, sig_en, sig_arst, sig_d, sig_q, val_arst, pol_en, pol_arst);
+ else
+ cell = module->addDlatch(name, sig_en, sig_d, sig_q, pol_en);
+ } else {
+ if (has_sr) {
+ if (has_en)
+ cell = module->addDffsre(name, sig_clk, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_en, pol_set, pol_clr);
+ else
+ cell = module->addDffsr(name, sig_clk, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_set, pol_clr);
+ } else if (has_arst) {
+ if (has_en)
+ cell = module->addAdffe(name, sig_clk, sig_en, sig_arst, sig_d, sig_q, val_arst, pol_clk, pol_en, pol_arst);
+ else
+ cell = module->addAdff(name, sig_clk, sig_arst, sig_d, sig_q, val_arst, pol_clk, pol_arst);
+ } else if (has_srst) {
+ if (has_en)
+ if (ce_over_srst)
+ cell = module->addSdffce(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffe(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdff(name, sig_clk, sig_srst, sig_d, sig_q, val_srst, pol_clk, pol_srst);
+ } else {
+ if (has_en)
+ cell = module->addDffe(name, sig_clk, sig_en, sig_d, sig_q, pol_clk, pol_en);
+ else
+ cell = module->addDff(name, sig_clk, sig_d, sig_q, pol_clk);
+ }
+ }
+ } else {
+ if (!has_d) {
+ log_assert(has_sr);
+ cell = module->addSrGate(name, sig_set, sig_clr, sig_q, pol_set, pol_clr);
+ } else if (!has_clk && !has_en) {
+ log_assert(!has_arst);
+ log_assert(!has_srst);
+ log_assert(!has_sr);
+ cell = module->addFfGate(name, sig_d, sig_q);
+ } else if (!has_clk) {
+ log_assert(!has_srst);
+ if (has_sr)
+ cell = module->addDlatchsrGate(name, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_en, pol_set, pol_clr);
+ else if (has_arst)
+ cell = module->addAdlatchGate(name, sig_en, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_en, pol_arst);
+ else
+ cell = module->addDlatchGate(name, sig_en, sig_d, sig_q, pol_en);
+ } else {
+ if (has_sr) {
+ if (has_en)
+ cell = module->addDffsreGate(name, sig_clk, sig_en, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_en, pol_set, pol_clr);
+ else
+ cell = module->addDffsrGate(name, sig_clk, sig_set, sig_clr, sig_d, sig_q, pol_clk, pol_set, pol_clr);
+ } else if (has_arst) {
+ if (has_en)
+ cell = module->addAdffeGate(name, sig_clk, sig_en, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_clk, pol_en, pol_arst);
+ else
+ cell = module->addAdffGate(name, sig_clk, sig_arst, sig_d, sig_q, val_arst.as_bool(), pol_clk, pol_arst);
+ } else if (has_srst) {
+ if (has_en)
+ if (ce_over_srst)
+ cell = module->addSdffceGate(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffeGate(name, sig_clk, sig_en, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_en, pol_srst);
+ else
+ cell = module->addSdffGate(name, sig_clk, sig_srst, sig_d, sig_q, val_srst.as_bool(), pol_clk, pol_srst);
+ } else {
+ if (has_en)
+ cell = module->addDffeGate(name, sig_clk, sig_en, sig_d, sig_q, pol_clk, pol_en);
+ else
+ cell = module->addDffGate(name, sig_clk, sig_d, sig_q, pol_clk);
+ }
+ }
+ }
+ cell->attributes = attributes;
+ return cell;
+ }
+};
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/ffinit.h b/kernel/ffinit.h
new file mode 100644
index 000000000..025b0c862
--- /dev/null
+++ b/kernel/ffinit.h
@@ -0,0 +1,141 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 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.
+ *
+ */
+
+#ifndef FFINIT_H
+#define FFINIT_H
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct FfInitVals
+{
+ const SigMap *sigmap;
+ RTLIL::Module *module;
+ dict<SigBit, std::pair<State,SigBit>> initbits;
+
+ void set(const SigMap *sigmap_, RTLIL::Module *module)
+ {
+ sigmap = sigmap_;
+ initbits.clear();
+ for (auto wire : module->wires())
+ {
+ if (wire->attributes.count(ID::init) == 0)
+ continue;
+
+ SigSpec wirebits = (*sigmap)(wire);
+ Const initval = wire->attributes.at(ID::init);
+
+ for (int i = 0; i < GetSize(wirebits) && i < GetSize(initval); i++)
+ {
+ SigBit bit = wirebits[i];
+ State val = initval[i];
+
+ if (val != State::S0 && val != State::S1 && bit.wire != nullptr)
+ continue;
+
+ if (initbits.count(bit)) {
+ if (initbits.at(bit).first != val)
+ log_error("Conflicting init values for signal %s (%s = %s != %s).\n",
+ log_signal(bit), log_signal(SigBit(wire, i)),
+ log_signal(val), log_signal(initbits.at(bit).first));
+ continue;
+ }
+
+ initbits[bit] = std::make_pair(val,SigBit(wire,i));
+ }
+ }
+ }
+
+ RTLIL::State operator()(RTLIL::SigBit bit) const
+ {
+ auto it = initbits.find((*sigmap)(bit));
+ if (it != initbits.end())
+ return it->second.first;
+ else
+ return State::Sx;
+ }
+
+ RTLIL::Const operator()(const RTLIL::SigSpec &sig) const
+ {
+ RTLIL::Const res;
+ for (auto bit : sig)
+ res.bits.push_back((*this)(bit));
+ return res;
+ }
+
+ void set_init(RTLIL::SigBit bit, RTLIL::State val)
+ {
+ SigBit mbit = (*sigmap)(bit);
+ SigBit abit = bit;
+ auto it = initbits.find(mbit);
+ if (it != initbits.end())
+ abit = it->second.second;
+ else if (val == State::Sx)
+ return;
+ log_assert(abit.wire);
+ initbits[mbit] = std::make_pair(val,abit);
+ auto it2 = abit.wire->attributes.find(ID::init);
+ if (it2 != abit.wire->attributes.end()) {
+ it2->second[abit.offset] = val;
+ if (it2->second.is_fully_undef())
+ abit.wire->attributes.erase(it2);
+ } else if (val != State::Sx) {
+ Const cval(State::Sx, GetSize(abit.wire));
+ cval[abit.offset] = val;
+ abit.wire->attributes[ID::init] = cval;
+ }
+ }
+
+ void set_init(const RTLIL::SigSpec &sig, RTLIL::Const val)
+ {
+ log_assert(GetSize(sig) == GetSize(val));
+ for (int i = 0; i < GetSize(sig); i++)
+ set_init(sig[i], val[i]);
+ }
+
+ void remove_init(RTLIL::SigBit bit)
+ {
+ set_init(bit, State::Sx);
+ }
+
+ void remove_init(const RTLIL::SigSpec &sig)
+ {
+ for (auto bit : sig)
+ remove_init(bit);
+ }
+
+ void clear()
+ {
+ initbits.clear();
+ }
+
+ FfInitVals (const SigMap *sigmap, RTLIL::Module *module)
+ {
+ set(sigmap, module);
+ }
+
+ FfInitVals () {}
+};
+
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/hashlib.h b/kernel/hashlib.h
index 5c87b55f5..a523afadd 100644
--- a/kernel/hashlib.h
+++ b/kernel/hashlib.h
@@ -363,6 +363,7 @@ public:
public:
const_iterator() { }
const_iterator operator++() { index--; return *this; }
+ const_iterator operator+=(int amt) { index -= amt; return *this; }
bool operator<(const const_iterator &other) const { return index > other.index; }
bool operator==(const const_iterator &other) const { return index == other.index; }
bool operator!=(const const_iterator &other) const { return index != other.index; }
@@ -380,6 +381,7 @@ public:
public:
iterator() { }
iterator operator++() { index--; return *this; }
+ iterator operator+=(int amt) { index -= amt; return *this; }
bool operator<(const iterator &other) const { return index > other.index; }
bool operator==(const iterator &other) const { return index == other.index; }
bool operator!=(const iterator &other) const { return index != other.index; }
diff --git a/kernel/log.cc b/kernel/log.cc
index 104bee078..1c1d0182e 100644
--- a/kernel/log.cc
+++ b/kernel/log.cc
@@ -319,7 +319,7 @@ void log_file_info(const std::string &filename, int lineno,
va_end(ap);
}
-YS_ATTRIBUTE(noreturn)
+[[noreturn]]
static void logv_error_with_prefix(const char *prefix,
const char *format, va_list ap)
{
diff --git a/kernel/log.h b/kernel/log.h
index 516744b50..8981c4cde 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -55,7 +55,9 @@
#else
# include <sys/time.h>
# include <sys/resource.h>
-# include <signal.h>
+# if defined(__unix__) || (defined(__APPLE__) && defined(__MACH__))
+# include <signal.h>
+# endif
#endif
#if defined(_MSC_VER)
@@ -137,7 +139,7 @@ void logv(const char *format, va_list ap);
void logv_header(RTLIL::Design *design, const char *format, va_list ap);
void logv_warning(const char *format, va_list ap);
void logv_warning_noprefix(const char *format, va_list ap);
-YS_NORETURN void logv_error(const char *format, va_list ap) YS_ATTRIBUTE(noreturn);
+[[noreturn]] void logv_error(const char *format, va_list ap);
void log(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
void log_header(RTLIL::Design *design, const char *format, ...) YS_ATTRIBUTE(format(printf, 2, 3));
@@ -149,17 +151,16 @@ void log_file_warning(const std::string &filename, int lineno, const char *forma
void log_file_info(const std::string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4));
void log_warning_noprefix(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
-YS_NORETURN void log_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2), noreturn);
-void log_file_error(const string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4), noreturn);
-YS_NORETURN void log_cmd_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2), noreturn);
+[[noreturn]] void log_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
+[[noreturn]] void log_file_error(const string &filename, int lineno, const char *format, ...) YS_ATTRIBUTE(format(printf, 3, 4));
+[[noreturn]] void log_cmd_error(const char *format, ...) YS_ATTRIBUTE(format(printf, 1, 2));
#ifndef NDEBUG
static inline bool ys_debug(int n = 0) { if (log_force_debug) return true; log_debug_suppressed += n; return false; }
-# define log_debug(...) do { if (ys_debug(1)) log(__VA_ARGS__); } while (0)
#else
static inline bool ys_debug(int = 0) { return false; }
-# define log_debug(_fmt, ...) do { } while (0)
#endif
+# define log_debug(...) do { if (ys_debug(1)) log(__VA_ARGS__); } while (0)
static inline void log_suppressed() {
if (log_debug_suppressed && !log_make_debug) {
@@ -234,7 +235,7 @@ static inline void log_assert_worker(bool cond, const char *expr, const char *fi
}
# define log_assert(_assert_expr_) YOSYS_NAMESPACE_PREFIX log_assert_worker(_assert_expr_, #_assert_expr_, __FILE__, __LINE__)
#else
-# define log_assert(_assert_expr_)
+# define log_assert(_assert_expr_) do { if (0) { (void)(_assert_expr_); } } while(0)
#endif
#define log_abort() YOSYS_NAMESPACE_PREFIX log_error("Abort in %s:%d.\n", __FILE__, __LINE__)
@@ -306,19 +307,17 @@ struct PerformanceTimer
static int64_t query() {
# ifdef _WIN32
return 0;
-# elif defined(_POSIX_TIMERS) && (_POSIX_TIMERS > 0)
- struct timespec ts;
- clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &ts);
- return int64_t(ts.tv_sec)*1000000000 + ts.tv_nsec;
# elif defined(RUSAGE_SELF)
struct rusage rusage;
- int64_t t;
- if (getrusage(RUSAGE_SELF, &rusage) == -1) {
- log_cmd_error("getrusage failed!\n");
- log_abort();
+ int64_t t = 0;
+ for (int who : {RUSAGE_SELF, RUSAGE_CHILDREN}) {
+ if (getrusage(who, &rusage) == -1) {
+ log_cmd_error("getrusage failed!\n");
+ log_abort();
+ }
+ t += 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL;
+ t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL;
}
- t = 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL;
- t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL;
return t;
# else
# error "Don't know how to measure per-process CPU time. Need alternative method (times()/clocks()/gettimeofday()?)."
@@ -369,7 +368,7 @@ static inline void log_dump_val_worker(char *v) { log("%s", v); }
static inline void log_dump_val_worker(const char *v) { log("%s", v); }
static inline void log_dump_val_worker(std::string v) { log("%s", v.c_str()); }
static inline void log_dump_val_worker(PerformanceTimer p) { log("%f seconds", p.sec()); }
-static inline void log_dump_args_worker(const char *p YS_ATTRIBUTE(unused)) { log_assert(*p == 0); }
+static inline void log_dump_args_worker(const char *p) { log_assert(*p == 0); }
void log_dump_val_worker(RTLIL::IdString v);
void log_dump_val_worker(RTLIL::SigSpec v);
void log_dump_val_worker(RTLIL::State v);
diff --git a/kernel/macc.h b/kernel/macc.h
index e9f6f05e9..d216e6772 100644
--- a/kernel/macc.h
+++ b/kernel/macc.h
@@ -107,10 +107,8 @@ struct Macc
std::vector<RTLIL::State> config_bits = cell->getParam(ID::CONFIG).bits;
int config_cursor = 0;
-#ifndef NDEBUG
int config_width = cell->getParam(ID::CONFIG_WIDTH).as_int();
log_assert(GetSize(config_bits) >= config_width);
-#endif
int num_bits = 0;
if (config_bits[config_cursor++] == State::S1) num_bits |= 1;
diff --git a/kernel/modtools.h b/kernel/modtools.h
index fbc5482ee..29c510059 100644
--- a/kernel/modtools.h
+++ b/kernel/modtools.h
@@ -158,7 +158,7 @@ struct ModIndex : public RTLIL::Monitor
#endif
}
- void notify_connect(RTLIL::Cell *cell, const RTLIL::IdString &port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) YS_OVERRIDE
+ void notify_connect(RTLIL::Cell *cell, const RTLIL::IdString &port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) override
{
log_assert(module == cell->module);
@@ -169,7 +169,7 @@ struct ModIndex : public RTLIL::Monitor
port_add(cell, port, sig);
}
- void notify_connect(RTLIL::Module *mod YS_ATTRIBUTE(unused), const RTLIL::SigSig &sigsig) YS_OVERRIDE
+ void notify_connect(RTLIL::Module *mod, const RTLIL::SigSig &sigsig) override
{
log_assert(module == mod);
@@ -214,13 +214,13 @@ struct ModIndex : public RTLIL::Monitor
}
}
- void notify_connect(RTLIL::Module *mod YS_ATTRIBUTE(unused), const std::vector<RTLIL::SigSig>&) YS_OVERRIDE
+ void notify_connect(RTLIL::Module *mod, const std::vector<RTLIL::SigSig>&) override
{
log_assert(module == mod);
auto_reload_module = true;
}
- void notify_blackout(RTLIL::Module *mod YS_ATTRIBUTE(unused)) YS_OVERRIDE
+ void notify_blackout(RTLIL::Module *mod) override
{
log_assert(module == mod);
auto_reload_module = true;
diff --git a/kernel/register.cc b/kernel/register.cc
index 02974e534..34735a608 100644
--- a/kernel/register.cc
+++ b/kernel/register.cc
@@ -753,7 +753,7 @@ static struct CellHelpMessages {
struct HelpPass : public Pass {
HelpPass() : Pass("help", "display help messages") { }
- void help() YS_OVERRIDE
+ void help() override
{
log("\n");
log(" help ................ list all commands\n");
@@ -822,7 +822,7 @@ struct HelpPass : public Pass {
fclose(f);
}
- void execute(std::vector<std::string> args, RTLIL::Design*) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design*) override
{
if (args.size() == 1) {
log("\n");
@@ -926,7 +926,7 @@ struct HelpPass : public Pass {
struct EchoPass : public Pass {
EchoPass() : Pass("echo", "turning echoing back of commands on and off") { }
- void help() YS_OVERRIDE
+ void help() override
{
log("\n");
log(" echo on\n");
@@ -939,7 +939,7 @@ struct EchoPass : public Pass {
log("Do not print all commands to log before executing them. (default)\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design*) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design*) override
{
if (args.size() > 2)
cmd_error(args, 2, "Unexpected argument.");
@@ -964,7 +964,7 @@ struct MinisatSatSolver : public SatSolver {
MinisatSatSolver() : SatSolver("minisat") {
yosys_satsolver = this;
}
- ezSAT *create() YS_OVERRIDE {
+ ezSAT *create() override {
return new ezMiniSAT();
}
} MinisatSatSolver;
diff --git a/kernel/register.h b/kernel/register.h
index 7bbcd1727..5cd849082 100644
--- a/kernel/register.h
+++ b/kernel/register.h
@@ -97,9 +97,9 @@ struct Frontend : Pass
std::string frontend_name;
Frontend(std::string name, std::string short_help = "** document me **");
- void run_register() YS_OVERRIDE;
- ~Frontend() YS_OVERRIDE;
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE YS_FINAL;
+ void run_register() override;
+ ~Frontend() override;
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override final;
virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) = 0;
static std::vector<std::string> next_args;
@@ -113,9 +113,9 @@ struct Backend : Pass
{
std::string backend_name;
Backend(std::string name, std::string short_help = "** document me **");
- void run_register() YS_OVERRIDE;
- ~Backend() YS_OVERRIDE;
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE YS_FINAL;
+ void run_register() override;
+ ~Backend() override;
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override final;
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) = 0;
void extra_args(std::ostream *&f, std::string &filename, std::vector<std::string> args, size_t argidx, bool bin_output = false);
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 109113370..c56f0dcab 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -54,8 +54,14 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($dff),
ID($dffe),
ID($dffsr),
+ ID($dffsre),
ID($adff),
+ ID($adffe),
+ ID($sdff),
+ ID($sdffe),
+ ID($sdffce),
ID($dlatch),
+ ID($adlatch),
ID($dlatchsr),
ID($_DFFE_NN_),
ID($_DFFE_NP_),
@@ -69,16 +75,102 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($_DFFSR_PNP_),
ID($_DFFSR_PPN_),
ID($_DFFSR_PPP_),
+ ID($_DFFSRE_NNNN_),
+ ID($_DFFSRE_NNNP_),
+ ID($_DFFSRE_NNPN_),
+ ID($_DFFSRE_NNPP_),
+ ID($_DFFSRE_NPNN_),
+ ID($_DFFSRE_NPNP_),
+ ID($_DFFSRE_NPPN_),
+ ID($_DFFSRE_NPPP_),
+ ID($_DFFSRE_PNNN_),
+ ID($_DFFSRE_PNNP_),
+ ID($_DFFSRE_PNPN_),
+ ID($_DFFSRE_PNPP_),
+ ID($_DFFSRE_PPNN_),
+ ID($_DFFSRE_PPNP_),
+ ID($_DFFSRE_PPPN_),
+ ID($_DFFSRE_PPPP_),
+ ID($_DFF_N_),
+ ID($_DFF_P_),
ID($_DFF_NN0_),
ID($_DFF_NN1_),
ID($_DFF_NP0_),
ID($_DFF_NP1_),
- ID($_DFF_N_),
ID($_DFF_PN0_),
ID($_DFF_PN1_),
ID($_DFF_PP0_),
ID($_DFF_PP1_),
- ID($_DFF_P_),
+ ID($_DFFE_NN0N_),
+ ID($_DFFE_NN0P_),
+ ID($_DFFE_NN1N_),
+ ID($_DFFE_NN1P_),
+ ID($_DFFE_NP0N_),
+ ID($_DFFE_NP0P_),
+ ID($_DFFE_NP1N_),
+ ID($_DFFE_NP1P_),
+ ID($_DFFE_PN0N_),
+ ID($_DFFE_PN0P_),
+ ID($_DFFE_PN1N_),
+ ID($_DFFE_PN1P_),
+ ID($_DFFE_PP0N_),
+ ID($_DFFE_PP0P_),
+ ID($_DFFE_PP1N_),
+ ID($_DFFE_PP1P_),
+ ID($_SDFF_NN0_),
+ ID($_SDFF_NN1_),
+ ID($_SDFF_NP0_),
+ ID($_SDFF_NP1_),
+ ID($_SDFF_PN0_),
+ ID($_SDFF_PN1_),
+ ID($_SDFF_PP0_),
+ ID($_SDFF_PP1_),
+ ID($_SDFFE_NN0N_),
+ ID($_SDFFE_NN0P_),
+ ID($_SDFFE_NN1N_),
+ ID($_SDFFE_NN1P_),
+ ID($_SDFFE_NP0N_),
+ ID($_SDFFE_NP0P_),
+ ID($_SDFFE_NP1N_),
+ ID($_SDFFE_NP1P_),
+ ID($_SDFFE_PN0N_),
+ ID($_SDFFE_PN0P_),
+ ID($_SDFFE_PN1N_),
+ ID($_SDFFE_PN1P_),
+ ID($_SDFFE_PP0N_),
+ ID($_SDFFE_PP0P_),
+ ID($_SDFFE_PP1N_),
+ ID($_SDFFE_PP1P_),
+ ID($_SDFFCE_NN0N_),
+ ID($_SDFFCE_NN0P_),
+ ID($_SDFFCE_NN1N_),
+ ID($_SDFFCE_NN1P_),
+ ID($_SDFFCE_NP0N_),
+ ID($_SDFFCE_NP0P_),
+ ID($_SDFFCE_NP1N_),
+ ID($_SDFFCE_NP1P_),
+ ID($_SDFFCE_PN0N_),
+ ID($_SDFFCE_PN0P_),
+ ID($_SDFFCE_PN1N_),
+ ID($_SDFFCE_PN1P_),
+ ID($_SDFFCE_PP0N_),
+ ID($_SDFFCE_PP0P_),
+ ID($_SDFFCE_PP1N_),
+ ID($_SDFFCE_PP1P_),
+ ID($_SR_NN_),
+ ID($_SR_NP_),
+ ID($_SR_PN_),
+ ID($_SR_PP_),
+ ID($_DLATCH_N_),
+ ID($_DLATCH_P_),
+ ID($_DLATCH_NN0_),
+ ID($_DLATCH_NN1_),
+ ID($_DLATCH_NP0_),
+ ID($_DLATCH_NP1_),
+ ID($_DLATCH_PN0_),
+ ID($_DLATCH_PN1_),
+ ID($_DLATCH_PP0_),
+ ID($_DLATCH_PP1_),
ID($_DLATCHSR_NNN_),
ID($_DLATCHSR_NNP_),
ID($_DLATCHSR_NPN_),
@@ -87,8 +179,6 @@ const pool<IdString> &RTLIL::builtin_ff_cell_types() {
ID($_DLATCHSR_PNP_),
ID($_DLATCHSR_PPN_),
ID($_DLATCHSR_PPP_),
- ID($_DLATCH_N_),
- ID($_DLATCH_P_),
ID($_FF_),
};
return res;
@@ -319,7 +409,7 @@ void RTLIL::AttrObject::set_strpool_attribute(RTLIL::IdString id, const pool<str
attrval += "|";
attrval += s;
}
- attributes[id] = RTLIL::Const(attrval);
+ set_string_attribute(id, attrval);
}
void RTLIL::AttrObject::add_strpool_attribute(RTLIL::IdString id, const pool<string> &data)
@@ -334,11 +424,27 @@ pool<string> RTLIL::AttrObject::get_strpool_attribute(RTLIL::IdString id) const
{
pool<string> data;
if (attributes.count(id) != 0)
- for (auto s : split_tokens(attributes.at(id).decode_string(), "|"))
+ for (auto s : split_tokens(get_string_attribute(id), "|"))
data.insert(s);
return data;
}
+void RTLIL::AttrObject::set_hdlname_attribute(const vector<string> &hierarchy)
+{
+ string attrval;
+ for (const auto &ident : hierarchy) {
+ if (!attrval.empty())
+ attrval += " ";
+ attrval += ident;
+ }
+ set_string_attribute(ID::hdlname, attrval);
+}
+
+vector<string> RTLIL::AttrObject::get_hdlname_attribute() const
+{
+ return split_tokens(get_string_attribute(ID::hdlname), " ");
+}
+
bool RTLIL::Selection::selected_module(RTLIL::IdString mod_name) const
{
if (full_selection)
@@ -929,7 +1035,11 @@ namespace {
}
if (cell->type.in(ID($shift), ID($shiftx))) {
- param_bool(ID::A_SIGNED);
+ if (cell->type == ID($shiftx)) {
+ param_bool(ID::A_SIGNED, /*expected=*/false);
+ } else {
+ param_bool(ID::A_SIGNED);
+ }
param_bool(ID::B_SIGNED);
port(ID::A, param(ID::A_WIDTH));
port(ID::B, param(ID::B_WIDTH));
@@ -1123,6 +1233,21 @@ namespace {
return;
}
+ if (cell->type == ID($dffsre)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::SET_POLARITY);
+ param_bool(ID::CLR_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::SET, param(ID::WIDTH));
+ port(ID::CLR, param(ID::WIDTH));
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($adff)) {
param_bool(ID::CLK_POLARITY);
param_bool(ID::ARST_POLARITY);
@@ -1135,6 +1260,46 @@ namespace {
return;
}
+ if (cell->type == ID($sdff)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::SRST_POLARITY);
+ param_bits(ID::SRST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::SRST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
+ if (cell->type.in(ID($sdffe), ID($sdffce))) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::SRST_POLARITY);
+ param_bits(ID::SRST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::SRST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
+ if (cell->type == ID($adffe)) {
+ param_bool(ID::CLK_POLARITY);
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::ARST_POLARITY);
+ param_bits(ID::ARST_VALUE, param(ID::WIDTH));
+ port(ID::CLK, 1);
+ port(ID::EN, 1);
+ port(ID::ARST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($dlatch)) {
param_bool(ID::EN_POLARITY);
port(ID::EN, 1);
@@ -1144,6 +1309,18 @@ namespace {
return;
}
+ if (cell->type == ID($adlatch)) {
+ param_bool(ID::EN_POLARITY);
+ param_bool(ID::ARST_POLARITY);
+ param_bits(ID::ARST_VALUE, param(ID::WIDTH));
+ port(ID::EN, 1);
+ port(ID::ARST, 1);
+ port(ID::D, param(ID::WIDTH));
+ port(ID::Q, param(ID::WIDTH));
+ check_expected();
+ return;
+ }
+
if (cell->type == ID($dlatchsr)) {
param_bool(ID::EN_POLARITY);
param_bool(ID::SET_POLARITY);
@@ -1335,49 +1512,69 @@ namespace {
if (cell->type == ID($_MUX8_)) { port(ID::A,1); port(ID::B,1); port(ID::C,1); port(ID::D,1); port(ID::E,1); port(ID::F,1); port(ID::G,1); port(ID::H,1); port(ID::S,1); port(ID::T,1); port(ID::U,1); port(ID::Y,1); check_expected(); return; }
if (cell->type == ID($_MUX16_)) { port(ID::A,1); port(ID::B,1); port(ID::C,1); port(ID::D,1); port(ID::E,1); port(ID::F,1); port(ID::G,1); port(ID::H,1); port(ID::I,1); port(ID::J,1); port(ID::K,1); port(ID::L,1); port(ID::M,1); port(ID::N,1); port(ID::O,1); port(ID::P,1); port(ID::S,1); port(ID::T,1); port(ID::U,1); port(ID::V,1); port(ID::Y,1); check_expected(); return; }
- if (cell->type == ID($_SR_NN_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_NP_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_PN_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_SR_PP_)) { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_FF_)) { port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFF_N_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
- if (cell->type == ID($_DFF_P_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
-
- if (cell->type == ID($_DFFE_NN_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_NP_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_PN_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
- if (cell->type == ID($_DFFE_PP_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
-
- if (cell->type == ID($_DFF_NN0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NN1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NP0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_NP1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PN0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PN1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PP0_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
- if (cell->type == ID($_DFF_PP1_)) { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
-
- if (cell->type == ID($_DFFSR_NNN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NNP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NPN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_NPP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PNN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PNP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PPN_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DFFSR_PPP_)) { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_DLATCH_N_)) { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCH_P_)) { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
-
- if (cell->type == ID($_DLATCHSR_NNN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NNP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NPN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_NPP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PNN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PNP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PPN_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
- if (cell->type == ID($_DLATCHSR_PPP_)) { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+ if (cell->type.in(ID($_SR_NN_), ID($_SR_NP_), ID($_SR_PN_), ID($_SR_PP_)))
+ { port(ID::S,1); port(ID::R,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type == ID($_FF_)) { port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DFFE_NN_), ID($_DFFE_NP_), ID($_DFFE_PN_), ID($_DFFE_PP_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+ ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFE_NN0N_), ID($_DFFE_NN0P_), ID($_DFFE_NN1N_), ID($_DFFE_NN1P_),
+ ID($_DFFE_NP0N_), ID($_DFFE_NP0P_), ID($_DFFE_NP1N_), ID($_DFFE_NP1P_),
+ ID($_DFFE_PN0N_), ID($_DFFE_PN0P_), ID($_DFFE_PN1N_), ID($_DFFE_PN1P_),
+ ID($_DFFE_PP0N_), ID($_DFFE_PP0P_), ID($_DFFE_PP1N_), ID($_DFFE_PP1P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+ ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
+ { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DFFSRE_NNNN_), ID($_DFFSRE_NNNP_), ID($_DFFSRE_NNPN_), ID($_DFFSRE_NNPP_),
+ ID($_DFFSRE_NPNN_), ID($_DFFSRE_NPNP_), ID($_DFFSRE_NPPN_), ID($_DFFSRE_NPPP_),
+ ID($_DFFSRE_PNNN_), ID($_DFFSRE_PNNP_), ID($_DFFSRE_PNPN_), ID($_DFFSRE_PNPP_),
+ ID($_DFFSRE_PPNN_), ID($_DFFSRE_PPNP_), ID($_DFFSRE_PPPN_), ID($_DFFSRE_PPPP_)))
+ { port(ID::C,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::E,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_SDFF_NN0_), ID($_SDFF_NN1_), ID($_SDFF_NP0_), ID($_SDFF_NP1_),
+ ID($_SDFF_PN0_), ID($_SDFF_PN1_), ID($_SDFF_PP0_), ID($_SDFF_PP1_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_SDFFE_NN0N_), ID($_SDFFE_NN0P_), ID($_SDFFE_NN1N_), ID($_SDFFE_NN1P_),
+ ID($_SDFFE_NP0N_), ID($_SDFFE_NP0P_), ID($_SDFFE_NP1N_), ID($_SDFFE_NP1P_),
+ ID($_SDFFE_PN0N_), ID($_SDFFE_PN0P_), ID($_SDFFE_PN1N_), ID($_SDFFE_PN1P_),
+ ID($_SDFFE_PP0N_), ID($_SDFFE_PP0P_), ID($_SDFFE_PP1N_), ID($_SDFFE_PP1P_),
+ ID($_SDFFCE_NN0N_), ID($_SDFFCE_NN0P_), ID($_SDFFCE_NN1N_), ID($_SDFFCE_NN1P_),
+ ID($_SDFFCE_NP0N_), ID($_SDFFCE_NP0P_), ID($_SDFFCE_NP1N_), ID($_SDFFCE_NP1P_),
+ ID($_SDFFCE_PN0N_), ID($_SDFFCE_PN0P_), ID($_SDFFCE_PN1N_), ID($_SDFFCE_PN1P_),
+ ID($_SDFFCE_PP0N_), ID($_SDFFCE_PP0P_), ID($_SDFFCE_PP1N_), ID($_SDFFCE_PP1P_)))
+ { port(ID::D,1); port(ID::Q,1); port(ID::C,1); port(ID::R,1); port(ID::E,1); check_expected(); return; }
+
+ if (cell->type.in(ID($_DLATCH_N_), ID($_DLATCH_P_)))
+ { port(ID::E,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DLATCH_NN0_), ID($_DLATCH_NN1_), ID($_DLATCH_NP0_), ID($_DLATCH_NP1_),
+ ID($_DLATCH_PN0_), ID($_DLATCH_PN1_), ID($_DLATCH_PP0_), ID($_DLATCH_PP1_)))
+ { port(ID::E,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
+
+ if (cell->type.in(
+ ID($_DLATCHSR_NNN_), ID($_DLATCHSR_NNP_), ID($_DLATCHSR_NPN_), ID($_DLATCHSR_NPP_),
+ ID($_DLATCHSR_PNN_), ID($_DLATCHSR_PNP_), ID($_DLATCHSR_PPN_), ID($_DLATCHSR_PPP_)))
+ { port(ID::E,1); port(ID::S,1); port(ID::R,1); port(ID::D,1); port(ID::Q,1); check_expected(); return; }
error(__LINE__);
}
@@ -1520,13 +1717,13 @@ void RTLIL::Module::cloneInto(RTLIL::Module *new_mod) const
new_mod->addWire(it.first, it.second);
for (auto &it : memories)
- new_mod->memories[it.first] = new RTLIL::Memory(*it.second);
+ new_mod->addMemory(it.first, it.second);
for (auto &it : cells_)
new_mod->addCell(it.first, it.second);
for (auto &it : processes)
- new_mod->processes[it.first] = it.second->clone();
+ new_mod->addProcess(it.first, it.second);
struct RewriteSigSpecWorker
{
@@ -1897,6 +2094,14 @@ RTLIL::Memory *RTLIL::Module::addMemory(RTLIL::IdString name, const RTLIL::Memor
return mem;
}
+RTLIL::Process *RTLIL::Module::addProcess(RTLIL::IdString name, const RTLIL::Process *other)
+{
+ RTLIL::Process *proc = other->clone();
+ proc->name = name;
+ processes[name] = proc;
+ return proc;
+}
+
#define DEF_METHOD(_func, _y_size, _type) \
RTLIL::Cell* RTLIL::Module::add ## _func(RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, bool is_signed, const std::string &src) { \
RTLIL::Cell *cell = addCell(name, _type); \
@@ -2275,6 +2480,25 @@ RTLIL::Cell* RTLIL::Module::addDffsr(RTLIL::IdString name, const RTLIL::SigSpec
return cell;
}
+RTLIL::Cell* RTLIL::Module::addDffsre(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($dffsre));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SET_POLARITY] = set_polarity;
+ cell->parameters[ID::CLR_POLARITY] = clr_polarity;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SET, sig_set);
+ cell->setPort(ID::CLR, sig_clr);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addAdff(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
RTLIL::Const arst_value, bool clk_polarity, bool arst_polarity, const std::string &src)
{
@@ -2291,6 +2515,76 @@ RTLIL::Cell* RTLIL::Module::addAdff(RTLIL::IdString name, const RTLIL::SigSpec &
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdffe(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const arst_value, bool clk_polarity, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($adffe));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::ARST_POLARITY] = arst_polarity;
+ cell->parameters[ID::ARST_VALUE] = arst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::ARST, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdff(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdff));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffe(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdffe));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffce(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($sdffce));
+ cell->parameters[ID::CLK_POLARITY] = clk_polarity;
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::SRST_POLARITY] = srst_polarity;
+ cell->parameters[ID::SRST_VALUE] = srst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::CLK, sig_clk);
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::SRST, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatch(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, ID($dlatch));
@@ -2303,6 +2597,22 @@ RTLIL::Cell* RTLIL::Module::addDlatch(RTLIL::IdString name, const RTLIL::SigSpec
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdlatch(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ RTLIL::Const arst_value, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, ID($adlatch));
+ cell->parameters[ID::EN_POLARITY] = en_polarity;
+ cell->parameters[ID::ARST_POLARITY] = arst_polarity;
+ cell->parameters[ID::ARST_VALUE] = arst_value;
+ cell->parameters[ID::WIDTH] = sig_q.size();
+ cell->setPort(ID::EN, sig_en);
+ cell->setPort(ID::ARST, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
{
@@ -2320,6 +2630,17 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, const RTLIL::SigSp
return cell;
}
+RTLIL::Cell* RTLIL::Module::addSrGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ const RTLIL::SigSpec &sig_q, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SR_%c%c_", set_polarity ? 'P' : 'N', clr_polarity ? 'P' : 'N'));
+ cell->setPort(ID::S, sig_set);
+ cell->setPort(ID::R, sig_clr);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, ID($_FF_));
@@ -2363,6 +2684,20 @@ RTLIL::Cell* RTLIL::Module::addDffsrGate(RTLIL::IdString name, const RTLIL::SigS
return cell;
}
+RTLIL::Cell* RTLIL::Module::addDffsreGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DFFSRE_%c%c%c%c_", clk_polarity ? 'P' : 'N', set_polarity ? 'P' : 'N', clr_polarity ? 'P' : 'N', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::S, sig_set);
+ cell->setPort(ID::R, sig_clr);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addAdffGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
bool arst_value, bool clk_polarity, bool arst_polarity, const std::string &src)
{
@@ -2375,6 +2710,57 @@ RTLIL::Cell* RTLIL::Module::addAdffGate(RTLIL::IdString name, const RTLIL::SigSp
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdffeGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value, bool clk_polarity, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DFFE_%c%c%c%c_", clk_polarity ? 'P' : 'N', arst_polarity ? 'P' : 'N', arst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_arst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFF_%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffeGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFFE_%c%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
+RTLIL::Cell* RTLIL::Module::addSdffceGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value, bool clk_polarity, bool en_polarity, bool srst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_SDFFCE_%c%c%c%c_", clk_polarity ? 'P' : 'N', srst_polarity ? 'P' : 'N', srst_value ? '1' : '0', en_polarity ? 'P' : 'N'));
+ cell->setPort(ID::C, sig_clk);
+ cell->setPort(ID::R, sig_srst);
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, const std::string &src)
{
RTLIL::Cell *cell = addCell(name, stringf("$_DLATCH_%c_", en_polarity ? 'P' : 'N'));
@@ -2385,6 +2771,18 @@ RTLIL::Cell* RTLIL::Module::addDlatchGate(RTLIL::IdString name, const RTLIL::Sig
return cell;
}
+RTLIL::Cell* RTLIL::Module::addAdlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value, bool en_polarity, bool arst_polarity, const std::string &src)
+{
+ RTLIL::Cell *cell = addCell(name, stringf("$_DLATCH_%c%c%c_", en_polarity ? 'P' : 'N', arst_polarity ? 'P' : 'N', arst_value ? '1' : '0'));
+ cell->setPort(ID::E, sig_en);
+ cell->setPort(ID::R, sig_arst);
+ cell->setPort(ID::D, sig_d);
+ cell->setPort(ID::Q, sig_q);
+ cell->set_src_attribute(src);
+ return cell;
+}
+
RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity, bool set_polarity, bool clr_polarity, const std::string &src)
{
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 86b4e25b6..6c561cb85 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -554,6 +554,29 @@ namespace RTLIL
return *this;
}
+ inline ObjIterator<T>& operator+=(int amt) {
+ log_assert(list_p != nullptr);
+ it += amt;
+ if (it == list_p->end()) {
+ (*refcount_p)--;
+ list_p = nullptr;
+ refcount_p = nullptr;
+ }
+ return *this;
+ }
+
+ inline ObjIterator<T> operator+(int amt) {
+ log_assert(list_p != nullptr);
+ ObjIterator<T> new_obj(*this);
+ new_obj.it += amt;
+ if (new_obj.it == list_p->end()) {
+ (*(new_obj.refcount_p))--;
+ new_obj.list_p = nullptr;
+ new_obj.refcount_p = nullptr;
+ }
+ return new_obj;
+ }
+
inline const ObjIterator<T> operator++(int) {
ObjIterator<T> result(*this);
++(*this);
@@ -682,6 +705,9 @@ struct RTLIL::AttrObject
std::string get_src_attribute() const {
return get_string_attribute(ID::src);
}
+
+ void set_hdlname_attribute(const vector<string> &hierarchy);
+ vector<string> get_hdlname_attribute() const;
};
struct RTLIL::SigChunk
@@ -1058,6 +1084,13 @@ struct RTLIL::Design
return selected_member(module->name, member->name);
}
+ template<typename T1> void select(T1 *module) {
+ if (selection_stack.size() > 0) {
+ RTLIL::Selection &sel = selection_stack.back();
+ sel.select(module);
+ }
+ }
+
template<typename T1, typename T2> void select(T1 *module, T2 *member) {
if (selection_stack.size() > 0) {
RTLIL::Selection &sel = selection_stack.back();
@@ -1172,6 +1205,8 @@ public:
RTLIL::Memory *addMemory(RTLIL::IdString name, const RTLIL::Memory *other);
+ RTLIL::Process *addProcess(RTLIL::IdString name, const RTLIL::Process *other);
+
// The add* methods create a cell and return the created cell. All signals must exist in advance.
RTLIL::Cell* addNot (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, bool is_signed = false, const std::string &src = "");
@@ -1239,8 +1274,14 @@ public:
RTLIL::Cell* addDff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffsr (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addDffsre (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addAdff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool clk_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool clk_polarity = true, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdff (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffe (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffce (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const srst_value, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatch (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdlatch (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, RTLIL::Const arst_value, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchsr (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addBufGate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_y, const std::string &src = "");
@@ -1260,14 +1301,28 @@ public:
RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const RTLIL::SigBit &sig_c, const RTLIL::SigBit &sig_d, const RTLIL::SigBit &sig_y, const std::string &src = "");
RTLIL::Cell* addOai4Gate (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const RTLIL::SigBit &sig_c, const RTLIL::SigBit &sig_d, const RTLIL::SigBit &sig_y, const std::string &src = "");
+ RTLIL::Cell* addSrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ const RTLIL::SigSpec &sig_q, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addFfGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src = "");
RTLIL::Cell* addDffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, const std::string &src = "");
RTLIL::Cell* addDffsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addDffsreGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
+ RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool clk_polarity = true, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
RTLIL::Cell* addAdffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
bool arst_value = false, bool clk_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value = false, bool clk_polarity = true, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffeGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addSdffceGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_clk, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_srst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool srst_value = false, bool clk_polarity = true, bool en_polarity = true, bool srst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, const std::string &src = "");
+ RTLIL::Cell* addAdlatchGate(RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_arst, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q,
+ bool arst_value = false, bool en_polarity = true, bool arst_polarity = true, const std::string &src = "");
RTLIL::Cell* addDlatchsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr,
RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = "");
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
new file mode 100644
index 000000000..2a54e78ec
--- /dev/null
+++ b/kernel/satgen.cc
@@ -0,0 +1,1239 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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/satgen.h"
+#include "kernel/ff.h"
+
+USING_YOSYS_NAMESPACE
+
+bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
+{
+ bool arith_undef_handled = false;
+ bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
+
+ if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ if (is_arith_compare)
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ else
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+ std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
+ undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
+ }
+
+ if (is_arith_compare) {
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+ ez->SET(undef_y_bit, undef_y.at(0));
+ } else {
+ std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
+ ez->assume(ez->vec_eq(undef_y_bits, undef_y));
+ }
+
+ arith_undef_handled = true;
+ }
+
+ if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
+ ID($and), ID($or), ID($xor), ID($xnor), ID($add), ID($sub)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type.in(ID($and), ID($_AND_)))
+ ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
+ if (cell->type == ID($_NAND_))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
+ if (cell->type.in(ID($or), ID($_OR_)))
+ ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
+ if (cell->type == ID($_NOR_))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
+ if (cell->type.in(ID($xor), ID($_XOR_)))
+ ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
+ if (cell->type.in(ID($xnor), ID($_XNOR_)))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
+ if (cell->type == ID($_ANDNOT_))
+ ez->assume(ez->vec_eq(ez->vec_and(a, ez->vec_not(b)), yy));
+ if (cell->type == ID($_ORNOT_))
+ ez->assume(ez->vec_eq(ez->vec_or(a, ez->vec_not(b)), yy));
+ if (cell->type == ID($add))
+ ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
+ if (cell->type == ID($sub))
+ ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
+
+ if (model_undef && !arith_undef_handled)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
+
+ if (cell->type.in(ID($and), ID($_AND_), ID($_NAND_))) {
+ std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
+ std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type.in(ID($or), ID($_OR_), ID($_NOR_))) {
+ std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
+ std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
+ std::vector<int> yX = ez->vec_or(undef_a, undef_b);
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else if (cell->type == ID($_ANDNOT_)) {
+ std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
+ std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b1)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+
+ else if (cell->type == ID($_ORNOT_)) {
+ std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
+ std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
+ std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b0)));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ }
+ else
+ log_abort();
+
+ undefGating(y, yy, undef_y);
+ }
+ else if (model_undef)
+ {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
+ {
+ bool aoi_mode = cell->type.in(ID($_AOI3_), ID($_AOI4_));
+ bool three_mode = cell->type.in(ID($_AOI3_), ID($_OAI3_));
+
+ int a = importDefSigSpec(cell->getPort(ID::A), timestep).at(0);
+ int b = importDefSigSpec(cell->getPort(ID::B), timestep).at(0);
+ int c = importDefSigSpec(cell->getPort(ID::C), timestep).at(0);
+ int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort(ID::D), timestep).at(0);
+ int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+ int yy = model_undef ? ez->literal() : y;
+
+ if (cell->type.in(ID($_AOI3_), ID($_AOI4_)))
+ ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
+ else
+ ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
+
+ if (model_undef)
+ {
+ int undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep).at(0);
+ int undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep).at(0);
+ int undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep).at(0);
+ int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort(ID::D), timestep).at(0);
+ int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ if (aoi_mode)
+ {
+ int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
+ int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
+ int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
+ int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
+
+ int ab = ez->AND(a, b), cd = ez->AND(c, d);
+ int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
+ int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
+
+ int ab1 = ez->AND(ab, ez->NOT(undef_ab));
+ int cd1 = ez->AND(cd, ez->NOT(undef_cd));
+ int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
+
+ ez->assume(ez->IFF(yX, undef_y));
+ }
+ else
+ {
+ int a1 = ez->AND(a, ez->NOT(undef_a));
+ int b1 = ez->AND(b, ez->NOT(undef_b));
+ int c1 = ez->AND(c, ez->NOT(undef_c));
+ int d1 = ez->AND(d, ez->NOT(undef_d));
+
+ int ab = ez->OR(a, b), cd = ez->OR(c, d);
+ int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
+ int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
+
+ int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
+ int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
+ int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
+
+ ez->assume(ez->IFF(yX, undef_y));
+ }
+
+ undefGating(y, yy, undef_y);
+ }
+
+ return true;
+ }
+
+ if (cell->type.in(ID($_NOT_), ID($not)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ ez->assume(ez->vec_eq(ez->vec_not(a), yy));
+
+ if (model_undef) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell, false);
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ if (cell->type == ID($_NMUX_))
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
+ else
+ ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
+ std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
+ std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
+ ez->assume(ez->vec_eq(yX, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($pmux))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> tmp = a;
+ for (size_t i = 0; i < s.size(); i++) {
+ std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
+ tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
+ }
+ ez->assume(ez->vec_eq(tmp, yy));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ int maybe_a = ez->CONST_TRUE;
+
+ std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+ std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+
+ for (size_t i = 0; i < s.size(); i++)
+ {
+ std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
+ std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
+
+ int maybe_s = ez->OR(s.at(i), undef_s.at(i));
+ int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
+
+ maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
+
+ bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
+ bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
+ }
+
+ bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
+ bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
+
+ ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($pos), ID($neg)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($pos)) {
+ ez->assume(ez->vec_eq(a, yy));
+ } else {
+ std::vector<int> zero(a.size(), ez->CONST_FALSE);
+ ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell);
+
+ if (cell->type == ID($pos)) {
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ } else {
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
+ ez->assume(ez->vec_eq(undef_y_bits, undef_y));
+ }
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($reduce_and))
+ ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
+ if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
+ ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
+ if (cell->type == ID($reduce_xor))
+ ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
+ if (cell->type == ID($reduce_xnor))
+ ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
+ if (cell->type == ID($logic_not))
+ ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ int aX = ez->expression(ezSAT::OpOr, undef_a);
+
+ if (cell->type == ID($reduce_and)) {
+ int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
+ ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
+ }
+ else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
+ int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
+ ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
+ }
+ else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
+ ez->assume(ez->IFF(aX, undef_y.at(0)));
+ } else
+ log_abort();
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($logic_and), ID($logic_or)))
+ {
+ std::vector<int> vec_a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> vec_b = importDefSigSpec(cell->getPort(ID::B), timestep);
+
+ int a = ez->expression(ez->OpOr, vec_a);
+ int b = ez->expression(ez->OpOr, vec_b);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (cell->type == ID($logic_and))
+ ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
+ else
+ ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
+ int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
+ int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
+ int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
+ int aX = ez->expression(ezSAT::OpOr, undef_a);
+ int bX = ez->expression(ezSAT::OpOr, undef_b);
+
+ if (cell->type == ID($logic_and))
+ ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
+ else if (cell->type == ID($logic_or))
+ ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
+ else
+ log_abort();
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt)))
+ {
+ bool is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(a, b, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ if (model_undef && cell->type.in(ID($eqx), ID($nex))) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ a = ez->vec_or(a, undef_a);
+ b = ez->vec_or(b, undef_b);
+ }
+
+ if (cell->type == ID($lt))
+ ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
+ if (cell->type == ID($le))
+ ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
+ if (cell->type.in(ID($eq), ID($eqx)))
+ ez->SET(ez->vec_eq(a, b), yy.at(0));
+ if (cell->type.in(ID($ne), ID($nex)))
+ ez->SET(ez->vec_ne(a, b), yy.at(0));
+ if (cell->type == ID($ge))
+ ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
+ if (cell->type == ID($gt))
+ ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
+ for (size_t i = 1; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, yy.at(i));
+
+ if (model_undef && cell->type.in(ID($eqx), ID($nex)))
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ if (cell->type == ID($eqx))
+ yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+ else
+ yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
+
+ for (size_t i = 0; i < y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+
+ ez->assume(ez->vec_eq(y, yy));
+ }
+ else if (model_undef && cell->type.in(ID($eq), ID($ne)))
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ int undef_any = ez->OR(undef_any_a, undef_any_b);
+
+ std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
+ std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
+
+ int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
+ int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
+
+ for (size_t i = 1; i < undef_y.size(); i++)
+ ez->SET(ez->CONST_FALSE, undef_y.at(i));
+ ez->SET(undef_y_bit, undef_y.at(0));
+
+ undefGating(y, yy, undef_y);
+ }
+ else
+ {
+ if (model_undef) {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ log_assert(!model_undef || arith_undef_handled);
+ }
+ return true;
+ }
+
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ int extend_bit = ez->CONST_FALSE;
+
+ if (cell->parameters[ID::A_SIGNED].as_bool())
+ extend_bit = a.back();
+
+ while (y.size() < a.size())
+ y.push_back(ez->literal());
+ while (y.size() > a.size())
+ a.push_back(extend_bit);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> shifted_a;
+
+ if (cell->type.in( ID($shl), ID($sshl)))
+ shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shr))
+ shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($sshr))
+ shifted_a = ez->vec_shift_right(a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type.in(ID($shift), ID($shiftx)))
+ shifted_a = ez->vec_shift_right(a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
+
+ ez->assume(ez->vec_eq(shifted_a, yy));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_a_shifted;
+
+ extend_bit = cell->type == ID($shiftx) ? ez->CONST_TRUE : ez->CONST_FALSE;
+ if (cell->parameters[ID::A_SIGNED].as_bool())
+ extend_bit = undef_a.back();
+
+ while (undef_y.size() < undef_a.size())
+ undef_y.push_back(ez->literal());
+ while (undef_y.size() > undef_a.size())
+ undef_a.push_back(extend_bit);
+
+ if (cell->type.in(ID($shl), ID($sshl)))
+ undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shr))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($sshr))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shift))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
+
+ if (cell->type == ID($shiftx))
+ undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
+
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+ std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
+ ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($mul))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> tmp(a.size(), ez->CONST_FALSE);
+ for (int i = 0; i < int(a.size()); i++)
+ {
+ std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
+ for (int j = i; j < int(a.size()); j++)
+ shifted_a.at(j) = a.at(j-i);
+ tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+ }
+ ez->assume(ez->vec_eq(tmp, yy));
+
+ if (model_undef) {
+ log_assert(arith_undef_handled);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($macc))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ Macc macc;
+ macc.from_cell(cell);
+
+ std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
+
+ for (auto &port : macc.ports)
+ {
+ std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
+ std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
+
+ while (GetSize(in_a) < GetSize(y))
+ in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
+ in_a.resize(GetSize(y));
+
+ if (GetSize(in_b))
+ {
+ while (GetSize(in_b) < GetSize(y))
+ in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
+ in_b.resize(GetSize(y));
+
+ for (int i = 0; i < GetSize(in_b); i++) {
+ std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
+ for (int j = i; j < int(in_a.size()); j++)
+ shifted_a.at(j) = in_a.at(j-i);
+ if (port.do_subtract)
+ tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
+ else
+ tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+ }
+ }
+ else
+ {
+ if (port.do_subtract)
+ tmp = ez->vec_sub(tmp, in_a);
+ else
+ tmp = ez->vec_add(tmp, in_a);
+ }
+ }
+
+ for (int i = 0; i < GetSize(b); i++) {
+ std::vector<int> val(GetSize(y), ez->CONST_FALSE);
+ val.at(0) = b.at(i);
+ tmp = ez->vec_add(tmp, val);
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+
+ int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+ int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
+
+ undefGating(y, tmp, undef_y);
+ }
+ else
+ ez->assume(ez->vec_eq(y, tmp));
+
+ return true;
+ }
+
+ if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidth(a, b, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
+ std::vector<int> a_u, b_u;
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
+ b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
+ } else {
+ a_u = a;
+ b_u = b;
+ }
+
+ std::vector<int> chain_buf = a_u;
+ std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
+ for (int i = int(a.size())-1; i >= 0; i--)
+ {
+ chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
+
+ std::vector<int> b_shl(i, ez->CONST_FALSE);
+ b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
+ b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
+
+ y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
+ chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
+
+ chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
+ }
+
+ std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
+
+ // modulo calculation
+ std::vector<int> modulo_trunc;
+ int floored_eq_trunc;
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
+ // floor == trunc when sgn(a) == sgn(b) or trunc == 0
+ floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
+ } else {
+ modulo_trunc = chain_buf;
+ floored_eq_trunc = ez->CONST_TRUE;
+ }
+
+ if (cell->type == ID($div)) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
+ else
+ ez->assume(ez->vec_eq(y_tmp, y_u));
+ } else if (cell->type == ID($mod)) {
+ ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
+ } else if (cell->type == ID($divfloor)) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
+ ez->XOR(a.back(), b.back()),
+ ez->vec_neg(ez->vec_ite(
+ ez->vec_reduce_or(modulo_trunc),
+ ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
+ y_u
+ )),
+ y_u
+ )));
+ else
+ ez->assume(ez->vec_eq(y_tmp, y_u));
+ } else if (cell->type == ID($modfloor)) {
+ ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
+ }
+
+ if (ignore_div_by_zero) {
+ ez->assume(ez->expression(ezSAT::OpOr, b));
+ } else {
+ std::vector<int> div_zero_result;
+ if (cell->type.in(ID($div), ID($divfloor))) {
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
+ std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
+ std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
+ only_first_one.at(0) = ez->CONST_TRUE;
+ div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
+ } else {
+ div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
+ }
+ } else if (cell->type.in(ID($mod), ID($modfloor))) {
+ // a mod 0 = a
+ int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
+ div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
+ if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
+ else
+ div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
+ }
+ ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
+ }
+
+ if (model_undef) {
+ log_assert(arith_undef_handled);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($lut))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> lut;
+ for (auto bit : cell->getParam(ID::LUT).bits)
+ lut.push_back(bit == State::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
+ while (GetSize(lut) < (1 << GetSize(a)))
+ lut.push_back(ez->CONST_FALSE);
+ lut.resize(1 << GetSize(a));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
+
+ for (int i = GetSize(a)-1; i >= 0; i--)
+ {
+ std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
+ std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
+
+ std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
+ std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
+
+ t = ez->vec_ite(a[i], t1, t0);
+ u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
+ }
+
+ log_assert(GetSize(t) == 1);
+ log_assert(GetSize(u) == 1);
+ undefGating(y, t, u);
+ ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort(ID::Y), timestep), u));
+ }
+ else
+ {
+ std::vector<int> t = lut;
+ for (int i = GetSize(a)-1; i >= 0; i--)
+ {
+ std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
+ std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
+ t = ez->vec_ite(a[i], t1, t0);
+ }
+
+ log_assert(GetSize(t) == 1);
+ ez->assume(ez->vec_eq(y, t));
+ }
+ return true;
+ }
+
+ if (cell->type == ID($sop))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ int width = cell->getParam(ID::WIDTH).as_int();
+ int depth = cell->getParam(ID::DEPTH).as_int();
+
+ vector<State> table_raw = cell->getParam(ID::TABLE).bits;
+ while (GetSize(table_raw) < 2*width*depth)
+ table_raw.push_back(State::S0);
+
+ vector<vector<int>> table(depth);
+
+ for (int i = 0; i < depth; i++)
+ for (int j = 0; j < width; j++)
+ {
+ bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
+ bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
+
+ if (pat0 && !pat1)
+ table.at(i).push_back(0);
+ else if (!pat0 && pat1)
+ table.at(i).push_back(1);
+ else
+ table.at(i).push_back(-1);
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> products, undef_products;
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_ua, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_ua.push_back(undef_a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
+ std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
+
+ int masked_eq = ez->vec_eq(masked_a, masked_b);
+ int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
+
+ undef_products.push_back(ez->AND(any_undef, masked_eq));
+ products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
+ }
+
+ int yy = ez->expression(ezSAT::OpOr, products);
+ ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
+ undefGating(y, yy, undef_y);
+ }
+ else
+ {
+ std::vector<int> products;
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ products.push_back(ez->vec_eq(cmp_a, cmp_b));
+ }
+
+ ez->SET(y, ez->expression(ezSAT::OpOr, products));
+ }
+
+ return true;
+ }
+
+ if (cell->type == ID($fa))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> c = importDefSigSpec(cell->getPort(ID::C), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
+
+ std::vector<int> t1 = ez->vec_xor(a, b);
+ ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
+
+ std::vector<int> t2 = ez->vec_and(a, b);
+ std::vector<int> t3 = ez->vec_and(c, t1);
+ ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
+
+ ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
+ ez->assume(ez->vec_eq(undef_x, undef_y));
+
+ undefGating(y, yy, undef_y);
+ undefGating(x, xx, undef_x);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($lcu))
+ {
+ std::vector<int> p = importDefSigSpec(cell->getPort(ID::P), timestep);
+ std::vector<int> g = importDefSigSpec(cell->getPort(ID::G), timestep);
+ std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
+
+ for (int i = 0; i < GetSize(co); i++)
+ ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_p = importUndefSigSpec(cell->getPort(ID::P), timestep);
+ std::vector<int> undef_g = importUndefSigSpec(cell->getPort(ID::G), timestep);
+ std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
+
+ int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
+ int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
+ int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
+ int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
+
+ std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
+ ez->assume(ez->vec_eq(undef_co_bits, undef_co));
+
+ undefGating(co, yy, undef_co);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($alu))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
+ std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> bi = importDefSigSpec(cell->getPort(ID::BI), timestep);
+ std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
+
+ extendSignalWidth(a, b, y, cell);
+ extendSignalWidth(a, b, x, cell);
+ extendSignalWidth(a, b, co, cell);
+
+ std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
+ std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
+
+ log_assert(GetSize(y) == GetSize(x));
+ log_assert(GetSize(y) == GetSize(co));
+ log_assert(GetSize(ci) == 1);
+ log_assert(GetSize(bi) == 1);
+
+ for (int i = 0; i < GetSize(y); i++)
+ {
+ int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
+ ez->SET(def_x.at(i), ez->XOR(s1, s2));
+ ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
+ ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+ std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
+ std::vector<int> undef_bi = importUndefSigSpec(cell->getPort(ID::BI), timestep);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
+ std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
+
+ extendSignalWidth(undef_a, undef_b, undef_y, cell);
+ extendSignalWidth(undef_a, undef_b, undef_x, cell);
+ extendSignalWidth(undef_a, undef_b, undef_co, cell);
+
+ std::vector<int> all_inputs_undef;
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
+ int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
+
+ for (int i = 0; i < GetSize(undef_y); i++) {
+ ez->SET(undef_y.at(i), undef_any);
+ ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
+ ez->SET(undef_co.at(i), undef_any);
+ }
+
+ undefGating(y, def_y, undef_y);
+ undefGating(x, def_x, undef_x);
+ undefGating(co, def_co, undef_co);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($slice))
+ {
+ RTLIL::SigSpec a = cell->getPort(ID::A);
+ RTLIL::SigSpec y = cell->getPort(ID::Y);
+ ez->assume(signals_eq(a.extract(cell->parameters.at(ID::OFFSET).as_int(), y.size()), y, timestep));
+ return true;
+ }
+
+ if (cell->type == ID($concat))
+ {
+ RTLIL::SigSpec a = cell->getPort(ID::A);
+ RTLIL::SigSpec b = cell->getPort(ID::B);
+ RTLIL::SigSpec y = cell->getPort(ID::Y);
+
+ RTLIL::SigSpec ab = a;
+ ab.append(b);
+
+ ez->assume(signals_eq(ab, y, timestep));
+ return true;
+ }
+
+ if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
+ {
+ FfData ff(nullptr, cell);
+
+ // Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
+ if (!ff.has_d || ff.has_arst || ff.has_sr || (ff.has_en && !ff.has_clk))
+ return false;
+
+ if (timestep == 1)
+ {
+ initial_state.add((*sigmap)(cell->getPort(ID::Q)));
+ }
+ else
+ {
+ std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
+ std::vector<int> undef_d;
+ if (model_undef)
+ undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
+ if (ff.has_srst && ff.has_en && ff.ce_over_srst) {
+ int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+ std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+ int undef_srst;
+ std::vector<int> undef_rval;
+ if (model_undef) {
+ undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+ undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+ }
+ if (ff.pol_srst)
+ std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+ else
+ std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+ }
+ if (ff.has_en) {
+ int en = importDefSigSpec(ff.sig_en, timestep-1).at(0);
+ std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
+ int undef_en;
+ std::vector<int> undef_old_q;
+ if (model_undef) {
+ undef_en = importUndefSigSpec(ff.sig_en, timestep-1).at(0);
+ undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1);
+ }
+ if (ff.pol_en)
+ std::tie(d, undef_d) = mux(en, undef_en, old_q, undef_old_q, d, undef_d);
+ else
+ std::tie(d, undef_d) = mux(en, undef_en, d, undef_d, old_q, undef_old_q);
+ }
+ if (ff.has_srst && !(ff.has_en && ff.ce_over_srst)) {
+ int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+ std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+ int undef_srst;
+ std::vector<int> undef_rval;
+ if (model_undef) {
+ undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+ undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+ }
+ if (ff.pol_srst)
+ std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+ else
+ std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+ }
+ std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
+
+ std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+ ez->assume(ez->vec_eq(d, qq));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
+
+ ez->assume(ez->vec_eq(undef_d, undef_q));
+ undefGating(q, qq, undef_q);
+ }
+ }
+ return true;
+ }
+
+ if (cell->type == ID($anyconst))
+ {
+ if (timestep < 2)
+ return true;
+
+ std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
+ std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+ std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+ ez->assume(ez->vec_eq(d, qq));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
+ std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+ ez->assume(ez->vec_eq(undef_d, undef_q));
+ undefGating(q, qq, undef_q);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($anyseq))
+ {
+ return true;
+ }
+
+ if (cell->type.in(ID($_BUF_), ID($equiv)))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(a, y, cell);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ ez->assume(ez->vec_eq(a, yy));
+
+ if (model_undef) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ extendSignalWidthUnary(undef_a, undef_y, cell, false);
+ ez->assume(ez->vec_eq(undef_a, undef_y));
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
+ if (cell->type == ID($initstate))
+ {
+ auto key = make_pair(prefix, timestep);
+ if (initstates.count(key) == 0)
+ initstates[key] = false;
+
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ log_assert(GetSize(y) == 1);
+ ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
+
+ if (model_undef) {
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ log_assert(GetSize(undef_y) == 1);
+ ez->SET(undef_y[0], ez->CONST_FALSE);
+ }
+
+ return true;
+ }
+
+ if (cell->type == ID($assert))
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ asserts_a[pf].append((*sigmap)(cell->getPort(ID::A)));
+ asserts_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
+ return true;
+ }
+
+ if (cell->type == ID($assume))
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ assumes_a[pf].append((*sigmap)(cell->getPort(ID::A)));
+ assumes_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
+ return true;
+ }
+
+ // Unsupported internal cell types: $pow $fsm $mem*
+ // .. and all sequential cells with asynchronous inputs
+ return false;
+}
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 3929a8708..cf2db733f 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -262,6 +262,18 @@ struct SatGen
}
}
+ std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) {
+ std::vector<int> res;
+ std::vector<int> undef_res;
+ res = ez->vec_ite(s, b, a);
+ if (model_undef) {
+ std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
+ std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
+ undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+ }
+ return std::make_pair(res, undef_res);
+ }
+
void undefGating(int y, int yy, int undef)
{
ez->assume(ez->OR(undef, ez->IFF(y, yy)));
@@ -274,1171 +286,7 @@ struct SatGen
initstates[key] = true;
}
- bool importCell(RTLIL::Cell *cell, int timestep = -1)
- {
- bool arith_undef_handled = false;
- bool is_arith_compare = cell->type.in(ID($lt), ID($le), ID($ge), ID($gt));
-
- if (model_undef && (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)) || is_arith_compare))
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- if (is_arith_compare)
- extendSignalWidth(undef_a, undef_b, cell, true);
- else
- extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- int undef_y_bit = ez->OR(undef_any_a, undef_any_b);
-
- if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
- std::vector<int> b = importSigSpec(cell->getPort(ID::B), timestep);
- undef_y_bit = ez->OR(undef_y_bit, ez->NOT(ez->expression(ezSAT::OpOr, b)));
- }
-
- if (is_arith_compare) {
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
- ez->SET(undef_y_bit, undef_y.at(0));
- } else {
- std::vector<int> undef_y_bits(undef_y.size(), undef_y_bit);
- ez->assume(ez->vec_eq(undef_y_bits, undef_y));
- }
-
- arith_undef_handled = true;
- }
-
- if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
- ID($and), ID($or), ID($xor), ID($xnor), ID($add), ID($sub)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type.in(ID($and), ID($_AND_)))
- ez->assume(ez->vec_eq(ez->vec_and(a, b), yy));
- if (cell->type == ID($_NAND_))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_and(a, b)), yy));
- if (cell->type.in(ID($or), ID($_OR_)))
- ez->assume(ez->vec_eq(ez->vec_or(a, b), yy));
- if (cell->type == ID($_NOR_))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_or(a, b)), yy));
- if (cell->type.in(ID($xor), ID($_XOR_)))
- ez->assume(ez->vec_eq(ez->vec_xor(a, b), yy));
- if (cell->type.in(ID($xnor), ID($_XNOR_)))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(a, b)), yy));
- if (cell->type == ID($_ANDNOT_))
- ez->assume(ez->vec_eq(ez->vec_and(a, ez->vec_not(b)), yy));
- if (cell->type == ID($_ORNOT_))
- ez->assume(ez->vec_eq(ez->vec_or(a, ez->vec_not(b)), yy));
- if (cell->type == ID($add))
- ez->assume(ez->vec_eq(ez->vec_add(a, b), yy));
- if (cell->type == ID($sub))
- ez->assume(ez->vec_eq(ez->vec_sub(a, b), yy));
-
- if (model_undef && !arith_undef_handled)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
-
- if (cell->type.in(ID($and), ID($_AND_), ID($_NAND_))) {
- std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
- std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b0)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type.in(ID($or), ID($_OR_), ID($_NOR_))) {
- std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
- std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b1)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
- std::vector<int> yX = ez->vec_or(undef_a, undef_b);
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else if (cell->type == ID($_ANDNOT_)) {
- std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
- std::vector<int> b1 = ez->vec_and(b, ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a0, b1)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
-
- else if (cell->type == ID($_ORNOT_)) {
- std::vector<int> a1 = ez->vec_and(a, ez->vec_not(undef_a));
- std::vector<int> b0 = ez->vec_and(ez->vec_not(b), ez->vec_not(undef_b));
- std::vector<int> yX = ez->vec_and(ez->vec_or(undef_a, undef_b), ez->vec_not(ez->vec_or(a1, b0)));
- ez->assume(ez->vec_eq(yX, undef_y));
- }
- else
- log_abort();
-
- undefGating(y, yy, undef_y);
- }
- else if (model_undef)
- {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
- {
- bool aoi_mode = cell->type.in(ID($_AOI3_), ID($_AOI4_));
- bool three_mode = cell->type.in(ID($_AOI3_), ID($_OAI3_));
-
- int a = importDefSigSpec(cell->getPort(ID::A), timestep).at(0);
- int b = importDefSigSpec(cell->getPort(ID::B), timestep).at(0);
- int c = importDefSigSpec(cell->getPort(ID::C), timestep).at(0);
- int d = three_mode ? (aoi_mode ? ez->CONST_TRUE : ez->CONST_FALSE) : importDefSigSpec(cell->getPort(ID::D), timestep).at(0);
- int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
- int yy = model_undef ? ez->literal() : y;
-
- if (cell->type.in(ID($_AOI3_), ID($_AOI4_)))
- ez->assume(ez->IFF(ez->NOT(ez->OR(ez->AND(a, b), ez->AND(c, d))), yy));
- else
- ez->assume(ez->IFF(ez->NOT(ez->AND(ez->OR(a, b), ez->OR(c, d))), yy));
-
- if (model_undef)
- {
- int undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep).at(0);
- int undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep).at(0);
- int undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep).at(0);
- int undef_d = three_mode ? ez->CONST_FALSE : importUndefSigSpec(cell->getPort(ID::D), timestep).at(0);
- int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- if (aoi_mode)
- {
- int a0 = ez->AND(ez->NOT(a), ez->NOT(undef_a));
- int b0 = ez->AND(ez->NOT(b), ez->NOT(undef_b));
- int c0 = ez->AND(ez->NOT(c), ez->NOT(undef_c));
- int d0 = ez->AND(ez->NOT(d), ez->NOT(undef_d));
-
- int ab = ez->AND(a, b), cd = ez->AND(c, d);
- int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a0, b0)));
- int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c0, d0)));
-
- int ab1 = ez->AND(ab, ez->NOT(undef_ab));
- int cd1 = ez->AND(cd, ez->NOT(undef_cd));
- int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab1, cd1)));
-
- ez->assume(ez->IFF(yX, undef_y));
- }
- else
- {
- int a1 = ez->AND(a, ez->NOT(undef_a));
- int b1 = ez->AND(b, ez->NOT(undef_b));
- int c1 = ez->AND(c, ez->NOT(undef_c));
- int d1 = ez->AND(d, ez->NOT(undef_d));
-
- int ab = ez->OR(a, b), cd = ez->OR(c, d);
- int undef_ab = ez->AND(ez->OR(undef_a, undef_b), ez->NOT(ez->OR(a1, b1)));
- int undef_cd = ez->AND(ez->OR(undef_c, undef_d), ez->NOT(ez->OR(c1, d1)));
-
- int ab0 = ez->AND(ez->NOT(ab), ez->NOT(undef_ab));
- int cd0 = ez->AND(ez->NOT(cd), ez->NOT(undef_cd));
- int yX = ez->AND(ez->OR(undef_ab, undef_cd), ez->NOT(ez->OR(ab0, cd0)));
-
- ez->assume(ez->IFF(yX, undef_y));
- }
-
- undefGating(y, yy, undef_y);
- }
-
- return true;
- }
-
- if (cell->type.in(ID($_NOT_), ID($not)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- ez->assume(ez->vec_eq(ez->vec_not(a), yy));
-
- if (model_undef) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell, false);
- ez->assume(ez->vec_eq(undef_a, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- if (cell->type == ID($_NMUX_))
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
- else
- ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
- std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
- std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
- ez->assume(ez->vec_eq(yX, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($pmux))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> tmp = a;
- for (size_t i = 0; i < s.size(); i++) {
- std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
- tmp = ez->vec_ite(s.at(i), part_of_b, tmp);
- }
- ez->assume(ez->vec_eq(tmp, yy));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- int maybe_a = ez->CONST_TRUE;
-
- std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
- std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
-
- for (size_t i = 0; i < s.size(); i++)
- {
- std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
- std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
-
- int maybe_s = ez->OR(s.at(i), undef_s.at(i));
- int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
-
- maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
-
- bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
- bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
- }
-
- bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
- bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
-
- ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($pos), ID($neg)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($pos)) {
- ez->assume(ez->vec_eq(a, yy));
- } else {
- std::vector<int> zero(a.size(), ez->CONST_FALSE);
- ez->assume(ez->vec_eq(ez->vec_sub(zero, a), yy));
- }
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell);
-
- if (cell->type == ID($pos)) {
- ez->assume(ez->vec_eq(undef_a, undef_y));
- } else {
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- std::vector<int> undef_y_bits(undef_y.size(), undef_any_a);
- ez->assume(ez->vec_eq(undef_y_bits, undef_y));
- }
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor), ID($reduce_bool), ID($logic_not)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($reduce_and))
- ez->SET(ez->expression(ez->OpAnd, a), yy.at(0));
- if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
- ez->SET(ez->expression(ez->OpOr, a), yy.at(0));
- if (cell->type == ID($reduce_xor))
- ez->SET(ez->expression(ez->OpXor, a), yy.at(0));
- if (cell->type == ID($reduce_xnor))
- ez->SET(ez->NOT(ez->expression(ez->OpXor, a)), yy.at(0));
- if (cell->type == ID($logic_not))
- ez->SET(ez->NOT(ez->expression(ez->OpOr, a)), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- int aX = ez->expression(ezSAT::OpOr, undef_a);
-
- if (cell->type == ID($reduce_and)) {
- int a0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a)));
- ez->assume(ez->IFF(ez->AND(ez->NOT(a0), aX), undef_y.at(0)));
- }
- else if (cell->type.in(ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
- int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(a, ez->vec_not(undef_a)));
- ez->assume(ez->IFF(ez->AND(ez->NOT(a1), aX), undef_y.at(0)));
- }
- else if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
- ez->assume(ez->IFF(aX, undef_y.at(0)));
- } else
- log_abort();
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($logic_and), ID($logic_or)))
- {
- std::vector<int> vec_a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> vec_b = importDefSigSpec(cell->getPort(ID::B), timestep);
-
- int a = ez->expression(ez->OpOr, vec_a);
- int b = ez->expression(ez->OpOr, vec_b);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (cell->type == ID($logic_and))
- ez->SET(ez->expression(ez->OpAnd, a, b), yy.at(0));
- else
- ez->SET(ez->expression(ez->OpOr, a, b), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- int a0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_a), ez->expression(ezSAT::OpOr, undef_a)));
- int b0 = ez->NOT(ez->OR(ez->expression(ezSAT::OpOr, vec_b), ez->expression(ezSAT::OpOr, undef_b)));
- int a1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_a, ez->vec_not(undef_a)));
- int b1 = ez->expression(ezSAT::OpOr, ez->vec_and(vec_b, ez->vec_not(undef_b)));
- int aX = ez->expression(ezSAT::OpOr, undef_a);
- int bX = ez->expression(ezSAT::OpOr, undef_b);
-
- if (cell->type == ID($logic_and))
- ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a1, b1)), ez->NOT(a0), ez->NOT(b0)), undef_y.at(0));
- else if (cell->type == ID($logic_or))
- ez->SET(ez->AND(ez->OR(aX, bX), ez->NOT(ez->AND(a0, b0)), ez->NOT(a1), ez->NOT(b1)), undef_y.at(0));
- else
- log_abort();
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type.in(ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt)))
- {
- bool is_signed = cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool();
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(a, b, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- if (model_undef && cell->type.in(ID($eqx), ID($nex))) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- extendSignalWidth(undef_a, undef_b, cell, true);
- a = ez->vec_or(a, undef_a);
- b = ez->vec_or(b, undef_b);
- }
-
- if (cell->type == ID($lt))
- ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
- if (cell->type == ID($le))
- ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0));
- if (cell->type.in(ID($eq), ID($eqx)))
- ez->SET(ez->vec_eq(a, b), yy.at(0));
- if (cell->type.in(ID($ne), ID($nex)))
- ez->SET(ez->vec_ne(a, b), yy.at(0));
- if (cell->type == ID($ge))
- ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0));
- if (cell->type == ID($gt))
- ez->SET(is_signed ? ez->vec_gt_signed(a, b) : ez->vec_gt_unsigned(a, b), yy.at(0));
- for (size_t i = 1; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, yy.at(i));
-
- if (model_undef && cell->type.in(ID($eqx), ID($nex)))
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(undef_a, undef_b, cell, true);
-
- if (cell->type == ID($eqx))
- yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
- else
- yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
-
- for (size_t i = 0; i < y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
-
- ez->assume(ez->vec_eq(y, yy));
- }
- else if (model_undef && cell->type.in(ID($eq), ID($ne)))
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(undef_a, undef_b, cell, true);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- int undef_any = ez->OR(undef_any_a, undef_any_b);
-
- std::vector<int> masked_a_bits = ez->vec_or(a, ez->vec_or(undef_a, undef_b));
- std::vector<int> masked_b_bits = ez->vec_or(b, ez->vec_or(undef_a, undef_b));
-
- int masked_ne = ez->vec_ne(masked_a_bits, masked_b_bits);
- int undef_y_bit = ez->AND(undef_any, ez->NOT(masked_ne));
-
- for (size_t i = 1; i < undef_y.size(); i++)
- ez->SET(ez->CONST_FALSE, undef_y.at(i));
- ez->SET(undef_y_bit, undef_y.at(0));
-
- undefGating(y, yy, undef_y);
- }
- else
- {
- if (model_undef) {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- log_assert(!model_undef || arith_undef_handled);
- }
- return true;
- }
-
- if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- int extend_bit = ez->CONST_FALSE;
-
- if (!cell->type.in(ID($shift), ID($shiftx)) && cell->parameters[ID::A_SIGNED].as_bool())
- extend_bit = a.back();
-
- while (y.size() < a.size())
- y.push_back(ez->literal());
- while (y.size() > a.size())
- a.push_back(extend_bit);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> shifted_a;
-
- if (cell->type.in( ID($shl), ID($sshl)))
- shifted_a = ez->vec_shift_left(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shr))
- shifted_a = ez->vec_shift_right(a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($sshr))
- shifted_a = ez->vec_shift_right(a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type.in(ID($shift), ID($shiftx)))
- shifted_a = ez->vec_shift_right(a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
-
- ez->assume(ez->vec_eq(shifted_a, yy));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> undef_a_shifted;
-
- extend_bit = cell->type == ID($shiftx) ? ez->CONST_TRUE : ez->CONST_FALSE;
- if (!cell->type.in(ID($shift), ID($shiftx)) && cell->parameters[ID::A_SIGNED].as_bool())
- extend_bit = undef_a.back();
-
- while (undef_y.size() < undef_a.size())
- undef_y.push_back(ez->literal());
- while (undef_y.size() > undef_a.size())
- undef_a.push_back(extend_bit);
-
- if (cell->type.in(ID($shl), ID($sshl)))
- undef_a_shifted = ez->vec_shift_left(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shr))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($sshr))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, false, cell->parameters[ID::A_SIGNED].as_bool() ? undef_a.back() : ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shift))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_FALSE, ez->CONST_FALSE);
-
- if (cell->type == ID($shiftx))
- undef_a_shifted = ez->vec_shift_right(undef_a, b, cell->parameters[ID::B_SIGNED].as_bool(), ez->CONST_TRUE, ez->CONST_TRUE);
-
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
- std::vector<int> undef_all_y_bits(undef_y.size(), undef_any_b);
- ez->assume(ez->vec_eq(ez->vec_or(undef_a_shifted, undef_all_y_bits), undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($mul))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> tmp(a.size(), ez->CONST_FALSE);
- for (int i = 0; i < int(a.size()); i++)
- {
- std::vector<int> shifted_a(a.size(), ez->CONST_FALSE);
- for (int j = i; j < int(a.size()); j++)
- shifted_a.at(j) = a.at(j-i);
- tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
- }
- ez->assume(ez->vec_eq(tmp, yy));
-
- if (model_undef) {
- log_assert(arith_undef_handled);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($macc))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- Macc macc;
- macc.from_cell(cell);
-
- std::vector<int> tmp(GetSize(y), ez->CONST_FALSE);
-
- for (auto &port : macc.ports)
- {
- std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
- std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
-
- while (GetSize(in_a) < GetSize(y))
- in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->CONST_FALSE);
- in_a.resize(GetSize(y));
-
- if (GetSize(in_b))
- {
- while (GetSize(in_b) < GetSize(y))
- in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->CONST_FALSE);
- in_b.resize(GetSize(y));
-
- for (int i = 0; i < GetSize(in_b); i++) {
- std::vector<int> shifted_a(in_a.size(), ez->CONST_FALSE);
- for (int j = i; j < int(in_a.size()); j++)
- shifted_a.at(j) = in_a.at(j-i);
- if (port.do_subtract)
- tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
- else
- tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
- }
- }
- else
- {
- if (port.do_subtract)
- tmp = ez->vec_sub(tmp, in_a);
- else
- tmp = ez->vec_add(tmp, in_a);
- }
- }
-
- for (int i = 0; i < GetSize(b); i++) {
- std::vector<int> val(GetSize(y), ez->CONST_FALSE);
- val.at(0) = b.at(i);
- tmp = ez->vec_add(tmp, val);
- }
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
-
- int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
- int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
-
- undefGating(y, tmp, undef_y);
- }
- else
- ez->assume(ez->vec_eq(y, tmp));
-
- return true;
- }
-
- if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidth(a, b, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
-
- std::vector<int> a_u, b_u;
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- a_u = ez->vec_ite(a.back(), ez->vec_neg(a), a);
- b_u = ez->vec_ite(b.back(), ez->vec_neg(b), b);
- } else {
- a_u = a;
- b_u = b;
- }
-
- std::vector<int> chain_buf = a_u;
- std::vector<int> y_u(a_u.size(), ez->CONST_FALSE);
- for (int i = int(a.size())-1; i >= 0; i--)
- {
- chain_buf.insert(chain_buf.end(), chain_buf.size(), ez->CONST_FALSE);
-
- std::vector<int> b_shl(i, ez->CONST_FALSE);
- b_shl.insert(b_shl.end(), b_u.begin(), b_u.end());
- b_shl.insert(b_shl.end(), chain_buf.size()-b_shl.size(), ez->CONST_FALSE);
-
- y_u.at(i) = ez->vec_ge_unsigned(chain_buf, b_shl);
- chain_buf = ez->vec_ite(y_u.at(i), ez->vec_sub(chain_buf, b_shl), chain_buf);
-
- chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
- }
-
- std::vector<int> y_tmp = ignore_div_by_zero ? yy : ez->vec_var(y.size());
-
- // modulo calculation
- std::vector<int> modulo_trunc;
- int floored_eq_trunc;
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- modulo_trunc = ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf);
- // floor == trunc when sgn(a) == sgn(b) or trunc == 0
- floored_eq_trunc = ez->OR(ez->IFF(a.back(), b.back()), ez->NOT(ez->expression(ezSAT::OpOr, modulo_trunc)));
- } else {
- modulo_trunc = chain_buf;
- floored_eq_trunc = ez->CONST_TRUE;
- }
-
- if (cell->type == ID($div)) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
- else
- ez->assume(ez->vec_eq(y_tmp, y_u));
- } else if (cell->type == ID($mod)) {
- ez->assume(ez->vec_eq(y_tmp, modulo_trunc));
- } else if (cell->type == ID($divfloor)) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(
- ez->XOR(a.back(), b.back()),
- ez->vec_neg(ez->vec_ite(
- ez->vec_reduce_or(modulo_trunc),
- ez->vec_add(y_u, ez->vec_const_unsigned(1, y_u.size())),
- y_u
- )),
- y_u
- )));
- else
- ez->assume(ez->vec_eq(y_tmp, y_u));
- } else if (cell->type == ID($modfloor)) {
- ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(floored_eq_trunc, modulo_trunc, ez->vec_add(modulo_trunc, b))));
- }
-
- if (ignore_div_by_zero) {
- ez->assume(ez->expression(ezSAT::OpOr, b));
- } else {
- std::vector<int> div_zero_result;
- if (cell->type.in(ID($div), ID($divfloor))) {
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool()) {
- std::vector<int> all_ones(y.size(), ez->CONST_TRUE);
- std::vector<int> only_first_one(y.size(), ez->CONST_FALSE);
- only_first_one.at(0) = ez->CONST_TRUE;
- div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
- } else {
- div_zero_result.insert(div_zero_result.end(), cell->getPort(ID::A).size(), ez->CONST_TRUE);
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
- }
- } else if (cell->type.in(ID($mod), ID($modfloor))) {
- // a mod 0 = a
- int copy_a_bits = min(cell->getPort(ID::A).size(), cell->getPort(ID::B).size());
- div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
- if (cell->parameters[ID::A_SIGNED].as_bool() && cell->parameters[ID::B_SIGNED].as_bool())
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
- else
- div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
- }
- ez->assume(ez->vec_eq(yy, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
- }
-
- if (model_undef) {
- log_assert(arith_undef_handled);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($lut))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> lut;
- for (auto bit : cell->getParam(ID::LUT).bits)
- lut.push_back(bit == State::S1 ? ez->CONST_TRUE : ez->CONST_FALSE);
- while (GetSize(lut) < (1 << GetSize(a)))
- lut.push_back(ez->CONST_FALSE);
- lut.resize(1 << GetSize(a));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> t(lut), u(GetSize(t), ez->CONST_FALSE);
-
- for (int i = GetSize(a)-1; i >= 0; i--)
- {
- std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
- std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
-
- std::vector<int> u0(u.begin(), u.begin() + GetSize(u)/2);
- std::vector<int> u1(u.begin() + GetSize(u)/2, u.end());
-
- t = ez->vec_ite(a[i], t1, t0);
- u = ez->vec_ite(undef_a[i], ez->vec_or(ez->vec_xor(t0, t1), ez->vec_or(u0, u1)), ez->vec_ite(a[i], u1, u0));
- }
-
- log_assert(GetSize(t) == 1);
- log_assert(GetSize(u) == 1);
- undefGating(y, t, u);
- ez->assume(ez->vec_eq(importUndefSigSpec(cell->getPort(ID::Y), timestep), u));
- }
- else
- {
- std::vector<int> t = lut;
- for (int i = GetSize(a)-1; i >= 0; i--)
- {
- std::vector<int> t0(t.begin(), t.begin() + GetSize(t)/2);
- std::vector<int> t1(t.begin() + GetSize(t)/2, t.end());
- t = ez->vec_ite(a[i], t1, t0);
- }
-
- log_assert(GetSize(t) == 1);
- ez->assume(ez->vec_eq(y, t));
- }
- return true;
- }
-
- if (cell->type == ID($sop))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- int y = importDefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- int width = cell->getParam(ID::WIDTH).as_int();
- int depth = cell->getParam(ID::DEPTH).as_int();
-
- vector<State> table_raw = cell->getParam(ID::TABLE).bits;
- while (GetSize(table_raw) < 2*width*depth)
- table_raw.push_back(State::S0);
-
- vector<vector<int>> table(depth);
-
- for (int i = 0; i < depth; i++)
- for (int j = 0; j < width; j++)
- {
- bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
- bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
-
- if (pat0 && !pat1)
- table.at(i).push_back(0);
- else if (!pat0 && pat1)
- table.at(i).push_back(1);
- else
- table.at(i).push_back(-1);
- }
-
- if (model_undef)
- {
- std::vector<int> products, undef_products;
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- int undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep).at(0);
-
- for (int i = 0; i < depth; i++)
- {
- std::vector<int> cmp_a, cmp_ua, cmp_b;
-
- for (int j = 0; j < width; j++)
- if (table.at(i).at(j) >= 0) {
- cmp_a.push_back(a.at(j));
- cmp_ua.push_back(undef_a.at(j));
- cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
- }
-
- std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
- std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
-
- int masked_eq = ez->vec_eq(masked_a, masked_b);
- int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
-
- undef_products.push_back(ez->AND(any_undef, masked_eq));
- products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
- }
-
- int yy = ez->expression(ezSAT::OpOr, products);
- ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
- undefGating(y, yy, undef_y);
- }
- else
- {
- std::vector<int> products;
-
- for (int i = 0; i < depth; i++)
- {
- std::vector<int> cmp_a, cmp_b;
-
- for (int j = 0; j < width; j++)
- if (table.at(i).at(j) >= 0) {
- cmp_a.push_back(a.at(j));
- cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
- }
-
- products.push_back(ez->vec_eq(cmp_a, cmp_b));
- }
-
- ez->SET(y, ez->expression(ezSAT::OpOr, products));
- }
-
- return true;
- }
-
- if (cell->type == ID($fa))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> c = importDefSigSpec(cell->getPort(ID::C), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> xx = model_undef ? ez->vec_var(x.size()) : x;
-
- std::vector<int> t1 = ez->vec_xor(a, b);
- ez->assume(ez->vec_eq(yy, ez->vec_xor(t1, c)));
-
- std::vector<int> t2 = ez->vec_and(a, b);
- std::vector<int> t3 = ez->vec_and(c, t1);
- ez->assume(ez->vec_eq(xx, ez->vec_or(t2, t3)));
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
-
- ez->assume(ez->vec_eq(undef_y, ez->vec_or(ez->vec_or(undef_a, undef_b), undef_c)));
- ez->assume(ez->vec_eq(undef_x, undef_y));
-
- undefGating(y, yy, undef_y);
- undefGating(x, xx, undef_x);
- }
- return true;
- }
-
- if (cell->type == ID($lcu))
- {
- std::vector<int> p = importDefSigSpec(cell->getPort(ID::P), timestep);
- std::vector<int> g = importDefSigSpec(cell->getPort(ID::G), timestep);
- std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
-
- std::vector<int> yy = model_undef ? ez->vec_var(co.size()) : co;
-
- for (int i = 0; i < GetSize(co); i++)
- ez->SET(yy[i], ez->OR(g[i], ez->AND(p[i], i ? yy[i-1] : ci[0])));
-
- if (model_undef)
- {
- std::vector<int> undef_p = importUndefSigSpec(cell->getPort(ID::P), timestep);
- std::vector<int> undef_g = importUndefSigSpec(cell->getPort(ID::G), timestep);
- std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
-
- int undef_any_p = ez->expression(ezSAT::OpOr, undef_p);
- int undef_any_g = ez->expression(ezSAT::OpOr, undef_g);
- int undef_any_ci = ez->expression(ezSAT::OpOr, undef_ci);
- int undef_co_bit = ez->OR(undef_any_p, undef_any_g, undef_any_ci);
-
- std::vector<int> undef_co_bits(undef_co.size(), undef_co_bit);
- ez->assume(ez->vec_eq(undef_co_bits, undef_co));
-
- undefGating(co, yy, undef_co);
- }
- return true;
- }
-
- if (cell->type == ID($alu))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> x = importDefSigSpec(cell->getPort(ID::X), timestep);
- std::vector<int> ci = importDefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> bi = importDefSigSpec(cell->getPort(ID::BI), timestep);
- std::vector<int> co = importDefSigSpec(cell->getPort(ID::CO), timestep);
-
- extendSignalWidth(a, b, y, cell);
- extendSignalWidth(a, b, x, cell);
- extendSignalWidth(a, b, co, cell);
-
- std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
- std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
- std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
-
- log_assert(GetSize(y) == GetSize(x));
- log_assert(GetSize(y) == GetSize(co));
- log_assert(GetSize(ci) == 1);
- log_assert(GetSize(bi) == 1);
-
- for (int i = 0; i < GetSize(y); i++)
- {
- int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
- ez->SET(def_x.at(i), ez->XOR(s1, s2));
- ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
- ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
- }
-
- if (model_undef)
- {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
- std::vector<int> undef_ci = importUndefSigSpec(cell->getPort(ID::CI), timestep);
- std::vector<int> undef_bi = importUndefSigSpec(cell->getPort(ID::BI), timestep);
-
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- std::vector<int> undef_x = importUndefSigSpec(cell->getPort(ID::X), timestep);
- std::vector<int> undef_co = importUndefSigSpec(cell->getPort(ID::CO), timestep);
-
- extendSignalWidth(undef_a, undef_b, undef_y, cell);
- extendSignalWidth(undef_a, undef_b, undef_x, cell);
- extendSignalWidth(undef_a, undef_b, undef_co, cell);
-
- std::vector<int> all_inputs_undef;
- all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
- all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
- int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
-
- for (int i = 0; i < GetSize(undef_y); i++) {
- ez->SET(undef_y.at(i), undef_any);
- ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
- ez->SET(undef_co.at(i), undef_any);
- }
-
- undefGating(y, def_y, undef_y);
- undefGating(x, def_x, undef_x);
- undefGating(co, def_co, undef_co);
- }
- return true;
- }
-
- if (cell->type == ID($slice))
- {
- RTLIL::SigSpec a = cell->getPort(ID::A);
- RTLIL::SigSpec y = cell->getPort(ID::Y);
- ez->assume(signals_eq(a.extract(cell->parameters.at(ID::OFFSET).as_int(), y.size()), y, timestep));
- return true;
- }
-
- if (cell->type == ID($concat))
- {
- RTLIL::SigSpec a = cell->getPort(ID::A);
- RTLIL::SigSpec b = cell->getPort(ID::B);
- RTLIL::SigSpec y = cell->getPort(ID::Y);
-
- RTLIL::SigSpec ab = a;
- ab.append(b);
-
- ez->assume(signals_eq(ab, y, timestep));
- return true;
- }
-
- if (timestep > 0 && cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
- {
- if (timestep == 1)
- {
- initial_state.add((*sigmap)(cell->getPort(ID::Q)));
- }
- else
- {
- std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
- std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
-
- std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
- ez->assume(ez->vec_eq(d, qq));
-
- if (model_undef)
- {
- std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
- std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
-
- ez->assume(ez->vec_eq(undef_d, undef_q));
- undefGating(q, qq, undef_q);
- }
- }
- return true;
- }
-
- if (cell->type == ID($anyconst))
- {
- if (timestep < 2)
- return true;
-
- std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1);
- std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep);
-
- std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
- ez->assume(ez->vec_eq(d, qq));
-
- if (model_undef)
- {
- std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1);
- std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep);
-
- ez->assume(ez->vec_eq(undef_d, undef_q));
- undefGating(q, qq, undef_q);
- }
- return true;
- }
-
- if (cell->type == ID($anyseq))
- {
- return true;
- }
-
- if (cell->type.in(ID($_BUF_), ID($equiv)))
- {
- std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(a, y, cell);
-
- std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
- ez->assume(ez->vec_eq(a, yy));
-
- if (model_undef) {
- std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- extendSignalWidthUnary(undef_a, undef_y, cell, false);
- ez->assume(ez->vec_eq(undef_a, undef_y));
- undefGating(y, yy, undef_y);
- }
- return true;
- }
-
- if (cell->type == ID($initstate))
- {
- auto key = make_pair(prefix, timestep);
- if (initstates.count(key) == 0)
- initstates[key] = false;
-
- std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
- log_assert(GetSize(y) == 1);
- ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
-
- if (model_undef) {
- std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
- log_assert(GetSize(undef_y) == 1);
- ez->SET(undef_y[0], ez->CONST_FALSE);
- }
-
- return true;
- }
-
- if (cell->type == ID($assert))
- {
- std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
- asserts_a[pf].append((*sigmap)(cell->getPort(ID::A)));
- asserts_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
- return true;
- }
-
- if (cell->type == ID($assume))
- {
- std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
- assumes_a[pf].append((*sigmap)(cell->getPort(ID::A)));
- assumes_en[pf].append((*sigmap)(cell->getPort(ID::EN)));
- return true;
- }
-
- // Unsupported internal cell types: $pow $lut
- // .. and all sequential cells except $dff and $_DFF_[NP]_
- return false;
- }
+ bool importCell(RTLIL::Cell *cell, int timestep = -1);
};
YOSYS_NAMESPACE_END
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index 2ec3dca0c..8986c8091 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -713,7 +713,7 @@ extern Tcl_Interp *yosys_get_tcl_interp()
struct TclPass : public Pass {
TclPass() : Pass("tcl", "execute a TCL script file") { }
- void help() YS_OVERRIDE {
+ void help() override {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" tcl <filename> [args]\n");
@@ -730,7 +730,7 @@ struct TclPass : public Pass {
log("the standard $argc and $argv variables.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *) override {
if (args.size() < 2)
log_cmd_error("Missing script file.\n");
@@ -1050,6 +1050,8 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
if (command == "auto") {
if (filename.size() > 2 && filename.compare(filename.size()-2, std::string::npos, ".v") == 0)
command = "verilog";
+ else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".sv") == 0)
+ command = "verilog -sv";
else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0)
command = "ilang";
else if (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".cc") == 0)
@@ -1220,7 +1222,7 @@ void shell(RTLIL::Design *design)
struct ShellPass : public Pass {
ShellPass() : Pass("shell", "enter interactive command mode") { }
- void help() YS_OVERRIDE {
+ void help() override {
log("\n");
log(" shell\n");
log("\n");
@@ -1252,7 +1254,7 @@ struct ShellPass : public Pass {
log("Press Ctrl-D or type 'exit' to leave the interactive shell.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override {
extra_args(args, 1, design, false);
shell(design);
}
@@ -1261,7 +1263,7 @@ struct ShellPass : public Pass {
#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
struct HistoryPass : public Pass {
HistoryPass() : Pass("history", "show last interactive commands") { }
- void help() YS_OVERRIDE {
+ void help() override {
log("\n");
log(" history\n");
log("\n");
@@ -1270,7 +1272,7 @@ struct HistoryPass : public Pass {
log("from executed scripts.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override {
extra_args(args, 1, design, false);
#ifdef YOSYS_ENABLE_READLINE
for(HIST_ENTRY **list = history_list(); *list != NULL; list++)
@@ -1285,7 +1287,7 @@ struct HistoryPass : public Pass {
struct ScriptCmdPass : public Pass {
ScriptCmdPass() : Pass("script", "execute commands from file or wire") { }
- void help() YS_OVERRIDE {
+ void help() override {
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" script <filename> [<from_label>:<to_label>]\n");
@@ -1308,7 +1310,7 @@ struct ScriptCmdPass : public Pass {
log("'-module' mode can be exited by using the 'cd' command.\n");
log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool scriptwire = false;
diff --git a/kernel/yosys.h b/kernel/yosys.h
index c922faf26..f1646d6bc 100644
--- a/kernel/yosys.h
+++ b/kernel/yosys.h
@@ -117,11 +117,11 @@ extern Tcl_Obj *Tcl_ObjSetVar2(Tcl_Interp *interp, Tcl_Obj *part1Ptr, Tcl_Obj *p
# define PATH_MAX MAX_PATH
# define isatty _isatty
# define fileno _fileno
-# else
-// mingw includes `wingdi.h` which defines a TRANSPARENT macro
-// that conflicts with X(TRANSPARENT) entry in kernel/constids.inc
-# undef TRANSPARENT
# endif
+
+// mingw and msvc include `wingdi.h` which defines a TRANSPARENT macro
+// that conflicts with X(TRANSPARENT) entry in kernel/constids.inc
+# undef TRANSPARENT
#endif
#ifndef PATH_MAX
@@ -136,23 +136,20 @@ extern Tcl_Obj *Tcl_ObjSetVar2(Tcl_Interp *interp, Tcl_Obj *part1Ptr, Tcl_Obj *p
#define YOSYS_NAMESPACE_PREFIX Yosys::
#define USING_YOSYS_NAMESPACE using namespace Yosys;
-#if __cplusplus >= 201103L
-# define YS_OVERRIDE override
-# define YS_FINAL final
-#else
-# define YS_OVERRIDE
-# define YS_FINAL
-#endif
-
#if defined(__GNUC__) || defined(__clang__)
# define YS_ATTRIBUTE(...) __attribute__((__VA_ARGS__))
-# define YS_NORETURN
#elif defined(_MSC_VER)
# define YS_ATTRIBUTE(...)
-# define YS_NORETURN __declspec(noreturn)
#else
# define YS_ATTRIBUTE(...)
-# define YS_NORETURN
+#endif
+
+#if __cplusplus >= 201703L
+# define YS_MAYBE_UNUSED [[maybe_unused]];
+#elif defined(__GNUC__) || defined(__clang__)
+# define YS_MAYBE_UNUSED __attribute__((__unused__))
+#else
+# define YS_MAYBE_UNUSED
#endif
#if __cplusplus >= 201703L
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 08:38:11 +0000