diff options
Diffstat (limited to 'tests')
63 files changed, 1704 insertions, 60 deletions
diff --git a/tests/ice40/.gitignore b/tests/ice40/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/ice40/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/ice40/add_sub.v b/tests/ice40/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/ice40/add_sub.v @@ -0,0 +1,13 @@ +module top +( + input [3:0] x, + input [3:0] y, + + output [3:0] A, + output [3:0] B + ); + +assign A = x + y; +assign B = x - y; + +endmodule diff --git a/tests/ice40/add_sub.ys b/tests/ice40/add_sub.ys new file mode 100644 index 000000000..4a998d98d --- /dev/null +++ b/tests/ice40/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog add_sub.v +hierarchy -top top +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 11 t:SB_LUT4 +select -assert-count 6 t:SB_CARRY +select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D + diff --git a/tests/ice40/adffs.v b/tests/ice40/adffs.v new file mode 100644 index 000000000..09dc36001 --- /dev/null +++ b/tests/ice40/adffs.v @@ -0,0 +1,87 @@ +module adff + ( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, posedge clr ) + if ( clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module adffn + ( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, negedge clr ) + if ( !clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module dffs + ( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, posedge pre ) + if ( pre ) + q <= 1'b1; + else + q <= d; +endmodule + +module ndffnr + ( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( negedge clk, negedge pre ) + if ( !pre ) + q <= 1'b1; + else + q <= d; +endmodule + +module top ( +input clk, +input clr, +input pre, +input a, +output b,b1,b2,b3 +); + +dffs u_dffs ( + .clk (clk ), + .clr (clr), + .pre (pre), + .d (a ), + .q (b ) + ); + +ndffnr u_ndffnr ( + .clk (clk ), + .clr (clr), + .pre (pre), + .d (a ), + .q (b1 ) + ); + +adff u_adff ( + .clk (clk ), + .clr (clr), + .d (a ), + .q (b2 ) + ); + +adffn u_adffn ( + .clk (clk ), + .clr (clr), + .d (a ), + .q (b3 ) + ); + +endmodule diff --git a/tests/ice40/adffs.ys b/tests/ice40/adffs.ys new file mode 100644 index 000000000..548060b66 --- /dev/null +++ b/tests/ice40/adffs.ys @@ -0,0 +1,11 @@ +read_verilog adffs.v +proc +flatten +equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFNS +select -assert-count 2 t:SB_DFFR +select -assert-count 1 t:SB_DFFS +select -assert-count 2 t:SB_LUT4 +select -assert-none t:SB_DFFNS t:SB_DFFR t:SB_DFFS t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/alu.v b/tests/ice40/alu.v new file mode 100644 index 000000000..f82cc2e21 --- /dev/null +++ b/tests/ice40/alu.v @@ -0,0 +1,19 @@ +module top ( + input clock, + input [31:0] dinA, dinB, + input [2:0] opcode, + output reg [31:0] dout +); + always @(posedge clock) begin + case (opcode) + 0: dout <= dinA + dinB; + 1: dout <= dinA - dinB; + 2: dout <= dinA >> dinB; + 3: dout <= $signed(dinA) >>> dinB; + 4: dout <= dinA << dinB; + 5: dout <= dinA & dinB; + 6: dout <= dinA | dinB; + 7: dout <= dinA ^ dinB; + endcase + end +endmodule diff --git a/tests/ice40/alu.ys b/tests/ice40/alu.ys new file mode 100644 index 000000000..bd859efc4 --- /dev/null +++ b/tests/ice40/alu.ys @@ -0,0 +1,11 @@ +read_verilog alu.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 62 t:SB_CARRY +select -assert-count 32 t:SB_DFF +select -assert-count 655 t:SB_LUT4 +select -assert-none t:SB_CARRY t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/counter.v b/tests/ice40/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/ice40/counter.v @@ -0,0 +1,17 @@ +module top (
+out,
+clk,
+reset
+);
+ output [7:0] out;
+ input clk, reset;
+ reg [7:0] out;
+
+ always @(posedge clk, posedge reset)
+ if (reset) begin
+ out <= 8'b0 ;
+ end else
+ out <= out + 1;
+
+
+endmodule
diff --git a/tests/ice40/counter.ys b/tests/ice40/counter.ys new file mode 100644 index 000000000..c65c21622 --- /dev/null +++ b/tests/ice40/counter.ys @@ -0,0 +1,11 @@ +read_verilog counter.v +hierarchy -top top +proc +flatten +equiv_opt -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 +select -assert-count 8 t:SB_DFFR +select -assert-count 8 t:SB_LUT4 +select -assert-none t:SB_CARRY t:SB_DFFR t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/dffs.v b/tests/ice40/dffs.v new file mode 100644 index 000000000..d97840c43 --- /dev/null +++ b/tests/ice40/dffs.v @@ -0,0 +1,37 @@ +module dff + ( input d, clk, output reg q ); + always @( posedge clk ) + q <= d; +endmodule + +module dffe + ( input d, clk, en, output reg q ); + initial begin + q = 0; + end + always @( posedge clk ) + if ( en ) + q <= d; +endmodule + +module top ( +input clk, +input en, +input a, +output b,b1, +); + +dff u_dff ( + .clk (clk ), + .d (a ), + .q (b ) + ); + +dffe u_ndffe ( + .clk (clk ), + .en (en), + .d (a ), + .q (b1 ) + ); + +endmodule diff --git a/tests/ice40/dffs.ys b/tests/ice40/dffs.ys new file mode 100644 index 000000000..ee7f884b1 --- /dev/null +++ b/tests/ice40/dffs.ys @@ -0,0 +1,10 @@ +read_verilog dffs.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFF +select -assert-count 1 t:SB_DFFE +select -assert-none t:SB_DFF t:SB_DFFE %% t:* %D diff --git a/tests/ice40/div_mod.v b/tests/ice40/div_mod.v new file mode 100644 index 000000000..64a36707d --- /dev/null +++ b/tests/ice40/div_mod.v @@ -0,0 +1,13 @@ +module top +( + input [3:0] x, + input [3:0] y, + + output [3:0] A, + output [3:0] B + ); + +assign A = x % y; +assign B = x / y; + +endmodule diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys new file mode 100644 index 000000000..821d6c301 --- /dev/null +++ b/tests/ice40/div_mod.ys @@ -0,0 +1,9 @@ +read_verilog div_mod.v +hierarchy -top top +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 59 t:SB_LUT4 +select -assert-count 41 t:SB_CARRY +select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D diff --git a/tests/ice40/dpram.v b/tests/ice40/dpram.v new file mode 100644 index 000000000..3ea4c1f27 --- /dev/null +++ b/tests/ice40/dpram.v @@ -0,0 +1,23 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72]. +*/ +module top (din, write_en, waddr, wclk, raddr, rclk, dout); +parameter addr_width = 8; +parameter data_width = 8; +input [addr_width-1:0] waddr, raddr; +input [data_width-1:0] din; +input write_en, wclk, rclk; +output [data_width-1:0] dout; +reg [data_width-1:0] dout; +reg [data_width-1:0] mem [(1<<addr_width)-1:0] +/* synthesis syn_ramstyle = "no_rw_check" */ ; +always @(posedge wclk) // Write memory. +begin +if (write_en) +mem[waddr] <= din; // Using write address bus. +end +always @(posedge rclk) // Read memory. +begin +dout <= mem[raddr]; // Using read address bus. +end +endmodule diff --git a/tests/ice40/dpram.ys b/tests/ice40/dpram.ys new file mode 100644 index 000000000..4f6a253ea --- /dev/null +++ b/tests/ice40/dpram.ys @@ -0,0 +1,15 @@ +read_verilog dpram.v +hierarchy -top top +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 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:SB_RAM40_4K +select -assert-none t:SB_RAM40_4K %% t:* %D diff --git a/tests/ice40/fsm.v b/tests/ice40/fsm.v new file mode 100644 index 000000000..0605bd102 --- /dev/null +++ b/tests/ice40/fsm.v @@ -0,0 +1,73 @@ + module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1
+ );
+ input clock,reset,req_0,req_1;
+ output gnt_0,gnt_1;
+ wire clock,reset,req_0,req_1;
+ reg gnt_0,gnt_1;
+
+ parameter SIZE = 3 ;
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+ state <= #1 IDLE;
+ gnt_0 <= 0;
+ gnt_1 <= 0;
+ end else
+ case(state)
+ IDLE : if (req_0 == 1'b1) begin
+ state <= #1 GNT0;
+ gnt_0 <= 1;
+ end else if (req_1 == 1'b1) begin
+ gnt_1 <= 1;
+ state <= #1 GNT0;
+ end else begin
+ state <= #1 IDLE;
+ end
+ GNT0 : if (req_0 == 1'b1) begin
+ state <= #1 GNT0;
+ end else begin
+ gnt_0 <= 0;
+ state <= #1 IDLE;
+ end
+ GNT1 : if (req_1 == 1'b1) begin
+ state <= #1 GNT2;
+ gnt_1 <= req_0;
+ end
+ GNT2 : if (req_0 == 1'b1) begin
+ state <= #1 GNT1;
+ gnt_1 <= req_1;
+ end
+ default : state <= #1 IDLE;
+ endcase
+ end
+
+ endmodule
+
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+ .reset(rst),
+ .req_0(a),
+ .req_1(b),
+ .gnt_0(g0),
+ .gnt_1(g1));
+
+endmodule
diff --git a/tests/ice40/fsm.ys b/tests/ice40/fsm.ys new file mode 100644 index 000000000..4cc8629d6 --- /dev/null +++ b/tests/ice40/fsm.ys @@ -0,0 +1,13 @@ +read_verilog fsm.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 2 t:SB_DFFESR +select -assert-count 2 t:SB_DFFSR +select -assert-count 1 t:SB_DFFSS +select -assert-count 13 t:SB_LUT4 +select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/ice40_opt.ys b/tests/ice40/ice40_opt.ys new file mode 100644 index 000000000..b17c69c91 --- /dev/null +++ b/tests/ice40/ice40_opt.ys @@ -0,0 +1,26 @@ +read_verilog -icells -formal <<EOT +module top(input CI, I0, output [1:0] CO, output O); + wire A = 1'b0, B = 1'b0; + \$__ICE40_CARRY_WRAPPER #( + // A[0]: 1010 1010 1010 1010 + // A[1]: 1100 1100 1100 1100 + // A[2]: 1111 0000 1111 0000 + // A[3]: 1111 1111 0000 0000 + .LUT(~16'b 0110_1001_1001_0110) + ) u0 ( + .A(A), + .B(B), + .CI(CI), + .I0(I0), + .I3(CI), + .CO(CO[0]), + .O(O) + ); + SB_CARRY u1 (.I0(~A), .I1(~B), .CI(CI), .CO(CO[1])); +endmodule +EOT + +equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt +design -load postopt +select -assert-count 1 t:* +select -assert-count 1 t:$lut diff --git a/tests/ice40/latches.v b/tests/ice40/latches.v new file mode 100644 index 000000000..9dc43e4c2 --- /dev/null +++ b/tests/ice40/latches.v @@ -0,0 +1,58 @@ +module latchp + ( input d, clk, en, output reg q ); + always @* + if ( en ) + q <= d; +endmodule + +module latchn + ( input d, clk, en, output reg q ); + always @* + if ( !en ) + q <= d; +endmodule + +module latchsr + ( input d, clk, en, clr, pre, output reg q ); + always @* + if ( clr ) + q <= 1'b0; + else if ( pre ) + q <= 1'b1; + else if ( en ) + q <= d; +endmodule + + +module top ( +input clk, +input clr, +input pre, +input a, +output b,b1,b2 +); + + +latchp u_latchp ( + .en (clk ), + .d (a ), + .q (b ) + ); + + +latchn u_latchn ( + .en (clk ), + .d (a ), + .q (b1 ) + ); + + +latchsr u_latchsr ( + .en (clk ), + .clr (clr), + .pre (pre), + .d (a ), + .q (b2 ) + ); + +endmodule diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys new file mode 100644 index 000000000..f3562559e --- /dev/null +++ b/tests/ice40/latches.ys @@ -0,0 +1,15 @@ +read_verilog latches.v +design -save read + +proc +async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock +flatten +synth_ice40 +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) + +design -load read +synth_ice40 +cd top +select -assert-count 4 t:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/logic.v b/tests/ice40/logic.v new file mode 100644 index 000000000..e5343cae0 --- /dev/null +++ b/tests/ice40/logic.v @@ -0,0 +1,18 @@ +module top +( + input [0:7] in, + output B1,B2,B3,B4,B5,B6,B7,B8,B9,B10 + ); + + assign B1 = in[0] & in[1]; + assign B2 = in[0] | in[1]; + assign B3 = in[0] ~& in[1]; + assign B4 = in[0] ~| in[1]; + assign B5 = in[0] ^ in[1]; + assign B6 = in[0] ~^ in[1]; + assign B7 = ~in[0]; + assign B8 = in[0]; + assign B9 = in[0:1] && in [2:3]; + assign B10 = in[0:1] || in [2:3]; + +endmodule diff --git a/tests/ice40/logic.ys b/tests/ice40/logic.ys new file mode 100644 index 000000000..fc5e5b1d8 --- /dev/null +++ b/tests/ice40/logic.ys @@ -0,0 +1,7 @@ +read_verilog logic.v +hierarchy -top top +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 9 t:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/macc.v b/tests/ice40/macc.v new file mode 100644 index 000000000..6c3676c83 --- /dev/null +++ b/tests/ice40/macc.v @@ -0,0 +1,25 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 77]. +*/ +module top(clk,a,b,c,set); +parameter A_WIDTH = 6 /*4*/; +parameter B_WIDTH = 6 /*3*/; +input set; +input clk; +input signed [(A_WIDTH - 1):0] a; +input signed [(B_WIDTH - 1):0] b; +output signed [(A_WIDTH + B_WIDTH - 1):0] c; +reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c; +assign c = reg_tmp_c; +always @(posedge clk) +begin +if(set) +begin +reg_tmp_c <= 0; +end +else +begin +reg_tmp_c <= a * b + c; +end +end +endmodule diff --git a/tests/ice40/macc.ys b/tests/ice40/macc.ys new file mode 100644 index 000000000..0f4c19be5 --- /dev/null +++ b/tests/ice40/macc.ys @@ -0,0 +1,13 @@ +read_verilog macc.v +proc +hierarchy -top top +#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check + +equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -dsp +async2sync +equiv_opt -run prove: -assert null + +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_MAC16 +select -assert-none t:SB_MAC16 %% t:* %D diff --git a/tests/ice40/memory.v b/tests/ice40/memory.v new file mode 100644 index 000000000..cb7753f7b --- /dev/null +++ b/tests/ice40/memory.v @@ -0,0 +1,21 @@ +module top +( + input [7:0] data_a, + input [6:1] addr_a, + input we_a, clk, + output reg [7:0] q_a +); + // Declare the RAM variable + reg [7:0] ram[63:0]; + + // Port A + always @ (posedge clk) + begin + if (we_a) + begin + ram[addr_a] <= data_a; + q_a <= data_a; + end + q_a <= ram[addr_a]; + end +endmodule diff --git a/tests/ice40/memory.ys b/tests/ice40/memory.ys new file mode 100644 index 000000000..a66afbae6 --- /dev/null +++ b/tests/ice40/memory.ys @@ -0,0 +1,15 @@ +read_verilog memory.v +hierarchy -top top +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 top +select -assert-count 1 t:SB_RAM40_4K +select -assert-none t:SB_RAM40_4K %% t:* %D diff --git a/tests/ice40/mul.v b/tests/ice40/mul.v new file mode 100644 index 000000000..d5b48b1d7 --- /dev/null +++ b/tests/ice40/mul.v @@ -0,0 +1,11 @@ +module top +( + input [5:0] x, + input [5:0] y, + + output [11:0] A, + ); + +assign A = x * y; + +endmodule diff --git a/tests/ice40/mul.ys b/tests/ice40/mul.ys new file mode 100644 index 000000000..8a0822a84 --- /dev/null +++ b/tests/ice40/mul.ys @@ -0,0 +1,7 @@ +read_verilog mul.v +hierarchy -top top +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_MAC16 +select -assert-none t:SB_MAC16 %% t:* %D diff --git a/tests/ice40/mux.v b/tests/ice40/mux.v new file mode 100644 index 000000000..0814b733e --- /dev/null +++ b/tests/ice40/mux.v @@ -0,0 +1,100 @@ +module mux2 (S,A,B,Y); + input S; + input A,B; + output reg Y; + + always @(*) + Y = (S)? B : A; +endmodule + +module mux4 ( S, D, Y ); + +input[1:0] S; +input[3:0] D; +output Y; + +reg Y; +wire[1:0] S; +wire[3:0] D; + +always @* +begin + case( S ) + 0 : Y = D[0]; + 1 : Y = D[1]; + 2 : Y = D[2]; + 3 : Y = D[3]; + endcase +end + +endmodule + +module mux8 ( S, D, Y ); + +input[2:0] S; +input[7:0] D; +output Y; + +reg Y; +wire[2:0] S; +wire[7:0] D; + +always @* +begin + case( S ) + 0 : Y = D[0]; + 1 : Y = D[1]; + 2 : Y = D[2]; + 3 : Y = D[3]; + 4 : Y = D[4]; + 5 : Y = D[5]; + 6 : Y = D[6]; + 7 : Y = D[7]; + endcase +end + +endmodule + +module mux16 (D, S, Y); + input [15:0] D; + input [3:0] S; + output Y; + +assign Y = D[S]; + +endmodule + + +module top ( +input [3:0] S, +input [15:0] D, +output M2,M4,M8,M16 +); + +mux2 u_mux2 ( + .S (S[0]), + .A (D[0]), + .B (D[1]), + .Y (M2) + ); + + +mux4 u_mux4 ( + .S (S[1:0]), + .D (D[3:0]), + .Y (M4) + ); + +mux8 u_mux8 ( + .S (S[2:0]), + .D (D[7:0]), + .Y (M8) + ); + +mux16 u_mux16 ( + .S (S[3:0]), + .D (D[15:0]), + .Y (M16) + ); + +endmodule diff --git a/tests/ice40/mux.ys b/tests/ice40/mux.ys new file mode 100644 index 000000000..182b49499 --- /dev/null +++ b/tests/ice40/mux.ys @@ -0,0 +1,8 @@ +read_verilog mux.v +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 19 t:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/rom.v b/tests/ice40/rom.v new file mode 100644 index 000000000..0a0f41f37 --- /dev/null +++ b/tests/ice40/rom.v @@ -0,0 +1,18 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74]. +*/ +module top(data, addr); +output [3:0] data; +input [4:0] addr; +always @(addr) begin +case (addr) +0 : data = 'h4; +1 : data = 'h9; +2 : data = 'h1; +15 : data = 'h8; +16 : data = 'h1; +17 : data = 'h0; +default : data = 'h0; +endcase +end +endmodule diff --git a/tests/ice40/rom.ys b/tests/ice40/rom.ys new file mode 100644 index 000000000..41d214e2a --- /dev/null +++ b/tests/ice40/rom.ys @@ -0,0 +1,8 @@ +read_verilog rom.v +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 5 t:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh new file mode 100755 index 000000000..46716f9a0 --- /dev/null +++ b/tests/ice40/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/ice40/shifter.v b/tests/ice40/shifter.v new file mode 100644 index 000000000..c55632552 --- /dev/null +++ b/tests/ice40/shifter.v @@ -0,0 +1,22 @@ +module top (
+out,
+clk,
+in
+);
+ output [7:0] out;
+ input signed clk, in;
+ reg signed [7:0] out = 0;
+
+ always @(posedge clk)
+ begin
+`ifndef BUG
+ out <= out >> 1;
+ out[7] <= in;
+`else
+
+ out <= out << 1;
+ out[7] <= in;
+`endif
+ end
+
+endmodule
diff --git a/tests/ice40/shifter.ys b/tests/ice40/shifter.ys new file mode 100644 index 000000000..47d95d298 --- /dev/null +++ b/tests/ice40/shifter.ys @@ -0,0 +1,9 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:SB_DFF +select -assert-none t:SB_DFF %% t:* %D diff --git a/tests/ice40/tribuf.v b/tests/ice40/tribuf.v new file mode 100644 index 000000000..870a02584 --- /dev/null +++ b/tests/ice40/tribuf.v @@ -0,0 +1,23 @@ +module tristate (en, i, o); + input en; + input i; + output o; + + assign o = en ? i : 1'bz; + +endmodule + + +module top ( +input en, +input a, +output b +); + +tristate u_tri ( + .en (en ), + .i (a ), + .o (b ) + ); + +endmodule diff --git a/tests/ice40/tribuf.ys b/tests/ice40/tribuf.ys new file mode 100644 index 000000000..d1e1b3108 --- /dev/null +++ b/tests/ice40/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog tribuf.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +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 f0306efa1..e0acead82 100644 --- a/tests/opt/opt_expr.ys +++ b/tests/opt/opt_expr.ys @@ -204,7 +204,7 @@ endmodule EOT check -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$alu r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i @@ -218,6 +218,76 @@ endmodule EOT check -equiv_opt opt_expr -fine +equiv_opt -assert opt_expr -fine design -load postopt select -assert-count 1 t:$alu r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_shiftx_1bit(input [2:0] a, input [1:0] b, output y); + \$shiftx #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(2), .Y_WIDTH(1)) shiftx (.A({1'bx,a}), .B(b), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr +design -load postopt +select -assert-count 1 t:$shiftx r:A_WIDTH=3 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_shiftx_3bit(input [9:0] a, input [3:0] b, output [2:0] y); + \$shiftx #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shiftx (.A({4'bxx00,a}), .B(b), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr +design -load postopt +select -assert-count 1 t:$shiftx r:A_WIDTH=12 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_shift_1bit(input [2:0] a, input [1:0] b, output y); + \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(2), .Y_WIDTH(1)) shift (.A({1'b0,a}), .B(b), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr +design -load postopt +select -assert-count 1 t:$shift r:A_WIDTH=3 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_shift_3bit(input [9:0] a, input [3:0] b, output [2:0] y); + \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shift (.A({4'b0x0x,a}), .B(b), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr +design -load postopt +select -assert-count 1 t:$shift r:A_WIDTH=10 %i + +########### + +design -reset +read_verilog -icells <<EOT +module opt_expr_shift_3bit_keepdc(input [9:0] a, input [3:0] b, output [2:0] y); + \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shift (.A({4'b0x0x,a}), .B(b), .Y(y)); +endmodule +EOT +check + +equiv_opt -assert opt_expr -keepdc +design -load postopt +select -assert-count 1 t:$shift r:A_WIDTH=13 %i diff --git a/tests/sat/initval.v b/tests/sat/initval.v index 5b661f8d6..81f71b5ba 100644 --- a/tests/sat/initval.v +++ b/tests/sat/initval.v @@ -1,6 +1,7 @@ -module test(input clk, input [3:0] bar, output [3:0] foo); +module test(input clk, input [3:0] bar, output [3:0] foo, asdf); reg [3:0] foo = 0; reg [3:0] last_bar = 0; + reg [3:0] asdf = 4'b1xxx; always @* foo[1:0] <= bar[1:0]; @@ -11,5 +12,10 @@ module test(input clk, input [3:0] bar, output [3:0] foo); always @(posedge clk) last_bar <= bar; + always @(posedge clk) + asdf[3] <= bar[3]; + always @* + asdf[2:0] = 3'b111; + assert property (foo == {last_bar[3:2], bar[1:0]}); endmodule diff --git a/tests/simple/peepopt.v b/tests/simple/peepopt.v deleted file mode 100644 index 1bf427897..000000000 --- a/tests/simple/peepopt.v +++ /dev/null @@ -1,13 +0,0 @@ -module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); -assign o = i[s*W+:W]; -endmodule - -module peepopt_shiftmul_1 (output y, input [2:0] w); -assign y = 1'b1 >> (w * (3'b110)); -endmodule - -module peepopt_muldiv_0(input [1:0] i, output [1:0] o); -wire [3:0] t; -assign t = i * 3; -assign o = t / 3; -endmodule diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh index 967ac49f2..f20fd0d30 100755 --- a/tests/simple/run-test.sh +++ b/tests/simple/run-test.sh @@ -12,7 +12,7 @@ done shift "$((OPTIND-1))" # check for Icarus Verilog -if ! which iverilog > /dev/null ; then +if ! command -v iverilog > /dev/null ; then echo "$0: Error: Icarus Verilog 'iverilog' not found." exit 1 fi diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh index 49ae23338..0d4262005 100755 --- a/tests/simple_abc9/run-test.sh +++ b/tests/simple_abc9/run-test.sh @@ -12,7 +12,7 @@ done shift "$((OPTIND-1))" # check for Icarus Verilog -if ! which iverilog > /dev/null ; then +if ! command -v iverilog > /dev/null ; then echo "$0: Error: Icarus Verilog 'iverilog' not found." exit 1 fi @@ -20,4 +20,10 @@ fi cp ../simple/*.v . cp ../simple/*.sv . DOLLAR='?' -exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p 'hierarchy; synth -run coarse; opt -full; techmap; abc9 -lut 4 -box ../abc.box; stat; check -assert; select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'" +exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\ + hierarchy; \ + synth -run coarse; \ + opt -full; \ + techmap; abc9 -lut 4 -box ../abc.box; \ + check -assert; \ + select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'" diff --git a/tests/techmap/.gitignore b/tests/techmap/.gitignore index 397b4a762..cfed22fc5 100644 --- a/tests/techmap/.gitignore +++ b/tests/techmap/.gitignore @@ -1 +1,2 @@ *.log +/*.mk diff --git a/tests/techmap/autopurge.ys b/tests/techmap/autopurge.ys new file mode 100644 index 000000000..1eb99ec37 --- /dev/null +++ b/tests/techmap/autopurge.ys @@ -0,0 +1,62 @@ +# https://github.com/YosysHQ/yosys/issues/1381 +read_verilog <<EOT +module sub(input i, output o, (* techmap_autopurge *) input j); +foobar f(i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +(* blackbox *) +module sub(input i, output o, input j); +endmodule + +(* blackbox *) +module foobar(input i, output o, input j); +endmodule + +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +hierarchy +check -assert + +# https://github.com/YosysHQ/yosys/issues/1391 +design -reset +read_verilog <<EOT +module sub(input i, output o, (* techmap_autopurge *) input [1:0] j); +foobar f(i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +(* blackbox *) +module sub(input i, output o, input j); +endmodule + +(* blackbox *) +module foobar(input i, output o, input j); +endmodule + +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +hierarchy +check -assert + +read_verilog -overwrite <<EOT +module top(input i, output o); +wire j; +sub s0(i, o, j); +endmodule +EOT + +techmap -map %techmap +hierarchy diff --git a/tests/techmap/clkbufmap.ys b/tests/techmap/clkbufmap.ys new file mode 100644 index 000000000..f1277864e --- /dev/null +++ b/tests/techmap/clkbufmap.ys @@ -0,0 +1,96 @@ +read_verilog <<EOT +module clkbuf (input i, (* clkbuf_driver *) output o); endmodule +module dff ((* clkbuf_sink *) input clk, input d, output q); endmodule +module dffe ((* clkbuf_sink *) input c, input d, e, output q); endmodule +module latch (input e, d, output q); endmodule +module clkgen (output o); endmodule + +module top(input clk1, clk2, clk3, d, e, output [4:0] q); +wire clk4, clk5, clk6; +dff s0 (.clk(clk1), .d(d), .q(q[0])); +dffe s1 (.c(clk2), .d(d), .e(e), .q(q[1])); +latch s2 (.e(clk3), .d(d), .q(q[2])); +sub s3 (.sclk4(clk4), .sclk5(clk5), .sclk6(clk6), .sd(d), .sq(q[3])); +dff s4 (.clk(clk4), .d(d), .q(q[4])); +dff s5 (.clk(clk5), .d(d), .q(q[4])); +dff s6 (.clk(clk6), .d(d), .q(q[4])); +endmodule + +module sub(output sclk4, output sclk5, output sclk6, input sd, output sq); +wire tmp; +clkgen s7(.o(sclk4)); +clkgen s8(.o(sclk5)); +clkgen s9(.o(tmp)); +clkbuf s10(.i(tmp), .o(sclk6)); +dff s11(.clk(sclk4), .d(sd), .q(sq)); +endmodule +EOT + +hierarchy -auto-top +design -save ref + +# ---------------------- + +design -load ref +clkbufmap -buf clkbuf o:i +select -assert-count 3 top/t:clkbuf +select -assert-count 2 sub/t:clkbuf +select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' +select -assert-count 1 @clk1 # Check there is one such fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i # And that one fanout is 's0' +select -set clk2 w:clk2 %a %co t:clkbuf %i +select -assert-count 1 @clk2 +select -assert-count 1 @clk2 %x:+[o] %co c:s* %i +select -assert-count 1 @clk2 %x:+[o] %co c:s1 %i +select -set clk5 w:clk5 %a %ci t:clkbuf %i +select -assert-count 1 @clk5 +select -assert-count 1 @clk5 %x:+[o] %co c:s5 %i +select -assert-count 1 @clk5 %x:+[i] %ci c:s3 %i +select -set sclk4 w:sclk4 %a %ci t:clkbuf %i +select -assert-count 1 @sclk4 +select -assert-count 1 @sclk4 %x:+[o] %co c:s11 %i +select -assert-count 1 @sclk4 %x:+[i] %ci c:s7 %i + +# ---------------------- + +design -load ref +setattr -set clkbuf_inhibit 0 w:clk1 +setattr -set clkbuf_inhibit 1 w:clk2 +clkbufmap -buf clkbuf o:i +select -assert-count 2 top/t:clkbuf +select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' +select -assert-count 1 @clk1 # Check there is one such fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i # And that one fanout is 's0' +select -assert-count 0 w:clk2 %a %co t:clkbuf %i + +# ---------------------- + +design -load ref +setattr -set clkbuf_inhibit 1 w:clk1 +setattr -set buffer_type "bufg" w:clk2 +clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d +select -assert-count 3 top/t:clkbuf +select -assert-count 2 sub/t:clkbuf +select -set clk1 w:clk1 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' +select -assert-count 1 @clk1 # Check there is one such fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout +select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i # And that one fanout is 's0' +select -set clk2 w:clk2 %a %co t:clkbuf %i # Find 'clk1' fanouts that are 'clkbuf' +select -assert-count 1 @clk2 # Check there is one such fanout +select -assert-count 1 @clk2 %x:+[o] %co c:s* %i # Check that the 'o' of that clkbuf drives one fanout +select -assert-count 1 @clk2 %x:+[o] %co c:s1 %i # And that one fanout is 's0' + +# ---------------------- + +design -load ref +setattr -set buffer_type "none" w:clk1 +setattr -set buffer_type "bufr" w:clk2 +setattr -set buffer_type "bufr" w:sclk4 +setattr -set buffer_type "bufr" w:sclk5 +clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d +select -assert-count 0 w:clk1 %a %co t:clkbuf %i +select -assert-count 0 w:clk2 %a %co t:clkbuf %i +select -assert-count 0 top/t:clkbuf +select -assert-count 1 sub/t:clkbuf diff --git a/tests/techmap/dff2dffs.ys b/tests/techmap/dff2dffs.ys new file mode 100644 index 000000000..13f1a3cf3 --- /dev/null +++ b/tests/techmap/dff2dffs.ys @@ -0,0 +1,50 @@ +read_verilog << EOT +module top(...); +input clk; +input d; +input sr; +output reg q0, q1, q2, q3, q4, q5; + +initial q0 = 1'b0; +initial q1 = 1'b0; +initial q2 = 1'b1; +initial q3 = 1'b1; +initial q4 = 1'bx; +initial q5 = 1'bx; + +always @(posedge clk) begin + q0 <= sr ? 1'b0 : d; + q1 <= sr ? 1'b1 : d; + q2 <= sr ? 1'b0 : d; + q3 <= sr ? 1'b1 : d; + q4 <= sr ? 1'b0 : d; + q5 <= sr ? 1'b1 : d; +end + +endmodule +EOT + +proc +simplemap +design -save ref + +dff2dffs +clean + +select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q1 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q2 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i + +design -load ref +dff2dffs -match-init +clean + +select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i +select -assert-count 0 w:q1 %x t:$__DFFS_PP1_ %i +select -assert-count 0 w:q2 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i +select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i +select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i diff --git a/tests/techmap/extractinv.ys b/tests/techmap/extractinv.ys new file mode 100644 index 000000000..6146f829a --- /dev/null +++ b/tests/techmap/extractinv.ys @@ -0,0 +1,41 @@ +read_verilog << EOT + +module ff4(...); +parameter [0:0] CLK_INV = 1'b0; +parameter [3:0] DATA_INV = 4'b0000; +(* invertible_pin = "CLK_INV" *) +input clk; +(* invertible_pin = "DATA_INV" *) +input [3:0] d; +output [3:0] q; +endmodule + +module inv(...); +output o; +input i; +endmodule + +module top(...); +input d0, d1, d2, d3; +input clk; +output q; +ff4 #(.DATA_INV(4'h5)) ff_inst (.clk(clk), .d({d3, d2, d1, d0}), .q(q)); +endmodule + +EOT + +extractinv -inv inv o:i +clean + +select -assert-count 2 top/t:inv +select -assert-count 2 top/t:inv top/t:ff4 %ci:+[d] %ci:+[o] %i + +select -assert-count 1 top/t:inv top/w:d0 %co:+[i] %i +select -assert-count 0 top/t:inv top/w:d1 %co:+[i] %i +select -assert-count 1 top/t:inv top/w:d2 %co:+[i] %i +select -assert-count 0 top/t:inv top/w:d3 %co:+[i] %i + +select -assert-count 0 top/t:ff4 top/w:d0 %co:+[d] %i +select -assert-count 1 top/t:ff4 top/w:d1 %co:+[d] %i +select -assert-count 0 top/t:ff4 top/w:d2 %co:+[d] %i +select -assert-count 1 top/t:ff4 top/w:d3 %co:+[d] %i diff --git a/tests/techmap/recursive.v b/tests/techmap/recursive.v new file mode 100644 index 000000000..d281b21d8 --- /dev/null +++ b/tests/techmap/recursive.v @@ -0,0 +1,8 @@ +module top; +sub s0(); +foo f0(); +endmodule + +module foo; +sub s0(); +endmodule diff --git a/tests/techmap/recursive_map.v b/tests/techmap/recursive_map.v new file mode 100644 index 000000000..934256552 --- /dev/null +++ b/tests/techmap/recursive_map.v @@ -0,0 +1,4 @@ +module sub; + sub _TECHMAP_REPLACE_ (); + bar f0(); +endmodule diff --git a/tests/techmap/recursive_runtest.sh b/tests/techmap/recursive_runtest.sh new file mode 100644 index 000000000..30c79bf03 --- /dev/null +++ b/tests/techmap/recursive_runtest.sh @@ -0,0 +1,3 @@ +set -ev + +../../yosys -p 'hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar' recursive.v diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh index e2fc11e52..96489ff15 100755 --- a/tests/techmap/run-test.sh +++ b/tests/techmap/run-test.sh @@ -1,10 +1,20 @@ -#!/bin/bash +#!/usr/bin/env bash set -e -for x in *_runtest.sh; do - echo "Running $x.." - if ! bash $x &> ${x%.sh}.log; then - tail ${x%.sh}.log - echo ERROR - exit 1 +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../yosys -ql ${x%.ys}.log $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s > ${s%.sh}.log 2>&1" fi done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/techmap/wireinit.ys b/tests/techmap/wireinit.ys new file mode 100644 index 000000000..89afaafb5 --- /dev/null +++ b/tests/techmap/wireinit.ys @@ -0,0 +1,108 @@ +read_verilog <<EOT +(* techmap_celltype = "$_DFF_P_" *) +module ffmap(...); +input D; +input C; +output Q; +parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx; + +ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C)); + +wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1; + +wire _TECHMAP_REMOVEINIT_Q_ = 1'b1; + +endmodule +EOT +design -stash map + +read_verilog <<EOT +(* techmap_celltype = "$_DFF_P_" *) +module ffmap(...); +input D; +input C; +output Q; +parameter [0:0] _TECHMAP_WIREINIT_Q_ = 1'bx; + +ffbb #(.INIT(_TECHMAP_WIREINIT_Q_)) _TECHMAP_REPLACE_(.D(D), .Q(Q), .C(C)); + +wire _TECHMAP_FAIL_ = _TECHMAP_WIREINIT_Q_ === 1'b1; + +wire _TECHMAP_REMOVEINIT_Q_ = 1'b0; + +endmodule +EOT +design -stash map_noremove + +read_verilog <<EOT +module ffbb (...); +parameter [0:0] INIT = 1'bx; +input D, C; +output Q; +endmodule + +module top(...); +input clk; +input d; +output reg q0 = 0; +output reg q1 = 1; +output reg qq0 = 0; +output reg qx; + +always @(posedge clk) begin + q0 <= d; + q1 <= d; + qq0 <= q0; + qx <= d; +end +endmodule +EOT + +design -save ref + +hierarchy -auto-top +proc +simplemap +techmap -map %map +clean +# Make sure the parameter was used properly. +select -assert-count 3 top/t:ffbb +select -set ff0 top/w:q0 %ci t:ffbb %i +select -set ffq0 top/w:qq0 %ci t:ffbb %i +select -set ffx top/w:qx %ci t:ffbb %i +select -assert-count 1 @ff0 +select -assert-count 1 @ffq0 +select -assert-count 1 @ffx +select -assert-count 1 @ff0 r:INIT=1'b0 %i +select -assert-count 1 @ffq0 r:INIT=1'b0 %i +select -assert-count 1 @ffx r:INIT=1'bx %i +select -assert-count 0 top/w:q1 %ci t:ffbb %i +# Make sure the init values are dropped from the wires iff mapping was performed. +select -assert-count 0 top/w:q0 a:init %i +select -assert-count 0 top/w:qq0 a:init %i +select -assert-count 1 top/w:q1 a:init=1'b1 %i +select -assert-count 0 top/w:qx a:init %i + +design -load ref +hierarchy -auto-top +proc +simplemap +techmap -map %map_noremove +clean +# Make sure the parameter was used properly. +select -assert-count 3 top/t:ffbb +select -set ff0 top/w:q0 %ci t:ffbb %i +select -set ffq0 top/w:qq0 %ci t:ffbb %i +select -set ffx top/w:qx %ci t:ffbb %i +select -assert-count 1 @ff0 +select -assert-count 1 @ffq0 +select -assert-count 1 @ffx +select -assert-count 1 @ff0 r:INIT=1'b0 %i +select -assert-count 1 @ffq0 r:INIT=1'b0 %i +select -assert-count 1 @ffx r:INIT=1'bx %i +select -assert-count 0 top/w:q1 %ci t:ffbb %i +# Make sure the init values are not dropped from the wires. +select -assert-count 1 top/w:q0 a:init=1'b0 %i +select -assert-count 1 top/w:qq0 a:init=1'b0 %i +select -assert-count 1 top/w:q1 a:init=1'b1 %i +select -assert-count 0 top/w:qx a:init %i diff --git a/tests/various/abc9.v b/tests/various/abc9.v index a08b613a8..30ebd4e26 100644 --- a/tests/various/abc9.v +++ b/tests/various/abc9.v @@ -5,5 +5,7 @@ always @* endmodule module abc9_test028(input i, output o); -unknown u(~i, o); +wire w; +unknown u(~i, w); +unknown2 u2(w, o); endmodule diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys new file mode 100644 index 000000000..81e36d018 --- /dev/null +++ b/tests/various/equiv_opt_multiclock.ys @@ -0,0 +1,12 @@ +read_verilog <<EOT +module top(input clk, pre, d, output reg q); + always @(posedge clk, posedge pre) + if (pre) + q <= 1'b1; + else + q <= d; +endmodule +EOT + +prep +equiv_opt -assert -multiclock -map +/simcells.v synth diff --git a/tests/various/hierarchy_defer.ys b/tests/various/hierarchy_defer.ys new file mode 100644 index 000000000..70f5b70a3 --- /dev/null +++ b/tests/various/hierarchy_defer.ys @@ -0,0 +1,27 @@ +read -noverific +read -vlog2k <<EOT +module first; +endmodule + +(* top *) +module top(input i, output o); +sub s0(i, o); +endmodule + +(* constant_expression=1+1?2*2:3/3 *) +module sub(input i, output o); +assign o = ~i; +endmodule +EOT +design -save read + +hierarchy -auto-top +select -assert-any top +select -assert-any sub +select -assert-none foo + +design -load read +hierarchy +select -assert-any top +select -assert-any sub +select -assert-none foo diff --git a/tests/various/mem2reg.ys b/tests/various/mem2reg.ys new file mode 100644 index 000000000..85d6267c5 --- /dev/null +++ b/tests/various/mem2reg.ys @@ -0,0 +1,14 @@ +read_verilog <<EOT +module top; +parameter DATADEPTH=2; +parameter DATAWIDTH=1; +(* keep, nomem2reg *) reg [DATAWIDTH-1:0] data1 [DATADEPTH-1:0]; +(* keep, mem2reg *) reg [DATAWIDTH-1:0] data2 [DATADEPTH-1:0]; +endmodule +EOT + +proc +cd top +select -assert-count 1 m:data1 a:src=<<EOT:4 %i +select -assert-count 2 w:data2[*] a:src=<<EOT:5 %i +select -assert-none a:mem2reg diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys new file mode 100644 index 000000000..6bca62e2b --- /dev/null +++ b/tests/various/peepopt.ys @@ -0,0 +1,175 @@ +read_verilog <<EOT +module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); +assign o = i[s*W+:W]; +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$shiftx +select -assert-count 0 t:$shiftx t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w); +assign y = 1'b1 >> (w * (3'b110)); +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y); + assign Y = D >> (S*3); +endmodule +EOT + +prep +design -save gold +peepopt +design -stash gate + +design -import gold -as gold peepopt_shiftmul_2 +design -import gate -as gate peepopt_shiftmul_2 + +miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter +sat -show-public -enable_undef -prove-asserts miter +cd gate +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_muldiv_0(input [1:0] i, output [1:0] o); +wire [3:0] t; +assign t = i * 3; +assign o = t / 3; +endmodule +EOT + +prep -nokeepdc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 0 t:* + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +clean +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o); + always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz}; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +select -assert-count 1 t:$dff r:WIDTH=5 %i +select -assert-count 1 t:$mux r:WIDTH=5 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i; +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +wreduce +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 2 t:$mux +select -assert-count 2 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog <<EOT +module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) begin + if (ce) o <= i; + if (!rstn) o <= 4'b1111; + end +endmodule +EOT + +proc +equiv_opt -assert peepopt +design -load postopt +wreduce +select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 2 t:$mux +select -assert-count 2 t:$mux r:WIDTH=2 %i +select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys index 0e5fe882b..16e5f40e1 100644 --- a/tests/various/shregmap.ys +++ b/tests/various/shregmap.ys @@ -31,36 +31,3 @@ sat -verify -prove-asserts -show-ports -seq 5 miter #design -load gate #stat - -########## - -design -load read -design -copy-to model $__XILINX_SHREG_ -hierarchy -top shregmap_variable_test -prep -design -save gold - -simplemap t:$dff t:$dffe -shregmap -tech xilinx - -#stat -# show -width -# write_verilog -noexpr -norename -select -assert-count 1 t:$_DFF_P_ -select -assert-count 2 t:$__XILINX_SHREG_ - -design -stash gate - -design -import gold -as gold -design -import gate -as gate -design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ -prep - -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -show-ports -seq 5 miter - -# design -load gold -# stat - -# design -load gate -# stat diff --git a/tests/xilinx/.gitignore b/tests/xilinx/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/xilinx/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/xilinx/pmgen_xilinx_srl.ys b/tests/xilinx/pmgen_xilinx_srl.ys new file mode 100644 index 000000000..ea2f20487 --- /dev/null +++ b/tests/xilinx/pmgen_xilinx_srl.ys @@ -0,0 +1,57 @@ +read_verilog -icells <<EOT +module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO); + parameter DEPTH = 1; + parameter [DEPTH-1:0] INIT = 0; + parameter CLKPOL = 1; + parameter ENPOL = 2; + + wire pos_clk = C == CLKPOL; + reg pos_en; + always @(E) + if (ENPOL == 2) pos_en = 1'b1; + else pos_en = (E == ENPOL[0]); + + reg [DEPTH-1:0] r; + always @(posedge pos_clk) + if (pos_en) + r <= {r[DEPTH-2:0], D}; + + assign Q = r[L]; + assign SO = r[DEPTH-1]; +endmodule +EOT +read_verilog +/xilinx/cells_sim.v +proc +design -save model + +test_pmgen -generate xilinx_srl.fixed +hierarchy -top pmtest_xilinx_srl_pm_fixed +flatten; opt_clean + +design -save gold +xilinx_srl -fixed +techmap -autoproc -map %model +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 + +design -load model + +test_pmgen -generate xilinx_srl.variable +hierarchy -top pmtest_xilinx_srl_pm_variable +flatten; opt_clean + +design -save gold +xilinx_srl -variable +techmap -autoproc -map %model +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/xilinx/run-test.sh b/tests/xilinx/run-test.sh new file mode 100755 index 000000000..ea56b70f0 --- /dev/null +++ b/tests/xilinx/run-test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +set -e +{ +echo "all::" +for x in *.ys; do + echo "all:: run-$x" + echo "run-$x:" + echo " @echo 'Running $x..'" + echo " @../../yosys -ql ${x%.ys}.log $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/xilinx/xilinx_srl.v b/tests/xilinx/xilinx_srl.v new file mode 100644 index 000000000..bc2a15ab2 --- /dev/null +++ b/tests/xilinx/xilinx_srl.v @@ -0,0 +1,40 @@ +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 + +module xilinx_srl_variable_test(input i, clk, input [1:0] l1, l2, 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[l2], shift1[l1]}; +endmodule + +module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q); +parameter CLKPOL = 1; +parameter ENPOL = 1; +parameter DEPTH = 1; +parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}}; +reg [DEPTH-1:0] r = INIT; +wire clk = C ^ CLKPOL; +always @(posedge C) + if (E) + r <= { r[DEPTH-2:0], D }; +assign Q = r[L]; +endmodule diff --git a/tests/xilinx/xilinx_srl.ys b/tests/xilinx/xilinx_srl.ys new file mode 100644 index 000000000..b8df0e55a --- /dev/null +++ b/tests/xilinx/xilinx_srl.ys @@ -0,0 +1,67 @@ +read_verilog xilinx_srl.v +design -save read + +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_static_test +prep +design -save gold + +techmap +xilinx_srl -fixed +opt + +# stat +# show -width +select -assert-count 1 t:$_DFF_P_ +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +dump gate +sat -verify -prove-asserts -show-ports -seq 5 miter + +#design -load gold +#stat + +#design -load gate +#stat + +########## + +design -load read +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_variable_test +prep +design -save gold + +xilinx_srl -variable +opt + +#stat +# show -width +# write_verilog -noexpr -norename +select -assert-count 1 t:$dff +select -assert-count 1 t:$dff r:WIDTH=1 %i +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -seq 5 miter + +# design -load gold +# stat + +# design -load gate +# stat |