From 1070f2e90b9ba37856932189ef09a0f2316d9a21 Mon Sep 17 00:00:00 2001 From: SergeyDegtyar Date: Mon, 23 Sep 2019 15:51:41 +0300 Subject: Add new tests for Efinix architecture. Problems/questions: - fsm.ys. equiv_opt -assert failed because of unproven cells; - latches.ys,tribuf.ys - internal cells present; - memory.ys - sat called with -verify and proof did fail. --- Makefile | 1 + tests/efinix/.gitignore | 3 ++ tests/efinix/add_sub.v | 13 ++++++ tests/efinix/add_sub.ys | 9 +++++ tests/efinix/adffs.v | 87 +++++++++++++++++++++++++++++++++++++++++ tests/efinix/adffs.ys | 12 ++++++ tests/efinix/alu.v | 19 +++++++++ tests/efinix/alu.ys | 13 ++++++ tests/efinix/counter.v | 17 ++++++++ tests/efinix/counter.ys | 12 ++++++ tests/efinix/dffs.v | 37 ++++++++++++++++++ tests/efinix/dffs.ys | 12 ++++++ tests/efinix/div_mod.v | 13 ++++++ tests/efinix/div_mod.ys | 10 +++++ tests/efinix/fsm.v | 73 ++++++++++++++++++++++++++++++++++ tests/efinix/fsm.ys | 14 +++++++ tests/efinix/latches.v | 58 +++++++++++++++++++++++++++ tests/efinix/latches.ys | 20 ++++++++++ tests/efinix/logic.v | 18 +++++++++ tests/efinix/logic.ys | 8 ++++ tests/efinix/memory.v | 21 ++++++++++ tests/efinix/memory.ys | 18 +++++++++ tests/efinix/mul.v | 11 ++++++ tests/efinix/mul.ys | 9 +++++ tests/efinix/mux.v | 100 +++++++++++++++++++++++++++++++++++++++++++++++ tests/efinix/mux.ys | 8 ++++ tests/efinix/run-test.sh | 20 ++++++++++ tests/efinix/shifter.v | 22 +++++++++++ tests/efinix/shifter.ys | 11 ++++++ tests/efinix/tribuf.v | 29 ++++++++++++++ tests/efinix/tribuf.ys | 12 ++++++ 31 files changed, 710 insertions(+) create mode 100644 tests/efinix/.gitignore create mode 100644 tests/efinix/add_sub.v create mode 100644 tests/efinix/add_sub.ys create mode 100644 tests/efinix/adffs.v create mode 100644 tests/efinix/adffs.ys create mode 100644 tests/efinix/alu.v create mode 100644 tests/efinix/alu.ys create mode 100644 tests/efinix/counter.v create mode 100644 tests/efinix/counter.ys create mode 100644 tests/efinix/dffs.v create mode 100644 tests/efinix/dffs.ys create mode 100644 tests/efinix/div_mod.v create mode 100644 tests/efinix/div_mod.ys create mode 100644 tests/efinix/fsm.v create mode 100644 tests/efinix/fsm.ys create mode 100644 tests/efinix/latches.v create mode 100644 tests/efinix/latches.ys create mode 100644 tests/efinix/logic.v create mode 100644 tests/efinix/logic.ys create mode 100644 tests/efinix/memory.v create mode 100644 tests/efinix/memory.ys create mode 100644 tests/efinix/mul.v create mode 100644 tests/efinix/mul.ys create mode 100644 tests/efinix/mux.v create mode 100644 tests/efinix/mux.ys create mode 100755 tests/efinix/run-test.sh create mode 100644 tests/efinix/shifter.v create mode 100644 tests/efinix/shifter.ys create mode 100644 tests/efinix/tribuf.v create mode 100644 tests/efinix/tribuf.ys diff --git a/Makefile b/Makefile index 2cac80f0f..1be01a86c 100644 --- a/Makefile +++ b/Makefile @@ -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/efinix && bash run-test.sh $(SEEDOPT) @echo "" @echo " Passed \"make test\"." @echo "" diff --git a/tests/efinix/.gitignore b/tests/efinix/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/efinix/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/efinix/add_sub.v b/tests/efinix/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/efinix/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/efinix/add_sub.ys b/tests/efinix/add_sub.ys new file mode 100644 index 000000000..67fa9f2e7 --- /dev/null +++ b/tests/efinix/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog add_sub.v +hierarchy -top top +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_ADD +select -assert-count 4 t:EFX_LUT4 +select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D + diff --git a/tests/efinix/adffs.v b/tests/efinix/adffs.v new file mode 100644 index 000000000..05e68caf7 --- /dev/null +++ b/tests/efinix/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 ) + 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 ) + if ( !clr ) + q <= 1'b0; + 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/efinix/adffs.ys b/tests/efinix/adffs.ys new file mode 100644 index 000000000..642faa76b --- /dev/null +++ b/tests/efinix/adffs.ys @@ -0,0 +1,12 @@ +read_verilog adffs.v +proc +#async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock +flatten +equiv_opt -multiclock -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 4 t:EFX_FF +select -assert-count 2 t:EFX_LUT4 +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/alu.v b/tests/efinix/alu.v new file mode 100644 index 000000000..f82cc2e21 --- /dev/null +++ b/tests/efinix/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/efinix/alu.ys b/tests/efinix/alu.ys new file mode 100644 index 000000000..0d58a7c8a --- /dev/null +++ b/tests/efinix/alu.ys @@ -0,0 +1,13 @@ +read_verilog alu.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_ADD +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 32 t:EFX_FF +select -assert-count 605 t:EFX_LUT4 +select -assert-none t:EFX_ADD t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/counter.v b/tests/efinix/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/efinix/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/efinix/counter.ys b/tests/efinix/counter.ys new file mode 100644 index 000000000..82e61d39b --- /dev/null +++ b/tests/efinix/counter.ys @@ -0,0 +1,12 @@ +read_verilog counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 8 t:EFX_FF +select -assert-count 9 t:EFX_ADD +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_ADD %% t:* %D diff --git a/tests/efinix/dffs.v b/tests/efinix/dffs.v new file mode 100644 index 000000000..d97840c43 --- /dev/null +++ b/tests/efinix/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/efinix/dffs.ys b/tests/efinix/dffs.ys new file mode 100644 index 000000000..557dfd3d0 --- /dev/null +++ b/tests/efinix/dffs.ys @@ -0,0 +1,12 @@ +read_verilog dffs.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 2 t:EFX_FF +select -assert-count 1 t:EFX_LUT4 +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/div_mod.v b/tests/efinix/div_mod.v new file mode 100644 index 000000000..64a36707d --- /dev/null +++ b/tests/efinix/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/efinix/div_mod.ys b/tests/efinix/div_mod.ys new file mode 100644 index 000000000..3b6f2f0f4 --- /dev/null +++ b/tests/efinix/div_mod.ys @@ -0,0 +1,10 @@ +read_verilog div_mod.v +hierarchy -top top +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 95 t:EFX_ADD +select -assert-count 114 t:EFX_LUT4 +select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/fsm.v b/tests/efinix/fsm.v new file mode 100644 index 000000000..0605bd102 --- /dev/null +++ b/tests/efinix/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/efinix/fsm.ys b/tests/efinix/fsm.ys new file mode 100644 index 000000000..9de6aa280 --- /dev/null +++ b/tests/efinix/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 +/efinix/cells_sim.v synth_efinix # equivalency check +equiv_opt -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 6 t:EFX_FF +select -assert-count 15 t:EFX_LUT4 +select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/latches.v b/tests/efinix/latches.v new file mode 100644 index 000000000..9dc43e4c2 --- /dev/null +++ b/tests/efinix/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/efinix/latches.ys b/tests/efinix/latches.ys new file mode 100644 index 000000000..2867ec93e --- /dev/null +++ b/tests/efinix/latches.ys @@ -0,0 +1,20 @@ +read_verilog latches.v +design -save read + +proc +async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock +flatten +synth_efinix +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) + +design -load read + +synth_efinix +flatten +cd top +#Internall cell type $_DLATCH_P_. Should be realized by using LUTs. +#The same result by using just synth_efinix. +select -assert-count 3 t:$_DLATCH_P_ +select -assert-count 3 t:EFX_LUT4 +select -assert-none t:$_DLATCH_P_ t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/logic.v b/tests/efinix/logic.v new file mode 100644 index 000000000..e5343cae0 --- /dev/null +++ b/tests/efinix/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/efinix/logic.ys b/tests/efinix/logic.ys new file mode 100644 index 000000000..c2a7f5169 --- /dev/null +++ b/tests/efinix/logic.ys @@ -0,0 +1,8 @@ +read_verilog logic.v +hierarchy -top top +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_LUT4 +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/memory.v b/tests/efinix/memory.v new file mode 100644 index 000000000..5634d6507 --- /dev/null +++ b/tests/efinix/memory.v @@ -0,0 +1,21 @@ +module top +( + input [7:0] data_a, + input [8: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/efinix/memory.ys b/tests/efinix/memory.ys new file mode 100644 index 000000000..fe24b0a9b --- /dev/null +++ b/tests/efinix/memory.ys @@ -0,0 +1,18 @@ +read_verilog memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/efinix/cells_sim.v synth_efinix +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +#ERROR: Called with -verify and proof did fail! +#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter +sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_RAM_5K +select -assert-none t:EFX_GBUFCE t:EFX_RAM_5K %% t:* %D diff --git a/tests/efinix/mul.v b/tests/efinix/mul.v new file mode 100644 index 000000000..0f1618698 --- /dev/null +++ b/tests/efinix/mul.v @@ -0,0 +1,11 @@ +module top +( + input [7:0] x, + input [7:0] y, + + output [15:0] A, + ); + +assign A = x * y; + +endmodule diff --git a/tests/efinix/mul.ys b/tests/efinix/mul.ys new file mode 100644 index 000000000..7d349f3f8 --- /dev/null +++ b/tests/efinix/mul.ys @@ -0,0 +1,9 @@ +read_verilog mul.v +hierarchy -top top +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 17 t:EFX_ADD +select -assert-count 149 t:EFX_LUT4 +select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/mux.v b/tests/efinix/mux.v new file mode 100644 index 000000000..0814b733e --- /dev/null +++ b/tests/efinix/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/efinix/mux.ys b/tests/efinix/mux.ys new file mode 100644 index 000000000..a2d653568 --- /dev/null +++ b/tests/efinix/mux.ys @@ -0,0 +1,8 @@ +read_verilog mux.v +proc +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 13 t:EFX_LUT4 +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/run-test.sh b/tests/efinix/run-test.sh new file mode 100755 index 000000000..ea56b70f0 --- /dev/null +++ b/tests/efinix/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/efinix/shifter.v b/tests/efinix/shifter.v new file mode 100644 index 000000000..c55632552 --- /dev/null +++ b/tests/efinix/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/efinix/shifter.ys b/tests/efinix/shifter.ys new file mode 100644 index 000000000..1a6b5565c --- /dev/null +++ b/tests/efinix/shifter.ys @@ -0,0 +1,11 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_GBUFCE +select -assert-count 8 t:EFX_FF +select -assert-none t:EFX_GBUFCE t:EFX_FF %% t:* %D diff --git a/tests/efinix/tribuf.v b/tests/efinix/tribuf.v new file mode 100644 index 000000000..3fa6eb6c6 --- /dev/null +++ b/tests/efinix/tribuf.v @@ -0,0 +1,29 @@ +module tristate (en, i, o); + input en; + input i; + output reg o; +`ifndef BUG + + always @(en or i) + o <= (en)? i : 1'bZ; +`else + + always @(en or i) + o <= (en)? ~i : 1'bZ; +`endif +endmodule + + +module top ( +input en, +input a, +output b +); + +tristate u_tri ( + .en (en ), + .i (a ), + .o (b ) + ); + +endmodule diff --git a/tests/efinix/tribuf.ys b/tests/efinix/tribuf.ys new file mode 100644 index 000000000..20d4f215d --- /dev/null +++ b/tests/efinix/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog tribuf.v +hierarchy -top top +proc +tribuf +flatten +synth +equiv_opt -assert -map +/efinix/cells_sim.v -map +/simcells.v synth_efinix # 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 +#Internal cell type used. Need support it. +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D -- cgit v1.2.3 From eb750670e3835a1bad36cb604e04bf4836cc7f91 Mon Sep 17 00:00:00 2001 From: Sergey <37293587+SergeyDegtyar@users.noreply.github.com> Date: Tue, 1 Oct 2019 11:14:12 +0300 Subject: run-test.sh Move $x at end of line. --- tests/efinix/run-test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/efinix/run-test.sh b/tests/efinix/run-test.sh index ea56b70f0..46716f9a0 100755 --- a/tests/efinix/run-test.sh +++ b/tests/efinix/run-test.sh @@ -6,7 +6,7 @@ for x in *.ys; do echo "all:: run-$x" echo "run-$x:" echo " @echo 'Running $x..'" - echo " @../../yosys -ql ${x%.ys}.log $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 -- cgit v1.2.3 From f94dc2c072572f5b4316cb26415e7a3a4183c362 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 12:41:41 +0200 Subject: Remove not needed tests --- tests/efinix/alu.v | 19 ------------------- tests/efinix/alu.ys | 13 ------------- tests/efinix/div_mod.v | 13 ------------- tests/efinix/div_mod.ys | 10 ---------- tests/efinix/mul.v | 11 ----------- tests/efinix/mul.ys | 9 --------- 6 files changed, 75 deletions(-) delete mode 100644 tests/efinix/alu.v delete mode 100644 tests/efinix/alu.ys delete mode 100644 tests/efinix/div_mod.v delete mode 100644 tests/efinix/div_mod.ys delete mode 100644 tests/efinix/mul.v delete mode 100644 tests/efinix/mul.ys diff --git a/tests/efinix/alu.v b/tests/efinix/alu.v deleted file mode 100644 index f82cc2e21..000000000 --- a/tests/efinix/alu.v +++ /dev/null @@ -1,19 +0,0 @@ -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/efinix/alu.ys b/tests/efinix/alu.ys deleted file mode 100644 index 0d58a7c8a..000000000 --- a/tests/efinix/alu.ys +++ /dev/null @@ -1,13 +0,0 @@ -read_verilog alu.v -hierarchy -top top -proc -flatten -equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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:EFX_ADD -select -assert-count 1 t:EFX_GBUFCE -select -assert-count 32 t:EFX_FF -select -assert-count 605 t:EFX_LUT4 -select -assert-none t:EFX_ADD t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/div_mod.v b/tests/efinix/div_mod.v deleted file mode 100644 index 64a36707d..000000000 --- a/tests/efinix/div_mod.v +++ /dev/null @@ -1,13 +0,0 @@ -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/efinix/div_mod.ys b/tests/efinix/div_mod.ys deleted file mode 100644 index 3b6f2f0f4..000000000 --- a/tests/efinix/div_mod.ys +++ /dev/null @@ -1,10 +0,0 @@ -read_verilog div_mod.v -hierarchy -top top -flatten -equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 95 t:EFX_ADD -select -assert-count 114 t:EFX_LUT4 -select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D diff --git a/tests/efinix/mul.v b/tests/efinix/mul.v deleted file mode 100644 index 0f1618698..000000000 --- a/tests/efinix/mul.v +++ /dev/null @@ -1,11 +0,0 @@ -module top -( - input [7:0] x, - input [7:0] y, - - output [15:0] A, - ); - -assign A = x * y; - -endmodule diff --git a/tests/efinix/mul.ys b/tests/efinix/mul.ys deleted file mode 100644 index 7d349f3f8..000000000 --- a/tests/efinix/mul.ys +++ /dev/null @@ -1,9 +0,0 @@ -read_verilog mul.v -hierarchy -top top -equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 17 t:EFX_ADD -select -assert-count 149 t:EFX_LUT4 -select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D -- cgit v1.2.3 From 286a2728729a6cf4b65afec6dbe65d269f1a5ca6 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 12:42:06 +0200 Subject: Cleaned tests --- tests/efinix/fsm.v | 18 ------------------ tests/efinix/fsm.ys | 4 ++-- tests/efinix/shifter.v | 6 ------ tests/efinix/tribuf.v | 21 --------------------- tests/efinix/tribuf.ys | 4 ++-- 5 files changed, 4 insertions(+), 49 deletions(-) diff --git a/tests/efinix/fsm.v b/tests/efinix/fsm.v index 0605bd102..368fbaace 100644 --- a/tests/efinix/fsm.v +++ b/tests/efinix/fsm.v @@ -52,22 +52,4 @@ 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/efinix/fsm.ys b/tests/efinix/fsm.ys index 9de6aa280..2ec75215d 100644 --- a/tests/efinix/fsm.ys +++ b/tests/efinix/fsm.ys @@ -1,12 +1,12 @@ read_verilog fsm.v -hierarchy -top top +hierarchy -top fsm proc flatten #ERROR: Found 4 unproven $equiv cells in 'equiv_status -assert'. #equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check equiv_opt -map +/efinix/cells_sim.v synth_efinix # 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 +cd fsm # Constrain all select calls below inside the top module select -assert-count 1 t:EFX_GBUFCE select -assert-count 6 t:EFX_FF diff --git a/tests/efinix/shifter.v b/tests/efinix/shifter.v index c55632552..ce2c81dd2 100644 --- a/tests/efinix/shifter.v +++ b/tests/efinix/shifter.v @@ -9,14 +9,8 @@ in 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/efinix/tribuf.v b/tests/efinix/tribuf.v index 3fa6eb6c6..c64468253 100644 --- a/tests/efinix/tribuf.v +++ b/tests/efinix/tribuf.v @@ -2,28 +2,7 @@ module tristate (en, i, o); input en; input i; output reg o; -`ifndef BUG always @(en or i) o <= (en)? i : 1'bZ; -`else - - always @(en or i) - o <= (en)? ~i : 1'bZ; -`endif -endmodule - - -module top ( -input en, -input a, -output b -); - -tristate u_tri ( - .en (en ), - .i (a ), - .o (b ) - ); - endmodule diff --git a/tests/efinix/tribuf.ys b/tests/efinix/tribuf.ys index 20d4f215d..2e2ab9e65 100644 --- a/tests/efinix/tribuf.ys +++ b/tests/efinix/tribuf.ys @@ -1,12 +1,12 @@ read_verilog tribuf.v -hierarchy -top top +hierarchy -top tristate proc tribuf flatten synth equiv_opt -assert -map +/efinix/cells_sim.v -map +/simcells.v synth_efinix # 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 +cd tristate # Constrain all select calls below inside the top module #Internal cell type used. Need support it. select -assert-count 1 t:$_TBUF_ select -assert-none t:$_TBUF_ %% t:* %D -- cgit v1.2.3 From 3de7889d08d0b02f1af6b9027b6e753eb0f6f490 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 12:48:27 +0200 Subject: Separate check for ff's types --- tests/efinix/adffs.v | 40 ------------------------------------- tests/efinix/adffs.ys | 55 ++++++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 48 insertions(+), 47 deletions(-) diff --git a/tests/efinix/adffs.v b/tests/efinix/adffs.v index 05e68caf7..223b52d21 100644 --- a/tests/efinix/adffs.v +++ b/tests/efinix/adffs.v @@ -45,43 +45,3 @@ module ndffnr 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/efinix/adffs.ys b/tests/efinix/adffs.ys index 642faa76b..d0be205d5 100644 --- a/tests/efinix/adffs.ys +++ b/tests/efinix/adffs.ys @@ -1,12 +1,53 @@ read_verilog adffs.v +design -save read + proc -#async2sync # converts async flops to a 'sync' variant clocked by a 'super'-clock -flatten -equiv_opt -multiclock -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +hierarchy -top adff +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 +cd adff # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF +select -assert-count 1 t:EFX_GBUFCE + +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + +design -load read +proc +hierarchy -top adffn +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE -select -assert-count 4 t:EFX_FF -select -assert-count 2 t:EFX_LUT4 -select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D + +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + + +design -load read +proc +hierarchy -top dffs +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffs # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D + + +design -load read +proc +hierarchy -top ndffnr +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF +select -assert-count 1 t:EFX_GBUFCE + +select -assert-count 1 t:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D -- cgit v1.2.3 From 2c3e14024637bed14d8e8142f4d05c471630dbf7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 12:51:45 +0200 Subject: split rest od ff's --- tests/efinix/adffs.ys | 3 --- tests/efinix/dffs.v | 22 ---------------------- tests/efinix/dffs.ys | 22 +++++++++++++++++----- 3 files changed, 17 insertions(+), 30 deletions(-) diff --git a/tests/efinix/adffs.ys b/tests/efinix/adffs.ys index d0be205d5..3471a0a80 100644 --- a/tests/efinix/adffs.ys +++ b/tests/efinix/adffs.ys @@ -43,9 +43,6 @@ hierarchy -top ndffnr equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd ndffnr # Constrain all select calls below inside the top module -select -assert-count 1 t:EFX_FF -select -assert-count 1 t:EFX_GBUFCE - select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE select -assert-count 1 t:EFX_LUT4 diff --git a/tests/efinix/dffs.v b/tests/efinix/dffs.v index d97840c43..3418787c9 100644 --- a/tests/efinix/dffs.v +++ b/tests/efinix/dffs.v @@ -13,25 +13,3 @@ module dffe 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/efinix/dffs.ys b/tests/efinix/dffs.ys index 557dfd3d0..fe8d93123 100644 --- a/tests/efinix/dffs.ys +++ b/tests/efinix/dffs.ys @@ -1,12 +1,24 @@ read_verilog dffs.v -hierarchy -top top +design -save read + proc -flatten +hierarchy -top dff equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 +cd dff # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF +select -assert-count 1 t:EFX_GBUFCE +select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + +design -load read +proc +hierarchy -top dffe +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_FF select -assert-count 1 t:EFX_GBUFCE -select -assert-count 2 t:EFX_FF select -assert-count 1 t:EFX_LUT4 -select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D -- cgit v1.2.3 From 77d557d00b5672eb4c20fe0179c5d706abb43807 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 12:58:11 +0200 Subject: Add missing latch mapping --- techlibs/efinix/cells_map.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/techlibs/efinix/cells_map.v b/techlibs/efinix/cells_map.v index 0aeab1902..3ecec3bac 100644 --- a/techlibs/efinix/cells_map.v +++ b/techlibs/efinix/cells_map.v @@ -17,6 +17,18 @@ module \$_DFF_NP1_ (input D, C, R, output Q); EFX_FF #(.CLK_POLARITY(1'b0), .CE module \$_DFF_PP0_ (input D, C, R, output Q); EFX_FF #(.CLK_POLARITY(1'b1), .CE_POLARITY(1'b1), .SR_POLARITY(1'b1), .D_POLARITY(1'b1), .SR_SYNC(1'b0), .SR_VALUE(1'b0), .SR_SYNC_PRIORITY(1'b1)) _TECHMAP_REPLACE_ (.D(D), .CE(1'b1), .CLK(C), .SR(R), .Q(Q)); endmodule module \$_DFF_PP1_ (input D, C, R, output Q); EFX_FF #(.CLK_POLARITY(1'b1), .CE_POLARITY(1'b1), .SR_POLARITY(1'b1), .D_POLARITY(1'b1), .SR_SYNC(1'b0), .SR_VALUE(1'b1), .SR_SYNC_PRIORITY(1'b1)) _TECHMAP_REPLACE_ (.D(D), .CE(1'b1), .CLK(C), .SR(R), .Q(Q)); endmodule +module \$_DLATCH_N_ (E, D, Q); + wire [1023:0] _TECHMAP_DO_ = "simplemap; opt"; + input E, D; + output Q = !E ? D : Q; +endmodule + +module \$_DLATCH_P_ (E, D, Q); + wire [1023:0] _TECHMAP_DO_ = "simplemap; opt"; + input E, D; + output Q = E ? D : Q; +endmodule + `ifndef NO_LUT module \$lut (A, Y); parameter WIDTH = 0; -- cgit v1.2.3 From 1b80489486434a427b8043579426b575e09edc0b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 13:00:09 +0200 Subject: Split latch check --- tests/efinix/latches.v | 34 ---------------------------------- tests/efinix/latches.ys | 35 ++++++++++++++++++++++++----------- 2 files changed, 24 insertions(+), 45 deletions(-) diff --git a/tests/efinix/latches.v b/tests/efinix/latches.v index 9dc43e4c2..adb5d5319 100644 --- a/tests/efinix/latches.v +++ b/tests/efinix/latches.v @@ -22,37 +22,3 @@ module latchsr 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/efinix/latches.ys b/tests/efinix/latches.ys index 2867ec93e..f729c3bd9 100644 --- a/tests/efinix/latches.ys +++ b/tests/efinix/latches.ys @@ -2,19 +2,32 @@ read_verilog latches.v design -save read proc -async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock -flatten +hierarchy -top latchp +# Can't run any sort of equivalence check because latches are blown to LUTs synth_efinix -equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + design -load read +proc +hierarchy -top latchn +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_efinix +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +proc +hierarchy -top latchsr +# Can't run any sort of equivalence check because latches are blown to LUTs synth_efinix -flatten -cd top -#Internall cell type $_DLATCH_P_. Should be realized by using LUTs. -#The same result by using just synth_efinix. -select -assert-count 3 t:$_DLATCH_P_ -select -assert-count 3 t:EFX_LUT4 -select -assert-none t:$_DLATCH_P_ t:EFX_LUT4 %% t:* %D +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D -- cgit v1.2.3 From c0fa6f3e1a001c3cd68c4be3eac877e08fd19971 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 13:05:16 +0200 Subject: Split mux tests per type --- tests/efinix/mux.v | 35 ----------------------------------- tests/efinix/mux.ys | 39 ++++++++++++++++++++++++++++++++++++--- 2 files changed, 36 insertions(+), 38 deletions(-) diff --git a/tests/efinix/mux.v b/tests/efinix/mux.v index 0814b733e..27bc0bf0b 100644 --- a/tests/efinix/mux.v +++ b/tests/efinix/mux.v @@ -63,38 +63,3 @@ module mux16 (D, S, 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/efinix/mux.ys b/tests/efinix/mux.ys index a2d653568..efe27583d 100644 --- a/tests/efinix/mux.ys +++ b/tests/efinix/mux.ys @@ -1,8 +1,41 @@ read_verilog mux.v +design -save read + proc -flatten +hierarchy -top mux2 equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 13 t:EFX_LUT4 +cd mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +proc +hierarchy -top mux4 +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux4 # Constrain all select calls below inside the top module +select -assert-count 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +proc +hierarchy -top mux8 +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux8 # Constrain all select calls below inside the top module +select -assert-count 5 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +proc +hierarchy -top mux16 +equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux16 # Constrain all select calls below inside the top module +select -assert-count 12 t:EFX_LUT4 + select -assert-none t:EFX_LUT4 %% t:* %D -- cgit v1.2.3 From 44c3472b9f92e2db855056bff9c0e9549e4cbf3c Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 4 Oct 2019 13:27:10 +0200 Subject: FF should be initialized to 0 --- techlibs/efinix/cells_sim.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/techlibs/efinix/cells_sim.v b/techlibs/efinix/cells_sim.v index 2fc2034a6..a74d1c571 100644 --- a/techlibs/efinix/cells_sim.v +++ b/techlibs/efinix/cells_sim.v @@ -59,7 +59,9 @@ module EFX_FF( assign ce = CE_POLARITY ? CE : ~CE; assign sr = SR_POLARITY ? SR : ~SR; assign d = D_POLARITY ? D : ~D; - + + initial Q = 1'b0; + generate if (SR_SYNC == 1) begin -- cgit v1.2.3 From b659082e4a72209af62a19668800bb6334a437d7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 18 Oct 2019 09:13:06 +0200 Subject: hierarchy - proc reorder --- tests/efinix/add_sub.ys | 1 + tests/efinix/adffs.ys | 8 ++++---- tests/efinix/dffs.ys | 4 ++-- tests/efinix/latches.ys | 6 +++--- tests/efinix/logic.ys | 1 + tests/efinix/mux.ys | 8 ++++---- 6 files changed, 15 insertions(+), 13 deletions(-) diff --git a/tests/efinix/add_sub.ys b/tests/efinix/add_sub.ys index 67fa9f2e7..8bd28c68e 100644 --- a/tests/efinix/add_sub.ys +++ b/tests/efinix/add_sub.ys @@ -1,5 +1,6 @@ read_verilog add_sub.v hierarchy -top top +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 diff --git a/tests/efinix/adffs.ys b/tests/efinix/adffs.ys index 3471a0a80..791626428 100644 --- a/tests/efinix/adffs.ys +++ b/tests/efinix/adffs.ys @@ -1,8 +1,8 @@ read_verilog adffs.v design -save read -proc hierarchy -top adff +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd adff # Constrain all select calls below inside the top module @@ -13,8 +13,8 @@ select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D design -load read -proc hierarchy -top adffn +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd adffn # Constrain all select calls below inside the top module @@ -25,8 +25,8 @@ select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D design -load read -proc hierarchy -top dffs +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd dffs # Constrain all select calls below inside the top module @@ -38,8 +38,8 @@ select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top ndffnr +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd ndffnr # Constrain all select calls below inside the top module diff --git a/tests/efinix/dffs.ys b/tests/efinix/dffs.ys index fe8d93123..cdd288233 100644 --- a/tests/efinix/dffs.ys +++ b/tests/efinix/dffs.ys @@ -1,8 +1,8 @@ read_verilog dffs.v design -save read -proc hierarchy -top dff +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd dff # Constrain all select calls below inside the top module @@ -12,8 +12,8 @@ select -assert-count 1 t:EFX_GBUFCE select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D design -load read -proc hierarchy -top dffe +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd dffe # Constrain all select calls below inside the top module diff --git a/tests/efinix/latches.ys b/tests/efinix/latches.ys index f729c3bd9..899d024ce 100644 --- a/tests/efinix/latches.ys +++ b/tests/efinix/latches.ys @@ -1,8 +1,8 @@ read_verilog latches.v design -save read -proc hierarchy -top latchp +proc # Can't run any sort of equivalence check because latches are blown to LUTs synth_efinix cd latchp # Constrain all select calls below inside the top module @@ -12,8 +12,8 @@ select -assert-none t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top latchn +proc # Can't run any sort of equivalence check because latches are blown to LUTs synth_efinix cd latchn # Constrain all select calls below inside the top module @@ -23,8 +23,8 @@ select -assert-none t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top latchsr +proc # Can't run any sort of equivalence check because latches are blown to LUTs synth_efinix cd latchsr # Constrain all select calls below inside the top module diff --git a/tests/efinix/logic.ys b/tests/efinix/logic.ys index c2a7f5169..fdedb337b 100644 --- a/tests/efinix/logic.ys +++ b/tests/efinix/logic.ys @@ -1,5 +1,6 @@ read_verilog logic.v hierarchy -top top +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # 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 diff --git a/tests/efinix/mux.ys b/tests/efinix/mux.ys index efe27583d..71a9681de 100644 --- a/tests/efinix/mux.ys +++ b/tests/efinix/mux.ys @@ -1,8 +1,8 @@ read_verilog mux.v design -save read -proc hierarchy -top mux2 +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux2 # Constrain all select calls below inside the top module @@ -11,8 +11,8 @@ select -assert-count 1 t:EFX_LUT4 select -assert-none t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top mux4 +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux4 # Constrain all select calls below inside the top module @@ -21,8 +21,8 @@ select -assert-count 2 t:EFX_LUT4 select -assert-none t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top mux8 +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux8 # Constrain all select calls below inside the top module @@ -31,8 +31,8 @@ select -assert-count 5 t:EFX_LUT4 select -assert-none t:EFX_LUT4 %% t:* %D design -load read -proc hierarchy -top mux16 +proc equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux16 # Constrain all select calls below inside the top module -- cgit v1.2.3