diff options
Diffstat (limited to 'tests')
150 files changed, 2648 insertions, 601 deletions
diff --git a/tests/ice40/.gitignore b/tests/arch/anlogic/.gitignore index 9a71dca69..9a71dca69 100644 --- a/tests/ice40/.gitignore +++ b/tests/arch/anlogic/.gitignore diff --git a/tests/arch/anlogic/add_sub.ys b/tests/arch/anlogic/add_sub.ys new file mode 100644 index 000000000..5396ce7ec --- /dev/null +++ b/tests/arch/anlogic/add_sub.ys @@ -0,0 +1,10 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 10 t:AL_MAP_ADDER +select -assert-count 4 t:AL_MAP_LUT1 + +select -assert-none t:AL_MAP_LUT1 t:AL_MAP_ADDER %% t:* %D diff --git a/tests/arch/anlogic/counter.ys b/tests/arch/anlogic/counter.ys new file mode 100644 index 000000000..d363ec24e --- /dev/null +++ b/tests/arch/anlogic/counter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # 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 9 t:AL_MAP_ADDER +select -assert-count 8 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ t:AL_MAP_ADDER %% t:* %D diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys new file mode 100644 index 000000000..d3281ab89 --- /dev/null +++ b/tests/arch/anlogic/dffs.ys @@ -0,0 +1,20 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT3 +select -assert-count 1 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys new file mode 100644 index 000000000..f45951b13 --- /dev/null +++ b/tests/arch/anlogic/fsm.ys @@ -0,0 +1,15 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +#flatten +#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. +#equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +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 +select -assert-count 1 t:AL_MAP_LUT2 +select -assert-count 5 t:AL_MAP_LUT5 +select -assert-count 1 t:AL_MAP_LUT6 +select -assert-count 6 t:AL_MAP_SEQ + +select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT5 t:AL_MAP_LUT6 t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/anlogic/latches.ys b/tests/arch/anlogic/latches.ys new file mode 100644 index 000000000..8d66f77b3 --- /dev/null +++ b/tests/arch/anlogic/latches.ys @@ -0,0 +1,33 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT5 + +select -assert-none t:AL_MAP_LUT5 %% t:* %D diff --git a/tests/arch/anlogic/logic.ys b/tests/arch/anlogic/logic.ys new file mode 100644 index 000000000..125ee5d0f --- /dev/null +++ b/tests/arch/anlogic/logic.ys @@ -0,0 +1,11 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT1 +select -assert-count 6 t:AL_MAP_LUT2 +select -assert-count 2 t:AL_MAP_LUT4 +select -assert-none t:AL_MAP_LUT1 t:AL_MAP_LUT2 t:AL_MAP_LUT4 %% t:* %D diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/memory.ys new file mode 100644 index 000000000..87b93c2fe --- /dev/null +++ b/tests/arch/anlogic/memory.ys @@ -0,0 +1,21 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +#ERROR: Failed to import cell gate.mem.0.0.0 (type EG_LOGIC_DRAM16X4) to SAT database. +#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top + +select -assert-count 8 t:AL_MAP_LUT2 +select -assert-count 8 t:AL_MAP_LUT4 +select -assert-count 8 t:AL_MAP_LUT5 +select -assert-count 36 t:AL_MAP_SEQ +select -assert-count 8 t:EG_LOGIC_DRAM16X4 #Why not AL_LOGIC_BRAM? +select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D diff --git a/tests/arch/anlogic/mux.ys b/tests/arch/anlogic/mux.ys new file mode 100644 index 000000000..3d5fe7c9a --- /dev/null +++ b/tests/arch/anlogic/mux.ys @@ -0,0 +1,42 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT6 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 3 t:AL_MAP_LUT4 +select -assert-count 1 t:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT4 t:AL_MAP_LUT6 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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-count 5 t:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT6 %% t:* %D diff --git a/tests/ice40/run-test.sh b/tests/arch/anlogic/run-test.sh index 2c72ca3a9..bf19b887d 100755 --- a/tests/ice40/run-test.sh +++ b/tests/arch/anlogic/run-test.sh @@ -6,7 +6,7 @@ for x in *.ys; do echo "all:: run-$x" echo "run-$x:" echo " @echo 'Running $x..'" - echo " @../../yosys -ql ${x%.ys}.log $x -w 'Yosys has only limited support for tri-state logic at the moment.'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" done for s in *.sh; do if [ "$s" != "run-test.sh" ]; then diff --git a/tests/arch/anlogic/shifter.ys b/tests/arch/anlogic/shifter.ys new file mode 100644 index 000000000..12df44b2a --- /dev/null +++ b/tests/arch/anlogic/shifter.ys @@ -0,0 +1,10 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # 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 8 t:AL_MAP_SEQ + +select -assert-none t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/anlogic/tribuf.ys b/tests/arch/anlogic/tribuf.ys new file mode 100644 index 000000000..eaa073750 --- /dev/null +++ b/tests/arch/anlogic/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v -map +/simcells.v synth_anlogic # 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 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/common/add_sub.v b/tests/arch/common/add_sub.v new file mode 100644 index 000000000..77e5f5745 --- /dev/null +++ b/tests/arch/common/add_sub.v @@ -0,0 +1,12 @@ +module top +( + input [3:0] x, + input [3:0] y, + + output [3:0] A, + output [3:0] B +); + + assign A = x + y; + assign B = x - y; +endmodule diff --git a/tests/arch/common/adffs.v b/tests/arch/common/adffs.v new file mode 100644 index 000000000..576bd81a6 --- /dev/null +++ b/tests/arch/common/adffs.v @@ -0,0 +1,43 @@ +module adff( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, posedge clr ) + if ( clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module adffn( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, negedge clr ) + if ( !clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module dffs( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk ) + if ( pre ) + q <= 1'b1; + else + q <= d; +endmodule + +module ndffnr( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( negedge clk ) + if ( !clr ) + q <= 1'b0; + else + q <= d; +endmodule diff --git a/tests/arch/common/counter.v b/tests/arch/common/counter.v new file mode 100644 index 000000000..9746fd701 --- /dev/null +++ b/tests/arch/common/counter.v @@ -0,0 +1,11 @@ +module top ( out, clk, reset );
+ output [7:0] out;
+ input clk, reset;
+ reg [7:0] out;
+
+ always @(posedge clk, posedge reset)
+ if (reset)
+ out <= 8'b0;
+ else
+ out <= out + 1;
+endmodule
diff --git a/tests/arch/common/dffs.v b/tests/arch/common/dffs.v new file mode 100644 index 000000000..636252d16 --- /dev/null +++ b/tests/arch/common/dffs.v @@ -0,0 +1,13 @@ +module dff ( input d, clk, output reg q ); + always @( posedge clk ) + q <= d; +endmodule + +module dffe( input d, clk, en, output reg q ); + initial begin + q = 0; + end + always @( posedge clk ) + if ( en ) + q <= d; +endmodule diff --git a/tests/arch/common/fsm.v b/tests/arch/common/fsm.v new file mode 100644 index 000000000..9d3fbb64a --- /dev/null +++ b/tests/arch/common/fsm.v @@ -0,0 +1,51 @@ + module fsm ( clock, reset, req_0, req_1, gnt_0, gnt_1 );
+ input clock,reset,req_0,req_1;
+ output gnt_0,gnt_1;
+ wire clock,reset,req_0,req_1;
+ reg gnt_0,gnt_1;
+
+ parameter SIZE = 3;
+ parameter IDLE = 3'b001;
+ parameter GNT0 = 3'b010;
+ parameter GNT1 = 3'b100;
+ parameter GNT2 = 3'b101;
+
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+ state <= #1 IDLE;
+ gnt_0 <= 0;
+ gnt_1 <= 0;
+ end
+ else
+ case(state)
+ IDLE : if (req_0 == 1'b1) begin
+ state <= #1 GNT0;
+ gnt_0 <= 1;
+ end else if (req_1 == 1'b1) begin
+ gnt_1 <= 1;
+ state <= #1 GNT0;
+ end else begin
+ state <= #1 IDLE;
+ end
+ GNT0 : if (req_0 == 1'b1) begin
+ state <= #1 GNT0;
+ end else begin
+ gnt_0 <= 0;
+ state <= #1 IDLE;
+ end
+ GNT1 : if (req_1 == 1'b1) begin
+ state <= #1 GNT2;
+ gnt_1 <= req_0;
+ end
+ GNT2 : if (req_0 == 1'b1) begin
+ state <= #1 GNT1;
+ gnt_1 <= req_1;
+ end
+ default : state <= #1 IDLE;
+ endcase
+ end
+endmodule
diff --git a/tests/arch/common/latches.v b/tests/arch/common/latches.v new file mode 100644 index 000000000..60b757103 --- /dev/null +++ b/tests/arch/common/latches.v @@ -0,0 +1,21 @@ +module latchp ( input d, clk, en, output reg q ); + always @* + if ( en ) + q <= d; +endmodule + +module latchn ( input d, clk, en, output reg q ); + always @* + if ( !en ) + q <= d; +endmodule + +module latchsr ( input d, clk, en, clr, pre, output reg q ); + always @* + if ( clr ) + q <= 1'b0; + else if ( pre ) + q <= 1'b1; + else if ( en ) + q <= d; +endmodule diff --git a/tests/arch/common/logic.v b/tests/arch/common/logic.v new file mode 100644 index 000000000..c17899fa0 --- /dev/null +++ b/tests/arch/common/logic.v @@ -0,0 +1,16 @@ +module top +( + input [0:7] in, + output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10 +); + assign B1 = in[0] & in[1]; + assign B2 = in[0] | in[1]; + assign B3 = in[0] ~& in[1]; + assign B4 = in[0] ~| in[1]; + assign B5 = in[0] ^ in[1]; + assign B6 = in[0] ~^ in[1]; + assign B7 = ~in[0]; + assign B8 = in[0]; + assign B9 = in[0:1] && in [2:3]; + assign B10 = in[0:1] || in [2:3]; +endmodule diff --git a/tests/ice40/memory.v b/tests/arch/common/memory.v index cb7753f7b..cb7753f7b 100644 --- a/tests/ice40/memory.v +++ b/tests/arch/common/memory.v diff --git a/tests/arch/common/mul.v b/tests/arch/common/mul.v new file mode 100644 index 000000000..437a91cfc --- /dev/null +++ b/tests/arch/common/mul.v @@ -0,0 +1,9 @@ +module top +( + input [5:0] x, + input [5:0] y, + + output [11:0] A, +); + assign A = x * y; +endmodule diff --git a/tests/arch/common/mux.v b/tests/arch/common/mux.v new file mode 100644 index 000000000..71c1ac7f2 --- /dev/null +++ b/tests/arch/common/mux.v @@ -0,0 +1,60 @@ +module mux2 (S,A,B,Y); + input S; + input A,B; + output reg Y; + + always @(*) + Y = (S)? B : A; +endmodule + +module mux4 ( S, D, Y ); + input[1:0] S; + input[3:0] D; + output Y; + + reg Y; + wire[1:0] S; + wire[3:0] D; + + always @* + begin + case( S ) + 0 : Y = D[0]; + 1 : Y = D[1]; + 2 : Y = D[2]; + 3 : Y = D[3]; + endcase + end +endmodule + +module mux8 ( S, D, Y ); + input[2:0] S; + input[7:0] D; + output Y; + + reg Y; + wire[2:0] S; + wire[7:0] D; + + always @* + begin + case( S ) + 0 : Y = D[0]; + 1 : Y = D[1]; + 2 : Y = D[2]; + 3 : Y = D[3]; + 4 : Y = D[4]; + 5 : Y = D[5]; + 6 : Y = D[6]; + 7 : Y = D[7]; + endcase + end +endmodule + +module mux16 (D, S, Y); + input [15:0] D; + input [3:0] S; + output Y; + + assign Y = D[S]; +endmodule diff --git a/tests/ice40/shifter.v b/tests/arch/common/shifter.v index c55632552..cace3b588 100644 --- a/tests/ice40/shifter.v +++ b/tests/arch/common/shifter.v @@ -1,22 +1,11 @@ -module top (
-out,
-clk,
-in
-);
+module top(out, clk, in);
output [7:0] out;
input signed clk, in;
reg signed [7:0] out = 0;
always @(posedge clk)
begin
-`ifndef BUG
out <= out >> 1;
out[7] <= in;
-`else
-
- out <= out << 1;
- out[7] <= in;
-`endif
- end
-
+ end
endmodule
diff --git a/tests/arch/common/tribuf.v b/tests/arch/common/tribuf.v new file mode 100644 index 000000000..e1d701611 --- /dev/null +++ b/tests/arch/common/tribuf.v @@ -0,0 +1,8 @@ +module tristate(en, i, o); + input en; + input i; + output reg o; + + always @(en or i) + o <= (en)? i : 1'bZ; +endmodule diff --git a/tests/arch/ecp5/.gitignore b/tests/arch/ecp5/.gitignore new file mode 100644 index 000000000..1d329c933 --- /dev/null +++ b/tests/arch/ecp5/.gitignore @@ -0,0 +1,2 @@ +*.log +/run-test.mk diff --git a/tests/arch/ecp5/add_sub.ys b/tests/arch/ecp5/add_sub.ys new file mode 100644 index 000000000..d85ce792e --- /dev/null +++ b/tests/arch/ecp5/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 10 t:LUT4 +select -assert-none t:LUT4 %% t:* %D + diff --git a/tests/arch/ecp5/adffs.ys b/tests/arch/ecp5/adffs.ys new file mode 100644 index 000000000..01605df70 --- /dev/null +++ b/tests/arch/ecp5/adffs.ys @@ -0,0 +1,40 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D diff --git a/tests/arch/ecp5/counter.ys b/tests/arch/ecp5/counter.ys new file mode 100644 index 000000000..f9f60fbff --- /dev/null +++ b/tests/arch/ecp5/counter.ys @@ -0,0 +1,10 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C +select -assert-count 8 t:TRELLIS_FF +select -assert-none t:CCU2C t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/dffs.ys b/tests/arch/ecp5/dffs.ys new file mode 100644 index 000000000..be97972db --- /dev/null +++ b/tests/arch/ecp5/dffs.ys @@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D
\ No newline at end of file diff --git a/tests/ice40/dpram.v b/tests/arch/ecp5/dpram.v index 3ea4c1f27..3ea4c1f27 100644 --- a/tests/ice40/dpram.v +++ b/tests/arch/ecp5/dpram.v diff --git a/tests/arch/ecp5/dpram.ys b/tests/arch/ecp5/dpram.ys new file mode 100644 index 000000000..3bc6bc1d0 --- /dev/null +++ b/tests/arch/ecp5/dpram.ys @@ -0,0 +1,18 @@ +read_verilog dpram.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter + +#Blocked by issue #1358 (Missing ECP5 simulation models) +#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) to SAT database. +#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:DP16KD +select -assert-none t:DP16KD %% t:* %D diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys new file mode 100644 index 000000000..f834a4c6b --- /dev/null +++ b/tests/arch/ecp5/fsm.ys @@ -0,0 +1,12 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +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 +select -assert-count 1 t:L6MUX21 +select -assert-count 13 t:LUT4 +select -assert-count 5 t:PFUMX +select -assert-count 5 t:TRELLIS_FF +select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/latches.ys b/tests/arch/ecp5/latches.ys new file mode 100644 index 000000000..3d011d74f --- /dev/null +++ b/tests/arch/ecp5/latches.ys @@ -0,0 +1,34 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ecp5 +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 + +select -assert-none t:LUT4 %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ecp5 +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 + +select -assert-none t:LUT4 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ecp5 +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:LUT4 +select -assert-count 1 t:PFUMX + +select -assert-none t:LUT4 t:PFUMX %% t:* %D diff --git a/tests/arch/ecp5/logic.ys b/tests/arch/ecp5/logic.ys new file mode 100644 index 000000000..3298b198f --- /dev/null +++ b/tests/arch/ecp5/logic.ys @@ -0,0 +1,8 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 9 t:LUT4 +select -assert-none t:LUT4 %% t:* %D diff --git a/tests/ice40/macc.v b/tests/arch/ecp5/macc.v index 6c3676c83..63a3d3a74 100644 --- a/tests/ice40/macc.v +++ b/tests/arch/ecp5/macc.v @@ -2,8 +2,8 @@ Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 77]. */ module top(clk,a,b,c,set); -parameter A_WIDTH = 6 /*4*/; -parameter B_WIDTH = 6 /*3*/; +parameter A_WIDTH = 4; +parameter B_WIDTH = 3; input set; input clk; input signed [(A_WIDTH - 1):0] a; diff --git a/tests/arch/ecp5/macc.ys b/tests/arch/ecp5/macc.ys new file mode 100644 index 000000000..1863ea4d2 --- /dev/null +++ b/tests/arch/ecp5/macc.ys @@ -0,0 +1,13 @@ +read_verilog macc.v +hierarchy -top top +proc +# Blocked by issue #1358 (Missing ECP5 simulation models) +#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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:MULT18X18D +select -assert-count 4 t:CCU2C +select -assert-count 7 t:TRELLIS_FF + +select -assert-none t:CCU2C t:MULT18X18D t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/memory.ys new file mode 100644 index 000000000..c82b7b405 --- /dev/null +++ b/tests/arch/ecp5/memory.ys @@ -0,0 +1,19 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 24 t:L6MUX21 +select -assert-count 71 t:LUT4 +select -assert-count 32 t:PFUMX +select -assert-count 8 t:TRELLIS_DPR16X4 +select -assert-count 35 t:TRELLIS_FF +select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/mul.ys b/tests/arch/ecp5/mul.ys new file mode 100644 index 000000000..2105be52c --- /dev/null +++ b/tests/arch/ecp5/mul.ys @@ -0,0 +1,11 @@ +read_verilog ../common/mul.v +hierarchy -top top +proc +# Blocked by issue #1358 (Missing ECP5 simulation models) +#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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:MULT18X18D +select -assert-none t:MULT18X18D %% t:* %D diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys new file mode 100644 index 000000000..92463aa32 --- /dev/null +++ b/tests/arch/ecp5/mux.ys @@ -0,0 +1,46 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:LUT4 +select -assert-none t:LUT4 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:L6MUX21 +select -assert-count 4 t:LUT4 +select -assert-count 2 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:L6MUX21 +select -assert-count 7 t:LUT4 +select -assert-count 2 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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-count 8 t:L6MUX21 +select -assert-count 26 t:LUT4 +select -assert-count 12 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D diff --git a/tests/ice40/rom.v b/tests/arch/ecp5/rom.v index 0a0f41f37..0a0f41f37 100644 --- a/tests/ice40/rom.v +++ b/tests/arch/ecp5/rom.v diff --git a/tests/arch/ecp5/rom.ys b/tests/arch/ecp5/rom.ys new file mode 100644 index 000000000..98645ae43 --- /dev/null +++ b/tests/arch/ecp5/rom.ys @@ -0,0 +1,10 @@ +read_verilog rom.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 6 t:LUT4 +select -assert-count 3 t:PFUMX +select -assert-none t:LUT4 t:PFUMX %% t:* %D diff --git a/tests/xilinx/run-test.sh b/tests/arch/ecp5/run-test.sh index ea56b70f0..bf19b887d 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/ecp5/run-test.sh @@ -6,7 +6,7 @@ for x in *.ys; do echo "all:: run-$x" echo "run-$x:" echo " @echo 'Running $x..'" - echo " @../../yosys -ql ${x%.ys}.log $x" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" done for s in *.sh; do if [ "$s" != "run-test.sh" ]; then diff --git a/tests/arch/ecp5/shifter.ys b/tests/arch/ecp5/shifter.ys new file mode 100644 index 000000000..3f0079f4a --- /dev/null +++ b/tests/arch/ecp5/shifter.ys @@ -0,0 +1,10 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 8 t:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/tribuf.ys b/tests/arch/ecp5/tribuf.ys new file mode 100644 index 000000000..0118705a2 --- /dev/null +++ b/tests/arch/ecp5/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v -map +/simcells.v synth_ecp5 # 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 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/xilinx/.gitignore b/tests/arch/efinix/.gitignore index b48f808a1..b48f808a1 100644 --- a/tests/xilinx/.gitignore +++ b/tests/arch/efinix/.gitignore diff --git a/tests/arch/efinix/add_sub.ys b/tests/arch/efinix/add_sub.ys new file mode 100644 index 000000000..20523c059 --- /dev/null +++ b/tests/arch/efinix/add_sub.ys @@ -0,0 +1,10 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 10 t:EFX_ADD +select -assert-count 4 t:EFX_LUT4 +select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D + diff --git a/tests/arch/efinix/adffs.ys b/tests/arch/efinix/adffs.ys new file mode 100644 index 000000000..49dc7f256 --- /dev/null +++ b/tests/arch/efinix/adffs.ys @@ -0,0 +1,50 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE + +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE + +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys new file mode 100644 index 000000000..d20b8ae27 --- /dev/null +++ b/tests/arch/efinix/counter.ys @@ -0,0 +1,12 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 8 t:EFX_FF +select -assert-count 9 t:EFX_ADD +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_ADD %% t:* %D diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys new file mode 100644 index 000000000..af787ab67 --- /dev/null +++ b/tests/arch/efinix/dffs.ys @@ -0,0 +1,24 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE + +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys new file mode 100644 index 000000000..a8ba70fdb --- /dev/null +++ b/tests/arch/efinix/fsm.ys @@ -0,0 +1,14 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten +#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. +#equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +equiv_opt -map +/efinix/cells_sim.v synth_efinix # equivalency check +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 + +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 6 t:EFX_FF +select -assert-count 15 t:EFX_LUT4 +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/latches.ys b/tests/arch/efinix/latches.ys new file mode 100644 index 000000000..1b1c00023 --- /dev/null +++ b/tests/arch/efinix/latches.ys @@ -0,0 +1,33 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_efinix +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_efinix +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_efinix +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/logic.ys b/tests/arch/efinix/logic.ys new file mode 100644 index 000000000..76e98e079 --- /dev/null +++ b/tests/arch/efinix/logic.ys @@ -0,0 +1,9 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 9 t:EFX_LUT4 +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/memory.ys b/tests/arch/efinix/memory.ys new file mode 100644 index 000000000..6f6acdcde --- /dev/null +++ b/tests/arch/efinix/memory.ys @@ -0,0 +1,18 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +#ERROR: Called with -verify and proof did fail! +#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter +sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_RAM_5K +select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D diff --git a/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys new file mode 100644 index 000000000..b46f641e1 --- /dev/null +++ b/tests/arch/efinix/mux.ys @@ -0,0 +1,41 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 5 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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-count 12 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/run-test.sh b/tests/arch/efinix/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/efinix/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/efinix/shifter.ys b/tests/arch/efinix/shifter.ys new file mode 100644 index 000000000..54f71167f --- /dev/null +++ b/tests/arch/efinix/shifter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 8 t:EFX_FF +select -assert-none t:EFX_GBUFCE t:EFX_FF %% t:* %D diff --git a/tests/arch/efinix/tribuf.ys b/tests/arch/efinix/tribuf.ys new file mode 100644 index 000000000..47904f2d5 --- /dev/null +++ b/tests/arch/efinix/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/efinix/cells_sim.v -map +/simcells.v synth_efinix # 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 +#Internal cell type used. Need support it. +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/ice40/.gitignore b/tests/arch/ice40/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/ice40/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/ice40/add_sub.ys b/tests/arch/ice40/add_sub.ys index 4a998d98d..578ec0803 100644 --- a/tests/ice40/add_sub.ys +++ b/tests/arch/ice40/add_sub.ys @@ -1,4 +1,4 @@ -read_verilog add_sub.v +read_verilog ../common/add_sub.v hierarchy -top top equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) diff --git a/tests/arch/ice40/adffs.ys b/tests/arch/ice40/adffs.ys new file mode 100644 index 000000000..e5dbabb43 --- /dev/null +++ b/tests/arch/ice40/adffs.ys @@ -0,0 +1,39 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFFR +select -assert-none t:SB_DFFR %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFFR +select -assert-count 1 t:SB_LUT4 +select -assert-none t:SB_DFFR t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFFSS +select -assert-none t:SB_DFFSS %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFFNSR +select -assert-count 1 t:SB_LUT4 +select -assert-none t:SB_DFFNSR t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/counter.ys b/tests/arch/ice40/counter.ys index c65c21622..f112eb97d 100644 --- a/tests/ice40/counter.ys +++ b/tests/arch/ice40/counter.ys @@ -1,4 +1,4 @@ -read_verilog counter.v +read_verilog ../common/counter.v hierarchy -top top proc flatten diff --git a/tests/arch/ice40/dffs.ys b/tests/arch/ice40/dffs.ys new file mode 100644 index 000000000..b28a5a91f --- /dev/null +++ b/tests/arch/ice40/dffs.ys @@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFF +select -assert-none t:SB_DFF %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFFE +select -assert-none t:SB_DFFE %% t:* %D
\ No newline at end of file diff --git a/tests/arch/ice40/dpram.v b/tests/arch/ice40/dpram.v new file mode 100644 index 000000000..3ea4c1f27 --- /dev/null +++ b/tests/arch/ice40/dpram.v @@ -0,0 +1,23 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72]. +*/ +module top (din, write_en, waddr, wclk, raddr, rclk, dout); +parameter addr_width = 8; +parameter data_width = 8; +input [addr_width-1:0] waddr, raddr; +input [data_width-1:0] din; +input write_en, wclk, rclk; +output [data_width-1:0] dout; +reg [data_width-1:0] dout; +reg [data_width-1:0] mem [(1<<addr_width)-1:0] +/* synthesis syn_ramstyle = "no_rw_check" */ ; +always @(posedge wclk) // Write memory. +begin +if (write_en) +mem[waddr] <= din; // Using write address bus. +end +always @(posedge rclk) // Read memory. +begin +dout <= mem[raddr]; // Using read address bus. +end +endmodule diff --git a/tests/ice40/dpram.ys b/tests/arch/ice40/dpram.ys index 4f6a253ea..4f6a253ea 100644 --- a/tests/ice40/dpram.ys +++ b/tests/arch/ice40/dpram.ys diff --git a/tests/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index 4cc8629d6..5aacc6c73 100644 --- a/tests/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -1,10 +1,10 @@ -read_verilog fsm.v -hierarchy -top top +read_verilog ../common/fsm.v +hierarchy -top fsm proc flatten equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 +cd fsm # Constrain all select calls below inside the top module select -assert-count 2 t:SB_DFFESR select -assert-count 2 t:SB_DFFSR diff --git a/tests/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index b17c69c91..b17c69c91 100644 --- a/tests/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys diff --git a/tests/arch/ice40/latches.ys b/tests/arch/ice40/latches.ys new file mode 100644 index 000000000..b06dd630b --- /dev/null +++ b/tests/arch/ice40/latches.ys @@ -0,0 +1,33 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ice40 +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ice40 +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ice40 +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/logic.ys b/tests/arch/ice40/logic.ys index fc5e5b1d8..7432f5b1f 100644 --- a/tests/ice40/logic.ys +++ b/tests/arch/ice40/logic.ys @@ -1,4 +1,4 @@ -read_verilog logic.v +read_verilog ../common/logic.v hierarchy -top top equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) diff --git a/tests/arch/ice40/macc.v b/tests/arch/ice40/macc.v new file mode 100644 index 000000000..6f68e7500 --- /dev/null +++ b/tests/arch/ice40/macc.v @@ -0,0 +1,47 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 77]. +*/ +module top(clk,a,b,c,set); +parameter A_WIDTH = 6 /*4*/; +parameter B_WIDTH = 6 /*3*/; +input set; +input clk; +input signed [(A_WIDTH - 1):0] a; +input signed [(B_WIDTH - 1):0] b; +output signed [(A_WIDTH + B_WIDTH - 1):0] c; +reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c; +assign c = reg_tmp_c; +always @(posedge clk) +begin + if(set) + begin + reg_tmp_c <= 0; + end + else + begin + reg_tmp_c <= a * b + c; + end +end +endmodule + +module top2(clk,a,b,c,hold); +parameter A_WIDTH = 6 /*4*/; +parameter B_WIDTH = 6 /*3*/; +input hold; +input clk; +input signed [(A_WIDTH - 1):0] a; +input signed [(B_WIDTH - 1):0] b; +output signed [(A_WIDTH + B_WIDTH - 1):0] c; +reg signed [A_WIDTH-1:0] reg_a; +reg signed [B_WIDTH-1:0] reg_b; +reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c; +assign c = reg_tmp_c; +always @(posedge clk) +begin + if (!hold) begin + reg_a <= a; + reg_b <= b; + reg_tmp_c <= reg_a * reg_b + c; + end +end +endmodule diff --git a/tests/arch/ice40/macc.ys b/tests/arch/ice40/macc.ys new file mode 100644 index 000000000..fd30e79c5 --- /dev/null +++ b/tests/arch/ice40/macc.ys @@ -0,0 +1,25 @@ +read_verilog macc.v +proc +design -save read + +hierarchy -top top +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # 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:SB_MAC16 +select -assert-none t:SB_MAC16 %% t:* %D + +design -load read +hierarchy -top top2 + +#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check + +equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check +clk2fflogic +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top2 # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_MAC16 +select -assert-none t:SB_MAC16 %% t:* %D diff --git a/tests/ice40/memory.ys b/tests/arch/ice40/memory.ys index a66afbae6..c356e67fb 100644 --- a/tests/ice40/memory.ys +++ b/tests/arch/ice40/memory.ys @@ -1,4 +1,4 @@ -read_verilog memory.v +read_verilog ../common/memory.v hierarchy -top top proc memory -nomap diff --git a/tests/ice40/mul.ys b/tests/arch/ice40/mul.ys index 8a0822a84..9891b77d6 100644 --- a/tests/ice40/mul.ys +++ b/tests/arch/ice40/mul.ys @@ -1,4 +1,4 @@ -read_verilog mul.v +read_verilog ../common/mul.v hierarchy -top top equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) diff --git a/tests/arch/ice40/mux.ys b/tests/arch/ice40/mux.ys new file mode 100644 index 000000000..99822391d --- /dev/null +++ b/tests/arch/ice40/mux.ys @@ -0,0 +1,40 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 2 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 5 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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-count 11 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/rom.v b/tests/arch/ice40/rom.v new file mode 100644 index 000000000..0a0f41f37 --- /dev/null +++ b/tests/arch/ice40/rom.v @@ -0,0 +1,18 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74]. +*/ +module top(data, addr); +output [3:0] data; +input [4:0] addr; +always @(addr) begin +case (addr) +0 : data = 'h4; +1 : data = 'h9; +2 : data = 'h1; +15 : data = 'h8; +16 : data = 'h1; +17 : data = 'h0; +default : data = 'h0; +endcase +end +endmodule diff --git a/tests/ice40/rom.ys b/tests/arch/ice40/rom.ys index 41d214e2a..41d214e2a 100644 --- a/tests/ice40/rom.ys +++ b/tests/arch/ice40/rom.ys diff --git a/tests/arch/ice40/run-test.sh b/tests/arch/ice40/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/ice40/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/ice40/shifter.ys b/tests/arch/ice40/shifter.ys index 47d95d298..08ea64f3d 100644 --- a/tests/ice40/shifter.ys +++ b/tests/arch/ice40/shifter.ys @@ -1,4 +1,4 @@ -read_verilog shifter.v +read_verilog ../common/shifter.v hierarchy -top top proc flatten diff --git a/tests/ice40/tribuf.ys b/tests/arch/ice40/tribuf.ys index d1e1b3108..10cded954 100644 --- a/tests/ice40/tribuf.ys +++ b/tests/arch/ice40/tribuf.ys @@ -1,9 +1,11 @@ -read_verilog tribuf.v -hierarchy -top top +read_verilog ../common/tribuf.v +hierarchy -top tristate proc +tribuf flatten +synth equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 # 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 +cd tristate # Constrain all select calls below inside the top module select -assert-count 1 t:$_TBUF_ select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/ice40/wrapcarry.ys b/tests/arch/ice40/wrapcarry.ys new file mode 100644 index 000000000..10c029e68 --- /dev/null +++ b/tests/arch/ice40/wrapcarry.ys @@ -0,0 +1,22 @@ +read_verilog <<EOT +module top(input A, B, CI, output O, CO); + SB_CARRY carry ( + .I0(A), + .I1(B), + .CI(CI), + .CO(CO) + ); + SB_LUT4 #( + .LUT_INIT(16'b 0110_1001_1001_0110) + ) adder ( + .I0(1'b0), + .I1(A), + .I2(B), + .I3(1'b0), + .O(O) + ); +endmodule +EOT + +ice40_wrapcarry +select -assert-count 1 t:$__ICE40_CARRY_WRAPPER diff --git a/tests/arch/xilinx/.gitignore b/tests/arch/xilinx/.gitignore new file mode 100644 index 000000000..c99b79371 --- /dev/null +++ b/tests/arch/xilinx/.gitignore @@ -0,0 +1,5 @@ +/*.log +/*.out +/run-test.mk +/*_uut.v +/test_macc diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys new file mode 100644 index 000000000..9dbddce47 --- /dev/null +++ b/tests/arch/xilinx/add_sub.ys @@ -0,0 +1,11 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 14 t:LUT2 +select -assert-count 6 t:MUXCY +select -assert-count 8 t:XORCY +select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D + diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys new file mode 100644 index 000000000..12c34415e --- /dev/null +++ b/tests/arch/xilinx/adffs.ys @@ -0,0 +1,51 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDCE + +select -assert-none t:BUFG t:FDCE %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDCE +select -assert-count 1 t:LUT1 + +select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE +select -assert-count 1 t:LUT2 + +select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE_1 +select -assert-count 1 t:LUT2 + +select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% t:* %D diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys new file mode 100644 index 000000000..57b645d19 --- /dev/null +++ b/tests/arch/xilinx/counter.ys @@ -0,0 +1,14 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDCE +select -assert-count 1 t:LUT1 +select -assert-count 7 t:MUXCY +select -assert-count 8 t:XORCY +select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys new file mode 100644 index 000000000..0bba4858f --- /dev/null +++ b/tests/arch/xilinx/dffs.ys @@ -0,0 +1,25 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D + + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D + diff --git a/tests/arch/xilinx/dsp_simd.ys b/tests/arch/xilinx/dsp_simd.ys new file mode 100644 index 000000000..956952327 --- /dev/null +++ b/tests/arch/xilinx/dsp_simd.ys @@ -0,0 +1,25 @@ +read_verilog <<EOT +module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24); +generate + genvar i; + // 4 x 12-bit adder + for (i = 0; i < 4; i++) + assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12]; + // 2 x 24-bit subtract + for (i = 0; i < 2; i++) + assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24]; +endgenerate +reg [3*12-1:0] ro; +always @* begin + ro[0*12+:12] = a[0*10+:10] + b[0*10+:10]; + ro[1*12+:12] = a[1*10+:10] + b[1*10+:10]; + ro[2*12+:12] = a[2*8+:8] + b[2*8+:8]; +end +assign o12[4*12+:3*12] = ro; +endmodule +EOT + +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx +design -load postopt +select -assert-count 3 t:DSP48E1 diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys new file mode 100644 index 000000000..d2b481421 --- /dev/null +++ b/tests/arch/xilinx/fsm.ys @@ -0,0 +1,14 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +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 + +select -assert-count 1 t:BUFG +select -assert-count 5 t:FDRE +select -assert-count 1 t:LUT3 +select -assert-count 2 t:LUT4 +select -assert-count 4 t:LUT6 +select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys new file mode 100644 index 000000000..fe7887e8d --- /dev/null +++ b/tests/arch/xilinx/latches.ys @@ -0,0 +1,35 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE + +select -assert-none t:LDCE %% t:* %D + + +design -load read +hierarchy -top latchn +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 1 t:LUT1 + +select -assert-none t:LDCE t:LUT1 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 2 t:LUT3 + +select -assert-none t:LDCE t:LUT3 %% t:* %D diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys new file mode 100644 index 000000000..c0f6da302 --- /dev/null +++ b/tests/arch/xilinx/logic.ys @@ -0,0 +1,11 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:LUT1 +select -assert-count 6 t:LUT2 +select -assert-count 2 t:LUT4 +select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D diff --git a/tests/arch/xilinx/macc.sh b/tests/arch/xilinx/macc.sh new file mode 100644 index 000000000..2272679ee --- /dev/null +++ b/tests/arch/xilinx/macc.sh @@ -0,0 +1,3 @@ +../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v +iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v +vvp -N ./test_macc diff --git a/tests/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v new file mode 100644 index 000000000..e36b2bab1 --- /dev/null +++ b/tests/arch/xilinx/macc.v @@ -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, b_reg; +reg sload_reg; +reg signed [2*SIZEIN-1:0] mult_reg; +reg signed [SIZEOUT-1:0] adder_out, 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, b_reg, a_reg2, b_reg2; +reg signed [2*SIZEIN-1:0] mult_reg = 0; +reg signed [SIZEOUT:0] adder_out = 0; +reg overflow_reg; +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 diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys new file mode 100644 index 000000000..6e884b35a --- /dev/null +++ b/tests/arch/xilinx/macc.ys @@ -0,0 +1,31 @@ +read_verilog macc.v +design -save read + +hierarchy -top macc +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -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:FDRE +select -assert-count 1 t:DSP48E1 +select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D + +design -load read +hierarchy -top macc2 +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -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:FDRE +select -assert-count 1 t:LUT2 +select -assert-count 41 t:LUT3 +select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D diff --git a/tests/arch/xilinx/macc_tb.v b/tests/arch/xilinx/macc_tb.v new file mode 100644 index 000000000..64aed05c4 --- /dev/null +++ b/tests/arch/xilinx/macc_tb.v @@ -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 diff --git a/tests/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys new file mode 100644 index 000000000..da1ed0e49 --- /dev/null +++ b/tests/arch/xilinx/memory.ys @@ -0,0 +1,17 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDRE +select -assert-count 8 t:RAM64X1D +select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys new file mode 100644 index 000000000..d76814966 --- /dev/null +++ b/tests/arch/xilinx/mul.ys @@ -0,0 +1,9 @@ +read_verilog ../common/mul.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 diff --git a/tests/arch/xilinx/mul_unsigned.v b/tests/arch/xilinx/mul_unsigned.v new file mode 100644 index 000000000..e3713a642 --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.v @@ -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 diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys new file mode 100644 index 000000000..62495b90c --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.ys @@ -0,0 +1,11 @@ +read_verilog mul_unsigned.v +hierarchy -top mul_unsigned +proc + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE +select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys new file mode 100644 index 000000000..821d0fab7 --- /dev/null +++ b/tests/arch/xilinx/mux.ys @@ -0,0 +1,45 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 +/xilinx/cells_sim.v synth_xilinx # 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 +/xilinx/cells_sim.v synth_xilinx # 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 +/xilinx/cells_sim.v synth_xilinx # 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-count 5 t:LUT6 + +select -assert-none t:LUT6 %% t:* %D diff --git a/tests/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys index ea2f20487..ea2f20487 100644 --- a/tests/xilinx/pmgen_xilinx_srl.ys +++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/xilinx/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys new file mode 100644 index 000000000..455437f18 --- /dev/null +++ b/tests/arch/xilinx/shifter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:FDRE +select -assert-none t:BUFG t:FDRE %% t:* %D diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys new file mode 100644 index 000000000..4697703ca --- /dev/null +++ b/tests/arch/xilinx/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # 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 +# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225 +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/xilinx/xilinx_srl.v b/tests/arch/xilinx/xilinx_srl.v index bc2a15ab2..bc2a15ab2 100644 --- a/tests/xilinx/xilinx_srl.v +++ b/tests/arch/xilinx/xilinx_srl.v diff --git a/tests/xilinx/xilinx_srl.ys b/tests/arch/xilinx/xilinx_srl.ys index b8df0e55a..b8df0e55a 100644 --- a/tests/xilinx/xilinx_srl.ys +++ b/tests/arch/xilinx/xilinx_srl.ys diff --git a/tests/ice40/add_sub.v b/tests/ice40/add_sub.v deleted file mode 100644 index 177c32e30..000000000 --- a/tests/ice40/add_sub.v +++ /dev/null @@ -1,13 +0,0 @@ -module top -( - input [3:0] x, - input [3:0] y, - - output [3:0] A, - output [3:0] B - ); - -assign A = x + y; -assign B = x - y; - -endmodule diff --git a/tests/ice40/adffs.v b/tests/ice40/adffs.v deleted file mode 100644 index 93c8bf52c..000000000 --- a/tests/ice40/adffs.v +++ /dev/null @@ -1,91 +0,0 @@ -module adff - ( input d, clk, clr, output reg q ); - initial begin - q = 0; - end - always @( posedge clk, posedge clr ) - if ( clr ) - q <= 1'b0; - else - q <= d; -endmodule - -module adffn - ( input d, clk, clr, output reg q ); - initial begin - q = 0; - end - always @( posedge clk, negedge clr ) - if ( !clr ) - q <= 1'b0; - else - q <= d; -endmodule - -module dffsr - ( input d, clk, pre, clr, output reg q ); - initial begin - q = 0; - end - always @( posedge clk, posedge pre, posedge clr ) - if ( clr ) - q <= 1'b0; - else if ( pre ) - q <= 1'b1; - else - q <= d; -endmodule - -module ndffnsnr - ( input d, clk, pre, clr, output reg q ); - initial begin - q = 0; - end - always @( negedge clk, negedge pre, negedge clr ) - if ( !clr ) - q <= 1'b0; - else if ( !pre ) - q <= 1'b1; - else - q <= d; -endmodule - -module top ( -input clk, -input clr, -input pre, -input a, -output b,b1,b2,b3 -); - -dffsr u_dffsr ( - .clk (clk ), - .clr (clr), - .pre (pre), - .d (a ), - .q (b ) - ); - -ndffnsnr u_ndffnsnr ( - .clk (clk ), - .clr (clr), - .pre (pre), - .d (a ), - .q (b1 ) - ); - -adff u_adff ( - .clk (clk ), - .clr (clr), - .d (a ), - .q (b2 ) - ); - -adffn u_adffn ( - .clk (clk ), - .clr (clr), - .d (a ), - .q (b3 ) - ); - -endmodule diff --git a/tests/ice40/adffs.ys b/tests/ice40/adffs.ys deleted file mode 100644 index 14b251c5c..000000000 --- a/tests/ice40/adffs.ys +++ /dev/null @@ -1,12 +0,0 @@ -read_verilog adffs.v -proc -async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock -flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFF -select -assert-count 1 t:SB_DFFN -select -assert-count 2 t:SB_DFFSR -select -assert-count 7 t:SB_LUT4 -select -assert-none t:SB_DFF t:SB_DFFN t:SB_DFFSR t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/alu.v b/tests/ice40/alu.v deleted file mode 100644 index f82cc2e21..000000000 --- a/tests/ice40/alu.v +++ /dev/null @@ -1,19 +0,0 @@ -module top ( - input clock, - input [31:0] dinA, dinB, - input [2:0] opcode, - output reg [31:0] dout -); - always @(posedge clock) begin - case (opcode) - 0: dout <= dinA + dinB; - 1: dout <= dinA - dinB; - 2: dout <= dinA >> dinB; - 3: dout <= $signed(dinA) >>> dinB; - 4: dout <= dinA << dinB; - 5: dout <= dinA & dinB; - 6: dout <= dinA | dinB; - 7: dout <= dinA ^ dinB; - endcase - end -endmodule diff --git a/tests/ice40/alu.ys b/tests/ice40/alu.ys deleted file mode 100644 index bd859efc4..000000000 --- a/tests/ice40/alu.ys +++ /dev/null @@ -1,11 +0,0 @@ -read_verilog alu.v -hierarchy -top top -proc -flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 62 t:SB_CARRY -select -assert-count 32 t:SB_DFF -select -assert-count 655 t:SB_LUT4 -select -assert-none t:SB_CARRY t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/counter.v b/tests/ice40/counter.v deleted file mode 100644 index 52852f8ac..000000000 --- a/tests/ice40/counter.v +++ /dev/null @@ -1,17 +0,0 @@ -module top (
-out,
-clk,
-reset
-);
- output [7:0] out;
- input clk, reset;
- reg [7:0] out;
-
- always @(posedge clk, posedge reset)
- if (reset) begin
- out <= 8'b0 ;
- end else
- out <= out + 1;
-
-
-endmodule
diff --git a/tests/ice40/dffs.v b/tests/ice40/dffs.v deleted file mode 100644 index d97840c43..000000000 --- a/tests/ice40/dffs.v +++ /dev/null @@ -1,37 +0,0 @@ -module dff - ( input d, clk, output reg q ); - always @( posedge clk ) - q <= d; -endmodule - -module dffe - ( input d, clk, en, output reg q ); - initial begin - q = 0; - end - always @( posedge clk ) - if ( en ) - q <= d; -endmodule - -module top ( -input clk, -input en, -input a, -output b,b1, -); - -dff u_dff ( - .clk (clk ), - .d (a ), - .q (b ) - ); - -dffe u_ndffe ( - .clk (clk ), - .en (en), - .d (a ), - .q (b1 ) - ); - -endmodule diff --git a/tests/ice40/dffs.ys b/tests/ice40/dffs.ys deleted file mode 100644 index ee7f884b1..000000000 --- a/tests/ice40/dffs.ys +++ /dev/null @@ -1,10 +0,0 @@ -read_verilog dffs.v -hierarchy -top top -proc -flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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:SB_DFF -select -assert-count 1 t:SB_DFFE -select -assert-none t:SB_DFF t:SB_DFFE %% t:* %D diff --git a/tests/ice40/div_mod.v b/tests/ice40/div_mod.v deleted file mode 100644 index 64a36707d..000000000 --- a/tests/ice40/div_mod.v +++ /dev/null @@ -1,13 +0,0 @@ -module top -( - input [3:0] x, - input [3:0] y, - - output [3:0] A, - output [3:0] B - ); - -assign A = x % y; -assign B = x / y; - -endmodule diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys deleted file mode 100644 index 21cac7144..000000000 --- a/tests/ice40/div_mod.ys +++ /dev/null @@ -1,9 +0,0 @@ -read_verilog div_mod.v -hierarchy -top top -flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 62 t:SB_LUT4 -select -assert-count 41 t:SB_CARRY -select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D diff --git a/tests/ice40/fsm.v b/tests/ice40/fsm.v deleted file mode 100644 index 0605bd102..000000000 --- a/tests/ice40/fsm.v +++ /dev/null @@ -1,73 +0,0 @@ - module fsm (
- clock,
- reset,
- req_0,
- req_1,
- gnt_0,
- gnt_1
- );
- input clock,reset,req_0,req_1;
- output gnt_0,gnt_1;
- wire clock,reset,req_0,req_1;
- reg gnt_0,gnt_1;
-
- parameter SIZE = 3 ;
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
-
- reg [SIZE-1:0] state;
- reg [SIZE-1:0] next_state;
-
- always @ (posedge clock)
- begin : FSM
- if (reset == 1'b1) begin
- state <= #1 IDLE;
- gnt_0 <= 0;
- gnt_1 <= 0;
- end else
- case(state)
- IDLE : if (req_0 == 1'b1) begin
- state <= #1 GNT0;
- gnt_0 <= 1;
- end else if (req_1 == 1'b1) begin
- gnt_1 <= 1;
- state <= #1 GNT0;
- end else begin
- state <= #1 IDLE;
- end
- GNT0 : if (req_0 == 1'b1) begin
- state <= #1 GNT0;
- end else begin
- gnt_0 <= 0;
- state <= #1 IDLE;
- end
- GNT1 : if (req_1 == 1'b1) begin
- state <= #1 GNT2;
- gnt_1 <= req_0;
- end
- GNT2 : if (req_0 == 1'b1) begin
- state <= #1 GNT1;
- gnt_1 <= req_1;
- end
- default : state <= #1 IDLE;
- endcase
- end
-
- endmodule
-
- module top (
-input clk,
-input rst,
-input a,
-input b,
-output g0,
-output g1
-);
-
-fsm u_fsm ( .clock(clk),
- .reset(rst),
- .req_0(a),
- .req_1(b),
- .gnt_0(g0),
- .gnt_1(g1));
-
-endmodule
diff --git a/tests/ice40/latches.v b/tests/ice40/latches.v deleted file mode 100644 index 9dc43e4c2..000000000 --- a/tests/ice40/latches.v +++ /dev/null @@ -1,58 +0,0 @@ -module latchp - ( input d, clk, en, output reg q ); - always @* - if ( en ) - q <= d; -endmodule - -module latchn - ( input d, clk, en, output reg q ); - always @* - if ( !en ) - q <= d; -endmodule - -module latchsr - ( input d, clk, en, clr, pre, output reg q ); - always @* - if ( clr ) - q <= 1'b0; - else if ( pre ) - q <= 1'b1; - else if ( en ) - q <= d; -endmodule - - -module top ( -input clk, -input clr, -input pre, -input a, -output b,b1,b2 -); - - -latchp u_latchp ( - .en (clk ), - .d (a ), - .q (b ) - ); - - -latchn u_latchn ( - .en (clk ), - .d (a ), - .q (b1 ) - ); - - -latchsr u_latchsr ( - .en (clk ), - .clr (clr), - .pre (pre), - .d (a ), - .q (b2 ) - ); - -endmodule diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys deleted file mode 100644 index f3562559e..000000000 --- a/tests/ice40/latches.ys +++ /dev/null @@ -1,15 +0,0 @@ -read_verilog latches.v -design -save read - -proc -async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock -flatten -synth_ice40 -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) - -design -load read -synth_ice40 -cd top -select -assert-count 4 t:SB_LUT4 -select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/logic.v b/tests/ice40/logic.v deleted file mode 100644 index e5343cae0..000000000 --- a/tests/ice40/logic.v +++ /dev/null @@ -1,18 +0,0 @@ -module top -( - input [0:7] in, - output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10 - ); - - assign B1 = in[0] & in[1]; - assign B2 = in[0] | in[1]; - assign B3 = in[0] ~& in[1]; - assign B4 = in[0] ~| in[1]; - assign B5 = in[0] ^ in[1]; - assign B6 = in[0] ~^ in[1]; - assign B7 = ~in[0]; - assign B8 = in[0]; - assign B9 = in[0:1] && in [2:3]; - assign B10 = in[0:1] || in [2:3]; - -endmodule diff --git a/tests/ice40/macc.ys b/tests/ice40/macc.ys deleted file mode 100644 index 0f4c19be5..000000000 --- a/tests/ice40/macc.ys +++ /dev/null @@ -1,13 +0,0 @@ -read_verilog macc.v -proc -hierarchy -top top -#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check - -equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -dsp -async2sync -equiv_opt -run prove: -assert null - -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:SB_MAC16 -select -assert-none t:SB_MAC16 %% t:* %D diff --git a/tests/ice40/mul.v b/tests/ice40/mul.v deleted file mode 100644 index d5b48b1d7..000000000 --- a/tests/ice40/mul.v +++ /dev/null @@ -1,11 +0,0 @@ -module top -( - input [5:0] x, - input [5:0] y, - - output [11:0] A, - ); - -assign A = x * y; - -endmodule diff --git a/tests/ice40/mux.v b/tests/ice40/mux.v deleted file mode 100644 index 0814b733e..000000000 --- a/tests/ice40/mux.v +++ /dev/null @@ -1,100 +0,0 @@ -module mux2 (S,A,B,Y); - input S; - input A,B; - output reg Y; - - always @(*) - Y = (S)? B : A; -endmodule - -module mux4 ( S, D, Y ); - -input[1:0] S; -input[3:0] D; -output Y; - -reg Y; -wire[1:0] S; -wire[3:0] D; - -always @* -begin - case( S ) - 0 : Y = D[0]; - 1 : Y = D[1]; - 2 : Y = D[2]; - 3 : Y = D[3]; - endcase -end - -endmodule - -module mux8 ( S, D, Y ); - -input[2:0] S; -input[7:0] D; -output Y; - -reg Y; -wire[2:0] S; -wire[7:0] D; - -always @* -begin - case( S ) - 0 : Y = D[0]; - 1 : Y = D[1]; - 2 : Y = D[2]; - 3 : Y = D[3]; - 4 : Y = D[4]; - 5 : Y = D[5]; - 6 : Y = D[6]; - 7 : Y = D[7]; - endcase -end - -endmodule - -module mux16 (D, S, Y); - input [15:0] D; - input [3:0] S; - output Y; - -assign Y = D[S]; - -endmodule - - -module top ( -input [3:0] S, -input [15:0] D, -output M2,M4,M8,M16 -); - -mux2 u_mux2 ( - .S (S[0]), - .A (D[0]), - .B (D[1]), - .Y (M2) - ); - - -mux4 u_mux4 ( - .S (S[1:0]), - .D (D[3:0]), - .Y (M4) - ); - -mux8 u_mux8 ( - .S (S[2:0]), - .D (D[7:0]), - .Y (M8) - ); - -mux16 u_mux16 ( - .S (S[3:0]), - .D (D[15:0]), - .Y (M16) - ); - -endmodule diff --git a/tests/ice40/mux.ys b/tests/ice40/mux.ys deleted file mode 100644 index 182b49499..000000000 --- a/tests/ice40/mux.ys +++ /dev/null @@ -1,8 +0,0 @@ -read_verilog mux.v -proc -flatten -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # 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 19 t:SB_LUT4 -select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/tribuf.v b/tests/ice40/tribuf.v deleted file mode 100644 index 870a02584..000000000 --- a/tests/ice40/tribuf.v +++ /dev/null @@ -1,23 +0,0 @@ -module tristate (en, i, o); - input en; - input i; - output o; - - assign o = en ? i : 1'bz; - -endmodule - - -module top ( -input en, -input a, -output b -); - -tristate u_tri ( - .en (en ), - .i (a ), - .o (b ) - ); - -endmodule diff --git a/tests/opt/opt_expr.ys b/tests/opt/opt_expr.ys index ecc2c8da8..e0acead82 100644 --- a/tests/opt/opt_expr.ys +++ b/tests/opt/opt_expr.ys @@ -204,7 +204,7 @@ endmodule EOT check -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i @@ -218,7 +218,7 @@ endmodule EOT check -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$alu r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i @@ -232,7 +232,7 @@ endmodule EOT check -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-count 1 t:$shiftx r:A_WIDTH=3 %i @@ -246,7 +246,7 @@ endmodule EOT check -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-count 1 t:$shiftx r:A_WIDTH=12 %i @@ -260,7 +260,7 @@ endmodule EOT check -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-count 1 t:$shift r:A_WIDTH=3 %i @@ -274,7 +274,7 @@ endmodule EOT check -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-count 1 t:$shift r:A_WIDTH=10 %i @@ -288,6 +288,6 @@ endmodule EOT check -equiv_opt opt_expr -keepdc +equiv_opt -assert opt_expr -keepdc design -load postopt select -assert-count 1 t:$shift r:A_WIDTH=13 %i diff --git a/tests/rpc/.gitignore b/tests/rpc/.gitignore new file mode 100644 index 000000000..397b4a762 --- /dev/null +++ b/tests/rpc/.gitignore @@ -0,0 +1 @@ +*.log diff --git a/tests/rpc/design.v b/tests/rpc/design.v new file mode 100644 index 000000000..80f1dac1a --- /dev/null +++ b/tests/rpc/design.v @@ -0,0 +1,8 @@ +module top(input [3:0] i, output [3:0] o); + python_inv #( + .width(4) + ) inv ( + .i(i), + .o(o), + ); +endmodule diff --git a/tests/rpc/exec.ys b/tests/rpc/exec.ys new file mode 100644 index 000000000..b46009fb9 --- /dev/null +++ b/tests/rpc/exec.ys @@ -0,0 +1,5 @@ +connect_rpc -exec python3 frontend.py stdio +read_verilog design.v +hierarchy -top top +flatten +select -assert-count 1 t:$neg diff --git a/tests/rpc/frontend.py b/tests/rpc/frontend.py new file mode 100644 index 000000000..eff41738a --- /dev/null +++ b/tests/rpc/frontend.py @@ -0,0 +1,126 @@ +def modules(): + return ["python_inv"] + +def derive(module, parameters): + assert module == r"python_inv" + if parameters.keys() != {r"\width"}: + raise ValueError("Invalid parameters") + return "ilang", r""" +module \impl + wire width {width:d} input 1 \i + wire width {width:d} output 2 \o + cell $neg $0 + parameter \A_SIGNED 1'0 + parameter \A_WIDTH 32'{width:b} + parameter \Y_WIDTH 32'{width:b} + connect \A \i + connect \Y \o + end +end +module \python_inv + wire width {width:d} input 1 \i + wire width {width:d} output 2 \o + cell \impl $0 + connect \i \i + connect \o \o + end +end +""".format(width=parameters[r"\width"]) + +# ---------------------------------------------------------------------------- + +import json +import argparse +import sys, socket, os +try: + import msvcrt, win32pipe, win32file +except ImportError: + msvcrt = win32pipe = win32file = None + +def map_parameter(parameter): + if parameter["type"] == "unsigned": + return int(parameter["value"], 2) + if parameter["type"] == "signed": + width = len(parameter["value"]) + value = int(parameter["value"], 2) + if value & (1 << (width - 1)): + value = -((1 << width) - value) + return value + if parameter["type"] == "string": + return parameter["value"] + if parameter["type"] == "real": + return float(parameter["value"]) + +def call(input_json): + input = json.loads(input_json) + if input["method"] == "modules": + return json.dumps({"modules": modules()}) + if input["method"] == "derive": + try: + frontend, source = derive(input["module"], + {name: map_parameter(value) for name, value in input["parameters"].items()}) + return json.dumps({"frontend": frontend, "source": source}) + except ValueError as e: + return json.dumps({"error": str(e)}) + +def main(): + parser = argparse.ArgumentParser() + modes = parser.add_subparsers(dest="mode") + mode_stdio = modes.add_parser("stdio") + if os.name == "posix": + mode_path = modes.add_parser("unix-socket") + if os.name == "nt": + mode_path = modes.add_parser("named-pipe") + mode_path.add_argument("path") + args = parser.parse_args() + + if args.mode == "stdio": + while True: + input = sys.stdin.readline() + if not input: break + sys.stdout.write(call(input) + "\n") + sys.stdout.flush() + + if args.mode == "unix-socket": + sock = socket.socket(socket.AF_UNIX, socket.SOCK_STREAM) + sock.bind(args.path) + try: + sock.listen(1) + conn, addr = sock.accept() + file = conn.makefile("rw") + while True: + input = file.readline() + if not input: break + file.write(call(input) + "\n") + file.flush() + finally: + sock.close() + os.unlink(args.path) + + if args.mode == "named-pipe": + pipe = win32pipe.CreateNamedPipe(args.path, win32pipe.PIPE_ACCESS_DUPLEX, + win32pipe.PIPE_TYPE_BYTE|win32pipe.PIPE_READMODE_BYTE|win32pipe.PIPE_WAIT, + 1, 4096, 4096, 0, None) + win32pipe.ConnectNamedPipe(pipe, None) + try: + while True: + input = b"" + while not input.endswith(b"\n"): + result, data = win32file.ReadFile(pipe, 4096) + assert result == 0 + input += data + assert not b"\n" in input or input.endswith(b"\n") + output = (call(input.decode("utf-8")) + "\n").encode("utf-8") + length = len(output) + while length > 0: + result, done = win32file.WriteFile(pipe, output) + assert result == 0 + length -= done + except win32file.error as e: + if e.args[0] == 109: # ERROR_BROKEN_PIPE + pass + else: + raise + +if __name__ == "__main__": + main() diff --git a/tests/rpc/run-test.sh b/tests/rpc/run-test.sh new file mode 100755 index 000000000..44ce7e674 --- /dev/null +++ b/tests/rpc/run-test.sh @@ -0,0 +1,6 @@ +#!/bin/bash +set -e +for x in *.ys; do + echo "Running $x.." + ../../yosys -ql ${x%.ys}.log $x +done diff --git a/tests/rpc/unix.ys b/tests/rpc/unix.ys new file mode 100644 index 000000000..cc7ec14ab --- /dev/null +++ b/tests/rpc/unix.ys @@ -0,0 +1,6 @@ +!python3 frontend.py unix-socket frontend.sock & sleep 0.1 +connect_rpc -path frontend.sock +read_verilog design.v +hierarchy -top top +flatten +select -assert-count 1 t:$neg diff --git a/tests/simple/peepopt.v b/tests/simple/peepopt.v deleted file mode 100644 index 1bf427897..000000000 --- a/tests/simple/peepopt.v +++ /dev/null @@ -1,13 +0,0 @@ -module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); -assign o = i[s*W+:W]; -endmodule - -module peepopt_shiftmul_1 (output y, input [2:0] w); -assign y = 1'b1 >> (w * (3'b110)); -endmodule - -module peepopt_muldiv_0(input [1:0] i, output [1:0] o); -wire [3:0] t; -assign t = i * 3; -assign o = t / 3; -endmodule diff --git a/tests/svtypes/.gitignore b/tests/svtypes/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/svtypes/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/svtypes/run-test.sh b/tests/svtypes/run-test.sh new file mode 100755 index 000000000..09a30eed1 --- /dev/null +++ b/tests/svtypes/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../yosys -ql ${x%.ys}.log $x" +done +for x in *.sv; do + if [ ! -f "${x%.sv}.ys" ]; then + echo "all:: check-$x" + echo "check-$x:" + echo " @echo 'Checking $x..'" + echo " @../../yosys -ql ${x%.sv}.log -p \"prep -top top; sat -verify -prove-asserts\" $x" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/svtypes/typedef_memory.sv b/tests/svtypes/typedef_memory.sv new file mode 100644 index 000000000..577e484ad --- /dev/null +++ b/tests/svtypes/typedef_memory.sv @@ -0,0 +1,10 @@ +module top(input [3:0] addr, wdata, input clk, wen, output reg [3:0] rdata); + typedef logic [3:0] ram16x4_t[0:15]; + + (ram16x4_t) mem; + + always @(posedge clk) begin + if (wen) mem[addr] <= wdata; + rdata <= mem[addr]; + end +endmodule diff --git a/tests/svtypes/typedef_memory.ys b/tests/svtypes/typedef_memory.ys new file mode 100644 index 000000000..93cf47bbe --- /dev/null +++ b/tests/svtypes/typedef_memory.ys @@ -0,0 +1,3 @@ +read_verilog -sv typedef_memory.sv +prep -top top +select -assert-count 1 t:$mem r:SIZE=16 %i r:WIDTH=4 %i diff --git a/tests/svtypes/typedef_memory_2.sv b/tests/svtypes/typedef_memory_2.sv new file mode 100644 index 000000000..f3089bf55 --- /dev/null +++ b/tests/svtypes/typedef_memory_2.sv @@ -0,0 +1,10 @@ +module top(input [3:0] addr, wdata, input clk, wen, output reg [3:0] rdata); + typedef logic [3:0] nibble; + + (nibble) mem[0:15]; + + always @(posedge clk) begin + if (wen) mem[addr] <= wdata; + rdata <= mem[addr]; + end +endmodule diff --git a/tests/svtypes/typedef_memory_2.ys b/tests/svtypes/typedef_memory_2.ys new file mode 100644 index 000000000..854e554f3 --- /dev/null +++ b/tests/svtypes/typedef_memory_2.ys @@ -0,0 +1,4 @@ +read_verilog -sv typedef_memory_2.sv +prep -top top +dump +select -assert-count 1 t:$mem r:SIZE=16 %i r:WIDTH=4 %i diff --git a/tests/svtypes/typedef_package.sv b/tests/svtypes/typedef_package.sv new file mode 100644 index 000000000..a1e16d4b1 --- /dev/null +++ b/tests/svtypes/typedef_package.sv @@ -0,0 +1,11 @@ +package pkg; + typedef logic [7:0] uint8_t; +endpackage + +module top; + + (* keep *) (pkg::uint8_t) a = 8'hAA; + + always @* assert(a == 8'hAA); + +endmodule diff --git a/tests/svtypes/typedef_param.sv b/tests/svtypes/typedef_param.sv new file mode 100644 index 000000000..ddbd471e0 --- /dev/null +++ b/tests/svtypes/typedef_param.sv @@ -0,0 +1,22 @@ +`define STRINGIFY(x) `"x`" +`define STATIC_ASSERT(x) if(!(x)) $error({"assert failed: ", `STRINGIFY(x)}) + +module top; + + typedef logic [1:0] uint2_t; + typedef logic signed [3:0] int4_t; + typedef logic signed [7:0] int8_t; + typedef (int8_t) char_t; + + parameter (uint2_t) int2 = 2'b10; + localparam (int4_t) int4 = -1; + localparam (int8_t) int8 = int4; + localparam (char_t) ch = int8; + + + `STATIC_ASSERT(int2 == 2'b10); + `STATIC_ASSERT(int4 == 4'b1111); + `STATIC_ASSERT(int8 == 8'b11111111); + `STATIC_ASSERT(ch == 8'b11111111); + +endmodule diff --git a/tests/svtypes/typedef_scopes.sv b/tests/svtypes/typedef_scopes.sv new file mode 100644 index 000000000..faa385bd6 --- /dev/null +++ b/tests/svtypes/typedef_scopes.sv @@ -0,0 +1,23 @@ + +typedef logic [3:0] outer_uint4_t; + +module top; + + (outer_uint4_t) u4_i = 8'hA5; + always @(*) assert(u4_i == 4'h5); + + typedef logic [3:0] inner_type; + (inner_type) inner_i1 = 8'h5A; + always @(*) assert(inner_i1 == 4'hA); + + if (1) begin: genblock + typedef logic [7:0] inner_type; + (inner_type) inner_gb_i = 8'hA5; + always @(*) assert(inner_gb_i == 8'hA5); + end + + (inner_type) inner_i2 = 8'h42; + always @(*) assert(inner_i2 == 4'h2); + + +endmodule diff --git a/tests/svtypes/typedef_simple.sv b/tests/svtypes/typedef_simple.sv new file mode 100644 index 000000000..7e760dee4 --- /dev/null +++ b/tests/svtypes/typedef_simple.sv @@ -0,0 +1,19 @@ +module top; + + typedef logic [1:0] uint2_t; + typedef logic signed [3:0] int4_t; + typedef logic signed [7:0] int8_t; + typedef (int8_t) char_t; + + (* keep *) (uint2_t) int2 = 2'b10; + (* keep *) (int4_t) int4 = -1; + (* keep *) (int8_t) int8 = int4; + (* keep *) (char_t) ch = int8; + + + always @* assert(int2 == 2'b10); + always @* assert(int4 == 4'b1111); + always @* assert(int8 == 8'b11111111); + always @* assert(ch == 8'b11111111); + +endmodule diff --git a/tests/techmap/aigmap.ys b/tests/techmap/aigmap.ys new file mode 100644 index 000000000..a40aa39f1 --- /dev/null +++ b/tests/techmap/aigmap.ys @@ -0,0 +1,10 @@ +read_verilog <<EOT +module top(input i, j, s, output o, p); +assign o = s ? j : i; +assign p = ~i; +endmodule +EOT + +select t:$mux +aigmap -select +select -assert-any % diff --git a/tests/techmap/autopurge.ys b/tests/techmap/autopurge.ys new file mode 100644 index 000000000..1eb99ec37 --- /dev/null +++ b/tests/techmap/autopurge.ys @@ -0,0 +1,62 @@ +# https://github.com/YosysHQ/yosys/issues/1381 +read_verilog <<EOT +module sub(input i, output o, (* techmap_autopurge *) input j); +foobar f(i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +(* blackbox *) +module sub(input i, output o, input j); +endmodule + +(* blackbox *) +module foobar(input i, output o, input j); +endmodule + +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +hierarchy +check -assert + +# https://github.com/YosysHQ/yosys/issues/1391 +design -reset +read_verilog <<EOT +module sub(input i, output o, (* techmap_autopurge *) input [1:0] j); +foobar f(i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +(* blackbox *) +module sub(input i, output o, input j); +endmodule + +(* blackbox *) +module foobar(input i, output o, input j); +endmodule + +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +hierarchy +check -assert + +read_verilog -overwrite <<EOT +module top(input i, output o); +wire j; +sub s0(i, o, j); +endmodule +EOT + +techmap -map %techmap +hierarchy diff --git a/tests/techmap/dff2dffs.ys b/tests/techmap/dff2dffs.ys new file mode 100644 index 000000000..13f1a3cf3 --- /dev/null +++ b/tests/techmap/dff2dffs.ys @@ -0,0 +1,50 @@ +read_verilog << EOT +module top(...); +input clk; +input d; +input sr; +output reg q0, q1, q2, q3, q4, q5; + +initial q0 = 1'b0; +initial q1 = 1'b0; +initial q2 = 1'b1; +initial q3 = 1'b1; +initial q4 = 1'bx; +initial q5 = 1'bx; + +always @(posedge clk) begin + q0 <= sr ? 1'b0 : d; + q1 <= sr ? 1'b1 : d; + q2 <= sr ? 1'b0 : d; + q3 <= sr ? 1'b1 : d; + q4 <= sr ? 1'b0 : d; + q5 <= sr ? 1'b1 : d; +end + +endmodule +EOT + +proc +simplemap +design -save ref + +dff2dffs +clean + +select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q1 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q2 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i + +design -load ref +dff2dffs -match-init +clean + +select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i +select -assert-count 0 w:q1 %x t:$__DFFS_PP1_ %i +select -assert-count 0 w:q2 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i diff --git a/tests/techmap/extractinv.ys b/tests/techmap/extractinv.ys new file mode 100644 index 000000000..6146f829a --- /dev/null +++ b/tests/techmap/extractinv.ys @@ -0,0 +1,41 @@ +read_verilog << EOT + +module ff4(...); +parameter [0:0] CLK_INV = 1'b0; +parameter [3:0] DATA_INV = 4'b0000; +(* invertible_pin = "CLK_INV" *) +input clk; +(* invertible_pin = "DATA_INV" *) +input [3:0] d; +output [3:0] q; +endmodule + +module inv(...); +output o; +input i; +endmodule + +module top(...); +input d0, d1, d2, d3; +input clk; +output q; +ff4 #(.DATA_INV(4'h5)) ff_inst (.clk(clk), .d({d3, d2, d1, d0}), .q(q)); +endmodule + +EOT + +extractinv -inv inv o:i +clean + +select -assert-count 2 top/t:inv +select -assert-count 2 top/t:inv top/t:ff4 %ci:+[d] %ci:+[o] %i + +select -assert-count 1 top/t:inv top/w:d0 %co:+[i] %i +select -assert-count 0 top/t:inv top/w:d1 %co:+[i] %i +select -assert-count 1 top/t:inv top/w:d2 %co:+[i] %i +select -assert-count 0 top/t:inv top/w:d3 %co:+[i] %i + +select -assert-count 0 top/t:ff4 top/w:d0 %co:+[d] %i +select -assert-count 1 top/t:ff4 top/w:d1 %co:+[d] %i +select -assert-count 0 top/t:ff4 top/w:d2 %co:+[d] %i +select -assert-count 1 top/t:ff4 top/w:d3 %co:+[d] %i diff --git a/tests/techmap/techmap_replace.ys b/tests/techmap/techmap_replace.ys new file mode 100644 index 000000000..c2f42d50b --- /dev/null +++ b/tests/techmap/techmap_replace.ys @@ -0,0 +1,18 @@ +read_verilog <<EOT +module sub(input i, output o, input j); +foobar _TECHMAP_REPLACE_(i, o, j); +wire _TECHMAP_REPLACE_.asdf = i ; +barfoo _TECHMAP_REPLACE_.blah (i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +select -assert-any w:s0.asdf +select -assert-any c:s0.blah diff --git a/tests/techmap/wireinit.ys b/tests/techmap/wireinit.ys new file mode 100644 index 000000000..89afaafb5 --- /dev/null +++ b/tests/techmap/wireinit.ys @@ -0,0 +1,108 @@ +read_verilog <<EOT +(* techmap_celltype = "$_DFF_P_" *) +module ffmap(...); +input D; +input C; +output Q; +parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx; + +ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C)); + +wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1; + +wire _TECHMAP_REMOVEINIT_Q_ = 1'b1; + +endmodule +EOT +design -stash map + +read_verilog <<EOT +(* techmap_celltype = "$_DFF_P_" *) +module ffmap(...); +input D; +input C; +output Q; +parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx; + +ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C)); + +wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1; + +wire _TECHMAP_REMOVEINIT_Q_ = 1'b0; + +endmodule +EOT +design -stash map_noremove + +read_verilog <<EOT +module ffbb (...); +parameter [0:0] INIT = 1'bx; +input D, C; +output Q; +endmodule + +module top(...); +input clk; +input d; +output reg q0 = 0; +output reg q1 = 1; +output reg qq0 = 0; +output reg qx; + +always @(posedge clk) begin + q0 <= d; + q1 <= d; + qq0 <= q0; + qx <= d; +end +endmodule +EOT + +design -save ref + +hierarchy -auto-top +proc +simplemap +techmap -map %map +clean +# Make sure the parameter was used properly. +select -assert-count 3 top/t:ffbb +select -set ff0 top/w:q0 %ci t:ffbb %i +select -set ffq0 top/w:qq0 %ci t:ffbb %i +select -set ffx top/w:qx %ci t:ffbb %i +select -assert-count 1 @ff0 +select -assert-count 1 @ffq0 +select -assert-count 1 @ffx +select -assert-count 1 @ff0 r:INIT=1'b0 %i +select -assert-count 1 @ffq0 r:INIT=1'b0 %i +select -assert-count 1 @ffx r:INIT=1'bx %i +select -assert-count 0 top/w:q1 %ci t:ffbb %i +# Make sure the init values are dropped from the wires iff mapping was performed. +select -assert-count 0 top/w:q0 a:init %i +select -assert-count 0 top/w:qq0 a:init %i +select -assert-count 1 top/w:q1 a:init=1'b1 %i +select -assert-count 0 top/w:qx a:init %i + +design -load ref +hierarchy -auto-top +proc +simplemap +techmap -map %map_noremove +clean +# Make sure the parameter was used properly. +select -assert-count 3 top/t:ffbb +select -set ff0 top/w:q0 %ci t:ffbb %i +select -set ffq0 top/w:qq0 %ci t:ffbb %i +select -set ffx top/w:qx %ci t:ffbb %i +select -assert-count 1 @ff0 +select -assert-count 1 @ffq0 +select -assert-count 1 @ffx +select -assert-count 1 @ff0 r:INIT=1'b0 %i +select -assert-count 1 @ffq0 r:INIT=1'b0 %i +select -assert-count 1 @ffx r:INIT=1'bx %i +select -assert-count 0 top/w:q1 %ci t:ffbb %i +# Make sure the init values are not dropped from the wires. +select -assert-count 1 top/w:q0 a:init=1'b0 %i +select -assert-count 1 top/w:qq0 a:init=1'b0 %i +select -assert-count 1 top/w:q1 a:init=1'b1 %i +select -assert-count 0 top/w:qx a:init %i diff --git a/tests/various/abc9.v b/tests/various/abc9.v index a08b613a8..30ebd4e26 100644 --- a/tests/various/abc9.v +++ b/tests/various/abc9.v @@ -5,5 +5,7 @@ always @* endmodule module abc9_test028(input i, output o); -unknown u(~i, o); +wire w; +unknown u(~i, w); +unknown2 u2(w, o); endmodule diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys new file mode 100644 index 000000000..81e36d018 --- /dev/null +++ b/tests/various/equiv_opt_multiclock.ys @@ -0,0 +1,12 @@ +read_verilog <<EOT +module top(input clk, pre, d, output reg q); + always @(posedge clk, posedge pre) + if (pre) + q <= 1'b1; + else + q <= d; +endmodule +EOT + +prep +equiv_opt -assert -multiclock -map +/simcells.v synth diff --git a/tests/various/hierarchy_defer.ys b/tests/various/hierarchy_defer.ys new file mode 100644 index 000000000..70f5b70a3 --- /dev/null +++ b/tests/various/hierarchy_defer.ys @@ -0,0 +1,27 @@ +read -noverific +read -vlog2k <<EOT +module first; +endmodule + +(* top *) +module top(input i, output o); +sub s0(i, o); +endmodule + +(* constant_expression=1+1?2*2:3/3 *) +module sub(input i, output o); +assign o = ~i; +endmodule +EOT +design -save read + +hierarchy -auto-top +select -assert-any top +select -assert-any sub +select -assert-none foo + +design -load read +hierarchy +select -assert-any top +select -assert-any sub +select -assert-none foo diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys new file mode 100644 index 000000000..ee5ad8a1a --- /dev/null +++ b/tests/various/peepopt.ys @@ -0,0 +1,213 @@ +read_verilog <<EOT +module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); +assign o = i[s*W+:W]; +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$shiftx +select -assert-count 0 t:$shiftx t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w); +assign y = 1'b1 >> (w * (3'b110)); +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y); + assign Y = D >> (S*3); +endmodule +EOT + +prep +design -save gold +peepopt +design -stash gate + +design -import gold -as gold peepopt_shiftmul_2 +design -import gate -as gate peepopt_shiftmul_2 + +miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter +sat -show-public -enable_undef -prove-asserts miter +cd gate +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_muldiv_0(input [1:0] i, output [1:0] o); +wire [3:0] t; +assign t = i * 3; +assign o = t / 3; +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 0 t:* + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +select -assert-count 1 t:$dff r:WIDTH=4 %i +select -assert-count 1 t:$mux r:WIDTH=4 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +wreduce +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 2 t:$mux +select -assert-count 2 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +wreduce +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 2 t:$mux +select -assert-count 2 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + initial o <= 4'b0010; + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +# NB: equiv_opt uses equiv_induct which covers +# only the induction half of temporal induction +# --- missing the base-case half +# This makes it akin to `sat -tempinduct-inductonly` +# instead of `sat -tempinduct-baseonly` or +# `sat -tempinduct` which is necessary for this +# testcase +#equiv_opt -assert peepopt + +design -save gold +peepopt +wreduce +design -stash gate +design -import gold -as gold +design -import gate -as gate +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -tempinduct -verify -prove-asserts -show-ports miter + +design -load gate +select -assert-count 1 t:$dff r:WIDTH=4 %i +select -assert-count 2 t:$mux +select -assert-count 2 t:$mux r:WIDTH=4 %i +select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D |