3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-09 09:21:58 +00:00

test suite

This commit is contained in:
Lofty 2025-09-24 20:56:27 +01:00
parent 276ca4eeda
commit 3f128474cb
38 changed files with 1282 additions and 161 deletions

View file

@ -82,6 +82,7 @@ struct EdifNames
used_names.count(gen_name) == 0)
break;
}
log("renamed '%s' to '%s'\n", id, gen_name);
generated_names.insert(gen_name);
name_map[id] = gen_name;
return gen_name;

View file

@ -453,7 +453,7 @@ endmodule
// Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L238-L250
(* abc9_flop, lib_whitebox *)
module FDRE (
module FFRE (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -494,7 +494,7 @@ module FDRE (
endmodule
(* abc9_flop, lib_whitebox *)
module FDRE_1 (
module FFRE_N (
output reg Q,
(* clkbuf_sink *)
input C,
@ -518,7 +518,7 @@ module FDRE_1 (
endmodule
(* abc9_flop, lib_whitebox *)
module FDSE (
module FFSE (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -559,7 +559,7 @@ module FDSE (
endmodule
(* abc9_flop, lib_whitebox *)
module FDSE_1 (
module FFSE_N (
output reg Q,
(* clkbuf_sink *)
input C,
@ -583,7 +583,7 @@ module FDSE_1 (
endspecify
endmodule
module FDRSE (
module FFRSE (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -618,7 +618,7 @@ module FDRSE (
Q <= d;
endmodule
module FDRSE_1 (
module FFRSE_N (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -654,7 +654,7 @@ module FDRSE_1 (
endmodule
(* abc9_box, lib_whitebox *)
module FDCE (
module FFCE (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -703,7 +703,7 @@ module FDCE (
endmodule
(* abc9_box, lib_whitebox *)
module FDCE_1 (
module FFCE_N (
output reg Q,
(* clkbuf_sink *)
input C,
@ -734,7 +734,7 @@ module FDCE_1 (
endmodule
(* abc9_box, lib_whitebox *)
module FDPE (
module FFPE (
output reg Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -782,7 +782,7 @@ module FDPE (
endmodule
(* abc9_box, lib_whitebox *)
module FDPE_1 (
module FFPE_N (
output reg Q,
(* clkbuf_sink *)
input C,
@ -812,7 +812,7 @@ module FDPE_1 (
endspecify
endmodule
module FDCPE (
module FFCPE (
output wire Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -857,7 +857,7 @@ module FDCPE (
assign Q = qs ? qp : qc;
endmodule
module FDCPE_1 (
module FFCPE_N (
output wire Q,
(* clkbuf_sink *)
(* invertible_pin = "IS_C_INVERTED" *)
@ -902,81 +902,6 @@ module FDCPE_1 (
assign Q = qs ? qp : qc;
endmodule
module LDCE (
output reg Q,
(* invertible_pin = "IS_CLR_INVERTED" *)
input CLR,
input D,
(* invertible_pin = "IS_G_INVERTED" *)
input G,
input GE
);
parameter [0:0] INIT = 1'b0;
parameter [0:0] IS_CLR_INVERTED = 1'b0;
parameter [0:0] IS_G_INVERTED = 1'b0;
parameter MSGON = "TRUE";
parameter XON = "TRUE";
initial Q = INIT;
wire clr = CLR ^ IS_CLR_INVERTED;
wire g = G ^ IS_G_INVERTED;
always @*
if (clr) Q <= 1'b0;
else if (GE && g) Q <= D;
endmodule
module LDPE (
output reg Q,
input D,
(* invertible_pin = "IS_G_INVERTED" *)
input G,
input GE,
(* invertible_pin = "IS_PRE_INVERTED" *)
input PRE
);
parameter [0:0] INIT = 1'b1;
parameter [0:0] IS_G_INVERTED = 1'b0;
parameter [0:0] IS_PRE_INVERTED = 1'b0;
parameter MSGON = "TRUE";
parameter XON = "TRUE";
initial Q = INIT;
wire g = G ^ IS_G_INVERTED;
wire pre = PRE ^ IS_PRE_INVERTED;
always @*
if (pre) Q <= 1'b1;
else if (GE && g) Q <= D;
endmodule
module LDCPE (
output reg Q,
(* invertible_pin = "IS_CLR_INVERTED" *)
input CLR,
(* invertible_pin = "IS_D_INVERTED" *)
input D,
(* invertible_pin = "IS_G_INVERTED" *)
input G,
(* invertible_pin = "IS_GE_INVERTED" *)
input GE,
(* invertible_pin = "IS_PRE_INVERTED" *)
input PRE
);
parameter [0:0] INIT = 1'b1;
parameter [0:0] IS_CLR_INVERTED = 1'b0;
parameter [0:0] IS_D_INVERTED = 1'b0;
parameter [0:0] IS_G_INVERTED = 1'b0;
parameter [0:0] IS_GE_INVERTED = 1'b0;
parameter [0:0] IS_PRE_INVERTED = 1'b0;
initial Q = INIT;
wire d = D ^ IS_D_INVERTED;
wire g = G ^ IS_G_INVERTED;
wire ge = GE ^ IS_GE_INVERTED;
wire clr = CLR ^ IS_CLR_INVERTED;
wire pre = PRE ^ IS_PRE_INVERTED;
always @*
if (clr) Q <= 1'b0;
else if (pre) Q <= 1'b1;
else if (ge && g) Q <= d;
endmodule
module AND2B1L (
output O,
input DI,

View file

@ -22,97 +22,40 @@
// Async reset, enable.
module \$_DFFE_NP0P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDCE_1 #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R));
FFCE_N #(.INIT(1'b0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DFFE_PP0P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDCE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R));
FFCE #(.INIT(1'b0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DFFE_NP1P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDPE_1 #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .PRE(R));
FFPE_N #(.INIT(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .PRE(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DFFE_PP1P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDPE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .PRE(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
// Async set and reset, enable.
module \$_DFFSRE_NPPP_ (input D, C, E, S, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDCPE #(.INIT(_TECHMAP_WIREINIT_Q_), .IS_C_INVERTED(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R), .PRE(S));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DFFSRE_PPPP_ (input D, C, E, S, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDCPE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .CLR(R), .PRE(S));
FFPE #(.INIT(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .PRE(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
// Sync reset, enable.
module \$_SDFFE_NP0P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDRE_1 #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .R(R));
FFRE_N #(.INIT(1'b0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .R(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_SDFFE_PP0P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDRE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .R(R));
FFRE #(.INIT(1'b0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .R(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_SDFFE_NP1P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDSE_1 #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .S(R));
FFSE_N #(.INIT(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .S(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_SDFFE_PP1P_ (input D, C, E, R, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
FDSE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .S(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
// Latches with reset.
module \$_DLATCH_NP0_ (input E, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDCE #(.INIT(_TECHMAP_WIREINIT_Q_), .IS_G_INVERTED(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .CLR(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DLATCH_PP0_ (input E, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDCE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .CLR(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DLATCH_NP1_ (input E, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDPE #(.INIT(_TECHMAP_WIREINIT_Q_), .IS_G_INVERTED(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .PRE(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DLATCH_PP1_ (input E, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDPE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .PRE(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
// Latches with set and reset.
module \$_DLATCH_NPP_ (input E, S, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDCPE #(.INIT(_TECHMAP_WIREINIT_Q_), .IS_G_INVERTED(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .CLR(R), .PRE(S));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule
module \$_DLATCH_PPP_ (input E, S, R, D, output Q);
parameter _TECHMAP_WIREINIT_Q_ = 1'bx;
LDCPE #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .G(E), .GE(1'b1), .CLR(R), .PRE(S));
FFSE #(.INIT(1'b1)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E), .S(R));
wire _TECHMAP_REMOVEINIT_Q_ = 1;
endmodule

View file

@ -14,14 +14,6 @@ ram distributed $__ANALOGDEVICES_LUTRAM_SP_ {
abits 6;
widths 4 global;
}
option "ABITS" 7 {
abits 7;
widths 2 global;
}
option "ABITS" 8 {
abits 8;
widths 1 global;
}
init no_undef;
prune_rom;
port arsw "RW" {

View file

@ -425,7 +425,7 @@ struct SynthAnalogDevicesPass : public ScriptPass
}
if (check_label("map_ffs")) {
run("dfflegalize -cell $_DFFE_?P?P_ 01 -cell $_SDFFE_?P?P_ 01");
run("dfflegalize -cell $_DFFE_?P?P_ r -cell $_SDFFE_?P?P_ r");
if (abc9 || help_mode) {
if (dff || help_mode)
run("zinit -all w:* t:$_SDFFE_*", "('-dff' only)");

View file

@ -0,0 +1,142 @@
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
logger -nowarn "Ignoring boxed module .*\."
read_verilog <<EOT
module top(input C, D, output [7:0] Q);
FFRE /*#(.INIT(0))*/ fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
FFSE #(.INIT(0)) fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
FFCE #(.INIT(0)) fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
FFPE #(.INIT(0)) fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
FFRE_N #(.INIT(0)) fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
FFSE_N #(.INIT(0)) fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
FFCE_N #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
FFPE_N #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
endmodule
EOT
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 6 t:FF*
select -assert-count 6 c:fd2 c:fd3 c:fd4 c:fd6 c:fd7 c:fd8
design -reset
read_verilog <<EOT
module top(input C, D, output [7:0] Q);
FFRE #(.INIT(0)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
FFSE #(.INIT(0)) fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
FFCE #(.INIT(0)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
FFPE #(.INIT(0)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
FFRE_N /*#(.INIT(0))*/ fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
FFSE_N #(.INIT(0)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
FFCE_N #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
FFPE_N #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
endmodule
EOT
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 4 t:FF*
select -assert-count 4 c:fd3 c:fd4 c:fd7 c:fd8
design -reset
read_verilog <<EOT
module top(input C, D, output [7:0] Q);
FFRE #(.INIT(1)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
FFSE /*#(.INIT(1))*/ fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
FFCE #(.INIT(1)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
FFPE #(.INIT(1)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
FFRE_N #(.INIT(1)) fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
FFSE_N #(.INIT(1)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
FFCE_N /*#(.INIT(1))*/ fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
FFPE_N #(.INIT(1)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
endmodule
EOT
logger -expect warning "Whitebox '\$paramod\\FFRE\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
logger -expect warning "Whitebox '\$paramod\\FFRE_N\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
logger -expect warning "Whitebox 'FFSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
logger -expect warning "Whitebox '\$paramod\\FFSE_N\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 8 t:FF*
design -reset
read_verilog <<EOT
module top(input clk, clr, pre, output reg q0 = 1'b0, output reg q1 = 1'b1);
always @(posedge clk or posedge clr)
if (clr)
q0 <= 1'b0;
else
q0 <= ~q0;
always @(posedge clk or posedge pre)
if (pre)
q1 <= 1'b1;
else
q1 <= ~q1;
endmodule
EOT
proc
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 1 t:FFCE
select -assert-count 1 t:FFPE
select -assert-count 2 t:INV
select -assert-count 0 t:FF* t:INV %% t:* %D
design -reset
read_verilog <<EOT
module top(input clk, input d, output q);
reg r;
always @(posedge clk) begin
r <= d;
end
assign q = ~r;
endmodule
EOT
proc
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 1 t:FFRE %co w:r %i
design -reset
read_verilog <<EOT
module top(input clk, input a, b, output reg q1, output q2);
reg r;
always @(posedge clk) begin
q1 <= a | b;
r <= ~(~a & ~b);
end
assign q2 = r;
endmodule
EOT
proc
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
design -load postopt
select -assert-count 1 t:FFRE %co %a w:r %i
design -reset
read_verilog <<EOT
module top(input clk, input a, b, output o);
reg r1, r2;
always @(posedge clk) begin
r1 <= a | b;
r2 <= ~(~a & ~b);
end
assign o = r1 | r2;
endmodule
EOT
proc
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -multiclock -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad -noclkbuf
logger -expect-no-warnings

View file

@ -0,0 +1,13 @@
read_verilog ../common/add_sub.v
hierarchy -top top
proc
design -save orig
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 8 t:LUT2
select -assert-count 2 t:CRY4
select -assert-none t:LUT2 t:CRY4 %% t:* %D

View file

@ -0,0 +1,51 @@
read_verilog ../common/adffs.v
design -save read
hierarchy -top adff
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFCE
select -assert-none t:BUFG t:FFCE %% t:* %D
design -load read
hierarchy -top adffn
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFCE
select -assert-count 1 t:INV
select -assert-none t:BUFG t:FFCE t:INV %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-count 1 t:LUT2
stat
select -assert-none t:BUFG t:FFRE t:LUT2 %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE_N
select -assert-count 1 t:INV
select -assert-none t:BUFG t:FFRE_N t:INV %% t:* %D

View file

@ -0,0 +1,50 @@
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
# w4b | r16b
design -reset
read_verilog asym_ram_sdp_read_wider.v
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w8b | r16b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set WIDTHA 8 -set SIZEA 512 -set ADDRWIDTHA 9 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w4b | r32b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set WIDTHB 32 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w16b | r4b
design -reset
read_verilog asym_ram_sdp_write_wider.v
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w16b | r8b
design -reset
read_verilog asym_ram_sdp_write_wider.v
chparam -set WIDTHB 8 -set SIZEB 512 -set ADDRWIDTHB 9 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w32b | r4b
design -reset
read_verilog asym_ram_sdp_write_wider.v
chparam -set WIDTHA 32 -set SIZEA 128 -set ADDRWIDTHA 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_write_wider -noiopad
select -assert-count 1 t:RAMB18E1
# w4b | r24b
design -reset
read_verilog asym_ram_sdp_read_wider.v
chparam -set SIZEA 768
chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
select -assert-count 1 t:RAMB18E1

View file

@ -0,0 +1,72 @@
// Asymmetric port RAM
// Read Wider than Write. Read Statement in loop
//asym_ram_sdp_read_wider.v
module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB);
parameter WIDTHA = 4;
parameter SIZEA = 1024;
parameter ADDRWIDTHA = 10;
parameter WIDTHB = 16;
parameter SIZEB = 256;
parameter ADDRWIDTHB = 8;
input clkA;
input clkB;
input weA;
input enaA, enaB;
input [ADDRWIDTHA-1:0] addrA;
input [ADDRWIDTHB-1:0] addrB;
input [WIDTHA-1:0] diA;
output [WIDTHB-1:0] doB;
`define max(a,b) {(a) > (b) ? (a) : (b)}
`define min(a,b) {(a) < (b) ? (a) : (b)}
function integer log2;
input integer value;
reg [31:0] shifted;
integer res;
begin
if (value < 2)
log2 = value;
else
begin
shifted = value-1;
for (res=0; shifted>0; res=res+1)
shifted = shifted>>1;
log2 = res;
end
end
endfunction
localparam maxSIZE = `max(SIZEA, SIZEB);
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
localparam minWIDTH = `min(WIDTHA, WIDTHB);
localparam RATIO = maxWIDTH / minWIDTH;
localparam log2RATIO = log2(RATIO);
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
reg [WIDTHB-1:0] readB;
always @(posedge clkA)
begin
if (enaA) begin
if (weA)
RAM[addrA] <= diA;
end
end
always @(posedge clkB)
begin : ramread
integer i;
reg [log2RATIO-1:0] lsbaddr;
if (enaB) begin
for (i = 0; i < RATIO; i = i+1) begin
lsbaddr = i;
readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}];
end
end
end
assign doB = readB;
endmodule

View file

@ -0,0 +1,71 @@
// Asymmetric port RAM
// Write wider than Read. Write Statement in a loop.
// asym_ram_sdp_write_wider.v
module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB);
parameter WIDTHB = 4;
parameter SIZEB = 1024;
parameter ADDRWIDTHB = 10;
parameter WIDTHA = 16;
parameter SIZEA = 256;
parameter ADDRWIDTHA = 8;
input clkA;
input clkB;
input weA;
input enaA, enaB;
input [ADDRWIDTHA-1:0] addrA;
input [ADDRWIDTHB-1:0] addrB;
input [WIDTHA-1:0] diA;
output [WIDTHB-1:0] doB;
`define max(a,b) {(a) > (b) ? (a) : (b)}
`define min(a,b) {(a) < (b) ? (a) : (b)}
function integer log2;
input integer value;
reg [31:0] shifted;
integer res;
begin
if (value < 2)
log2 = value;
else
begin
shifted = value-1;
for (res=0; shifted>0; res=res+1)
shifted = shifted>>1;
log2 = res;
end
end
endfunction
localparam maxSIZE = `max(SIZEA, SIZEB);
localparam maxWIDTH = `max(WIDTHA, WIDTHB);
localparam minWIDTH = `min(WIDTHA, WIDTHB);
localparam RATIO = maxWIDTH / minWIDTH;
localparam log2RATIO = log2(RATIO);
reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
reg [WIDTHB-1:0] readB;
always @(posedge clkB) begin
if (enaB) begin
readB <= RAM[addrB];
end
end
assign doB = readB;
always @(posedge clkA)
begin : ramwrite
integer i;
reg [log2RATIO-1:0] lsbaddr;
for (i=0; i< RATIO; i= i+ 1) begin : write1
lsbaddr = i;
if (enaA) begin
if (weA)
RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];
end
end
end
endmodule

View file

@ -0,0 +1,37 @@
# Check that blockram memory without parameters is not modified
read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top block_ram
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1
# Check that distributed memory without parameters is not modified
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top distributed_ram
synth_analogdevices -top distributed_ram -noiopad
cd distributed_ram # Constrain all select calls below inside the top module
select -assert-count 1 t:RAM32M
# Set ram_style distributed to blockram memory; will be implemented as distributed
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
setattr -set ram_style "distributed" block_ram/m:*
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
select -assert-count 64 t:RAM64X1S
# Set synthesis, logic_block to blockram memory; will be implemented as distributed
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
setattr -set logic_block 1 block_ram/m:*
synth_analogdevices -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module
select -assert-count 0 t:RAMB18E1
# Set ram_style block to a distributed memory; will be implemented as blockram
design -reset
read_verilog ../common/memory_attributes/attributes_test.v
synth_analogdevices -top distributed_ram_manual -noiopad
cd distributed_ram_manual # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1

View file

@ -0,0 +1,73 @@
### TODO: Not running equivalence checking because BRAM models does not exists
### currently. Checking instance counts instead.
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 12 -set DATA_WIDTH 1 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1
# Anything memory bits < 1024 -> LUTRAM
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1
select -assert-count 4 t:RAM64M
# More than 18K bits, data width <= 36 (TDP), and address width from 10 to 15b (non-cascaded) -> RAMB36E1
design -reset
read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB36E1
### With parameters
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 12 -chparam DATA_WIDTH 1
setattr -set logic_block 1 m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1
design -reset
read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory
synth_analogdevices -top sync_ram_sdp -noiopad
cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1

View file

@ -0,0 +1,34 @@
read_verilog <<EOT
module register_file(
input wire clk,
input wire write_enable,
input wire [63:0] write_data,
input wire [4:0] write_reg,
input wire [4:0] read1_reg,
input wire [4:0] read2_reg,
input wire [4:0] read3_reg,
output reg [63:0] read1_data,
output reg [63:0] read2_data,
output reg [63:0] read3_data
);
reg [63:0] registers[0:31];
always @(posedge clk) begin
if (write_enable == 1'b1) begin
registers[write_reg] <= write_data;
end
end
always @(all) begin
read1_data <= registers[read1_reg];
read2_data <= registers[read2_reg];
read3_data <= registers[read3_reg];
end
endmodule
EOT
synth_analogdevices -noiopad
cd register_file
select -assert-count 33 t:RAM32M
select -assert-none t:* t:BUFG %d t:RAM32M %d

View file

@ -0,0 +1,11 @@
read_verilog << EOF
module top(...);
input wire [31:0] A;
output wire [31:0] P;
assign P = A * 32'h12300000;
endmodule
EOF
synth_analogdevices

View file

@ -0,0 +1,18 @@
read_verilog << EOF
module top(...);
input signed [17:0] A;
input signed [17:0] B;
output X;
output Y;
wire [35:0] P;
assign P = A * B;
assign X = P[0];
assign Y = P[35];
endmodule
EOF
synth_analogdevices

View file

@ -0,0 +1,16 @@
read_verilog <<EOT
module led_blink (
input clk,
output ledc
);
reg [6:0] led_counter = 0;
always @( posedge clk ) begin
led_counter <= led_counter + 1;
end
assign ledc = !led_counter[ 6:3 ];
endmodule
EOT
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices

View file

@ -0,0 +1,19 @@
read_verilog <<EOT
module top(inout io);
wire in;
wire t;
wire o;
IOBUF IOBUF(
.I(in),
.T(t),
.IO(io),
.O(o)
);
endmodule
EOT
synth_analogdevices
cd top
select -assert-count 1 t:IOBUF
select -assert-none t:* t:IOBUF %d

View file

@ -0,0 +1,13 @@
module bug3670(input we, output [31:0] o1, o2, output o3);
// Completely missing port connections, where first affected port
// (ADDRARDADDR) has a $setup delay
RAMB36E1 ram1(.DOADO(o1));
// Under-specified input port connections (WEA is 4 bits) which
// has a $setup delay
RAMB36E1 ram2(.WEA(we), .DOADO(o2));
// Under-specified output port connections (DOADO is 32 bits)
// with clk-to-q delay
RAMB36E1 ram3(.DOADO(o3));
endmodule

View file

@ -0,0 +1,3 @@
read_verilog bug3670.v
read_verilog -lib -specify +/analogdevices/cells_sim.v
abc9

View file

@ -0,0 +1,13 @@
read_verilog ../common/counter.v
hierarchy -top top
proc
flatten
equiv_opt -async2sync -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 8 t:FFCE
select -assert-count 1 t:INV
select -assert-count 2 t:CRY4
select -assert-none t:BUFG t:FFCE t:INV t:CRY4 %% t:* %D

View file

@ -0,0 +1,45 @@
read_verilog ../common/dffs.v
design -save read
hierarchy -top dff
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-none t:BUFG t:FFRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-none t:BUFG t:FFRE %% t:* %D
design -load read
hierarchy -top dff
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-none t:BUFG t:FFRE %% t:* %D
design -load read
hierarchy -top dffe
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -dff -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-none t:BUFG t:FFRE %% t:* %D

View file

@ -0,0 +1,56 @@
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
logger -nowarn "Ignoring boxed module .*\."
read_verilog <<EOT
module top(input [24:0] A, input [17:0] B, output [47:0] P);
DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
endmodule
EOT
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt
scc -expect 0
design -reset
read_verilog <<EOT
module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
assign P = A * B;
endmodule
EOT
synth_analogdevices
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt -full -fine
select -assert-count 1 t:$mul
select -assert-count 0 t:* t:$mul %D
design -reset
read_verilog -icells -formal <<EOT
module top(output [42:0] P);
\$__MUL25X18 mul (.A(42), .B(42), .Y(P));
assert property (P == 42*42);
endmodule
EOT
async2sync
techmap -map +/analogdevices/xc7_dsp_map.v
verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
synth_analogdevices
techmap -autoproc -wb -map +/analogdevices/cells_sim.v
opt -full -fine
select -assert-count 0 t:* t:$assert %d
sat -verify -prove-asserts
design -reset
read_verilog <<EOT
module top(input signed [29:0] A, input signed [17:0] B, output signed [47:0] P);
wire [47:0] casc;
DSP48E1 #(.AREG(1)) u1(.A(A), .B(B), .PCOUT(casc));
DSP48E1 #(.AREG(1)) u2(.A(A), .B(B), .PCIN(casc), .P(P));
endmodule
EOT
synth_analogdevices -run :prepare
abc9
clean
check
logger -expect-no-warnings

View file

@ -0,0 +1,21 @@
read_verilog ../common/fsm.v
hierarchy -top fsm
proc
flatten
design -save orig
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
miter -equiv -make_assert -flatten gold gate miter
sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
stat
select -assert-count 1 t:BUFG
select -assert-count 6 t:FFRE
select -assert-count 1 t:INV
select -assert-count 1 t:LUT3
select -assert-count 1 t:LUT4
select -assert-count 5 t:LUT5
select -assert-none t:BUFG t:FFRE t:INV t:LUT3 t:LUT4 t:LUT5 %% t:* %D

View file

@ -0,0 +1,11 @@
read_verilog ../common/logic.v
hierarchy -top top
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:INV
select -assert-count 6 t:LUT2
select -assert-count 2 t:LUT4
select -assert-none t:INV t:LUT2 t:LUT4 %% t:* %D

View file

@ -0,0 +1,119 @@
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 1 t:BUFG
select -assert-count 8 t:FFRE
select -assert-count 1 t:RAM32M
select -assert-none t:BUFG t:FFRE t:RAM32M %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
dump
select -assert-count 1 t:BUFG
select -assert-count 8 t:FFRE
select -assert-count 8 t:RAM64X1S
select -assert-none t:BUFG t:FFRE t:RAM64X1S %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w3r
select -assert-count 1 t:BUFG
select -assert-count 24 t:FFRE
select -assert-count 4 t:RAM32M
select -assert-none t:BUFG t:FFRE t:RAM32M %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r -chparam A_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w3r
select -assert-count 1 t:BUFG
select -assert-count 24 t:FFRE
select -assert-count 16 t:RAM64X1D
select -assert-none t:BUFG t:FFRE t:RAM64X1D %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 1 t:BUFG
select -assert-count 6 t:FFRE
select -assert-count 1 t:RAM32M
select -assert-none t:BUFG t:FFRE t:RAM32M %% t:* %D
design -reset
read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
proc
memory -nomap
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
design -load postopt
cd lutram_1w1r
select -assert-count 1 t:BUFG
select -assert-count 6 t:FFRE
select -assert-count 6 t:RAM64X1S
select -assert-none t:BUFG t:FFRE t:RAM64X1S %% t:* %D

View file

@ -0,0 +1,6 @@
../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
vvp -N ./test_macc
../../../yosys -qp "synth_xilinx -family xc6s -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
vvp -N ./test_macc

View file

@ -0,0 +1,84 @@
// Signed 40-bit streaming accumulator with 16-bit inputs
// File: HDL_Coding_Techniques/multipliers/multipliers4.v
//
// Source:
// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
//
module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
input clk, ce, sload,
input signed [SIZEIN-1:0] a, b,
output signed [SIZEOUT-1:0] accum_out
);
// Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0;
reg sload_reg = 0;
reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT-1:0] adder_out = 0, old_result;
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
if (sload_reg)
old_result <= 0;
else
// 'sload' is now active (=low) and opens the accumulation loop.
// The accumulator takes the next multiplier output in
// the same cycle.
old_result <= adder_out;
end
always @(posedge clk)
if (ce)
begin
a_reg <= a;
b_reg <= b;
mult_reg <= a_reg * b_reg;
sload_reg <= sload;
// Store accumulation result into a register
adder_out <= old_result + mult_reg;
end
// Output accumulation result
assign accum_out = adder_out;
endmodule
// Adapted variant of above
module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
input clk,
input ce,
input rst,
input signed [SIZEIN-1:0] a, b,
output signed [SIZEOUT-1:0] accum_out,
output overflow
);
// Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0, a_reg2 = 0, b_reg2 = 0;
reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT:0] adder_out = 0;
reg overflow_reg = 0;
always @(posedge clk) begin
//if (ce)
begin
a_reg <= a;
b_reg <= b;
a_reg2 <= a_reg;
b_reg2 <= b_reg;
mult_reg <= a_reg2 * b_reg2;
// Store accumulation result into a register
adder_out <= adder_out + mult_reg;
overflow_reg <= overflow;
end
if (rst) begin
a_reg <= 0;
a_reg2 <= 0;
b_reg <= 0;
b_reg2 <= 0;
mult_reg <= 0;
adder_out <= 0;
overflow_reg <= 1'b0;
end
end
assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg;
// Output accumulation result
assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out;
endmodule

View file

@ -0,0 +1,32 @@
read_verilog macc.v
design -save read
hierarchy -top macc
proc
#equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad ### TODO
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 3 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FFRE
select -assert-count 1 t:DSP48E1
select -assert-none t:BUFG t:FFRE t:DSP48E1 %% t:* %D
design -load read
hierarchy -top macc2
proc
#equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad ### TODO
equiv_opt -run :prove -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc2 # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:DSP48E1
select -assert-count 1 t:FFRE
select -assert-count 1 t:LUT2
select -assert-count 40 t:LUT3
select -assert-none t:BUFG t:DSP48E1 t:FFRE t:LUT2 t:LUT3 %% t:* %D

View file

@ -0,0 +1,96 @@
`timescale 1ns / 1ps
module testbench;
parameter SIZEIN = 16, SIZEOUT = 40;
reg clk, ce, rst;
reg signed [SIZEIN-1:0] a, b;
output signed [SIZEOUT-1:0] REF_accum_out, accum_out;
output REF_overflow, overflow;
integer errcount = 0;
reg ERROR_FLAG = 0;
task clkcycle;
begin
#5;
clk = ~clk;
#10;
clk = ~clk;
#2;
ERROR_FLAG = 0;
if (REF_accum_out !== accum_out) begin
$display("ERROR at %1t: REF_accum_out=%b UUT_accum_out=%b DIFF=%b", $time, REF_accum_out, accum_out, REF_accum_out ^ accum_out);
errcount = errcount + 1;
ERROR_FLAG = 1;
end
if (REF_overflow !== overflow) begin
$display("ERROR at %1t: REF_overflow=%b UUT_overflow=%b DIFF=%b", $time, REF_overflow, overflow, REF_overflow ^ overflow);
errcount = errcount + 1;
ERROR_FLAG = 1;
end
#3;
end
endtask
initial begin
//$dumpfile("test_macc.vcd");
//$dumpvars(0, testbench);
#2;
clk = 1'b0;
ce = 1'b0;
a = 0;
b = 0;
rst = 1'b1;
repeat (10) begin
#10;
clk = 1'b1;
#10;
clk = 1'b0;
#10;
clk = 1'b1;
#10;
clk = 1'b0;
end
rst = 1'b0;
repeat (10000) begin
clkcycle;
ce = 1; //$urandom & $urandom;
//rst = $urandom & $urandom & $urandom & $urandom & $urandom & $urandom;
a = $urandom & ~(1 << (SIZEIN-1));
b = $urandom & ~(1 << (SIZEIN-1));
end
if (errcount == 0) begin
$display("All tests passed.");
$finish;
end else begin
$display("Caught %1d errors.", errcount);
$stop;
end
end
macc2 ref (
.clk(clk),
.ce(ce),
.rst(rst),
.a(a),
.b(b),
.accum_out(REF_accum_out),
.overflow(REF_overflow)
);
macc2_uut uut (
.clk(clk),
.ce(ce),
.rst(rst),
.a(a),
.b(b),
.accum_out(accum_out),
.overflow(overflow)
);
endmodule

View file

@ -0,0 +1,9 @@
read_verilog ../common/mul.v
hierarchy -top top
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:DSP48E1
select -assert-none t:DSP48E1 %% t:* %D

View file

@ -0,0 +1,30 @@
/*
Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89].
*/
// Unsigned 16x24-bit Multiplier
// 1 latency stage on operands
// 3 latency stage after the multiplication
// File: multipliers2.v
//
module mul_unsigned (clk, A, B, RES);
parameter WIDTHA = /*16*/ 6;
parameter WIDTHB = /*24*/ 9;
input clk;
input [WIDTHA-1:0] A;
input [WIDTHB-1:0] B;
output [WIDTHA+WIDTHB-1:0] RES;
reg [WIDTHA-1:0] rA;
reg [WIDTHB-1:0] rB;
reg [WIDTHA+WIDTHB-1:0] M [3:0];
integer i;
always @(posedge clk)
begin
rA <= A;
rB <= B;
M[0] <= rA * rB;
for (i = 0; i < 3; i = i+1)
M[i+1] <= M[i];
end
assign RES = M[3];
endmodule

View file

@ -0,0 +1,11 @@
read_verilog mul_unsigned.v
hierarchy -top mul_unsigned
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:DSP48E1
select -assert-count 30 t:FFRE
select -assert-none t:DSP48E1 t:FFRE t:BUFG %% t:* %D

View file

@ -0,0 +1,50 @@
read_verilog ../common/mux.v
design -save read
hierarchy -top mux2
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-none t:LUT3 %% t:* %D
design -load read
hierarchy -top mux4
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT6
select -assert-none t:LUT6 %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-count 2 t:LUT6
select -assert-none t:LUT3 t:LUT6 %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
select -assert-max 2 t:LUT3
select -assert-max 2 t:LUT4
select -assert-min 4 t:LUT6
select -assert-max 7 t:LUT6
select -assert-max 2 t:MUXF7
dump
select -assert-none t:LUT6 t:LUT4 t:LUT3 t:MUXF7 %% t:* %D

View file

@ -0,0 +1,26 @@
read_rtlil << EOF
module \top
wire width 4 input 1 \A
wire output 2 \O
cell \LUT4 $0
parameter \INIT 16'1111110011000000
connect \I0 \A [0]
connect \I1 \A [1]
connect \I2 \A [2]
connect \I3 \A [3]
connect \O \O
end
end
EOF
read_verilog -lib +/analogdevices/cells_sim.v
equiv_opt -assert -map +/analogdevices/cells_sim.v opt_lut_ins -tech xilinx
design -load postopt
select -assert-count 1 t:LUT3

View file

@ -0,0 +1,4 @@
#!/usr/bin/env bash
set -eu
source ../../gen-tests-makefile.sh
generate_mk --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'"

View file

@ -0,0 +1,11 @@
read_verilog ../common/shifter.v
hierarchy -top top
proc
flatten
equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 8 t:FFRE
select -assert-none t:BUFG t:FFRE %% t:* %D

View file

@ -0,0 +1,13 @@
read_verilog ../common/tribuf.v
hierarchy -top tristate
proc
tribuf
flatten
synth
equiv_opt -assert -map +/analogdevices/cells_sim.v -map +/simcells.v synth_analogdevices # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd tristate # Constrain all select calls below inside the top module
select -assert-count 2 t:INBUF
select -assert-count 1 t:INV
select -assert-count 1 t:OBUFT
select -assert-none t:INBUF t:INV t:OBUFT %% t:* %D