diff options
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | tests/anlogic/.gitignore | 4 | ||||
-rw-r--r-- | tests/anlogic/add_sub.v | 13 | ||||
-rw-r--r-- | tests/anlogic/add_sub.ys | 9 | ||||
-rw-r--r-- | tests/anlogic/alu.v | 19 | ||||
-rw-r--r-- | tests/anlogic/alu.ys | 17 | ||||
-rw-r--r-- | tests/anlogic/counter.v | 17 | ||||
-rw-r--r-- | tests/anlogic/counter.ys | 11 | ||||
-rw-r--r-- | tests/anlogic/dffs.v | 37 | ||||
-rw-r--r-- | tests/anlogic/dffs.ys | 10 | ||||
-rw-r--r-- | tests/anlogic/fsm.v | 73 | ||||
-rw-r--r-- | tests/anlogic/fsm.ys | 14 | ||||
-rw-r--r-- | tests/anlogic/latches.v | 58 | ||||
-rw-r--r-- | tests/anlogic/latches.ys | 16 | ||||
-rw-r--r-- | tests/anlogic/memory.v | 21 | ||||
-rw-r--r-- | tests/anlogic/memory.ys | 21 | ||||
-rw-r--r-- | tests/anlogic/mux.v | 100 | ||||
-rw-r--r-- | tests/anlogic/mux.ys | 12 | ||||
-rwxr-xr-x | tests/anlogic/run-test.sh | 20 | ||||
-rw-r--r-- | tests/anlogic/shifter.v | 22 | ||||
-rw-r--r-- | tests/anlogic/shifter.ys | 9 | ||||
-rw-r--r-- | tests/anlogic/tribuf.v | 23 | ||||
-rw-r--r-- | tests/anlogic/tribuf.ys | 9 |
23 files changed, 536 insertions, 0 deletions
@@ -710,6 +710,7 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/aiger && bash run-test.sh $(ABCOPT) +cd tests/arch && bash run-test.sh +cd tests/ice40 && bash run-test.sh $(SEEDOPT) + +cd tests/anlogic && bash run-test.sh $(SEEDOPT) @echo "" @echo " Passed \"make test\"." @echo "" diff --git a/tests/anlogic/.gitignore b/tests/anlogic/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/anlogic/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/anlogic/add_sub.v b/tests/anlogic/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/anlogic/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/anlogic/add_sub.ys b/tests/anlogic/add_sub.ys new file mode 100644 index 000000000..55c090506 --- /dev/null +++ b/tests/anlogic/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog add_sub.v +hierarchy -top top +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 10 t:AL_MAP_ADDER +select -assert-count 4 t:AL_MAP_LUT1 +select -assert-none t:AL_MAP_LUT1 t:AL_MAP_ADDER %% t:* %D + diff --git a/tests/anlogic/alu.v b/tests/anlogic/alu.v new file mode 100644 index 000000000..f82cc2e21 --- /dev/null +++ b/tests/anlogic/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/anlogic/alu.ys b/tests/anlogic/alu.ys new file mode 100644 index 000000000..532ce82d5 --- /dev/null +++ b/tests/anlogic/alu.ys @@ -0,0 +1,17 @@ +read_verilog alu.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 66 t:AL_MAP_ADDER +select -assert-count 32 t:AL_MAP_LUT1 +select -assert-count 23 t:AL_MAP_LUT2 +select -assert-count 61 t:AL_MAP_LUT3 +select -assert-count 209 t:AL_MAP_LUT4 +select -assert-count 100 t:AL_MAP_LUT5 +select -assert-count 79 t:AL_MAP_LUT6 +select -assert-count 32 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_ADDER t:AL_MAP_LUT1 t:AL_MAP_LUT2 t:AL_MAP_LUT3 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_LUT6 t:AL_MAP_SEQ %% t:* %D diff --git a/tests/anlogic/counter.v b/tests/anlogic/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/anlogic/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/anlogic/counter.ys b/tests/anlogic/counter.ys new file mode 100644 index 000000000..5210221e3 --- /dev/null +++ b/tests/anlogic/counter.ys @@ -0,0 +1,11 @@ +read_verilog counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 9 t:AL_MAP_ADDER +select -assert-count 8 t:AL_MAP_SEQ +select -assert-none t:SB_CARRY t:AL_MAP_SEQ t:AL_MAP_ADDER %% t:* %D diff --git a/tests/anlogic/dffs.v b/tests/anlogic/dffs.v new file mode 100644 index 000000000..d97840c43 --- /dev/null +++ b/tests/anlogic/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/anlogic/dffs.ys b/tests/anlogic/dffs.ys new file mode 100644 index 000000000..a15c6f24e --- /dev/null +++ b/tests/anlogic/dffs.ys @@ -0,0 +1,10 @@ +read_verilog dffs.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 +select -assert-count 2 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D diff --git a/tests/anlogic/fsm.v b/tests/anlogic/fsm.v new file mode 100644 index 000000000..0605bd102 --- /dev/null +++ b/tests/anlogic/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/anlogic/fsm.ys b/tests/anlogic/fsm.ys new file mode 100644 index 000000000..6eb7b9a71 --- /dev/null +++ b/tests/anlogic/fsm.ys @@ -0,0 +1,14 @@ +read_verilog fsm.v +hierarchy -top top +proc +flatten +#ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. +#equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +equiv_opt -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # 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 diff --git a/tests/anlogic/latches.v b/tests/anlogic/latches.v new file mode 100644 index 000000000..9dc43e4c2 --- /dev/null +++ b/tests/anlogic/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/anlogic/latches.ys b/tests/anlogic/latches.ys new file mode 100644 index 000000000..b5e52cf16 --- /dev/null +++ b/tests/anlogic/latches.ys @@ -0,0 +1,16 @@ +read_verilog latches.v +design -save read + +proc +async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock +flatten +synth_anlogic +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) + +design -load read +synth_anlogic +cd top +select -assert-count 2 t:AL_MAP_LUT3 +select -assert-count 1 t:AL_MAP_LUT5 +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_LUT5 %% t:* %D diff --git a/tests/anlogic/memory.v b/tests/anlogic/memory.v new file mode 100644 index 000000000..cb7753f7b --- /dev/null +++ b/tests/anlogic/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/anlogic/memory.ys b/tests/anlogic/memory.ys new file mode 100644 index 000000000..8c0ce844e --- /dev/null +++ b/tests/anlogic/memory.ys @@ -0,0 +1,21 @@ +read_verilog memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +#ERROR: Failed to import cell gate.mem.0.0.0 (type EG_LOGIC_DRAM16X4) to SAT database. +#sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top + +select -assert-count 8 t:AL_MAP_LUT2 +select -assert-count 8 t:AL_MAP_LUT4 +select -assert-count 8 t:AL_MAP_LUT5 +select -assert-count 36 t:AL_MAP_SEQ +select -assert-count 8 t:EG_LOGIC_DRAM16X4 #Why not AL_LOGIC_BRAM? +select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_SEQ t:EG_LOGIC_DRAM16X4 %% t:* %D diff --git a/tests/anlogic/mux.v b/tests/anlogic/mux.v new file mode 100644 index 000000000..0814b733e --- /dev/null +++ b/tests/anlogic/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/anlogic/mux.ys b/tests/anlogic/mux.ys new file mode 100644 index 000000000..84a8bcccf --- /dev/null +++ b/tests/anlogic/mux.ys @@ -0,0 +1,12 @@ +read_verilog mux.v +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:AL_MAP_LUT3 +select -assert-count 4 t:AL_MAP_LUT4 +select -assert-count 4 t:AL_MAP_LUT5 +select -assert-count 1 t:AL_MAP_LUT6 +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_LUT4 t:AL_MAP_LUT5 t:AL_MAP_LUT6 %% t:* %D diff --git a/tests/anlogic/run-test.sh b/tests/anlogic/run-test.sh new file mode 100755 index 000000000..2c72ca3a9 --- /dev/null +++ b/tests/anlogic/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 -w 'Yosys has only limited support for tri-state logic at the moment.'" +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/anlogic/shifter.v b/tests/anlogic/shifter.v new file mode 100644 index 000000000..c55632552 --- /dev/null +++ b/tests/anlogic/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/anlogic/shifter.ys b/tests/anlogic/shifter.ys new file mode 100644 index 000000000..edd89b344 --- /dev/null +++ b/tests/anlogic/shifter.ys @@ -0,0 +1,9 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ %% t:* %D diff --git a/tests/anlogic/tribuf.v b/tests/anlogic/tribuf.v new file mode 100644 index 000000000..870a02584 --- /dev/null +++ b/tests/anlogic/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/anlogic/tribuf.ys b/tests/anlogic/tribuf.ys new file mode 100644 index 000000000..663e93fb2 --- /dev/null +++ b/tests/anlogic/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog tribuf.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/anlogic/cells_sim.v -map +/simcells.v synth_anlogic # 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 |