aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/btor/.gitignore1
-rw-r--r--backends/btor/btor.cc26
-rwxr-xr-x[-rw-r--r--]backends/btor/test_cells.sh4
-rw-r--r--backends/cxxrtl/cxxrtl.h24
-rw-r--r--backends/cxxrtl/cxxrtl_backend.cc112
-rw-r--r--backends/cxxrtl/cxxrtl_capi.h72
-rw-r--r--backends/ilang/Makefile.inc3
-rw-r--r--backends/intersynth/intersynth.cc4
-rw-r--r--backends/rtlil/Makefile.inc3
-rw-r--r--backends/rtlil/rtlil_backend.cc (renamed from backends/ilang/ilang_backend.cc)65
-rw-r--r--backends/rtlil/rtlil_backend.h (renamed from backends/ilang/ilang_backend.h)8
-rw-r--r--backends/smt2/smt2.cc31
-rw-r--r--backends/smv/.gitignore1
-rw-r--r--backends/verilog/verilog_backend.cc10
14 files changed, 273 insertions, 91 deletions
diff --git a/backends/btor/.gitignore b/backends/btor/.gitignore
new file mode 100644
index 000000000..d23d492d7
--- /dev/null
+++ b/backends/btor/.gitignore
@@ -0,0 +1 @@
+/test_cells.tmp/
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index e5da6c1e7..5abab8978 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -205,9 +205,8 @@ struct BtorWorker
if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor";
log_assert(!btor_op.empty());
- int width = GetSize(cell->getPort(ID::Y));
- width = std::max(width, GetSize(cell->getPort(ID::A)));
- width = std::max(width, GetSize(cell->getPort(ID::B)));
+ int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
+ int width = std::max(width_ay, GetSize(cell->getPort(ID::B)));
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
@@ -224,11 +223,23 @@ struct BtorWorker
int sid = get_bv_sid(width);
int nid;
+ int nid_a;
+ if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) {
+ // sign-extend A up to the width of Y
+ int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed);
+
+ // zero-extend the rest
+ int zeroes = get_sig_nid(Const(0, width-width_ay));
+ nid_a = next_nid++;
+ btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded);
+ } else {
+ nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+ }
+
+ int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
+
if (btor_op == "shift")
{
- int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
- int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
-
int nid_r = next_nid++;
btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
@@ -248,9 +259,6 @@ struct BtorWorker
}
else
{
- int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
- int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
-
nid = next_nid++;
btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
}
diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh
index 3f077201a..0a011932d 100644..100755
--- a/backends/btor/test_cells.sh
+++ b/backends/btor/test_cells.sh
@@ -6,7 +6,7 @@ rm -rf test_cells.tmp
mkdir -p test_cells.tmp
cd test_cells.tmp
-../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor'
+../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx'
for fn in test_*.il; do
../../../yosys -p "
@@ -19,7 +19,7 @@ for fn in test_*.il; do
hierarchy -top main
write_btor ${fn%.il}.btor
"
- boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
+ btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
if grep " SATISFIABLE" ${fn%.il}.out; then
echo "Check failed for ${fn%.il}."
exit 1
diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index f0d7b9fc7..41089a153 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -452,10 +452,11 @@ struct value : public expr_base<value<Bits>> {
bool carry = CarryIn;
for (size_t n = 0; n < result.chunks; n++) {
result.data[n] = data[n] + (Invert ? ~other.data[n] : other.data[n]) + carry;
+ if (result.chunks - 1 == n)
+ result.data[result.chunks - 1] &= result.msb_mask;
carry = (result.data[n] < data[n]) ||
(result.data[n] == data[n] && carry);
}
- result.data[result.chunks - 1] &= result.msb_mask;
return {result, carry};
}
@@ -823,6 +824,7 @@ struct debug_alias {};
// To avoid violating strict aliasing rules, this structure has to be a subclass of the one used
// in the C API, or it would not be possible to cast between the pointers to these.
struct debug_item : ::cxxrtl_object {
+ // Object types.
enum : uint32_t {
VALUE = CXXRTL_VALUE,
WIRE = CXXRTL_WIRE,
@@ -830,13 +832,24 @@ struct debug_item : ::cxxrtl_object {
ALIAS = CXXRTL_ALIAS,
};
+ // Object flags.
+ enum : uint32_t {
+ INPUT = CXXRTL_INPUT,
+ OUTPUT = CXXRTL_OUTPUT,
+ INOUT = CXXRTL_INOUT,
+ DRIVEN_SYNC = CXXRTL_DRIVEN_SYNC,
+ DRIVEN_COMB = CXXRTL_DRIVEN_COMB,
+ UNDRIVEN = CXXRTL_UNDRIVEN,
+ };
+
debug_item(const ::cxxrtl_object &object) : cxxrtl_object(object) {}
template<size_t Bits>
- debug_item(value<Bits> &item, size_t lsb_offset = 0) {
+ debug_item(value<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) {
static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
"value<Bits> is not compatible with C layout");
type = VALUE;
+ flags = flags_;
width = Bits;
lsb_at = lsb_offset;
depth = 1;
@@ -850,6 +863,7 @@ struct debug_item : ::cxxrtl_object {
static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
"value<Bits> is not compatible with C layout");
type = VALUE;
+ flags = DRIVEN_COMB;
width = Bits;
lsb_at = lsb_offset;
depth = 1;
@@ -859,11 +873,12 @@ struct debug_item : ::cxxrtl_object {
}
template<size_t Bits>
- debug_item(wire<Bits> &item, size_t lsb_offset = 0) {
+ debug_item(wire<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) {
static_assert(sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) &&
sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t),
"wire<Bits> is not compatible with C layout");
type = WIRE;
+ flags = flags_;
width = Bits;
lsb_at = lsb_offset;
depth = 1;
@@ -877,6 +892,7 @@ struct debug_item : ::cxxrtl_object {
static_assert(sizeof(item.data[0]) == value<Width>::chunks * sizeof(chunk_t),
"memory<Width> is not compatible with C layout");
type = MEMORY;
+ flags = 0;
width = Width;
lsb_at = 0;
depth = item.data.size();
@@ -890,6 +906,7 @@ struct debug_item : ::cxxrtl_object {
static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
"value<Bits> is not compatible with C layout");
type = ALIAS;
+ flags = DRIVEN_COMB;
width = Bits;
lsb_at = lsb_offset;
depth = 1;
@@ -904,6 +921,7 @@ struct debug_item : ::cxxrtl_object {
sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t),
"wire<Bits> is not compatible with C layout");
type = ALIAS;
+ flags = DRIVEN_COMB;
width = Bits;
lsb_at = lsb_offset;
depth = 1;
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index 6d3c2f4f9..dfea04409 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -200,16 +200,12 @@ bool is_elidable_cell(RTLIL::IdString type)
ID($mux), ID($concat), ID($slice), ID($pmux));
}
-bool is_sync_ff_cell(RTLIL::IdString type)
-{
- return type.in(
- ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce));
-}
-
bool is_ff_cell(RTLIL::IdString type)
{
- return is_sync_ff_cell(type) || type.in(
- ID($adff), ID($adffe), ID($dffsr), ID($dffsre), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr));
+ return type.in(
+ ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce),
+ ID($adff), ID($adffe), ID($dffsr), ID($dffsre),
+ ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr));
}
bool is_internal_cell(RTLIL::IdString type)
@@ -277,6 +273,7 @@ struct FlowGraph {
std::vector<Node*> nodes;
dict<const RTLIL::Wire*, pool<Node*, hash_ptr_ops>> wire_comb_defs, wire_sync_defs, wire_uses;
dict<const RTLIL::Wire*, bool> wire_def_elidable, wire_use_elidable;
+ dict<RTLIL::SigBit, bool> bit_has_state;
~FlowGraph()
{
@@ -284,17 +281,24 @@ struct FlowGraph {
delete node;
}
- void add_defs(Node *node, const RTLIL::SigSpec &sig, bool fully_sync, bool elidable)
+ void add_defs(Node *node, const RTLIL::SigSpec &sig, bool is_ff, bool elidable)
{
for (auto chunk : sig.chunks())
if (chunk.wire) {
- if (fully_sync)
+ if (is_ff) {
+ // A sync def means that a wire holds design state because it is driven directly by
+ // a flip-flop output. Such a wire can never be unbuffered.
wire_sync_defs[chunk.wire].insert(node);
- else
+ } else {
+ // A comb def means that a wire doesn't hold design state. It might still be connected,
+ // indirectly, to a flip-flop output.
wire_comb_defs[chunk.wire].insert(node);
+ }
}
+ for (auto bit : sig.bits())
+ bit_has_state[bit] |= is_ff;
// Only comb defs of an entire wire in the right order can be elided.
- if (!fully_sync && sig.is_wire())
+ if (!is_ff && sig.is_wire())
wire_def_elidable[sig.as_wire()] = elidable;
}
@@ -322,7 +326,7 @@ struct FlowGraph {
// Connections
void add_connect_defs_uses(Node *node, const RTLIL::SigSig &conn)
{
- add_defs(node, conn.first, /*fully_sync=*/false, /*elidable=*/true);
+ add_defs(node, conn.first, /*is_ff=*/false, /*elidable=*/true);
add_uses(node, conn.second);
}
@@ -369,7 +373,7 @@ struct FlowGraph {
if (cell->output(conn.first))
if (is_cxxrtl_sync_port(cell, conn.first)) {
// See note regarding elidability below.
- add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false);
+ add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false);
}
}
@@ -378,18 +382,18 @@ struct FlowGraph {
for (auto conn : cell->connections()) {
if (cell->output(conn.first)) {
if (is_elidable_cell(cell->type))
- add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/true);
- else if (is_sync_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool()))
- add_defs(node, conn.second, /*fully_sync=*/true, /*elidable=*/false);
+ add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/true);
+ else if (is_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool()))
+ add_defs(node, conn.second, /*is_ff=*/true, /*elidable=*/false);
else if (is_internal_cell(cell->type))
- add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false);
+ add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false);
else if (!is_cxxrtl_sync_port(cell, conn.first)) {
// Although at first it looks like outputs of user-defined cells may always be elided, the reality is
// more complex. Fully sync outputs produce no defs and so don't participate in elision. Fully comb
// outputs are assigned in a different way depending on whether the cell's eval() immediately converged.
// Unknown/mixed outputs could be elided, but should be rare in practical designs and don't justify
// the infrastructure required to elide outputs of cells with many of them.
- add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false);
+ add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false);
}
}
if (cell->input(conn.first))
@@ -427,7 +431,7 @@ struct FlowGraph {
void add_case_defs_uses(Node *node, const RTLIL::CaseRule *case_)
{
for (auto &action : case_->actions) {
- add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false);
+ add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false);
add_uses(node, action.second);
}
for (auto sub_switch : case_->switches) {
@@ -446,9 +450,9 @@ struct FlowGraph {
for (auto sync : process->syncs)
for (auto action : sync->actions) {
if (sync->type == RTLIL::STp || sync->type == RTLIL::STn || sync->type == RTLIL::STe)
- add_defs(node, action.first, /*is_sync=*/true, /*elidable=*/false);
+ add_defs(node, action.first, /*is_ff=*/true, /*elidable=*/false);
else
- add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false);
+ add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false);
add_uses(node, action.second);
}
}
@@ -549,6 +553,7 @@ struct CxxrtlWorker {
pool<const RTLIL::Wire*> localized_wires;
dict<const RTLIL::Wire*, const RTLIL::Wire*> debug_alias_wires;
dict<const RTLIL::Wire*, RTLIL::Const> debug_const_wires;
+ dict<RTLIL::SigBit, bool> bit_has_state;
dict<const RTLIL::Module*, pool<std::string>> blackbox_specializations;
dict<const RTLIL::Module*, bool> eval_converges;
@@ -1142,7 +1147,7 @@ struct CxxrtlWorker {
}
// The generated code has two bounds checks; one in an assertion, and another that guards the read.
// This is done so that the code does not invoke undefined behavior under any conditions, but nevertheless
- // loudly crashes if an illegal condition is encountered. The assert may be turned off with -NDEBUG not
+ // loudly crashes if an illegal condition is encountered. The assert may be turned off with -DNDEBUG not
// just for release builds, but also to make sure the simulator (which is presumably embedded in some
// larger program) will never crash the code that calls into it.
//
@@ -1635,6 +1640,10 @@ struct CxxrtlWorker {
size_t count_alias_wires = 0;
size_t count_member_wires = 0;
size_t count_skipped_wires = 0;
+ size_t count_driven_sync = 0;
+ size_t count_driven_comb = 0;
+ size_t count_undriven = 0;
+ size_t count_mixed_driver = 0;
inc_indent();
f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n";
for (auto wire : module->wires()) {
@@ -1660,9 +1669,55 @@ struct CxxrtlWorker {
count_alias_wires++;
} else if (!localized_wires.count(wire)) {
// Member wire
+ std::vector<std::string> flags;
+
+ if (wire->port_input && wire->port_output)
+ flags.push_back("INOUT");
+ else if (wire->port_input)
+ flags.push_back("INPUT");
+ else if (wire->port_output)
+ flags.push_back("OUTPUT");
+
+ bool has_driven_sync = false;
+ bool has_driven_comb = false;
+ bool has_undriven = false;
+ SigSpec sig(wire);
+ for (auto bit : sig.bits())
+ if (!bit_has_state.count(bit))
+ has_undriven = true;
+ else if (bit_has_state[bit])
+ has_driven_sync = true;
+ else
+ has_driven_comb = true;
+ if (has_driven_sync)
+ flags.push_back("DRIVEN_SYNC");
+ if (has_driven_sync && !has_driven_comb && !has_undriven)
+ count_driven_sync++;
+ if (has_driven_comb)
+ flags.push_back("DRIVEN_COMB");
+ if (!has_driven_sync && has_driven_comb && !has_undriven)
+ count_driven_comb++;
+ if (has_undriven)
+ flags.push_back("UNDRIVEN");
+ if (!has_driven_sync && !has_driven_comb && has_undriven)
+ count_undriven++;
+ if (has_driven_sync + has_driven_comb + has_undriven > 1)
+ count_mixed_driver++;
+
f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire));
f << ", debug_item(" << mangle(wire) << ", ";
- f << wire->start_offset << "));\n";
+ f << wire->start_offset;
+ bool first = true;
+ for (auto flag : flags) {
+ if (first) {
+ first = false;
+ f << ", ";
+ } else {
+ f << "|";
+ }
+ f << "debug_item::" << flag;
+ }
+ f << "));\n";
count_member_wires++;
} else {
count_skipped_wires++;
@@ -1690,7 +1745,11 @@ struct CxxrtlWorker {
log_debug(" Public wires: %zu, of which:\n", count_public_wires);
log_debug(" Const wires: %zu\n", count_const_wires);
log_debug(" Alias wires: %zu\n", count_alias_wires);
- log_debug(" Member wires: %zu\n", count_member_wires);
+ log_debug(" Member wires: %zu, of which:\n", count_member_wires);
+ log_debug(" Driven sync: %zu\n", count_driven_sync);
+ log_debug(" Driven comb: %zu\n", count_driven_comb);
+ log_debug(" Undriven: %zu\n", count_undriven);
+ log_debug(" Mixed driver: %zu\n", count_mixed_driver);
log_debug(" Other wires: %zu (no debug information)\n", count_skipped_wires);
}
@@ -2209,6 +2268,9 @@ struct CxxrtlWorker {
eval_converges[module] = feedback_wires.empty() && buffered_comb_wires.empty();
+ for (auto item : flow.bit_has_state)
+ bit_has_state.insert(item);
+
if (debug_info) {
// Find wires that alias other wires or are tied to a constant; debug information can be enriched with these
// at essentially zero additional cost.
diff --git a/backends/cxxrtl/cxxrtl_capi.h b/backends/cxxrtl/cxxrtl_capi.h
index 1f1942803..385d6dcf3 100644
--- a/backends/cxxrtl/cxxrtl_capi.h
+++ b/backends/cxxrtl/cxxrtl_capi.h
@@ -73,6 +73,10 @@ int cxxrtl_commit(cxxrtl_handle handle);
size_t cxxrtl_step(cxxrtl_handle handle);
// Type of a simulated object.
+//
+// The type of a simulated object indicates the way it is stored and the operations that are legal
+// to perform on it (i.e. won't crash the simulation). It says very little about object semantics,
+// which is specified through flags.
enum cxxrtl_type {
// Values correspond to singly buffered netlist nodes, i.e. nodes driven exclusively by
// combinatorial cells, or toplevel input nodes.
@@ -86,7 +90,8 @@ enum cxxrtl_type {
CXXRTL_VALUE = 0,
// Wires correspond to doubly buffered netlist nodes, i.e. nodes driven, at least in part, by
- // storage cells, or by combinatorial cells that are a part of a feedback path.
+ // storage cells, or by combinatorial cells that are a part of a feedback path. They are also
+ // present in non-optimized builds.
//
// Wires can be inspected via the `curr` pointer and modified via the `next` pointer (which are
// distinct for wires). Note that changes to the bits driven by combinatorial cells will be
@@ -103,7 +108,7 @@ enum cxxrtl_type {
CXXRTL_MEMORY = 2,
// Aliases correspond to netlist nodes driven by another node such that their value is always
- // exactly equal, or driven by a constant value.
+ // exactly equal.
//
// Aliases can be inspected via the `curr` pointer. They cannot be modified, and the `next`
// pointer is always NULL.
@@ -112,6 +117,66 @@ enum cxxrtl_type {
// More object types may be added in the future, but the existing ones will never change.
};
+// Flags of a simulated object.
+//
+// The flags of a simulated object indicate its role in the netlist:
+// * The flags `CXXRTL_INPUT` and `CXXRTL_OUTPUT` designate module ports.
+// * The flags `CXXRTL_DRIVEN_SYNC`, `CXXRTL_DRIVEN_COMB`, and `CXXRTL_UNDRIVEN` specify
+// the semantics of node state. An object with several of these flags set has different bits
+// follow different semantics.
+enum cxxrtl_flag {
+ // Node is a module input port.
+ //
+ // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined
+ // with `CXXRTL_OUTPUT`, as well as other flags.
+ CXXRTL_INPUT = 1 << 0,
+
+ // Node is a module output port.
+ //
+ // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with `CXXRTL_INPUT`,
+ // as well as other flags.
+ CXXRTL_OUTPUT = 1 << 1,
+
+ // Node is a module inout port.
+ //
+ // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with other flags.
+ CXXRTL_INOUT = (CXXRTL_INPUT|CXXRTL_OUTPUT),
+
+ // Node has bits that are driven by a storage cell.
+ //
+ // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with
+ // `CXXRTL_DRIVEN_COMB` and `CXXRTL_UNDRIVEN`, as well as other flags.
+ //
+ // This flag is set on wires that have bits connected directly to the output of a flip-flop or
+ // a latch, and hold its state. Many `CXXRTL_WIRE` objects may not have the `CXXRTL_DRIVEN_SYNC`
+ // flag set; for example, output ports and feedback wires generally won't. Writing to the `next`
+ // pointer of these wires updates stored state, and for designs without combinatorial loops,
+ // capturing the value from every of these wires through the `curr` pointer creates a complete
+ // snapshot of the design state.
+ CXXRTL_DRIVEN_SYNC = 1 << 2,
+
+ // Node has bits that are driven by a combinatorial cell or another node.
+ //
+ // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined
+ // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_UNDRIVEN`, as well as other flags.
+ //
+ // This flag is set on objects that have bits connected to the output of a combinatorial cell,
+ // or directly to another node. For designs without combinatorial loops, writing to such bits
+ // through the `next` pointer (if it is not NULL) has no effect.
+ CXXRTL_DRIVEN_COMB = 1 << 3,
+
+ // Node has bits that are not driven.
+ //
+ // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined
+ // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_DRIVEN_COMB`, as well as other flags.
+ //
+ // This flag is set on objects that have bits not driven by an output of any cell or by another
+ // node, such as inputs and dangling wires.
+ CXXRTL_UNDRIVEN = 1 << 4,
+
+ // More object flags may be added in the future, but the existing ones will never change.
+};
+
// Description of a simulated object.
//
// The `data` array can be accessed directly to inspect and, if applicable, modify the bits
@@ -123,6 +188,9 @@ struct cxxrtl_object {
// determines all other properties of the object.
uint32_t type; // actually `enum cxxrtl_type`
+ // Flags of the object.
+ uint32_t flags; // actually bit mask of `enum cxxrtl_flags`
+
// Width of the object in bits.
size_t width;
diff --git a/backends/ilang/Makefile.inc b/backends/ilang/Makefile.inc
deleted file mode 100644
index 52fc2b891..000000000
--- a/backends/ilang/Makefile.inc
+++ /dev/null
@@ -1,3 +0,0 @@
-
-OBJS += backends/ilang/ilang_backend.o
-
diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc
index 98a14173b..a6b36de6c 100644
--- a/backends/intersynth/intersynth.cc
+++ b/backends/intersynth/intersynth.cc
@@ -59,7 +59,7 @@ struct IntersynthBackend : public Backend {
log(" do not generate celltypes and conntypes commands. i.e. just output\n");
log(" the netlists. this is used for postsilicon synthesis.\n");
log("\n");
- log(" -lib <verilog_or_ilang_file>\n");
+ log(" -lib <verilog_or_rtlil_file>\n");
log(" Use the specified library file for determining whether cell ports are\n");
log(" inputs or outputs. This option can be used multiple times to specify\n");
log(" more than one library.\n");
@@ -108,7 +108,7 @@ struct IntersynthBackend : public Backend {
if (f.fail())
log_error("Can't open lib file `%s'.\n", filename.c_str());
RTLIL::Design *lib = new RTLIL::Design;
- Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "ilang" : "verilog"));
+ Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "rtlil" : "verilog"));
libs.push_back(lib);
}
diff --git a/backends/rtlil/Makefile.inc b/backends/rtlil/Makefile.inc
new file mode 100644
index 000000000..f691282ca
--- /dev/null
+++ b/backends/rtlil/Makefile.inc
@@ -0,0 +1,3 @@
+
+OBJS += backends/rtlil/rtlil_backend.o
+
diff --git a/backends/ilang/ilang_backend.cc b/backends/rtlil/rtlil_backend.cc
index aa5a175ca..01b4bde53 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -18,19 +18,19 @@
* ---
*
* A very simple and straightforward backend for the RTLIL text
- * representation (as understood by the 'ilang' frontend).
+ * representation.
*
*/
-#include "ilang_backend.h"
+#include "rtlil_backend.h"
#include "kernel/yosys.h"
#include <errno.h>
USING_YOSYS_NAMESPACE
-using namespace ILANG_BACKEND;
+using namespace RTLIL_BACKEND;
YOSYS_NAMESPACE_BEGIN
-void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint)
+void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint)
{
if (width < 0)
width = data.bits.size() - offset;
@@ -83,7 +83,7 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
}
}
-void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint)
+void RTLIL_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint)
{
if (chunk.wire == NULL) {
dump_const(f, chunk.data, chunk.width, chunk.offset, autoint);
@@ -97,7 +97,7 @@ void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk,
}
}
-void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint)
+void RTLIL_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint)
{
if (sig.is_chunk()) {
dump_sigchunk(f, sig.as_chunk(), autoint);
@@ -111,7 +111,7 @@ void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, boo
}
}
-void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire)
+void RTLIL_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire)
{
for (auto &it : wire->attributes) {
f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
@@ -136,7 +136,7 @@ void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::
f << stringf("%s\n", wire->name.c_str());
}
-void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory)
+void RTLIL_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory)
{
for (auto &it : memory->attributes) {
f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
@@ -153,7 +153,7 @@ void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL
f << stringf("%s\n", memory->name.c_str());
}
-void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
+void RTLIL_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
{
for (auto &it : cell->attributes) {
f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str());
@@ -177,7 +177,7 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::
f << stringf("%s" "end\n", indent.c_str());
}
-void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs)
+void RTLIL_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs)
{
for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it)
{
@@ -192,7 +192,7 @@ void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, con
dump_proc_switch(f, indent, *it);
}
-void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw)
+void RTLIL_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw)
{
for (auto it = sw->attributes.begin(); it != sw->attributes.end(); ++it) {
f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
@@ -225,7 +225,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
f << stringf("%s" "end\n", indent.c_str());
}
-void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy)
+void RTLIL_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy)
{
f << stringf("%s" "sync ", indent.c_str());
switch (sy->type) {
@@ -251,7 +251,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
}
}
-void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc)
+void RTLIL_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc)
{
for (auto it = proc->attributes.begin(); it != proc->attributes.end(); ++it) {
f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str());
@@ -265,7 +265,7 @@ void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::
f << stringf("%s" "end\n", indent.c_str());
}
-void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right)
+void RTLIL_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right)
{
f << stringf("%s" "connect ", indent.c_str());
dump_sigspec(f, left);
@@ -274,7 +274,7 @@ void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::
f << stringf("\n");
}
-void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n)
+void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n)
{
bool print_header = flag_m || design->selected_whole_module(module->name);
bool print_body = !flag_n || !design->selected_whole_module(module->name);
@@ -360,7 +360,7 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
f << stringf("%s" "end\n", indent.c_str());
}
-void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n)
+void RTLIL_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n)
{
int init_autoidx = autoidx;
@@ -396,15 +396,15 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
YOSYS_NAMESPACE_END
PRIVATE_NAMESPACE_BEGIN
-struct IlangBackend : public Backend {
- IlangBackend() : Backend("ilang", "write design to ilang file") { }
+struct RTLILBackend : public Backend {
+ RTLILBackend() : Backend("rtlil", "write design to RTLIL file") { }
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" write_ilang [filename]\n");
+ log(" write_rtlil [filename]\n");
log("\n");
- log("Write the current design to an 'ilang' file. (ilang is a text representation\n");
+ log("Write the current design to an RTLIL file. (RTLIL is a text representation\n");
log("of a design in yosys's internal format.)\n");
log("\n");
log(" -selected\n");
@@ -415,7 +415,7 @@ struct IlangBackend : public Backend {
{
bool selected = false;
- log_header(design, "Executing ILANG backend.\n");
+ log_header(design, "Executing RTLIL backend.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -432,12 +432,27 @@ struct IlangBackend : public Backend {
log("Output filename: %s\n", filename.c_str());
*f << stringf("# Generated by %s\n", yosys_version_str);
- ILANG_BACKEND::dump_design(*f, design, selected, true, false);
+ RTLIL_BACKEND::dump_design(*f, design, selected, true, false);
+ }
+} RTLILBackend;
+
+struct IlangBackend : public Backend {
+ IlangBackend() : Backend("ilang", "(deprecated) alias of write_rtlil") { }
+ void help() override
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log("See `help write_rtlil`.\n");
+ log("\n");
+ }
+ void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
+ {
+ RTLILBackend.execute(f, filename, args, design);
}
} IlangBackend;
struct DumpPass : public Pass {
- DumpPass() : Pass("dump", "print parts of the design in ilang format") { }
+ DumpPass() : Pass("dump", "print parts of the design in RTLIL format") { }
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -445,7 +460,7 @@ struct DumpPass : public Pass {
log(" dump [options] [selection]\n");
log("\n");
log("Write the selected parts of the design to the console or specified file in\n");
- log("ilang format.\n");
+ log("RTLIL format.\n");
log("\n");
log(" -m\n");
log(" also dump the module headers, even if only parts of a single\n");
@@ -508,7 +523,7 @@ struct DumpPass : public Pass {
f = &buf;
}
- ILANG_BACKEND::dump_design(*f, design, true, flag_m, flag_n);
+ RTLIL_BACKEND::dump_design(*f, design, true, flag_m, flag_n);
if (!filename.empty()) {
delete f;
diff --git a/backends/ilang/ilang_backend.h b/backends/rtlil/rtlil_backend.h
index 97dcbb628..77eea353c 100644
--- a/backends/ilang/ilang_backend.h
+++ b/backends/rtlil/rtlil_backend.h
@@ -18,19 +18,19 @@
* ---
*
* A very simple and straightforward backend for the RTLIL text
- * representation (as understood by the 'ilang' frontend).
+ * representation.
*
*/
-#ifndef ILANG_BACKEND_H
-#define ILANG_BACKEND_H
+#ifndef RTLIL_BACKEND_H
+#define RTLIL_BACKEND_H
#include "kernel/yosys.h"
#include <stdio.h>
YOSYS_NAMESPACE_BEGIN
-namespace ILANG_BACKEND {
+namespace RTLIL_BACKEND {
void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool autoint = true);
void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint = true);
void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint = true);
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a79c0bd99..4a53ce6d5 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -824,38 +824,49 @@ struct Smt2Worker
is_register = true;
if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire);
+ std::vector<std::string> comments;
if (wire->port_input)
- decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
if (wire->port_output)
- decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
if (is_register)
- decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
- decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
- decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
+ comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
if (bvmode && GetSize(sig) > 1) {
+ std::string sig_bv = get_bv(sig);
+ if (!comments.empty())
+ decls.insert(decls.end(), comments.begin(), comments.end());
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
- get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
+ get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
get_id(module), get_id(wire), get_id(module), get_id(wire)));
} else {
- for (int i = 0; i < GetSize(sig); i++)
+ std::vector<std::string> sig_bool;
+ for (int i = 0; i < GetSize(sig); i++) {
+ sig_bool.push_back(get_bool(sig[i]));
+ }
+ if (!comments.empty())
+ decls.insert(decls.end(), comments.begin(), comments.end());
+ for (int i = 0; i < GetSize(sig); i++) {
if (GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
- get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
} else {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
- get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
get_id(module), get_id(wire), get_id(module), get_id(wire)));
}
+ }
}
}
}
@@ -1392,7 +1403,7 @@ struct Smt2Backend : public Backend {
log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n");
log("\n");
log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
- log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n");
+ log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n");
log("\n");
log("---------------------------------------------------------------------------\n");
log("\n");
diff --git a/backends/smv/.gitignore b/backends/smv/.gitignore
new file mode 100644
index 000000000..d23d492d7
--- /dev/null
+++ b/backends/smv/.gitignore
@@ -0,0 +1 @@
+/test_cells.tmp/
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index a0e677d13..372f68ea5 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -750,21 +750,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf(" = ");
if (cell->getParam(ID::B_SIGNED).as_bool())
{
- f << stringf("$signed(");
- dump_sigspec(f, cell->getPort(ID::B));
- f << stringf(")");
+ dump_cell_expr_port(f, cell, "B", true);
f << stringf(" < 0 ? ");
- dump_sigspec(f, cell->getPort(ID::A));
+ dump_cell_expr_port(f, cell, "A", true);
f << stringf(" << - ");
dump_sigspec(f, cell->getPort(ID::B));
f << stringf(" : ");
- dump_sigspec(f, cell->getPort(ID::A));
+ dump_cell_expr_port(f, cell, "A", true);
f << stringf(" >> ");
dump_sigspec(f, cell->getPort(ID::B));
}
else
{
- dump_sigspec(f, cell->getPort(ID::A));
+ dump_cell_expr_port(f, cell, "A", true);
f << stringf(" >> ");
dump_sigspec(f, cell->getPort(ID::B));
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 19:57:59 +0000