-synth_ice40
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-select -assert-count 12 t:SB_LUT4
-select -assert-count 7 t:SB_CARRY
-select -assert-count 2 t:$logic_and
-select -assert-count 2 t:$logic_or
+read_verilog add_sub.v
+hierarchy -top top
+synth -flatten -run coarse # technology-independent coarse grained synthesis
+equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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 dffe
+ ( input d, clk, en, output reg q );
+ initial begin
+ q = 0;
+ end
+ always @( posedge clk )
+ if ( en )
+ q <= d;
+endmodule
+
+module dffsr
+ ( input d, clk, pre, clr, output reg q );
+ initial begin
+ q = 0;
+ end
+ always @( posedge clk, posedge pre, posedge clr )
+ if ( clr )
+ q <= 1'b0;
+ else if ( pre )
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+
+module ndffnsnr
+ ( input d, clk, pre, clr, output reg q );
+ initial begin
+ q = 0;
+ end
+ always @( negedge clk, negedge pre, negedge clr )
+ if ( !clr )
+ q <= 1'b0;
+ else if ( !pre )
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+
+module top (
+input clk,
+input clr,
+input pre,
+input a,
+output b,b1,b2,b3,b4
+);
+
+dffsr u_dffsr (
+ .clk (clk ),
+ .clr (clr),
+ .pre (pre),
+ .d (a ),
+ .q (b )
+ );
+
+ndffnsnr u_ndffnsnr (
+ .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 )
+ );
+
+dffe u_dffe (
+ .clk (clk ),
+ .en (clr),
+ .d (a ),
+ .q (b4 )
+ );
+
+endmodule
--- /dev/null
+read_verilog adffs.v
+proc
+dff2dffe
+synth_ice40
+select -assert-count 2 t:SB_DFFR
+select -assert-count 1 t:SB_DFFE
+select -assert-count 4 t:SB_LUT4
+#select -assert-none t:SB_LUT4 t:SB_DFFR t:SB_DFFE t:$_DFFSR_NPP_ t:$_DFFSR_PPP_ %% t:* %D
+write_verilog adffs_synth.v
--- /dev/null
+module testbench;
+ reg clk;
+
+ initial begin
+ // $dumpfile("testbench.vcd");
+ // $dumpvars(0, testbench);
+
+ #5 clk = 0;
+ repeat (10000) begin
+ #5 clk = 1;
+ #5 clk = 0;
+ end
+
+ $display("OKAY");
+ end
+
+
+ reg [2:0] dinA = 0;
+ wire doutB,doutB1,doutB2,doutB3,doutB4;
+ reg dff,ndff,adff,adffn,dffe = 0;
+
+ top uut (
+ .clk (clk ),
+ .a (dinA[0] ),
+ .pre (dinA[1] ),
+ .clr (dinA[2] ),
+ .b (doutB ),
+ .b1 (doutB1 ),
+ .b2 (doutB2 )
+ );
+
+ always @(posedge clk) begin
+ #3;
+ dinA <= dinA + 1;
+ end
+
+ always @( posedge clk, posedge dinA[1], posedge dinA[2] )
+ if ( dinA[2] )
+ dff <= 1'b0;
+ else if ( dinA[1] )
+ dff <= 1'b1;
+ else
+ dff <= dinA[0];
+
+ always @( negedge clk, negedge dinA[1], negedge dinA[2] )
+ if ( !dinA[2] )
+ ndff <= 1'b0;
+ else if ( !dinA[1] )
+ ndff <= 1'b1;
+ else
+ ndff <= dinA[0];
+
+ always @( posedge clk, posedge dinA[2] )
+ if ( dinA[2] )
+ adff <= 1'b0;
+ else
+ adff <= dinA[0];
+
+ always @( posedge clk, negedge dinA[2] )
+ if ( !dinA[2] )
+ adffn <= 1'b0;
+ else
+ adffn <= dinA[0];
+
+ always @( posedge clk )
+ if ( dinA[2] )
+ dffe <= dinA[0];
+
+ assert_dff dff_test(.clk(clk), .test(doutB), .pat(dff));
+ assert_dff ndff_test(.clk(clk), .test(doutB1), .pat(ndff));
+ assert_dff adff_test(.clk(clk), .test(doutB2), .pat(adff));
+ //assert_dff adffn_test(.clk(clk), .test(doutB3), .pat(adffn));
+ //assert_dff dffe_test(.clk(clk), .test(doutB4), .pat(dffe));
+
+endmodule
--- /dev/null
+module assert_dff(input clk, input test, input pat);
+ always @(posedge clk)
+ begin
+ #1;
+ if (test != pat)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time);
+ $stop;
+ end
+ end
+endmodule
+
+module assert_tri(input en, input A, input B);
+ always @(posedge en)
+ begin
+ #1;
+ if (A !== B)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
+ $stop;
+ end
+ end
+endmodule
+
+module assert_Z(input clk, input A);
+ always @(posedge clk)
+ begin
+ #1;
+ if (A === 1'bZ)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
+ $stop;
+ end
+ end
+endmodule
+
+module assert_comb(input A, input B);
+ always @(*)
+ begin
+ #1;
+ if (A !== B)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
+ $stop;
+ end
+ end
+endmodule
-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 dffe
- ( input d, clk, en, output reg q );
- initial begin
- q = 0;
- end
+module top
+ ( input d, clk, output reg q );
always @( posedge clk )
- if ( en )
- q <= d;
-endmodule
-
-module dffsr
- ( input d, clk, pre, clr, output reg q );
- initial begin
- q = 0;
- end
- always @( posedge clk, posedge pre, posedge clr )
- if ( clr )
- q <= 1'b0;
- else if ( pre )
- q <= 1'b1;
- else
- q <= d;
-endmodule
-
-module ndffnsnr
- ( input d, clk, pre, clr, output reg q );
- initial begin
- q = 0;
- end
- always @( negedge clk, negedge pre, negedge clr )
- if ( !clr )
- q <= 1'b0;
- else if ( !pre )
- q <= 1'b1;
- else
q <= d;
endmodule
-
-module top (
-input clk,
-input clr,
-input pre,
-input a,
-output b,b1,b2,b3,b4
-);
-
-dffsr u_dffsr (
- .clk (clk ),
- .clr (clr),
- .pre (pre),
- .d (a ),
- .q (b )
- );
-
-ndffnsnr u_ndffnsnr (
- .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 )
- );
-
-dffe u_dffe (
- .clk (clk ),
- .en (clr),
- .d (a ),
- .q (b4 )
- );
-
-endmodule
+read_verilog dffs.v
proc
flatten
dff2dffe
-synth_ice40
-#equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40
-equiv_opt -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40
-design -load postopt
-select -assert-count 2 t:SB_DFFR
-select -assert-count 1 t:SB_DFFE
-select -assert-count 4 t:SB_LUT4
-select -assert-count 1 t:$_DFFSR_PPP_
-select -assert-count 1 t:$_DFFSR_NPP_
+hierarchy -top top
+synth -flatten -run coarse # technology-independent coarse grained synthesis
+equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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-none t:SB_DFF %% t:* %D
-synth_ice40
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-equiv_opt -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-select -assert-count 85 t:SB_LUT4
-select -assert-count 54 t:SB_CARRY
+read_verilog div_mod.v
+hierarchy -top top
+synth -flatten -run coarse # technology-independent coarse grained synthesis
+equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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 88 t:SB_LUT4
+select -assert-count 65 t:SB_CARRY
+select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
+read_verilog latches.v
synth_ice40
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-equiv_opt -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-proc
select -assert-count 5 t:SB_LUT4
+#select -assert-none t:SB_LUT4 %% t:* %D
+write_verilog latches_synth.v
--- /dev/null
+module testbench;
+ reg clk;
+
+ initial begin
+ // $dumpfile("testbench.vcd");
+ // $dumpvars(0, testbench);
+
+ #5 clk = 0;
+ repeat (10000) begin
+ #5 clk = 1;
+ #5 clk = 0;
+ end
+
+ $display("OKAY");
+ end
+
+
+ reg [2:0] dinA = 0;
+ wire doutB,doutB1,doutB2;
+ reg lat,latn,latsr = 0;
+
+ top uut (
+ .clk (clk ),
+ .a (dinA[0] ),
+ .pre (dinA[1] ),
+ .clr (dinA[2] ),
+ .b (doutB ),
+ .b1 (doutB1 ),
+ .b2 (doutB2 )
+ );
+
+ always @(posedge clk) begin
+ #3;
+ dinA <= dinA + 1;
+ end
+
+ always @*
+ if ( clk )
+ lat <= dinA[0];
+
+
+ always @*
+ if ( !clk )
+ latn <= dinA[0];
+
+
+ always @*
+ if ( dinA[2] )
+ latsr <= 1'b0;
+ else if ( dinA[1] )
+ latsr <= 1'b1;
+ else if ( clk )
+ latsr <= dinA[0];
+
+ assert_dff lat_test(.clk(clk), .test(doutB), .pat(lat));
+ assert_dff latn_test(.clk(clk), .test(doutB1), .pat(latn));
+ assert_dff latsr_test(.clk(clk), .test(doutB2), .pat(latsr));
+
+endmodule
-proc
-memory
+read_verilog memory.v
synth_ice40
-equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-
-select -assert-count 8 t:SB_DFF
-select -assert-count 512 t:SB_DFFE
+select -assert-count 1 t:SB_RAM40_4K
+write_verilog memory_synth.v
--- /dev/null
+module testbench;
+ reg clk;
+
+ initial begin
+ // $dumpfile("testbench.vcd");
+ // $dumpvars(0, testbench);
+
+ #5 clk = 0;
+ repeat (10000) begin
+ #5 clk = 1;
+ #5 clk = 0;
+ end
+
+ $display("OKAY");
+ end
+
+
+ reg [7:0] data_a = 0;
+ reg [5:0] addr_a = 0;
+ reg we_a = 0;
+ reg re_a = 1;
+ wire [7:0] q_a;
+ reg mem_init = 0;
+
+ reg [7:0] pq_a;
+
+ top uut (
+ .data_a(data_a),
+ .addr_a(addr_a),
+ .we_a(we_a),
+ .clk(clk),
+ .q_a(q_a)
+ );
+
+ always @(posedge clk) begin
+ #3;
+ data_a <= data_a + 17;
+
+ addr_a <= addr_a + 1;
+ end
+
+ always @(posedge addr_a) begin
+ #10;
+ if(addr_a > 6'h3E)
+ mem_init <= 1;
+ end
+
+ always @(posedge clk) begin
+ //#3;
+ we_a <= !we_a;
+ end
+
+ // Declare the RAM variable for check
+ reg [7:0] ram[63:0];
+
+ // Port A for check
+ always @ (posedge clk)
+ begin
+ if (we_a)
+ begin
+ ram[addr_a] <= data_a;
+ pq_a <= data_a;
+ end
+ pq_a <= ram[addr_a];
+ end
+
+ uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
+
+endmodule
+
+module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
+ always @(posedge clk)
+ begin
+ #1;
+ if (en == 1 & init == 1 & A !== B)
+ begin
+ $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
+ $stop;
+ end
+ end
+endmodule
--- /dev/null
+module top
+(
+ input [3:0] x,
+ input [3:0] y,
+
+ output [3:0] A,
+ output [3:0] B
+ );
+
+assign A = x * y;
+
+endmodule
--- /dev/null
+read_verilog mul.v
+hierarchy -top top
+synth -flatten -run coarse # technology-independent coarse grained synthesis
+equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check same as technology-dependent fine-grained synthesis
+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 15 t:SB_LUT4
+select -assert-count 3 t:SB_CARRY
+select -assert-none t:SB_LUT4 t:SB_CARRY %% 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
-synth_ice40
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
-equiv_opt -map +/ice40/cells_sim.v synth_ice40
-design -load postopt
-select -assert-count 16 t:SB_LUT4
-select -assert-count 4 t:SB_CARRY
-select -assert-count 1 t:$pow
-
+read_verilog mux.v
synth_ice40
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40
design -load postopt
-#!/bin/bash
set -e
-for x in *.v; do
- echo "Running $x.."
- ../../yosys -q -s ${x%.v}.ys -l ./temp/${x%.v}.log $x
+if [ -f "../../../../../techlibs/common/simcells.v" ]; then
+ COMMON_PREFIX=../../../../../techlibs/common
+ TECHLIBS_PREFIX=../../../../../techlibs
+else
+ COMMON_PREFIX=/usr/local/share/yosys
+ TECHLIBS_PREFIX=/usr/local/share/yosys
+fi
+{
+echo "all::"
+for x in *.ys; do
+ echo "all:: run-$x"
+ echo "run-$x:"
+ echo " @echo 'Running $x..'"
+ echo " @../../yosys -ql ${x%.ys}.log $x"
done
+for t in *_tb.v; do
+ echo "all:: run-$t"
+ echo "run-$t:"
+ echo " @echo 'Running $t..'"
+ echo " @iverilog -o ${t%_tb.v}_testbench $t ${t%_tb.v}_synth.v common.v $COMMON_PREFIX/simcells.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
+ echo " @if ! vvp -N ${t%_tb.v}_testbench > ${t%_tb.v}_testbench.log 2>&1; then grep 'ERROR' ${t%_tb.v}_testbench.log; exit 0; elif grep 'ERROR' ${t%_tb.v}_testbench.log || ! grep 'OKAY' ${t%_tb.v}_testbench.log; then echo "FAIL"; exit 0; fi"
+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
module tristate (en, i, o);
input en;
input i;
- output reg o;
+ output o;
+
+ assign o = en ? i : 1'bz;
- always @(en or i)
- o <= (en)? i : 1'bZ;
endmodule
-synth_ice40
-equiv_opt -assert -map +/ice40/cells_sim.v -map +/simcells.v synth_ice40
-design -load postopt
-select -assert-count 1 t:SB_LUT4
-select -assert-count 1 t:SB_CARRY
+read_verilog tribuf.v
+hierarchy -top top
+synth -flatten -run coarse # technology-independent coarse grained synthesis
+equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check same as technology-dependent fine-grained synthesis
+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
projects / yosys.git / commitdiff