mirror of https://github.com/YosysHQ/yosys.git
Merge origin/master
This commit is contained in:
parent
c226af3f56
commit
6c256b8cda
|
@ -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));
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -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":
|
||||||
|
|
|
@ -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;
|
||||||
|
|
|
@ -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");
|
||||||
|
|
|
@ -81,6 +81,23 @@ struct MuxcoverWorker
|
||||||
decode_mux_counter = 0;
|
decode_mux_counter = 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
bool xcmp(std::initializer_list<SigBit> list)
|
||||||
|
{
|
||||||
|
auto cursor = list.begin(), end = list.end();
|
||||||
|
log_assert(cursor != end);
|
||||||
|
SigBit tmp = *(cursor++);
|
||||||
|
while (cursor != end) {
|
||||||
|
SigBit bit = *(cursor++);
|
||||||
|
if (bit == State::Sx)
|
||||||
|
continue;
|
||||||
|
if (tmp == State::Sx)
|
||||||
|
tmp = bit;
|
||||||
|
if (bit != tmp)
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
void treeify()
|
void treeify()
|
||||||
{
|
{
|
||||||
pool<SigBit> roots;
|
pool<SigBit> roots;
|
||||||
|
@ -144,6 +161,8 @@ struct MuxcoverWorker
|
||||||
if (tree.muxes.count(bit) == 0) {
|
if (tree.muxes.count(bit) == 0) {
|
||||||
if (first_layer || nopartial)
|
if (first_layer || nopartial)
|
||||||
return false;
|
return false;
|
||||||
|
while (path[0] && path[1])
|
||||||
|
path++;
|
||||||
if (path[0] == 'S')
|
if (path[0] == 'S')
|
||||||
ret_bit = State::Sx;
|
ret_bit = State::Sx;
|
||||||
else
|
else
|
||||||
|
@ -280,7 +299,7 @@ struct MuxcoverWorker
|
||||||
ok = ok && follow_muxtree(S2, tree, bit, "BS");
|
ok = ok && follow_muxtree(S2, tree, bit, "BS");
|
||||||
|
|
||||||
if (nodecode)
|
if (nodecode)
|
||||||
ok = ok && S1 == S2;
|
ok = ok && xcmp({S1, S2});
|
||||||
|
|
||||||
ok = ok && follow_muxtree(T1, tree, bit, "S");
|
ok = ok && follow_muxtree(T1, tree, bit, "S");
|
||||||
|
|
||||||
|
@ -330,13 +349,13 @@ struct MuxcoverWorker
|
||||||
ok = ok && follow_muxtree(S4, tree, bit, "BBS");
|
ok = ok && follow_muxtree(S4, tree, bit, "BBS");
|
||||||
|
|
||||||
if (nodecode)
|
if (nodecode)
|
||||||
ok = ok && S1 == S2 && S2 == S3 && S3 == S4;
|
ok = ok && xcmp({S1, S2, 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");
|
||||||
|
|
||||||
if (nodecode)
|
if (nodecode)
|
||||||
ok = ok && T1 == T2;
|
ok = ok && xcmp({T1, T2});
|
||||||
|
|
||||||
ok = ok && follow_muxtree(U1, tree, bit, "S");
|
ok = ok && follow_muxtree(U1, tree, bit, "S");
|
||||||
|
|
||||||
|
@ -407,7 +426,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 && xcmp({S1, S2, S3, S4, S5, S6, S7, S8});
|
||||||
|
|
||||||
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
|
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
|
||||||
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
|
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
|
||||||
|
@ -415,13 +434,13 @@ struct MuxcoverWorker
|
||||||
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
|
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
|
||||||
|
|
||||||
if (nodecode)
|
if (nodecode)
|
||||||
ok = ok && T1 == T2 && T2 == T3 && T3 == T4;
|
ok = ok && xcmp({T1, T2, T3, T4});
|
||||||
|
|
||||||
ok = ok && follow_muxtree(U1, tree, bit, "AS");
|
ok = ok && follow_muxtree(U1, tree, bit, "AS");
|
||||||
ok = ok && follow_muxtree(U2, tree, bit, "BS");
|
ok = ok && follow_muxtree(U2, tree, bit, "BS");
|
||||||
|
|
||||||
if (nodecode)
|
if (nodecode)
|
||||||
ok = ok && U1 == U2;
|
ok = ok && xcmp({U1, U2});
|
||||||
|
|
||||||
ok = ok && follow_muxtree(V1, tree, bit, "S");
|
ok = ok && follow_muxtree(V1, tree, bit, "S");
|
||||||
|
|
||||||
|
|
|
@ -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);
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -286,7 +286,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;
|
||||||
|
|
|
@ -45,8 +45,9 @@ struct SynthXilinxPass : public ScriptPass
|
||||||
log(" -top <module>\n");
|
log(" -top <module>\n");
|
||||||
log(" use the specified module as top module\n");
|
log(" use the specified module as top module\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
log(" -arch {xcup|xcu|xc7|xc6s}\n");
|
log(" -family {xcup|xcu|xc7|xc6s}\n");
|
||||||
log(" run synthesis for the specified Xilinx architecture\n");
|
log(" run synthesis for the specified Xilinx architecture\n");
|
||||||
|
log(" generate the synthesis netlist for the specified family.\n");
|
||||||
log(" default: xc7\n");
|
log(" default: xc7\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
log(" -edif <file>\n");
|
log(" -edif <file>\n");
|
||||||
|
@ -99,7 +100,7 @@ struct SynthXilinxPass : public ScriptPass
|
||||||
log("\n");
|
log("\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
std::string top_opt, edif_file, blif_file, arch;
|
std::string top_opt, edif_file, blif_file, family;
|
||||||
bool flatten, retime, vpr, nobram, nodram, nosrl, nocarry, nowidelut, abc9;
|
bool flatten, retime, vpr, nobram, nodram, nosrl, nocarry, nowidelut, abc9;
|
||||||
|
|
||||||
void clear_flags() YS_OVERRIDE
|
void clear_flags() YS_OVERRIDE
|
||||||
|
@ -107,7 +108,7 @@ struct SynthXilinxPass : public ScriptPass
|
||||||
top_opt = "-auto-top";
|
top_opt = "-auto-top";
|
||||||
edif_file.clear();
|
edif_file.clear();
|
||||||
blif_file.clear();
|
blif_file.clear();
|
||||||
arch = "xc7";
|
family = "xc7";
|
||||||
flatten = false;
|
flatten = false;
|
||||||
retime = false;
|
retime = false;
|
||||||
vpr = false;
|
vpr = false;
|
||||||
|
@ -132,8 +133,8 @@ struct SynthXilinxPass : public ScriptPass
|
||||||
top_opt = "-top " + args[++argidx];
|
top_opt = "-top " + args[++argidx];
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
if (args[argidx] == "-arch" && argidx+1 < args.size()) {
|
if ((args[argidx] == "-family" || args[argidx] == "-arch") && argidx+1 < args.size()) {
|
||||||
arch = args[++argidx];
|
family = args[++argidx];
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
if (args[argidx] == "-edif" && argidx+1 < args.size()) {
|
if (args[argidx] == "-edif" && argidx+1 < args.size()) {
|
||||||
|
@ -196,8 +197,8 @@ struct SynthXilinxPass : public ScriptPass
|
||||||
}
|
}
|
||||||
extra_args(args, argidx, design);
|
extra_args(args, argidx, design);
|
||||||
|
|
||||||
if (arch != "xcup" && arch != "xcu" && arch != "xc7" && arch != "xc6s")
|
if (family != "xcup" && family != "xcu" && family != "xc7" && family != "xc6s")
|
||||||
log_cmd_error("Invalid Xilinx -arch setting: %s\n", arch.c_str());
|
log_cmd_error("Invalid Xilinx -family setting: %s\n", family.c_str());
|
||||||
|
|
||||||
if (!design->full_selection())
|
if (!design->full_selection())
|
||||||
log_cmd_error("This command only operates on fully selected designs!\n");
|
log_cmd_error("This command only operates on fully selected designs!\n");
|
||||||
|
|
|
@ -188,3 +188,323 @@ 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=99 -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=99 -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=299 -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=99 -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=299 -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=699 -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
|
||||||
|
|
||||||
|
## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -formal <<EOT
|
||||||
|
module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
|
||||||
|
always @* begin
|
||||||
|
o <= {{W{{1'bx}}}};
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
if (s[1] == 1'b0)
|
||||||
|
if (s[2] == 1'b0)
|
||||||
|
o <= i[0*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[1*W+:W];
|
||||||
|
else
|
||||||
|
if (s[2] == 1'b0)
|
||||||
|
o <= i[2*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[3*W+:W];
|
||||||
|
else
|
||||||
|
if (s[1] == 1'b0)
|
||||||
|
if (s[2] == 1'b0)
|
||||||
|
o <= i[4*W+:W];
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
prep
|
||||||
|
design -save gold
|
||||||
|
|
||||||
|
wreduce
|
||||||
|
opt -full
|
||||||
|
techmap
|
||||||
|
muxcover -mux8=350
|
||||||
|
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 -ignore_gold_x gold gate miter
|
||||||
|
sat -verify -prove-asserts -show-ports miter
|
||||||
|
|
||||||
|
## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
|
||||||
|
design -load gold
|
||||||
|
|
||||||
|
wreduce
|
||||||
|
opt -full
|
||||||
|
techmap
|
||||||
|
muxcover -mux8=350 -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 -ignore_gold_x gold gate miter
|
||||||
|
sat -verify -prove-asserts -show-ports miter
|
||||||
|
|
||||||
|
## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
read_verilog -formal <<EOT
|
||||||
|
module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
|
||||||
|
always @* begin
|
||||||
|
o <= {{W{{1'bx}}}};
|
||||||
|
if (s[3] == 1'b0)
|
||||||
|
if (s[2] == 1'b0)
|
||||||
|
if (s[1] == 1'b0)
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
o <= i[0*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[1*W+:W];
|
||||||
|
else
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
o <= i[2*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[3*W+:W];
|
||||||
|
else
|
||||||
|
if (s[1] == 1'b0)
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
o <= i[4*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[5*W+:W];
|
||||||
|
else
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
o <= i[6*W+:W];
|
||||||
|
else
|
||||||
|
o <= i[7*W+:W];
|
||||||
|
else
|
||||||
|
if (s[2] == 1'b0)
|
||||||
|
if (s[1] == 1'b0)
|
||||||
|
if (s[0] == 1'b0)
|
||||||
|
o <= i[8*W+:W];
|
||||||
|
end
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
prep
|
||||||
|
design -save gold
|
||||||
|
|
||||||
|
wreduce
|
||||||
|
opt -full
|
||||||
|
techmap
|
||||||
|
muxcover -mux16=750
|
||||||
|
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 -ignore_gold_x gold gate miter
|
||||||
|
sat -verify -prove-asserts -show-ports miter
|
||||||
|
|
||||||
|
## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
|
||||||
|
|
||||||
|
design -load gold
|
||||||
|
|
||||||
|
wreduce
|
||||||
|
opt -full
|
||||||
|
techmap
|
||||||
|
muxcover -mux16=750 -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 -ignore_gold_x gold gate miter
|
||||||
|
sat -verify -prove-asserts -show-ports miter
|
||||||
|
|
Loading…
Reference in New Issue