Skip to content

Y
yosys-tests
Commit 7be25b8c by SergeyDegtyar
Options

Add new tests to backends and frontends; Fix some tests from reported issues

parent 10f53cb1
Showing with 1731 additions and 6 deletions
backends/Makefile
......@@ -32,15 +32,22 @@ $(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))
$(eval $(call template,write_btor_and_or,write_btor_and_or))
$(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s))
#write_edif
$(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc write_edif_pvector_par write_edif_pvector_bra write_edif_pvector_ang write_edif_attrprop ))
#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 ))
$(eval $(call template,write_firrtl,write_firrtl write_firrtl))
#write_firrtl_mem_wr - issue #938
#terminate called after throwing an instance of 'std::out_of_range'
# what(): dict::at()
#run.sh: line 11: 9808 Aborted (core dumped)
$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
$(eval $(call template,write_firrtl_logic,write_firrtl ))
$(eval $(call template,write_firrtl_reduce,write_firrtl ))
$(eval $(call template,write_firrtl_shift,write_firrtl ))
$(eval $(call template,write_firrtl_shiftx,write_firrtl ))
#write_ilang
$(eval $(call template,write_ilang,write_ilang write_ilang_selected))
......@@ -67,6 +74,7 @@ $(eval $(call template,write_smt2_mem,write_smt2 write_smt2_verbose write_smt2_s
$(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_init_assert,write_smt2_init_assert))
$(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
#write_smv
$(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
......@@ -77,6 +85,7 @@ $(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))
$(eval $(call template,write_smv_init_assert,write_smv_init_assert))
$(eval $(call template,write_smv_cmos4,write_smv_cmos4))
$(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
#write_spice
$(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_endian write_spice_neg_i write_spice_pos_i write_spice_nc_prefix write_spice_inames ))
......@@ -90,6 +99,7 @@ $(eval $(call template,write_verilog_tri,write_verilog write_verilog_nostr write
$(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 ))
$(eval $(call template,write_verilog_shiftx,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
......
backends/scripts/write_firrtl_mem.ys
read_verilog ../top.v
memory_collect
proc
memory_dff -nordff
memory_collect
opt_reduce
clean
write_firrtl firrtl.firrtl
write_verilog synth.v
write_verilog synth.v
backends/scripts/write_firrtl_mem_wr.ys 0 → 100644
read_verilog ../top.v
proc
memory_dff -nordff
opt_reduce
clean
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/write_btor_shiftx/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
wire out,y;
top uut (
.a(in),
.y(out)
);
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[in];
assert_comb out_test(.A(y), .B(out));
endmodule
backends/write_btor_shiftx/top.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_btor_shiftx/top_clean.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input [4:0] a;
output y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_firrtl_logic/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
reg patt_out1 = 0;
reg patt_carry_out1 = 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]) begin
patt_out1 <= ~in[1] + &in[2];
end
always @(negedge in[0]) begin
patt_carry_out1 <= in[2] ? |in[1] : patt_out;
end
always @(*) begin
if (in[0])
patt_out <= patt_out|in[1]~&in[2];
end
always @(*) begin
if (~in[0])
patt_carry_out <= patt_carry_out1&in[2]~|in[1];
end
assert_Z out_test(.A(out));
endmodule
backends/write_firrtl_logic/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg A1,cout1;
reg int1,int2,int3;
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A1 <= ~y + &cin;
end
always @(posedge x) begin
cout1 <= cin ? |y : ~^A;
end
always @(posedge x) begin
A <= A1|y~&cin~^A1;
end
always @(posedge x) begin
cout <= cout1&cin~|y;
end
always @(posedge x)
begin
if (x == 1'b1) begin
int1 = x ^ y;
end
if (x != 1'b1) begin
if (y > 1'b0) begin
if (cin < 1'b1) begin
int2 = cout1;
end
end
end
end
always @(posedge x)
if (x >= 1'b1) begin
if (y <= 1'b0) begin
int3 = A1;
end
end
`else
assign {cout,A} = 1'bZ;
`endif
endmodule
backends/write_firrtl_logic/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_firrtl_reduce/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
reg patt_out1 = 0;
reg patt_carry_out1 = 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]) begin
patt_out1 <= ~in[1] + &in[2];
end
always @(negedge in[0]) begin
patt_carry_out1 <= in[2] ? |in[1] : patt_out;
end
always @(*) begin
if (in[0])
patt_out <= patt_out|in[1]~&in[2];
end
always @(*) begin
if (~in[0])
patt_carry_out <= patt_carry_out1&in[2]~|in[1];
end
assert_Z out_test(.A(out));
endmodule
backends/write_firrtl_reduce/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output A,
output cout
);
wire A1,cout1;
// initial begin
// A = 0;
// cout = 0;
// end
`ifndef BUG
assign A1 = ~y + &cin;
assign cout1 = cin ? |y : ^A;
assign A = A1|y~&cin~^A1;
assign cout = cout1&cin~|y;
`else
assign {cout,A} = 1'bZ;
`endif
endmodule
backends/write_firrtl_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_firrtl_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_firrtl_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_firrtl_shiftx/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
wire out,y;
top uut (
.a(in),
.y(out)
);
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[in];
assert_comb out_test(.A(y), .B(out));
endmodule
backends/write_firrtl_shiftx/top.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer signed i = 0, j = 0;
reg signed [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_firrtl_shiftx/top_clean.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input [4:0] a;
output y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_smt2_shiftx/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
wire out,y;
top uut (
.a(in),
.y(out)
);
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[in];
assert_comb out_test(.A(y), .B(out));
endmodule
backends/write_smt2_shiftx/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_smt2_shiftx/top.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer signed i = 0, j = 0;
reg signed [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_smt2_shiftx/top_clean.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input [4:0] a;
output y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_smv_shiftx/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
wire out,y;
top uut (
.a(in),
.y(out)
);
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[in];
assert_comb out_test(.A(y), .B(out));
endmodule
backends/write_smv_shiftx/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_shiftx/top.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer signed i = 0, j = 0;
reg signed [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_smv_shiftx/top_clean.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input [4:0] a;
output y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_verilog_shiftx/testbench.v 0 → 100644
module testbench;
reg [4:0] in;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
wire out,y;
top uut (
.a(in),
.y(out)
);
integer i, j;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[in];
assert_comb out_test(.A(y), .B(out));
endmodule
backends/write_verilog_shiftx/top.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input signed [4:0] a;
output signed y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
backends/write_verilog_shiftx/top_clean.v 0 → 100644
// VERIFIC-SKIP
module top(a, y);
input [4:0] a;
output y;
integer i = 0, j = 0;
reg [31:0] lut;
initial begin
for (i = 0; i < 32; i = i+1) begin
lut[i] = i > 1;
for (j = 2; j*j <= i; j = j+1)
if (i % j == 0)
lut[i] = 0;
end
end
assign y = lut[a];
endmodule
frontends/Makefile
......@@ -55,4 +55,25 @@ $(eval $(call template,read_liberty_latch,read_liberty read_liberty_nooverwrite
$(eval $(call template,read_liberty_latch_n,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
$(eval $(call template,read_liberty_diff_inv,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
$(eval $(call template,read_liberty_tri,read_liberty read_liberty_nooverwrite read_liberty_ignore_miss_func read_liberty_ignore_miss_dir read_liberty_ignore_miss_data_latch read_liberty_setattr ))
#read_aiger
$(eval $(call template,read_aiger,read_aiger read_aiger_proc read_aiger_ascii read_aiger_module read_aiger_clk read_aiger_clk_module ))
$(eval $(call template,read_aiger_latch,read_aiger_aig))
$(eval $(call template,read_aiger_logic,read_aiger_aig))
$(eval $(call template,read_aiger_ff,read_aiger_aig))
$(eval $(call template,read_aiger_mult,read_aiger_aig))
#read
# read_vhdl87 read_vhdl93 read_vhdl2k read_vhdl2008 read_vhdl - ERROR: This version of Yosys is built without Verific support.
$(eval $(call template,read,read_vlog95 read_vlog2k read_sv2005 read_sv2009 read_sv2012 read_sv read_formal read_define read_define_value read_undef read_incdir read_noverific))
#read_verilog
$(eval $(call template,read_verilog,read_verilog read_verilog_assert_assumes read_verilog_assume_asserts read_verilog_debug read_verilog_defer read_verilog_dname read_verilog_dname_value read_verilog_dump_ast1 read_verilog_dump_ast2 read_verilog_dump_rtlil read_verilog_dump_vlog1 read_verilog_dump_vlog2 read_verilog_formal read_verilog_icells read_verilog_idir read_verilog_i_dir read_verilog_lib read_verilog_mem2reg read_verilog_noassert read_verilog_noassume read_verilog_noautowire read_verilog_nodpi read_verilog_no_dump_ptr read_verilog_nolatches read_verilog_nomem2reg read_verilog_nomeminit read_verilog_noopt read_verilog_nooverwrite read_verilog_nopp read_verilog_norestrict read_verilog_overwrite read_verilog_ppdump read_verilog_setattr read_verilog_sv read_verilog_yydebug ))
#verilog_defaults
$(eval $(call template,verilog_defaults,verilog_defaults verilog_defaults_push verilog_defaults_pop verilog_defaults_clear))
#verilog_defines
$(eval $(call template,verilog_defines,verilog_defines verilog_defines_val verilog_defines_u verilog_defines_d verilog_defines_u_val))
.PHONY: all clean
frontends/read/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
wire patt_out = 0;
wire 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)
);
assign patt_out = in[1] + in[2];
assign 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
frontends/read/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
input clk,
output A,
output cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
assign A = y + cin;
assign cout = y + A;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
frontends/read/top.vhd 0 → 100644
library IEEE;
use IEEE.STD_LOGIC_1164.ALL;
entity top is
Port ( x : in STD_LOGIC;
y : in STD_LOGIC;
cin : in STD_LOGIC;
clk : in STD_LOGIC;
A : out STD_LOGIC;
cout : out STD_LOGIC
);
end entity;
architecture beh of top is
begin
A <= y + cin;
cout <= y + A;
end architecture;
frontends/read_aiger/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
wire patt_out = 0;
wire 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)
);
assign patt_out = in[1] + in[2];
assign 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
frontends/read_aiger/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
input clk,
output A,
output cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
assign A = y + cin;
assign cout = y + A;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
frontends/read_aiger/top2.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
frontends/read_aiger_ff/aiger.aiger 0 → 100644
aag 7 2 1 2 4
2
4
6 8
6
7
8 4 10
10 13 15
12 2 6
14 3 7
frontends/read_aiger_ff/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 n1,n2 = 0;
wire n3,n3_inv;
reg n3p;
wire n3ip;
top uut (
.clk (clk ),
.n1 (n1 ),
.n2 (n2 ),
.n3 (n3 ),
.n3_inv (n3_inv )
);
always @(posedge clk) begin
#3;
n1 <= n1 + 1;
#1;
n2 <= n2 + 1;
end
wire _0_;
wire n4p;
assign _0_ = ~(n3p ^ n1);
assign n4p = n2 & ~(_0_);
assign n3ip = ~n3p;
always @(posedge clk)
n3p <= n4p;
assert_dff dff_test(.clk(clk), .test(n3), .pat(n3p));
endmodule
frontends/read_aiger_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 dinA = 0;
wire doutB;
reg lat = 0;
top uut (
.clk (en ),
//.n1 (dinA ),
.n1_inv (doutB )
);
always @(posedge en) begin
#3;
dinA <= dinA + 1;
end
always @(* )
if ( en )
lat <= dinA;
assert_dff lat_test(.clk(en), .test(doutB), .pat(lat));
endmodule
frontends/read_aiger_logic/aiger.aiger 0 → 100644
aag 7 2 0 2 3
2
4
6
12
6 13 15
12 2 4
14 3 5
i0 x
i1 y
o0 s
o1 c
c
half adder
frontends/read_aiger_logic/testbench.v 0 → 100644
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.c(c),
.s(s),
.x(in[0]),
.y(in[1])
);
assign pat = in[1] ^ in[0];
assign pat1 = in[1] & in[0];
assert_comb out_test(.A(pat), .B(s));
assert_comb out1_test(.A(pat1), .B(c));
endmodule
frontends/read_aiger_mult/testbench.v 0 → 100644
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
endmodule
frontends/read_aiger_s2c/testbench.v 0 → 100644
module testbench;
reg [0:1] in;
wire pat,pat1;
wire c,s;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
endmodule
frontends/read_verilog/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 [15:0] D = 1;
reg [3:0] S = 0;
wire M2,M4,M8,M16;
top uut (
.S (S ),
.D (D ),
.M2 (M2 ),
.M4 (M4 ),
.M8 (M8 ),
.M16 (M16 )
);
always @(posedge clk) begin
//#3;
D <= {D[14:0],D[15]};
//D <= D <<< 1;
S <= S + 1;
end
assert_tri m2_test(.en(clk), .A(D[0]|D[1]), .B(M2));
assert_tri m4_test(.en(clk), .A(D[0]|D[1]|D[2]|D[3]), .B(M4));
assert_tri m8_test(.en(clk), .A(!S[3]), .B(M8));
assert_tri m16_test(.en(clk), .A(1'b1), .B(M16));
endmodule
frontends/read_verilog/top.v 0 → 100644
module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
`ifndef BUG
always @(*)
Y = (S)? B : A;
`else
always @(*)
Y = (~S)? B : A;
`endif
endmodule
module mux4 ( S, D, Y );
input[1:0] S;
input[3:0] D;
output Y;
reg Y;
wire[1:0] S;
wire[3:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
`ifndef BUG
2 : Y = D[2];
`else
2 : Y = D[3];
`endif
3 : Y = D[3];
endcase
end
endmodule
module mux8 ( S, D, Y );
input[2:0] S;
input[7:0] D;
output Y;
reg Y;
wire[2:0] S;
wire[7:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
`ifndef BUG
4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
endcase
end
endmodule
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M2,M4,M8,M16
);
mux2 u_mux2 (
.S (S[0]),
.A (D[0]),
.B (D[1]),
.Y (M2)
);
mux4 u_mux4 (
.S (S[1:0]),
.D (D[3:0]),
.Y (M4)
);
mux8 u_mux8 (
.S (S[2:0]),
.D (D[7:0]),
.Y (M8)
);
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule
frontends/read_verilog/top1.v 0 → 100644
module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
always @(*)
Y = (S)? B : A;
endmodule
module mux4 ( S, D, Y );
input[1:0] S;
input[3:0] D;
output Y;
reg Y;
wire[1:0] S;
wire[3:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
endcase
end
endmodule
module mux8 ( S, D, Y );
input[2:0] S;
input[7:0] D;
output Y;
reg Y;
wire[2:0] S;
wire[7:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
4 : Y = D[4];
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
endcase
end
endmodule
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
assign Y = D[S];
endmodule
module top (
input [3:0] S,
input [15:0] D,
output M2,M4,M8,M16
);
mux2 u_mux2 (
.S (S[0]),
.A (D[0]),
.B (D[1]),
.Y (M2)
);
mux4 u_mux4 (
.S (S[1:0]),
.D (D[3:0]),
.Y (M4)
);
mux8 u_mux8 (
.S (S[2:0]),
.D (D[7:0]),
.Y (M8)
);
mux16 u_mux16 (
.S (S[3:0]),
.D (D[15:0]),
.Y (M16)
);
endmodule
frontends/scripts/read_aiger.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_aig.ys 0 → 100644
read_aiger -clk_name clk -module_name top ../aiger.aiger
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_ascii.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger -ascii aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_clk.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_aiger -clk_name clk aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_clk_module.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_aiger -clk_name clk -module_name top aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_module.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_aiger -module_name top aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_aiger_proc.ys 0 → 100644
read_verilog -sv ../top.v
proc
aigmap
write_aiger aiger.aiger
design -reset
read_aiger aiger.aiger
design -reset
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_define.ys 0 → 100644
read -formal ../top.v
read -define MACRO
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_define_value.ys 0 → 100644
read -formal ../top.v
read -define MACRO=1
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_formal.ys 0 → 100644
read -formal ../top.v
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_incdir.ys 0 → 100644
read -formal ../top.v
read -incdir ../include_dir
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_noverific.ys 0 → 100644
read -noverific
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_sv.ys 0 → 100644
read -sv ../top.v
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_sv2005.ys 0 → 100644
read -sv2005 ../top.v
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_sv2009.ys 0 → 100644
read -sv2009 ../top.v
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_sv2012.ys 0 → 100644
read -sv2012 ../top.v
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_undef.ys 0 → 100644
read -formal ../top.v
read -define MACRO
read -undef MACRO
design -reset
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog.ys 0 → 100644
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_assert_assumes.ys 0 → 100644
read_verilog -assert-assumes ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_assume_asserts.ys 0 → 100644
read_verilog -assume-asserts ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_debug.ys 0 → 100644
read_verilog -debug ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_defer.ys 0 → 100644
read_verilog -defer ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dname.ys 0 → 100644
read_verilog -Dname ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dname_value.ys 0 → 100644
read_verilog -Dname=9 ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dump_ast1.ys 0 → 100644
read_verilog -dump_ast1 ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dump_ast2.ys 0 → 100644
read_verilog -dump_ast2 ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dump_rtlil.ys 0 → 100644
read_verilog -dump_rtlil ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dump_vlog1.ys 0 → 100644
read_verilog -dump_vlog1 ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_dump_vlog2.ys 0 → 100644
read_verilog -dump_vlog2 ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_formal.ys 0 → 100644
read_verilog -formal ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_i_dir.ys 0 → 100644
read_verilog -I dir ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_icells.ys 0 → 100644
read_verilog -icells ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_idir.ys 0 → 100644
read_verilog -Idir ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_lib.ys 0 → 100644
read_verilog -lib ../top.v
read_verilog ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_mem2reg.ys 0 → 100644
read_verilog -mem2reg ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_no_dump_ptr.ys 0 → 100644
read_verilog -no_dump_ptr ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_noassert.ys 0 → 100644
read_verilog -noassert ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_noassume.ys 0 → 100644
read_verilog -noassume ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_noautowire.ys 0 → 100644
read_verilog -noautowire ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nodpi.ys 0 → 100644
read_verilog -nodpi ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nolatches.ys 0 → 100644
read_verilog -nolatches ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nomem2reg.ys 0 → 100644
read_verilog -nomem2reg ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nomeminit.ys 0 → 100644
read_verilog -nomeminit ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_noopt.ys 0 → 100644
read_verilog -noopt ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nooverwrite.ys 0 → 100644
read_verilog -nooverwrite ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_nopp.ys 0 → 100644
read_verilog -nopp ../top1.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_norestrict.ys 0 → 100644
read_verilog -norestrict ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_overwrite.ys 0 → 100644
read_verilog -overwrite ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_ppdump.ys 0 → 100644
read_verilog -ppdump ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_setattr.ys 0 → 100644
read_verilog -setattr attr ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_sv.ys 0 → 100644
read_verilog -sv ../top.v
synth -top top
write_verilog synth.v
frontends/scripts/read_verilog_yydebug.ys 0 → 100644
read_verilog -yydebug ../top.v
synth -top top
write_verilog synth.v
misc/log/.dummy 0 → 100644
This diff is collapsed. Click to expand it.
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