diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/arch/ice40/mux.ys | 3 | ||||
| -rw-r--r-- | tests/arch/xilinx/macc.v | 12 | ||||
| -rw-r--r-- | tests/arch/xilinx/macc.ys | 4 | ||||
| -rw-r--r-- | tests/simple/constmuldivmod.v | 42 | ||||
| -rw-r--r-- | tests/svtypes/logic_rom.sv | 6 | ||||
| -rw-r--r-- | tests/svtypes/logic_rom.ys | 3 | ||||
| -rw-r--r-- | tests/various/printattr.ys | 14 | ||||
| -rw-r--r-- | tests/verilog/bug2037.ys | 58 |
8 files changed, 132 insertions, 10 deletions
diff --git a/tests/arch/ice40/mux.ys b/tests/arch/ice40/mux.ys index 99822391d..2b661fd6b 100644 --- a/tests/arch/ice40/mux.ys +++ b/tests/arch/ice40/mux.ys @@ -35,6 +35,7 @@ proc equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux16 # Constrain all select calls below inside the top module -select -assert-count 11 t:SB_LUT4 +select -assert-min 11 t:SB_LUT4 +select -assert-max 12 t:SB_LUT4 select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v index e36b2bab1..1645537fd 100644 --- a/tests/arch/xilinx/macc.v +++ b/tests/arch/xilinx/macc.v @@ -10,10 +10,10 @@ module macc # (parameter SIZEIN = 16, SIZEOUT = 40) ( output signed [SIZEOUT-1:0] accum_out ); // Declare registers for intermediate values -reg signed [SIZEIN-1:0] a_reg, b_reg; -reg sload_reg; -reg signed [2*SIZEIN-1:0] mult_reg; -reg signed [SIZEOUT-1:0] adder_out, old_result; +reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0; +reg sload_reg = 0; +reg signed [2*SIZEIN-1:0] mult_reg = 0; +reg signed [SIZEOUT-1:0] adder_out = 0, old_result; always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch if (sload_reg) old_result <= 0; @@ -50,10 +50,10 @@ module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) ( output overflow ); // Declare registers for intermediate values -reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2; +reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0, a_reg2 = 0, b_reg2 = 0; reg signed [2*SIZEIN-1:0] mult_reg = 0; reg signed [SIZEOUT:0] adder_out = 0; -reg overflow_reg; +reg overflow_reg = 0; always @(posedge clk) begin //if (ce) begin diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys index bf2b36320..61a570f48 100644 --- a/tests/arch/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys @@ -6,7 +6,7 @@ proc #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +sat -verify -prove-asserts -seq 3 -show-inputs -show-outputs miter design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd macc # Constrain all select calls below inside the top module select -assert-count 1 t:BUFG @@ -20,7 +20,7 @@ proc #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd macc2 # Constrain all select calls below inside the top module diff --git a/tests/simple/constmuldivmod.v b/tests/simple/constmuldivmod.v index d1d8be862..5dd8f9295 100644 --- a/tests/simple/constmuldivmod.v +++ b/tests/simple/constmuldivmod.v @@ -1,4 +1,4 @@ -module constmuldivmod(input [7:0] A, input [2:0] mode, output reg [7:0] Y); +module constmuldivmod(input [7:0] A, input [5:0] mode, output reg [7:0] Y); always @* begin case (mode) 0: Y = A / 8'd0; @@ -21,6 +21,46 @@ module constmuldivmod(input [7:0] A, input [2:0] mode, output reg [7:0] Y); 13: Y = A % 8'd8; 14: Y = A * 8'd8; + 15: Y = $signed(A) / $signed(8'd0); + 16: Y = $signed(A) % $signed(8'd0); + 17: Y = $signed(A) * $signed(8'd0); + + 18: Y = $signed(A) / $signed(8'd1); + 19: Y = $signed(A) % $signed(8'd1); + 20: Y = $signed(A) * $signed(8'd1); + + 21: Y = $signed(A) / $signed(8'd2); + 22: Y = $signed(A) % $signed(8'd2); + 23: Y = $signed(A) * $signed(8'd2); + + 24: Y = $signed(A) / $signed(8'd4); + 25: Y = $signed(A) % $signed(8'd4); + 26: Y = $signed(A) * $signed(8'd4); + + 27: Y = $signed(A) / $signed(8'd8); + 28: Y = $signed(A) % $signed(8'd8); + 29: Y = $signed(A) * $signed(8'd8); + + 30: Y = $signed(A) / $signed(-8'd0); + 31: Y = $signed(A) % $signed(-8'd0); + 32: Y = $signed(A) * $signed(-8'd0); + + 33: Y = $signed(A) / $signed(-8'd1); + 34: Y = $signed(A) % $signed(-8'd1); + 35: Y = $signed(A) * $signed(-8'd1); + + 36: Y = $signed(A) / $signed(-8'd2); + 37: Y = $signed(A) % $signed(-8'd2); + 38: Y = $signed(A) * $signed(-8'd2); + + 39: Y = $signed(A) / $signed(-8'd4); + 40: Y = $signed(A) % $signed(-8'd4); + 41: Y = $signed(A) * $signed(-8'd4); + + 42: Y = $signed(A) / $signed(-8'd8); + 43: Y = $signed(A) % $signed(-8'd8); + 44: Y = $signed(A) * $signed(-8'd8); + default: Y = 8'd16 * A; endcase end diff --git a/tests/svtypes/logic_rom.sv b/tests/svtypes/logic_rom.sv new file mode 100644 index 000000000..45fe0a4ca --- /dev/null +++ b/tests/svtypes/logic_rom.sv @@ -0,0 +1,6 @@ +module top(input [3:0] addr, output [7:0] data); + logic [7:0] mem[0:15]; + assign data = mem[addr]; + integer i; + initial for(i = 0; i < 16; i = i + 1) mem[i] = i; +endmodule diff --git a/tests/svtypes/logic_rom.ys b/tests/svtypes/logic_rom.ys new file mode 100644 index 000000000..7b079c136 --- /dev/null +++ b/tests/svtypes/logic_rom.ys @@ -0,0 +1,3 @@ +read_verilog -sv logic_rom.sv +prep -top top +select -assert-count 1 t:$mem r:SIZE=16 %i r:WIDTH=8 %i diff --git a/tests/various/printattr.ys b/tests/various/printattr.ys new file mode 100644 index 000000000..afc6d8eb6 --- /dev/null +++ b/tests/various/printattr.ys @@ -0,0 +1,14 @@ +logger -expect log ".*cells_not_processed=[01]* .*" 1 +logger -expect log ".*src=.<<EOT:1\.1-9\.10. .*" 1 +read_verilog <<EOT +module mux2(a, b, s, y); + input a, b, s; + output y; + + wire s_n = ~s; + wire t0 = s & a; + wire t1 = s_n & b; + assign y = t0 | t1; +endmodule +EOT +printattrs diff --git a/tests/verilog/bug2037.ys b/tests/verilog/bug2037.ys new file mode 100644 index 000000000..4b629ba92 --- /dev/null +++ b/tests/verilog/bug2037.ys @@ -0,0 +1,58 @@ +logger -expect-no-warnings +read_verilog <<EOT +module test (); + localparam y = 1; + always @(*) + if (y) (* foo *) ; +endmodule +EOT +select -assert-none a:* a:src %d + + +design -reset +logger -expect-no-warnings +read_verilog <<EOT +module test (); + localparam y = 1; + always @(*) + if (y) (* foo *) ; else (* bar *) ; +endmodule +EOT +select -assert-none a:* a:src %d + + +design -reset +logger -expect-no-warnings +read_verilog <<EOT +module test (); + localparam y = 1; + generate if (y) (* foo *) ; endgenerate +endmodule +EOT +select -assert-none a:* + + +design -reset +logger -expect-no-warnings +read_verilog <<EOT +module test (); + localparam y = 1; + generate if (y) (* foo *) ; else (* bar *); endgenerate +endmodule +EOT +select -assert-none a:* + + +design -reset +read_verilog <<EOT +module test (); + localparam y = 1; + reg x = 1'b0; + always @(*) begin + if (y) + (* foo *) x <= 1'b1; + else + (* bar *) x = 1'b0; + end +endmodule +EOT |