+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
- +cd tests/efinix && bash run-test.sh $(SEEDOPT)
- +cd tests/anlogic && bash run-test.sh $(SEEDOPT)
- +cd tests/ecp5 && bash run-test.sh $(SEEDOPT)
- +cd tests/xilinx && bash run-test.sh $(SEEDOPT)
@echo ""
@echo " Passed \"make test\"."
@echo ""
+++ /dev/null
-*.log
-/run-test.mk
-+*_synth.v
-+*_testbench
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-reset\r
-);\r
- output [7:0] out;\r
- input clk, reset;\r
- reg [7:0] out;\r
-\r
- always @(posedge clk, posedge reset)\r
- if (reset) begin\r
- out <= 8'b0 ;\r
- end else\r
- out <= out + 1;\r
-\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
- module fsm (\r
- clock,\r
- reset,\r
- req_0,\r
- req_1,\r
- gnt_0,\r
- gnt_1\r
- );\r
- input clock,reset,req_0,req_1;\r
- output gnt_0,gnt_1;\r
- wire clock,reset,req_0,req_1;\r
- reg gnt_0,gnt_1;\r
-\r
- parameter SIZE = 3 ;\r
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
-\r
- reg [SIZE-1:0] state;\r
- reg [SIZE-1:0] next_state;\r
-\r
- always @ (posedge clock)\r
- begin : FSM\r
- if (reset == 1'b1) begin\r
- state <= #1 IDLE;\r
- gnt_0 <= 0;\r
- gnt_1 <= 0;\r
- end else\r
- case(state)\r
- IDLE : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- gnt_0 <= 1;\r
- end else if (req_1 == 1'b1) begin\r
- gnt_1 <= 1;\r
- state <= #1 GNT0;\r
- end else begin\r
- state <= #1 IDLE;\r
- end\r
- GNT0 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- end else begin\r
- gnt_0 <= 0;\r
- state <= #1 IDLE;\r
- end\r
- GNT1 : if (req_1 == 1'b1) begin\r
- state <= #1 GNT2;\r
- gnt_1 <= req_0;\r
- end\r
- GNT2 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT1;\r
- gnt_1 <= req_1;\r
- end\r
- default : state <= #1 IDLE;\r
- endcase\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-#!/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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-in\r
-);\r
- output [7:0] out;\r
- input signed clk, in;\r
- reg signed [7:0] out = 0;\r
-\r
- always @(posedge clk)\r
- begin\r
- out <= out >> 1;\r
- out[7] <= in;\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-module tristate (en, i, o);
- input en;
- input i;
- output o;
-
- assign o = en ? i : 1'bz;
-
-endmodule
+++ /dev/null
-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
--- /dev/null
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+reset\r
+);\r
+ output [7:0] out;\r
+ input clk, reset;\r
+ reg [7:0] out;\r
+\r
+ always @(posedge clk, posedge reset)\r
+ if (reset) begin\r
+ out <= 8'b0 ;\r
+ end else\r
+ out <= out + 1;\r
+\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+ module fsm (\r
+ clock,\r
+ reset,\r
+ req_0,\r
+ req_1,\r
+ gnt_0,\r
+ gnt_1\r
+ );\r
+ input clock,reset,req_0,req_1;\r
+ output gnt_0,gnt_1;\r
+ wire clock,reset,req_0,req_1;\r
+ reg gnt_0,gnt_1;\r
+\r
+ parameter SIZE = 3 ;\r
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
+\r
+ reg [SIZE-1:0] state;\r
+ reg [SIZE-1:0] next_state;\r
+\r
+ always @ (posedge clock)\r
+ begin : FSM\r
+ if (reset == 1'b1) begin\r
+ state <= #1 IDLE;\r
+ gnt_0 <= 0;\r
+ gnt_1 <= 0;\r
+ end else\r
+ case(state)\r
+ IDLE : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ gnt_0 <= 1;\r
+ end else if (req_1 == 1'b1) begin\r
+ gnt_1 <= 1;\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT0 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ gnt_0 <= 0;\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT1 : if (req_1 == 1'b1) begin\r
+ state <= #1 GNT2;\r
+ gnt_1 <= req_0;\r
+ end\r
+ GNT2 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT1;\r
+ gnt_1 <= req_1;\r
+ end\r
+ default : state <= #1 IDLE;\r
+ endcase\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+#!/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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+in\r
+);\r
+ output [7:0] out;\r
+ input signed clk, in;\r
+ reg signed [7:0] out = 0;\r
+\r
+ always @(posedge clk)\r
+ begin\r
+ out <= out >> 1;\r
+ out[7] <= in;\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+module tristate (en, i, o);
+ input en;
+ input i;
+ output o;
+
+ assign o = en ? i : 1'bz;
+
+endmodule
--- /dev/null
+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
--- /dev/null
+*.log
+/run-test.mk
--- /dev/null
+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
--- /dev/null
+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
+
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+reset\r
+);\r
+ output [7:0] out;\r
+ input clk, reset;\r
+ reg [7:0] out;\r
+\r
+ always @(posedge clk, posedge reset)\r
+ if (reset) begin\r
+ out <= 8'b0 ;\r
+ end else\r
+ out <= out + 1;\r
+\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+/*
+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<<addr_width)-1:0]
+/* synthesis syn_ramstyle = "no_rw_check" */ ;
+always @(posedge wclk) // Write memory.
+begin
+if (write_en)
+mem[waddr] <= din; // Using write address bus.
+end
+always @(posedge rclk) // Read memory.
+begin
+dout <= mem[raddr]; // Using read address bus.
+end
+endmodule
--- /dev/null
+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
--- /dev/null
+ module fsm (\r
+ clock,\r
+ reset,\r
+ req_0,\r
+ req_1,\r
+ gnt_0,\r
+ gnt_1\r
+ );\r
+ input clock,reset,req_0,req_1;\r
+ output gnt_0,gnt_1;\r
+ wire clock,reset,req_0,req_1;\r
+ reg gnt_0,gnt_1;\r
+\r
+ parameter SIZE = 3 ;\r
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
+\r
+ reg [SIZE-1:0] state;\r
+ reg [SIZE-1:0] next_state;\r
+\r
+ always @ (posedge clock)\r
+ begin : FSM\r
+ if (reset == 1'b1) begin\r
+ state <= #1 IDLE;\r
+ gnt_0 <= 0;\r
+ gnt_1 <= 0;\r
+ end else\r
+ case(state)\r
+ IDLE : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ gnt_0 <= 1;\r
+ end else if (req_1 == 1'b1) begin\r
+ gnt_1 <= 1;\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT0 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ gnt_0 <= 0;\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT1 : if (req_1 == 1'b1) begin\r
+ state <= #1 GNT2;\r
+ gnt_1 <= req_0;\r
+ end\r
+ GNT2 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT1;\r
+ gnt_1 <= req_1;\r
+ end\r
+ default : state <= #1 IDLE;\r
+ endcase\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+read_verilog 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
--- /dev/null
+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
--- /dev/null
+
+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_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
--- /dev/null
+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
--- /dev/null
+read_verilog 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
--- /dev/null
+/*
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+read_verilog 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
--- /dev/null
+module top
+(
+ input [5:0] x,
+ input [5:0] y,
+
+ output [11:0] A,
+ );
+
+assign A = x * y;
+
+endmodule
--- /dev/null
+read_verilog 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
--- /dev/null
+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
+
--- /dev/null
+read_verilog 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
--- /dev/null
+/*
+Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
+*/
+module top(data, addr);
+output [3:0] data;
+input [4:0] addr;
+always @(addr) begin
+case (addr)
+0 : data = 'h4;
+1 : data = 'h9;
+2 : data = 'h1;
+15 : data = 'h8;
+16 : data = 'h1;
+17 : data = 'h0;
+default : data = 'h0;
+endcase
+end
+endmodule
--- /dev/null
+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
--- /dev/null
+#!/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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+in\r
+);\r
+ output [7:0] out;\r
+ input signed clk, in;\r
+ reg signed [7:0] out = 0;\r
+\r
+ always @(posedge clk)\r
+ begin\r
+ out <= out >> 1;\r
+ out[7] <= in;\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+module tristate (en, i, o);
+ input en;
+ input i;
+ output o;
+
+ assign o = en ? i : 1'bz;
+
+endmodule
--- /dev/null
+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
--- /dev/null
+/*.log
+/*.out
+/run-test.mk
--- /dev/null
+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
--- /dev/null
+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
+
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+reset\r
+);\r
+ output [7:0] out;\r
+ input clk, reset;\r
+ reg [7:0] out;\r
+\r
+ always @(posedge clk, posedge reset)\r
+ if (reset) begin\r
+ out <= 8'b0 ;\r
+ end else\r
+ out <= out + 1;\r
+\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+ module fsm (\r
+ clock,\r
+ reset,\r
+ req_0,\r
+ req_1,\r
+ gnt_0,\r
+ gnt_1\r
+ );\r
+ input clock,reset,req_0,req_1;\r
+ output gnt_0,gnt_1;\r
+ wire clock,reset,req_0,req_1;\r
+ reg gnt_0,gnt_1;\r
+\r
+ parameter SIZE = 3 ;\r
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
+\r
+ reg [SIZE-1:0] state;\r
+ reg [SIZE-1:0] next_state;\r
+\r
+ always @ (posedge clock)\r
+ begin : FSM\r
+ if (reset == 1'b1) begin\r
+ state <= #1 IDLE;\r
+ gnt_0 <= 0;\r
+ gnt_1 <= 0;\r
+ end else\r
+ case(state)\r
+ IDLE : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ gnt_0 <= 1;\r
+ end else if (req_1 == 1'b1) begin\r
+ gnt_1 <= 1;\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT0 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ gnt_0 <= 0;\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT1 : if (req_1 == 1'b1) begin\r
+ state <= #1 GNT2;\r
+ gnt_1 <= req_0;\r
+ end\r
+ GNT2 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT1;\r
+ gnt_1 <= req_1;\r
+ end\r
+ default : state <= #1 IDLE;\r
+ endcase\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+#!/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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+in\r
+);\r
+ output [7:0] out;\r
+ input signed clk, in;\r
+ reg signed [7:0] out = 0;\r
+\r
+ always @(posedge clk)\r
+ begin\r
+ out <= out << 1;\r
+ out[7] <= in;\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+module tristate (en, i, o);
+ input en;
+ input i;
+ output reg o;
+
+ always @(en or i)
+ o <= (en)? i : 1'bZ;
+endmodule
--- /dev/null
+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
--- /dev/null
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
--- /dev/null
+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
--- /dev/null
+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
+
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+reset\r
+);\r
+ output [7:0] out;\r
+ input clk, reset;\r
+ reg [7:0] out;\r
+\r
+ always @(posedge clk, posedge reset)\r
+ if (reset) begin\r
+ out <= 8'b0 ;\r
+ end else\r
+ out <= out + 1;\r
+\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+/*
+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<<addr_width)-1:0]
+/* synthesis syn_ramstyle = "no_rw_check" */ ;
+always @(posedge wclk) // Write memory.
+begin
+if (write_en)
+mem[waddr] <= din; // Using write address bus.
+end
+always @(posedge rclk) // Read memory.
+begin
+dout <= mem[raddr]; // Using read address bus.
+end
+endmodule
--- /dev/null
+read_verilog dpram.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
+
+design -load postopt
+cd top
+select -assert-count 1 t:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D
--- /dev/null
+ module fsm (\r
+ clock,\r
+ reset,\r
+ req_0,\r
+ req_1,\r
+ gnt_0,\r
+ gnt_1\r
+ );\r
+ input clock,reset,req_0,req_1;\r
+ output gnt_0,gnt_1;\r
+ wire clock,reset,req_0,req_1;\r
+ reg gnt_0,gnt_1;\r
+\r
+ parameter SIZE = 3 ;\r
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
+\r
+ reg [SIZE-1:0] state;\r
+ reg [SIZE-1:0] next_state;\r
+\r
+ always @ (posedge clock)\r
+ begin : FSM\r
+ if (reset == 1'b1) begin\r
+ state <= #1 IDLE;\r
+ gnt_0 <= 0;\r
+ gnt_1 <= 0;\r
+ end else\r
+ case(state)\r
+ IDLE : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ gnt_0 <= 1;\r
+ end else if (req_1 == 1'b1) begin\r
+ gnt_1 <= 1;\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT0 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ gnt_0 <= 0;\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT1 : if (req_1 == 1'b1) begin\r
+ state <= #1 GNT2;\r
+ gnt_1 <= req_0;\r
+ end\r
+ GNT2 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT1;\r
+ gnt_1 <= req_1;\r
+ end\r
+ default : state <= #1 IDLE;\r
+ endcase\r
+ end\r
+\r
+ endmodule\r
+\r
+ module top (\r
+input clk,\r
+input rst,\r
+input a,\r
+input b,\r
+output g0,\r
+output g1\r
+);\r
+\r
+fsm u_fsm ( .clock(clk),\r
+ .reset(rst),\r
+ .req_0(a),\r
+ .req_1(b),\r
+ .gnt_0(g0),\r
+ .gnt_1(g1));\r
+\r
+endmodule\r
--- /dev/null
+read_verilog fsm.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 2 t:SB_DFFESR
+select -assert-count 2 t:SB_DFFSR
+select -assert-count 1 t:SB_DFFSS
+select -assert-count 13 t:SB_LUT4
+select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D
--- /dev/null
+read_verilog -icells -formal <<EOT
+module top(input CI, I0, output [1:0] CO, output O);
+ wire A = 1'b0, B = 1'b0;
+ \$__ICE40_CARRY_WRAPPER #(
+ // A[0]: 1010 1010 1010 1010
+ // A[1]: 1100 1100 1100 1100
+ // A[2]: 1111 0000 1111 0000
+ // A[3]: 1111 1111 0000 0000
+ .LUT(~16'b 0110_1001_1001_0110)
+ ) u0 (
+ .A(A),
+ .B(B),
+ .CI(CI),
+ .I0(I0),
+ .I3(CI),
+ .CO(CO[0]),
+ .O(O)
+ );
+ SB_CARRY u1 (.I0(~A), .I1(~B), .CI(CI), .CO(CO[1]));
+endmodule
+EOT
+
+equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt
+design -load postopt
+select -assert-count 1 t:*
+select -assert-count 1 t:$lut
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+read_verilog 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)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 9 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
--- /dev/null
+/*
+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 = 6 /*4*/;
+parameter B_WIDTH = 6 /*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
+
+module top2(clk,a,b,c,hold);
+parameter A_WIDTH = 6 /*4*/;
+parameter B_WIDTH = 6 /*3*/;
+input hold;
+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 signed [A_WIDTH-1:0] reg_a;
+reg signed [B_WIDTH-1:0] reg_b;
+reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
+assign c = reg_tmp_c;
+always @(posedge clk)
+begin
+ if (!hold) begin
+ reg_a <= a;
+ reg_b <= b;
+ reg_tmp_c <= reg_a * reg_b + c;
+ end
+end
+endmodule
--- /dev/null
+read_verilog macc.v
+proc
+design -save read
+
+hierarchy -top top
+equiv_opt -assert -multiclock -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)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
+
+design -load read
+hierarchy -top top2
+
+#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+
+equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+clk2fflogic
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
--- /dev/null
+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
--- /dev/null
+read_verilog memory.v
+hierarchy -top top
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
+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:SB_RAM40_4K
+select -assert-none t:SB_RAM40_4K %% t:* %D
--- /dev/null
+module top
+(
+ input [5:0] x,
+ input [5:0] y,
+
+ output [11:0] A,
+ );
+
+assign A = x * y;
+
+endmodule
--- /dev/null
+read_verilog 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)
+cd top # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+/*
+Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
+*/
+module top(data, addr);
+output [3:0] data;
+input [4:0] addr;
+always @(addr) begin
+case (addr)
+0 : data = 'h4;
+1 : data = 'h9;
+2 : data = 'h1;
+15 : data = 'h8;
+16 : data = 'h1;
+17 : data = 'h0;
+default : data = 'h0;
+endcase
+end
+endmodule
--- /dev/null
+read_verilog rom.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 5 t:SB_LUT4
+select -assert-none t:SB_LUT4 %% t:* %D
--- /dev/null
+#!/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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+in\r
+);\r
+ output [7:0] out;\r
+ input signed clk, in;\r
+ reg signed [7:0] out = 0;\r
+\r
+ always @(posedge clk)\r
+ begin\r
+`ifndef BUG\r
+ out <= out >> 1;\r
+ out[7] <= in;\r
+`else\r
+\r
+ out <= out << 1;\r
+ out[7] <= in;\r
+`endif\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+read_verilog <<EOT
+module top(input A, B, CI, output O, CO);
+ SB_CARRY carry (
+ .I0(A),
+ .I1(B),
+ .CI(CI),
+ .CO(CO)
+ );
+ SB_LUT4 #(
+ .LUT_INIT(16'b 0110_1001_1001_0110)
+ ) adder (
+ .I0(1'b0),
+ .I1(A),
+ .I2(B),
+ .I3(1'b0),
+ .O(O)
+ );
+endmodule
+EOT
+
+ice40_wrapcarry
+select -assert-count 1 t:$__ICE40_CARRY_WRAPPER
--- /dev/null
+/*.log
+/*.out
+/run-test.mk
+/*_uut.v
+/test_macc
--- /dev/null
+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
--- /dev/null
+read_verilog 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
+
--- /dev/null
+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
--- /dev/null
+read_verilog 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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+reset\r
+);\r
+ output [7:0] out;\r
+ input clk, reset;\r
+ reg [7:0] out;\r
+\r
+ always @(posedge clk, posedge reset)\r
+ if (reset) begin\r
+ out <= 8'b0 ;\r
+ end else\r
+ out <= out + 1;\r
+\r
+\r
+endmodule\r
--- /dev/null
+read_verilog 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
--- /dev/null
+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
--- /dev/null
+read_verilog 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
+
--- /dev/null
+read_verilog <<EOT
+module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24);
+generate
+ genvar i;
+ // 4 x 12-bit adder
+ for (i = 0; i < 4; i++)
+ assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12];
+ // 2 x 24-bit subtract
+ for (i = 0; i < 2; i++)
+ assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24];
+endgenerate
+reg [3*12-1:0] ro;
+always @* begin
+ ro[0*12+:12] = a[0*10+:10] + b[0*10+:10];
+ ro[1*12+:12] = a[1*10+:10] + b[1*10+:10];
+ ro[2*12+:12] = a[2*8+:8] + b[2*8+:8];
+end
+assign o12[4*12+:3*12] = ro;
+endmodule
+EOT
+
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
+design -load postopt
+select -assert-count 3 t:DSP48E1
--- /dev/null
+ module fsm (\r
+ clock,\r
+ reset,\r
+ req_0,\r
+ req_1,\r
+ gnt_0,\r
+ gnt_1\r
+ );\r
+ input clock,reset,req_0,req_1;\r
+ output gnt_0,gnt_1;\r
+ wire clock,reset,req_0,req_1;\r
+ reg gnt_0,gnt_1;\r
+\r
+ parameter SIZE = 3 ;\r
+ parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
+\r
+ reg [SIZE-1:0] state;\r
+ reg [SIZE-1:0] next_state;\r
+\r
+ always @ (posedge clock)\r
+ begin : FSM\r
+ if (reset == 1'b1) begin\r
+ state <= #1 IDLE;\r
+ gnt_0 <= 0;\r
+ gnt_1 <= 0;\r
+ end else\r
+ case(state)\r
+ IDLE : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ gnt_0 <= 1;\r
+ end else if (req_1 == 1'b1) begin\r
+ gnt_1 <= 1;\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT0 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT0;\r
+ end else begin\r
+ gnt_0 <= 0;\r
+ state <= #1 IDLE;\r
+ end\r
+ GNT1 : if (req_1 == 1'b1) begin\r
+ state <= #1 GNT2;\r
+ gnt_1 <= req_0;\r
+ end\r
+ GNT2 : if (req_0 == 1'b1) begin\r
+ state <= #1 GNT1;\r
+ gnt_1 <= req_1;\r
+ end\r
+ default : state <= #1 IDLE;\r
+ endcase\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+read_verilog 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
--- /dev/null
+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
--- /dev/null
+read_verilog 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
--- /dev/null
+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
--- /dev/null
+read_verilog 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
--- /dev/null
+../../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
--- /dev/null
+// Signed 40-bit streaming accumulator with 16-bit inputs
+// File: HDL_Coding_Techniques/multipliers/multipliers4.v
+//
+// Source:
+// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
+//
+module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
+ input clk, ce, sload,
+ input signed [SIZEIN-1:0] a, b,
+ output signed [SIZEOUT-1:0] accum_out
+);
+// Declare registers for intermediate values
+reg signed [SIZEIN-1:0] a_reg, b_reg;
+reg sload_reg;
+reg signed [2*SIZEIN-1:0] mult_reg;
+reg signed [SIZEOUT-1:0] adder_out, old_result;
+always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
+ if (sload_reg)
+ old_result <= 0;
+ else
+ // 'sload' is now active (=low) and opens the accumulation loop.
+ // The accumulator takes the next multiplier output in
+ // the same cycle.
+ old_result <= adder_out;
+end
+
+always @(posedge clk)
+ if (ce)
+ begin
+ a_reg <= a;
+ b_reg <= b;
+ mult_reg <= a_reg * b_reg;
+ sload_reg <= sload;
+ // Store accumulation result into a register
+ adder_out <= old_result + mult_reg;
+ end
+
+// Output accumulation result
+assign accum_out = adder_out;
+
+endmodule
+
+// Adapted variant of above
+module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
+ input clk,
+ input ce,
+ input rst,
+ input signed [SIZEIN-1:0] a, b,
+ output signed [SIZEOUT-1:0] accum_out,
+ output overflow
+);
+// Declare registers for intermediate values
+reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
+reg signed [2*SIZEIN-1:0] mult_reg = 0;
+reg signed [SIZEOUT:0] adder_out = 0;
+reg overflow_reg;
+always @(posedge clk) begin
+ //if (ce)
+ begin
+ a_reg <= a;
+ b_reg <= b;
+ a_reg2 <= a_reg;
+ b_reg2 <= b_reg;
+ mult_reg <= a_reg2 * b_reg2;
+ // Store accumulation result into a register
+ adder_out <= adder_out + mult_reg;
+ overflow_reg <= overflow;
+ end
+ if (rst) begin
+ a_reg <= 0;
+ a_reg2 <= 0;
+ b_reg <= 0;
+ b_reg2 <= 0;
+ mult_reg <= 0;
+ adder_out <= 0;
+ overflow_reg <= 1'b0;
+ end
+end
+assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg;
+
+// Output accumulation result
+assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out;
+
+endmodule
--- /dev/null
+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
--- /dev/null
+`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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+module top
+(
+ input [5:0] x,
+ input [5:0] y,
+
+ output [11:0] A,
+ );
+
+assign A = x * y;
+
+endmodule
--- /dev/null
+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
--- /dev/null
+/*
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+read_verilog -icells <<EOT
+module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO);
+ parameter DEPTH = 1;
+ parameter [DEPTH-1:0] INIT = 0;
+ parameter CLKPOL = 1;
+ parameter ENPOL = 2;
+
+ wire pos_clk = C == CLKPOL;
+ reg pos_en;
+ always @(E)
+ if (ENPOL == 2) pos_en = 1'b1;
+ else pos_en = (E == ENPOL[0]);
+
+ reg [DEPTH-1:0] r;
+ always @(posedge pos_clk)
+ if (pos_en)
+ r <= {r[DEPTH-2:0], D};
+
+ assign Q = r[L];
+ assign SO = r[DEPTH-1];
+endmodule
+EOT
+read_verilog +/xilinx/cells_sim.v
+proc
+design -save model
+
+test_pmgen -generate xilinx_srl.fixed
+hierarchy -top pmtest_xilinx_srl_pm_fixed
+flatten; opt_clean
+
+design -save gold
+xilinx_srl -fixed
+techmap -autoproc -map %model
+design -stash gate
+
+design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
+design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
+dff2dffe -unmap # sat does not support flops-with-enable yet
+miter -equiv -flatten -make_assert gold gate miter
+sat -set-init-zero -seq 5 -verify -prove-asserts miter
+
+design -load model
+
+test_pmgen -generate xilinx_srl.variable
+hierarchy -top pmtest_xilinx_srl_pm_variable
+flatten; opt_clean
+
+design -save gold
+xilinx_srl -variable
+techmap -autoproc -map %model
+design -stash gate
+
+design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
+design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
+dff2dffe -unmap # sat does not support flops-with-enable yet
+miter -equiv -flatten -make_assert gold gate miter
+sat -set-init-zero -seq 5 -verify -prove-asserts miter
--- /dev/null
+#!/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
--- /dev/null
+module top (\r
+out,\r
+clk,\r
+in\r
+);\r
+ output [7:0] out;\r
+ input signed clk, in;\r
+ reg signed [7:0] out = 0;\r
+\r
+ always @(posedge clk)\r
+ begin\r
+ out <= out >> 1;\r
+ out[7] <= in;\r
+ end\r
+\r
+endmodule\r
--- /dev/null
+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
--- /dev/null
+module tristate (en, i, o);
+ input en;
+ input i;
+ output reg o;
+
+ always @(en or i)
+ o <= (en)? i : 1'bZ;
+endmodule
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
+++ /dev/null
-*.log
-/run-test.mk
+++ /dev/null
-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
+++ /dev/null
-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
-
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-reset\r
-);\r
- output [7:0] out;\r
- input clk, reset;\r
- reg [7:0] out;\r
-\r
- always @(posedge clk, posedge reset)\r
- if (reset) begin\r
- out <= 8'b0 ;\r
- end else\r
- out <= out + 1;\r
-\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-/*
-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<<addr_width)-1:0]
-/* synthesis syn_ramstyle = "no_rw_check" */ ;
-always @(posedge wclk) // Write memory.
-begin
-if (write_en)
-mem[waddr] <= din; // Using write address bus.
-end
-always @(posedge rclk) // Read memory.
-begin
-dout <= mem[raddr]; // Using read address bus.
-end
-endmodule
+++ /dev/null
-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
+++ /dev/null
- module fsm (\r
- clock,\r
- reset,\r
- req_0,\r
- req_1,\r
- gnt_0,\r
- gnt_1\r
- );\r
- input clock,reset,req_0,req_1;\r
- output gnt_0,gnt_1;\r
- wire clock,reset,req_0,req_1;\r
- reg gnt_0,gnt_1;\r
-\r
- parameter SIZE = 3 ;\r
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
-\r
- reg [SIZE-1:0] state;\r
- reg [SIZE-1:0] next_state;\r
-\r
- always @ (posedge clock)\r
- begin : FSM\r
- if (reset == 1'b1) begin\r
- state <= #1 IDLE;\r
- gnt_0 <= 0;\r
- gnt_1 <= 0;\r
- end else\r
- case(state)\r
- IDLE : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- gnt_0 <= 1;\r
- end else if (req_1 == 1'b1) begin\r
- gnt_1 <= 1;\r
- state <= #1 GNT0;\r
- end else begin\r
- state <= #1 IDLE;\r
- end\r
- GNT0 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- end else begin\r
- gnt_0 <= 0;\r
- state <= #1 IDLE;\r
- end\r
- GNT1 : if (req_1 == 1'b1) begin\r
- state <= #1 GNT2;\r
- gnt_1 <= req_0;\r
- end\r
- GNT2 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT1;\r
- gnt_1 <= req_1;\r
- end\r
- default : state <= #1 IDLE;\r
- endcase\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog 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
+++ /dev/null
-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
+++ /dev/null
-
-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_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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
+++ /dev/null
-/*
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
+++ /dev/null
-module top
-(
- input [5:0] x,
- input [5:0] y,
-
- output [11:0] A,
- );
-
-assign A = x * y;
-
-endmodule
+++ /dev/null
-read_verilog 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
+++ /dev/null
-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
-
+++ /dev/null
-read_verilog 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
+++ /dev/null
-/*
-Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
-*/
-module top(data, addr);
-output [3:0] data;
-input [4:0] addr;
-always @(addr) begin
-case (addr)
-0 : data = 'h4;
-1 : data = 'h9;
-2 : data = 'h1;
-15 : data = 'h8;
-16 : data = 'h1;
-17 : data = 'h0;
-default : data = 'h0;
-endcase
-end
-endmodule
+++ /dev/null
-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
+++ /dev/null
-#!/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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-in\r
-);\r
- output [7:0] out;\r
- input signed clk, in;\r
- reg signed [7:0] out = 0;\r
-\r
- always @(posedge clk)\r
- begin\r
- out <= out >> 1;\r
- out[7] <= in;\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-module tristate (en, i, o);
- input en;
- input i;
- output o;
-
- assign o = en ? i : 1'bz;
-
-endmodule
+++ /dev/null
-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
+++ /dev/null
-/*.log
-/*.out
-/run-test.mk
+++ /dev/null
-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
+++ /dev/null
-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
-
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-reset\r
-);\r
- output [7:0] out;\r
- input clk, reset;\r
- reg [7:0] out;\r
-\r
- always @(posedge clk, posedge reset)\r
- if (reset) begin\r
- out <= 8'b0 ;\r
- end else\r
- out <= out + 1;\r
-\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
- module fsm (\r
- clock,\r
- reset,\r
- req_0,\r
- req_1,\r
- gnt_0,\r
- gnt_1\r
- );\r
- input clock,reset,req_0,req_1;\r
- output gnt_0,gnt_1;\r
- wire clock,reset,req_0,req_1;\r
- reg gnt_0,gnt_1;\r
-\r
- parameter SIZE = 3 ;\r
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
-\r
- reg [SIZE-1:0] state;\r
- reg [SIZE-1:0] next_state;\r
-\r
- always @ (posedge clock)\r
- begin : FSM\r
- if (reset == 1'b1) begin\r
- state <= #1 IDLE;\r
- gnt_0 <= 0;\r
- gnt_1 <= 0;\r
- end else\r
- case(state)\r
- IDLE : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- gnt_0 <= 1;\r
- end else if (req_1 == 1'b1) begin\r
- gnt_1 <= 1;\r
- state <= #1 GNT0;\r
- end else begin\r
- state <= #1 IDLE;\r
- end\r
- GNT0 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- end else begin\r
- gnt_0 <= 0;\r
- state <= #1 IDLE;\r
- end\r
- GNT1 : if (req_1 == 1'b1) begin\r
- state <= #1 GNT2;\r
- gnt_1 <= req_0;\r
- end\r
- GNT2 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT1;\r
- gnt_1 <= req_1;\r
- end\r
- default : state <= #1 IDLE;\r
- endcase\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-#!/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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-in\r
-);\r
- output [7:0] out;\r
- input signed clk, in;\r
- reg signed [7:0] out = 0;\r
-\r
- always @(posedge clk)\r
- begin\r
- out <= out << 1;\r
- out[7] <= in;\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-module tristate (en, i, o);
- input en;
- input i;
- output reg o;
-
- always @(en or i)
- o <= (en)? i : 1'bZ;
-endmodule
+++ /dev/null
-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
+++ /dev/null
-*.log
-/run-test.mk
-+*_synth.v
-+*_testbench
+++ /dev/null
-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
+++ /dev/null
-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
-
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-reset\r
-);\r
- output [7:0] out;\r
- input clk, reset;\r
- reg [7:0] out;\r
-\r
- always @(posedge clk, posedge reset)\r
- if (reset) begin\r
- out <= 8'b0 ;\r
- end else\r
- out <= out + 1;\r
-\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-/*
-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<<addr_width)-1:0]
-/* synthesis syn_ramstyle = "no_rw_check" */ ;
-always @(posedge wclk) // Write memory.
-begin
-if (write_en)
-mem[waddr] <= din; // Using write address bus.
-end
-always @(posedge rclk) // Read memory.
-begin
-dout <= mem[raddr]; // Using read address bus.
-end
-endmodule
+++ /dev/null
-read_verilog dpram.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
-memory
-opt -full
-
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
-
-design -load postopt
-cd top
-select -assert-count 1 t:SB_RAM40_4K
-select -assert-none t:SB_RAM40_4K %% t:* %D
+++ /dev/null
- module fsm (\r
- clock,\r
- reset,\r
- req_0,\r
- req_1,\r
- gnt_0,\r
- gnt_1\r
- );\r
- input clock,reset,req_0,req_1;\r
- output gnt_0,gnt_1;\r
- wire clock,reset,req_0,req_1;\r
- reg gnt_0,gnt_1;\r
-\r
- parameter SIZE = 3 ;\r
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
-\r
- reg [SIZE-1:0] state;\r
- reg [SIZE-1:0] next_state;\r
-\r
- always @ (posedge clock)\r
- begin : FSM\r
- if (reset == 1'b1) begin\r
- state <= #1 IDLE;\r
- gnt_0 <= 0;\r
- gnt_1 <= 0;\r
- end else\r
- case(state)\r
- IDLE : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- gnt_0 <= 1;\r
- end else if (req_1 == 1'b1) begin\r
- gnt_1 <= 1;\r
- state <= #1 GNT0;\r
- end else begin\r
- state <= #1 IDLE;\r
- end\r
- GNT0 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- end else begin\r
- gnt_0 <= 0;\r
- state <= #1 IDLE;\r
- end\r
- GNT1 : if (req_1 == 1'b1) begin\r
- state <= #1 GNT2;\r
- gnt_1 <= req_0;\r
- end\r
- GNT2 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT1;\r
- gnt_1 <= req_1;\r
- end\r
- default : state <= #1 IDLE;\r
- endcase\r
- end\r
-\r
- endmodule\r
-\r
- module top (\r
-input clk,\r
-input rst,\r
-input a,\r
-input b,\r
-output g0,\r
-output g1\r
-);\r
-\r
-fsm u_fsm ( .clock(clk),\r
- .reset(rst),\r
- .req_0(a),\r
- .req_1(b),\r
- .gnt_0(g0),\r
- .gnt_1(g1));\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog fsm.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 2 t:SB_DFFESR
-select -assert-count 2 t:SB_DFFSR
-select -assert-count 1 t:SB_DFFSS
-select -assert-count 13 t:SB_LUT4
-select -assert-none t:SB_DFFESR t:SB_DFFSR t:SB_DFFSS t:SB_LUT4 %% t:* %D
+++ /dev/null
-read_verilog -icells -formal <<EOT
-module top(input CI, I0, output [1:0] CO, output O);
- wire A = 1'b0, B = 1'b0;
- \$__ICE40_CARRY_WRAPPER #(
- // A[0]: 1010 1010 1010 1010
- // A[1]: 1100 1100 1100 1100
- // A[2]: 1111 0000 1111 0000
- // A[3]: 1111 1111 0000 0000
- .LUT(~16'b 0110_1001_1001_0110)
- ) u0 (
- .A(A),
- .B(B),
- .CI(CI),
- .I0(I0),
- .I3(CI),
- .CO(CO[0]),
- .O(O)
- );
- SB_CARRY u1 (.I0(~A), .I1(~B), .CI(CI), .CO(CO[1]));
-endmodule
-EOT
-
-equiv_opt -assert -map +/ice40/cells_map.v -map +/ice40/cells_sim.v ice40_opt
-design -load postopt
-select -assert-count 1 t:*
-select -assert-count 1 t:$lut
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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)
-cd top # Constrain all select calls below inside the top module
-select -assert-count 9 t:SB_LUT4
-select -assert-none t:SB_LUT4 %% t:* %D
+++ /dev/null
-/*
-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 = 6 /*4*/;
-parameter B_WIDTH = 6 /*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
-
-module top2(clk,a,b,c,hold);
-parameter A_WIDTH = 6 /*4*/;
-parameter B_WIDTH = 6 /*3*/;
-input hold;
-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 signed [A_WIDTH-1:0] reg_a;
-reg signed [B_WIDTH-1:0] reg_b;
-reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
-assign c = reg_tmp_c;
-always @(posedge clk)
-begin
- if (!hold) begin
- reg_a <= a;
- reg_b <= b;
- reg_tmp_c <= reg_a * reg_b + c;
- end
-end
-endmodule
+++ /dev/null
-read_verilog macc.v
-proc
-design -save read
-
-hierarchy -top top
-equiv_opt -assert -multiclock -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)
-cd top # Constrain all select calls below inside the top module
-select -assert-count 1 t:SB_MAC16
-select -assert-none t:SB_MAC16 %% t:* %D
-
-design -load read
-hierarchy -top top2
-
-#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
-
-equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
-clk2fflogic
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd top2 # Constrain all select calls below inside the top module
-select -assert-count 1 t:SB_MAC16
-select -assert-none t:SB_MAC16 %% t:* %D
+++ /dev/null
-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
+++ /dev/null
-read_verilog memory.v
-hierarchy -top top
-proc
-memory -nomap
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
-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:SB_RAM40_4K
-select -assert-none t:SB_RAM40_4K %% t:* %D
+++ /dev/null
-module top
-(
- input [5:0] x,
- input [5:0] y,
-
- output [11:0] A,
- );
-
-assign A = x * y;
-
-endmodule
+++ /dev/null
-read_verilog 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)
-cd top # Constrain all select calls below inside the top module
-select -assert-count 1 t:SB_MAC16
-select -assert-none t:SB_MAC16 %% t:* %D
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-/*
-Example from: https://www.latticesemi.com/-/media/LatticeSemi/Documents/UserManuals/EI/iCEcube201701UserGuide.ashx?document_id=52071 [p. 74].
-*/
-module top(data, addr);
-output [3:0] data;
-input [4:0] addr;
-always @(addr) begin
-case (addr)
-0 : data = 'h4;
-1 : data = 'h9;
-2 : data = 'h1;
-15 : data = 'h8;
-16 : data = 'h1;
-17 : data = 'h0;
-default : data = 'h0;
-endcase
-end
-endmodule
+++ /dev/null
-read_verilog rom.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 5 t:SB_LUT4
-select -assert-none t:SB_LUT4 %% t:* %D
+++ /dev/null
-#!/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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-in\r
-);\r
- output [7:0] out;\r
- input signed clk, in;\r
- reg signed [7:0] out = 0;\r
-\r
- always @(posedge clk)\r
- begin\r
-`ifndef BUG\r
- out <= out >> 1;\r
- out[7] <= in;\r
-`else\r
-\r
- out <= out << 1;\r
- out[7] <= in;\r
-`endif\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-read_verilog <<EOT
-module top(input A, B, CI, output O, CO);
- SB_CARRY carry (
- .I0(A),
- .I1(B),
- .CI(CI),
- .CO(CO)
- );
- SB_LUT4 #(
- .LUT_INIT(16'b 0110_1001_1001_0110)
- ) adder (
- .I0(1'b0),
- .I1(A),
- .I2(B),
- .I3(1'b0),
- .O(O)
- );
-endmodule
-EOT
-
-ice40_wrapcarry
-select -assert-count 1 t:$__ICE40_CARRY_WRAPPER
+++ /dev/null
-/*.log
-/*.out
-/run-test.mk
-/*_uut.v
-/test_macc
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
-
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-reset\r
-);\r
- output [7:0] out;\r
- input clk, reset;\r
- reg [7:0] out;\r
-\r
- always @(posedge clk, posedge reset)\r
- if (reset) begin\r
- out <= 8'b0 ;\r
- end else\r
- out <= out + 1;\r
-\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog 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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
-
+++ /dev/null
-read_verilog <<EOT
-module simd(input [12*4-1:0] a, input [12*4-1:0] b, (* use_dsp="simd" *) output [7*12-1:0] o12, (* use_dsp="simd" *) output [2*24-1:0] o24);
-generate
- genvar i;
- // 4 x 12-bit adder
- for (i = 0; i < 4; i++)
- assign o12[i*12+:12] = a[i*12+:12] + b[i*12+:12];
- // 2 x 24-bit subtract
- for (i = 0; i < 2; i++)
- assign o24[i*24+:24] = a[i*24+:24] - b[i*24+:24];
-endgenerate
-reg [3*12-1:0] ro;
-always @* begin
- ro[0*12+:12] = a[0*10+:10] + b[0*10+:10];
- ro[1*12+:12] = a[1*10+:10] + b[1*10+:10];
- ro[2*12+:12] = a[2*8+:8] + b[2*8+:8];
-end
-assign o12[4*12+:3*12] = ro;
-endmodule
-EOT
-
-proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx
-design -load postopt
-select -assert-count 3 t:DSP48E1
+++ /dev/null
- module fsm (\r
- clock,\r
- reset,\r
- req_0,\r
- req_1,\r
- gnt_0,\r
- gnt_1\r
- );\r
- input clock,reset,req_0,req_1;\r
- output gnt_0,gnt_1;\r
- wire clock,reset,req_0,req_1;\r
- reg gnt_0,gnt_1;\r
-\r
- parameter SIZE = 3 ;\r
- parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;\r
-\r
- reg [SIZE-1:0] state;\r
- reg [SIZE-1:0] next_state;\r
-\r
- always @ (posedge clock)\r
- begin : FSM\r
- if (reset == 1'b1) begin\r
- state <= #1 IDLE;\r
- gnt_0 <= 0;\r
- gnt_1 <= 0;\r
- end else\r
- case(state)\r
- IDLE : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- gnt_0 <= 1;\r
- end else if (req_1 == 1'b1) begin\r
- gnt_1 <= 1;\r
- state <= #1 GNT0;\r
- end else begin\r
- state <= #1 IDLE;\r
- end\r
- GNT0 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT0;\r
- end else begin\r
- gnt_0 <= 0;\r
- state <= #1 IDLE;\r
- end\r
- GNT1 : if (req_1 == 1'b1) begin\r
- state <= #1 GNT2;\r
- gnt_1 <= req_0;\r
- end\r
- GNT2 : if (req_0 == 1'b1) begin\r
- state <= #1 GNT1;\r
- gnt_1 <= req_1;\r
- end\r
- default : state <= #1 IDLE;\r
- endcase\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog 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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
+++ /dev/null
-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
+++ /dev/null
-read_verilog 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
+++ /dev/null
-../../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
+++ /dev/null
-// Signed 40-bit streaming accumulator with 16-bit inputs
-// File: HDL_Coding_Techniques/multipliers/multipliers4.v
-//
-// Source:
-// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
-//
-module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
- input clk, ce, sload,
- input signed [SIZEIN-1:0] a, b,
- output signed [SIZEOUT-1:0] accum_out
-);
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg;
-reg sload_reg;
-reg signed [2*SIZEIN-1:0] mult_reg;
-reg signed [SIZEOUT-1:0] adder_out, old_result;
-always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
- if (sload_reg)
- old_result <= 0;
- else
- // 'sload' is now active (=low) and opens the accumulation loop.
- // The accumulator takes the next multiplier output in
- // the same cycle.
- old_result <= adder_out;
-end
-
-always @(posedge clk)
- if (ce)
- begin
- a_reg <= a;
- b_reg <= b;
- mult_reg <= a_reg * b_reg;
- sload_reg <= sload;
- // Store accumulation result into a register
- adder_out <= old_result + mult_reg;
- end
-
-// Output accumulation result
-assign accum_out = adder_out;
-
-endmodule
-
-// Adapted variant of above
-module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
- input clk,
- input ce,
- input rst,
- input signed [SIZEIN-1:0] a, b,
- output signed [SIZEOUT-1:0] accum_out,
- output overflow
-);
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
-reg signed [2*SIZEIN-1:0] mult_reg = 0;
-reg signed [SIZEOUT:0] adder_out = 0;
-reg overflow_reg;
-always @(posedge clk) begin
- //if (ce)
- begin
- a_reg <= a;
- b_reg <= b;
- a_reg2 <= a_reg;
- b_reg2 <= b_reg;
- mult_reg <= a_reg2 * b_reg2;
- // Store accumulation result into a register
- adder_out <= adder_out + mult_reg;
- overflow_reg <= overflow;
- end
- if (rst) begin
- a_reg <= 0;
- a_reg2 <= 0;
- b_reg <= 0;
- b_reg2 <= 0;
- mult_reg <= 0;
- adder_out <= 0;
- overflow_reg <= 1'b0;
- end
-end
-assign overflow = (adder_out >= 2**(SIZEOUT-1)) | overflow_reg;
-
-// Output accumulation result
-assign accum_out = overflow ? 2**(SIZEOUT-1)-1 : adder_out;
-
-endmodule
+++ /dev/null
-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
+++ /dev/null
-`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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-module top
-(
- input [5:0] x,
- input [5:0] y,
-
- output [11:0] A,
- );
-
-assign A = x * y;
-
-endmodule
+++ /dev/null
-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
+++ /dev/null
-/*
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-read_verilog -icells <<EOT
-module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO);
- parameter DEPTH = 1;
- parameter [DEPTH-1:0] INIT = 0;
- parameter CLKPOL = 1;
- parameter ENPOL = 2;
-
- wire pos_clk = C == CLKPOL;
- reg pos_en;
- always @(E)
- if (ENPOL == 2) pos_en = 1'b1;
- else pos_en = (E == ENPOL[0]);
-
- reg [DEPTH-1:0] r;
- always @(posedge pos_clk)
- if (pos_en)
- r <= {r[DEPTH-2:0], D};
-
- assign Q = r[L];
- assign SO = r[DEPTH-1];
-endmodule
-EOT
-read_verilog +/xilinx/cells_sim.v
-proc
-design -save model
-
-test_pmgen -generate xilinx_srl.fixed
-hierarchy -top pmtest_xilinx_srl_pm_fixed
-flatten; opt_clean
-
-design -save gold
-xilinx_srl -fixed
-techmap -autoproc -map %model
-design -stash gate
-
-design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
-design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
-dff2dffe -unmap # sat does not support flops-with-enable yet
-miter -equiv -flatten -make_assert gold gate miter
-sat -set-init-zero -seq 5 -verify -prove-asserts miter
-
-design -load model
-
-test_pmgen -generate xilinx_srl.variable
-hierarchy -top pmtest_xilinx_srl_pm_variable
-flatten; opt_clean
-
-design -save gold
-xilinx_srl -variable
-techmap -autoproc -map %model
-design -stash gate
-
-design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
-design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
-dff2dffe -unmap # sat does not support flops-with-enable yet
-miter -equiv -flatten -make_assert gold gate miter
-sat -set-init-zero -seq 5 -verify -prove-asserts miter
+++ /dev/null
-#!/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
+++ /dev/null
-module top (\r
-out,\r
-clk,\r
-in\r
-);\r
- output [7:0] out;\r
- input signed clk, in;\r
- reg signed [7:0] out = 0;\r
-\r
- always @(posedge clk)\r
- begin\r
- out <= out >> 1;\r
- out[7] <= in;\r
- end\r
-\r
-endmodule\r
+++ /dev/null
-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
+++ /dev/null
-module tristate (en, i, o);
- input en;
- input i;
- output reg o;
-
- always @(en or i)
- o <= (en)? i : 1'bZ;
-endmodule
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
projects / yosys.git / commitdiff