From c2ec7ca7031e2e9c655723fcdb3ce3cb83cc74b1 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 18 Oct 2019 11:06:12 +0200 Subject: Moved all tests in arch sub directory --- tests/arch/anlogic/.gitignore | 4 ++ tests/arch/anlogic/add_sub.v | 13 +++++ tests/arch/anlogic/add_sub.ys | 10 ++++ tests/arch/anlogic/counter.v | 17 ++++++ tests/arch/anlogic/counter.ys | 11 ++++ tests/arch/anlogic/dffs.v | 15 +++++ tests/arch/anlogic/dffs.ys | 20 +++++++ tests/arch/anlogic/fsm.v | 55 +++++++++++++++++++ tests/arch/anlogic/fsm.ys | 15 +++++ tests/arch/anlogic/latches.v | 24 ++++++++ tests/arch/anlogic/latches.ys | 33 +++++++++++ tests/arch/anlogic/memory.v | 21 +++++++ tests/arch/anlogic/memory.ys | 21 +++++++ tests/arch/anlogic/mux.v | 65 ++++++++++++++++++++++ tests/arch/anlogic/mux.ys | 42 ++++++++++++++ tests/arch/anlogic/run-test.sh | 20 +++++++ tests/arch/anlogic/shifter.v | 16 ++++++ tests/arch/anlogic/shifter.ys | 10 ++++ tests/arch/anlogic/tribuf.v | 8 +++ tests/arch/anlogic/tribuf.ys | 9 +++ tests/arch/ecp5/.gitignore | 2 + tests/arch/ecp5/add_sub.v | 13 +++++ tests/arch/ecp5/add_sub.ys | 9 +++ tests/arch/ecp5/adffs.v | 47 ++++++++++++++++ tests/arch/ecp5/adffs.ys | 40 ++++++++++++++ tests/arch/ecp5/counter.v | 17 ++++++ tests/arch/ecp5/counter.ys | 10 ++++ tests/arch/ecp5/dffs.v | 15 +++++ tests/arch/ecp5/dffs.ys | 19 +++++++ tests/arch/ecp5/dpram.v | 23 ++++++++ tests/arch/ecp5/dpram.ys | 18 ++++++ tests/arch/ecp5/fsm.v | 55 +++++++++++++++++++ tests/arch/ecp5/fsm.ys | 12 ++++ tests/arch/ecp5/latches.v | 24 ++++++++ tests/arch/ecp5/latches.ys | 35 ++++++++++++ tests/arch/ecp5/logic.v | 18 ++++++ tests/arch/ecp5/logic.ys | 8 +++ tests/arch/ecp5/macc.v | 25 +++++++++ tests/arch/ecp5/macc.ys | 13 +++++ tests/arch/ecp5/memory.v | 21 +++++++ tests/arch/ecp5/memory.ys | 19 +++++++ tests/arch/ecp5/mul.v | 11 ++++ tests/arch/ecp5/mul.ys | 11 ++++ tests/arch/ecp5/mux.v | 66 ++++++++++++++++++++++ tests/arch/ecp5/mux.ys | 46 ++++++++++++++++ tests/arch/ecp5/rom.v | 18 ++++++ tests/arch/ecp5/rom.ys | 10 ++++ tests/arch/ecp5/run-test.sh | 20 +++++++ tests/arch/ecp5/shifter.v | 16 ++++++ tests/arch/ecp5/shifter.ys | 10 ++++ tests/arch/ecp5/tribuf.v | 8 +++ tests/arch/ecp5/tribuf.ys | 9 +++ tests/arch/efinix/.gitignore | 3 + tests/arch/efinix/add_sub.v | 13 +++++ tests/arch/efinix/add_sub.ys | 10 ++++ tests/arch/efinix/adffs.v | 47 ++++++++++++++++ tests/arch/efinix/adffs.ys | 50 +++++++++++++++++ tests/arch/efinix/counter.v | 17 ++++++ tests/arch/efinix/counter.ys | 12 ++++ tests/arch/efinix/dffs.v | 15 +++++ tests/arch/efinix/dffs.ys | 24 ++++++++ tests/arch/efinix/fsm.v | 55 +++++++++++++++++++ tests/arch/efinix/fsm.ys | 14 +++++ tests/arch/efinix/latches.v | 24 ++++++++ tests/arch/efinix/latches.ys | 33 +++++++++++ tests/arch/efinix/logic.v | 18 ++++++ tests/arch/efinix/logic.ys | 9 +++ tests/arch/efinix/memory.v | 21 +++++++ tests/arch/efinix/memory.ys | 18 ++++++ tests/arch/efinix/mux.v | 65 ++++++++++++++++++++++ tests/arch/efinix/mux.ys | 41 ++++++++++++++ tests/arch/efinix/run-test.sh | 20 +++++++ tests/arch/efinix/shifter.v | 16 ++++++ tests/arch/efinix/shifter.ys | 11 ++++ tests/arch/efinix/tribuf.v | 8 +++ tests/arch/efinix/tribuf.ys | 12 ++++ tests/arch/ice40/.gitignore | 4 ++ tests/arch/ice40/add_sub.v | 13 +++++ tests/arch/ice40/add_sub.ys | 9 +++ tests/arch/ice40/adffs.v | 87 +++++++++++++++++++++++++++++ tests/arch/ice40/adffs.ys | 11 ++++ tests/arch/ice40/alu.v | 19 +++++++ tests/arch/ice40/alu.ys | 11 ++++ tests/arch/ice40/counter.v | 17 ++++++ tests/arch/ice40/counter.ys | 11 ++++ tests/arch/ice40/dffs.v | 37 +++++++++++++ tests/arch/ice40/dffs.ys | 10 ++++ tests/arch/ice40/div_mod.v | 13 +++++ tests/arch/ice40/div_mod.ys | 9 +++ tests/arch/ice40/dpram.v | 23 ++++++++ tests/arch/ice40/dpram.ys | 15 +++++ tests/arch/ice40/fsm.v | 73 +++++++++++++++++++++++++ tests/arch/ice40/fsm.ys | 13 +++++ tests/arch/ice40/ice40_opt.ys | 26 +++++++++ tests/arch/ice40/latches.v | 58 ++++++++++++++++++++ tests/arch/ice40/latches.ys | 12 ++++ tests/arch/ice40/logic.v | 18 ++++++ tests/arch/ice40/logic.ys | 7 +++ tests/arch/ice40/macc.v | 47 ++++++++++++++++ tests/arch/ice40/macc.ys | 25 +++++++++ tests/arch/ice40/memory.v | 21 +++++++ tests/arch/ice40/memory.ys | 15 +++++ tests/arch/ice40/mul.v | 11 ++++ tests/arch/ice40/mul.ys | 7 +++ tests/arch/ice40/mux.v | 100 ++++++++++++++++++++++++++++++++++ tests/arch/ice40/mux.ys | 8 +++ tests/arch/ice40/rom.v | 18 ++++++ tests/arch/ice40/rom.ys | 8 +++ tests/arch/ice40/run-test.sh | 20 +++++++ tests/arch/ice40/shifter.v | 22 ++++++++ tests/arch/ice40/shifter.ys | 9 +++ tests/arch/ice40/tribuf.v | 23 ++++++++ tests/arch/ice40/tribuf.ys | 9 +++ tests/arch/ice40/wrapcarry.ys | 22 ++++++++ tests/arch/xilinx/.gitignore | 5 ++ tests/arch/xilinx/add_sub.v | 13 +++++ tests/arch/xilinx/add_sub.ys | 11 ++++ tests/arch/xilinx/adffs.v | 47 ++++++++++++++++ tests/arch/xilinx/adffs.ys | 51 +++++++++++++++++ tests/arch/xilinx/counter.v | 17 ++++++ tests/arch/xilinx/counter.ys | 14 +++++ tests/arch/xilinx/dffs.v | 15 +++++ tests/arch/xilinx/dffs.ys | 25 +++++++++ tests/arch/xilinx/dsp_simd.ys | 25 +++++++++ tests/arch/xilinx/fsm.v | 55 +++++++++++++++++++ tests/arch/xilinx/fsm.ys | 14 +++++ tests/arch/xilinx/latches.v | 24 ++++++++ tests/arch/xilinx/latches.ys | 35 ++++++++++++ tests/arch/xilinx/logic.v | 18 ++++++ tests/arch/xilinx/logic.ys | 11 ++++ tests/arch/xilinx/macc.sh | 3 + tests/arch/xilinx/macc.v | 84 ++++++++++++++++++++++++++++ tests/arch/xilinx/macc.ys | 31 +++++++++++ tests/arch/xilinx/macc_tb.v | 96 ++++++++++++++++++++++++++++++++ tests/arch/xilinx/memory.v | 21 +++++++ tests/arch/xilinx/memory.ys | 17 ++++++ tests/arch/xilinx/mul.v | 11 ++++ tests/arch/xilinx/mul.ys | 9 +++ tests/arch/xilinx/mul_unsigned.v | 30 ++++++++++ tests/arch/xilinx/mul_unsigned.ys | 11 ++++ tests/arch/xilinx/mux.v | 65 ++++++++++++++++++++++ tests/arch/xilinx/mux.ys | 45 +++++++++++++++ tests/arch/xilinx/pmgen_xilinx_srl.ys | 57 +++++++++++++++++++ tests/arch/xilinx/run-test.sh | 20 +++++++ tests/arch/xilinx/shifter.v | 16 ++++++ tests/arch/xilinx/shifter.ys | 11 ++++ tests/arch/xilinx/tribuf.v | 8 +++ tests/arch/xilinx/tribuf.ys | 12 ++++ tests/arch/xilinx/xilinx_srl.v | 40 ++++++++++++++ tests/arch/xilinx/xilinx_srl.ys | 67 +++++++++++++++++++++++ 150 files changed, 3548 insertions(+) create mode 100644 tests/arch/anlogic/.gitignore create mode 100644 tests/arch/anlogic/add_sub.v create mode 100644 tests/arch/anlogic/add_sub.ys create mode 100644 tests/arch/anlogic/counter.v create mode 100644 tests/arch/anlogic/counter.ys create mode 100644 tests/arch/anlogic/dffs.v create mode 100644 tests/arch/anlogic/dffs.ys create mode 100644 tests/arch/anlogic/fsm.v create mode 100644 tests/arch/anlogic/fsm.ys create mode 100644 tests/arch/anlogic/latches.v create mode 100644 tests/arch/anlogic/latches.ys create mode 100644 tests/arch/anlogic/memory.v create mode 100644 tests/arch/anlogic/memory.ys create mode 100644 tests/arch/anlogic/mux.v create mode 100644 tests/arch/anlogic/mux.ys create mode 100755 tests/arch/anlogic/run-test.sh create mode 100644 tests/arch/anlogic/shifter.v create mode 100644 tests/arch/anlogic/shifter.ys create mode 100644 tests/arch/anlogic/tribuf.v create mode 100644 tests/arch/anlogic/tribuf.ys create mode 100644 tests/arch/ecp5/.gitignore create mode 100644 tests/arch/ecp5/add_sub.v create mode 100644 tests/arch/ecp5/add_sub.ys create mode 100644 tests/arch/ecp5/adffs.v create mode 100644 tests/arch/ecp5/adffs.ys create mode 100644 tests/arch/ecp5/counter.v create mode 100644 tests/arch/ecp5/counter.ys create mode 100644 tests/arch/ecp5/dffs.v create mode 100644 tests/arch/ecp5/dffs.ys create mode 100644 tests/arch/ecp5/dpram.v create mode 100644 tests/arch/ecp5/dpram.ys create mode 100644 tests/arch/ecp5/fsm.v create mode 100644 tests/arch/ecp5/fsm.ys create mode 100644 tests/arch/ecp5/latches.v create mode 100644 tests/arch/ecp5/latches.ys create mode 100644 tests/arch/ecp5/logic.v create mode 100644 tests/arch/ecp5/logic.ys create mode 100644 tests/arch/ecp5/macc.v create mode 100644 tests/arch/ecp5/macc.ys create mode 100644 tests/arch/ecp5/memory.v create mode 100644 tests/arch/ecp5/memory.ys create mode 100644 tests/arch/ecp5/mul.v create mode 100644 tests/arch/ecp5/mul.ys create mode 100644 tests/arch/ecp5/mux.v create mode 100644 tests/arch/ecp5/mux.ys create mode 100644 tests/arch/ecp5/rom.v create mode 100644 tests/arch/ecp5/rom.ys create mode 100755 tests/arch/ecp5/run-test.sh create mode 100644 tests/arch/ecp5/shifter.v create mode 100644 tests/arch/ecp5/shifter.ys create mode 100644 tests/arch/ecp5/tribuf.v create mode 100644 tests/arch/ecp5/tribuf.ys create mode 100644 tests/arch/efinix/.gitignore create mode 100644 tests/arch/efinix/add_sub.v create mode 100644 tests/arch/efinix/add_sub.ys create mode 100644 tests/arch/efinix/adffs.v create mode 100644 tests/arch/efinix/adffs.ys create mode 100644 tests/arch/efinix/counter.v create mode 100644 tests/arch/efinix/counter.ys create mode 100644 tests/arch/efinix/dffs.v create mode 100644 tests/arch/efinix/dffs.ys create mode 100644 tests/arch/efinix/fsm.v create mode 100644 tests/arch/efinix/fsm.ys create mode 100644 tests/arch/efinix/latches.v create mode 100644 tests/arch/efinix/latches.ys create mode 100644 tests/arch/efinix/logic.v create mode 100644 tests/arch/efinix/logic.ys create mode 100644 tests/arch/efinix/memory.v create mode 100644 tests/arch/efinix/memory.ys create mode 100644 tests/arch/efinix/mux.v create mode 100644 tests/arch/efinix/mux.ys create mode 100755 tests/arch/efinix/run-test.sh create mode 100644 tests/arch/efinix/shifter.v create mode 100644 tests/arch/efinix/shifter.ys create mode 100644 tests/arch/efinix/tribuf.v create mode 100644 tests/arch/efinix/tribuf.ys create mode 100644 tests/arch/ice40/.gitignore create mode 100644 tests/arch/ice40/add_sub.v create mode 100644 tests/arch/ice40/add_sub.ys create mode 100644 tests/arch/ice40/adffs.v create mode 100644 tests/arch/ice40/adffs.ys create mode 100644 tests/arch/ice40/alu.v create mode 100644 tests/arch/ice40/alu.ys create mode 100644 tests/arch/ice40/counter.v create mode 100644 tests/arch/ice40/counter.ys create mode 100644 tests/arch/ice40/dffs.v create mode 100644 tests/arch/ice40/dffs.ys create mode 100644 tests/arch/ice40/div_mod.v create mode 100644 tests/arch/ice40/div_mod.ys create mode 100644 tests/arch/ice40/dpram.v create mode 100644 tests/arch/ice40/dpram.ys create mode 100644 tests/arch/ice40/fsm.v create mode 100644 tests/arch/ice40/fsm.ys create mode 100644 tests/arch/ice40/ice40_opt.ys create mode 100644 tests/arch/ice40/latches.v create mode 100644 tests/arch/ice40/latches.ys create mode 100644 tests/arch/ice40/logic.v create mode 100644 tests/arch/ice40/logic.ys create mode 100644 tests/arch/ice40/macc.v create mode 100644 tests/arch/ice40/macc.ys create mode 100644 tests/arch/ice40/memory.v create mode 100644 tests/arch/ice40/memory.ys create mode 100644 tests/arch/ice40/mul.v create mode 100644 tests/arch/ice40/mul.ys create mode 100644 tests/arch/ice40/mux.v create mode 100644 tests/arch/ice40/mux.ys create mode 100644 tests/arch/ice40/rom.v create mode 100644 tests/arch/ice40/rom.ys create mode 100755 tests/arch/ice40/run-test.sh create mode 100644 tests/arch/ice40/shifter.v create mode 100644 tests/arch/ice40/shifter.ys create mode 100644 tests/arch/ice40/tribuf.v create mode 100644 tests/arch/ice40/tribuf.ys create mode 100644 tests/arch/ice40/wrapcarry.ys create mode 100644 tests/arch/xilinx/.gitignore create mode 100644 tests/arch/xilinx/add_sub.v create mode 100644 tests/arch/xilinx/add_sub.ys create mode 100644 tests/arch/xilinx/adffs.v create mode 100644 tests/arch/xilinx/adffs.ys create mode 100644 tests/arch/xilinx/counter.v create mode 100644 tests/arch/xilinx/counter.ys create mode 100644 tests/arch/xilinx/dffs.v create mode 100644 tests/arch/xilinx/dffs.ys create mode 100644 tests/arch/xilinx/dsp_simd.ys create mode 100644 tests/arch/xilinx/fsm.v create mode 100644 tests/arch/xilinx/fsm.ys create mode 100644 tests/arch/xilinx/latches.v create mode 100644 tests/arch/xilinx/latches.ys create mode 100644 tests/arch/xilinx/logic.v create mode 100644 tests/arch/xilinx/logic.ys create mode 100644 tests/arch/xilinx/macc.sh create mode 100644 tests/arch/xilinx/macc.v create mode 100644 tests/arch/xilinx/macc.ys create mode 100644 tests/arch/xilinx/macc_tb.v create mode 100644 tests/arch/xilinx/memory.v create mode 100644 tests/arch/xilinx/memory.ys create mode 100644 tests/arch/xilinx/mul.v create mode 100644 tests/arch/xilinx/mul.ys create mode 100644 tests/arch/xilinx/mul_unsigned.v create mode 100644 tests/arch/xilinx/mul_unsigned.ys create mode 100644 tests/arch/xilinx/mux.v create mode 100644 tests/arch/xilinx/mux.ys create mode 100644 tests/arch/xilinx/pmgen_xilinx_srl.ys create mode 100755 tests/arch/xilinx/run-test.sh create mode 100644 tests/arch/xilinx/shifter.v create mode 100644 tests/arch/xilinx/shifter.ys create mode 100644 tests/arch/xilinx/tribuf.v create mode 100644 tests/arch/xilinx/tribuf.ys create mode 100644 tests/arch/xilinx/xilinx_srl.v create mode 100644 tests/arch/xilinx/xilinx_srl.ys (limited to 'tests/arch') diff --git a/tests/arch/anlogic/.gitignore b/tests/arch/anlogic/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/anlogic/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/anlogic/add_sub.v b/tests/arch/anlogic/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/arch/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/arch/anlogic/add_sub.ys b/tests/arch/anlogic/add_sub.ys new file mode 100644 index 000000000..b8b67cc46 --- /dev/null +++ b/tests/arch/anlogic/add_sub.ys @@ -0,0 +1,10 @@ +read_verilog add_sub.v +hierarchy -top top +proc +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/arch/anlogic/counter.v b/tests/arch/anlogic/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/arch/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/arch/anlogic/counter.ys b/tests/arch/anlogic/counter.ys new file mode 100644 index 000000000..036fdba46 --- /dev/null +++ b/tests/arch/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:AL_MAP_SEQ t:AL_MAP_ADDER %% t:* %D diff --git a/tests/arch/anlogic/dffs.v b/tests/arch/anlogic/dffs.v new file mode 100644 index 000000000..3418787c9 --- /dev/null +++ b/tests/arch/anlogic/dffs.v @@ -0,0 +1,15 @@ +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 diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys new file mode 100644 index 000000000..9cbe5fce7 --- /dev/null +++ b/tests/arch/anlogic/dffs.ys @@ -0,0 +1,20 @@ +read_verilog dffs.v +design -save read + +hierarchy -top dff +proc +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 dff # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ %% t:* %D + +design -load read +hierarchy -top dffe +proc +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 dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 +select -assert-count 1 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D diff --git a/tests/arch/anlogic/fsm.v b/tests/arch/anlogic/fsm.v new file mode 100644 index 000000000..368fbaace --- /dev/null +++ b/tests/arch/anlogic/fsm.v @@ -0,0 +1,55 @@ + 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 diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys new file mode 100644 index 000000000..452ef9251 --- /dev/null +++ b/tests/arch/anlogic/fsm.ys @@ -0,0 +1,15 @@ +read_verilog fsm.v +hierarchy -top fsm +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 fsm # 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/arch/anlogic/latches.v b/tests/arch/anlogic/latches.v new file mode 100644 index 000000000..adb5d5319 --- /dev/null +++ b/tests/arch/anlogic/latches.v @@ -0,0 +1,24 @@ +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 diff --git a/tests/arch/anlogic/latches.ys b/tests/arch/anlogic/latches.ys new file mode 100644 index 000000000..c00c7a25d --- /dev/null +++ b/tests/arch/anlogic/latches.ys @@ -0,0 +1,33 @@ +read_verilog latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + + +design -load read +hierarchy -top latchn +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_anlogic +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT5 + +select -assert-none t:AL_MAP_LUT5 %% t:* %D diff --git a/tests/arch/anlogic/memory.v b/tests/arch/anlogic/memory.v new file mode 100644 index 000000000..cb7753f7b --- /dev/null +++ b/tests/arch/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/arch/anlogic/memory.ys b/tests/arch/anlogic/memory.ys new file mode 100644 index 000000000..8c0ce844e --- /dev/null +++ b/tests/arch/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/arch/anlogic/mux.v b/tests/arch/anlogic/mux.v new file mode 100644 index 000000000..27bc0bf0b --- /dev/null +++ b/tests/arch/anlogic/mux.v @@ -0,0 +1,65 @@ +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/tests/arch/anlogic/mux.ys b/tests/arch/anlogic/mux.ys new file mode 100644 index 000000000..64ed2a2bd --- /dev/null +++ b/tests/arch/anlogic/mux.ys @@ -0,0 +1,42 @@ +read_verilog mux.v +design -save read + +hierarchy -top mux2 +proc +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 mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT3 + +select -assert-none t:AL_MAP_LUT3 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +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 mux4 # Constrain all select calls below inside the top module +select -assert-count 1 t:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT6 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +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 mux8 # Constrain all select calls below inside the top module +select -assert-count 3 t:AL_MAP_LUT4 +select -assert-count 1 t:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT4 t:AL_MAP_LUT6 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +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 mux16 # Constrain all select calls below inside the top module +select -assert-count 5 t:AL_MAP_LUT6 + +select -assert-none t:AL_MAP_LUT6 %% t:* %D diff --git a/tests/arch/anlogic/run-test.sh b/tests/arch/anlogic/run-test.sh new file mode 100755 index 000000000..46716f9a0 --- /dev/null +++ b/tests/arch/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 -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/anlogic/shifter.v b/tests/arch/anlogic/shifter.v new file mode 100644 index 000000000..04ae49d83 --- /dev/null +++ b/tests/arch/anlogic/shifter.v @@ -0,0 +1,16 @@ +module top ( +out, +clk, +in +); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out = 0; + + always @(posedge clk) + begin + out <= out >> 1; + out[7] <= in; + end + +endmodule diff --git a/tests/arch/anlogic/shifter.ys b/tests/arch/anlogic/shifter.ys new file mode 100644 index 000000000..5eaed30a3 --- /dev/null +++ b/tests/arch/anlogic/shifter.ys @@ -0,0 +1,10 @@ +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/arch/anlogic/tribuf.v b/tests/arch/anlogic/tribuf.v new file mode 100644 index 000000000..90dd314e4 --- /dev/null +++ b/tests/arch/anlogic/tribuf.v @@ -0,0 +1,8 @@ +module tristate (en, i, o); + input en; + input i; + output o; + + assign o = en ? i : 1'bz; + +endmodule diff --git a/tests/arch/anlogic/tribuf.ys b/tests/arch/anlogic/tribuf.ys new file mode 100644 index 000000000..0eb1338ac --- /dev/null +++ b/tests/arch/anlogic/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog tribuf.v +hierarchy -top tristate +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 tristate # Constrain all select calls below inside the top module +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/ecp5/.gitignore b/tests/arch/ecp5/.gitignore new file mode 100644 index 000000000..1d329c933 --- /dev/null +++ b/tests/arch/ecp5/.gitignore @@ -0,0 +1,2 @@ +*.log +/run-test.mk diff --git a/tests/arch/ecp5/add_sub.v b/tests/arch/ecp5/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/arch/ecp5/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/arch/ecp5/add_sub.ys b/tests/arch/ecp5/add_sub.ys new file mode 100644 index 000000000..ee72d732f --- /dev/null +++ b/tests/arch/ecp5/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog add_sub.v +hierarchy -top top +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:LUT4 +select -assert-none t:LUT4 %% t:* %D + diff --git a/tests/arch/ecp5/adffs.v b/tests/arch/ecp5/adffs.v new file mode 100644 index 000000000..223b52d21 --- /dev/null +++ b/tests/arch/ecp5/adffs.v @@ -0,0 +1,47 @@ +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 diff --git a/tests/arch/ecp5/adffs.ys b/tests/arch/ecp5/adffs.ys new file mode 100644 index 000000000..c6780e565 --- /dev/null +++ b/tests/arch/ecp5/adffs.ys @@ -0,0 +1,40 @@ +read_verilog adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 +select -assert-count 1 t:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-count 1 t:LUT4 +select -assert-none t:TRELLIS_FF t:LUT4 %% t:* %D diff --git a/tests/arch/ecp5/counter.v b/tests/arch/ecp5/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/arch/ecp5/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/arch/ecp5/counter.ys b/tests/arch/ecp5/counter.ys new file mode 100644 index 000000000..8ef70778f --- /dev/null +++ b/tests/arch/ecp5/counter.ys @@ -0,0 +1,10 @@ +read_verilog counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/ecp5/cells_sim.v synth_ecp5 # 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 4 t:CCU2C +select -assert-count 8 t:TRELLIS_FF +select -assert-none t:CCU2C t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/dffs.v b/tests/arch/ecp5/dffs.v new file mode 100644 index 000000000..3418787c9 --- /dev/null +++ b/tests/arch/ecp5/dffs.v @@ -0,0 +1,15 @@ +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 diff --git a/tests/arch/ecp5/dffs.ys b/tests/arch/ecp5/dffs.ys new file mode 100644 index 000000000..a4f45d2fb --- /dev/null +++ b/tests/arch/ecp5/dffs.ys @@ -0,0 +1,19 @@ +read_verilog dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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 +select -assert-count 1 t:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D \ No newline at end of file diff --git a/tests/arch/ecp5/dpram.v b/tests/arch/ecp5/dpram.v new file mode 100644 index 000000000..3ea4c1f27 --- /dev/null +++ b/tests/arch/ecp5/dpram.v @@ -0,0 +1,23 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72]. +*/ +module top (din, write_en, waddr, wclk, raddr, rclk, dout); +parameter addr_width = 8; +parameter data_width = 8; +input [addr_width-1:0] waddr, raddr; +input [data_width-1:0] din; +input write_en, wclk, rclk; +output [data_width-1:0] dout; +reg [data_width-1:0] dout; +reg [data_width-1:0] mem [(1< run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/ecp5/shifter.v b/tests/arch/ecp5/shifter.v new file mode 100644 index 000000000..04ae49d83 --- /dev/null +++ b/tests/arch/ecp5/shifter.v @@ -0,0 +1,16 @@ +module top ( +out, +clk, +in +); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out = 0; + + always @(posedge clk) + begin + out <= out >> 1; + out[7] <= in; + end + +endmodule diff --git a/tests/arch/ecp5/shifter.ys b/tests/arch/ecp5/shifter.ys new file mode 100644 index 000000000..e1901e1a8 --- /dev/null +++ b/tests/arch/ecp5/shifter.ys @@ -0,0 +1,10 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # 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:TRELLIS_FF +select -assert-none t:TRELLIS_FF %% t:* %D diff --git a/tests/arch/ecp5/tribuf.v b/tests/arch/ecp5/tribuf.v new file mode 100644 index 000000000..90dd314e4 --- /dev/null +++ b/tests/arch/ecp5/tribuf.v @@ -0,0 +1,8 @@ +module tristate (en, i, o); + input en; + input i; + output o; + + assign o = en ? i : 1'bz; + +endmodule diff --git a/tests/arch/ecp5/tribuf.ys b/tests/arch/ecp5/tribuf.ys new file mode 100644 index 000000000..a6e9c9598 --- /dev/null +++ b/tests/arch/ecp5/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog tribuf.v +hierarchy -top tristate +proc +flatten +equiv_opt -assert -map +/ecp5/cells_sim.v -map +/simcells.v synth_ecp5 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/efinix/.gitignore b/tests/arch/efinix/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/arch/efinix/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/arch/efinix/add_sub.v b/tests/arch/efinix/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/arch/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/arch/efinix/add_sub.ys b/tests/arch/efinix/add_sub.ys new file mode 100644 index 000000000..8bd28c68e --- /dev/null +++ b/tests/arch/efinix/add_sub.ys @@ -0,0 +1,10 @@ +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 +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/arch/efinix/adffs.v b/tests/arch/efinix/adffs.v new file mode 100644 index 000000000..223b52d21 --- /dev/null +++ b/tests/arch/efinix/adffs.v @@ -0,0 +1,47 @@ +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 diff --git a/tests/arch/efinix/adffs.ys b/tests/arch/efinix/adffs.ys new file mode 100644 index 000000000..1069c6c5c --- /dev/null +++ b/tests/arch/efinix/adffs.ys @@ -0,0 +1,50 @@ +read_verilog adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -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 +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 +hierarchy -top adffn +proc +equiv_opt -async2sync -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-none t:EFX_FF t:EFX_GBUFCE %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -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 +hierarchy -top ndffnr +proc +equiv_opt -async2sync -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_LUT4 + +select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/counter.v b/tests/arch/efinix/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/arch/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/arch/efinix/counter.ys b/tests/arch/efinix/counter.ys new file mode 100644 index 000000000..82e61d39b --- /dev/null +++ b/tests/arch/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/arch/efinix/dffs.v b/tests/arch/efinix/dffs.v new file mode 100644 index 000000000..3418787c9 --- /dev/null +++ b/tests/arch/efinix/dffs.v @@ -0,0 +1,15 @@ +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 diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys new file mode 100644 index 000000000..cdd288233 --- /dev/null +++ b/tests/arch/efinix/dffs.ys @@ -0,0 +1,24 @@ +read_verilog dffs.v +design -save read + +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 +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 +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 +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 diff --git a/tests/arch/efinix/fsm.v b/tests/arch/efinix/fsm.v new file mode 100644 index 000000000..368fbaace --- /dev/null +++ b/tests/arch/efinix/fsm.v @@ -0,0 +1,55 @@ + 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 diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys new file mode 100644 index 000000000..2ec75215d --- /dev/null +++ b/tests/arch/efinix/fsm.ys @@ -0,0 +1,14 @@ +read_verilog fsm.v +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 fsm # 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/arch/efinix/latches.v b/tests/arch/efinix/latches.v new file mode 100644 index 000000000..adb5d5319 --- /dev/null +++ b/tests/arch/efinix/latches.v @@ -0,0 +1,24 @@ +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 diff --git a/tests/arch/efinix/latches.ys b/tests/arch/efinix/latches.ys new file mode 100644 index 000000000..899d024ce --- /dev/null +++ b/tests/arch/efinix/latches.ys @@ -0,0 +1,33 @@ +read_verilog latches.v +design -save read + +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 +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + + +design -load read +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 +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + + +design -load read +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 +select -assert-count 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/logic.v b/tests/arch/efinix/logic.v new file mode 100644 index 000000000..e5343cae0 --- /dev/null +++ b/tests/arch/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/arch/efinix/logic.ys b/tests/arch/efinix/logic.ys new file mode 100644 index 000000000..fdedb337b --- /dev/null +++ b/tests/arch/efinix/logic.ys @@ -0,0 +1,9 @@ +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 + +select -assert-count 9 t:EFX_LUT4 +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/memory.v b/tests/arch/efinix/memory.v new file mode 100644 index 000000000..5634d6507 --- /dev/null +++ b/tests/arch/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/arch/efinix/memory.ys b/tests/arch/efinix/memory.ys new file mode 100644 index 000000000..fe24b0a9b --- /dev/null +++ b/tests/arch/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/arch/efinix/mux.v b/tests/arch/efinix/mux.v new file mode 100644 index 000000000..27bc0bf0b --- /dev/null +++ b/tests/arch/efinix/mux.v @@ -0,0 +1,65 @@ +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/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys new file mode 100644 index 000000000..71a9681de --- /dev/null +++ b/tests/arch/efinix/mux.ys @@ -0,0 +1,41 @@ +read_verilog mux.v +design -save read + +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 +select -assert-count 1 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +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 +select -assert-count 2 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +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 +select -assert-count 5 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D + +design -load read +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 +select -assert-count 12 t:EFX_LUT4 + +select -assert-none t:EFX_LUT4 %% t:* %D diff --git a/tests/arch/efinix/run-test.sh b/tests/arch/efinix/run-test.sh new file mode 100755 index 000000000..46716f9a0 --- /dev/null +++ b/tests/arch/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 -w 'Yosys has only limited support for tri-state logic at the moment.' $x" +done +for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + echo "all:: run-$s" + echo "run-$s:" + echo " @echo 'Running $s..'" + echo " @bash $s" + fi +done +} > run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/efinix/shifter.v b/tests/arch/efinix/shifter.v new file mode 100644 index 000000000..ce2c81dd2 --- /dev/null +++ b/tests/arch/efinix/shifter.v @@ -0,0 +1,16 @@ +module top ( +out, +clk, +in +); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out = 0; + + always @(posedge clk) + begin + out <= out << 1; + out[7] <= in; + end + +endmodule diff --git a/tests/arch/efinix/shifter.ys b/tests/arch/efinix/shifter.ys new file mode 100644 index 000000000..1a6b5565c --- /dev/null +++ b/tests/arch/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/arch/efinix/tribuf.v b/tests/arch/efinix/tribuf.v new file mode 100644 index 000000000..c64468253 --- /dev/null +++ b/tests/arch/efinix/tribuf.v @@ -0,0 +1,8 @@ +module tristate (en, i, o); + input en; + input i; + output reg o; + + always @(en or i) + o <= (en)? i : 1'bZ; +endmodule diff --git a/tests/arch/efinix/tribuf.ys b/tests/arch/efinix/tribuf.ys new file mode 100644 index 000000000..2e2ab9e65 --- /dev/null +++ b/tests/arch/efinix/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog tribuf.v +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 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 diff --git a/tests/arch/ice40/.gitignore b/tests/arch/ice40/.gitignore new file mode 100644 index 000000000..9a71dca69 --- /dev/null +++ b/tests/arch/ice40/.gitignore @@ -0,0 +1,4 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench diff --git a/tests/arch/ice40/add_sub.v b/tests/arch/ice40/add_sub.v new file mode 100644 index 000000000..177c32e30 --- /dev/null +++ b/tests/arch/ice40/add_sub.v @@ -0,0 +1,13 @@ +module top +( + input [3:0] x, + input [3:0] y, + + output [3:0] A, + output [3:0] B + ); + +assign A = x + y; +assign B = x - y; + +endmodule diff --git a/tests/arch/ice40/add_sub.ys b/tests/arch/ice40/add_sub.ys new file mode 100644 index 000000000..4a998d98d --- /dev/null +++ b/tests/arch/ice40/add_sub.ys @@ -0,0 +1,9 @@ +read_verilog add_sub.v +hierarchy -top top +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 11 t:SB_LUT4 +select -assert-count 6 t:SB_CARRY +select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D + diff --git a/tests/arch/ice40/adffs.v b/tests/arch/ice40/adffs.v new file mode 100644 index 000000000..09dc36001 --- /dev/null +++ b/tests/arch/ice40/adffs.v @@ -0,0 +1,87 @@ +module adff + ( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, posedge clr ) + if ( clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module adffn + ( input d, clk, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, negedge clr ) + if ( !clr ) + q <= 1'b0; + else + q <= d; +endmodule + +module dffs + ( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( posedge clk, posedge pre ) + if ( pre ) + q <= 1'b1; + else + q <= d; +endmodule + +module ndffnr + ( input d, clk, pre, clr, output reg q ); + initial begin + q = 0; + end + always @( negedge clk, negedge pre ) + if ( !pre ) + q <= 1'b1; + else + q <= d; +endmodule + +module top ( +input clk, +input clr, +input pre, +input a, +output b,b1,b2,b3 +); + +dffs u_dffs ( + .clk (clk ), + .clr (clr), + .pre (pre), + .d (a ), + .q (b ) + ); + +ndffnr u_ndffnr ( + .clk (clk ), + .clr (clr), + .pre (pre), + .d (a ), + .q (b1 ) + ); + +adff u_adff ( + .clk (clk ), + .clr (clr), + .d (a ), + .q (b2 ) + ); + +adffn u_adffn ( + .clk (clk ), + .clr (clr), + .d (a ), + .q (b3 ) + ); + +endmodule diff --git a/tests/arch/ice40/adffs.ys b/tests/arch/ice40/adffs.ys new file mode 100644 index 000000000..548060b66 --- /dev/null +++ b/tests/arch/ice40/adffs.ys @@ -0,0 +1,11 @@ +read_verilog adffs.v +proc +flatten +equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFNS +select -assert-count 2 t:SB_DFFR +select -assert-count 1 t:SB_DFFS +select -assert-count 2 t:SB_LUT4 +select -assert-none t:SB_DFFNS t:SB_DFFR t:SB_DFFS t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/alu.v b/tests/arch/ice40/alu.v new file mode 100644 index 000000000..f82cc2e21 --- /dev/null +++ b/tests/arch/ice40/alu.v @@ -0,0 +1,19 @@ +module top ( + input clock, + input [31:0] dinA, dinB, + input [2:0] opcode, + output reg [31:0] dout +); + always @(posedge clock) begin + case (opcode) + 0: dout <= dinA + dinB; + 1: dout <= dinA - dinB; + 2: dout <= dinA >> dinB; + 3: dout <= $signed(dinA) >>> dinB; + 4: dout <= dinA << dinB; + 5: dout <= dinA & dinB; + 6: dout <= dinA | dinB; + 7: dout <= dinA ^ dinB; + endcase + end +endmodule diff --git a/tests/arch/ice40/alu.ys b/tests/arch/ice40/alu.ys new file mode 100644 index 000000000..bd859efc4 --- /dev/null +++ b/tests/arch/ice40/alu.ys @@ -0,0 +1,11 @@ +read_verilog alu.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 62 t:SB_CARRY +select -assert-count 32 t:SB_DFF +select -assert-count 655 t:SB_LUT4 +select -assert-none t:SB_CARRY t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/counter.v b/tests/arch/ice40/counter.v new file mode 100644 index 000000000..52852f8ac --- /dev/null +++ b/tests/arch/ice40/counter.v @@ -0,0 +1,17 @@ +module top ( +out, +clk, +reset +); + output [7:0] out; + input clk, reset; + reg [7:0] out; + + always @(posedge clk, posedge reset) + if (reset) begin + out <= 8'b0 ; + end else + out <= out + 1; + + +endmodule diff --git a/tests/arch/ice40/counter.ys b/tests/arch/ice40/counter.ys new file mode 100644 index 000000000..c65c21622 --- /dev/null +++ b/tests/arch/ice40/counter.ys @@ -0,0 +1,11 @@ +read_verilog counter.v +hierarchy -top top +proc +flatten +equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 6 t:SB_CARRY +select -assert-count 8 t:SB_DFFR +select -assert-count 8 t:SB_LUT4 +select -assert-none t:SB_CARRY t:SB_DFFR t:SB_LUT4 %% t:* %D diff --git a/tests/arch/ice40/dffs.v b/tests/arch/ice40/dffs.v new file mode 100644 index 000000000..d97840c43 --- /dev/null +++ b/tests/arch/ice40/dffs.v @@ -0,0 +1,37 @@ +module dff + ( input d, clk, output reg q ); + always @( posedge clk ) + q <= d; +endmodule + +module dffe + ( input d, clk, en, output reg q ); + initial begin + q = 0; + end + always @( posedge clk ) + if ( en ) + q <= d; +endmodule + +module top ( +input clk, +input en, +input a, +output b,b1, +); + +dff u_dff ( + .clk (clk ), + .d (a ), + .q (b ) + ); + +dffe u_ndffe ( + .clk (clk ), + .en (en), + .d (a ), + .q (b1 ) + ); + +endmodule diff --git a/tests/arch/ice40/dffs.ys b/tests/arch/ice40/dffs.ys new file mode 100644 index 000000000..ee7f884b1 --- /dev/null +++ b/tests/arch/ice40/dffs.ys @@ -0,0 +1,10 @@ +read_verilog dffs.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFF +select -assert-count 1 t:SB_DFFE +select -assert-none t:SB_DFF t:SB_DFFE %% t:* %D diff --git a/tests/arch/ice40/div_mod.v b/tests/arch/ice40/div_mod.v new file mode 100644 index 000000000..64a36707d --- /dev/null +++ b/tests/arch/ice40/div_mod.v @@ -0,0 +1,13 @@ +module top +( + input [3:0] x, + input [3:0] y, + + output [3:0] A, + output [3:0] B + ); + +assign A = x % y; +assign B = x / y; + +endmodule diff --git a/tests/arch/ice40/div_mod.ys b/tests/arch/ice40/div_mod.ys new file mode 100644 index 000000000..821d6c301 --- /dev/null +++ b/tests/arch/ice40/div_mod.ys @@ -0,0 +1,9 @@ +read_verilog div_mod.v +hierarchy -top top +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 59 t:SB_LUT4 +select -assert-count 41 t:SB_CARRY +select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D diff --git a/tests/arch/ice40/dpram.v b/tests/arch/ice40/dpram.v new file mode 100644 index 000000000..3ea4c1f27 --- /dev/null +++ b/tests/arch/ice40/dpram.v @@ -0,0 +1,23 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 72]. +*/ +module top (din, write_en, waddr, wclk, raddr, rclk, dout); +parameter addr_width = 8; +parameter data_width = 8; +input [addr_width-1:0] waddr, raddr; +input [data_width-1:0] din; +input write_en, wclk, rclk; +output [data_width-1:0] dout; +reg [data_width-1:0] dout; +reg [data_width-1:0] mem [(1< run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/ice40/shifter.v b/tests/arch/ice40/shifter.v new file mode 100644 index 000000000..c55632552 --- /dev/null +++ b/tests/arch/ice40/shifter.v @@ -0,0 +1,22 @@ +module top ( +out, +clk, +in +); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out = 0; + + always @(posedge clk) + begin +`ifndef BUG + out <= out >> 1; + out[7] <= in; +`else + + out <= out << 1; + out[7] <= in; +`endif + end + +endmodule diff --git a/tests/arch/ice40/shifter.ys b/tests/arch/ice40/shifter.ys new file mode 100644 index 000000000..47d95d298 --- /dev/null +++ b/tests/arch/ice40/shifter.ys @@ -0,0 +1,9 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:SB_DFF +select -assert-none t:SB_DFF %% t:* %D diff --git a/tests/arch/ice40/tribuf.v b/tests/arch/ice40/tribuf.v new file mode 100644 index 000000000..870a02584 --- /dev/null +++ b/tests/arch/ice40/tribuf.v @@ -0,0 +1,23 @@ +module tristate (en, i, o); + input en; + input i; + output o; + + assign o = en ? i : 1'bz; + +endmodule + + +module top ( +input en, +input a, +output b +); + +tristate u_tri ( + .en (en ), + .i (a ), + .o (b ) + ); + +endmodule diff --git a/tests/arch/ice40/tribuf.ys b/tests/arch/ice40/tribuf.ys new file mode 100644 index 000000000..d1e1b3108 --- /dev/null +++ b/tests/arch/ice40/tribuf.ys @@ -0,0 +1,9 @@ +read_verilog tribuf.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/ice40/wrapcarry.ys b/tests/arch/ice40/wrapcarry.ys new file mode 100644 index 000000000..10c029e68 --- /dev/null +++ b/tests/arch/ice40/wrapcarry.ys @@ -0,0 +1,22 @@ +read_verilog <= 2**(SIZEOUT-1)) | overflow_reg; + +// Output accumulation result +assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out; + +endmodule diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys new file mode 100644 index 000000000..6e884b35a --- /dev/null +++ b/tests/arch/xilinx/macc.ys @@ -0,0 +1,31 @@ +read_verilog macc.v +design -save read + +hierarchy -top macc +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd macc # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE +select -assert-count 1 t:DSP48E1 +select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D + +design -load read +hierarchy -top macc2 +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd macc2 # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:DSP48E1 +select -assert-count 1 t:FDRE +select -assert-count 1 t:LUT2 +select -assert-count 41 t:LUT3 +select -assert-none t:BUFG t:DSP48E1 t:FDRE t:LUT2 t:LUT3 %% t:* %D diff --git a/tests/arch/xilinx/macc_tb.v b/tests/arch/xilinx/macc_tb.v new file mode 100644 index 000000000..64aed05c4 --- /dev/null +++ b/tests/arch/xilinx/macc_tb.v @@ -0,0 +1,96 @@ +`timescale 1ns / 1ps + +module testbench; + + parameter SIZEIN = 16, SIZEOUT = 40; + reg clk, ce, rst; + reg signed [SIZEIN-1:0] a, b; + output signed [SIZEOUT-1:0] REF_accum_out, accum_out; + output REF_overflow, overflow; + + integer errcount = 0; + + reg ERROR_FLAG = 0; + + task clkcycle; + begin + #5; + clk = ~clk; + #10; + clk = ~clk; + #2; + ERROR_FLAG = 0; + if (REF_accum_out !== accum_out) begin + $display("ERROR at %1t: REF_accum_out=%b UUT_accum_out=%b DIFF=%b", $time, REF_accum_out, accum_out, REF_accum_out ^ accum_out); + errcount = errcount + 1; + ERROR_FLAG = 1; + end + if (REF_overflow !== overflow) begin + $display("ERROR at %1t: REF_overflow=%b UUT_overflow=%b DIFF=%b", $time, REF_overflow, overflow, REF_overflow ^ overflow); + errcount = errcount + 1; + ERROR_FLAG = 1; + end + #3; + end + endtask + + initial begin + //$dumpfile("test_macc.vcd"); + //$dumpvars(0, testbench); + + #2; + clk = 1'b0; + ce = 1'b0; + a = 0; + b = 0; + + rst = 1'b1; + repeat (10) begin + #10; + clk = 1'b1; + #10; + clk = 1'b0; + #10; + clk = 1'b1; + #10; + clk = 1'b0; + end + rst = 1'b0; + + repeat (10000) begin + clkcycle; + ce = 1; //$urandom & $urandom; + //rst = $urandom & $urandom & $urandom & $urandom & $urandom & $urandom; + a = $urandom & ~(1 << (SIZEIN-1)); + b = $urandom & ~(1 << (SIZEIN-1)); + end + + if (errcount == 0) begin + $display("All tests passed."); + $finish; + end else begin + $display("Caught %1d errors.", errcount); + $stop; + end + end + + macc2 ref ( + .clk(clk), + .ce(ce), + .rst(rst), + .a(a), + .b(b), + .accum_out(REF_accum_out), + .overflow(REF_overflow) + ); + + macc2_uut uut ( + .clk(clk), + .ce(ce), + .rst(rst), + .a(a), + .b(b), + .accum_out(accum_out), + .overflow(overflow) + ); +endmodule diff --git a/tests/arch/xilinx/memory.v b/tests/arch/xilinx/memory.v new file mode 100644 index 000000000..cb7753f7b --- /dev/null +++ b/tests/arch/xilinx/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/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys new file mode 100644 index 000000000..5402513a2 --- /dev/null +++ b/tests/arch/xilinx/memory.ys @@ -0,0 +1,17 @@ +read_verilog memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd top +select -assert-count 1 t:BUFG +select -assert-count 8 t:FDRE +select -assert-count 8 t:RAM64X1D +select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D diff --git a/tests/arch/xilinx/mul.v b/tests/arch/xilinx/mul.v new file mode 100644 index 000000000..d5b48b1d7 --- /dev/null +++ b/tests/arch/xilinx/mul.v @@ -0,0 +1,11 @@ +module top +( + input [5:0] x, + input [5:0] y, + + output [11:0] A, + ); + +assign A = x * y; + +endmodule diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys new file mode 100644 index 000000000..66a06efdc --- /dev/null +++ b/tests/arch/xilinx/mul.ys @@ -0,0 +1,9 @@ +read_verilog mul.v +hierarchy -top top +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:DSP48E1 +select -assert-none t:DSP48E1 %% t:* %D diff --git a/tests/arch/xilinx/mul_unsigned.v b/tests/arch/xilinx/mul_unsigned.v new file mode 100644 index 000000000..e3713a642 --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.v @@ -0,0 +1,30 @@ +/* +Example from: https://www.xilinx.com/support/documentation/sw_manuals/xilinx2019_1/ug901-vivado-synthesis.pdf [p. 89]. +*/ + +// Unsigned 16x24-bit Multiplier +// 1 latency stage on operands +// 3 latency stage after the multiplication +// File: multipliers2.v +// +module mul_unsigned (clk, A, B, RES); +parameter WIDTHA = /*16*/ 6; +parameter WIDTHB = /*24*/ 9; +input clk; +input [WIDTHA-1:0] A; +input [WIDTHB-1:0] B; +output [WIDTHA+WIDTHB-1:0] RES; +reg [WIDTHA-1:0] rA; +reg [WIDTHB-1:0] rB; +reg [WIDTHA+WIDTHB-1:0] M [3:0]; +integer i; +always @(posedge clk) + begin + rA <= A; + rB <= B; + M[0] <= rA * rB; + for (i = 0; i < 3; i = i+1) + M[i+1] <= M[i]; + end +assign RES = M[3]; +endmodule diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys new file mode 100644 index 000000000..62495b90c --- /dev/null +++ b/tests/arch/xilinx/mul_unsigned.ys @@ -0,0 +1,11 @@ +read_verilog mul_unsigned.v +hierarchy -top mul_unsigned +proc + +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mul_unsigned # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:DSP48E1 +select -assert-count 30 t:FDRE +select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D diff --git a/tests/arch/xilinx/mux.v b/tests/arch/xilinx/mux.v new file mode 100644 index 000000000..27bc0bf0b --- /dev/null +++ b/tests/arch/xilinx/mux.v @@ -0,0 +1,65 @@ +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/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys new file mode 100644 index 000000000..420dece4e --- /dev/null +++ b/tests/arch/xilinx/mux.ys @@ -0,0 +1,45 @@ +read_verilog mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 +select -assert-count 1 t:LUT3 + +select -assert-none t:LUT3 %% t:* %D + + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 1 t:LUT6 + +select -assert-none t:LUT6 %% t:* %D + + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 1 t:LUT3 +select -assert-count 2 t:LUT6 + +select -assert-none t:LUT3 t:LUT6 %% t:* %D + + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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 5 t:LUT6 + +select -assert-none t:LUT6 %% t:* %D diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys new file mode 100644 index 000000000..ea2f20487 --- /dev/null +++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys @@ -0,0 +1,57 @@ +read_verilog -icells < run-test.mk +exec ${MAKE:-make} -f run-test.mk diff --git a/tests/arch/xilinx/shifter.v b/tests/arch/xilinx/shifter.v new file mode 100644 index 000000000..04ae49d83 --- /dev/null +++ b/tests/arch/xilinx/shifter.v @@ -0,0 +1,16 @@ +module top ( +out, +clk, +in +); + output [7:0] out; + input signed clk, in; + reg signed [7:0] out = 0; + + always @(posedge clk) + begin + out <= out >> 1; + out[7] <= in; + end + +endmodule diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys new file mode 100644 index 000000000..84e16f41e --- /dev/null +++ b/tests/arch/xilinx/shifter.ys @@ -0,0 +1,11 @@ +read_verilog shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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:BUFG +select -assert-count 8 t:FDRE +select -assert-none t:BUFG t:FDRE %% t:* %D diff --git a/tests/arch/xilinx/tribuf.v b/tests/arch/xilinx/tribuf.v new file mode 100644 index 000000000..c64468253 --- /dev/null +++ b/tests/arch/xilinx/tribuf.v @@ -0,0 +1,8 @@ +module tristate (en, i, o); + input en; + input i; + output reg o; + + always @(en or i) + o <= (en)? i : 1'bZ; +endmodule diff --git a/tests/arch/xilinx/tribuf.ys b/tests/arch/xilinx/tribuf.ys new file mode 100644 index 000000000..c9cfb8546 --- /dev/null +++ b/tests/arch/xilinx/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225 +select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/xilinx/xilinx_srl.v b/tests/arch/xilinx/xilinx_srl.v new file mode 100644 index 000000000..bc2a15ab2 --- /dev/null +++ b/tests/arch/xilinx/xilinx_srl.v @@ -0,0 +1,40 @@ +module xilinx_srl_static_test(input i, clk, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[3], shift1[3]}; +endmodule + +module xilinx_srl_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[l2], shift1[l1]}; +endmodule + +module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q); +parameter CLKPOL = 1; +parameter ENPOL = 1; +parameter DEPTH = 1; +parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}}; +reg [DEPTH-1:0] r = INIT; +wire clk = C ^ CLKPOL; +always @(posedge C) + if (E) + r <= { r[DEPTH-2:0], D }; +assign Q = r[L]; +endmodule diff --git a/tests/arch/xilinx/xilinx_srl.ys b/tests/arch/xilinx/xilinx_srl.ys new file mode 100644 index 000000000..b8df0e55a --- /dev/null +++ b/tests/arch/xilinx/xilinx_srl.ys @@ -0,0 +1,67 @@ +read_verilog xilinx_srl.v +design -save read + +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_static_test +prep +design -save gold + +techmap +xilinx_srl -fixed +opt + +# stat +# show -width +select -assert-count 1 t:$_DFF_P_ +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +dump gate +sat -verify -prove-asserts -show-ports -seq 5 miter + +#design -load gold +#stat + +#design -load gate +#stat + +########## + +design -load read +design -copy-to model $__XILINX_SHREG_ +hierarchy -top xilinx_srl_variable_test +prep +design -save gold + +xilinx_srl -variable +opt + +#stat +# show -width +# write_verilog -noexpr -norename +select -assert-count 1 t:$dff +select -assert-count 1 t:$dff r:WIDTH=1 %i +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -seq 5 miter + +# design -load gold +# stat + +# design -load gate +# stat -- cgit v1.2.3