Added tests for ql-qlf plugin with PP3 architecture Signed-off-by: Maciej Kurc <mkurc@antmicro.com>
diff --git a/ql-qlf-plugin/tests/.gitignore b/ql-qlf-plugin/tests/.gitignore new file mode 100644 index 0000000..9766475 --- /dev/null +++ b/ql-qlf-plugin/tests/.gitignore
@@ -0,0 +1 @@ +ok
diff --git a/ql-qlf-plugin/tests/Makefile b/ql-qlf-plugin/tests/Makefile index 3377ef7..525750d 100644 --- a/ql-qlf-plugin/tests/Makefile +++ b/ql-qlf-plugin/tests/Makefile
@@ -8,17 +8,22 @@ # The bram test will be enable in a future PR after it's been fixed. -TESTS = dffs \ +TESTS = consts \ + dffs \ latches \ shreg \ iob_no_flatten \ full_adder \ mac_unit \ multiplier \ - logic + logic \ + mux \ + tribuf \ + fsm include $(shell pwd)/../../Makefile_test.common +consts_verify = true dffs_verify = true shreg_verify = true iob_no_flatten_verify = true @@ -27,3 +32,6 @@ mac_unit_verify = true multiplier_verify = true logic_verify = true +mux_verify = true +tribuf_verify = true +fsm_verify = true
diff --git a/ql-qlf-plugin/tests/consts/consts.tcl b/ql-qlf-plugin/tests/consts/consts.tcl new file mode 100644 index 0000000..71ca0ad --- /dev/null +++ b/ql-qlf-plugin/tests/consts/consts.tcl
@@ -0,0 +1,14 @@ +yosys -import +if { [info procs synth_quicklogic] == {} } { plugin -i ql-qlf } +yosys -import ;# ingest plugin commands + +read_verilog $::env(DESIGN_TOP).v + +synth_quicklogic -top my_top -family pp3 +stat +yosys cd my_top +select -assert-count 1 t:my_lut +select -assert-count 1 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1
diff --git a/ql-qlf-plugin/tests/consts/consts.v b/ql-qlf-plugin/tests/consts/consts.v new file mode 100644 index 0000000..2e305ce --- /dev/null +++ b/ql-qlf-plugin/tests/consts/consts.v
@@ -0,0 +1,27 @@ +(* keep_hierarchy *) +module my_lut ( + input wire [3:0] i, + output wire o +); + + LUT4 #(.INIT(16'hAAAA)) my_lut ( + .I0 (i[0]), + .I1 (i[1]), + .I2 (i[2]), + .I3 (1'bx), + .O (o) + ); + +endmodule + +module my_top ( + input wire i, + output wire o +); + + my_lut my_lut ( + .i ({1'b0, 1'b1, i}), + .o (o) + ); + +endmodule
diff --git a/ql-qlf-plugin/tests/dffs/dffs.tcl b/ql-qlf-plugin/tests/dffs/dffs.tcl index 737acc1..9b1941c 100644 --- a/ql-qlf-plugin/tests/dffs/dffs.tcl +++ b/ql-qlf-plugin/tests/dffs/dffs.tcl
@@ -402,3 +402,109 @@ stat select -assert-count 1 t:dffsre select -assert-count 3 t:\$lut + +design -reset + +# DFF on pp3 device +read_verilog $::env(DESIGN_TOP).v +design -save read + +# DFF +hierarchy -top my_dff +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dff +design -load postopt +yosys cd my_dff +stat +select -assert-count 1 t:dffepc +select -assert-count 1 t:ckpad +select -assert-count 1 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 + +# DFFE +design -load read +hierarchy -top my_dffe +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dffe +design -load postopt +yosys cd my_dffe +stat +select -assert-count 1 t:dffepc +select -assert-count 1 t:ckpad +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:logic_0 + +# ADFF a.k.a. DFFR_P +design -load read +hierarchy -top my_dffr_p +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dffr_p +design -load postopt +yosys cd my_dffr_p +stat +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 1 t:inpad +select -assert-count 1 t:outpad +select -assert-count 2 t:ckpad + +select -assert-none t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + +# ADFFN a.k.a. DFFR_N +design -load read +hierarchy -top my_dffr_n +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dffr_n +design -load postopt +yosys cd my_dffr_n +stat +select -assert-count 1 t:LUT1 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT1 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + +# DFFS (posedge, sync set) +design -load read +hierarchy -top my_dffs_clk_p +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dffs_clk_p +design -load postopt +yosys cd my_dffs_clk_p +stat +select -assert-count 1 t:LUT2 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D + +# DFFS (negedge, sync reset) +design -load read +hierarchy -top my_dffs_clk_n +yosys proc +equiv_opt -async2sync -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 -top my_dffs_clk_n +design -load postopt +yosys cd my_dffs_clk_n +stat +select -assert-count 1 t:LUT1 +select -assert-count 1 t:LUT2 +select -assert-count 1 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT1 t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D +
diff --git a/ql-qlf-plugin/tests/dffs/dffs.v b/ql-qlf-plugin/tests/dffs/dffs.v index 702c385..be159a1 100644 --- a/ql-qlf-plugin/tests/dffs/dffs.v +++ b/ql-qlf-plugin/tests/dffs/dffs.v
@@ -14,6 +14,15 @@ always @(posedge clk) q <= d; endmodule +module my_dffe( input d, clk, en, output reg q ); + initial begin + q = 0; + end + always @( posedge clk ) + if ( en ) + q <= d; +endmodule + module my_dffr_p ( input d, clk, @@ -413,3 +422,18 @@ else if (!clr) q <= 1'b0; else if (en) q <= d; endmodule + +module my_dffs_clk_p( input d, clk, pre, output reg q ); + initial q <= 0; + always @( posedge clk ) + if ( pre ) q <= 1'b1; + else q <= d; +endmodule + +module my_dffs_clk_n( input d, clk, clr, output reg q ); + initial q <= 0; + always @( negedge clk ) + if ( !clr ) q <= 1'b0; + else q <= d; +endmodule +
diff --git a/ql-qlf-plugin/tests/fsm/fsm.tcl b/ql-qlf-plugin/tests/fsm/fsm.tcl new file mode 100644 index 0000000..d6d72e2 --- /dev/null +++ b/ql-qlf-plugin/tests/fsm/fsm.tcl
@@ -0,0 +1,30 @@ +yosys -import +if { [info procs synth_quicklogic] == {} } { plugin -i ql-qlf } +yosys -import ;# ingest plugin commands + +read_verilog $::env(DESIGN_TOP).v +design -save read + +hierarchy -top fsm +yosys proc +flatten + +equiv_opt -run :prove -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +async2sync +miter -equiv -make_assert -flatten gold gate miter +sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter + +design -load postopt +yosys cd fsm + +select -assert-count 1 t:LUT2 +select -assert-count 9 t:LUT3 +select -assert-count 4 t:dffepc +select -assert-count 1 t:logic_0 +select -assert-count 1 t:logic_1 +select -assert-count 3 t:inpad +select -assert-count 2 t:outpad +select -assert-count 1 t:ckpad + +select -assert-none t:LUT2 t:LUT3 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D +
diff --git a/ql-qlf-plugin/tests/fsm/fsm.v b/ql-qlf-plugin/tests/fsm/fsm.v new file mode 100644 index 0000000..cf1c21a --- /dev/null +++ b/ql-qlf-plugin/tests/fsm/fsm.v
@@ -0,0 +1,51 @@ + 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; + parameter GNT0 = 3'b010; + parameter GNT1 = 3'b100; + parameter 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
diff --git a/ql-qlf-plugin/tests/full_adder/full_adder.tcl b/ql-qlf-plugin/tests/full_adder/full_adder.tcl index fbcd3ca..3093086 100644 --- a/ql-qlf-plugin/tests/full_adder/full_adder.tcl +++ b/ql-qlf-plugin/tests/full_adder/full_adder.tcl
@@ -32,3 +32,41 @@ #hierarchy -check -top subtractor #yosys proc #equiv_opt -assert -map +/quicklogic/qlf_k6n10_cells_sim.v synth_quicklogic -family qlf_k6n10 + +design -reset + +# Equivalence check for adder synthesis for pp3 +read_verilog -icells -DWIDTH=4 $::env(DESIGN_TOP).v +hierarchy -check -top full_adder +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd full_adder + +stat +select -assert-count 2 t:LUT2 +select -assert-count 6 t:LUT3 +select -assert-count 8 t:inpad +select -assert-count 5 t:outpad + +select -assert-none t:LUT2 t:LUT3 t:inpad t:outpad %% t:* %D + + +design -reset + +# Equivalence check for subtractor synthesis for pp3 +read_verilog -icells -DWIDTH=4 $::env(DESIGN_TOP).v +hierarchy -check -top subtractor +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd subtractor + +stat +select -assert-count 2 t:LUT2 +select -assert-count 6 t:LUT3 +select -assert-count 8 t:inpad +select -assert-count 5 t:outpad + +select -assert-none t:LUT2 t:LUT3 t:inpad t:outpad %% t:* %D +
diff --git a/ql-qlf-plugin/tests/latches/latches.tcl b/ql-qlf-plugin/tests/latches/latches.tcl index d5821a6..864876c 100644 --- a/ql-qlf-plugin/tests/latches/latches.tcl +++ b/ql-qlf-plugin/tests/latches/latches.tcl
@@ -45,3 +45,45 @@ #stat #select -assert-count 1 t:\$_DLATCH_P_ +# Latches for PP3 + +# LATCHP +design -load read +hierarchy -top latchp_noinit +yosys proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_quicklogic -family pp3 -top latchp_noinit +yosys cd latchp_noinit +select -assert-count 1 t:LUT3 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +# LATCHN +design -load read +hierarchy -top latchn +yosys proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_quicklogic -family pp3 -top latchn +yosys cd latchn +select -assert-count 1 t:LUT3 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +# LATCHSRE +design -load read +hierarchy -top my_latchsre +yosys proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_quicklogic -family pp3 -top my_latchsre +yosys cd my_latchsre +select -assert-count 1 t:LUT2 +select -assert-count 1 t:LUT4 +select -assert-count 5 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT2 t:LUT4 t:inpad t:outpad %% t:* %D +
diff --git a/ql-qlf-plugin/tests/logic/logic.tcl b/ql-qlf-plugin/tests/logic/logic.tcl index 8017272..6bfb7cb 100644 --- a/ql-qlf-plugin/tests/logic/logic.tcl +++ b/ql-qlf-plugin/tests/logic/logic.tcl
@@ -25,3 +25,22 @@ stat select -assert-count 9 t:\$lut + +design -reset + +#Logic test for pp3 device +read_verilog $::env(DESIGN_TOP).v +hierarchy -top top +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd top + +stat +select -assert-count 1 t:LUT1 +select -assert-count 6 t:LUT2 +select -assert-count 2 t:LUT3 +select -assert-count 8 t:inpad +select -assert-count 10 t:outpad + +select -assert-none t:LUT1 t:LUT2 t:LUT3 t:inpad t:outpad %% t:* %D
diff --git a/ql-qlf-plugin/tests/mux/mux.tcl b/ql-qlf-plugin/tests/mux/mux.tcl new file mode 100644 index 0000000..260e242 --- /dev/null +++ b/ql-qlf-plugin/tests/mux/mux.tcl
@@ -0,0 +1,56 @@ +yosys -import +if { [info procs synth_quicklogic] == {} } { plugin -i ql-qlf } +yosys -import ;# ingest plugin commands + +read_verilog $::env(DESIGN_TOP).v +design -save read + +hierarchy -top mux2 +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd mux2 +select -assert-count 1 t:LUT3 +select -assert-count 3 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux4 +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd mux4 +select -assert-count 3 t:LUT3 +select -assert-count 6 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux8 +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd mux8 +select -assert-count 1 t:LUT1 +select -assert-count 1 t:LUT3 +select -assert-count 2 t:mux4x0 +select -assert-count 11 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT1 t:LUT3 t:mux4x0 t:inpad t:outpad %% t:* %D + +design -load read +hierarchy -top mux16 +yosys proc +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v synth_quicklogic -family pp3 +design -load postopt +yosys cd mux16 +select -assert-count 1 t:LUT3 +select -assert-count 2 t:mux8x0 +select -assert-count 20 t:inpad +select -assert-count 1 t:outpad + +select -assert-none t:LUT3 t:mux8x0 t:inpad t:outpad %% t:* %D
diff --git a/ql-qlf-plugin/tests/mux/mux.v b/ql-qlf-plugin/tests/mux/mux.v new file mode 100644 index 0000000..d7698fc --- /dev/null +++ b/ql-qlf-plugin/tests/mux/mux.v
@@ -0,0 +1,61 @@ +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 +
diff --git a/ql-qlf-plugin/tests/tribuf/tribuf.tcl b/ql-qlf-plugin/tests/tribuf/tribuf.tcl new file mode 100644 index 0000000..067e7fd --- /dev/null +++ b/ql-qlf-plugin/tests/tribuf/tribuf.tcl
@@ -0,0 +1,19 @@ +yosys -import +if { [info procs synth_quicklogic] == {} } { plugin -i ql-qlf } +yosys -import ;# ingest plugin commands + +read_verilog $::env(DESIGN_TOP).v + +hierarchy -top tristate +yosys proc +tribuf +flatten +synth +equiv_opt -assert -map +/quicklogic/pp3_cells_sim.v -map +/simcells.v synth_quicklogic -family pp3 +design -load postopt +yosys cd tristate +select -assert-count 2 t:inpad +select -assert-count 1 t:outpad +select -assert-count 1 t:\$_TBUF_ +select -assert-none t:inpad t:outpad t:\$_TBUF_ %% t:* %D +
diff --git a/ql-qlf-plugin/tests/tribuf/tribuf.v b/ql-qlf-plugin/tests/tribuf/tribuf.v new file mode 100644 index 0000000..e4b6f81 --- /dev/null +++ b/ql-qlf-plugin/tests/tribuf/tribuf.v
@@ -0,0 +1,9 @@ +module tristate(en, i, o); + input en; + input i; + output reg o; + + always @(en or i) + o <= (en)? i : 1'bZ; +endmodule +