Add new tests for Anlogic architecture

Problems/questions:
	- memory.ys: ERROR: Failed to import cell gate.mem.0.0.0 (type
EG_LOGIC_DRAM16X4) to SAT database.
		Why EG_LOGIC_DRAM16X4, not AL_LOGIC_BRAM?
	- Internal cell type $_TBUF_  is present.
This commit is contained in:
SergeyDegtyar 2019-09-23 12:12:02 +03:00
parent 7e8f7f4c59
commit 27377c4663
23 changed files with 536 additions and 0 deletions

View File

@ -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 ""

4
tests/anlogic/.gitignore vendored Normal file
View File

@ -0,0 +1,4 @@
*.log
/run-test.mk
+*_synth.v
+*_testbench

13
tests/anlogic/add_sub.v Normal file
View File

@ -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

9
tests/anlogic/add_sub.ys Normal file
View File

@ -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

19
tests/anlogic/alu.v Normal file
View File

@ -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

17
tests/anlogic/alu.ys Normal file
View File

@ -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

17
tests/anlogic/counter.v Normal file
View File

@ -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

11
tests/anlogic/counter.ys Normal file
View File

@ -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

37
tests/anlogic/dffs.v Normal file
View File

@ -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

10
tests/anlogic/dffs.ys Normal file
View File

@ -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

73
tests/anlogic/fsm.v Normal file
View File

@ -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

14
tests/anlogic/fsm.ys Normal file
View File

@ -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

58
tests/anlogic/latches.v Normal file
View File

@ -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

16
tests/anlogic/latches.ys Normal file
View File

@ -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

21
tests/anlogic/memory.v Normal file
View File

@ -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

21
tests/anlogic/memory.ys Normal file
View File

@ -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

100
tests/anlogic/mux.v Normal file
View File

@ -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

12
tests/anlogic/mux.ys Normal file
View File

@ -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

20
tests/anlogic/run-test.sh Executable file
View File

@ -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

22
tests/anlogic/shifter.v Normal file
View File

@ -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

9
tests/anlogic/shifter.ys Normal file
View File

@ -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

23
tests/anlogic/tribuf.v Normal file
View File

@ -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

9
tests/anlogic/tribuf.ys Normal file
View File

@ -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