aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/btor/btor.cc30
-rw-r--r--backends/smt2/smtio.py5
-rw-r--r--frontends/verilog/const2ast.cc2
-rw-r--r--passes/opt/opt_clean.cc6
-rw-r--r--techlibs/ecp5/cells_map.v40
-rw-r--r--techlibs/ecp5/cells_sim.v94
-rw-r--r--techlibs/xilinx/cells_sim.v2
7 files changed, 127 insertions, 52 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 511a11942..a507b120b 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -17,6 +17,11 @@
*
*/
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
#include "kernel/rtlil.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
@@ -875,9 +880,28 @@ struct BtorWorker
else
{
if (bit_cell.count(bit) == 0)
- log_error("No driver for signal bit %s.\n", log_signal(bit));
- export_cell(bit_cell.at(bit));
- log_assert(bit_nid.count(bit));
+ {
+ SigSpec s = bit;
+
+ while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+ bit_cell.count(sig[i+GetSize(s)]) == 0)
+ s.append(sig[i+GetSize(s)]);
+
+ log_warning("No driver for signal %s.\n", log_signal(s));
+
+ int sid = get_bv_sid(GetSize(s));
+ int nid = next_nid++;
+ btorf("%d input %d %s\n", nid, sid);
+ nid_width[nid] = GetSize(s);
+
+ i += GetSize(s)-1;
+ continue;
+ }
+ else
+ {
+ export_cell(bit_cell.at(bit));
+ log_assert(bit_nid.count(bit));
+ }
}
}
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index cea0fc56c..ae7968a1b 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -1043,7 +1043,10 @@ class MkVcd:
scope = scope[:-1]
while uipath[:-1] != scope:
- print("$scope module %s $end" % uipath[len(scope)], file=self.f)
+ scopename = uipath[len(scope)]
+ if scopename.startswith("$"):
+ scopename = "\\" + scopename
+ print("$scope module %s $end" % scopename, file=self.f)
scope.append(uipath[len(scope)])
if path in self.clocks and self.clocks[path][1] == "event":
diff --git a/frontends/verilog/const2ast.cc b/frontends/verilog/const2ast.cc
index 3a3634d34..f6a17b242 100644
--- a/frontends/verilog/const2ast.cc
+++ b/frontends/verilog/const2ast.cc
@@ -153,7 +153,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
{
if (warn_z) {
AstNode *ret = const2ast(code, case_type);
- if (std::find(ret->bits.begin(), ret->bits.end(), RTLIL::State::Sz) != ret->bits.end())
+ if (ret != nullptr && std::find(ret->bits.begin(), ret->bits.end(), RTLIL::State::Sz) != ret->bits.end())
log_warning("Yosys has only limited support for tri-state logic at the moment. (%s:%d)\n",
current_filename.c_str(), get_line_num());
return ret;
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index cfb0f788a..a8a8e0bc7 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -326,8 +326,8 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
if (wire->port_id != 0 || wire->get_bool_attribute("\\keep") || !initval.is_fully_undef()) {
// do not delete anything with "keep" or module ports or initialized wires
} else
- if (!purge_mode && check_public_name(wire->name)) {
- // do not get rid of public names unless in purge mode
+ if (!purge_mode && check_public_name(wire->name) && (raw_used_signals.check_any(s1) || used_signals.check_any(s2) || s1 != s2)) {
+ // do not get rid of public names unless in purge mode or if the wire is entirely unused, not even aliased
} else
if (!raw_used_signals.check_any(s1)) {
// delete wires that aren't used by anything directly
@@ -480,7 +480,7 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool verbose, bool
std::vector<RTLIL::Cell*> delcells;
for (auto cell : module->cells())
- if (cell->type.in("$pos", "$_BUF_")) {
+ if (cell->type.in("$pos", "$_BUF_") && !cell->has_keep_attr()) {
bool is_signed = cell->type == "$pos" && cell->getParam("\\A_SIGNED").as_bool();
RTLIL::SigSpec a = cell->getPort("\\A");
RTLIL::SigSpec y = cell->getPort("\\Y");
diff --git a/techlibs/ecp5/cells_map.v b/techlibs/ecp5/cells_map.v
index f6c71a03d..a90d5e034 100644
--- a/techlibs/ecp5/cells_map.v
+++ b/techlibs/ecp5/cells_map.v
@@ -47,6 +47,28 @@ module \$__DFFSE_NP1 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"
module \$__DFFSE_PP0 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule
module \$__DFFSE_PP1 (input D, C, E, R, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("CE"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(C), .CE(E), .LSR(R), .DI(D), .Q(Q)); endmodule
+// TODO: Diamond flip-flops
+// module FD1P3AX(); endmodule
+// module FD1P3AY(); endmodule
+// module FD1P3BX(); endmodule
+// module FD1P3DX(); endmodule
+// module FD1P3IX(); endmodule
+// module FD1P3JX(); endmodule
+// module FD1S3AX(); endmodule
+// module FD1S3AY(); endmodule
+module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
+module FD1S3DX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
+module FD1S3IX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
+module FD1S3JX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
+// module FL1P3AY(); endmodule
+// module FL1P3AZ(); endmodule
+// module FL1P3BX(); endmodule
+// module FL1P3DX(); endmodule
+// module FL1P3IY(); endmodule
+// module FL1P3JY(); endmodule
+// module FL1S3AX(); endmodule
+// module FL1S3AY(); endmodule
+
// Diamond I/O buffers
module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule
module IBPU (input I, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule
@@ -62,8 +84,22 @@ module BBPD (input I, T, output O, inout B); (* PULLMODE="DOWN" *) TRELLIS_IO #(
module ILVDS(input A, AN, output Z); TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(A), .O(Z)); endmodule
module OLVDS(input A, output Z, ZN); TRELLIS_IO #(.DIR("OUTPUT")) _TECHMAP_REPLACE_ (.B(Z), .I(A)); endmodule
-// For Diamond compatibility, FIXME: add all Diamond flipflop mappings
-module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
+// Diamond I/O registers
+module IFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+
+module OFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) _TECHMAP_REPLACE_ (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+
+// TODO: Diamond I/O latches
+// module IFS1S1B(input PD, D, SCLK, output Q); endmodule
+// module IFS1S1D(input CD, D, SCLK, output Q); endmodule
+// module IFS1S1I(input PD, D, SCLK, output Q); endmodule
+// module IFS1S1J(input CD, D, SCLK, output Q); endmodule
`ifndef NO_LUT
module \$lut (A, Y);
diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v
index 1e4002ee0..07fadfa10 100644
--- a/techlibs/ecp5/cells_sim.v
+++ b/techlibs/ecp5/cells_sim.v
@@ -251,18 +251,6 @@ module TRELLIS_FF(input CLK, LSR, CE, DI, M, output reg Q);
endmodule
// ---------------------------------------
-
-module OBZ(input I, T, output O);
-assign O = T ? 1'bz : I;
-endmodule
-
-// ---------------------------------------
-
-module IB(input I, output O);
-assign O = I;
-endmodule
-
-// ---------------------------------------
(* keep *)
module TRELLIS_IO(
inout B,
@@ -293,19 +281,6 @@ endmodule
// ---------------------------------------
-module OB(input I, output O);
-assign O = I;
-endmodule
-
-// ---------------------------------------
-
-module BB(input I, T, output O, inout B);
-assign B = T ? 1'bz : I;
-assign O = B;
-endmodule
-
-// ---------------------------------------
-
module INV(input A, output Z);
assign Z = !A;
endmodule
@@ -558,19 +533,56 @@ module DP16KD(
parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000;
endmodule
-// For Diamond compatibility, FIXME: add all Diamond flipflop mappings
-module FD1S3BX(input PD, D, CK, output Q);
- TRELLIS_FF #(
- .GSR("DISABLED"),
- .CEMUX("1"),
- .CLKMUX("CLK"),
- .LSRMUX("LSR"),
- .REGSET("SET"),
- .SRMODE("ASYNC")
- ) tff_i (
- .CLK(CK),
- .LSR(PD),
- .DI(D),
- .Q(Q)
- );
-endmodule
+// TODO: Diamond flip-flops
+// module FD1P3AX(); endmodule
+// module FD1P3AY(); endmodule
+// module FD1P3BX(); endmodule
+// module FD1P3DX(); endmodule
+// module FD1P3IX(); endmodule
+// module FD1P3JX(); endmodule
+// module FD1S3AX(); endmodule
+// module FD1S3AY(); endmodule
+module FD1S3BX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
+module FD1S3DX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
+module FD1S3IX(input CD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(CK), .LSR(CD), .DI(D), .Q(Q)); endmodule
+module FD1S3JX(input PD, D, CK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(CK), .LSR(PD), .DI(D), .Q(Q)); endmodule
+// module FL1P3AY(); endmodule
+// module FL1P3AZ(); endmodule
+// module FL1P3BX(); endmodule
+// module FL1P3DX(); endmodule
+// module FL1P3IY(); endmodule
+// module FL1P3JY(); endmodule
+// module FL1S3AX(); endmodule
+// module FL1S3AY(); endmodule
+
+// Diamond I/O buffers
+module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
+module IBPU (input I, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
+module IBPD (input I, output O); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("INPUT")) tio (.B(I), .O(O)); endmodule
+module OB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I)); endmodule
+module OBZ (input I, T, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
+module OBZPU(input I, T, output O); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
+module OBZPD(input I, T, output O); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(O), .I(I), .T(T)); endmodule
+module OBCO (input I, output OT, OC); OLVDS olvds (.A(I), .Z(OT), .ZN(OC)); endmodule
+module BB (input I, T, output O, inout B); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
+module BBPU (input I, T, output O, inout B); (* PULLMODE="UP" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
+module BBPD (input I, T, output O, inout B); (* PULLMODE="DOWN" *) TRELLIS_IO #(.DIR("BIDIR")) tio (.B(B), .I(I), .O(O), .T(T)); endmodule
+module ILVDS(input A, AN, output Z); TRELLIS_IO #(.DIR("INPUT")) tio (.B(A), .O(Z)); endmodule
+module OLVDS(input A, output Z, ZN); TRELLIS_IO #(.DIR("OUTPUT")) tio (.B(Z), .I(A)); endmodule
+
+// Diamond I/O registers
+module IFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module IFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+
+module OFS1P3BX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3DX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("ASYNC")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3IX(input CD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("RESET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(CD), .CE(SP), .DI(D), .Q(Q)); endmodule
+module OFS1P3JX(input PD, D, SP, SCLK, output Q); TRELLIS_FF #(.GSR("DISABLED"), .CEMUX("1"), .CLKMUX("CLK"), .LSRMUX("LSR"), .REGSET("SET"), .SRMODE("LSR_OVER_CE")) tff (.CLK(SCLK), .LSR(PD), .CE(SP), .DI(D), .Q(Q)); endmodule
+
+// TODO: Diamond I/O latches
+// module IFS1S1B(input PD, D, SCLK, output Q); endmodule
+// module IFS1S1D(input CD, D, SCLK, output Q); endmodule
+// module IFS1S1I(input PD, D, SCLK, output Q); endmodule
+// module IFS1S1J(input CD, D, SCLK, output Q); endmodule
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index 50d588a9e..f4598dcf4 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -282,7 +282,7 @@ module RAM32X1D (
output DPO, SPO,
input D, WCLK, WE,
input A0, A1, A2, A3, A4,
- input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4,
+ input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4
);
parameter INIT = 32'h0;
parameter IS_WCLK_INVERTED = 1'b0;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 19:48:06 +0000