Skip to content

Y
yosys-tests
Commit 69456969 by Eddie Hung
Options

Merge remote-tracking branch 'origin/master' into xc7srl

parents 97ee0d05 435c14ef
Showing with 2183 additions and 19 deletions
architecture/Makefile
......@@ -19,32 +19,39 @@ endef
#achronix
$(eval $(call template,synth_achronix,synth_achronix synth_achronix_top synth_achronix_vout synth_achronix_run synth_achronix_noflatten synth_achronix_retime))
$(eval $(call template,synth_achronix_error,synth_achronix_fully_selected))
#anlogic
$(eval $(call template,synth_anlogic,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime))
$(eval $(call template,synth_anlogic_fulladder,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime))
$(eval $(call template,synth_anlogic_mem,synth_anlogic synth_anlogic_top synth_anlogic_edif synth_anlogic_json synth_anlogic_run synth_anlogic_noflatten synth_anlogic_retime anlogic_determine_init_eqn))
$(eval $(call template,synth_anlogic_error,synth_anlogic_fully_selected))
#coolrunner2
$(eval $(call template,synth_coolrunner2,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime))
$(eval $(call template,synth_coolrunner2_fulladder,synth_coolrunner2 synth_coolrunner2_top synth_coolrunner2_vout synth_coolrunner2_run synth_coolrunner2_noflatten synth_coolrunner2_retime))
$(eval $(call template,synth_coolrunner2_error,synth_coolrunner2_fully_selected))
#easic - issue #920
# we do not have eTools anymore available, commented until aquired
#$(eval $(call template,synth_easic,synth_easic synth_easic_top synth_easic_vlog synth_easic_run synth_easic_noflatten synth_easic_retime))
$(eval $(call template,synth_easic_error,synth_easic_fully_selected))
#ecp5
$(eval $(call template,synth_ecp5,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr ecp5_ffinit))
$(eval $(call template,synth_ecp5_wide_ffs,synth_ecp5 synth_ecp5_top synth_ecp5_blif synth_ecp5_edif synth_ecp5_json synth_ecp5_run synth_ecp5_flatten synth_ecp5_noflatten synth_ecp5_retime synth_ecp5_noccu2 synth_ecp5_nodffe synth_ecp5_nobram synth_ecp5_nodram synth_ecp5_nomux synth_ecp5_abc2 synth_ecp5_vpr ecp5_ffinit))
$(eval $(call template,synth_ecp5_error,synth_ecp5_fully_selected))
#gowin
$(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime synth_gowin_nobram synth_gowin_noflatten ))
$(eval $(call template,synth_gowin_mem,synth_gowin synth_gowin_top synth_gowin_vout synth_gowin_run synth_gowin_retime synth_gowin_nobram synth_gowin_noflatten ))
$(eval $(call template,synth_gowin_error,synth_gowin_fully_selected ))
#ice40
$(eval $(call template,synth_ice40,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
$(eval $(call template,synth_ice40_mem,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_retime synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
$(eval $(call template,synth_ice40_wide_ffs,synth_ice40 synth_ice40_top synth_ice40_blif synth_ice40_edif synth_ice40_json synth_ice40_run synth_ice40_noflatten synth_ice40_flatten synth_ice40_nocarry synth_ice40_nodffe synth_ice40_nobram synth_ice40_abc2 synth_ice40_vpr synth_ice40_relut synth_ice40_dsp synth_ice40_min_ce synth_ice40_noabc))
$(eval $(call template,synth_ice40_error,synth_ice40_fully_selected))
#intel
$(eval $(call template,synth_intel,synth_intel synth_intel_top synth_intel_vqm synth_intel_vpr synth_intel_run synth_intel_noflatten synth_intel_retime synth_intel_noiopads synth_intel_nobram synth_intel_max10 ))
......@@ -53,16 +60,20 @@ $(eval $(call template,synth_intel_cycloneive,synth_intel_cycloneive ))
$(eval $(call template,synth_intel_cyclonev ,synth_intel_cyclonev ))
$(eval $(call template,synth_intel_cyclone10,synth_intel_cyclone10 ))
$(eval $(call template,synth_intel_a10gx ,synth_intel_a10gx ))
$(eval $(call template,synth_intel_error ,synth_intel_fully_selected synth_intel_invalid_family ))
#sf2
$(eval $(call template,synth_sf2,synth_sf2 synth_sf2_top synth_sf2_edif synth_sf2_json synth_sf2_run synth_sf2_noflatten synth_sf2_retime synth_sf2_vlog synth_sf2_noiobs synth_sf2_clkbuf ))
$(eval $(call template,synth_sf2_error,synth_sf2_fully_selected ))
#xilinx
$(eval $(call template,synth_xilinx,synth_xilinx synth_xilinx_top synth_xilinx_blif synth_xilinx_edif synth_xilinx_run synth_xilinx_flatten synth_xilinx_retime synth_xilinx_vpr))
$(eval $(call template,synth_xilinx,synth_xilinx synth_xilinx_top synth_xilinx_blif synth_xilinx_edif synth_xilinx_run synth_xilinx_flatten synth_xilinx_retime synth_xilinx_vpr synth_xilinx_arch_xcup synth_xilinx_arch_xcu synth_xilinx_arch_xc7 synth_xilinx_arch_xc6s synth_xilinx_nobram synth_xilinx_nodram synth_xilinx_nosrl))
$(eval $(call template,synth_xilinx_error,synth_xilinx_fully_selected synth_xilinx_invalid_arch ))
$(eval $(call template,synth_xilinx_srl,synth_xilinx_srl))
#greenpak4
$(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
$(eval $(call template,synth_greenpak4_wide_ffs,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
$(eval $(call template,synth_greenpak4_error,synth_greenpak4_fully_selected synth_greenpak4_invalid_part))
.PHONY: all clean
architecture/scripts/synth_achronix_fully_selected.ys 0 → 100644
read_verilog ../top.v
select top2
synth_achronix
write_verilog synth.v
architecture/scripts/synth_anlogic_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_anlogic
write_verilog synth.v
architecture/scripts/synth_coolrunner2_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_coolrunner2
write_verilog synth.v
architecture/scripts/synth_easic_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_easic
write_verilog synth.v
architecture/scripts/synth_ecp5_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_ecp5
write_verilog synth.v
architecture/scripts/synth_gowin_fully_selected.ys 0 → 100644
read_verilog ../top.v
select top2
synth_gowin
write_verilog synth.v
architecture/scripts/synth_greenpak4_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_greenpak4
write_verilog synth.v
architecture/scripts/synth_greenpak4_invalid_part.ys 0 → 100644
read_verilog ../top.v
synth_greenpak4 -part ggg
write_verilog synth.v
architecture/scripts/synth_ice40_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_ice40
write_verilog synth.v
architecture/scripts/synth_intel_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_intel
write_verilog synth.v
architecture/scripts/synth_intel_invalid_family.ys 0 → 100644
read_verilog ../top.v
synth_intel -family u
write_verilog synth.v
architecture/scripts/synth_sf2_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_sf2
write_verilog synth.v
architecture/scripts/synth_xilinx_arch_xc6s.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch xc6s
write_verilog synth.v
architecture/scripts/synth_xilinx_arch_xc7.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch xc7
write_verilog synth.v
architecture/scripts/synth_xilinx_arch_xcu.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch xcu
write_verilog synth.v
architecture/scripts/synth_xilinx_arch_xcup.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch xcup
write_verilog synth.v
architecture/scripts/synth_xilinx_fully_selected.ys 0 → 100644
read_verilog ../top.v
select dffe
synth_xilinx
write_verilog synth.v
architecture/scripts/synth_xilinx_invalid_arch.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -arch zinq7000
write_verilog synth.v
architecture/scripts/synth_xilinx_nobram.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -nobram
write_verilog synth.v
architecture/scripts/synth_xilinx_nodram.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -nodram
write_verilog synth.v
architecture/scripts/synth_xilinx_nosrl.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -nosrl
write_verilog synth.v
architecture/scripts/synth_xilinx_nosrt.ys 0 → 100644
read_verilog ../top.v
synth_xilinx -nosrl
write_verilog synth.v
architecture/synth_achronix_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
wire patt_out,out;
wire patt_carry_out,carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
assign {patt_carry_out,patt_out} = in[2] + in[1] + in[0];
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
architecture/synth_achronix_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
architecture/synth_anlogic_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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
architecture/synth_anlogic_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_coolrunner2_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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, posedge dinA[2] )
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
architecture/synth_coolrunner2_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge en )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_easic_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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, posedge dinA[2] )
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
architecture/synth_easic_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge en )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_ecp5_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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
architecture/synth_ecp5_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_gowin_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
wire patt_out,out;
wire patt_carry_out,carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
assign {patt_carry_out,patt_out} = in[2] + in[1] + in[0];
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
architecture/synth_gowin_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
architecture/synth_greenpak4_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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
architecture/synth_greenpak4_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk)
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_ice40_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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
architecture/synth_ice40_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_ice40_mem/top.v
......@@ -24,7 +24,7 @@ module top
SB_RAM40_4K #(
.READ_MODE(2'h1),
.WRITE_MODE(2'h1),
.INIT_FILE("init.txt")
.INIT_FILE("../init.txt")
) \ram.0.0.0 (
.MASK(16'hxxxx),
.RADDR({ 5'h00, addr_a }),
......
architecture/synth_intel_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
wire patt_out,out;
wire patt_carry_out,carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
assign {patt_carry_out,patt_out} = in[2] + in[1] + in[0];
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
architecture/synth_intel_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
architecture/synth_sf2_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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, posedge dinA[2] )
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
architecture/synth_sf2_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge en )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
architecture/synth_xilinx_error/testbench.v 0 → 100644
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 ),
.b3 (doutB3 ),
.b4 (doutB4 )
);
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
architecture/synth_xilinx_error/top.v 0 → 100644
module adff
( input d, clk, clr, output reg q );
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
module dffe
( input d, clk, en, output reg q );
initial begin
q = 0;
end
always @( posedge clk )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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 )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
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
backends/Makefile
......@@ -52,7 +52,7 @@ $(eval $(call template,write_firrtl_paramod,write_firrtl))
#write_ilang
$(eval $(call template,write_ilang,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_mem,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_mem,write_ilang_mem))
$(eval $(call template,write_ilang_mux,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_fsm,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected))
......@@ -79,8 +79,8 @@ $(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_
#write_smv
$(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_wide,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_shift,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_wide,write_smv write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_shift,write_smv_shift))
$(eval $(call template,write_smv_fsm,write_smv write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_reduce,write_smv_noproc))
$(eval $(call template,write_smv_logic,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
......
backends/common.v
module assert_equal(input clk, input test, input pat);
always @(posedge clk)
begin
if (test != pat)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time);
$stop;
end
end
endmodule
module assert_dff(input clk, input test, input pat);
always @(posedge clk)
begin
......
backends/scripts/write_aiger.ys
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_B.ys
read_verilog -sv ../top.v
aigmap
write_aiger -B aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_I.ys
read_verilog -sv ../top.v
aigmap
write_aiger -I aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_O.ys
read_verilog -sv ../top.v
aigmap
write_aiger -O aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_ascii.ys
read_verilog -sv ../top.v
aigmap
write_aiger -ascii aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_map.ys
read_verilog -sv ../top.v
aigmap
write_aiger -map a.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_miter.ys
......@@ -2,4 +2,9 @@ read_verilog -sv ../top_clean.v
synth -top top
aigmap
write_aiger -miter aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_symbols.ys
read_verilog -sv ../top.v
aigmap
write_aiger -symbols aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_vmap.ys
read_verilog -sv ../top.v
aigmap
write_aiger -vmap a.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_ilang.ys
......@@ -4,4 +4,5 @@ proc
dump -o file.il
write_ilang ilang.ilang
dump -n -o file1.il
synth
write_verilog synth.v
backends/scripts/write_ilang_mem.ys 0 → 100644
read_verilog ../top.v
proc
memory
dump -o file.il
write_ilang ilang.ilang
dump -n -o file1.il
write_verilog synth.v
backends/scripts/write_smt2.ys
read_verilog ../top.v
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_bv.ys
read_verilog ../top.v
proc
memory
write_smt2 -bv smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_mem.ys
read_verilog ../top.v
proc
memory
write_smt2 -mem smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_mem_memtest.ys
read_verilog ../top.v
memory_collect
proc
memory
write_smt2 -mem smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_memtest.ys
read_verilog ../top.v
memory_collect
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_nomem.ys
read_verilog ../top.v
proc
memory
write_smt2 -nomem smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_stbv.ys
read_verilog ../top.v
proc
memory
write_smt2 -stbv smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_stbv_memtest.ys
read_verilog ../top.v
memory_collect
proc
memory
write_smt2 -stbv smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_stdt.ys
read_verilog ../top.v
proc
memory
write_smt2 -stdt smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_tpl.ys
read_verilog ../top.v
proc
memory
write_smt2 -tpl ../top.tpl smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_verbose.ys
read_verilog ../top.v
proc
memory
write_smt2 -verbose smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_wires.ys
read_verilog ../top.v
proc
memory
write_smt2 -wires smt2.smt2
write_verilog synth.v
backends/scripts/write_smv_shift.ys 0 → 100644
read_verilog ../top.v
proc
write_smv smv.smv
design -reset
read_verilog ../top_clean.v
proc
write_smv smv.smv
write_verilog synth.v
backends/write_simplec/testbench.v
......@@ -31,10 +31,10 @@ module testbench;
dinA <= !dinA;
end
assert_dff b_test(.clk(en), .test(dinA), .pat(dioB[0]));
assert_equal b_test(.clk(en), .test(dinA), .pat(dioB[0]));
assert_dff c_test(.clk(en), .test(dinA), .pat(doutC[0]));
assert_equal c_test(.clk(en), .test(dinA), .pat(doutC[0]));
assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
assert_equal cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
endmodule
bigsim/.gitignore
/.stamp
/.start
/*_cmos.status
/*_ice40.status
/*_falsify.status
/*_sim.status
/*/work_sim
/*/work_cmos
/*/work_ice40
......
bigsim/run.sh
......@@ -14,6 +14,12 @@ for fn in $RTL; do
rtl_files="$rtl_files ../rtl/$fn"
done
if [ -f "../../../../../techlibs/common/simcells.v" ]; then
TECHLIBS_PREFIX=../../../../../techlibs
else
TECHLIBS_PREFIX=/usr/local/share/yosys
fi
case "$2" in
sim)
touch ../../.start
......@@ -28,7 +34,7 @@ case "$2" in
;;
ice40)
yosys -ql synthlog.txt -p "synth_ice40 -top $TOP; write_verilog synth.v" $rtl_files
iverilog_cmd="$iverilog_cmd synth.v $(yosys-config --datdir/ice40/cells_sim.v)"
iverilog_cmd="$iverilog_cmd synth.v $TECHLIBS_PREFIX/ice40/cells_sim.v"
;;
*)
exit 1
......@@ -64,4 +70,6 @@ elif [ "$2" != "sim" ]; then
else
echo FAIL > ../../${1}_${2}.status
fi
elif [ "$2" == "sim" ]; then
echo PASS > ../../${1}_${2}.status
fi
frontends/Makefile
......@@ -39,7 +39,7 @@ $(eval $(call template,read_ilang_tri,read_ilang read_ilang_selected))
$(eval $(call template,read_json,read_json))
$(eval $(call template,read_json_fsm,read_json))
$(eval $(call template,read_json_logic,read_json))
$(eval $(call template,read_json_mem,read_json))
$(eval $(call template,read_json_mem,read_json_mem))
$(eval $(call template,read_json_mux,read_json))
$(eval $(call template,read_json_tri,read_json))
......
frontends/read/testbench.v
......@@ -27,7 +27,7 @@ module testbench;
);
assign patt_out = in[1] + in[2];
assign patt_carry_out = in[1] + patt_out;
assign patt_carry_out = in[0] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
......
frontends/read/top.v
......@@ -11,7 +11,7 @@ module top
`ifndef BUG
assign A = y + cin;
assign cout = y + A;
assign cout = x + A;
`else
assign {cout,A} = cin - y * x;
......
frontends/read_aiger_latch/testbench.v
......@@ -2,8 +2,8 @@ module testbench;
reg en;
initial begin
$dumpfile("testbench.vcd");
$dumpvars(0, testbench);
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
......
frontends/read_liberty_latch/testbench.v
......@@ -2,7 +2,7 @@ module testbench;
reg [2:0] in;
reg patt_out = 0;
wire out;
wire out = 0;
initial begin
// $dumpfile("testbench.vcd");
......
frontends/read_liberty_latch_n/testbench.v
......@@ -2,7 +2,7 @@ module testbench;
reg [2:0] in;
reg patt_out = 0;
wire out;
wire out = 0;
initial begin
// $dumpfile("testbench.vcd");
......
frontends/scripts/read_ilang.ys
read_verilog ../top.v
proc
memory
dump -o file.il
write_ilang ilang.ilang
design -reset
......
frontends/scripts/read_ilang_selected.ys
read_verilog ../top.v
proc
memory
dump -o file.il
write_ilang -selected ilang.ilang
design -reset
......
frontends/scripts/read_json.ys
read_verilog ../top.v
proc
write_json json.json
design -reset
read_json json.json
......
frontends/scripts/read_json_mem.ys 0 → 100644
read_verilog ../top.v
write_json json.json
design -reset
read_json json.json
design -reset
read_verilog ../top.v
proc
memory
write_verilog synth.v
misc/abc_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign cout = x / y * cin;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/add_error/top.v 0 → 100644
(* black_box *) module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/bugpoint_error/script.ys 0 → 100644
read_verilog ../top2.v
abc -g cmos4
misc/bugpoint_error/top.v 0 → 100644
module bb
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
bb u_bb (x,y,cin,A,cout);
endmodule
misc/bugpoint_error/top2.v 0 → 100644
module bb2
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
bb2 u_bb2 (x,y,cin,A,cout);
endmodule
misc/check/top.v
module top
( input d, clk, output reg q );
wire u;
always @( posedge clk )
q <= d;
endmodule
misc/check/top1.v 0 → 100644
module top
( input d, clk, output reg q );
wire u;
wire s;
assign u = s;
assign u = d;
assign u = clk;
always @( posedge clk )
q <= u;
endmodule
misc/check_error/top.v 0 → 100644
module top
( input d, clk, output reg q );
wire u;
wire s;
assign u = s;
assign u = d;
assign u = clk;
always @( posedge clk )
q <= u;
endmodule
misc/chformal_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
regression/issue_00940/TopEntity.v 0 → 100644
This source diff could not be displayed because it is too large. You can view the blob instead.
regression/issue_00981/top.v 0 → 100644
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment