Merge pull request #1452 from nakengelhardt/fix_dsp_mem_reg Call memory_dff before DSP mapping to reserve registers (fixes #1447)
diff --git a/Makefile b/Makefile index 895cfbf..845a97b 100644 --- a/Makefile +++ b/Makefile
@@ -147,9 +147,9 @@ include Makefile.conf endif +PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi) ifeq ($(ENABLE_PYOSYS),1) PYTHON_VERSION_TESTCODE := "import sys;t='{v[0]}.{v[1]}'.format(v=list(sys.version_info[:2]));print(t)" -PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi) PYTHON_VERSION := $(shell $(PYTHON_EXECUTABLE) -c ""$(PYTHON_VERSION_TESTCODE)"") PYTHON_MAJOR_VERSION := $(shell echo $(PYTHON_VERSION) | cut -f1 -d.) PYTHON_PREFIX := $(shell $(PYTHON_EXECUTABLE)-config --prefix) @@ -713,7 +713,11 @@ +cd tests/opt && bash run-test.sh +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/arch/ice40 && bash run-test.sh $(SEEDOPT) + +cd tests/arch/xilinx && bash run-test.sh $(SEEDOPT) + +cd tests/arch/ecp5 && bash run-test.sh $(SEEDOPT) + +cd tests/arch/efinix && bash run-test.sh $(SEEDOPT) + +cd tests/arch/anlogic && bash run-test.sh $(SEEDOPT) +cd tests/rpc && bash run-test.sh @echo "" @echo " Passed \"make test\"."
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index c5eef4b..9f9eeb7 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc
@@ -1256,7 +1256,7 @@ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) sva_asserts.insert(inst); - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) + if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_RESTRICT) sva_assumes.insert(inst); if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc index 0e2bead..058d750 100644 --- a/frontends/verilog/verilog_frontend.cc +++ b/frontends/verilog/verilog_frontend.cc
@@ -553,6 +553,12 @@ log(" -Uname[=definition]\n"); log(" undefine the preprocessor symbol 'name'\n"); log("\n"); + log(" -reset\n"); + log(" clear list of defined preprocessor symbols\n"); + log("\n"); + log(" -list\n"); + log(" list currently defined preprocessor symbols\n"); + log("\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE { @@ -588,6 +594,16 @@ design->verilog_defines.erase(name); continue; } + if (arg == "-reset") { + design->verilog_defines.clear(); + continue; + } + if (arg == "-list") { + for (auto &it : design->verilog_defines) { + log("`define %s%s %s\n", it.first.c_str(), it.second.second ? "()" : "", it.second.first.c_str()); + } + continue; + } break; }
diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc index 366c379..145d2eb 100644 --- a/passes/pmgen/Makefile.inc +++ b/passes/pmgen/Makefile.inc
@@ -1,5 +1,5 @@ %_pm.h: passes/pmgen/pmgen.py %.pmg - $(P) mkdir -p passes/pmgen && python3 $< -o $@ -p $(subst _pm.h,,$(notdir $@)) $(filter-out $<,$^) + $(P) mkdir -p passes/pmgen && $(PYTHON_EXECUTABLE) $< -o $@ -p $(subst _pm.h,,$(notdir $@)) $(filter-out $<,$^) # -------------------------------------- @@ -38,7 +38,7 @@ PEEPOPT_PATTERN += passes/pmgen/peepopt_dffmux.pmg passes/pmgen/peepopt_pm.h: passes/pmgen/pmgen.py $(PEEPOPT_PATTERN) - $(P) mkdir -p passes/pmgen && python3 $< -o $@ -p peepopt $(filter-out $<,$^) + $(P) mkdir -p passes/pmgen && $(PYTHON_EXECUTABLE) $< -o $@ -p peepopt $(filter-out $<,$^) # --------------------------------------
diff --git a/techlibs/common/Makefile.inc b/techlibs/common/Makefile.inc index 6c0a4fe..a42f631 100644 --- a/techlibs/common/Makefile.inc +++ b/techlibs/common/Makefile.inc
@@ -9,12 +9,12 @@ techlibs/common/simlib_help.inc: techlibs/common/cellhelp.py techlibs/common/simlib.v $(Q) mkdir -p techlibs/common - $(P) python3 $^ > $@.new + $(P) $(PYTHON_EXECUTABLE) $^ > $@.new $(Q) mv $@.new $@ techlibs/common/simcells_help.inc: techlibs/common/cellhelp.py techlibs/common/simcells.v $(Q) mkdir -p techlibs/common - $(P) python3 $^ > $@.new + $(P) $(PYTHON_EXECUTABLE) $^ > $@.new $(Q) mv $@.new $@ kernel/register.o: techlibs/common/simlib_help.inc techlibs/common/simcells_help.inc
diff --git a/techlibs/ecp5/Makefile.inc b/techlibs/ecp5/Makefile.inc index 5832d07..46463f5 100644 --- a/techlibs/ecp5/Makefile.inc +++ b/techlibs/ecp5/Makefile.inc
@@ -27,12 +27,12 @@ techlibs/ecp5/brams_init.mk: techlibs/ecp5/brams_init.py $(Q) mkdir -p techlibs/ecp5 - $(P) python3 $< + $(P) $(PYTHON_EXECUTABLE) $< $(Q) touch $@ techlibs/ecp5/brams_connect.mk: techlibs/ecp5/brams_connect.py $(Q) mkdir -p techlibs/ecp5 - $(P) python3 $< + $(P) $(PYTHON_EXECUTABLE) $< $(Q) touch $@
diff --git a/techlibs/ecp5/synth_ecp5.cc b/techlibs/ecp5/synth_ecp5.cc index a79dee3..800a8ce 100644 --- a/techlibs/ecp5/synth_ecp5.cc +++ b/techlibs/ecp5/synth_ecp5.cc
@@ -314,9 +314,9 @@ if (abc9) { run("read_verilog -icells -lib +/ecp5/abc9_model.v"); if (nowidelut) - run("abc9 -lut +/ecp5/abc9_5g_nowide.lut -box +/ecp5/abc9_5g.box -W 200"); + run("abc9 -lut +/ecp5/abc9_5g_nowide.lut -box +/ecp5/abc9_5g.box -W 200 -nomfs"); else - run("abc9 -lut +/ecp5/abc9_5g.lut -box +/ecp5/abc9_5g.box -W 200"); + run("abc9 -lut +/ecp5/abc9_5g.lut -box +/ecp5/abc9_5g.box -W 200 -nomfs"); run("techmap -map +/ecp5/abc9_unmap.v"); } else { if (nowidelut)
diff --git a/techlibs/efinix/cells_map.v b/techlibs/efinix/cells_map.v index 0aeab19..3ecec3b 100644 --- a/techlibs/efinix/cells_map.v +++ b/techlibs/efinix/cells_map.v
@@ -17,6 +17,18 @@ 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;
diff --git a/techlibs/efinix/cells_sim.v b/techlibs/efinix/cells_sim.v index 2fc2034..a74d1c5 100644 --- a/techlibs/efinix/cells_sim.v +++ b/techlibs/efinix/cells_sim.v
@@ -59,7 +59,9 @@ 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
diff --git a/techlibs/ice40/Makefile.inc b/techlibs/ice40/Makefile.inc index 3c33fcb..31478e8 100644 --- a/techlibs/ice40/Makefile.inc +++ b/techlibs/ice40/Makefile.inc
@@ -14,7 +14,7 @@ techlibs/ice40/brams_init.mk: techlibs/ice40/brams_init.py $(Q) mkdir -p techlibs/ice40 - $(P) python3 $< + $(P) $(PYTHON_EXECUTABLE) $< $(Q) touch techlibs/ice40/brams_init.mk techlibs/ice40/brams_init1.vh: techlibs/ice40/brams_init.mk
diff --git a/techlibs/xilinx/Makefile.inc b/techlibs/xilinx/Makefile.inc index 0ae67d9..1e59f0a 100644 --- a/techlibs/xilinx/Makefile.inc +++ b/techlibs/xilinx/Makefile.inc
@@ -13,7 +13,7 @@ techlibs/xilinx/brams_init.mk: techlibs/xilinx/brams_init.py $(Q) mkdir -p techlibs/xilinx - $(P) python3 $< + $(P) $(PYTHON_EXECUTABLE) $< $(Q) touch $@ techlibs/xilinx/brams_init_36.vh: techlibs/xilinx/brams_init.mk
diff --git a/tests/ice40/.gitignore b/tests/arch/anlogic/.gitignore similarity index 100% copy from tests/ice40/.gitignore copy to tests/arch/anlogic/.gitignore
diff --git a/tests/arch/anlogic/add_sub.ys b/tests/arch/anlogic/add_sub.ys new file mode 100644 index 0000000..5396ce7 --- /dev/null +++ b/tests/arch/anlogic/add_sub.ys
@@ -0,0 +1,10 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/counter.ys new file mode 100644 index 0000000..d363ec2 --- /dev/null +++ b/tests/arch/anlogic/counter.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/dffs.ys new file mode 100644 index 0000000..d3281ab --- /dev/null +++ b/tests/arch/anlogic/dffs.ys
@@ -0,0 +1,20 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/fsm.ys new file mode 100644 index 0000000..f45951b --- /dev/null +++ b/tests/arch/anlogic/fsm.ys
@@ -0,0 +1,15 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/latches.ys new file mode 100644 index 0000000..8d66f77 --- /dev/null +++ b/tests/arch/anlogic/latches.ys
@@ -0,0 +1,33 @@ +read_verilog ../common/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/logic.ys b/tests/arch/anlogic/logic.ys new file mode 100644 index 0000000..125ee5d --- /dev/null +++ b/tests/arch/anlogic/logic.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/logic.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 1 t:AL_MAP_LUT1 +select -assert-count 6 t:AL_MAP_LUT2 +select -assert-count 2 t:AL_MAP_LUT4 +select -assert-none t:AL_MAP_LUT1 t:AL_MAP_LUT2 t:AL_MAP_LUT4 %% t:* %D
diff --git a/tests/arch/anlogic/memory.ys b/tests/arch/anlogic/memory.ys new file mode 100644 index 0000000..87b93c2 --- /dev/null +++ b/tests/arch/anlogic/memory.ys
@@ -0,0 +1,21 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/mux.ys new file mode 100644 index 0000000..3d5fe7c --- /dev/null +++ b/tests/arch/anlogic/mux.ys
@@ -0,0 +1,42 @@ +read_verilog ../common/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/xilinx/run-test.sh b/tests/arch/anlogic/run-test.sh similarity index 74% rename from tests/xilinx/run-test.sh rename to tests/arch/anlogic/run-test.sh index ea56b70..bf19b88 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/anlogic/run-test.sh
@@ -6,7 +6,7 @@ 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
diff --git a/tests/arch/anlogic/shifter.ys b/tests/arch/anlogic/shifter.ys new file mode 100644 index 0000000..12df44b --- /dev/null +++ b/tests/arch/anlogic/shifter.ys
@@ -0,0 +1,10 @@ +read_verilog ../common/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.ys b/tests/arch/anlogic/tribuf.ys new file mode 100644 index 0000000..eaa0737 --- /dev/null +++ b/tests/arch/anlogic/tribuf.ys
@@ -0,0 +1,9 @@ +read_verilog ../common/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/common/add_sub.v b/tests/arch/common/add_sub.v new file mode 100644 index 0000000..77e5f57 --- /dev/null +++ b/tests/arch/common/add_sub.v
@@ -0,0 +1,12 @@ +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/common/adffs.v b/tests/arch/common/adffs.v new file mode 100644 index 0000000..576bd81 --- /dev/null +++ b/tests/arch/common/adffs.v
@@ -0,0 +1,43 @@ +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/common/counter.v b/tests/arch/common/counter.v new file mode 100644 index 0000000..9746fd7 --- /dev/null +++ b/tests/arch/common/counter.v
@@ -0,0 +1,11 @@ +module top ( out, clk, reset ); + output [7:0] out; + input clk, reset; + reg [7:0] out; + + always @(posedge clk, posedge reset) + if (reset) + out <= 8'b0; + else + out <= out + 1; +endmodule
diff --git a/tests/arch/common/dffs.v b/tests/arch/common/dffs.v new file mode 100644 index 0000000..636252d --- /dev/null +++ b/tests/arch/common/dffs.v
@@ -0,0 +1,13 @@ +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/common/fsm.v b/tests/arch/common/fsm.v new file mode 100644 index 0000000..9d3fbb6 --- /dev/null +++ b/tests/arch/common/fsm.v
@@ -0,0 +1,51 @@ + module fsm ( clock, reset, req_0, req_1, gnt_0, gnt_1 ); + input clock,reset,req_0,req_1; + output gnt_0,gnt_1; + wire clock,reset,req_0,req_1; + reg gnt_0,gnt_1; + + parameter SIZE = 3; + parameter IDLE = 3'b001; + parameter GNT0 = 3'b010; + parameter GNT1 = 3'b100; + parameter GNT2 = 3'b101; + + reg [SIZE-1:0] state; + reg [SIZE-1:0] next_state; + + always @ (posedge clock) + begin : FSM + if (reset == 1'b1) begin + state <= #1 IDLE; + gnt_0 <= 0; + gnt_1 <= 0; + end + else + case(state) + IDLE : if (req_0 == 1'b1) begin + state <= #1 GNT0; + gnt_0 <= 1; + end else if (req_1 == 1'b1) begin + gnt_1 <= 1; + state <= #1 GNT0; + end else begin + state <= #1 IDLE; + end + GNT0 : if (req_0 == 1'b1) begin + state <= #1 GNT0; + end else begin + gnt_0 <= 0; + state <= #1 IDLE; + end + GNT1 : if (req_1 == 1'b1) begin + state <= #1 GNT2; + gnt_1 <= req_0; + end + GNT2 : if (req_0 == 1'b1) begin + state <= #1 GNT1; + gnt_1 <= req_1; + end + default : state <= #1 IDLE; + endcase + end +endmodule
diff --git a/tests/arch/common/latches.v b/tests/arch/common/latches.v new file mode 100644 index 0000000..60b7571 --- /dev/null +++ b/tests/arch/common/latches.v
@@ -0,0 +1,21 @@ +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/common/logic.v b/tests/arch/common/logic.v new file mode 100644 index 0000000..c17899f --- /dev/null +++ b/tests/arch/common/logic.v
@@ -0,0 +1,16 @@ +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/ice40/memory.v b/tests/arch/common/memory.v similarity index 100% rename from tests/ice40/memory.v rename to tests/arch/common/memory.v
diff --git a/tests/arch/common/mul.v b/tests/arch/common/mul.v new file mode 100644 index 0000000..437a91c --- /dev/null +++ b/tests/arch/common/mul.v
@@ -0,0 +1,9 @@ +module top +( + input [5:0] x, + input [5:0] y, + + output [11:0] A, +); + assign A = x * y; +endmodule
diff --git a/tests/arch/common/mux.v b/tests/arch/common/mux.v new file mode 100644 index 0000000..71c1ac7 --- /dev/null +++ b/tests/arch/common/mux.v
@@ -0,0 +1,60 @@ +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/ice40/shifter.v b/tests/arch/common/shifter.v similarity index 61% rename from tests/ice40/shifter.v rename to tests/arch/common/shifter.v index c556325..cace3b5 100644 --- a/tests/ice40/shifter.v +++ b/tests/arch/common/shifter.v
@@ -1,22 +1,11 @@ -module top ( -out, -clk, -in -); +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 - + end endmodule
diff --git a/tests/arch/common/tribuf.v b/tests/arch/common/tribuf.v new file mode 100644 index 0000000..e1d7016 --- /dev/null +++ b/tests/arch/common/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/ecp5/.gitignore b/tests/arch/ecp5/.gitignore new file mode 100644 index 0000000..1d329c9 --- /dev/null +++ b/tests/arch/ecp5/.gitignore
@@ -0,0 +1,2 @@ +*.log +/run-test.mk
diff --git a/tests/arch/ecp5/add_sub.ys b/tests/arch/ecp5/add_sub.ys new file mode 100644 index 0000000..d85ce79 --- /dev/null +++ b/tests/arch/ecp5/add_sub.ys
@@ -0,0 +1,9 @@ +read_verilog ../common/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.ys b/tests/arch/ecp5/adffs.ys new file mode 100644 index 0000000..01605df --- /dev/null +++ b/tests/arch/ecp5/adffs.ys
@@ -0,0 +1,40 @@ +read_verilog ../common/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.ys b/tests/arch/ecp5/counter.ys new file mode 100644 index 0000000..f9f60fb --- /dev/null +++ b/tests/arch/ecp5/counter.ys
@@ -0,0 +1,10 @@ +read_verilog ../common/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.ys b/tests/arch/ecp5/dffs.ys new file mode 100644 index 0000000..be97972 --- /dev/null +++ b/tests/arch/ecp5/dffs.ys
@@ -0,0 +1,19 @@ +read_verilog ../common/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/ice40/dpram.v b/tests/arch/ecp5/dpram.v similarity index 100% copy from tests/ice40/dpram.v copy to tests/arch/ecp5/dpram.v
diff --git a/tests/arch/ecp5/dpram.ys b/tests/arch/ecp5/dpram.ys new file mode 100644 index 0000000..3bc6bc1 --- /dev/null +++ b/tests/arch/ecp5/dpram.ys
@@ -0,0 +1,18 @@ +read_verilog dpram.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter + +#Blocked by issue #1358 (Missing ECP5 simulation models) +#ERROR: Failed to import cell gate.mem.0.0.0 (type DP16KD) 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 1 t:DP16KD +select -assert-none t:DP16KD %% t:* %D
diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys new file mode 100644 index 0000000..f834a4c --- /dev/null +++ b/tests/arch/ecp5/fsm.ys
@@ -0,0 +1,12 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +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 fsm # Constrain all select calls below inside the top module +select -assert-count 1 t:L6MUX21 +select -assert-count 13 t:LUT4 +select -assert-count 5 t:PFUMX +select -assert-count 5 t:TRELLIS_FF +select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/latches.ys b/tests/arch/ecp5/latches.ys new file mode 100644 index 0000000..3d011d7 --- /dev/null +++ b/tests/arch/ecp5/latches.ys
@@ -0,0 +1,34 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ecp5 +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 + +select -assert-none t: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_ecp5 +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 + +select -assert-none t: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_ecp5 +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:LUT4 +select -assert-count 1 t:PFUMX + +select -assert-none t:LUT4 t:PFUMX %% t:* %D
diff --git a/tests/arch/ecp5/logic.ys b/tests/arch/ecp5/logic.ys new file mode 100644 index 0000000..3298b19 --- /dev/null +++ b/tests/arch/ecp5/logic.ys
@@ -0,0 +1,8 @@ +read_verilog ../common/logic.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 9 t:LUT4 +select -assert-none t:LUT4 %% t:* %D
diff --git a/tests/arch/ecp5/macc.v b/tests/arch/ecp5/macc.v new file mode 100644 index 0000000..63a3d3a --- /dev/null +++ b/tests/arch/ecp5/macc.v
@@ -0,0 +1,25 @@ +/* +Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 77]. +*/ +module top(clk,a,b,c,set); +parameter A_WIDTH = 4; +parameter B_WIDTH = 3; +input set; +input clk; +input signed [(A_WIDTH - 1):0] a; +input signed [(B_WIDTH - 1):0] b; +output signed [(A_WIDTH + B_WIDTH - 1):0] c; +reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c; +assign c = reg_tmp_c; +always @(posedge clk) +begin +if(set) +begin +reg_tmp_c <= 0; +end +else +begin +reg_tmp_c <= a * b + c; +end +end +endmodule
diff --git a/tests/arch/ecp5/macc.ys b/tests/arch/ecp5/macc.ys new file mode 100644 index 0000000..1863ea4 --- /dev/null +++ b/tests/arch/ecp5/macc.ys
@@ -0,0 +1,13 @@ +read_verilog macc.v +hierarchy -top top +proc +# Blocked by issue #1358 (Missing ECP5 simulation models) +#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +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 1 t:MULT18X18D +select -assert-count 4 t:CCU2C +select -assert-count 7 t:TRELLIS_FF + +select -assert-none t:CCU2C t:MULT18X18D t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/memory.ys b/tests/arch/ecp5/memory.ys new file mode 100644 index 0000000..c82b7b4 --- /dev/null +++ b/tests/arch/ecp5/memory.ys
@@ -0,0 +1,19 @@ +read_verilog ../common/memory.v +hierarchy -top top +proc +memory -nomap +equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5 +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 24 t:L6MUX21 +select -assert-count 71 t:LUT4 +select -assert-count 32 t:PFUMX +select -assert-count 8 t:TRELLIS_DPR16X4 +select -assert-count 35 t:TRELLIS_FF +select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_DPR16X4 t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/ecp5/mul.ys b/tests/arch/ecp5/mul.ys new file mode 100644 index 0000000..2105be5 --- /dev/null +++ b/tests/arch/ecp5/mul.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/mul.v +hierarchy -top top +proc +# Blocked by issue #1358 (Missing ECP5 simulation models) +#equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check +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 1 t:MULT18X18D +select -assert-none t:MULT18X18D %% t:* %D
diff --git a/tests/arch/ecp5/mux.ys b/tests/arch/ecp5/mux.ys new file mode 100644 index 0000000..92463aa --- /dev/null +++ b/tests/arch/ecp5/mux.ys
@@ -0,0 +1,46 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +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 mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 +select -assert-none t:LUT4 %% t:* %D + +design -load read +hierarchy -top mux4 +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 mux4 # Constrain all select calls below inside the top module +select -assert-count 1 t:L6MUX21 +select -assert-count 4 t:LUT4 +select -assert-count 2 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D + +design -load read +hierarchy -top mux8 +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 mux8 # Constrain all select calls below inside the top module +select -assert-count 1 t:L6MUX21 +select -assert-count 7 t:LUT4 +select -assert-count 2 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D + +design -load read +hierarchy -top mux16 +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 mux16 # Constrain all select calls below inside the top module +select -assert-count 8 t:L6MUX21 +select -assert-count 26 t:LUT4 +select -assert-count 12 t:PFUMX + +select -assert-none t:LUT4 t:L6MUX21 t:PFUMX %% t:* %D
diff --git a/tests/ice40/rom.v b/tests/arch/ecp5/rom.v similarity index 100% copy from tests/ice40/rom.v copy to tests/arch/ecp5/rom.v
diff --git a/tests/arch/ecp5/rom.ys b/tests/arch/ecp5/rom.ys new file mode 100644 index 0000000..98645ae --- /dev/null +++ b/tests/arch/ecp5/rom.ys
@@ -0,0 +1,10 @@ +read_verilog rom.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 6 t:LUT4 +select -assert-count 3 t:PFUMX +select -assert-none t:LUT4 t:PFUMX %% t:* %D
diff --git a/tests/xilinx/run-test.sh b/tests/arch/ecp5/run-test.sh similarity index 74% copy from tests/xilinx/run-test.sh copy to tests/arch/ecp5/run-test.sh index ea56b70..bf19b88 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/ecp5/run-test.sh
@@ -6,7 +6,7 @@ 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
diff --git a/tests/arch/ecp5/shifter.ys b/tests/arch/ecp5/shifter.ys new file mode 100644 index 0000000..3f0079f --- /dev/null +++ b/tests/arch/ecp5/shifter.ys
@@ -0,0 +1,10 @@ +read_verilog ../common/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.ys b/tests/arch/ecp5/tribuf.ys new file mode 100644 index 0000000..0118705 --- /dev/null +++ b/tests/arch/ecp5/tribuf.ys
@@ -0,0 +1,9 @@ +read_verilog ../common/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/xilinx/.gitignore b/tests/arch/efinix/.gitignore similarity index 74% copy from tests/xilinx/.gitignore copy to tests/arch/efinix/.gitignore index 54733fb..b48f808 100644 --- a/tests/xilinx/.gitignore +++ b/tests/arch/efinix/.gitignore
@@ -1,4 +1,3 @@ /*.log /*.out /run-test.mk -/*_uut.v
diff --git a/tests/arch/efinix/add_sub.ys b/tests/arch/efinix/add_sub.ys new file mode 100644 index 0000000..20523c0 --- /dev/null +++ b/tests/arch/efinix/add_sub.ys
@@ -0,0 +1,10 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/adffs.ys new file mode 100644 index 0000000..49dc7f2 --- /dev/null +++ b/tests/arch/efinix/adffs.ys
@@ -0,0 +1,50 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/counter.ys new file mode 100644 index 0000000..d20b8ae --- /dev/null +++ b/tests/arch/efinix/counter.ys
@@ -0,0 +1,12 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/dffs.ys new file mode 100644 index 0000000..af787ab --- /dev/null +++ b/tests/arch/efinix/dffs.ys
@@ -0,0 +1,24 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/fsm.ys new file mode 100644 index 0000000..a8ba70f --- /dev/null +++ b/tests/arch/efinix/fsm.ys
@@ -0,0 +1,14 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/latches.ys new file mode 100644 index 0000000..1b1c000 --- /dev/null +++ b/tests/arch/efinix/latches.ys
@@ -0,0 +1,33 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/logic.ys new file mode 100644 index 0000000..76e98e0 --- /dev/null +++ b/tests/arch/efinix/logic.ys
@@ -0,0 +1,9 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/memory.ys new file mode 100644 index 0000000..6f6acdc --- /dev/null +++ b/tests/arch/efinix/memory.ys
@@ -0,0 +1,18 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/mux.ys new file mode 100644 index 0000000..b46f641 --- /dev/null +++ b/tests/arch/efinix/mux.ys
@@ -0,0 +1,41 @@ +read_verilog ../common/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/xilinx/run-test.sh b/tests/arch/efinix/run-test.sh similarity index 74% copy from tests/xilinx/run-test.sh copy to tests/arch/efinix/run-test.sh index ea56b70..bf19b88 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/efinix/run-test.sh
@@ -6,7 +6,7 @@ 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
diff --git a/tests/arch/efinix/shifter.ys b/tests/arch/efinix/shifter.ys new file mode 100644 index 0000000..54f7116 --- /dev/null +++ b/tests/arch/efinix/shifter.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/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.ys b/tests/arch/efinix/tribuf.ys new file mode 100644 index 0000000..47904f2 --- /dev/null +++ b/tests/arch/efinix/tribuf.ys
@@ -0,0 +1,12 @@ +read_verilog ../common/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/ice40/.gitignore b/tests/arch/ice40/.gitignore similarity index 100% rename from tests/ice40/.gitignore rename to tests/arch/ice40/.gitignore
diff --git a/tests/ice40/add_sub.ys b/tests/arch/ice40/add_sub.ys similarity index 91% rename from tests/ice40/add_sub.ys rename to tests/arch/ice40/add_sub.ys index 4a998d9..578ec08 100644 --- a/tests/ice40/add_sub.ys +++ b/tests/arch/ice40/add_sub.ys
@@ -1,4 +1,4 @@ -read_verilog add_sub.v +read_verilog ../common/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)
diff --git a/tests/arch/ice40/adffs.ys b/tests/arch/ice40/adffs.ys new file mode 100644 index 0000000..e5dbabb --- /dev/null +++ b/tests/arch/ice40/adffs.ys
@@ -0,0 +1,39 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -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 adff # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFR +select -assert-none t:SB_DFFR %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -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 adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFR +select -assert-count 1 t:SB_LUT4 +select -assert-none t:SB_DFFR t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -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 dffs # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFSS +select -assert-none t:SB_DFFSS %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -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 ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFNSR +select -assert-count 1 t:SB_LUT4 +select -assert-none t:SB_DFFNSR t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/counter.ys b/tests/arch/ice40/counter.ys similarity index 92% rename from tests/ice40/counter.ys rename to tests/arch/ice40/counter.ys index c65c216..f112eb9 100644 --- a/tests/ice40/counter.ys +++ b/tests/arch/ice40/counter.ys
@@ -1,4 +1,4 @@ -read_verilog counter.v +read_verilog ../common/counter.v hierarchy -top top proc flatten
diff --git a/tests/arch/ice40/dffs.ys b/tests/arch/ice40/dffs.ys new file mode 100644 index 0000000..b28a5a9 --- /dev/null +++ b/tests/arch/ice40/dffs.ys
@@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +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 dff # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFF +select -assert-none t:SB_DFF %% t:* %D + +design -load read +hierarchy -top dffe +proc +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 dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_DFFE +select -assert-none t:SB_DFFE %% t:* %D \ No newline at end of file
diff --git a/tests/ice40/dpram.v b/tests/arch/ice40/dpram.v similarity index 100% rename from tests/ice40/dpram.v rename to tests/arch/ice40/dpram.v
diff --git a/tests/ice40/dpram.ys b/tests/arch/ice40/dpram.ys similarity index 100% rename from tests/ice40/dpram.ys rename to tests/arch/ice40/dpram.ys
diff --git a/tests/ice40/fsm.ys b/tests/arch/ice40/fsm.ys similarity index 77% rename from tests/ice40/fsm.ys rename to tests/arch/ice40/fsm.ys index 4cc8629..5aacc6c 100644 --- a/tests/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys
@@ -1,10 +1,10 @@ -read_verilog fsm.v -hierarchy -top top +read_verilog ../common/fsm.v +hierarchy -top fsm 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 +cd fsm # Constrain all select calls below inside the top module select -assert-count 2 t:SB_DFFESR select -assert-count 2 t:SB_DFFSR
diff --git a/tests/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys similarity index 100% rename from tests/ice40/ice40_opt.ys rename to tests/arch/ice40/ice40_opt.ys
diff --git a/tests/arch/ice40/latches.ys b/tests/arch/ice40/latches.ys new file mode 100644 index 0000000..b06dd63 --- /dev/null +++ b/tests/arch/ice40/latches.ys
@@ -0,0 +1,33 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +# Can't run any sort of equivalence check because latches are blown to LUTs +synth_ice40 +cd latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_LUT4 + +select -assert-none t:SB_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_ice40 +cd latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_LUT4 + +select -assert-none t:SB_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_ice40 +cd latchsr # Constrain all select calls below inside the top module +select -assert-count 2 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/logic.ys b/tests/arch/ice40/logic.ys similarity index 91% rename from tests/ice40/logic.ys rename to tests/arch/ice40/logic.ys index fc5e5b1..7432f5b 100644 --- a/tests/ice40/logic.ys +++ b/tests/arch/ice40/logic.ys
@@ -1,4 +1,4 @@ -read_verilog logic.v +read_verilog ../common/logic.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)
diff --git a/tests/ice40/macc.v b/tests/arch/ice40/macc.v similarity index 100% rename from tests/ice40/macc.v rename to tests/arch/ice40/macc.v
diff --git a/tests/ice40/macc.ys b/tests/arch/ice40/macc.ys similarity index 100% rename from tests/ice40/macc.ys rename to tests/arch/ice40/macc.ys
diff --git a/tests/ice40/memory.ys b/tests/arch/ice40/memory.ys similarity index 91% rename from tests/ice40/memory.ys rename to tests/arch/ice40/memory.ys index a66afba..c356e67 100644 --- a/tests/ice40/memory.ys +++ b/tests/arch/ice40/memory.ys
@@ -1,4 +1,4 @@ -read_verilog memory.v +read_verilog ../common/memory.v hierarchy -top top proc memory -nomap
diff --git a/tests/ice40/mul.ys b/tests/arch/ice40/mul.ys similarity index 91% rename from tests/ice40/mul.ys rename to tests/arch/ice40/mul.ys index 8a0822a..9891b77 100644 --- a/tests/ice40/mul.ys +++ b/tests/arch/ice40/mul.ys
@@ -1,4 +1,4 @@ -read_verilog mul.v +read_verilog ../common/mul.v hierarchy -top top equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
diff --git a/tests/arch/ice40/mux.ys b/tests/arch/ice40/mux.ys new file mode 100644 index 0000000..9982239 --- /dev/null +++ b/tests/arch/ice40/mux.ys
@@ -0,0 +1,40 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +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 mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:SB_LUT4 +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +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 mux4 # Constrain all select calls below inside the top module +select -assert-count 2 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +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 mux8 # Constrain all select calls below inside the top module +select -assert-count 5 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +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 mux16 # Constrain all select calls below inside the top module +select -assert-count 11 t:SB_LUT4 + +select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/rom.v b/tests/arch/ice40/rom.v similarity index 100% rename from tests/ice40/rom.v rename to tests/arch/ice40/rom.v
diff --git a/tests/ice40/rom.ys b/tests/arch/ice40/rom.ys similarity index 100% rename from tests/ice40/rom.ys rename to tests/arch/ice40/rom.ys
diff --git a/tests/xilinx/run-test.sh b/tests/arch/ice40/run-test.sh similarity index 74% copy from tests/xilinx/run-test.sh copy to tests/arch/ice40/run-test.sh index ea56b70..bf19b88 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/ice40/run-test.sh
@@ -6,7 +6,7 @@ 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
diff --git a/tests/ice40/shifter.ys b/tests/arch/ice40/shifter.ys similarity index 90% rename from tests/ice40/shifter.ys rename to tests/arch/ice40/shifter.ys index 47d95d2..08ea64f 100644 --- a/tests/ice40/shifter.ys +++ b/tests/arch/ice40/shifter.ys
@@ -1,4 +1,4 @@ -read_verilog shifter.v +read_verilog ../common/shifter.v hierarchy -top top proc flatten
diff --git a/tests/ice40/tribuf.ys b/tests/arch/ice40/tribuf.ys similarity index 66% rename from tests/ice40/tribuf.ys rename to tests/arch/ice40/tribuf.ys index d1e1b31..10cded9 100644 --- a/tests/ice40/tribuf.ys +++ b/tests/arch/ice40/tribuf.ys
@@ -1,9 +1,11 @@ -read_verilog tribuf.v -hierarchy -top top +read_verilog ../common/tribuf.v +hierarchy -top tristate proc +tribuf flatten +synth 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 +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/ice40/wrapcarry.ys b/tests/arch/ice40/wrapcarry.ys similarity index 100% rename from tests/ice40/wrapcarry.ys rename to tests/arch/ice40/wrapcarry.ys
diff --git a/tests/xilinx/.gitignore b/tests/arch/xilinx/.gitignore similarity index 76% rename from tests/xilinx/.gitignore rename to tests/arch/xilinx/.gitignore index 54733fb..c99b793 100644 --- a/tests/xilinx/.gitignore +++ b/tests/arch/xilinx/.gitignore
@@ -2,3 +2,4 @@ /*.out /run-test.mk /*_uut.v +/test_macc
diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys new file mode 100644 index 0000000..9dbddce --- /dev/null +++ b/tests/arch/xilinx/add_sub.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/add_sub.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 14 t:LUT2 +select -assert-count 6 t:MUXCY +select -assert-count 8 t:XORCY +select -assert-none t:LUT2 t:MUXCY t:XORCY %% t:* %D +
diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys new file mode 100644 index 0000000..12c3441 --- /dev/null +++ b/tests/arch/xilinx/adffs.ys
@@ -0,0 +1,51 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -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 adff # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDCE + +select -assert-none t:BUFG t:FDCE %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -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 adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDCE +select -assert-count 1 t:LUT1 + +select -assert-none t:BUFG t:FDCE t:LUT1 %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -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 dffs # 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:LUT2 + +select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -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 ndffnr # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE_1 +select -assert-count 1 t:LUT2 + +select -assert-none t:BUFG t:FDRE_1 t:LUT2 %% t:* %D
diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys new file mode 100644 index 0000000..57b645d --- /dev/null +++ b/tests/arch/xilinx/counter.ys
@@ -0,0 +1,14 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -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:FDCE +select -assert-count 1 t:LUT1 +select -assert-count 7 t:MUXCY +select -assert-count 8 t:XORCY +select -assert-none t:BUFG t:FDCE t:LUT1 t:MUXCY t:XORCY %% t:* %D
diff --git a/tests/arch/xilinx/dffs.ys b/tests/arch/xilinx/dffs.ys new file mode 100644 index 0000000..0bba485 --- /dev/null +++ b/tests/arch/xilinx/dffs.ys
@@ -0,0 +1,25 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +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 dff # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D + + +design -load read +hierarchy -top dffe +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 dffe # Constrain all select calls below inside the top module +select -assert-count 1 t:BUFG +select -assert-count 1 t:FDRE + +select -assert-none t:BUFG t:FDRE %% t:* %D +
diff --git a/tests/xilinx/dsp_simd.ys b/tests/arch/xilinx/dsp_simd.ys similarity index 100% rename from tests/xilinx/dsp_simd.ys rename to tests/arch/xilinx/dsp_simd.ys
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys new file mode 100644 index 0000000..d2b4814 --- /dev/null +++ b/tests/arch/xilinx/fsm.ys
@@ -0,0 +1,14 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +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 fsm # Constrain all select calls below inside the top module + +select -assert-count 1 t:BUFG +select -assert-count 5 t:FDRE +select -assert-count 1 t:LUT3 +select -assert-count 2 t:LUT4 +select -assert-count 4 t:LUT6 +select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D
diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys new file mode 100644 index 0000000..fe7887e --- /dev/null +++ b/tests/arch/xilinx/latches.ys
@@ -0,0 +1,35 @@ +read_verilog ../common/latches.v +design -save read + +hierarchy -top latchp +proc +equiv_opt -async2sync -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 latchp # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE + +select -assert-none t:LDCE %% t:* %D + + +design -load read +hierarchy -top latchn +proc +equiv_opt -async2sync -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 latchn # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 1 t:LUT1 + +select -assert-none t:LDCE t:LUT1 %% t:* %D + + +design -load read +hierarchy -top latchsr +proc +equiv_opt -async2sync -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 latchsr # Constrain all select calls below inside the top module +select -assert-count 1 t:LDCE +select -assert-count 2 t:LUT3 + +select -assert-none t:LDCE t:LUT3 %% t:* %D
diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys new file mode 100644 index 0000000..c0f6da3 --- /dev/null +++ b/tests/arch/xilinx/logic.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/logic.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:LUT1 +select -assert-count 6 t:LUT2 +select -assert-count 2 t:LUT4 +select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D
diff --git a/tests/arch/xilinx/macc.sh b/tests/arch/xilinx/macc.sh new file mode 100644 index 0000000..2272679 --- /dev/null +++ b/tests/arch/xilinx/macc.sh
@@ -0,0 +1,3 @@ +../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v +iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v +vvp -N ./test_macc
diff --git a/tests/xilinx/macc.v b/tests/arch/xilinx/macc.v similarity index 100% rename from tests/xilinx/macc.v rename to tests/arch/xilinx/macc.v
diff --git a/tests/xilinx/macc.ys b/tests/arch/xilinx/macc.ys similarity index 99% rename from tests/xilinx/macc.ys rename to tests/arch/xilinx/macc.ys index 417a3b2..6e884b3 100644 --- a/tests/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys
@@ -1,8 +1,8 @@ read_verilog macc.v design -save read -proc 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 @@ -15,8 +15,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D design -load read -proc 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
diff --git a/tests/xilinx/macc_tb.v b/tests/arch/xilinx/macc_tb.v similarity index 100% rename from tests/xilinx/macc_tb.v rename to tests/arch/xilinx/macc_tb.v
diff --git a/tests/arch/xilinx/memory.ys b/tests/arch/xilinx/memory.ys new file mode 100644 index 0000000..da1ed0e --- /dev/null +++ b/tests/arch/xilinx/memory.ys
@@ -0,0 +1,17 @@ +read_verilog ../common/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.ys b/tests/arch/xilinx/mul.ys new file mode 100644 index 0000000..d768149 --- /dev/null +++ b/tests/arch/xilinx/mul.ys
@@ -0,0 +1,9 @@ +read_verilog ../common/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/xilinx/mul_unsigned.v b/tests/arch/xilinx/mul_unsigned.v similarity index 100% rename from tests/xilinx/mul_unsigned.v rename to tests/arch/xilinx/mul_unsigned.v
diff --git a/tests/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys similarity index 99% rename from tests/xilinx/mul_unsigned.ys rename to tests/arch/xilinx/mul_unsigned.ys index 77990bd..62495b9 100644 --- a/tests/xilinx/mul_unsigned.ys +++ b/tests/arch/xilinx/mul_unsigned.ys
@@ -1,6 +1,7 @@ read_verilog mul_unsigned.v -proc 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
diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys new file mode 100644 index 0000000..821d0fa --- /dev/null +++ b/tests/arch/xilinx/mux.ys
@@ -0,0 +1,45 @@ +read_verilog ../common/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/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys similarity index 100% rename from tests/xilinx/pmgen_xilinx_srl.ys rename to tests/arch/xilinx/pmgen_xilinx_srl.ys
diff --git a/tests/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh similarity index 74% copy from tests/xilinx/run-test.sh copy to tests/arch/xilinx/run-test.sh index ea56b70..bf19b88 100755 --- a/tests/xilinx/run-test.sh +++ b/tests/arch/xilinx/run-test.sh
@@ -6,7 +6,7 @@ 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
diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys new file mode 100644 index 0000000..455437f --- /dev/null +++ b/tests/arch/xilinx/shifter.ys
@@ -0,0 +1,11 @@ +read_verilog ../common/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.ys b/tests/arch/xilinx/tribuf.ys new file mode 100644 index 0000000..4697703 --- /dev/null +++ b/tests/arch/xilinx/tribuf.ys
@@ -0,0 +1,12 @@ +read_verilog ../common/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/xilinx/xilinx_srl.v b/tests/arch/xilinx/xilinx_srl.v similarity index 100% rename from tests/xilinx/xilinx_srl.v rename to tests/arch/xilinx/xilinx_srl.v
diff --git a/tests/xilinx/xilinx_srl.ys b/tests/arch/xilinx/xilinx_srl.ys similarity index 100% rename from tests/xilinx/xilinx_srl.ys rename to tests/arch/xilinx/xilinx_srl.ys
diff --git a/tests/ice40/add_sub.v b/tests/ice40/add_sub.v deleted file mode 100644 index 177c32e..0000000 --- a/tests/ice40/add_sub.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/ice40/adffs.v b/tests/ice40/adffs.v deleted file mode 100644 index 09dc360..0000000 --- a/tests/ice40/adffs.v +++ /dev/null
@@ -1,87 +0,0 @@ -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/ice40/adffs.ys b/tests/ice40/adffs.ys deleted file mode 100644 index 548060b..0000000 --- a/tests/ice40/adffs.ys +++ /dev/null
@@ -1,11 +0,0 @@ -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/ice40/alu.v b/tests/ice40/alu.v deleted file mode 100644 index f82cc2e..0000000 --- a/tests/ice40/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/ice40/alu.ys b/tests/ice40/alu.ys deleted file mode 100644 index bd859ef..0000000 --- a/tests/ice40/alu.ys +++ /dev/null
@@ -1,11 +0,0 @@ -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/ice40/counter.v b/tests/ice40/counter.v deleted file mode 100644 index 52852f8..0000000 --- a/tests/ice40/counter.v +++ /dev/null
@@ -1,17 +0,0 @@ -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/ice40/dffs.v b/tests/ice40/dffs.v deleted file mode 100644 index d97840c..0000000 --- a/tests/ice40/dffs.v +++ /dev/null
@@ -1,37 +0,0 @@ -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/ice40/dffs.ys b/tests/ice40/dffs.ys deleted file mode 100644 index ee7f884..0000000 --- a/tests/ice40/dffs.ys +++ /dev/null
@@ -1,10 +0,0 @@ -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/ice40/div_mod.v b/tests/ice40/div_mod.v deleted file mode 100644 index 64a3670..0000000 --- a/tests/ice40/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/ice40/div_mod.ys b/tests/ice40/div_mod.ys deleted file mode 100644 index 821d6c3..0000000 --- a/tests/ice40/div_mod.ys +++ /dev/null
@@ -1,9 +0,0 @@ -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/ice40/fsm.v b/tests/ice40/fsm.v deleted file mode 100644 index 0605bd1..0000000 --- a/tests/ice40/fsm.v +++ /dev/null
@@ -1,73 +0,0 @@ - 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/ice40/latches.v b/tests/ice40/latches.v deleted file mode 100644 index 9dc43e4..0000000 --- a/tests/ice40/latches.v +++ /dev/null
@@ -1,58 +0,0 @@ -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/ice40/latches.ys b/tests/ice40/latches.ys deleted file mode 100644 index 708734e..0000000 --- a/tests/ice40/latches.ys +++ /dev/null
@@ -1,12 +0,0 @@ -read_verilog latches.v - -proc -flatten -# Can't run any sort of equivalence check because latches are blown to LUTs -#equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check - -#design -load preopt -synth_ice40 -cd top -select -assert-count 4 t:SB_LUT4 -select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/logic.v b/tests/ice40/logic.v deleted file mode 100644 index e5343ca..0000000 --- a/tests/ice40/logic.v +++ /dev/null
@@ -1,18 +0,0 @@ -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/ice40/mul.v b/tests/ice40/mul.v deleted file mode 100644 index d5b48b1..0000000 --- a/tests/ice40/mul.v +++ /dev/null
@@ -1,11 +0,0 @@ -module top -( - input [5:0] x, - input [5:0] y, - - output [11:0] A, - ); - -assign A = x * y; - -endmodule
diff --git a/tests/ice40/mux.v b/tests/ice40/mux.v deleted file mode 100644 index 0814b73..0000000 --- a/tests/ice40/mux.v +++ /dev/null
@@ -1,100 +0,0 @@ -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/ice40/mux.ys b/tests/ice40/mux.ys deleted file mode 100644 index 182b494..0000000 --- a/tests/ice40/mux.ys +++ /dev/null
@@ -1,8 +0,0 @@ -read_verilog mux.v -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 19 t:SB_LUT4 -select -assert-none t:SB_LUT4 %% t:* %D
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh deleted file mode 100755 index 46716f9..0000000 --- a/tests/ice40/run-test.sh +++ /dev/null
@@ -1,20 +0,0 @@ -#!/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/ice40/tribuf.v b/tests/ice40/tribuf.v deleted file mode 100644 index 870a025..0000000 --- a/tests/ice40/tribuf.v +++ /dev/null
@@ -1,23 +0,0 @@ -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/xilinx/latches.v b/tests/xilinx/latches.v deleted file mode 100644 index 83bad7f..0000000 --- a/tests/xilinx/latches.v +++ /dev/null
@@ -1,58 +0,0 @@ -module latchp - ( input d, en, output reg q ); - always @* - if ( en ) - q <= d; -endmodule - -module latchn - ( input d, en, output reg q ); - always @* - if ( !en ) - q <= d; -endmodule - -module latchsr - ( input d, 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/xilinx/latches.ys b/tests/xilinx/latches.ys deleted file mode 100644 index bd1dffd..0000000 --- a/tests/xilinx/latches.ys +++ /dev/null
@@ -1,13 +0,0 @@ -read_verilog latches.v - -proc -flatten -equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check - -design -load preopt -synth_xilinx -cd top -select -assert-count 1 t:LUT1 -select -assert-count 2 t:LUT3 -select -assert-count 3 t:LDCE -select -assert-none t:LUT1 t:LUT3 t:LDCE %% t:* %D
diff --git a/tests/xilinx/macc.sh b/tests/xilinx/macc.sh deleted file mode 100644 index 86e4c2b..0000000 --- a/tests/xilinx/macc.sh +++ /dev/null
@@ -1,3 +0,0 @@ -../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" macc.v -o macc_uut.v -iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../techlibs/xilinx/cells_sim.v -vvp -N ./test_macc