diff options
Diffstat (limited to 'tests/arch')
106 files changed, 1927 insertions, 431 deletions
diff --git a/tests/arch/anlogic/blockram.ys b/tests/arch/anlogic/blockram.ys new file mode 100644 index 000000000..da23409ba --- /dev/null +++ b/tests/arch/anlogic/blockram.ys @@ -0,0 +1,13 @@ +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sp +proc +memory -nomap +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +memory +opt -full + +design -load postopt +cd sync_ram_sp + +select -assert-count 1 t:EG_PHY_BRAM +select -assert-none t:EG_PHY_BRAM %% t:* %D diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys index d3281ab89..deb90e051 100644 --- a/tests/arch/anlogic/dffs.ys +++ b/tests/arch/anlogic/dffs.ys @@ -15,6 +15,5 @@ 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 +select -assert-none t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/anlogic/latches.ys b/tests/arch/anlogic/latches.ys index 8d66f77b3..34a3b14d0 100644 --- a/tests/arch/anlogic/latches.ys +++ b/tests/arch/anlogic/latches.ys @@ -3,31 +3,33 @@ design -save read hierarchy -top latchp proc -# Can't run any sort of equivalence check because latches are blown to LUTs -synth_anlogic +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt 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 +select -assert-count 1 t:AL_MAP_SEQ +select -assert-count 1 t:AL_MAP_LUT1 +select -assert-none t:AL_MAP_SEQ t:AL_MAP_LUT1 %% 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 +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt 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 +select -assert-count 1 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ %% 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 +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt 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 +select -assert-count 1 t:AL_MAP_SEQ +select -assert-count 2 t:AL_MAP_LUT3 +select -assert-none t:AL_MAP_SEQ t:AL_MAP_LUT3 %% t:* %D diff --git a/tests/arch/anlogic/lutram.ys b/tests/arch/anlogic/lutram.ys index 9ebb75443..fe6135c73 100644 --- a/tests/arch/anlogic/lutram.ys +++ b/tests/arch/anlogic/lutram.ys @@ -2,7 +2,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r proc memory -nomap -equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic -nobram memory opt -full @@ -13,9 +13,8 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter design -load postopt cd lutram_1w1r -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 4 t:AL_MAP_LUT3 +select -assert-count 8 t:AL_MAP_LUT6 +select -assert-count 8 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 +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_LUT6 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D diff --git a/tests/arch/anlogic/run-test.sh b/tests/arch/anlogic/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/anlogic/run-test.sh +++ b/tests/arch/anlogic/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/common/adffs.v b/tests/arch/common/adffs.v index 576bd81a6..966e7c2b8 100644 --- a/tests/arch/common/adffs.v +++ b/tests/arch/common/adffs.v @@ -1,7 +1,9 @@ module adff( input d, clk, clr, output reg q ); +`ifndef NO_INIT initial begin q = 0; end +`endif always @( posedge clk, posedge clr ) if ( clr ) q <= 1'b0; @@ -10,9 +12,11 @@ module adff( input d, clk, clr, output reg q ); endmodule module adffn( input d, clk, clr, output reg q ); +`ifndef NO_INIT initial begin q = 0; end +`endif always @( posedge clk, negedge clr ) if ( !clr ) q <= 1'b0; @@ -21,9 +25,11 @@ module adffn( input d, clk, clr, output reg q ); endmodule module dffs( input d, clk, pre, clr, output reg q ); +`ifndef NO_INIT initial begin q = 0; end +`endif always @( posedge clk ) if ( pre ) q <= 1'b1; @@ -32,9 +38,11 @@ module dffs( input d, clk, pre, clr, output reg q ); endmodule module ndffnr( input d, clk, pre, clr, output reg q ); +`ifndef NO_INIT initial begin q = 0; end +`endif always @( negedge clk ) if ( !clr ) q <= 1'b0; diff --git a/tests/arch/common/counter.v b/tests/arch/common/counter.v index 9746fd701..1e0a13dc9 100644 --- a/tests/arch/common/counter.v +++ b/tests/arch/common/counter.v @@ -1,11 +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
+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 index 636252d16..0c607af50 100644 --- a/tests/arch/common/dffs.v +++ b/tests/arch/common/dffs.v @@ -4,9 +4,11 @@ module dff ( input d, clk, output reg q ); endmodule module dffe( input d, clk, en, output reg q ); +`ifndef NO_INIT initial begin q = 0; end +`endif always @( posedge clk ) if ( en ) q <= d; diff --git a/tests/arch/common/fsm.v b/tests/arch/common/fsm.v index 9d3fbb64a..cf1c21a58 100644 --- a/tests/arch/common/fsm.v +++ b/tests/arch/common/fsm.v @@ -1,51 +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
+ 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/mul.v b/tests/arch/common/mul.v index 437a91cfc..baed64fcd 100644 --- a/tests/arch/common/mul.v +++ b/tests/arch/common/mul.v @@ -1,9 +1,10 @@ module top +#(parameter X_WIDTH=6, Y_WIDTH=6, A_WIDTH=12) ( - input [5:0] x, - input [5:0] y, + input [X_WIDTH-1:0] x, + input [Y_WIDTH-1:0] y, - output [11:0] A, + output [A_WIDTH-1:0] A, ); assign A = x * y; endmodule diff --git a/tests/arch/common/shifter.v b/tests/arch/common/shifter.v index cace3b588..06e63c9af 100644 --- a/tests/arch/common/shifter.v +++ b/tests/arch/common/shifter.v @@ -1,11 +1,17 @@ -module top(out, clk, in);
- output [7:0] out;
- input signed clk, in;
- reg signed [7:0] out = 0;
-
- always @(posedge clk)
- begin
- out <= out >> 1;
- out[7] <= in;
- end
-endmodule
+module top(out, clk, in); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out; + +`ifndef NO_INIT + initial begin + out = 0; + end +`endif + + always @(posedge clk) + begin + out <= out >> 1; + out[7] <= in; + end +endmodule diff --git a/tests/arch/ecp5/bug2409.ys b/tests/arch/ecp5/bug2409.ys new file mode 100644 index 000000000..5ba9cec17 --- /dev/null +++ b/tests/arch/ecp5/bug2409.ys @@ -0,0 +1,24 @@ +read_verilog <<EOT +module t (...); + +input CLK; +input [10:0] A; +input WE; +input C; +input [7:0] DI; +output reg [7:0] DO; + +reg [7:0] mem[2047:0]; + +always @(posedge CLK) begin + if (C) + if (WE) + mem[A] <= DI; + DO <= mem[A]; +end + +endmodule +EOT + +synth_ecp5 +select -assert-count 1 t:DP16KD diff --git a/tests/arch/ecp5/bug2731.ys b/tests/arch/ecp5/bug2731.ys new file mode 100644 index 000000000..c609cea3b --- /dev/null +++ b/tests/arch/ecp5/bug2731.ys @@ -0,0 +1,7 @@ +read_verilog -icells <<EOF +module top(input c, r, input [1:0] d, output reg [1:0] q); +TRELLIS_FF #(.REGSET("SET")) ff1(.CLK(c), .LSR(r), .DI(d[0]), .Q(q[0])); +TRELLIS_FF #(.REGSET("SET")) ff2(.CLK(c), .LSR(r), .DI(d[1]), .Q(q[1])); +endmodule +EOF +synth_ecp5 -abc9 -dff diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys index ba91e5fc0..a77986bbc 100644 --- a/tests/arch/ecp5/fsm.ys +++ b/tests/arch/ecp5/fsm.ys @@ -10,8 +10,8 @@ sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 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 15 t:LUT4 -select -assert-count 6 t:PFUMX +select -assert-max 1 t:L6MUX21 +select -assert-max 16 t:LUT4 +select -assert-max 7 t:PFUMX select -assert-count 6 t:TRELLIS_FF select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/lutram.ys b/tests/arch/ecp5/lutram.ys index e1ae7abd5..9bef37c68 100644 --- a/tests/arch/ecp5/lutram.ys +++ b/tests/arch/ecp5/lutram.ys @@ -11,9 +11,9 @@ sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs mite design -load postopt cd lutram_1w1r -select -assert-count 24 t:L6MUX21 -select -assert-count 71 t:LUT4 -select -assert-count 32 t:PFUMX +select -assert-count 8 t:L6MUX21 +select -assert-count 36 t:LUT4 +select -assert-count 16 t:PFUMX select -assert-count 8 t:TRELLIS_DPR16X4 -select -assert-count 35 t:TRELLIS_FF +select -assert-count 8 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/memories.ys b/tests/arch/ecp5/memories.ys index f55bf01d2..44651ba25 100644 --- a/tests/arch/ecp5/memories.ys +++ b/tests/arch/ecp5/memories.ys @@ -1,328 +1,379 @@ # ================================ RAM ================================ # RAM bits <= 18K; Data width <= 36; Address width <= 9: -> PDPW16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:PDPW16KD ## With parameters -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:PDPW16KD # too inefficient select -assert-count 9 t:TRELLIS_DPR16X4 -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:PDPW16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "Block_RAM" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:PDPW16KD # any case works -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:PDPW16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "registers" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:PDPW16KD # requested FFRAM explicitly select -assert-count 180 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set logic_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:PDPW16KD # requested FFRAM explicitly select -assert-count 180 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_romstyle "ebr" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set rom_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ecp5 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled # RAM bits <= 18K; Data width <= 18; Address width <= 10: -> DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 9 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 12 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 13 -set DATA_WIDTH 2 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD ## With parameters -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:DP16KD # too inefficient select -assert-count 5 t:TRELLIS_DPR16X4 -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "Block_RAM" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD # any case works -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "registers" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:DP16KD # requested FFRAM explicitly select -assert-count 90 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set logic_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:DP16KD # requested FFRAM explicitly select -assert-count 90 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_romstyle "ebr" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set rom_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ecp5 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled # RAM bits <= 64; Data width <= 4; Address width <= 4: -> DPR16X4 -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:TRELLIS_DPR16X4 ## With parameters -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "distributed" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:TRELLIS_DPR16X4 -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "registers" m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:TRELLIS_DPR16X4 # requested FFRAM explicitly select -assert-count 68 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set logic_block 1 m:memory synth_ecp5 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:TRELLIS_DPR16X4 # requested FFRAM explicitly select -assert-count 68 t:TRELLIS_FF -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "distributed" m:memory synth_ecp5 -top sync_ram_sdp -nolutram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested LUTRAM but LUTRAM is disabled +select -assert-count 1 t:$mem_v2 # requested LUTRAM but LUTRAM is disabled # ================================ ROM ================================ # ROM bits <= 18K; Data width <= 36; Address width <= 9: -> PDPW16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:PDPW16KD ## With parameters -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:PDPW16KD # too inefficient select -assert-min 18 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "ebr" m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:PDPW16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:PDPW16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "logic" m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:PDPW16KD # requested LUTROM explicitly select -assert-min 18 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set logic_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:PDPW16KD # requested LUTROM explicitly select -assert-min 18 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set ram_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set syn_ramstyle "block_rom" m:memory synth_ecp5 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ecp5 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled # ROM bits <= 18K; Data width <= 18; Address width <= 10: -> DP16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:DP16KD ## With parameters -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:DP16KD # too inefficient select -assert-min 9 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "ebr" m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 1 t:DP16KD -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "logic" m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:DP16KD # requested LUTROM explicitly select -assert-min 9 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set logic_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom select -assert-count 0 t:DP16KD # requested LUTROM explicitly select -assert-min 9 t:LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set syn_ramstyle "block_ram" m:memory synth_ecp5 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set ram_block 1 m:memory synth_ecp5 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set syn_ramstyle "block_rom" m:memory synth_ecp5 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ecp5 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys index 92463aa32..db63dda5f 100644 --- a/tests/arch/ecp5/mux.ys +++ b/tests/arch/ecp5/mux.ys @@ -15,9 +15,9 @@ 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-max 1 t:L6MUX21 +select -assert-max 4 t:LUT4 +select -assert-max 2 t:PFUMX select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D @@ -27,9 +27,9 @@ 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-max 1 t:L6MUX21 +select -assert-max 7 t:LUT4 +select -assert-max 2 t:PFUMX select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D @@ -39,8 +39,8 @@ 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-max 12 t:L6MUX21 +select -assert-max 34 t:LUT4 +select -assert-max 17 t:PFUMX select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D diff --git a/tests/arch/ecp5/run-test.sh b/tests/arch/ecp5/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/ecp5/run-test.sh +++ b/tests/arch/ecp5/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/efinix/adffs.ys b/tests/arch/efinix/adffs.ys index 49dc7f256..86d446439 100644 --- a/tests/arch/efinix/adffs.ys +++ b/tests/arch/efinix/adffs.ys @@ -32,9 +32,8 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p 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 +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D design -load read @@ -45,6 +44,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p 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 +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys index af787ab67..f9111873c 100644 --- a/tests/arch/efinix/dffs.ys +++ b/tests/arch/efinix/dffs.ys @@ -19,6 +19,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p 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 +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D diff --git a/tests/arch/efinix/run-test.sh b/tests/arch/efinix/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/efinix/run-test.sh +++ b/tests/arch/efinix/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/gatemate/.gitignore b/tests/arch/gatemate/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/gatemate/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/gatemate/add_sub.ys b/tests/arch/gatemate/add_sub.ys new file mode 100644 index 000000000..bf261ba5a --- /dev/null +++ b/tests/arch/gatemate/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:CC_ADDF +select -assert-max 4 t:CC_LUT1 +select -assert-none t:CC_ADDF t:CC_LUT1 %% t:* %D diff --git a/tests/arch/gatemate/adffs.ys b/tests/arch/gatemate/adffs.ys new file mode 100644 index 000000000..b2ded6e9d --- /dev/null +++ b/tests/arch/gatemate/adffs.ys @@ -0,0 +1,43 @@ +read_verilog -D NO_INIT ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adff # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-none t:CC_BUFG t:CC_DFF %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-none t:CC_BUFG t:CC_DFF %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffs # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-max 1 t:CC_LUT2 +select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-max 1 t:CC_LUT2 +select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 %% t:* %D diff --git a/tests/arch/gatemate/counter.ys b/tests/arch/gatemate/counter.ys new file mode 100644 index 000000000..77ed858b3 --- /dev/null +++ b/tests/arch/gatemate/counter.ys @@ -0,0 +1,12 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 8 t:CC_ADDF +select -assert-count 1 t:CC_BUFG +select -assert-count 8 t:CC_DFF +select -assert-none t:CC_ADDF t:CC_BUFG t:CC_DFF %% t:* %D diff --git a/tests/arch/gatemate/dffs.ys b/tests/arch/gatemate/dffs.ys new file mode 100644 index 000000000..022322419 --- /dev/null +++ b/tests/arch/gatemate/dffs.ys @@ -0,0 +1,21 @@ +read_verilog -D NO_INIT ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dff # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-none t:CC_BUFG t:CC_DFF %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_DFF +select -assert-none t:CC_BUFG t:CC_DFF %% t:* %D diff --git a/tests/arch/gatemate/fsm.ys b/tests/arch/gatemate/fsm.ys new file mode 100644 index 000000000..6b43ead7a --- /dev/null +++ b/tests/arch/gatemate/fsm.ys @@ -0,0 +1,20 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/gatemate/cells_sim.v synth_gatemate -noiopad +async2sync +miter -equiv -make_assert -flatten gold gate miter +stat +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-count 1 t:CC_BUFG +select -assert-count 6 t:CC_DFF +select -assert-max 5 t:CC_LUT2 +select -assert-max 4 t:CC_LUT3 +select -assert-max 9 t:CC_LUT4 +select -assert-none t:CC_BUFG t:CC_DFF t:CC_LUT2 t:CC_LUT3 t:CC_LUT4 %% t:* %D diff --git a/tests/arch/gatemate/latches.ys b/tests/arch/gatemate/latches.ys new file mode 100644 index 000000000..5f64c6db5 --- /dev/null +++ b/tests/arch/gatemate/latches.ys @@ -0,0 +1,29 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # 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:CC_DLT +select -assert-none t:CC_DLT %% t:* %D + +design -load read +hierarchy -top latchn +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # 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:CC_DLT +select -assert-none t:CC_DLT %% t:* %D + +design -load read +hierarchy -top latchsr +proc +equiv_opt -async2sync -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # 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:CC_DLT +select -assert-max 2 t:CC_LUT3 +select -assert-none t:CC_DLT t:CC_LUT3 %% t:* %D diff --git a/tests/arch/gatemate/logic.ys b/tests/arch/gatemate/logic.ys new file mode 100644 index 000000000..026406bc8 --- /dev/null +++ b/tests/arch/gatemate/logic.ys @@ -0,0 +1,10 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-max 1 t:CC_LUT1 +select -assert-max 6 t:CC_LUT2 +select -assert-max 2 t:CC_LUT4 +select -assert-none t:CC_LUT1 t:CC_LUT2 t:CC_LUT4 %% t:* %D diff --git a/tests/arch/gatemate/memory.ys b/tests/arch/gatemate/memory.ys new file mode 100644 index 000000000..e919920f8 --- /dev/null +++ b/tests/arch/gatemate/memory.ys @@ -0,0 +1,34 @@ +# 512 x 40 bit -> CC_BRAM_20K SDP RAM +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 40 sync_ram_sdp +synth_gatemate -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_BRAM_20K + +# 512 x 80 bit -> CC_BRAM_40K SDP RAM +design -reset +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 80 sync_ram_sdp +synth_gatemate -top sync_ram_sdp -noiopad +cd sync_ram_sdp +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_BRAM_40K + +# 512 x 40 bit -> CC_BRAM_20K SDP ROM +design -reset +read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 40 sync_rom +synth_gatemate -top sync_rom -noiopad +cd sync_rom +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_BRAM_20K + +# 512 x 80 bit -> CC_BRAM_40K SDP ROM +design -reset +read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 80 sync_rom +synth_gatemate -top sync_rom -noiopad +cd sync_rom +select -assert-count 1 t:CC_BUFG +select -assert-count 1 t:CC_BRAM_40K diff --git a/tests/arch/gatemate/mul.v b/tests/arch/gatemate/mul.v new file mode 100644 index 000000000..55e8f9006 --- /dev/null +++ b/tests/arch/gatemate/mul.v @@ -0,0 +1,79 @@ + +module mul_plain(a, b, p); + + parameter M = 6; + parameter N = 6; + + input wire [M-1:0] a; + input wire [N-1:0] b; + output wire [M+N-1:0] p; + + assign p = a * b; + +endmodule + +module mul_signed_async (clk, rst, en, a, b, p); + + parameter M = 8; + parameter N = 6; + + input wire signed clk, rst, en; + input wire signed [M-1:0] a; + input wire signed [N-1:0] b; + output reg signed [M+N-1:0] p; + + reg signed [M-1:0] a_reg; + reg signed [N-1:0] b_reg; + + // signed M*N multiplier with + // - input and output pipeline registers + // - asynchronous reset (active high) + // - clock enable (active high) + always @(posedge clk or posedge rst) + begin + if (rst) begin + a_reg <= 0; + b_reg <= 0; + p <= 0; + end + else if (en) begin + a_reg <= a; + b_reg <= b; + p <= a_reg * b_reg; + end + end + +endmodule + +module mul_unsigned_sync (clk, rst, en, a, b, p); + + parameter M = 6; + parameter N = 3; + + input wire clk, rst, en; + input wire [M-1:0] a; + input wire [N-1:0] b; + output reg [M+N-1:0] p; + + reg [M-1:0] a_reg; + reg [N-1:0] b_reg; + + // unsigned M*N multiplier with + // - input and output pipeline registers + // - synchronous reset (active high) + // - clock enable (active high) + always @(posedge clk) + begin + if (rst) begin + a_reg <= 0; + b_reg <= 0; + p <= 0; + end + else if (en) begin + a_reg <= a; + b_reg <= b; + p <= a_reg * b_reg; + end + end + +endmodule diff --git a/tests/arch/gatemate/mul.ys b/tests/arch/gatemate/mul.ys new file mode 100644 index 000000000..ded5fe729 --- /dev/null +++ b/tests/arch/gatemate/mul.ys @@ -0,0 +1,33 @@ +read_verilog mul.v +design -save read + +hierarchy -top mul_plain +proc +equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_plain # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_MULT +select -assert-none t:CC_MULT %% t:* %D + +design -load read +hierarchy -top mul_signed_async +proc +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_signed_async # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_MULT +select -assert-count 1 t:CC_BUFG +select -assert-count 28 t:CC_DFF +select -assert-none t:CC_MULT t:CC_BUFG t:CC_DFF %% t:* %D + +design -load read +hierarchy -top mul_unsigned_sync +proc +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_unsigned_sync # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_MULT +select -assert-count 1 t:CC_BUFG +select -assert-max 18 t:CC_LUT4 +select -assert-count 18 t:CC_DFF +select -assert-none t:CC_MULT t:CC_BUFG t:CC_LUT4 t:CC_DFF %% t:* %D diff --git a/tests/arch/gatemate/mux.ys b/tests/arch/gatemate/mux.ys new file mode 100644 index 000000000..320ff33d7 --- /dev/null +++ b/tests/arch/gatemate/mux.ys @@ -0,0 +1,24 @@ +read_verilog ../common/mux.v +design -save read + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux4 # Constrain all select calls below inside the top module +select -assert-max 1 t:CC_LUT2 +select -assert-max 2 t:CC_LUT4 +select -assert-max 1 t:CC_MX2 +select -assert-none t:CC_LUT2 t:CC_LUT4 t:CC_MX2 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux8 # Constrain all select calls below inside the top module +select -assert-max 1 t:CC_LUT3 +select -assert-max 5 t:CC_LUT4 +select -assert-max 1 t:CC_MX2 +select -assert-none t:CC_LUT3 t:CC_LUT4 t:CC_MX2 %% t:* %D diff --git a/tests/arch/gatemate/run-test.sh b/tests/arch/gatemate/run-test.sh new file mode 100755 index 000000000..4be4b70ae --- /dev/null +++ b/tests/arch/gatemate/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/gatemate/shifter.ys b/tests/arch/gatemate/shifter.ys new file mode 100644 index 000000000..0006a298a --- /dev/null +++ b/tests/arch/gatemate/shifter.ys @@ -0,0 +1,10 @@ +read_verilog -D NO_INIT ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -async2sync -map +/gatemate/cells_sim.v synth_gatemate -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:CC_BUFG +select -assert-count 8 t:CC_DFF +select -assert-none t:CC_BUFG t:CC_DFF %% t:* %D diff --git a/tests/arch/gatemate/tribuf.ys b/tests/arch/gatemate/tribuf.ys new file mode 100644 index 000000000..d900fa5e4 --- /dev/null +++ b/tests/arch/gatemate/tribuf.ys @@ -0,0 +1,13 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/gatemate/cells_sim.v -map +/simcells.v synth_gatemate # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 2 t:CC_IBUF +select -assert-max 1 t:CC_LUT1 +select -assert-count 1 t:CC_TOBUF +select -assert-none t:CC_IBUF t:CC_LUT1 t:CC_TOBUF %% t:* %D diff --git a/tests/arch/gowin/init-error.ys b/tests/arch/gowin/init-error.ys new file mode 100644 index 000000000..de3813d6f --- /dev/null +++ b/tests/arch/gowin/init-error.ys @@ -0,0 +1,5 @@ +read_verilog init.v +chparam -set INIT 0 myDFF*P* +hierarchy -top myDFFP +logger -expect error "unsupported initial value and async reset value combination" 1 +synth_gowin diff --git a/tests/arch/gowin/init.ys b/tests/arch/gowin/init.ys index ddc0e4757..fba7c2fa5 100644 --- a/tests/arch/gowin/init.ys +++ b/tests/arch/gowin/init.ys @@ -30,45 +30,40 @@ select -assert-count 1 t:DFFRE select -assert-count 1 t:DFFS select -assert-count 1 t:DFFSE -delete design -load read # these should synth to a flop with reset chparam -set INIT 1 myDFF myDFFN myDFFE myDFFNE -# async should give a warning +# async would give an error # sync should synth to a mux -chparam -set INIT 0 myDFF*S* myDFF*P* -chparam -set INIT 1 myDFF*R* myDFF*C* +chparam -set INIT 0 myDFF*S* +chparam -set INIT 1 myDFF*R* proc flatten synth_gowin -run coarse: # check the flops mapped as expected -select -assert-count 1 t:DFF +select -assert-count 2 t:DFF select -assert-count 1 t:DFFC select -assert-count 1 t:DFFCE -select -assert-count 1 t:DFFE -select -assert-count 1 t:DFFN +select -assert-count 0 t:DFFE +select -assert-count 2 t:DFFN select -assert-count 1 t:DFFNC select -assert-count 1 t:DFFNCE -select -assert-count 1 t:DFFNE +select -assert-count 0 t:DFFNE select -assert-count 1 t:DFFNP select -assert-count 1 t:DFFNPE select -assert-count 0 t:DFFNR select -assert-count 0 t:DFFNRE -select -assert-count 2 t:DFFNS -select -assert-count 2 t:DFFNSE +select -assert-count 3 t:DFFNS +select -assert-count 1 t:DFFNSE select -assert-count 1 t:DFFP select -assert-count 1 t:DFFPE select -assert-count 0 t:DFFR select -assert-count 0 t:DFFRE -select -assert-count 2 t:DFFS -select -assert-count 2 t:DFFSE -select -assert-count 12 t:LUT2 - -# check the expected leftover init values -# this would happen if your reset value is not the initial value -# which would be weird -select -assert-count 8 a:init +select -assert-count 3 t:DFFS +select -assert-count 1 t:DFFSE +select -assert-count 4 t:LUT2 +select -assert-count 4 t:LUT4 diff --git a/tests/arch/gowin/lutram.ys b/tests/arch/gowin/lutram.ys index 56f69e7c5..d668783a2 100644 --- a/tests/arch/gowin/lutram.ys +++ b/tests/arch/gowin/lutram.ys @@ -7,12 +7,11 @@ 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 -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 lutram_1w1r -select -assert-count 8 t:RAM16S4 +select -assert-count 8 t:RAM16SDP4 # other logic present that is not simple #select -assert-none t:RAM16S4 %% t:* %D diff --git a/tests/arch/gowin/run-test.sh b/tests/arch/gowin/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/gowin/run-test.sh +++ b/tests/arch/gowin/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/gowin/tribuf.ys b/tests/arch/gowin/tribuf.ys index 5855b9d97..eef7e379f 100644 --- a/tests/arch/gowin/tribuf.ys +++ b/tests/arch/gowin/tribuf.ys @@ -9,5 +9,6 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p 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-count 1 t:LUT1 select -assert-count 2 t:IBUF -select -assert-none t:TBUF t:IBUF %% t:* %D +select -assert-none t:TBUF t:IBUF t:LUT1 %% t:* %D
\ No newline at end of file diff --git a/tests/arch/ice40/bug2061.ys b/tests/arch/ice40/bug2061.ys new file mode 100644 index 000000000..7dd7ee6a3 --- /dev/null +++ b/tests/arch/ice40/bug2061.ys @@ -0,0 +1,24 @@ +read_verilog <<EOT +module top #( + parameter integer WIDTH = 12 +)( + output reg [WIDTH:0] cnt, + input wire clk, + input wire rst +); + wire last_n; + + assign last_n = cnt[WIDTH]; + + always @(posedge clk or posedge rst) + if (rst) + cnt <= 0; + else + cnt <= last_n ? ( cnt + { (WIDTH+1){last_n} } ) : 13'h1aaa; + +endmodule +EOT + +synth_ice40 +splitnets +select -assert-count 12 t:SB_CARRY %co:+[CO] t:SB_LUT4 %ci:+[I3] %i diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index 223ba070e..e3b746202 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module select -assert-count 4 t:SB_DFF select -assert-count 2 t:SB_DFFESR -select -assert-count 15 t:SB_LUT4 +select -assert-max 15 t:SB_LUT4 select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/memories.ys b/tests/arch/ice40/memories.ys index c32f12315..4920a45e3 100644 --- a/tests/arch/ice40/memories.ys +++ b/tests/arch/ice40/memories.ys @@ -1,167 +1,194 @@ # ================================ RAM ================================ # RAM bits <= 4K; Data width <= 16; Address width <= 11: -> SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 2 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 4 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 16 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K ## With parameters -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:SB_RAM40_4K # too inefficient select -assert-min 1 t:SB_DFFE -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "Block_RAM" m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K # any case works -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "registers" m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:SB_RAM40_4K # requested FFRAM explicitly select -assert-min 1 t:SB_DFFE -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set logic_block 1 m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp select -assert-count 0 t:SB_RAM40_4K # requested FFRAM explicitly select -assert-min 1 t:SB_DFFE -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_romstyle "ebr" m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set rom_block 1 m:memory synth_ice40 -top sync_ram_sdp; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BROM but this is a RAM +select -assert-count 1 t:$mem_v2 # requested BROM but this is a RAM -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set syn_ramstyle "block_ram" m:memory synth_ice40 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled -design -reset; read_verilog ../common/blockram.v +design -reset; read_verilog -defer ../common/blockram.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_ram_sdp +hierarchy -top sync_ram_sdp setattr -set ram_block 1 m:memory synth_ice40 -top sync_ram_sdp -nobram; cd sync_ram_sdp -select -assert-count 1 t:$mem # requested BRAM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BRAM but BRAM is disabled # ================================ ROM ================================ # ROM bits <= 4K; Data width <= 16; Address width <= 11: -> SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 2 sync_rom +hierarchy -top sync_rom synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 4 sync_rom +hierarchy -top sync_rom synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 16 sync_rom +hierarchy -top sync_rom synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K ## With parameters -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom synth_ice40 -top sync_rom; cd sync_rom select -assert-count 0 t:SB_RAM40_4K # too inefficient select -assert-min 1 t:SB_LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "ebr" m:memory synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ice40 -top sync_rom; cd sync_rom select -assert-count 1 t:SB_RAM40_4K -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "logic" m:memory synth_ice40 -top sync_rom; cd sync_rom select -assert-count 0 t:SB_RAM40_4K # requested LUTROM explicitly select -assert-min 1 t:SB_LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set logic_block 1 m:memory synth_ice40 -top sync_rom; cd sync_rom select -assert-count 0 t:SB_RAM40_4K # requested LUTROM explicitly select -assert-min 1 t:SB_LUT4 -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set syn_ramstyle "block_ram" m:memory synth_ice40 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set ram_block 1 m:memory synth_ice40 -top sync_rom; cd sync_rom -select -assert-count 1 t:$mem # requested BRAM but this is a ROM +select -assert-count 1 t:$mem_v2 # requested BRAM but this is a ROM -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set syn_romstyle "ebr" m:memory synth_ice40 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled -design -reset; read_verilog ../common/blockrom.v +design -reset; read_verilog -defer ../common/blockrom.v chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +hierarchy -top sync_rom setattr -set rom_block 1 m:memory synth_ice40 -top sync_rom -nobram; cd sync_rom -select -assert-count 1 t:$mem # requested BROM but BRAM is disabled +select -assert-count 1 t:$mem_v2 # requested BROM but BRAM is disabled diff --git a/tests/arch/ice40/run-test.sh b/tests/arch/ice40/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/ice40/run-test.sh +++ b/tests/arch/ice40/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/intel_alm/add_sub.ys b/tests/arch/intel_alm/add_sub.ys index 4cb2c2e0d..8f87adf27 100644 --- a/tests/arch/intel_alm/add_sub.ys +++ b/tests/arch/intel_alm/add_sub.ys @@ -1,8 +1,18 @@ read_verilog ../common/add_sub.v hierarchy -top top -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module stat -select -assert-count 8 t:MISTRAL_ALUT_ARITH +select -assert-count 9 t:MISTRAL_ALUT_ARITH +select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D + +design -reset +read_verilog ../common/add_sub.v +hierarchy -top top +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 9 t:MISTRAL_ALUT_ARITH select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys index 5d8d3a220..d7487c40b 100644 --- a/tests/arch/intel_alm/adffs.ys +++ b/tests/arch/intel_alm/adffs.ys @@ -3,7 +3,19 @@ design -save read hierarchy -top adff proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF +select -assert-count 1 t:MISTRAL_NOT + +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D + + +design -load read +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF @@ -15,7 +27,18 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D design -load read hierarchy -top adffn proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF @@ -26,7 +49,19 @@ select -assert-none t:MISTRAL_FF %% t:* %D design -load read hierarchy -top dffs proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF +select -assert-count 1 t:MISTRAL_ALUT2 + +select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF @@ -38,11 +73,22 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D design -load read hierarchy -top ndffnr proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF -select -assert-count 1 t:MISTRAL_NOT -select -assert-count 1 t:MISTRAL_ALUT2 +select -assert-count 2 t:MISTRAL_NOT -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF +select -assert-count 2 t:MISTRAL_NOT + +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys new file mode 100644 index 000000000..c157c3165 --- /dev/null +++ b/tests/arch/intel_alm/blockram.ys @@ -0,0 +1,6 @@ +read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp +synth_intel_alm -family cyclonev -noiopad -noclkbuf +cd sync_ram_sdp +select -assert-count 1 t:MISTRAL_M10K +select -assert-none t:MISTRAL_M10K %% t:* %D diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 945c318d8..56c9cabb3 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -2,12 +2,26 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 2 t:MISTRAL_NOT +select -assert-count 1 t:MISTRAL_NOT select -assert-count 8 t:MISTRAL_ALUT_ARITH select -assert-count 8 t:MISTRAL_FF +select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D + +design -reset +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_NOT +select -assert-count 8 t:MISTRAL_ALUT_ARITH +select -assert-count 8 t:MISTRAL_FF select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/dffs.ys b/tests/arch/intel_alm/dffs.ys index 149b3121a..34b99f04c 100644 --- a/tests/arch/intel_alm/dffs.ys +++ b/tests/arch/intel_alm/dffs.ys @@ -3,7 +3,7 @@ design -save read hierarchy -top dff proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF @@ -11,9 +11,31 @@ select -assert-count 1 t:MISTRAL_FF select -assert-none t:MISTRAL_FF %% t:* %D design -load read +hierarchy -top dff +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read +hierarchy -top dffe +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read hierarchy -top dffe proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys index 67965569b..0aeea450a 100644 --- a/tests/arch/intel_alm/fsm.ys +++ b/tests/arch/intel_alm/fsm.ys @@ -3,7 +3,7 @@ hierarchy -top fsm proc flatten -equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf async2sync miter -equiv -make_assert -flatten gold gate miter sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter @@ -12,8 +12,33 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd fsm # Constrain all select calls below inside the top module select -assert-count 6 t:MISTRAL_FF +select -assert-max 1 t:MISTRAL_NOT select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 -select -assert-count 1 t:MISTRAL_ALUT3 -select -assert-count 5 t:MISTRAL_ALUT5 -select -assert-count 2 t:MISTRAL_ALUT6 -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D +select -assert-max 1 t:MISTRAL_ALUT3 +select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 +select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 +select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D + +design -reset +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf +async2sync +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-count 6 t:MISTRAL_FF +select -assert-max 1 t:MISTRAL_NOT +select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 +select -assert-max 2 t:MISTRAL_ALUT3 # Clang returns 2, GCC returns 1 +select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 +select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 +select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 +select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/logic.ys b/tests/arch/intel_alm/logic.ys index fad45db74..d34d1bc65 100644 --- a/tests/arch/intel_alm/logic.ys +++ b/tests/arch/intel_alm/logic.ys @@ -1,7 +1,7 @@ read_verilog ../common/logic.v hierarchy -top top proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 @@ -9,3 +9,17 @@ select -assert-count 1 t:MISTRAL_NOT select -assert-count 6 t:MISTRAL_ALUT2 select -assert-count 2 t:MISTRAL_ALUT4 select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D + + +design -reset +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_NOT +select -assert-count 6 t:MISTRAL_ALUT2 +select -assert-count 2 t:MISTRAL_ALUT4 +select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D
\ No newline at end of file diff --git a/tests/arch/intel_alm/lutram.ys b/tests/arch/intel_alm/lutram.ys index 6f997b67b..9ddb1ec87 100644 --- a/tests/arch/intel_alm/lutram.ys +++ b/tests/arch/intel_alm/lutram.ys @@ -2,19 +2,38 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r proc memory -nomap -equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad -noclkbuf 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 +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter design -load postopt cd lutram_1w1r select -assert-count 16 t:MISTRAL_MLAB -select -assert-count 1 t:MISTRAL_NOT select -assert-count 2 t:MISTRAL_ALUT2 select -assert-count 8 t:MISTRAL_ALUT3 -select -assert-count 17 t:MISTRAL_FF -select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D +select -assert-count 8 t:MISTRAL_FF +select -assert-none t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r +proc +memory -nomap +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram -noiopad -noclkbuf +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 16 t:MISTRAL_MLAB +select -assert-count 2 t:MISTRAL_ALUT2 +select -assert-count 8 t:MISTRAL_ALUT3 +select -assert-count 8 t:MISTRAL_FF +select -assert-none t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D diff --git a/tests/arch/intel_alm/mul.ys b/tests/arch/intel_alm/mul.ys new file mode 100644 index 000000000..e147d93ac --- /dev/null +++ b/tests/arch/intel_alm/mul.ys @@ -0,0 +1,60 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_MUL9X9 +select -assert-none t:MISTRAL_MUL9X9 %% t:* %D + +# Cyclone 10 GX does not have 9x9 multipliers. + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_MUL18X18 +select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_MUL18X18 +select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys index 308e45268..6fb6ae80a 100644 --- a/tests/arch/intel_alm/mux.ys +++ b/tests/arch/intel_alm/mux.ys @@ -1,41 +1,84 @@ read_verilog ../common/mux.v design -save read + hierarchy -top mux2 proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_ALUT3 +select -assert-none t:MISTRAL_ALUT3 %% t:* %D + +design -load read +hierarchy -top mux2 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_ALUT3 select -assert-none t:MISTRAL_ALUT3 %% t:* %D + design -load read hierarchy -top mux4 proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT6 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT6 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_ALUT3 +select -assert-count 2 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D + + design -load read hierarchy -top mux8 proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_ALUT3 -select -assert-count 1 t:MISTRAL_ALUT5 select -assert-count 2 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 1 t:MISTRAL_ALUT3 +select -assert-max 2 t:MISTRAL_ALUT5 +select -assert-max 5 t:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D + design -load read hierarchy -top mux16 proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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 1 t:MISTRAL_ALUT3 diff --git a/tests/arch/intel_alm/quartus_ice.ys b/tests/arch/intel_alm/quartus_ice.ys index 4b9b54d10..4e1896b82 100644 --- a/tests/arch/intel_alm/quartus_ice.ys +++ b/tests/arch/intel_alm/quartus_ice.ys @@ -10,3 +10,17 @@ EOT synth_intel_alm -family cyclonev -quartus select -assert-none w:*[* w:*]* + +design -reset +read_verilog <<EOT +// Verilog has syntax for raw identifiers, where you start it with \ and end it with a space. +// This test crashes Quartus due to it parsing \a[10] as a wire slice and not a raw identifier. +module top(); + (* keep *) wire [31:0] \a[10] ; + (* keep *) wire b; + assign b = \a[10] [31]; +endmodule +EOT + +synth_intel_alm -family cyclone10gx -quartus -noiopad -noclkbuf +select -assert-none w:*[* w:*]* diff --git a/tests/arch/intel_alm/run-test.sh b/tests/arch/intel_alm/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/intel_alm/run-test.sh +++ b/tests/arch/intel_alm/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/intel_alm/shifter.ys b/tests/arch/intel_alm/shifter.ys index 014dbd1a8..77ff98896 100644 --- a/tests/arch/intel_alm/shifter.ys +++ b/tests/arch/intel_alm/shifter.ys @@ -2,9 +2,20 @@ read_verilog ../common/shifter.v hierarchy -top top proc flatten -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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:MISTRAL_FF +select -assert-none t:MISTRAL_FF %% t:* %D + +design -reset +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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:MISTRAL_FF select -assert-none t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/tribuf.ys b/tests/arch/intel_alm/tribuf.ys index 71b05a747..fb5fecb78 100644 --- a/tests/arch/intel_alm/tribuf.ys +++ b/tests/arch/intel_alm/tribuf.ys @@ -4,10 +4,24 @@ proc tribuf flatten synth -equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev # equivalency check +equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # 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 + +design -reset +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # 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/machxo2/.gitignore b/tests/arch/machxo2/.gitignore new file mode 100644 index 000000000..1d329c933 --- /dev/null +++ b/tests/arch/machxo2/.gitignore @@ -0,0 +1,2 @@ +*.log +/run-test.mk diff --git a/tests/arch/machxo2/add_sub.ys b/tests/arch/machxo2/add_sub.ys new file mode 100644 index 000000000..d9497b818 --- /dev/null +++ b/tests/arch/machxo2/add_sub.ys @@ -0,0 +1,8 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/dffs.ys b/tests/arch/machxo2/dffs.ys new file mode 100644 index 000000000..83a79a9d6 --- /dev/null +++ b/tests/arch/machxo2/dffs.ys @@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:FACADE_FF +select -assert-none t:FACADE_FF t:FACADE_IO %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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 2 t:FACADE_FF t:LUT4 +select -assert-none t:FACADE_FF t:LUT4 t:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/fsm.ys b/tests/arch/machxo2/fsm.ys new file mode 100644 index 000000000..847a61161 --- /dev/null +++ b/tests/arch/machxo2/fsm.ys @@ -0,0 +1,15 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/machxo2/cells_sim.v synth_machxo2 +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-max 16 t:LUT4 +select -assert-count 6 t:FACADE_FF +select -assert-none t:FACADE_FF t:LUT4 t:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/logic.ys b/tests/arch/machxo2/logic.ys new file mode 100644 index 000000000..bf93ab128 --- /dev/null +++ b/tests/arch/machxo2/logic.ys @@ -0,0 +1,8 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/mux.ys b/tests/arch/machxo2/mux.ys new file mode 100644 index 000000000..7b7e62d4c --- /dev/null +++ b/tests/arch/machxo2/mux.ys @@ -0,0 +1,40 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:FACADE_IO %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:LUT4 + +select -assert-none t:LUT4 t:FACADE_IO %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:LUT4 + +select -assert-none t:LUT4 t:FACADE_IO %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux16 # Constrain all select calls below inside the top module +select -assert-max 12 t:LUT4 + +select -assert-none t:LUT4 t:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/run-test.sh b/tests/arch/machxo2/run-test.sh new file mode 100644 index 000000000..4be4b70ae --- /dev/null +++ b/tests/arch/machxo2/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/machxo2/shifter.ys b/tests/arch/machxo2/shifter.ys new file mode 100644 index 000000000..87fdab0fa --- /dev/null +++ b/tests/arch/machxo2/shifter.ys @@ -0,0 +1,10 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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:FACADE_FF +select -assert-none t:FACADE_FF t:FACADE_IO %% t:* %D diff --git a/tests/arch/machxo2/tribuf.ys b/tests/arch/machxo2/tribuf.ys new file mode 100644 index 000000000..fce342e18 --- /dev/null +++ b/tests/arch/machxo2/tribuf.ys @@ -0,0 +1,10 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +flatten +equiv_opt -assert -map +/machxo2/cells_sim.v synth_machxo2 # 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 3 t:FACADE_IO +select -assert-count 1 t:LUT4 +select -assert-none t:FACADE_IO t:LUT4 %% t:* %D diff --git a/tests/arch/nexus/.gitignore b/tests/arch/nexus/.gitignore new file mode 100644 index 000000000..ba42e1ee6 --- /dev/null +++ b/tests/arch/nexus/.gitignore @@ -0,0 +1,2 @@ +/*.log +/run-test.mk diff --git a/tests/arch/nexus/add_sub.ys b/tests/arch/nexus/add_sub.ys new file mode 100644 index 000000000..4317bab81 --- /dev/null +++ b/tests/arch/nexus/add_sub.ys @@ -0,0 +1,21 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +design -save orig + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 10 t:LUT4 +select -assert-none t:IB t:OB t:VLO t:LUT4 %% t:* %D + +design -load orig + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus -abc9 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 6 t:LUT4 +select -assert-count 4 t:WIDEFN9 +select -assert-none t:IB t:OB t:VLO t:LUT4 t:WIDEFN9 %% t:* %D diff --git a/tests/arch/nexus/adffs.ys b/tests/arch/nexus/adffs.ys new file mode 100644 index 000000000..f8796425c --- /dev/null +++ b/tests/arch/nexus/adffs.ys @@ -0,0 +1,44 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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 +stat +select -assert-count 1 t:FD1P3DX +select -assert-none t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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 +stat +select -assert-count 1 t:FD1P3DX +select -assert-count 1 t:INV +select -assert-none t:FD1P3DX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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 +stat +select -assert-count 1 t:FD1P3IX +select -assert-count 1 t:LUT4 +select -assert-none t:FD1P3IX t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # 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 +stat +select -assert-count 1 t:FD1P3IX +select -assert-count 2 t:INV +select -assert-none t:FD1P3IX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/blockram.ys b/tests/arch/nexus/blockram.ys new file mode 100644 index 000000000..9540136d5 --- /dev/null +++ b/tests/arch/nexus/blockram.ys @@ -0,0 +1,18 @@ +read_verilog ../common/blockram.v +design -save read + +# Check that we use the right dual and single clock variants + +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp +synth_nexus -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:PDPSC16K +select -assert-none t:PDPSC16K t:INV t:IB t:OB t:VLO t:VHI %% t:* %D + +design -reset +read_verilog blockram_dc.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp_dc +synth_nexus -top sync_ram_sdp_dc +cd sync_ram_sdp_dc +select -assert-count 1 t:PDP16K +select -assert-none t:PDP16K t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/blockram_dc.v b/tests/arch/nexus/blockram_dc.v new file mode 100644 index 000000000..4f5d4f5a6 --- /dev/null +++ b/tests/arch/nexus/blockram_dc.v @@ -0,0 +1,25 @@ + +`default_nettype none +module sync_ram_sdp_dc #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire clkw, clkr, write_enable, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in_r, address_in_w, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clkw) begin + if (write_enable) + memory[address_in_w] <= data_in; + end + always @(posedge clkr) begin + data_out_r <= memory[address_in_r]; + end + + assign data_out = data_out_r; + +endmodule // sync_ram_sdp_dc diff --git a/tests/arch/nexus/counter.ys b/tests/arch/nexus/counter.ys new file mode 100644 index 000000000..44421e377 --- /dev/null +++ b/tests/arch/nexus/counter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -multiclock -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 5 t:CCU2 +select -assert-count 8 t:FD1P3DX +select -assert-none t:CCU2 t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/dffs.ys b/tests/arch/nexus/dffs.ys new file mode 100644 index 000000000..9ebf68bf4 --- /dev/null +++ b/tests/arch/nexus/dffs.ys @@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX +select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX +select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D diff --git a/tests/arch/nexus/fsm.ys b/tests/arch/nexus/fsm.ys new file mode 100644 index 000000000..24ad8fe5b --- /dev/null +++ b/tests/arch/nexus/fsm.ys @@ -0,0 +1,19 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +stat + +select -assert-max 1 t:INV +select -assert-max 2 t:LUT4 +select -assert-max 6 t:WIDEFN9 +select -assert-count 6 t:FD1P3IX +select -assert-none t:LUT4 t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/logic.ys b/tests/arch/nexus/logic.ys new file mode 100644 index 000000000..cff61b509 --- /dev/null +++ b/tests/arch/nexus/logic.ys @@ -0,0 +1,8 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:LUT4 +select -assert-none t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/lutram.ys b/tests/arch/nexus/lutram.ys new file mode 100644 index 000000000..6e33431b6 --- /dev/null +++ b/tests/arch/nexus/lutram.ys @@ -0,0 +1,19 @@ +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r +proc +memory -nomap +equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus +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 lutram_1w1r +stat +select -assert-count 8 t:WIDEFN9 +select -assert-count 12 t:LUT4 +select -assert-count 8 t:DPR16X4 +select -assert-count 8 t:FD1P3IX +select -assert-none t:DPR16X4 t:FD1P3IX t:WIDEFN9 t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/mul.ys b/tests/arch/nexus/mul.ys new file mode 100644 index 000000000..65a2fd8c3 --- /dev/null +++ b/tests/arch/nexus/mul.ys @@ -0,0 +1,50 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc + +design -save read + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus +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:MULT9X9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT9X9 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT18X18 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X36 +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT18X36 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT36X36 %% t:* %D diff --git a/tests/arch/nexus/mux.ys b/tests/arch/nexus/mux.ys new file mode 100644 index 000000000..0e12d674a --- /dev/null +++ b/tests/arch/nexus/mux.ys @@ -0,0 +1,43 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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 4 t:LUT4 +select -assert-count 1 t:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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-min 11 t:LUT4 +select -assert-max 12 t:LUT4 +select -assert-count 1 t:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D diff --git a/tests/arch/nexus/run-test.sh b/tests/arch/nexus/run-test.sh new file mode 100644 index 000000000..4be4b70ae --- /dev/null +++ b/tests/arch/nexus/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/nexus/shifter.ys b/tests/arch/nexus/shifter.ys new file mode 100644 index 000000000..a8e34b0f9 --- /dev/null +++ b/tests/arch/nexus/shifter.ys @@ -0,0 +1,9 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX +select -assert-none t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/tribuf.ys b/tests/arch/nexus/tribuf.ys new file mode 100644 index 000000000..70fb7cb5f --- /dev/null +++ b/tests/arch/nexus/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/nexus/cells_sim.v -map +/simcells.v synth_nexus # 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:OBZ +select -assert-count 1 t:INV +select -assert-none t:OBZ t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/quicklogic/.gitignore b/tests/arch/quicklogic/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/quicklogic/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/quicklogic/add_sub.ys b/tests/arch/quicklogic/add_sub.ys new file mode 100644 index 000000000..73ee5cb44 --- /dev/null +++ b/tests/arch/quicklogic/add_sub.ys @@ -0,0 +1,11 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +equiv_opt -assert -map +/quicklogic/lut_sim.v -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 # 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 2 t:LUT2 +select -assert-count 8 t:LUT3 +select -assert-count 2 t:LUT4 +select -assert-count 8 t:inpad +select -assert-count 8 t:outpad +select -assert-none t:LUT2 t:LUT3 t:LUT4 t:inpad t:outpad %% t:* %D diff --git a/tests/arch/quicklogic/adffs.ys b/tests/arch/quicklogic/adffs.ys new file mode 100644 index 000000000..41a175844 --- /dev/null +++ b/tests/arch/quicklogic/adffs.ys @@ -0,0 +1,67 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # 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:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 1 t:inpad +select -assert-count 1 t:outpad +select -assert-count 2 t:ckpad + +select -assert-none t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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:LUT1 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT1 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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:LUT2 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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:LUT1 +select -assert-count 1 t:LUT2 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 4 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT1 t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad %% t:* %D diff --git a/tests/arch/quicklogic/counter.ys b/tests/arch/quicklogic/counter.ys new file mode 100644 index 000000000..2e266417c --- /dev/null +++ b/tests/arch/quicklogic/counter.ys @@ -0,0 +1,18 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -multiclock -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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 3 t:LUT2 +select -assert-count 5 t:LUT3 +select -assert-count 1 t:LUT4 +select -assert-count 8 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 8 t:outpad +select -assert-count 2 t:ckpad + +select -assert-none t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:dffepc t:logic_0 t:logic_1 t:outpad t:ckpad %% t:* %D diff --git a/tests/arch/quicklogic/dffs.ys b/tests/arch/quicklogic/dffs.ys new file mode 100644 index 000000000..2e0a34540 --- /dev/null +++ b/tests/arch/quicklogic/dffs.ys @@ -0,0 +1,20 @@ +read_verilog ../common/dffs.v +rename dff my_dff # Work around conflicting module names between test and vendor cells +rename dffe my_dffe +design -save read + +hierarchy -top my_dff +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # 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-none t:* + +design -load read +hierarchy -top my_dffe +proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v synth_quicklogic # 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-none t:*
\ No newline at end of file diff --git a/tests/arch/quicklogic/fsm.ys b/tests/arch/quicklogic/fsm.ys new file mode 100644 index 000000000..130dacf42 --- /dev/null +++ b/tests/arch/quicklogic/fsm.ys @@ -0,0 +1,23 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic +async2sync +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd fsm # Constrain all select calls below inside the top module + +select -assert-count 1 t:LUT2 +select -assert-count 9 t:LUT3 +select -assert-count 4 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 3 t:inpad +select -assert-count 2 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT2 t:LUT3 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D diff --git a/tests/arch/quicklogic/latches.ys b/tests/arch/quicklogic/latches.ys new file mode 100644 index 000000000..bcef42990 --- /dev/null +++ b/tests/arch/quicklogic/latches.ys @@ -0,0 +1,40 @@ +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_quicklogic +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT3 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_quicklogic +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT3 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_quicklogic +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT2 +select -assert-count 1 t:LUT4 +select -assert-count 5 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT2 t:LUT4 t:inpad t:outpad %% t:* %D diff --git a/tests/arch/quicklogic/logic.ys b/tests/arch/quicklogic/logic.ys new file mode 100644 index 000000000..4b327c00a --- /dev/null +++ b/tests/arch/quicklogic/logic.ys @@ -0,0 +1,14 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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:LUT3 +select -assert-count 8 t:inpad +select -assert-count 10 t:outpad + +select -assert-none t:LUT1 t:LUT2 t:LUT3 t:inpad t:outpad %% t:* %D diff --git a/tests/arch/quicklogic/mux.ys b/tests/arch/quicklogic/mux.ys new file mode 100644 index 000000000..ea17fa99b --- /dev/null +++ b/tests/arch/quicklogic/mux.ys @@ -0,0 +1,52 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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 3 t:LUT3 +select -assert-count 6 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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:LUT1 +select -assert-count 1 t:LUT3 +select -assert-count 2 t:mux4x0 +select -assert-count 11 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT1 t:LUT3 t:mux4x0 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/quicklogic/lut_sim.v synth_quicklogic # 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 1 t:LUT3 +select -assert-count 2 t:mux8x0 +select -assert-count 20 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:mux8x0 t:inpad t:outpad %% t:* %D diff --git a/tests/arch/quicklogic/run-test.sh b/tests/arch/quicklogic/run-test.sh new file mode 100755 index 000000000..4be4b70ae --- /dev/null +++ b/tests/arch/quicklogic/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/quicklogic/tribuf.ys b/tests/arch/quicklogic/tribuf.ys new file mode 100644 index 000000000..de763009e --- /dev/null +++ b/tests/arch/quicklogic/tribuf.ys @@ -0,0 +1,13 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/quicklogic/cells_sim.v -map +/simcells.v synth_quicklogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:$_TBUF_ +select -assert-none t:inpad t:outpad t:$_TBUF_ %% t:* %D diff --git a/tests/arch/run-test.sh b/tests/arch/run-test.sh index 170078a7f..5d923db56 100755 --- a/tests/arch/run-test.sh +++ b/tests/arch/run-test.sh @@ -11,7 +11,7 @@ for arch in ../../techlibs/*; do if [ "${defines[$arch_name]}" ]; then for def in ${defines[$arch_name]}; do echo -n "Test $path -D$def ->" - iverilog -t null -I$arch -D$def $path + iverilog -t null -I$arch -D$def -DNO_ICE40_DEFAULT_ASSIGNMENTS $path echo " ok" done else diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys index 210e87477..0ba3901f7 100644 --- a/tests/arch/xilinx/abc9_dff.ys +++ b/tests/arch/xilinx/abc9_dff.ys @@ -50,10 +50,10 @@ FDCE_1 /*#(.INIT(1))*/ fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); FDPE_1 #(.INIT(1)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); endmodule EOT -logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 -logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 -logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 8 t:FD* diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys index 7bdd94a63..58552d8fb 100644 --- a/tests/arch/xilinx/attributes_test.ys +++ b/tests/arch/xilinx/attributes_test.ys @@ -16,8 +16,7 @@ select -assert-count 8 t:RAM32X1D # Set ram_style distributed to blockram memory; will be implemented as distributed design -reset read_verilog ../common/memory_attributes/attributes_test.v -prep -setattr -mod -set ram_style "distributed" block_ram +setattr -set ram_style "distributed" block_ram/m:* synth_xilinx -top block_ram -noiopad cd block_ram # Constrain all select calls below inside the top module select -assert-count 32 t:RAM128X1D @@ -25,8 +24,7 @@ select -assert-count 32 t:RAM128X1D # Set synthesis, logic_block to blockram memory; will be implemented as distributed design -reset read_verilog ../common/memory_attributes/attributes_test.v -prep -setattr -mod -set logic_block 1 block_ram +setattr -set logic_block 1 block_ram/m:* synth_xilinx -top block_ram -noiopad cd block_ram # Constrain all select calls below inside the top module select -assert-count 0 t:RAMB18E1 diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys new file mode 100644 index 000000000..909e54149 --- /dev/null +++ b/tests/arch/xilinx/dsp_abc9.ys @@ -0,0 +1,37 @@ +read_verilog <<EOT +module top(input [24:0] A, input [17:0] B, output [47:0] P); +DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P)); +endmodule +EOT +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt +scc -expect 0 + + +design -reset +read_verilog <<EOT +module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P); +assign P = A * B; +endmodule +EOT +synth_xilinx -abc9 +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt -full -fine +select -assert-count 1 t:$mul +select -assert-count 0 t:* t:$mul %D + + +design -reset +read_verilog -icells -formal <<EOT +module top(output [42:0] P); +\$__MUL25X18 mul (.A(42), .B(42), .Y(P)); +assert property (P == 42*42); +endmodule +EOT +techmap -map +/xilinx/xc7_dsp_map.v +verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1 +synth_xilinx -abc9 +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt -full -fine +select -assert-count 0 t:* t:$assert %d +sat -verify -prove-asserts diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys index fec4c6082..3b1919627 100644 --- a/tests/arch/xilinx/fsm.ys +++ b/tests/arch/xilinx/fsm.ys @@ -13,12 +13,11 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd fsm # Constrain all select calls below inside the top module stat select -assert-count 1 t:BUFG -select -assert-count 4 t:FDRE -select -assert-count 1 t:FDSE -select -assert-count 1 t:LUT2 -select -assert-count 3 t:LUT5 +select -assert-count 6 t:FDRE +select -assert-count 1 t:LUT4 +select -assert-count 4 t:LUT5 select -assert-count 1 t:LUT6 -select -assert-none t:BUFG t:FDRE t:FDSE t:LUT2 t:LUT5 t:LUT6 %% t:* %D +select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D design -load orig @@ -32,7 +31,7 @@ stat select -assert-count 1 t:BUFG select -assert-count 6 t:FDRE select -assert-count 1 t:LUT1 -select -assert-count 3 t:LUT3 -select -assert-count 6 t:LUT4 -select -assert-count 6 t:MUXF5 +select -assert-max 1 t:LUT3 +select -assert-max 8 t:LUT4 +select -assert-count 5 t:MUXF5 select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT3 t:LUT4 t:MUXF5 %% t:* %D diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys index e226c2ec8..ee87fee21 100644 --- a/tests/arch/xilinx/latches.ys +++ b/tests/arch/xilinx/latches.ys @@ -18,9 +18,8 @@ equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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:INV -select -assert-none t:LDCE t:INV %% t:* %D +select -assert-none t:LDCE %% t:* %D design -load read diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys index 1b2788448..c2a23de6d 100644 --- a/tests/arch/xilinx/mux.ys +++ b/tests/arch/xilinx/mux.ys @@ -40,10 +40,11 @@ proc equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux16 # Constrain all select calls below inside the top module +select -assert-max 2 t:LUT3 select -assert-max 2 t:LUT4 select -assert-min 4 t:LUT6 select -assert-max 7 t:LUT6 select -assert-max 2 t:MUXF7 dump -select -assert-none t:LUT6 t:LUT4 t:MUXF7 %% t:* %D +select -assert-none t:LUT6 t:LUT4 t:LUT3 t:MUXF7 %% t:* %D diff --git a/tests/arch/xilinx/nosrl.ys b/tests/arch/xilinx/nosrl.ys new file mode 100644 index 000000000..31bd5d377 --- /dev/null +++ b/tests/arch/xilinx/nosrl.ys @@ -0,0 +1,41 @@ +read_verilog <<EOT + +module xilinx_srl_static_test(input i, clk, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[3], shift1[3]}; +endmodule + +EOT + +design -save read + +hierarchy -top xilinx_srl_static_test +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +equiv_opt -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd xilinx_srl_static_test # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 1 t:SRL16E +select -assert-none t:BUFG t:SRL16E %% t:* %D + +design -load read +hierarchy -top xilinx_srl_static_test +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nosrl -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd xilinx_srl_static_test # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 5 t:FDRE +select -assert-none t:BUFG t:FDRE %% t:* %D diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys index e76fb20ab..9a5e70ea9 100644 --- a/tests/arch/xilinx/pmgen_xilinx_srl.ys +++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys @@ -35,7 +35,6 @@ design -stash gate design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed -dff2dffe -unmap # sat does not support flops-with-enable yet miter -equiv -flatten -make_assert gold gate miter sat -set-init-zero -seq 5 -verify -prove-asserts miter @@ -52,6 +51,5 @@ design -stash gate design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable -dff2dffe -unmap # sat does not support flops-with-enable yet miter -equiv -flatten -make_assert gold gate miter sat -set-init-zero -seq 5 -verify -prove-asserts miter diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/xilinx/run-test.sh +++ b/tests/arch/xilinx/run-test.sh @@ -1,20 +1,4 @@ #!/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 +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/xilinx/tribuf.sh b/tests/arch/xilinx/tribuf.sh index bd44395cb..eca33e490 100644 --- a/tests/arch/xilinx/tribuf.sh +++ b/tests/arch/xilinx/tribuf.sh @@ -1,5 +1,5 @@ -! ../../../yosys -qp "synth_xilinx" ../common/tribuf.v -../../../yosys -qp "synth_xilinx -iopad; \ +../../../yosys -f verilog -qp "synth_xilinx" ../common/tribuf.v +../../../yosys -f verilog -qp "synth_xilinx -iopad; \ select -assert-count 2 t:IBUF; \ select -assert-count 1 t:INV; \ select -assert-count 1 t:OBUFT" ../common/tribuf.v diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index 2c729832e..c09699411 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -223,3 +223,49 @@ select -assert-count 1 t:LUT2 select -assert-none t:FDRSE t:LUT4 t:LUT2 %% t:* %D design -reset + + +read_verilog << EOT + +// FDSE_1, mergeable CE and S, but CE only not worth it. + +module t0 (...); +input wire clk; +input wire [7:0] i; +output wire [7:0] o; + +wire [7:0] tmp ; + +LUT2 #(.INIT(4'h6)) lut0 (.I0(i[0]), .I1(i[1]), .O(tmp[0])); +LUT2 #(.INIT(4'h6)) lut1 (.I0(i[1]), .I1(i[2]), .O(tmp[1])); + +FDSE_1 ff (.D(tmp[0]), .CE(i[7]), .S(tmp[1]), .Q(o[0])); + +endmodule + +EOT + +read_verilog -lib +/xilinx/cells_sim.v +design -save t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt +design -load postopt +clean + +cd t0 +select -assert-count 1 t:FDSE_1 +select -assert-count 1 t:LUT5 +select -assert-none t:FDSE_1 t:LUT5 %% t:* %D + +design -load t0 + +equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt -lut4 +design -load postopt +clean + +cd t0 +select -assert-count 1 t:FDSE_1 +select -assert-count 2 t:LUT2 +select -assert-none t:FDSE_1 t:LUT2 %% t:* %D + +design -reset |