diff options
Diffstat (limited to 'tests')
33 files changed, 1291 insertions, 46 deletions
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys index 0bcc4e011..eb94177ad 100644 --- a/tests/arch/anlogic/fsm.ys +++ b/tests/arch/anlogic/fsm.ys @@ -10,9 +10,6 @@ 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:AL_MAP_LUT2 -select -assert-count 5 t:AL_MAP_LUT5 -select -assert-count 1 t:AL_MAP_LUT6 select -assert-count 6 t:AL_MAP_SEQ -select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT5 t:AL_MAP_LUT6 t:AL_MAP_SEQ %% t:* %D +select -assert-none t:AL_MAP_LUT* t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/common/blockram.v b/tests/arch/common/blockram.v index dbc6ca65c..5ed0736d0 100644 --- a/tests/arch/common/blockram.v +++ b/tests/arch/common/blockram.v @@ -5,19 +5,20 @@ module sync_ram_sp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) input wire [ADDRESS_WIDTH-1:0] address_in, output wire [DATA_WIDTH-1:0] data_out); - localparam WORD = (DATA_WIDTH-1); - localparam DEPTH = (2**ADDRESS_WIDTH-1); + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); - reg [WORD:0] data_out_r; - reg [WORD:0] memory [0:DEPTH]; + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; - always @(posedge clk) begin - if (write_enable) - memory[address_in] <= data_in; - data_out_r <= memory[address_in]; - end + always @(posedge clk) begin + if (write_enable) + memory[address_in] <= data_in; + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; - assign data_out = data_out_r; endmodule // sync_ram_sp @@ -28,18 +29,19 @@ module sync_ram_sdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) 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); + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; - reg [WORD:0] data_out_r; - reg [WORD:0] memory [0:DEPTH]; + always @(posedge clk) begin + if (write_enable) + memory[address_in_w] <= data_in; + data_out_r <= memory[address_in_r]; + end - always @(posedge clk) begin - if (write_enable) - memory[address_in_w] <= data_in; - data_out_r <= memory[address_in_r]; - end + assign data_out = data_out_r; - assign data_out = data_out_r; endmodule // sync_ram_sdp diff --git a/tests/arch/common/blockrom.v b/tests/arch/common/blockrom.v new file mode 100644 index 000000000..93f5c9ddf --- /dev/null +++ b/tests/arch/common/blockrom.v @@ -0,0 +1,31 @@ +`default_nettype none +module sync_rom #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire clk, + input wire [ADDRESS_WIDTH-1:0] address_in, + 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]; + + integer i,j = 64'hF4B1CA8127865242; + initial + for (i = 0; i <= DEPTH; i++) begin + // In case this ROM will be implemented in fabric: fill the memory with some data + // uncorrelated with the address, or Yosys might see through the ruse and e.g. not + // emit any LUTs at all for `memory[i] = i;`, just a latch. + memory[i] = j * 64'h2545F4914F6CDD1D; + j = j ^ (j >> 12); + j = j ^ (j << 25); + j = j ^ (j >> 27); + end + + always @(posedge clk) begin + data_out_r <= memory[address_in]; + end + + assign data_out = data_out_r; + +endmodule // sync_rom diff --git a/tests/arch/ecp5/memories.ys b/tests/arch/ecp5/memories.ys new file mode 100644 index 000000000..e1f748e26 --- /dev/null +++ b/tests/arch/ecp5/memories.ys @@ -0,0 +1,330 @@ +# ================================ RAM ================================ +# RAM bits <= 18K; Data width <= 36; Address width <= 9: -> PDPW16KD + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +# RAM bits <= 18K; Data width <= 18; Address width <= 10: -> DP16KD + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 9 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 +chparam -set ADDRESS_WIDTH 12 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 13 -set DATA_WIDTH 2 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 +chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +# RAM bits <= 64; Data width <= 4; Address width <= 4: -> DPR16X4 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 4 -set DATA_WIDTH 4 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 + +# ================================ ROM ================================ +# ROM bits <= 18K; Data width <= 36; Address width <= 9: -> PDPW16KD + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 sync_rom +write_ilang +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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 36 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 36 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 + +# ROM bits <= 18K; Data width <= 18; Address width <= 10: -> DP16KD + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 sync_rom +write_ilang +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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 3 -set DATA_WIDTH 18 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 18 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 diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys index a2db2ad98..aef720d46 100644 --- a/tests/arch/efinix/fsm.ys +++ b/tests/arch/efinix/fsm.ys @@ -10,7 +10,6 @@ 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:EFX_GBUFCE -select -assert-count 6 t:EFX_FF -select -assert-count 15 t:EFX_LUT4 +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 6 t:EFX_FF select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/ice40/lutram.ys b/tests/arch/ice40/lutram.ys deleted file mode 100644 index 1ba40f8ec..000000000 --- a/tests/arch/ice40/lutram.ys +++ /dev/null @@ -1,15 +0,0 @@ -read_verilog ../common/lutram.v -hierarchy -top lutram_1w1r -proc -memory -nomap -equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -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 -select -assert-count 1 t:SB_RAM40_4K -select -assert-none t:SB_RAM40_4K %% t:* %D diff --git a/tests/arch/ice40/memories.ys b/tests/arch/ice40/memories.ys new file mode 100644 index 000000000..571edec1d --- /dev/null +++ b/tests/arch/ice40/memories.ys @@ -0,0 +1,168 @@ +# ================================ RAM ================================ +# RAM bits <= 4K; Data width <= 16; Address width <= 11: -> SB_RAM40_4K + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 2 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 +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 16 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockram.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +# ================================ ROM ================================ +# ROM bits <= 4K; Data width <= 16; Address width <= 11: -> SB_RAM40_4K + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 11 -set DATA_WIDTH 2 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 +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 4 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 +chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 16 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 sync_rom +write_ilang +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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 + +design -reset; read_verilog ../common/blockrom.v +chparam -set ADDRESS_WIDTH 2 -set DATA_WIDTH 8 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 diff --git a/tests/arch/intel_alm/add_sub.ys b/tests/arch/intel_alm/add_sub.ys new file mode 100644 index 000000000..4cb2c2e0d --- /dev/null +++ b/tests/arch/intel_alm/add_sub.ys @@ -0,0 +1,8 @@ +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 +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-none t:MISTRAL_ALUT_ARITH %% t:* %D diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys new file mode 100644 index 000000000..5d8d3a220 --- /dev/null +++ b/tests/arch/intel_alm/adffs.ys @@ -0,0 +1,48 @@ +read_verilog ../common/adffs.v +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 +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 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 +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 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 +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 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 +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-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys new file mode 100644 index 000000000..945c318d8 --- /dev/null +++ b/tests/arch/intel_alm/counter.ys @@ -0,0 +1,13 @@ +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 +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 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 new file mode 100644 index 000000000..cf29ad8e0 --- /dev/null +++ b/tests/arch/intel_alm/dffs.ys @@ -0,0 +1,22 @@ +read_verilog ../common/dffs.v +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 +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 # 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-count 1 t:MISTRAL_ALUT3 + +select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT3 %% t:* %D diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys new file mode 100644 index 000000000..8bb0ebab2 --- /dev/null +++ b/tests/arch/intel_alm/fsm.ys @@ -0,0 +1,18 @@ +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 cyclonev +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 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 +select -assert-count 5 t:MISTRAL_ALUT5 +select -assert-count 1 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/logic.ys b/tests/arch/intel_alm/logic.ys new file mode 100644 index 000000000..fad45db74 --- /dev/null +++ b/tests/arch/intel_alm/logic.ys @@ -0,0 +1,11 @@ +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 +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 diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys new file mode 100644 index 000000000..308e45268 --- /dev/null +++ b/tests/arch/intel_alm/mux.ys @@ -0,0 +1,45 @@ +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 +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 +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 # 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_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 +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-count 2 t:MISTRAL_ALUT5 +select -assert-count 4 t:MISTRAL_ALUT6 + +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/run-test.sh b/tests/arch/intel_alm/run-test.sh new file mode 100755 index 000000000..bf19b887d --- /dev/null +++ b/tests/arch/intel_alm/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/intel_alm/shifter.ys b/tests/arch/intel_alm/shifter.ys new file mode 100644 index 000000000..014dbd1a8 --- /dev/null +++ b/tests/arch/intel_alm/shifter.ys @@ -0,0 +1,10 @@ +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 +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 new file mode 100644 index 000000000..71b05a747 --- /dev/null +++ b/tests/arch/intel_alm/tribuf.ys @@ -0,0 +1,13 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclonev # 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/opt/opt_expr.ys b/tests/opt/opt_expr.ys index e0acead82..7c446afd1 100644 --- a/tests/opt/opt_expr.ys +++ b/tests/opt/opt_expr.ys @@ -291,3 +291,31 @@ check equiv_opt -assert opt_expr -keepdc design -load postopt select -assert-count 1 t:$shift r:A_WIDTH=13 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_mul_low_bits(input [2:0] a, input [2:0] b, output [7:0] y); + \$mul #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(4), .Y_WIDTH(8)) mul (.A({a, 1'b0}), .B({b, 1'b0}), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr +design -load postopt +select -assert-count 1 t:$mul r:A_WIDTH=3 %i r:B_WIDTH=3 %i r:Y_WIDTH=6 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_mul_low_bits(input [2:0] a, input [2:0] b, output [7:0] y); + \$mul #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(4), .Y_WIDTH(8)) mul (.A({a, 1'b0}), .B({b, 1'b0}), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr -keepdc +design -load postopt +select -assert-count 1 t:$mul r:A_WIDTH=4 %i r:B_WIDTH=4 %i r:Y_WIDTH=8 %i diff --git a/tests/opt/opt_expr_alu.ys b/tests/opt/opt_expr_alu.ys new file mode 100644 index 000000000..e288bcea6 --- /dev/null +++ b/tests/opt/opt_expr_alu.ys @@ -0,0 +1,111 @@ +read_verilog <<EOT +module test(input a, output [1:0] y); +assign y = {a,1'b0} + 1'b1; +endmodule +EOT + +alumacc +equiv_opt -assert opt_expr -fine +design -load postopt +select -assert-count 1 t:$pos +select -assert-count none t:$pos t:* %D + + +design -reset +read_verilog <<EOT +module test(input a, output [1:0] y); +assign y = {a,1'b1} + 1'b1; +endmodule +EOT + +alumacc +select -assert-count 1 t:$alu +select -assert-count none t:$alu t:* %D + + +design -reset +read_verilog <<EOT +module test(input a, output [1:0] y); +assign y = {a,1'b1} - 1'b1; +endmodule +EOT + +equiv_opt -assert opt_expr -fine +design -load postopt +select -assert-count 1 t:$pos +select -assert-count none t:$pos t:* %D + + +design -reset +read_verilog <<EOT +module test(input a, output [3:0] y); +assign y = {a,3'b101} - 1'b1; +endmodule +EOT + +equiv_opt -assert opt_expr -fine +design -load postopt +select -assert-count 1 t:$pos +select -assert-count none t:$pos t:* %D + + +design -reset +read_verilog <<EOT +module test(input a, output [3:0] y); +assign y = {a,3'b101} - 1'b1; +endmodule +EOT + +alumacc +equiv_opt -assert opt_expr -fine +design -load postopt +select -assert-count 1 t:$pos +select -assert-count none t:$pos t:* %D + + +design -reset +read_verilog <<EOT +module test(input [1:0] a, output [3:0] y); +assign y = -{a[1], 2'b10, a[0]}; +endmodule +EOT + +alumacc +equiv_opt -assert opt -fine +design -load postopt +select -assert-count 1 t:$alu +select -assert-count 1 t:$alu r:Y_WIDTH=3 %i +select -assert-count 1 t:$not +select -assert-count none t:$alu t:$not t:* %D %D + + +design -reset +read_verilog <<EOT +module test(input [3:0] a, input [2:0] b, output [5:0] y); +assign y = {a[3:2], 1'b1, a[1:0]} + {b[2], 2'b11, b[1:0]}; +endmodule +EOT + +alumacc +equiv_opt -assert opt -fine +design -load postopt +dump +select -assert-count 2 t:$alu +select -assert-count 1 t:$alu r:Y_WIDTH=2 %i +select -assert-count 1 t:$alu r:Y_WIDTH=3 %i +select -assert-count none t:$alu t:* %D + + +design -reset +read_verilog <<EOT +module test(input [3:0] a, input [3:0] b, output [5:0] y); +assign y = {a[3:2], 1'b0, a[1:0]} + {b[3:2], 1'b0, b[1:0]}; +endmodule +EOT + +alumacc +equiv_opt -assert opt -fine +design -load postopt +select -assert-count 2 t:$alu +select -assert-count 2 t:$alu r:Y_WIDTH=3 %i +select -assert-count none t:$alu t:* %D diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys new file mode 100644 index 000000000..21439fd53 --- /dev/null +++ b/tests/opt/opt_expr_xor.ys @@ -0,0 +1,52 @@ +read_verilog <<EOT +module top(input a, output [3:0] y); +assign y[0] = a^1'b0; +assign y[1] = 1'b1^a; +assign y[2] = a~^1'b0; +assign y[3] = 1'b1^~a; +endmodule +EOT +design -save read +select -assert-count 2 t:$xor +select -assert-count 2 t:$xnor + +equiv_opt opt_expr +design -load postopt +select -assert-none t:$xor +select -assert-none t:$xnor +select -assert-count 2 t:$not + + +design -load read +simplemap +equiv_opt opt_expr +design -load postopt +select -assert-none t:$_XOR_ +select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ +select -assert-count 3 t:$_NOT_ + + +design -reset +read_verilog -icells <<EOT +module top(input a, output [1:0] y); +$_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0])); +$_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1])); +endmodule +EOT +select -assert-count 2 t:$_XNOR_ +equiv_opt opt_expr +design -load postopt +select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ +select -assert-count 1 t:$_NOT_ + + +design -reset +read_verilog <<EOT +module top(input a, output [1:0] w, x, y, z); +assign w = a^1'b0; +assign x = a^1'b1; +assign y = a~^1'b0; +assign z = a~^1'b1; +endmodule +EOT +equiv_opt opt_expr diff --git a/tests/opt/opt_merge_init.ys b/tests/opt/opt_merge_init.ys index a29c29df6..0176f09c7 100644 --- a/tests/opt/opt_merge_init.ys +++ b/tests/opt/opt_merge_init.ys @@ -20,6 +20,7 @@ endmodule EOT opt_merge +select -assert-count 1 t:$dff select -assert-count 1 a:init=1'0 @@ -46,4 +47,31 @@ endmodule EOT opt_merge +select -assert-count 1 t:$dff select -assert-count 1 a:init=2'bx1 + + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, (* init = 1'b0 *) output o, /* NB: no init here! */ output p); + \$dff #( + .CLK_POLARITY(1'h1), + .WIDTH(32'd1) + ) ffo ( + .CLK(clk), + .D(i), + .Q(o) + ); + \$dff #( + .CLK_POLARITY(1'h1), + .WIDTH(32'd1) + ) ffp ( + .CLK(clk), + .D(i), + .Q(p) + ); +endmodule +EOT + +opt_merge +select -assert-count 2 t:$dff diff --git a/tests/opt/opt_merge_keep.ys b/tests/opt/opt_merge_keep.ys new file mode 100644 index 000000000..2a9202901 --- /dev/null +++ b/tests/opt/opt_merge_keep.ys @@ -0,0 +1,64 @@ +read_verilog -icells <<EOT +module top(input clk, i, output o, p); + (* keep *) + \$_DFF_P_ ffo ( + .C(clk), + .D(i), + .Q(o) + ); + \$_DFF_P_ ffp ( + .C(clk), + .D(i), + .Q(p) + ); +endmodule +EOT + +opt_merge +select -assert-count 1 t:$_DFF_P_ +select -assert-count 1 a:keep + + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, output o, p); + \$_DFF_P_ ffo ( + .C(clk), + .D(i), + .Q(o) + ); + (* keep *) + \$_DFF_P_ ffp ( + .C(clk), + .D(i), + .Q(p) + ); +endmodule +EOT + +opt_merge +select -assert-count 1 t:$_DFF_P_ +select -assert-count 1 a:keep + + +design -reset +read_verilog -icells <<EOT +module top(input clk, i, output o, p); + (* keep *) + \$_DFF_P_ ffo ( + .C(clk), + .D(i), + .Q(o) + ); + (* keep *) + \$_DFF_P_ ffp ( + .C(clk), + .D(i), + .Q(p) + ); +endmodule +EOT + +opt_merge +select -assert-count 2 t:$_DFF_P_ +select -assert-count 2 a:keep diff --git a/tests/select/.gitignore b/tests/select/.gitignore new file mode 100644 index 000000000..50e13221d --- /dev/null +++ b/tests/select/.gitignore @@ -0,0 +1 @@ +/*.log diff --git a/tests/simple/dynslice.v b/tests/simple/dynslice.v new file mode 100644 index 000000000..7236ac3a5 --- /dev/null +++ b/tests/simple/dynslice.v @@ -0,0 +1,12 @@ +module dynslice ( + input clk , + input [9:0] ctrl , + input [15:0] din , + input [3:0] sel , + output reg [127:0] dout +); +always @(posedge clk) +begin + dout[ctrl*sel+:16] <= din ; +end +endmodule diff --git a/tests/svtypes/typedef_package.sv b/tests/svtypes/typedef_package.sv index 57a78c53a..2d83742c5 100644 --- a/tests/svtypes/typedef_package.sv +++ b/tests/svtypes/typedef_package.sv @@ -1,6 +1,9 @@ package pkg; typedef logic [7:0] uint8_t; - typedef enum logic [7:0] {bb=8'hBB} enum8_t; + typedef enum logic [7:0] {bb=8'hBB, cc=8'hCC} enum8_t; + + localparam uint8_t PCONST = cc; + parameter uint8_t PCONST_COPY = PCONST; endpackage module top; @@ -8,7 +11,9 @@ module top; (* keep *) pkg::uint8_t a = 8'hAA; (* keep *) pkg::enum8_t b_enum = pkg::bb; - always @* assert(a == 8'hAA); - always @* assert(b_enum == 8'hBB); + always_comb assert(a == 8'hAA); + always_comb assert(b_enum == 8'hBB); + always_comb assert(pkg::PCONST == pkg::cc); + always_comb assert(pkg::PCONST_COPY == pkg::cc); endmodule diff --git a/tests/techmap/cmp2lcu.ys b/tests/techmap/cmp2lcu.ys new file mode 100644 index 000000000..7c8a63692 --- /dev/null +++ b/tests/techmap/cmp2lcu.ys @@ -0,0 +1,52 @@ +read_verilog <<EOT +module top(input [12:0] a, b, output gtu, gts, ltu, lts, geu, ges, leu, les); +assign gtu = a > b; +assign gts = $signed(a) > $signed(b); +assign ltu = a < b; +assign lts = $signed(a) < $signed(b); +assign geu = a >= b; +assign ges = $signed(a) >= $signed(b); +assign leu = a <= b; +assign les = $signed(a) <= $signed(b); +endmodule +EOT + +equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=6 +design -load postopt +select -assert-count 8 t:$lcu r:WIDTH=5 %i +select -assert-none t:$gt t:$ge t:$lt t:$le + +design -load preopt +equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=4 +design -load postopt +select -assert-count 8 t:$lcu r:WIDTH=7 %i +select -assert-none t:$gt t:$ge t:$lt t:$le + + +design -reset +read_verilog <<EOT +module top(input [8:0] a, b, output gtu, gts, ltu, lts, geu, ges, leu, les); +wire [13:0] c = {a[8:6], 3'b101, a[5:4], 2'b11, a[3:0]}; +wire [13:0] d = {b[8], 3'b101, b[7:4], 2'b01, b[3:0]}; +assign gtu = c > d; +assign gts = $signed(c) > $signed(d); +assign ltu = c < d; +assign lts = $signed(c) < $signed(d); +assign geu = c >= d; +assign ges = $signed(c) >= $signed(d); +assign leu = c <= d; +assign les = $signed(c) <= $signed(d); +endmodule +EOT +design -save gold + +equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=5 +design -load postopt +select -assert-count 8 t:$lcu r:WIDTH=2 %i +select -assert-none t:$gt t:$ge t:$lt t:$le + +design -load preopt +equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=3 +design -load postopt +select -assert-count 8 t:$lcu r:WIDTH=4 %i +select -assert-none t:$gt t:$ge t:$lt t:$le diff --git a/tests/techmap/dffinit.ys b/tests/techmap/dffinit.ys new file mode 100644 index 000000000..218d411f8 --- /dev/null +++ b/tests/techmap/dffinit.ys @@ -0,0 +1,25 @@ +read_verilog <<EOT + +module ff(...); +input d; +output q; + +endmodule + +module top(...); +input d; +output q1; +(* init = 1'b1 *) +output q2; + +ff my_ff1(.d(d), .q(q1)); +ff my_ff2(.d(d), .q(q2)); + +endmodule + +EOT + +dffinit -ff ff q init +select -assert-count 2 t:ff +select -assert-count 1 t:ff r:init %i +select -assert-count 1 t:ff r:init=1'b1 %i diff --git a/tests/techmap/iopadmap.ys b/tests/techmap/iopadmap.ys index 25ea94dfc..df029b3a0 100644 --- a/tests/techmap/iopadmap.ys +++ b/tests/techmap/iopadmap.ys @@ -55,13 +55,19 @@ obuf b (.i(i), .o(tmp)); assign o = tmp; endmodule +module k(inout o, o2); +assign o = 1'bz; +endmodule + EOT opt_clean tribuf simplemap -iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io a b c d e f g h i j +iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io a b c d e f g h i j k opt_clean +hierarchy -check +check select -assert-count 1 a/t:ibuf select -assert-count 1 a/t:obuf @@ -140,6 +146,8 @@ select -assert-count 0 i/t:obuf select -assert-count 1 j/t:ibuf select -assert-count 1 j/t:obuf +select -assert-count 2 k/t:iobuf + # Check that \init attributes get moved from output buffer # to buffer input diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys new file mode 100644 index 000000000..18b17621f --- /dev/null +++ b/tests/techmap/zinit.ys @@ -0,0 +1,57 @@ +read_verilog -icells <<EOT +module top(input C, R, input [1:0] D, (* init = {2'b10, 2'b01, 1'b1, {8{1'b1}}} *) output [12:0] Q); + +(* init = 1'b1 *) +wire unused; + +$_DFF_NN0_ dff0 (.C(C), .D(D[0]), .R(R), .Q(Q[0])); +$_DFF_NN1_ dff1 (.C(C), .D(D[0]), .R(R), .Q(Q[1])); +$_DFF_NP0_ dff2 (.C(C), .D(D[0]), .R(R), .Q(Q[2])); +$_DFF_NP1_ dff3 (.C(C), .D(D[0]), .R(R), .Q(Q[3])); +$_DFF_PN0_ dff4 (.C(C), .D(D[0]), .R(R), .Q(Q[4])); +$_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); +$_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); +$_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); + +$adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); +$adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); +endmodule +EOT +equiv_opt -assert -map +/simcells.v -multiclock zinit +design -load postopt + +select -assert-count 20 t:$_NOT_ +select -assert-count 1 w:unused a:init %i +select -assert-count 1 w:Q a:init=13'bxxxx1xxxxxxxx %i +select -assert-count 4 c:dff0 c:dff2 c:dff4 c:dff6 %% t:$_DFF_??1_ %i +select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$_DFF_??0_ %i + + +design -reset +read_verilog -icells <<EOT +module top(input C, R, input [1:0] D, (* init = {2'bx0, 2'b0x, 1'b1, {8{1'b0}}} *) output [12:0] Q); + +(* init = 1'b1 *) +wire unused; + +$_DFF_NN0_ dff0 (.C(C), .D(D[0]), .R(R), .Q(Q[0])); +$_DFF_NN1_ dff1 (.C(C), .D(D[0]), .R(R), .Q(Q[1])); +$_DFF_NP0_ dff2 (.C(C), .D(D[0]), .R(R), .Q(Q[2])); +$_DFF_NP1_ dff3 (.C(C), .D(D[0]), .R(R), .Q(Q[3])); +$_DFF_PN0_ dff4 (.C(C), .D(D[0]), .R(R), .Q(Q[4])); +$_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); +$_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); +$_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); + +$adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); +$adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); +endmodule +EOT +equiv_opt -assert -map +/simcells.v -multiclock zinit +design -load postopt + +select -assert-count 0 t:$_NOT_ +select -assert-count 1 w:unused a:init %i +select -assert-count 1 w:Q a:init=13'bxxxx1xxxxxxxx %i +select -assert-count 4 c:dff0 c:dff2 c:dff4 c:dff6 %% t:$_DFF_??0_ %i +select -assert-count 4 c:dff1 c:dff3 c:dff5 c:dff7 %% t:$_DFF_??1_ %i diff --git a/tests/various/.gitignore b/tests/various/.gitignore index 4b286fd61..12d4e5048 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -3,3 +3,4 @@ /write_gzip.v /write_gzip.v.gz /run-test.mk +/plugin.so diff --git a/tests/various/bug1876.ys b/tests/various/bug1876.ys new file mode 100644 index 000000000..7995eedcf --- /dev/null +++ b/tests/various/bug1876.ys @@ -0,0 +1,60 @@ +read_verilog <<EOT +module expression_00032(b5, y15); + input signed [5:0] b5; + output [3:0] y15; + assign y15 = (0 ? b5 : b5) > 0; +endmodule +EOT + + +design -reset +read_verilog <<EOT +module expression_00057(a0, a1, a2, a3, a4, a5, b0, b1, b2, b3, b4, b5, y8); + input [3:0] a0; + input [4:0] a1; + input [5:0] a2; + input signed [3:0] a3; + input signed [4:0] a4; + input signed [5:0] a5; + + input [3:0] b0; + input [4:0] b1; + input [5:0] b2; + input signed [3:0] b3; + input signed [4:0] b4; + input signed [5:0] b5; + + output [5:0] y8; + + localparam signed [4:0] p4 = ((2'd3)||(-4'sd1)); + localparam signed [3:0] p9 = {3{(((2'sd0)^~(5'd20))>((-3'sd0)>>(4'sd2)))}}; + + assign y8 = (-(!($signed({3{p9}})<(p4?b4:b5)))); +endmodule +EOT + + +design -reset +read_verilog <<EOT +module expression_00354(a0, a1, a2, a3, a4, a5, b0, b1, b2, b3, b4, b5, y4); + input [3:0] a0; + input [4:0] a1; + input [5:0] a2; + input signed [3:0] a3; + input signed [4:0] a4; + input signed [5:0] a5; + + input [3:0] b0; + input [4:0] b1; + input [5:0] b2; + input signed [3:0] b3; + input signed [4:0] b4; + input signed [5:0] b5; + + output wire signed [4:0] y4; + + localparam signed [4:0] p10 = ((3'd0)?(2'd1):(-2'sd1)); + + assign y4 = ((p10?a4:b4)&$signed(b3)); +endmodule +EOT diff --git a/tests/various/plugin.cc b/tests/various/plugin.cc new file mode 100644 index 000000000..be305fbda --- /dev/null +++ b/tests/various/plugin.cc @@ -0,0 +1,15 @@ +#include "kernel/rtlil.h" + +YOSYS_NAMESPACE_BEGIN + +struct TestPass : public Pass { + TestPass() : Pass("test", "test") { } + void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + { + size_t argidx = 1; + extra_args(args, argidx, design); + log("Plugin test passed!\n"); + } +} TestPass; + +YOSYS_NAMESPACE_END diff --git a/tests/various/plugin.sh b/tests/various/plugin.sh new file mode 100644 index 000000000..d6d4aee59 --- /dev/null +++ b/tests/various/plugin.sh @@ -0,0 +1,6 @@ +set -e +rm -f plugin.so +CXXFLAGS=$(../../yosys-config --cxxflags) +CXXFLAGS=${CXXFLAGS// -I\/usr\/local\/share\/yosys\/include/ -I..\/..\/share\/include} +../../yosys-config --exec --cxx ${CXXFLAGS} --ldflags -shared -o plugin.so plugin.cc +../../yosys -m ./plugin.so -p "test" | grep -q "Plugin test passed!" |