mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Merge remote-tracking branch 'origin/eddie/fix1132' into xc7mux

Browse source
This commit is contained in:
Eddie Hung 2019-06-26 14:48:35 -07:00
commit 812469aaa3
9 changed files with 352 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

30
backends/btor/btor.cc
View file

@ -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/rtlil.h"
#include "kernel/register.h" #include "kernel/register.h"
#include "kernel/sigtools.h" #include "kernel/sigtools.h"
@ -875,9 +880,28 @@ struct BtorWorker
else else
{ {
if (bit_cell.count(bit) == 0) if (bit_cell.count(bit) == 0)
log_error("No driver for signal bit %s.\n", log_signal(bit)); {
export_cell(bit_cell.at(bit)); SigSpec s = bit;
log_assert(bit_nid.count(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));
}
} }
} }

5
backends/smt2/smtio.py
View file

@ -1043,7 +1043,10 @@ class MkVcd:
scope = scope[:-1] scope = scope[:-1]
while uipath[:-1] != scope: 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)]) scope.append(uipath[len(scope)])
if path in self.clocks and self.clocks[path][1] == "event": if path in self.clocks and self.clocks[path][1] == "event":

2
frontends/verilog/const2ast.cc
View file

@ -153,7 +153,7 @@ AstNode *VERILOG_FRONTEND::const2ast(std::string code, char case_type, bool warn
{ {
if (warn_z) { if (warn_z) {
AstNode *ret = const2ast(code, case_type); 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", log_warning("Yosys has only limited support for tri-state logic at the moment. (%s:%d)\n",
current_filename.c_str(), get_line_num()); current_filename.c_str(), get_line_num());
return ret; return ret;

6
passes/opt/opt_clean.cc
View file

@ -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()) { 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 // do not delete anything with "keep" or module ports or initialized wires
} else } else
if (!purge_mode && check_public_name(wire->name)) { 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 // do not get rid of public names unless in purge mode or if the wire is entirely unused, not even aliased
} else } else
if (!raw_used_signals.check_any(s1)) { if (!raw_used_signals.check_any(s1)) {
// delete wires that aren't used by anything directly // 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; std::vector<RTLIL::Cell*> delcells;
for (auto cell : module->cells()) 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(); bool is_signed = cell->type == "$pos" && cell->getParam("\\A_SIGNED").as_bool();
RTLIL::SigSpec a = cell->getPort("\\A"); RTLIL::SigSpec a = cell->getPort("\\A");
RTLIL::SigSpec y = cell->getPort("\\Y"); RTLIL::SigSpec y = cell->getPort("\\Y");

98
passes/techmap/muxcover.cc
View file

@ -324,13 +324,7 @@ struct MuxcoverWorker
ok = ok && follow_muxtree(G, tree, bit, "BBA"); ok = ok && follow_muxtree(G, tree, bit, "BBA");
ok = ok && follow_muxtree(H, tree, bit, "BBB"); ok = ok && follow_muxtree(H, tree, bit, "BBB");
ok = ok && follow_muxtree(S1, tree, bit, "AAS"); ok = ok && follow_muxtree(U1, tree, bit, "S");
ok = ok && follow_muxtree(S2, tree, bit, "ABS");
ok = ok && follow_muxtree(S3, tree, bit, "BAS");
ok = ok && follow_muxtree(S4, tree, bit, "BBS");
if (nodecode)
ok = ok && S1 == S2 && S2 == S3 && S3 == S4;
ok = ok && follow_muxtree(T1, tree, bit, "AS"); ok = ok && follow_muxtree(T1, tree, bit, "AS");
ok = ok && follow_muxtree(T2, tree, bit, "BS"); ok = ok && follow_muxtree(T2, tree, bit, "BS");
@ -338,7 +332,14 @@ struct MuxcoverWorker
if (nodecode) if (nodecode)
ok = ok && T1 == T2; ok = ok && T1 == T2;
ok = ok && follow_muxtree(U1, tree, bit, "S"); ok = ok && follow_muxtree(S1, tree, bit, "AAS");
ok = ok && follow_muxtree(S2, tree, bit, "ABS");
ok = ok && follow_muxtree(S3, tree, bit, "BAS");
ok = ok && follow_muxtree(S4, tree, bit, "BBS");
if (nodecode)
ok = ok && S1 == S2 && /*S2 == S3 &&*/ S3 == S4;
// ^^ Should already be checked by T1 == T2 above
if (ok) if (ok)
{ {
@ -353,12 +354,16 @@ struct MuxcoverWorker
mux.inputs.push_back(G); mux.inputs.push_back(G);
mux.inputs.push_back(H); mux.inputs.push_back(H);
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
mux.cost += prepare_decode_mux(T1, T2, U1, bit); mux.cost += prepare_decode_mux(T1, T2, U1, bit);
if (T1 != RTLIL::Sx) {
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
}
else
S1 = RTLIL::Sx;
mux.selects.push_back(S1); mux.selects.push_back(S1);
mux.selects.push_back(T1); mux.selects.push_back(T1);
mux.selects.push_back(U1); mux.selects.push_back(U1);
@ -397,6 +402,23 @@ struct MuxcoverWorker
ok = ok && follow_muxtree(O, tree, bit, "BBBA"); ok = ok && follow_muxtree(O, tree, bit, "BBBA");
ok = ok && follow_muxtree(P, tree, bit, "BBBB"); ok = ok && follow_muxtree(P, tree, bit, "BBBB");
ok = ok && follow_muxtree(V1, tree, bit, "S");
ok = ok && follow_muxtree(U1, tree, bit, "AS");
ok = ok && follow_muxtree(U2, tree, bit, "BS");
if (nodecode)
ok = ok && U1 == U2;
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
ok = ok && follow_muxtree(T3, tree, bit, "BAS");
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
if (nodecode)
ok = ok && T1 == T2 && /*T2 == T3 &&*/ T3 == T4;
// ^^ Should already be checked by U1 == U2 above
ok = ok && follow_muxtree(S1, tree, bit, "AAAS"); ok = ok && follow_muxtree(S1, tree, bit, "AAAS");
ok = ok && follow_muxtree(S2, tree, bit, "AABS"); ok = ok && follow_muxtree(S2, tree, bit, "AABS");
ok = ok && follow_muxtree(S3, tree, bit, "ABAS"); ok = ok && follow_muxtree(S3, tree, bit, "ABAS");
@ -407,23 +429,7 @@ struct MuxcoverWorker
ok = ok && follow_muxtree(S8, tree, bit, "BBBS"); ok = ok && follow_muxtree(S8, tree, bit, "BBBS");
if (nodecode) if (nodecode)
ok = ok && S1 == S2 && S2 == S3 && S3 == S4 && S4 == S5 && S5 == S6 && S6 == S7 && S7 == S8; ok = ok && S1 == S2 && /*S2 == S3 &&*/ S3 == S4 && /*S4 == S5 &&*/ S5 == S6 && /*S6 == S7 &&*/ S7 == S8;
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
ok = ok && follow_muxtree(T3, tree, bit, "BAS");
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
if (nodecode)
ok = ok && T1 == T2 && T2 == T3 && T3 == T4;
ok = ok && follow_muxtree(U1, tree, bit, "AS");
ok = ok && follow_muxtree(U2, tree, bit, "BS");
if (nodecode)
ok = ok && U1 == U2;
ok = ok && follow_muxtree(V1, tree, bit, "S");
if (ok) if (ok)
{ {
@ -446,20 +452,30 @@ struct MuxcoverWorker
mux.inputs.push_back(O); mux.inputs.push_back(O);
mux.inputs.push_back(P); mux.inputs.push_back(P);
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
mux.cost += prepare_decode_mux(S5, S6, T3, bit);
mux.cost += prepare_decode_mux(S7, S8, T4, bit);
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
mux.cost += prepare_decode_mux(S5, S7, U2, bit);
mux.cost += prepare_decode_mux(S1, S5, V1, bit);
mux.cost += prepare_decode_mux(T1, T2, U1, bit);
mux.cost += prepare_decode_mux(T3, T4, U2, bit);
mux.cost += prepare_decode_mux(T1, T3, V1, bit);
mux.cost += prepare_decode_mux(U1, U2, V1, bit); mux.cost += prepare_decode_mux(U1, U2, V1, bit);
if (U1 != RTLIL::Sx) {
mux.cost += prepare_decode_mux(T1, T2, U1, bit);
mux.cost += prepare_decode_mux(T3, T4, U2, bit);
mux.cost += prepare_decode_mux(T1, T3, V1, bit);
if (T1 != RTLIL::Sx) {
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
mux.cost += prepare_decode_mux(S5, S6, T3, bit);
mux.cost += prepare_decode_mux(S7, S8, T4, bit);
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
mux.cost += prepare_decode_mux(S5, S7, U2, bit);
mux.cost += prepare_decode_mux(S1, S5, V1, bit);
}
else
S1 = RTLIL::Sx;
}
else {
T1 = RTLIL::Sx;
S1 = RTLIL::Sx;
}
mux.selects.push_back(S1); mux.selects.push_back(S1);
mux.selects.push_back(T1); mux.selects.push_back(T1);
mux.selects.push_back(U1); mux.selects.push_back(U1);

40
techlibs/ecp5/cells_map.v
View file

@ -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_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 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 // Diamond I/O buffers
module IB (input I, output O); (* PULLMODE="NONE" *) TRELLIS_IO #(.DIR("INPUT")) _TECHMAP_REPLACE_ (.B(I), .O(O)); endmodule 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 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 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 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 // Diamond I/O registers
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 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 `ifndef NO_LUT
module \$lut (A, Y); module \$lut (A, Y);

94
techlibs/ecp5/cells_sim.v
View file

@ -260,18 +260,6 @@ module TRELLIS_FF(input CLK, LSR, CE, DI, M, output reg Q);
endgenerate endgenerate
endmodule 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 *) (* keep *)
module TRELLIS_IO( module TRELLIS_IO(
@ -303,19 +291,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); module INV(input A, output Z);
assign Z = !A; assign Z = !A;
endmodule endmodule
@ -568,19 +543,56 @@ module DP16KD(
parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000; parameter INITVAL_3F = 320'h00000000000000000000000000000000000000000000000000000000000000000000000000000000;
endmodule endmodule
// For Diamond compatibility, FIXME: add all Diamond flipflop mappings // TODO: Diamond flip-flops
module FD1S3BX(input PD, D, CK, output Q); // module FD1P3AX(); endmodule
TRELLIS_FF #( // module FD1P3AY(); endmodule
.GSR("DISABLED"), // module FD1P3BX(); endmodule
.CEMUX("1"), // module FD1P3DX(); endmodule
.CLKMUX("CLK"), // module FD1P3IX(); endmodule
.LSRMUX("LSR"), // module FD1P3JX(); endmodule
.REGSET("SET"), // module FD1S3AX(); endmodule
.SRMODE("ASYNC") // module FD1S3AY(); endmodule
) tff_i ( 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
.CLK(CK), 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
.LSR(PD), 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
.DI(D), 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
.Q(Q) // module FL1P3AY(); endmodule
); // module FL1P3AZ(); endmodule
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

2
techlibs/xilinx/cells_sim.v
View file

@ -294,7 +294,7 @@ module RAM32X1D (
output DPO, SPO, output DPO, SPO,
input D, WCLK, WE, input D, WCLK, WE,
input A0, A1, A2, A3, A4, input A0, A1, A2, A3, A4,
input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4, input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4
); );
parameter INIT = 32'h0; parameter INIT = 32'h0;
parameter IS_WCLK_INVERTED = 1'b0; parameter IS_WCLK_INVERTED = 1'b0;

168
tests/various/muxcover.ys
View file

@ -188,3 +188,171 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter sat -verify -prove-asserts -show-ports miter
## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux2in4(input [1:0] i, input s, output o);
assign o = s ? i[1] : i[0];
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux4=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 1 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 0 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX4_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux2in8(input [1:0] i, input s, output o);
assign o = s ? i[1] : i[0];
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux8=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 1 t:$_MUX8_
select -assert-count 0 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX8_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux4in8(input [3:0] i, input [1:0] s, output o);
assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux8=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 1 t:$_MUX8_
select -assert-count 0 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX8_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux2in16(input [1:0] i, input s, output o);
assign o = s ? i[1] : i[0];
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux16=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 1 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX16_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux4in16(input [3:0] i, input [1:0] s, output o);
assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux16=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 1 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX16_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
design -reset
read_verilog -formal <<EOT
module mux4in16(input [7:0] i, input [2:0] s, output o);
assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0])
: s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]);
endmodule
EOT
prep
design -save gold
techmap
muxcover -mux16=0 -nodecode
clean
opt_expr -mux_bool
select -assert-count 0 t:$_MUX_
select -assert-count 0 t:$_MUX4_
select -assert-count 0 t:$_MUX8_
select -assert-count 1 t:$_MUX16_
techmap -map +/simcells.v t:$_MUX16_
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter