Commit 50fc2cde by SergeyDegtyar

Add new tests to 'simple' and 'misc' test groups

simple & misc
===========
Note that some of commands you can not test with checking with testbench
so those place in misc.

1. passes/cmds/add.cc
Note that here you need to load some existing verilog and add additional
wires, inputs or outputs
2. passes/cmds/blackbox.cc
you could create design with sub module, execute blackbox  and check if
sub module is replaced with blackbox module.
3. passes/cmds/bugpoint.cc

4. passes/cmds/chformal.cc

5. passes/cmds/chtype.cc

6. passes/cmds/connect.cc
Maybe can be covered together with add command

7.passes/cmds/connwrappers.cc

8. passes/cmds/design.cc
missing covering -import option

9.passes/cmds/plugin.cc

10. passes/cmds/rename.cc
rename parts of existing design

11. /passes/cmds/select.cc
Lot of options is not used , so room to improve

12.passes/cmds/setattr.cc
note there are 3 commands to cover here

13. passes/cmds/setundef.cc
setting with one, anyseq, anyconst ...

14. passes/sat/assertpmux.cc
15. passes/sat/async2sync.cc
16. passes/sat/eval.cc
17. passes/sat/freduce.cc
18. passes/sat/miter.cc
run with -assert option
19. passes/sat/sat.cc
many options are not tested
20. passes/sat/sim.cc

21. passes/techmap/flowmap.cc
parent 5b39f7c6
......@@ -48,7 +48,7 @@ $(eval $(call template,scc, scc scc_all_cell_types scc_expect scc_max_depth scc_
$(eval $(call template,scatter, scatter ))
#rename
$(eval $(call template,rename, rename rename_top rename_src rename_hide rename_enumerate rename_enumerate_pat))
$(eval $(call template,rename, rename rename_top rename_src rename_hide rename_enumerate rename_enumerate_pat rename_wire))
#qwp
#qwp_v - exception
......@@ -72,4 +72,72 @@ $(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))
#add
$(eval $(call template,add, add add_wire add_input add_output add_inout add_global_input ))
#blackbox
$(eval $(call template,blackbox, blackbox ))
#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 ))
#chformal
$(eval $(call template,chformal, chformal chformal_assert2assume chformal_assert chformal_assume2assert chformal_assume chformal_cover chformal_delay chformal_early chformal_proc_early chformal_fair2live_assert2assume chformal_fair2live chformal_fair chformal_live2fair chformal_live chformal_skip ))
$(eval $(call template,chformal_dff, chformal chformal_assert2assume chformal_assert chformal_assume2assert chformal_assume chformal_cover chformal_delay chformal_early chformal_proc_early chformal_fair2live_assert2assume chformal_fair2live chformal_fair chformal_live2fair chformal_live chformal_skip ))
#chtype
$(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))
#connwrappers
$(eval $(call template,connwrappers, connwrappers connwrappers_signed connwrappers_unsigned connwrappers_port ))
#plugin
$(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_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_%))
#setattr
$(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
#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
$(eval $(call template,chparam, chparam chparam_set chparam_top chparam_list ))
#setundef
$(eval $(call template,setundef, setundef_one setundef_anyseq setundef_anyconst setundef_init setundef_random setundef_undef setundef_undriven setundef_expose))
#assertpmux
$(eval $(call template,assertpmux, assertpmux assertpmux_noinit assertpmux_always))
#eval
$(eval $(call template,eval, eval eval_set eval_set_undef eval_table eval_show eval_brute_force_equiv_checker eval_show_not_set eval_table_set eval_vloghammer_report eval_vloghammer_report_rtl))
#freduce
$(eval $(call template,freduce, freduce freduce_v freduce_vv freduce_inv freduce_stop freduce_dump ))
$(eval $(call template,freduce_dff, freduce freduce_v freduce_vv freduce_inv freduce_stop freduce_dump ))
$(eval $(call template,freduce_mem, freduce freduce_v freduce_vv freduce_inv freduce_stop freduce_dump ))
#miter -assert
$(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
$(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
#sat
$(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 ))
#sim
$(eval $(call template,sim,sim sim_a sim_clock sim_d sim_n sim_rstlen sim_vcd sim_w sim_zinit ))
$(eval $(call template,sim_mem,sim sim_a sim_clockn sim_clock_mem sim_d sim_n sim_resetn sim_reset sim_rstlen sim_vcd sim_w sim_zinit_mem ))
.PHONY: all clean
(* 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
module top(C, S, Y);
input C;
input [1:0] S;
output reg [3:0] Y;
initial Y = 0;
always @(posedge C) begin
case (S)
2'b00: Y <= 4'b0001;
2'b01: Y <= 4'b0010;
2'b10: Y <= 4'b0100;
2'b11: Y <= 4'b1000;
endcase
end
endmodule
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
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
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
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
parameter X = 1;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid (.x(x),.o(o),.y(1'b0));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
(
input [7:0] data_a, data_b,
input [6:1] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clka, clkb,
output reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
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
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module middle
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
read_verilog ../top.v
tee -o result.log add -wire w 0
read_verilog ../top.v
tee -o result.log add -global_input gi 32000
read_verilog ../top.v
tee -o result.log add -inout \34 3
read_verilog ../top.v
add -input i 2
tee -o result.log add -input i 2
read_verilog ../top.v
tee -o result.log add -output o 3
read_verilog ../top.v
tee -o result.log add -wire w 1
read_verilog ../top.v
proc
tee -o result.log assertpmux
read_verilog ../top.v
proc
tee -o result.log assertpmux -always
read_verilog ../top.v
proc
tee -o result.log assertpmux -noinit
read_verilog ../top.v
tee -o result.log blackbox bb
read_verilog ../top.v
tee -o result.log bugpoint
read_verilog ../top.v
tee -o result.log bugpoint -cells
read_verilog ../top.v
tee -o result.log bugpoint -clean
read_verilog ../top.v
tee -o result.log bugpoint -connections
read_verilog ../top.v
tee -o result.log bugpoint -fast
read_verilog ../top.v
tee -o result.log bugpoint -grep "Yosys"
read_verilog ../top.v
tee -o result.log bugpoint -modules
read_verilog ../top.v
tee -o result.log bugpoint -ports
read_verilog ../top.v
tee -o result.log bugpoint -script script.ys
read_verilog ../top.v
tee -o result.log bugpoint -yosys yosys.ys
read_verilog -sv ../top.v
tee -o result.log chformal -remove
read_verilog -sv ../top.v
tee -o result.log chformal -assert -remove
read_verilog -sv ../top.v
tee -o result.log chformal -assert2assume
read_verilog -sv ../top.v
tee -o result.log chformal -assume -remove
read_verilog -sv ../top.v
tee -o result.log chformal -assume2assert
read_verilog -sv ../top.v
tee -o result.log chformal -cover -remove
read_verilog -sv ../top.v
tee -o result.log chformal -delay 2
read_verilog -sv ../top.v
tee -o result.log chformal -early
read_verilog -sv ../top.v
tee -o result.log chformal -fair -remove
read_verilog -sv ../top.v
tee -o result.log chformal -fair2live
read_verilog -sv ../top.v
tee -o result.log chformal -fair2live -assert2assume
read_verilog -sv ../top.v
tee -o result.log chformal -live -remove
read_verilog -sv ../top.v
tee -o result.log chformal -live2fair
read_verilog -sv ../top.v
proc
tee -o result.log chformal -early
read_verilog -sv ../top.v
tee -o result.log chformal -skip 2
read_verilog ../top.v
proc
tee -o result.log chparam
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 top
tee -o result.log chparam -list
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 top
read_verilog ../top.v
proc
tee -o result.log chparam top
read_verilog -sv ../top.v
proc
tee -o result.log chtype
read_verilog -sv ../top.v
proc
tee -o result.log chtype -map $dff $adff $2
read_verilog -sv ../top.v
proc
tee -o result.log chtype $2
read_verilog -sv ../top.v
proc
tee -o result.log chtype -set $adff $2
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -port $dff d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -set d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -unset d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -nounset -set d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -port $2 d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q
read_verilog -sv ../top.v
proc
tee -o result.log connect -unset d q
read_verilog ../top.v
proc
tee -o result.log connwrappers
read_verilog ../top.v
proc
tee -o result.log connwrappers -port $dff d 32000 1
read_verilog ../top.v
proc
tee -o result.log connwrappers -signed $dff d 3
read_verilog ../top.v
proc
tee -o result.log connwrappers -unsigned $dff d 0
read_verilog ../top.v
proc
tee -o result.log eval middle
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker_x top top
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 middle
read_verilog ../top.v
proc
tee -o result.log eval -set-undef middle
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 -show o middle
read_verilog ../top.v
proc
tee -o result.log eval -show o middle
read_verilog ../top.v
proc
tee -o result.log eval -table o middle
read_verilog ../top.v
proc
tee -o result.log eval -set-undef -table o middle
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report mid dle x 1
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report u_ rtl y 1
read_verilog ../top.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog ../top.v
proc
tee -o result.log freduce -dump fred
read_verilog ../top.v
proc
tee -o result.log freduce -inv
read_verilog ../top.v
proc
tee -o result.log freduce -stop 1
read_verilog ../top.v
proc
tee -o result.log freduce -v
read_verilog ../top.v
proc
tee -o result.log freduce -vv
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -make_outputs top
tee -o result.log miter -assert -make_outputs middle
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -flatten top
tee -o result.log miter -assert -flatten middle
tee -o result.log plugin
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so
read_verilog ../top.v
tee -o result.log plugin -l
plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
tee -o result.log plugin -l
read_verilog ../top.v
proc
tee -o result.log rename -enumerate
tee -o result.log rename -enumerate middle mid_module
read_verilog ../top.v
proc
tee -o result.log rename -src
tee -o result.log rename -src middle mid_module
read_verilog ../top.v
proc
tee -o result.log rename -wire middle mid_module
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