Skip to content

Y
yosys-tests
Commit 10f53cb1 by SergeyDegtyar
Options

Add new tests to backends and architecture; 

Add new tests to backends and architecture;
Merge commit "Add regression test for Yosys PR 896"
parent 7a5e0b7b
Showing with 1762 additions and 84 deletions
architecture/Makefile
......@@ -29,7 +29,7 @@ $(eval $(call template,synth_anlogic_mem,synth_anlogic synth_anlogic_top synth_a
$(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))
#easic
#easic - issue #920
#$(eval $(call template,synth_easic,synth_easic synth_easic_top synth_easic_vlog synth_easic_run synth_easic_noflatten synth_easic_retime))
#ecp5
......@@ -41,21 +41,23 @@ $(eval $(call template,synth_gowin,synth_gowin synth_gowin_top synth_gowin_vout
$(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 ))
#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))
$(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))
$(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))
$(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))
#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 ))
$(eval $(call template,synth_intel_cycloneiv,synth_intel_cycloneiv ))
$(eval $(call template,synth_intel_cycloneive,synth_intel_cycloneive ))
# - issue #921
#../../../../../techlibs/intel/cyclonev/cells_sim.v:88: error: Unable to bind wire/reg/memory `upper_mask_value' in `testbench.uut._05_.lut5'
#$(eval $(call template,synth_intel_cyclonev ,synth_intel_cyclonev ))
$(eval $(call template,synth_intel_cyclone10,synth_intel_cyclone10 ))
$(eval $(call template,synth_intel_cyclone10,synth_intel_cyclone10 ))
$(eval $(call template,synth_intel_a10gx ,synth_intel_a10gx ))
#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 ))
$(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 ))
#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))
......
architecture/scripts/synth_ice40_dsp.ys 0 → 100644
read_verilog ../top.v
synth_ice40 -dsp
write_verilog synth.v
architecture/scripts/synth_ice40_min_ce.ys 0 → 100644
read_verilog ../top.v
synth_ice40 -dffe_min_ce_use 2
write_verilog synth.v
architecture/scripts/synth_ice40_noabc.ys 0 → 100644
read_verilog ../top.v
synth_ice40 -noabc
write_verilog synth.v
architecture/scripts/synth_ice40_relut.ys 0 → 100644
read_verilog ../top.v
synth_ice40 -relut
write_verilog synth.v
architecture/scripts/synth_sf2_clkbuf.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -clkbuf
write_verilog synth.v
architecture/scripts/synth_sf2_noiobs.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -noiobs
write_verilog synth.v
architecture/scripts/synth_sf2_vlog.ys 0 → 100644
read_verilog ../top.v
synth_sf2 -vlog vlog.v
write_verilog synth.v
backends/Makefile
......@@ -25,6 +25,9 @@ $(eval $(call template,write_blif,write_blif write_blif_top write_blif_buf write
#write_btor
$(eval $(call template,write_btor,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_shift,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_div_mod,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_fsm,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_logic,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor_mem_s))
$(eval $(call template,write_btor_pmux,write_btor_pmux))
......@@ -35,6 +38,7 @@ $(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc
#write_firrtl
$(eval $(call template,write_firrtl,write_firrtl ))
# - issue #922
#ERROR: Unclocked write port 0 on memory top.ram.
#$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
......@@ -49,7 +53,7 @@ $(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected))
$(eval $(call template,write_intersynth,write_intersynth write_intersynth_selected write_intersynth_lib write_intersynth_notypes))
#write_json
$(eval $(call template,write_json,write_json write_json_aig))
$(eval $(call template,write_json,write_json write_json_aig json json_o json_o_aig json_aig))
#write_simplec
$(eval $(call template,write_simplec,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
......@@ -66,6 +70,8 @@ $(eval $(call template,write_smt2_reduce,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_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))
......@@ -78,6 +84,13 @@ $(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_e
#write_table
$(eval $(call template,write_table,write_table ))
#write_verilog
$(eval $(call template,write_verilog,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_tri,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_ffs,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_latch,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
$(eval $(call template,write_verilog_concat,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
.PHONY: all clean
backends/scripts/json.ys 0 → 100644
read_verilog ../top.v
proc
json
write_verilog synth.v
backends/scripts/json_aig.ys 0 → 100644
read_verilog ../top.v
proc
json -aig
write_verilog synth.v
backends/scripts/json_o.ys 0 → 100644
read_verilog ../top.v
proc
json -o json.json
write_verilog synth.v
backends/scripts/json_o_aig.ys 0 → 100644
read_verilog ../top.v
proc
json -aig -o json.json
write_verilog synth.v
backends/scripts/write_btor.ys
read_verilog -sv ../top.v
synth -top top
hierarchy -top top
proc
write_btor btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor btor1.btor
design -reset
read_verilog -sv ../top.v
proc_init
proc_mux
proc_dff
write_btor btor.btor
write_btor btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor btor.btor
write_btor btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor btor.btor
write_btor btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor btor.btor
write_btor btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor btor.btor
write_btor btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor btor.btor
write_btor btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor btor.btor
write_btor btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor btor9.btor
synth -top top
write_btor btor.btor
write_btor btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_btor_mem.ys
read_verilog -sv ../top.v
memory_collect
memory
proc
write_btor btor.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
write_btor btor1.btor
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor btor9.btor
synth -top top
write_btor btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_btor_mem_s.ys
......@@ -5,4 +5,51 @@ write_btor -s btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor -s btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor -s btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor -s btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor -s btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor -s btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor -s btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor -s btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
backends/scripts/write_btor_mem_v.ys
......@@ -3,6 +3,58 @@ memory_collect
proc
write_btor -v btor.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
write_btor -v btor1.btor
design -reset
read_verilog -sv ../top.v
synth -top top
design -reset
read_verilog -sv ../top.v
memory
synth
abc
write_btor -v btor3.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g AND,XOR,NOR
write_btor -v btor4.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g ANDNOT,ORNOT
write_btor -v btor5.btor
design -reset
read_verilog -sv ../top.v
memory
synth -top top
abc -g cmos3
write_btor -v btor6.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g AOI4
synth -top top
write_btor -v btor7.btor
design -reset
read_verilog -sv ../top.v
memory
abc -g OAI4
synth -top top
write_btor -v btor8.btor
design -reset
read_verilog -sv ../top.v
memory
aigmap
proc
write_btor -v btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_btor_s.ys
read_verilog -sv ../top.v
synth -top top
proc
write_btor -s btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor -s btor1.btor
design -reset
read_verilog -sv ../top.v
proc_init
proc_mux
proc_dff
write_btor -s btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor -s btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor -s btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor -s btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor -s btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor -s btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor -s btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor -s btor9.btor
synth -top top
write_btor -s btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_btor_v.ys
read_verilog -sv ../top.v
synth -top top
proc
write_btor -v btor.btor
design -reset
read_verilog -sv ../top.v
synth -top top
write_btor -v btor1.btor
design -reset
read_verilog -sv ../top.v
proc_init
proc_mux
proc_dff
write_btor -v btor2.btor
design -reset
read_verilog -sv ../top.v
synth
abc
write_btor -v btor3.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g AND,XOR,NOR
write_btor -v btor4.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g ANDNOT,ORNOT
write_btor -v btor5.btor
design -reset
read_verilog -sv ../top.v
synth -top top
abc -g cmos3
write_btor -v btor6.btor
design -reset
read_verilog -sv ../top.v
abc -g AOI4
synth -top top
write_btor -v btor7.btor
design -reset
read_verilog -sv ../top.v
abc -g OAI4
synth -top top
write_btor -v btor8.btor
design -reset
read_verilog -sv ../top.v
aigmap
proc
write_btor -v btor9.btor
synth -top top
write_btor -v btor10.btor
design -reset
read_verilog -sv ../top_clean.v
synth -top top
write_verilog synth.v
backends/scripts/write_ilang.ys
read_verilog ../top.v
write_ilang ilang.ilang
proc
dump -o file.il
write_ilang ilang.ilang
dump -n -o file1.il
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_ilang_selected.ys
read_verilog ../top.v
write_ilang -selected ilang.ilang
proc
dump -a file.il
write_ilang -selected ilang.ilang
dump -m -a file1.il
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_verilog.ys 0 → 100644
read_verilog ../top.v
proc
tribuf
dff2dffe
write_verilog synth.v
backends/scripts/write_verilog_nostr.ys 0 → 100644
read_verilog ../top.v
proc
tribuf
dff2dffe
write_verilog -nostr synth.v
backends/scripts/write_verilog_siminit.ys 0 → 100644
read_verilog ../top.v
proc
tribuf
dff2dffe
write_verilog -siminit synth.v
backends/scripts/write_verilog_v.ys 0 → 100644
read_verilog ../top.v
proc
dff2dffe
write_verilog -v synth.v
backends/write_btor_div_mod/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out = 0;
wire carryout = 0;
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)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_btor_div_mod/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output reg B,C
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
A <= y / too;
end
always @(posedge x) begin
cout <= y + A % foo;
end
assign {B,C} = {cout,A} << 1;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_btor_div_mod/top_clean.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_btor_fsm/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 a = 0;
reg b = 0;
reg rst;
reg en;
wire s;
wire bs;
wire f;
top uut ( .clk(clk),
.rst(rst),
.en(en),
.a(a),
.b(b),
.s(s),
.bs(bs),
.f(f));
always @(posedge clk)
begin
#2
a <= ~a;
end
always @(posedge clk)
begin
#4
b <= ~b;
end
initial begin
en <= 1;
rst <= 1;
#5
rst <= 0;
end
assert_expr s_test(.clk(clk), .A(s));
assert_expr bs_test(.clk(clk), .A(bs));
assert_expr f_test(.clk(clk), .A(f));
endmodule
module assert_expr(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
backends/write_btor_fsm/top.v 0 → 100644
module top (
input clk,
input rst,
input en,
input a,
input b,
output s,
output bs,
output f
);
parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
reg [3:0] ns, st;
reg [2:0] count;
always @(posedge clk)
begin : CurrstProc
if (rst)
st <= S0;
else
st <= ns;
end
always @*
begin : NextstProc
ns = st;
case (st)
S0: ns = S1;
S1: ns = S2;
S2:
if (b == 1'b1)
ns = S3;
else
ns = S4;
S3: ns = S1;
S4: if (count > 7)
ns = S10;
else
ns = S5;
S5: if (a == 1'b0)
ns = S6;
else
ns = S3;
S6:
if (a == 1'b1)
ns = S7;
else
ns = S8;
S7:
if (a == 1'b1 && b == 1'b1)
ns = S5;
else
ns = S13;
S8: ns = S9;
S9: ns = S8;
S10:
if (a == 1'b1 || b == 1'b1)
ns = S11;
else
ns = S4;
S11: ns = S12;
S12: ns = S10;
S13: ;
default: ns = S0;
endcase;
end
always @(posedge clk)
if(~rst)
count <= 0;
else
begin
if(st == S4)
if (count > 7)
count <= 0;
else
count <= count + 1;
end
//FSM outputs (combinatorial)
assign s = (st == S3 || st == S12) ? 1'b1 : 1'b0;
assign f = (st == S13) ? 1'b1 : 1'b0;
assign bs = (st == S8 || st == S9) ? 1'b1 : 1'b0;
endmodule
backends/write_btor_fsm/top_clean.v 0 → 100644
module top (
input clk,
input rst,
input en,
input a,
input b,
output s,
output bs,
output f
);
parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
reg [3:0] ns, st;
reg [2:0] count;
always @(posedge clk)
begin : CurrstProc
if (rst)
st <= S0;
else
st <= ns;
end
always @*
begin : NextstProc
ns = st;
case (st)
S0: ns = S1;
S1: ns = S2;
S2:
if (b == 1'b1)
ns = S3;
else
ns = S4;
S3: ns = S1;
S4: if (count > 7)
ns = S10;
else
ns = S5;
S5: if (a == 1'b0)
ns = S6;
else
ns = S3;
S6:
if (a == 1'b1)
ns = S7;
else
ns = S8;
S7:
if (a == 1'b1 && b == 1'b1)
ns = S5;
else
ns = S13;
S8: ns = S9;
S9: ns = S8;
S10:
if (a == 1'b1 || b == 1'b1)
ns = S11;
else
ns = S4;
S11: ns = S12;
S12: ns = S10;
S13: ;
default: ns = S0;
endcase;
end
always @(posedge clk)
if(~rst)
count <= 0;
else
begin
if(st == S4)
if (count > 7)
count <= 0;
else
count <= count + 1;
end
//FSM outputs (combinatorial)
assign s = (st == S3 || st == S12) ? 1'b1 : 1'b0;
assign f = (st == S13) ? 1'b1 : 1'b0;
assign bs = (st == S8 || st == S9) ? 1'b1 : 1'b0;
endmodule
backends/write_btor_logic/top.v
......@@ -7,9 +7,9 @@ module top
output reg A,
output reg cout
);
reg A1,cout1;
initial begin
A = 0;
cout = 0;
......@@ -20,7 +20,7 @@ always @(posedge x) begin
A1 <= ~y + &cin;
end
always @(posedge x) begin
cout1 <= cin ? |y : ^A;
cout1 <= cin ? |y : ~^A;
end
always @(posedge x) begin
......
backends/write_btor_shift/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out = 0;
wire carryout = 0;
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)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_btor_shift/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output reg B,C
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
A <= y >> too;
end
always @(posedge x) begin
cout <= y + A >>> foo;
end
assign {B,C} = {cout,A} << 1;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_btor_shift/top_clean.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_smv_cmos4/testbench.v
module testbench;
reg [0:7] in;
wire patt_B;
wire B;
wire x,y,z,A;
reg clk;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
#5 clk = 0;
repeat (10000) begin
#5 in = in + 1;
#5 clk = 1;
#5 clk = 0;
end
$display("OKAY");
$display("OKAY");
end
reg [15:0] D = 1;
reg [3:0] S = 0;
wire M16;
top uut (
.x(in[1:2]),
.y(in[3:4]),
.z(in[5:6]),
.clk(in[0]),
.A(in[7]),
.B(B)
);
assign patt_B = (x || y || !z)? (A & z) : ~x;
assign x = in[1:2];
assign y = in[3:4];
assign z = in[5:6];
assign A = in[7];
.S (S ),
.D (D ),
.M16 (M16 )
);
always @(posedge clk) begin
//#3;
D <= {D[14:0],D[15]};
//D <= D <<< 1;
S <= S + 1;
end
assert_comb out_test(.A(patt_B), .B(B));
assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
endmodule
backends/write_smv_cmos4/top.v
module top
(
input x,
input y,
input z,
input clk,
input A,
output signed B,
output signed C,D,E
);
`ifndef BUG
assign B = (x || y || !z)? (A & z) : ~x;
assign {D,C} = {y,z} >>> 1;
assign E = {x,y,z} / 3;
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
`ifndef BUG
assign Y = D[S];
`else
assign B = z - y + x;
assign Y = D[S+1];
`endif
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M16
);
`endif
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule
backends/write_smv_shift/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out = 0;
wire carryout = 0;
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)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_smv_shift/top.tpl 0 → 100644
; we need QF_UFBV for this poof
(set-logic QF_UFBV)
; insert the auto-generated code here
%%
; declare two state variables s1 and s2
(declare-fun s1 () test_s)
(declare-fun s2 () test_s)
; state s2 is the successor of state s1
(assert (test_t s1 s2))
; we are looking for a model with y non-zero in s1
(assert (distinct (|test_n y| s1) #b0000))
; we are looking for a model with y zero in s2
(assert (= (|test_n y| s2) #b0000))
; is there such a model?
(check-sat)
backends/write_smv_shift/top.v 0 → 100644
module top
(
input signed x,
input signed y,
input signed cin,
output signed A,
output signed cout,
output signed B,C
);
`ifndef BUG
assign A = y >> x;
assign cout = y + A >>> y;
assign {B,C} = {cout,A} << 1;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_smv_shift/top_clean.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_smv_wide/testbench.v 0 → 100644
module testbench;
reg en;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg [3:0] dinA = 0;
wire [3:0] dioB;
wire [1:0] doutC;
top uut (
.en (en ),
.a (dinA ),
.b (dioB ),
.c (doutC )
);
always @(posedge en) begin
#3;
dinA <= dinA + 1;
end
assert_dff b_test(.clk(en), .test(dinA[0]), .pat(dioB[0]));
//assert_dff c_test(.clk(en), .test(dinA[0]), .pat(doutC[0]));
assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
endmodule
backends/write_smv_wide/top.tpl 0 → 100644
; we need QF_UFBV for this poof
(set-logic QF_UFBV)
; insert the auto-generated code here
%%
; declare two state variables s1 and s2
(declare-fun s1 () test_s)
(declare-fun s2 () test_s)
; state s2 is the successor of state s1
(assert (test_t s1 s2))
; we are looking for a model with y non-zero in s1
(assert (distinct (|test_n y| s1) #b0000))
; we are looking for a model with y zero in s2
(assert (= (|test_n y| s2) #b0000))
; is there such a model?
(check-sat)
backends/write_smv_wide/top.v 0 → 100644
module tristate (en, i, io, o);
input en;
input [3:0] i;
inout [3:0] io;
output [1:0] o;
wire [3:0] io;
`ifndef BUG
assign io[1:0] = (en)? i[1:0] : 1'bZ;
assign io[3:2] = (i[1:0])? en : 1'bZ;
assign o = io[2:1];
`else
assign io[1:0] = (en)? ~i[1:0] : 1'bZ;
assign io[3:2] = (i[1:0])? ~en : 1'bZ;
assign o = ~io[2:1];
`endif
endmodule
module top (
input en,
input [3:0] a,
inout [3:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
backends/write_verilog/testbench.v 0 → 100644
module testbench;
reg en;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg [3:0] dinA = 0;
wire [3:0] dioB;
wire [1:0] doutC;
top uut (
.en (en ),
.a (dinA ),
.b (dioB ),
.c (doutC )
);
always @(posedge en) begin
#3;
dinA <= dinA + 1;
end
assert_dff b_test(.clk(en), .test(dinA[0]), .pat(dioB[0]));
//assert_dff c_test(.clk(en), .test(dinA[0]), .pat(doutC[0]));
assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
endmodule
backends/write_verilog/top.v 0 → 100644
module tristate (en, i, io, o);
input en;
input [3:0] i;
inout [3:0] io;
output [1:0] o;
wire [3:0] io;
`ifndef BUG
assign io[1:0] = (en)? i[1:0] : 1'bZ;
assign io[3:2] = (i[1:0])? en : 1'bZ;
assign o = io[2:1];
`else
assign io[1:0] = (en)? ~i[1:0] : 1'bZ;
assign io[3:2] = (i[1:0])? ~en : 1'bZ;
assign o = ~io[2:1];
`endif
endmodule
module top (
input en,
input [3:0] a,
inout [3:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
backends/write_verilog_concat/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
wire [1:0] Ap = 0;
wire [2:0] Bp = 0;
wire [2:0] Cp = 0;
wire [1:0] A = 0;
wire [2:0] B = 0;
wire [2:0] C = 0;
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[2:1]),
.z(in[3]),
.A(A),
.B(B),
.C(C)
);
assign Ap = {in[0],in[3]};
assign Bp = {in[0],in[2:1]};
assign Cp = {in[0],in[2:1],in[3]};
assert_comb A_test(.A(A[0]), .B(Ap[0]));
assert_comb B_test(.A(B[0]), .B(Bp[0]));
assert_comb C_test(.A(C[0]), .B(Cp[0]));
endmodule
backends/write_verilog_concat/top.v 0 → 100644
module top
(
input x,
input [1:0] y,
input z,
output [1:0] A,
output [2:0] B,
output [3:0] C
);
`ifndef BUG
assign A = {x,z};
assign B = {x,y};
assign C = {x,y,z};
`else
assign A = x + z;
assign B = x * y;
assign C = x - y - z;
`endif
endmodule
module test(input [7:0] A, B, output [7:0] Y);
wire [15:0] AB = (A * B) + {A, B}; // merging to create {A, B}
assign Y = AB[15:8] + AB[7:0]; // splitting to create AB[15:8] and AB[7:0]
endmodule
backends/write_verilog_ffs/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
backends/write_verilog_ffs/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/write_verilog_latch/testbench.v 0 → 100644
module testbench;
reg en;
initial begin
$dumpfile("testbench.vcd");
$dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg [2:0] dinA = 0;
wire doutB,doutB1,doutB2,doutB3;
reg lat,nlat,alat,alatn = 0;
top uut (
.en (en ),
.a (dinA[0] ),
.pre (dinA[1] ),
.clr (dinA[2] ),
.b (doutB ),
.b1 (doutB1 ),
.b2 (doutB2 ),
.b3 (doutB3 )
);
always @(posedge en) begin
#3;
dinA <= dinA + 1;
end
always @( en or dinA[0] or dinA[1] or dinA[2] )
if ( dinA[2] )
lat <= 1'b0;
else if ( dinA[1] )
lat <= 1'b1;
else if ( en )
lat <= dinA[0];
always @( en or dinA[0] or dinA[1] or dinA[2] )
if ( !dinA[2] )
nlat <= 1'b0;
else if ( !dinA[1] )
nlat <= 1'b1;
else if (!en)
nlat <= dinA[0];
always @( en or dinA[0] or dinA[2] )
if ( dinA[2] )
alat <= 1'b0;
else if (en)
alat <= dinA[0];
always @( en or dinA[0] or dinA[2] )
if ( !dinA[2] )
alatn <= 1'b0;
else if (!en)
alatn <= dinA[0];
assert_dff lat_test(.clk(en), .test(doutB), .pat(lat));
assert_dff nlat_test(.clk(en), .test(doutB1), .pat(nlat));
assert_dff alat_test(.clk(en), .test(doutB2), .pat(alat));
assert_dff alatn_test(.clk(en), .test(doutB3), .pat(alatn));
endmodule
backends/write_verilog_latch/top.v 0 → 100644
module alat
( input d, en, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if (en)
q <= d;
endmodule
module alatn
( input d, en, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if (!en)
q <= d;
endmodule
module latsr
( input d, en, pre, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else if ( en )
q <= d;
endmodule
module nlatsr
( input d, en, pre, clr, output reg q );
initial begin
q = 0;
end
always @(*)
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else if ( !en )
q <= d;
endmodule
module top (
input en,
input clr,
input pre,
input a,
output b,b1,b2,b3
);
latsr u_latsr (
.en (en ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b )
);
nlatsr u_nlatsr (
.en (en ),
.clr (clr),
.pre (pre),
.d (a ),
.q (b1 )
);
alat u_alat (
.en (en ),
.clr (clr),
.d (a ),
.q (b2 )
);
alatn u_alatn (
.en (en ),
.clr (clr),
.d (a ),
.q (b3 )
);
endmodule
backends/write_verilog_tri/testbench.v 0 → 100644
module testbench;
reg en;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg dinA = 0;
wire [1:0] dioB;
wire [1:0] doutC;
top uut (
.en (en ),
.a (dinA ),
.b (dioB ),
.c (doutC )
);
always @(posedge en) begin
#3;
dinA <= !dinA;
end
assert_dff b_test(.clk(en), .test(dinA), .pat(dioB[0]));
assert_dff c_test(.clk(en), .test(dinA), .pat(doutC[0]));
assert_dff cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
endmodule
backends/write_verilog_tri/top.v 0 → 100644
module tristate (en, i, io, o);
input en;
input i;
inout [1:0] io;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
equiv/scripts/equiv_add.ys
......@@ -10,6 +10,8 @@ design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
equiv_make gold gate equiv
design -save something
design -push
equiv_add gold gate
design -reset
read_verilog ../top.v
......
misc/Makefile
......@@ -55,7 +55,7 @@ $(eval $(call template,scatter, scatter ))
$(eval $(call template,rename, rename rename_top rename_src rename_hide rename_enumerate rename_enumerate_pat rename_wire))
#qwp
#qwp_v - exception
#qwp_v - exception (issue #923)
#+ yosys -ql yosys.log ../../scripts/qwp_v.ys
#run.sh: line 11: 28262 Floating point exception(core dumped) yosys -ql yosys.log ../../scripts/$2.ys
$(eval $(call template,qwp, qwp qwp_ltr qwp_grid qwp_dump qwp_alpha))
......@@ -74,7 +74,8 @@ $(eval $(call template,delete_mem, delete_mem ))
$(eval $(call template,cover, cover cover_q cover_o cover_dir cover_a ))
#insbuf ERROR: Found error in internal cell
#$(eval $(call template,insbuf,insbuf insbuf_cell))
#insbuf_cell - issue #924
$(eval $(call template,insbuf,insbuf))
#add
$(eval $(call template,add, add add_wire add_input add_output add_inout add_global_input ))
......@@ -82,6 +83,7 @@ $(eval $(call template,add, add add_wire add_input add_output add_inout add_glob
#blackbox
$(eval $(call template,blackbox, blackbox ))
# - issue #925
#bugpoint ERROR: No such command: autoidx (type 'help' for a command overview)
#$(eval $(call template,bugpoint, bugpoint bugpoint_yosys bugpoint_script bugpoint_grep bugpoint_fast bugpoint_clean bugpoint_modules bugpoint_ports bugpoint_cells bugpoint_connections ))
......@@ -93,8 +95,7 @@ $(eval $(call template,chformal_dff, chformal chformal_assert2assume chformal_as
$(eval $(call template,chtype, chtype chtype_map chtype_selection chtype_set))
#connect
#connect_nomap_port connect_port - ERROR: Can't find cell $2.
$(eval $(call template,connect, connect_nomap_set connect_nomap_unset connect_nounset_set connect_set connect_unset))
$(eval $(call template,connect, connect_nomap_set connect_nomap_unset connect_nounset_set connect_set connect_unset connect_port connect_nomap_port))
#connwrappers
$(eval $(call template,connwrappers, connwrappers connwrappers_signed connwrappers_unsigned connwrappers_port ))
......@@ -104,7 +105,7 @@ $(eval $(call template,plugin, plugin plugin_i plugin_a plugin_l ))
#select
$(eval $(call template,select, select select_all select_add select_add_all select_assert_any select_assert_count select_assert_max select_assert_min select_assert_none select_clear select_count select_del select_list select_module select_none select_read select_set select_write select_add_A_eq select_add_a_eq select_add_A_lesseq select_add_a_lesseq select_add_A_less select_add_a_less select_add_A_moreeq select_add_a_moreeq select_add_A_more select_add_a_more select_add_A select_add_a select_add_c select_add_i select_add_mid select_add_m select_add_n select_add_obj select_add_o select_add_p select_add_r_eq select_add_r_lesseq select_add_r_less select_add_r_moreeq select_add_r_more select_add_r select_add_ss select_add_s select_add_t select_add_w select_add_x ))
$(eval $(call template,select_mem, select select_all select_add select_add_all select_assert_any select_assert_count_mem select_assert_max_mem select_assert_min select_assert_none select_clear select_count select_del select_list select_module_mem select_none select_read select_set select_write select_add_A_eq select_add_a_eq select_add_A_lesseq select_add_a_lesseq select_add_A_less select_add_a_less select_add_A_moreeq select_add_a_moreeq select_add_A_more select_add_a_more select_add_A select_add_a select_add_c select_add_i select_add_mid select_add_m select_add_n select_add_obj select_add_o select_add_p select_add_r_eq select_add_r_lesseq select_add_r_less select_add_r_moreeq select_add_r_more select_add_r select_add_ss select_add_s select_add_t select_add_w select_add_x ))
$(eval $(call template,select_mem, select select_all select_add select_add_all select_assert_any select_assert_count_mem select_assert_max_mem select_assert_min select_assert_none select_clear select_count select_del select_list select_module_mem ))
$(eval $(call template,select_ls, select_ls select_ls_top))
$(eval $(call template,select_cd, select_cd select_cd_up select_cd_module ))
$(eval $(call template,select_stack,select_%a select_%cie select_%ci select_%coe select_%co select_%C select_%c select_%i select_%M select_%m select_%n select_%R4 select_%R select_%s select_%u select_%x_%D select_%x_%d select_%xe select_%))
......@@ -113,7 +114,7 @@ $(eval $(call template,select_stack,select_%a select_%cie select_%ci select_%coe
$(eval $(call template,setattr, setattr setattr_mod setattr_set setattr_top setattr_unset setattr_set_proc ))
$(eval $(call template,setattr_mem, setattr setattr_mod setattr_set setattr_top setattr_unset setattr_set_proc ))
#setparam
#setparam_type
#setparam_type - issue #926
#ERROR: Found error in internal cell \top.$procdff$4 ($dff) at kernel/rtlil.cc:715:
$(eval $(call template,setparam, setparam setparam_set setparam_unset setparam_top ))
#chparam
......@@ -138,7 +139,7 @@ $(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
$(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
#sat
#sat_tempinduct_def sat_tempinduct_tempinduct_def
#sat_tempinduct_def sat_tempinduct_tempinduct_def - issue #883
#ERROR: Assert `!undef_mode || model_undef' failed in ./kernel/satgen.h:90.
$(eval $(call template,sat, sat_dump_cnf sat_dump_json sat_dump_vcd sat_initsteps sat_maxsteps sat_max sat_prove_x sat_set_all_undef_at sat_set_all_undef sat_set_any_undef_at sat_set_any_undef sat_set_def_at sat_set_def sat_set_init sat_set sat_show sat_stepsize sat_tempinduct_skip sat_unset_at sat_set_at sat_seq sat_prove_skip sat_timeout sat_prove sat_tempinduct sat sat_all sat_ignore_unknown_cells sat_enable_undef sat_max_undef sat_show_inputs sat_show_outputs sat_show_ports sat_show_regs sat_show_public sat_show_all sat_set_assumes sat_set_init_undef sat_set_init_def sat_set_init_zero sat_tempinduct_baseonly sat_tempinduct_inductonly sat_verify sat_verify_no_timeout sat_falsify sat_falsify_no_timeout sat_prove_asserts sat_tempinduct_tempinduct_baseonly sat_set_def_inputs sat_tempinduct_baseonly_maxsteps ))
......
misc/scripts/connect_nomap_port.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -port $dff d q
tee -o result.log connect -nomap -port $procdff$2 D d
misc/scripts/connect_port.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -port $2 d q
tee -o result.log connect -port $procdff$2 D d
misc/scripts/insbuf_cell.ys
read_verilog ../top.v
synth
insbuf -buf $_BUF_ in out
insbuf -buf $_BUF_ in in
write_verilog synth.v
regression/Makefile
......@@ -10,7 +10,7 @@ $(foreach script,$(2),
work:: $(design)/work_$(script)/.stamp
$(design)/work_$(script)/.stamp:
bash run.sh $(design) $(script)
./run.sh $(design) $(script)
clean::
rm -rf $(design)/work_$(script)
......@@ -298,7 +298,7 @@ $(eval $(call template,issue_00763,issue_00763))
$(eval $(call template,issue_00767,issue_00767))
#issue_00774
$(eval $(call template,issue_00774,issue_00774))
#$(eval $(call template,issue_00774,issue_00774))
#issue_00781
$(eval $(call template,issue_00781,issue_00781))
......@@ -339,6 +339,7 @@ $(eval $(call template,issue_00862,issue_00862))
#issue_00865 - test failed (should be ok after merge https://github.com/YosysHQ/yosys/pull/866)
$(eval $(call template,issue_00865,issue_00865))
$(eval $(call template,pr_00896,pr_00896))
.PHONY: all clean
regression/pr_00896/outreg.v 0 → 100644
module dut(
input fast_clk, slow_clk,
input [3:0] waddr, raddr,
input [3:0] wdata,
input wen,
output [3:0] rdata
);
reg [3:0] mem[0:15];
reg [3:0] raddr_reg;
always @(posedge fast_clk) begin
if (wen)
mem[waddr] <= wdata;
end
always @(posedge slow_clk)
raddr_reg <= raddr;
assign rdata = mem[raddr_reg];
endmodule
regression/pr_00896/testbench.v 0 → 100644
`include "../outreg.v"
module tb;
reg fast_clk, slow_clk;
initial begin
$dumpfile("testbench.vcd");
$dumpvars(0, tb);
repeat (80) @(posedge slow_clk);
$display("OKAY");
$finish;
end
always #4 fast_clk = (fast_clk === 1'b0);
always #12 slow_clk = (slow_clk === 1'b0);
reg [7:0] wdata = 1;
always @(posedge fast_clk) wdata <= {wdata[6:0], wdata[7] ^ wdata[2]};
reg [3:0] waddr = 0;
always @(posedge fast_clk) waddr <= waddr + 1'b1;
reg [3:0] raddr = 0;
always @(posedge slow_clk) raddr <= raddr + 1'b1;
wire [3:0] rdata, rdata_postsyn;
dut dut_i(
.fast_clk(fast_clk), .slow_clk(slow_clk),
.raddr(raddr), .waddr(waddr), .wen(1'b1),
.wdata(wdata[3:0]), .rdata(rdata)
);
dut_syn dut_syn_i(
.fast_clk(fast_clk), .slow_clk(slow_clk),
.raddr(raddr), .waddr(waddr), .wen(1'b1),
.wdata(wdata[3:0]), .rdata(rdata_postsyn)
);
always @(posedge fast_clk)
if (rdata_postsyn != rdata) begin
$display("ERROR");
$finish;
end
endmodule
regression/run.sh
......@@ -150,6 +150,8 @@ else
[ "$1" = "issue_00589" ] ||\
[ "$1" = "issue_00628" ]; then
iverilog_adds="../../../../../techlibs/ice40/cells_sim.v"
elif [ "$1" = "pr_00896" ]; then
iverilog_adds="../../../../../techlibs/ecp5/cells_sim.v"
fi
yosys -ql yosys.log ../../scripts/$2.ys
......
regression/scripts/pr_00896.ys 0 → 100644
read_verilog ../outreg.v
synth_ecp5
rename dut dut_syn
write_verilog -norename synth.v
simple/Makefile
......@@ -66,7 +66,6 @@ $(eval $(call template,zinit,zinit zinit_singleton))
$(eval $(call template,clk2fflogic,clk2fflogic))
$(eval $(call template,clk2fflogic_latch,clk2fflogic))
$(eval $(call template,clk2fflogic_mem,clk2fflogic_mem))
# ??? one loop isn't reached $(eval $(call template,clk2fflogic_mem2,clk2fflogic_mem))
#muxcover
$(eval $(call template,muxcover,muxcover muxcover_nodecode muxcover_mux4 muxcover_mux4_nodecode muxcover_mux8 muxcover_mux8_nodecode muxcover_mux16 muxcover_mux16_nodecode muxcover_4_8_16_nodecode))
......
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