diff options
Diffstat (limited to 'tests/arch/ice40')
-rw-r--r-- | tests/arch/ice40/bug1598.ys | 16 | ||||
-rw-r--r-- | tests/arch/ice40/counter.ys | 2 | ||||
-rw-r--r-- | tests/arch/ice40/lutram.ys (renamed from tests/arch/ice40/memory.ys) | 6 | ||||
-rw-r--r-- | tests/arch/ice40/mul.ys | 2 | ||||
-rw-r--r-- | tests/arch/ice40/rom.v | 3 |
5 files changed, 23 insertions, 6 deletions
diff --git a/tests/arch/ice40/bug1598.ys b/tests/arch/ice40/bug1598.ys new file mode 100644 index 000000000..8438cb979 --- /dev/null +++ b/tests/arch/ice40/bug1598.ys @@ -0,0 +1,16 @@ +read_verilog <<EOT +module led_blink ( + input clk, + output ledc + ); + + reg [6:0] led_counter = 0; + always @( posedge clk ) begin + led_counter <= led_counter + 1; + end + assign ledc = !led_counter[ 6:3 ]; + +endmodule +EOT +proc +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -abc9 diff --git a/tests/arch/ice40/counter.ys b/tests/arch/ice40/counter.ys index f112eb97d..7bbc4f2c3 100644 --- a/tests/arch/ice40/counter.ys +++ b/tests/arch/ice40/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module select -assert-count 6 t:SB_CARRY diff --git a/tests/arch/ice40/memory.ys b/tests/arch/ice40/lutram.ys index c356e67fb..1ba40f8ec 100644 --- a/tests/arch/ice40/memory.ys +++ b/tests/arch/ice40/lutram.ys @@ -1,5 +1,5 @@ -read_verilog ../common/memory.v -hierarchy -top top +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r proc memory -nomap equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 @@ -10,6 +10,6 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt -cd top +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/mul.ys b/tests/arch/ice40/mul.ys index 9891b77d6..b8c3eb941 100644 --- a/tests/arch/ice40/mul.ys +++ b/tests/arch/ice40/mul.ys @@ -1,6 +1,6 @@ read_verilog ../common/mul.v hierarchy -top top -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module select -assert-count 1 t:SB_MAC16 diff --git a/tests/arch/ice40/rom.v b/tests/arch/ice40/rom.v index 0a0f41f37..71459fe38 100644 --- a/tests/arch/ice40/rom.v +++ b/tests/arch/ice40/rom.v @@ -2,7 +2,8 @@ Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74]. */ module top(data, addr); -output [3:0] data; +output [3:0] data; // Note: this prompts a Yosys warning, but + // vendor doc does not contain 'reg' input [4:0] addr; always @(addr) begin case (addr) |