Commit ee7949ea by SergeyDegtyar

Review 'misc' test group. Rename back to "misc".

parent cfa2a1ef

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

*/work_*/ */work_*/
/.stamp /.stamp
/run-test.mk
all: work PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
touch .stamp
clean:: all::
rm -f .stamp
define template run-test.mk: ../generate.py
$(foreach design,$(1), @$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
$(foreach script,$(2),
work:: $(design)/work_$(script)/.stamp
$(design)/work_$(script)/.stamp:
bash run.sh $(design) $(script)
clean::
rm -rf $(design)/work_$(script)
))
endef
#test_abcloop
$(eval $(call template,test_abcloop,test_abcloop test_abcloop_n test_abcloop_s ))
#test_cell
#test_cell_map - takes a lot of time
# test_cell_mux, test_cell_pmux - is not supported
$(eval $(call template,test_cell,test_cell test_cell_aigmap test_cell_const test_cell_edges test_cell_f test_cell_div test_cell_muxdiv test_cell_n test_cell_noeval test_cell_nosat test_cell_s test_cell_script test_cell_simlib test_cell_v test_cell_vlog test_cell_w test_cell_alu test_cell_sop test_cell_lut test_cell_macc test_cell_lcu test_cell_fa test_cell_wo_synth test_cell_map))
$(eval $(call template,test_cell_error, test_cell_failed_to_open test_cell_unexpected_opt test_cell_cell_type_not_supported test_cell_no_cell_t_specified test_cell_dont_spec_cell_type_with_f ))
#torder
$(eval $(call template,torder,torder torder_stop torder_noautostop ))
#trace
$(eval $(call template,trace,trace ))
$(eval $(call template,trace_mem,trace_mem ))
#write_file
$(eval $(call template,write_file,write_file write_file_a ))
$(eval $(call template,write_file_error,write_file_missing_name write_file_a_missing_name ))
#stat
$(eval $(call template,stat, stat stat_top stat_width stat_liberty stat_tech_xilinx ))
$(eval $(call template,stat_error, stat_unsupported_tech stat_cant_find_module stat_cant_open_lib_file ))
#show
# show_pause - skipped
$(eval $(call template,show, show show_colorattr show_colors show_color show_enum show_format show_label show_lib show_long show_notitle show_prefix show_signed show_stretch show_viewer show_width))
$(eval $(call template,show_error, show_only_one_module show_cant_open_dot_file show_cant_open_lib_file show_nothing_there_to_show))
#scc
$(eval $(call template,scc, scc scc_all_cell_types scc_expect scc_max_depth scc_nofeedback scc_select scc_set_attr ))
$(eval $(call template,scc_feedback, scc scc_all_cell_types scc_expect1 scc_max_depth scc_nofeedback scc_select scc_set_attr ))
$(eval $(call template,scc_hier_feedback, scc scc_all_cell_types scc_expect scc_max_depth scc_nofeedback scc_select scc_set_attr ))
$(eval $(call template,scc_error, scc_expect1 ))
#scatter
$(eval $(call template,scatter, scatter ))
#rename
$(eval $(call template,rename, rename rename_top rename_src rename_hide rename_enumerate rename_enumerate_pat rename_wire rename_top_top rename_low))
$(eval $(call template,rename_error, rename_obj_not_found rename_no_top_module rename_invalid_number_of_args rename_invalid_number_of_args_top rename_mode_out_requires))
#qwp
#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_v qwp_ltr qwp_grid qwp_dump qwp_alpha))
#ltp
$(eval $(call template,ltp, ltp ltp_noff ))
#edgetypes
$(eval $(call template,edgetypes, edgetypes ))
#delete
$(eval $(call template,delete, delete delete_input delete_output delete_port delete_cell delete_wire delete_proc ))
$(eval $(call template,delete_mem, delete_mem ))
#cover
$(eval $(call template,cover, cover cover_q cover_o cover_dir cover_a ))
$(eval $(call template,cover_error, cover_cant_create_file ))
#insbuf
$(eval $(call template,insbuf,insbuf insbuf_cell))
#add
$(eval $(call template,add, add add_wire add_input add_output add_inout add_global_input ))
$(eval $(call template,add_error, add_error ))
#blackbox
$(eval $(call template,blackbox, blackbox ))
$(eval $(call template,blackbox_mem, blackbox blackbox_top))
# - issue #925
#bugpoint ERROR: No such command: autoidx (type 'help' for a command overview)
$(eval $(call template,bugpoint,bugpoint_yosys bugpoint_script bugpoint_grep bugpoint_fast bugpoint_clean bugpoint_modules bugpoint_ports bugpoint_cells bugpoint_connections ))
$(eval $(call template,bugpoint_error, bugpoint_missing_script bugpoint_do_not_crash bugpoint_fully_selected_des))
#bugpoint_grep_string_not_found - no error
#chformal
$(eval $(call template,chformal, chformal chformal_ff 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_ff 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_ff, chformal chformal_ff 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_error, chformal_error ))
#chtype
$(eval $(call template,chtype, chtype chtype_map chtype_selection chtype_set))
#connect
$(eval $(call template,connect, connect_nomap_set connect_nomap_unset connect_nounset_set connect_set connect_unset connect_port connect_nomap_port))
$(eval $(call template,connect_error, connect_multiple_modules connect_found_process connect_no_modules connect_set_with_unset connect_set_with_port connect_set_with_unset_and_port connect_cannot_parse_set_lhs_expr connect_cannot_parse_set_rhs_expr connect_unset_with_nounset connect_unset_with_port connect_unset_with_nounset_and_port connect_failed_parse_unset connect_port_with_nounset connect_cant_find_cell connect_failed_to_parse_port_expr connect_opt_expected))
#connwrappers
$(eval $(call template,connwrappers, connwrappers connwrappers_signed connwrappers_unsigned connwrappers_port ))
#plugin
$(eval $(call template,plugin, plugin plugin_i plugin_a plugin_l ))
$(eval $(call template,plugin_error, plugin_error ))
#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 ))
$(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_%))
$(eval $(call template,select_error, select_add_with_del select_assert_any_failed select_assert_any_with_count select_assert_count_failed select_assert_list_with_assert_max select_assert_list_with_del select_assert_max_failed select_assert_max_with_del select_assert_min_failed select_assert_none_failed select_assert_none_with_min select_cant_open_for_reading select_cant_open_for_writing select_clear_with_other_opt select_count_with_assert_min select_count_with_assert_none select_error_in_expand_op select_none_with_other_opt select_no_sel_to_check_as_any select_no_sel_to_check_as_count select_no_sel_to_check_as_max select_no_sel_to_check_as_min select_no_sel_to_check_as_none select_no_such_module select_nothing_to_add select_nothing_to_del select_one_elem_for__a select_one_elem_for__cie select_one_elem_for__ci select_one_elem_for__coe select_one_elem_for__co select_one_elem_for__C select_one_elem_for__c select_one_elem_for__D select_one_elem_for__d select_one_elem_for__i select_one_elem_for__m select_one_elem_for__M select_one_elem_for__n select_one_elem_for__R select_one_elem_for__s select_one_elem_for__u select_one_elem_for__xe select_one_elem_for__x select_read_with_selection_expr select_selection_isnt_defined select_set_with_assert_any select_set_with_assert_max select_set_with_count select_set_with_del select_set_with_list select_unknown_opt select_unknown_selection select_write_with_assert_count select_write_with_del))
$(eval $(call template,select_cd_error, select_cd_invalid_number_of_args select_cd_no_such_module ))
#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 ))
$(eval $(call template,setattr_error, setattr_cant_decode_value ))
#setparam
#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 setparam_type))
#chparam
$(eval $(call template,chparam, chparam chparam_set chparam_top chparam_list ))
$(eval $(call template,chparam_error, chparam_error))
#setundef
$(eval $(call template,setundef, setundef_one setundef_anyseq setundef_anyconst setundef_init setundef_random setundef_undef setundef_undriven setundef_expose))
# issue #1092
$(eval $(call template,setundef_error, setundef_expose_without_undriven setundef_init_with_anyconst setundef_init_with_anyseq setundef_one_of_options setundef_undriven_with_process))
#assertpmux
$(eval $(call template,assertpmux, assertpmux assertpmux_noinit assertpmux_always))
$(eval $(call template,assertpmux_mux, 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))
$(eval $(call template,eval_error, eval_only_one_module eval_failed_to_parse_lhs eval_failed_to_parse_rhs eval_rhs_expr eval_diff_lhs_rhs_sizes eval_failed_to_parse_show_expr eval_failed_to_parse_table_expr eval_empty_selection eval_port_doesnt_match eval_cant_find_mod_1 eval_cant_find_mod_2 eval_mods_arent_equiv eval_cant_find_mod_in_curr_des eval_no_output_wire eval_cant_find_input eval_wire_isnt_an_input eval_failed_to_parse_pattern eval_pattern_is_to_short eval_two_distinct_solutions))
#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_ffs, 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 ))
$(eval $(call template,freduce_error, freduce_logic_loop ))
#miter -assert
$(eval $(call template,miter_assert, miter_assert miter_assert_flatten ))
$(eval $(call template,miter_assert_assume, miter_assert miter_assert_flatten ))
$(eval $(call template,miter_error, miter_cant_find_gate_module miter_cant_find_gold_module miter_cant_find_module miter_missing_mode_param miter_no_match_in_gate miter_no_match_in_gold miter_there_is_already_a_module ))
#sat
#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 sat_tempinduct_def sat_tempinduct_tempinduct_def))
$(eval $(call template,sat_error, sat_show_fail sat_provex_diff_size sat_provex_lhs_fail sat_provex_rhs_fail sat_prove_rhs_fail sat_prove_lhs_fail sat_prove_diff_size sat_set_all_undef_fail sat_set_any_undef_fail sat_set_def_fail sat_set_diff_size sat_set_rhs_fail sat_set_lhs_fail sat_cnf_open_json_file sat_cant_open_json_file sat_cant_open_vcd_file sat_falsify_fail sat_verify_fail sat_all_with_tempinduct sat_maxundef_with_tempinduct sat_max_with_tempinduct sat_max_max_undef_with_tempinduct sat_max_all_with_tempinduct sat_max_maxundef_with_tempinduct sat_max_maxundef_all_with_tempinduct sat_maxsteps_only_for_tempinduct sat_si_def_zero sat_si_undef_zero sat_si_def_undef sat_si_def_undef_zero sat_failed_to_import_cell sat_prove_skip_must_be_smaller_than_seq sat_prove_and_tempinduct sat_got_tempinduct_but_nothing_to_prove sat_cant_perform_sat_on_empty_sel sat_only_one_module_must_be_sel))
#sat_set_all_undef_at_fail sat_set_any_undef_at_fail sat_set_def_at_fail sat_unset_at_fail sat_set_at_diff_size sat_set_at_lhs_fail sat_set_at_rhs_fail - no errors
#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 ))
#splitnets
$(eval $(call template,splitnets, splitnets splitnets_format splitnets_ports splitnets_driver splitnets_dpf ))
$(eval $(call template,splitnets_logic, splitnets splitnets_format splitnets_ports splitnets_driver splitnets_dpf ))
#splice
$(eval $(call template,splice, splice splice_sel_by_cell splice_sel_by_wire splice_sel_any_bit splice_wires splice_no_outputs splice_port splice_no_port ))
$(eval $(call template,splice_error, splice_sel_by_cell_and_sel_by_wire splice_sel_by_cell_and_sel_any_bit splice_port_and_no_port ))
#supercover
$(eval $(call template,supercover, supercover))
#rmports
$(eval $(call template,rmports, rmports))
#check
$(eval $(call template,check, check check_noinit check_initdrv check_assert))
$(eval $(call template,check_error, check_error ))
#design
$(eval $(call template,design, design_import design_copy_from design_copy_to design_as))
$(eval $(call template,design_error, design_no_saved_design_copy_from design_no_saved_design_import design_no_saved_design_load design_no_pushed_design design_no_top_module))
#log
$(eval $(call template,log, log log_stdout log_stderr log_nolog log_n))
#tee
$(eval $(call template,tee, tee))
$(eval $(call template,tee_error, tee_o_cant_create_file tee_a_cant_create_file ))
#test_autotb
$(eval $(call template,test_autotb, test_autotb test_autotb_file test_autotb_n test_autotb_seed))
#abc
$(eval $(call template,abc, abc_D abc_g_aig abc_g_cmos2 abc_g_cmos abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S abc_dff abc_constr_liberty))
$(eval $(call template,abc_dff, abc_D abc_g_aig abc_g_cmos2 abc_g_cmos abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S abc_dff abc_constr_liberty))
$(eval $(call template,abc_mux, abc_D abc_g_aig abc_g_cmos2 abc_g_cmos abc_g_simple abc_mux16 abc_mux4 abc_mux8 abc_S abc_dff abc_constr_liberty))
$(eval $(call template,abc_error, abc_cannot_open abc_constr_no_liberty abc_lut_liberty abc_unsup_gate_type abc_inv_luts_synt abc_return_code abc_clk_domain_not_found abc_script_o abc_script_top))
#hilomap
$(eval $(call template,hilomap, hilomap hilomap_hicell hilomap_locell hilomap_singleton hilomap_hicell_singleton hilomap_locell_singleton hilomap_hicell_locell_singleton))
#cutpoint
$(eval $(call template,cutpoint, cutpoint cutpoint_undef))
#mutate
$(eval $(call template,mutate, mutate_list mutate_cnot1 mutate_cnot0 mutate_const1 mutate_const0 mutate_inv mutate_all mutate_list_cfg mutate_list_ctrl mutate_list_none mutate_list_o mutate_list_seed mutate_list_s))
$(eval $(call template,mutate_mem, mutate_list mutate_all))
$(eval $(call template,mutate_error, mutate_error))
#fmconbine
#fmcombine_gate_cell_not_found - failed #1063
$(eval $(call template,fmcombine, fmcombine fmcombine_fwd fmcombine_bwd fmcombine_nop fmcombine_bwd_fwd fmcombine_anyeq fmcombine_initeq))
$(eval $(call template,fmcombine_assert_assume, fmcombine fmcombine_fwd fmcombine_bwd fmcombine_nop fmcombine_bwd_fwd fmcombine_anyeq fmcombine_initeq))
$(eval $(call template,fmcombine_error, fmcombine_invalid_number_of_param fmcombine_module_not_found fmcombine_gold_cell_not_found fmcombine_gate_cell_not_found fmcombine_types_not_match fmcombine_nop_with_fwd fmcombine_nop_with_bwd fmcombine_nop_with_fwd_bwd))
#pmuxtree
$(eval $(call template,pmuxtree, pmuxtree))
#opt_rmdff_sat
$(eval $(call template,opt_rmdff_sat, opt_rmdff_sat))
#wbflip
$(eval $(call template,wbflip, wbflip wbflip_top))
#pmux2shiftx
$(eval $(call template,pmux2shiftx, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
$(eval $(call template,pmux2shiftx_2, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
$(eval $(call template,pmux2shiftx_fsm, pmux2shiftx_norange pmux2shiftx_onehot_shiftx pmux2shiftx_onehot_pmux pmux2shiftx_onehot_ignore pmux2shiftx_min_choices_0 pmux2shiftx_min_choices_3000 pmux2shiftx_min_dens_3000 pmux2shiftx_min_dens_0 pmux2shiftx_vv pmux2shiftx_v pmux2shiftx_top pmux2shiftx ))
#onehot
$(eval $(call template,onehot, onehot onehot_v onehot_vv ))
#help
$(eval $(call template,help, help_celltype_plus help_celltype help_cells help_all help_command help help_no_such_command ))
#echo
$(eval $(call template,echo, echo echo_off echo_on ))
#debug
$(eval $(call template,debug, debug ))
#muxpack
$(eval $(call template,muxpack, muxpack ))
#history
$(eval $(call template,history, history ))
#script
$(eval $(call template,script, script script_from_to script_scriptwire ))
#tcl
$(eval $(call template,tcl, tcl ))
#abc9
$(eval $(call template,abc9, abc9_markgroups abc9_showtmp abc9_nocleanup abc9_luts abc9_lut abc9_fast abc9_D abc9_W abc9_wo_proc abc9_wo_synth abc9_box abc9_script))
$(eval $(call template,abc9_dff, abc9_markgroups abc9_showtmp abc9_nocleanup abc9_luts abc9_lut abc9_fast abc9_D abc9_W abc9_wo_proc abc9_wo_synth))
$(eval $(call template,abc9_mux, abc9_markgroups abc9_showtmp abc9_nocleanup abc9_luts abc9_lut abc9_fast abc9_D abc9_W abc9_wo_proc abc9_wo_synth))
$(eval $(call template,abc9_mem, abc9_markgroups abc9_showtmp abc9_nocleanup abc9_luts abc9_lut abc9_fast abc9_D abc9_W abc9_wo_proc abc9_wo_synth))
$(eval $(call template,abc9_error, abc9_invalid_luts_syntax abc9_cant_open_output_file))
include run-test.mk
.PHONY: all clean .PHONY: all clean
...@@ -2,4 +2,9 @@ read_verilog ../top.v ...@@ -2,4 +2,9 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc -g simple abc
select -assert-count 3 t:$_NAND_
select -assert-count 2 t:$_XOR_
select -assert-none t:$_NAND_ t:$_XOR_ %% t:* %D
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -D 2 -lut 2 tee -o result.out abc -D 2
ERROR: Can't open ABC output file
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -liberty -constr tee -o result.out abc -liberty -constr
abc -liberty -constr abc -liberty -constr
ERROR: Clock domain u not found.
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -dff -clk u tee -o result.out abc -dff -clk u
abc -dff -clk u abc -dff -clk u
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -liberty -constr top.lib tee -o result.out abc -liberty -constr top.lib
ERROR: Got -constr but no -liberty!
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -constr -liberty tee -o result.out abc -constr -liberty
abc -constr -liberty abc -constr -liberty
read_verilog ../top_dff.v
synth -top top
dff2dffe
tee -o result.log abc -dff
abc -dff
read_verilog ../top_dff.v
synth -top top
tee -o result.log abc -keepff
abc -dff
read_verilog ../top_div_mul.v
proc
dff2dffe
synth -top top
tee -o result.out abc
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -clk clk
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
read_verilog ../top_fsm.v
synth -top top
abc -g cmos4
select -assert-count 6 t:$_AOI3_
select -assert-count 1 t:$_AOI4_
select -assert-count 2 t:$_OAI3_
read_verilog ../top_fsm.v
synth -top top
abc -g gates
read_verilog ../top.v
synth -top top
abc -g aig
select -assert-count 2 t:$_AND_
select -assert-count 3 t:$_NAND_
select -assert-count 2 t:$_OR_
read_verilog ../top.v
synth -top top
abc -g cmos
select -assert-count 1 t:$_NAND_
select -assert-count 1 t:$_NOT_
select -assert-count 1 t:$_OAI3_
select -assert-count 2 t:$_XNOR_
read_verilog ../top.v
synth -top top
abc -g cmos2
select -assert-count 4 t:$_NAND_
select -assert-count 5 t:$_NOR_
select -assert-count 3 t:$_NOT_
read_verilog ../top.v
proc
dff2dffe
synth -top top
abc -g simple
select -assert-count 2 t:$_AND_
select -assert-count 1 t:$_OR_
select -assert-count 2 t:$_NOT_
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -dff tee -o result.log abc -I 4
abc -dff abc -dff
ERROR: Invalid -luts syntax.
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -luts : tee -o result.out abc -luts :
abc -liberty -luts : abc -liberty -luts :
read_verilog ../top_logic.v
proc
synth -top top
tee -o result.out abc
read_verilog ../top_logic_loop.v
proc
synth -top top
tee -o result.out abc
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut 4
abc -lut 3
stat
ERROR: Got -lut and -liberty! This two options are exclusive.
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -lut 2 -liberty top.lib tee -o result.out abc -lut 2 -liberty top.lib
abc -lut 2 -liberty top.lib abc -lut 2 -liberty top.lib
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut -4
abc -lut -3:1
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -g aig tee -o result.log abc -luts 3:4
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -markgroups
read_verilog ../top_mux.v
proc
synth -top top
abc
select -assert-count 139 t:$_MUX_
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux16
stat
read_verilog ../top_mux.v
synth -top top
abc -mux4
select -assert-count 75 t:$_MUX4_
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux8
stat
read_verilog ../top_mux.v
synth -top top
tee -o result.out abc -g cmos3
abc -g cmos3
select -assert-count 144 t:$_AOI3_
select -assert-count 169 t:$_OAI3_
read_verilog ../top_mux.v
synth -top top
tee -o result.out abc -g cmos4
abc -g cmos4
select -assert-count 111 t:$_AOI3_
select -assert-count 28 t:$_AOI4_
select -assert-count 111 t:$_AOI3_
select -assert-count 24 t:$_OAI4_
read_verilog ../top.v read_verilog ../top.v
tee -o result.log abc9 -luts uu tee -o result.out abc
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log abc9 -lut 2 tee -o result.out abc
read_verilog ../top.v
synth -top top
tee -o result.log abc -P 4
abc -dff
failed: return code 134.
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -g XOR tee -o result.out abc -g XOR
abc -g XOR abc -g XOR
ERROR: Can't open ABC output file
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -script o tee -o result.out abc -script o
abc -script o abc -script o
ERROR: Can't open ABC output file
read_verilog ../top.v
synth -top top
tee -o result.out abc -script top.yss
abc -script top.yss
read_verilog ../top_dff.v
tee -o result.out abc
ERROR: Command syntax error: Unsupported gate type: XO
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -g XO tee -o result.out abc -g XO
abc -g XO abc -g XO
...@@ -8,10 +8,6 @@ ...@@ -8,10 +8,6 @@
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -5,11 +5,7 @@ module adff ...@@ -5,11 +5,7 @@ module adff
end end
always @( posedge clk, posedge clr ) always @( posedge clk, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -21,11 +17,7 @@ module adffn ...@@ -21,11 +17,7 @@ module adffn
end end
always @( posedge clk, negedge clr ) always @( posedge clk, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -37,11 +29,7 @@ module dffe ...@@ -37,11 +29,7 @@ module dffe
end end
always @( posedge clk ) always @( posedge clk )
if ( en ) if ( en )
`ifndef BUG
q <= d; q <= d;
`else
q <= 1'b0;
`endif
endmodule endmodule
module dffsr module dffsr
...@@ -51,11 +39,7 @@ module dffsr ...@@ -51,11 +39,7 @@ module dffsr
end end
always @( posedge clk, posedge pre, posedge clr ) always @( posedge clk, posedge pre, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( pre ) else if ( pre )
q <= 1'b1; q <= 1'b1;
else else
...@@ -69,11 +53,7 @@ module ndffnsnr ...@@ -69,11 +53,7 @@ module ndffnsnr
end end
always @( negedge clk, negedge pre, negedge clr ) always @( negedge clk, negedge pre, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre ) else if ( !pre )
q <= 1'b1; q <= 1'b1;
else else
......
...@@ -8,10 +8,6 @@ module top ...@@ -8,10 +8,6 @@ module top
output cout output cout
); );
`ifndef BUG
assign cout = x / y * cin; assign cout = x / y * cin;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
module FSM ( clk,rst, en, ls, rs, stop, busy, finish);
input wire clk;
input wire rst;
input wire en;
input wire ls;
input wire rs;
output wire stop;
output wire busy;
output wire finish;
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 (rs == 1'b1)
ns = S3;
else
ns = S4;
S3: ns = S1;
S4: if (count > 7)
ns = S10;
else
ns = S5;
S5: if (ls == 1'b0)
ns = S6;
else
ns = S3;
S6:
if (ls == 1'b1)
ns = S7;
else
ns = S8;
S7:
if (ls == 1'b1 && rs == 1'b1)
ns = S5;
else
ns = S13;
S8: ns = S9;
S9: ns = S8;
S10:
if (ls == 1'b1 || rs == 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 stop = (st == S3 || st == S12) ? 1'b1 : 1'b0;
assign finish = (st == S13) ? 1'b1 : 1'b0;
assign busy = (st == S8 || st == S9) ? 1'b1 : 1'b0;
endmodule
module top (
input clk,
input rst,
input en,
input a,
input b,
output s,
output bs,
output f
);
FSM u_FSM ( .clk(clk),
.rst(rst),
.en(en),
.ls(a),
.rs(b),
.stop(s),
.busy(bs),
.finish(f));
endmodule
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg A1,cout1,A2,cout2;
initial begin
A = 0;
cout = 0;
end
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
A2 <= ~(y | cin);
end
always @(posedge x) begin
cout2 <= cin ~|y;
end
endmodule
module top
(
input x,
input y,
input z,
output A,
output B
);
wire A1,B1,A2,B2;
assign A1 = x & A2;
assign A2 = A1 & y;
assign A = ~A2;
endmodule
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -W -lut 2 abc9 -D 2 -lut 2
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -fast -lut 2 abc9 -W -lut 2
abc9 -box box.txt -lut 2
ERROR: Can't open ABC output file
read_verilog ../top.v read_verilog ../top.v
tee -o result.log abc9 -luts 2:2:2:/2 abc9 -luts uu
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5
abc9 -lut 5
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5 -nomfs
abc9 -lut 5
read_verilog ../top_dff.v
proc
dff2dffe
techmap
abc9 -lut 5
abc9 -lut 5
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -lut 2 abc9 -fast -lut 2
read_verilog ../top.v read_verilog ../top.v
tee -o result.log abc9 -lut 2 abc9 -luts 2:2:2:/2
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -luts 2,3,4 abc9 -lut 2
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -markgroups -lut 2 abc9 -luts 2,3,4
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -nocleanup -lut 2 abc9 -markgroups -lut 2
read_verilog ../top_mem.v
proc
dff2dffe
synth -top top
abc9 -D 2 -lut 2
read_verilog ../top_mux.v
proc
synth -top top
abc9 -lut 2
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc9 -showtmp -lut 2 abc9 -nocleanup -lut 2
abc9 -script box.txt -lut 2
...@@ -2,4 +2,4 @@ read_verilog ../top.v ...@@ -2,4 +2,4 @@ read_verilog ../top.v
proc proc
dff2dffe dff2dffe
synth -top top synth -top top
tee -o result.log abc -D 2 abc9 -showtmp -lut 2
read_verilog ../top_mux.v
proc
techmap
abc9 -lut 2
read_verilog ../top_dff.v
abc9 -lut 2
read_verilog ../top_mux.v
proc
abc9 -lut 2
...@@ -8,10 +8,6 @@ ...@@ -8,10 +8,6 @@
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -5,11 +5,7 @@ module adff ...@@ -5,11 +5,7 @@ module adff
end end
always @( posedge clk, posedge clr ) always @( posedge clk, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -21,11 +17,7 @@ module adffn ...@@ -21,11 +17,7 @@ module adffn
end end
always @( posedge clk, negedge clr ) always @( posedge clk, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -37,11 +29,7 @@ module dffe ...@@ -37,11 +29,7 @@ module dffe
end end
always @( posedge clk ) always @( posedge clk )
if ( en ) if ( en )
`ifndef BUG
q <= d; q <= d;
`else
q <= 1'b0;
`endif
endmodule endmodule
module dffsr module dffsr
...@@ -51,11 +39,7 @@ module dffsr ...@@ -51,11 +39,7 @@ module dffsr
end end
always @( posedge clk, posedge pre, posedge clr ) always @( posedge clk, posedge pre, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( pre ) else if ( pre )
q <= 1'b1; q <= 1'b1;
else else
...@@ -69,11 +53,7 @@ module ndffnsnr ...@@ -69,11 +53,7 @@ module ndffnsnr
end end
always @( negedge clk, negedge pre, negedge clr ) always @( negedge clk, negedge pre, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre ) else if ( !pre )
q <= 1'b1; q <= 1'b1;
else else
......
...@@ -16,11 +16,7 @@ module top ...@@ -16,11 +16,7 @@ module top
// Port A // Port A
always @ (posedge clka) always @ (posedge clka)
begin begin
`ifndef BUG
if (we_a) if (we_a)
`else
if (we_b)
`endif
begin begin
ram[addr_a] <= data_a; ram[addr_a] <= data_a;
q_a <= data_a; q_a <= data_a;
...@@ -34,11 +30,7 @@ module top ...@@ -34,11 +30,7 @@ module top
// Port B // Port B
always @ (posedge clkb) always @ (posedge clkb)
begin begin
`ifndef BUG
if (we_b) if (we_b)
`else
if (we_a)
`endif
begin begin
ram[addr_b] <= data_b; ram[addr_b] <= data_b;
q_b <= data_b; q_b <= data_b;
......
...@@ -3,6 +3,7 @@ input [7:0] S, ...@@ -3,6 +3,7 @@ input [7:0] S,
input [255:0] D, input [255:0] D,
output M256 output M256
); );
parameter i = 3;
assign M256 = D[S]; assign M256 = D[S];
......
(* 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
wire width 0 \\w
read_verilog ../top.v read_verilog ../top.v
add -wire w 0 add -wire w 0
tee -o result.log dump tee -o result.out dump
ERROR: Found incompatible object with same name in module \\top2!
wire width 32000 input 6 \\gi
read_verilog ../top.v read_verilog ../top.v
add -global_input gi 32000 add -global_input gi 32000
tee -o result.log dump tee -o result.out dump
wire width 3 inout 6 \\34
read_verilog ../top.v read_verilog ../top.v
add -inout \34 3 add -inout \34 3
tee -o result.log dump tee -o result.out dump
wire width 2 input 6 \\i
read_verilog ../top.v read_verilog ../top.v
add -input i 2 add -input i 2
add -input i 2 add -input i 2
tee -o result.log dump tee -o result.out dump
read_verilog ../top.v
add -mod top3 -wire w 0
tee -o result.out dump
wire width 3 output 6 \\o
read_verilog ../top.v read_verilog ../top.v
add -output o 3 add -output o 3
tee -o result.log dump tee -o result.out dump
read_verilog ../top.v read_verilog ../top.v
add -wire w 1 add -wire w 1
tee -o result.log dump tee -o result.out dump
(* black_box *) module top module top
( (
input x, input x,
input y, input y,
...@@ -8,10 +8,20 @@ ...@@ -8,10 +8,20 @@
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x; endmodule
`endif
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
assign {cout,A} = cin * y / x;
endmodule endmodule
(* 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
read_verilog ../top_mux.v
proc
assertpmux
tee -o result.log dump
...@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y); ...@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y);
input S; input S;
input A,B; input A,B;
output reg Y; output reg Y;
`ifndef BUG
always @(*) always @(*)
Y = (S)? B : A; Y = (S)? B : A;
`else
always @(*)
Y = (~S)? B : A;
`endif
endmodule endmodule
module mux4 ( S, D, Y ); module mux4 ( S, D, Y );
...@@ -53,11 +47,7 @@ always @* ...@@ -53,11 +47,7 @@ always @*
1 : Y = D[1]; 1 : Y = D[1];
2 : Y = D[2]; 2 : Y = D[2];
3 : Y = D[3]; 3 : Y = D[3];
`ifndef BUG
4 : Y = D[4]; 4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5]; 5 : Y = D[5];
6 : Y = D[6]; 6 : Y = D[6];
7 : Y = D[7]; 7 : Y = D[7];
...@@ -83,11 +73,7 @@ always @* ...@@ -83,11 +73,7 @@ always @*
1 : Y = D[1]; 1 : Y = D[1];
2 : Y = D[2]; 2 : Y = D[2];
3 : Y = D[3]; 3 : Y = D[3];
`ifndef BUG
4 : Y = D[4]; 4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5]; 5 : Y = D[5];
6 : Y = D[6]; 6 : Y = D[6];
7 : Y = D[7]; 7 : Y = D[7];
......
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:1"
module \\bb
read_verilog ../top.v read_verilog ../top.v
blackbox bb blackbox bb
tee -o result.log dump tee -o result.out dump
read_verilog ../top.v read_verilog ../top_mem.v
blackbox top blackbox top
tee -o result.log dump tee -o result.log dump
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:15"
module \\top
read_verilog ../top.v
blackbox top
tee -o result.out dump
...@@ -8,11 +8,7 @@ module bb ...@@ -8,11 +8,7 @@ module bb
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule 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
if (we_a)
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
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -cells
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -cells tee -o result.log bugpoint -script ../script.yss -clean
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -clean tee -o result.log bugpoint -script ../script.yss -connections
ERROR: The provided script file and Yosys binary do not crash on this design!
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -connections tee -o result.log bugpoint -script ../script.yss -connections
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -connections tee -o result.log bugpoint -script ../script.yss -fast
ERROR: This command only operates on fully selected designs!
read_verilog ../top.v read_verilog ../top.v
select bb select bb
tee -o result.log bugpoint -script ../script.ys tee -o result.log bugpoint -script ../script.yss
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -grep "Simplifications exhausted"
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -fast tee -o result.log bugpoint -script ../script.yss -grep "SSS"
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -grep "SSS" tee -o result.log bugpoint -script ../script.yss -modules
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint tee -o result.log bugpoint -script ../script.yss -ports
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -modules tee -o result.log bugpoint -script ../script.yss
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -ports tee -o result.log bugpoint -script script.ys -yosys yosys.yss
read_verilog ../top2.v
abc -g cmos4
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 bb2
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
bb2 u_bb2 (x,y,cin,A,cout);
endmodule
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log check tee -o result.out check
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log check -assert tee -o result.out check -assert
ERROR: Found 1 problems in 'check -assert'.
read_verilog -sv ../top1.v read_verilog -sv ../top1.v
proc proc
tee -o result.log check -initdrv check -assert
read_verilog -sv ../top1.v read_verilog -sv ../top1.v
proc proc
tee -o result.log check -noinit tee -o result.out check -initdrv
read_verilog -sv ../top_logic_loop.v
proc
tee -o result.out check
read_verilog -sv ../top1.v
proc
tee -o result.out check -noinit
module top
(
input x,
input y,
input z,
output A,
output B
);
wire A1,B1,A2,B2;
assign A1 = x & A2;
assign A2 = A1 & y;
assign A = ~A2;
endmodule
module top
( input d, clk, output reg q );
wire u;
wire s;
assign u = s;
assign u = d;
assign u = clk;
always @( posedge clk )
q <= u;
endmodule
read_verilog -sv ../top_dff.v
chformal -remove
tee -o result.log dump
ERROR: Mode option is missing.
read_verilog -sv ../top_lat.v
chformal -remove
tee -o result.log dump
...@@ -21,7 +21,6 @@ module top ...@@ -21,7 +21,6 @@ module top
end end
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
if ($initstate) if ($initstate)
A <= 0; A <= 0;
...@@ -36,8 +35,5 @@ always @(negedge x) begin ...@@ -36,8 +35,5 @@ always @(negedge x) begin
assert(ASSERT); assert(ASSERT);
assert(s_eventually ASSERT); assert(s_eventually ASSERT);
end end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -5,11 +5,7 @@ module alat ...@@ -5,11 +5,7 @@ module alat
end end
always @(*) always @(*)
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if (en) else if (en)
q <= d; q <= d;
endmodule endmodule
...@@ -21,11 +17,7 @@ module alatn ...@@ -21,11 +17,7 @@ module alatn
end end
always @(*) always @(*)
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if (!en) else if (!en)
q <= d; q <= d;
endmodule endmodule
...@@ -37,11 +29,7 @@ module latsr ...@@ -37,11 +29,7 @@ module latsr
end end
always @(*) always @(*)
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( pre ) else if ( pre )
q <= 1'b1; q <= 1'b1;
else if ( en ) else if ( en )
...@@ -55,11 +43,7 @@ module nlatsr ...@@ -55,11 +43,7 @@ module nlatsr
end end
always @(*) always @(*)
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre ) else if ( !pre )
q <= 1'b1; q <= 1'b1;
else if ( !en ) else if ( !en )
......
ERROR: The options -set and -list cannot be used together.
read_verilog ../top.v
proc
chparam -set X 2 top
tee -o result.out chparam -list
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log chparam -set X 2 top tee -o result.out chparam -set X 2 top
...@@ -10,16 +10,12 @@ module top ...@@ -10,16 +10,12 @@ module top
wire o; wire o;
parameter X = 1; parameter X = 1;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid (x,y,o); middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule 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
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log check -assert chtype
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log chtype chtype -map $dff $adff $2
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log chtype -map $dff $adff $2 chtype $2
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o d.txt dump
tee -o result.log chtype -set $adff $2 tee -o result.log chtype -set $adff $2
tee -o d1.txt dump
ERROR: Failed to parse set lhs expression `sdf'.
ERROR: Failed to parse set rhs expression `sdf'.
ERROR: Can't find cell $procddff$2.
ERROR: Failed to parse unset expression `sdf'.
ERROR: Failed to parse port expression `dd'.
ERROR: Found processes in selected module.
ERROR: Multiple modules selected: top2, top
read_verilog -sv ../top.v
proc
connect -nomap -port $procdff$2 D d1
tee -o result.out dump
read_verilog -sv ../top.v
proc
connect -nomap -set d1 q
tee -o result.out dump
wire $auto$connect.cc:33:unset_drivers$3
read_verilog -sv ../top.v
proc
connect -nomap -unset d q
tee -o result.out dump
read_verilog -sv ../top.v
proc
connect -nounset -set d1 q
tee -o result.out dump
ERROR: Expected -set, -unset, or -port.
read_verilog -sv ../top.v
proc
connect -port $procdff$2 D d1
tee -o result.out dump
ERROR: Can't use -port together with -nounset.
read_verilog -sv ../top.v
proc
connect -set d1 q
tee -o result.out dump
ERROR: Can't use -set together with -unset and/or -port.
ERROR: Can't use -set together with -unset and/or -port.
ERROR: Can't use -set together with -unset and/or -port.
connect $auto$connect.cc:33:unset_drivers$4 \\q
read_verilog -sv ../top.v
proc
connect -set d1 q
connect -unset d1 q
tee -o result.out dump
ERROR: Can't use -unset together with -port and/or -nounset.
ERROR: Can't use -unset together with -port and/or -nounset.
ERROR: Can't use -unset together with -port and/or -nounset.
module top module top
( input d, clk, output reg q ); ( input d, d1, clk, output reg q );
always @( posedge clk ) always @( posedge clk )
q <= d; q <= d;
endmodule endmodule
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log connwrappers connwrappers
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log connwrappers -port $dff d 32000 1 connwrappers -port $dff d1 32000 1
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log connwrappers -signed $dff d 3 connwrappers -signed $dff d 3
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log connwrappers -unsigned $dff d 0 connwrappers -unsigned $dff d 0
ERROR: Can't create file aa/out.txt.
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys tee -o result.log cover -d ../test
ERROR: Can't create file in directory test.
read_verilog ../top.v read_verilog ../top.v
tee -o result.log bugpoint -script script.ys -yosys yosys.ys tee -o result.log cover -d test
...@@ -8,10 +8,6 @@ module top ...@@ -8,10 +8,6 @@ module top
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
read_verilog -sv ../top_asserts.v
tee -o result.log cutpoint top/y top/x top/cout top/A top/cin
tee -o result.log cutpoint -undef top/cin
tee -o result.log cutpoint top/$auto$cutpoint.cc:70:execute$53
dump
...@@ -8,11 +8,8 @@ module bb ...@@ -8,11 +8,8 @@ module bb
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
...@@ -21,7 +21,6 @@ module top ...@@ -21,7 +21,6 @@ module top
end end
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
if ($initstate) if ($initstate)
A <= 0; A <= 0;
...@@ -36,8 +35,5 @@ always @(negedge x) begin ...@@ -36,8 +35,5 @@ always @(negedge x) begin
assert(ASSERT); assert(ASSERT);
assert(s_eventually ASSERT); assert(s_eventually ASSERT);
end end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -8,10 +8,6 @@ module top ...@@ -8,10 +8,6 @@ module top
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
read_verilog ../top.v read_verilog ../top_mem.v
delete top/$memrd$\ram$../top.v:30$7 delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump tee -o result.log dump
read_verilog ../top_mem.v
proc
memory
delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump
...@@ -16,11 +16,7 @@ module top ...@@ -16,11 +16,7 @@ module top
// Port A // Port A
always @ (posedge clka) always @ (posedge clka)
begin begin
`ifndef BUG
if (we_a) if (we_a)
`else
if (we_b)
`endif
begin begin
ram[addr_a] <= data_a; ram[addr_a] <= data_a;
q_a <= data_a; q_a <= data_a;
...@@ -34,11 +30,7 @@ module top ...@@ -34,11 +30,7 @@ module top
// Port B // Port B
always @ (posedge clkb) always @ (posedge clkb)
begin begin
`ifndef BUG
if (we_b) if (we_b)
`else
if (we_a)
`endif
begin begin
ram[addr_b] <= data_b; ram[addr_b] <= data_b;
q_b <= data_b; q_b <= data_b;
......
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
design -save first design -save first
tee -o result.log design -copy-from first -as top_2 top design -copy-from first -as top_2 top
tee -o result.log design -copy-to first -as top_2 top design -copy-to first -as top_2 top
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
design -save first design -save first
tee -o result.log design -copy-to first top design -reset
design -copy-from first top
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
design -save first design -save first
tee -o result.log design -import first top design -reset
design -copy-to first top
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
design -save first design -save first
tee -o result.log design -copy-from first top design -import first top
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log chtype $2 design -pop
ERROR: No saved design 'first' found!
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -nomap -port $procdff$2 D d design -copy-from first -as top_2 top
ERROR: No saved design 'first' found!
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -nomap -set d q design -import first top
ERROR: No saved design 'first' found!
ERROR: No top module found in source design.
read_verilog -sv ../top.v
design -save first
design -import first
...@@ -10,17 +10,12 @@ module top ...@@ -10,17 +10,12 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o)); middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o)); u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
$_DFF_P_.Q $_XOR_.A
$_XOR_.Y $_DFF_N_.D
$_XOR_.Y $_DFF_P_.D
read_verilog ../top.v
synth
tee -o result.out edgetypes
$_ANDNOT_.Y $_OR_.A
$_AND_.Y $_OR_.B
$_XNOR_.Y $_ANDNOT_.B
$_XNOR_.Y $_XNOR_.A
read_verilog ../top_fulladder.v
edgetypes
synth
tee -o result.out edgetypes
...@@ -4,14 +4,22 @@ module top ...@@ -4,14 +4,22 @@ module top
input y, input y,
input cin, input cin,
output A, output reg A,
output cout output reg cout
); );
`ifndef BUG initial begin
assign {cout,A} = cin + y + x; begin
`else A = 0;
assign {cout,A} = cin - y * x; cout = 0;
`endif end
end
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
endmodule endmodule
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log chparam -set X 2 top tee -o result.log eval middle
tee -o result.log chparam -list
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker_x top top
ERROR: Can't find input s in module middle!
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle s 1
ERROR: Can't find module `\\u'!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u top
ERROR: Can't find module `\\u'!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u
ERROR: Can't find module dle in current design!
read_verilog ../top.v read_verilog ../top.v
tee -o result.log cover -d out_dir tee -o result.log eval -vloghammer_report middle dle x 1
ERROR: Set expression with different lhs and rhs sizes:
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 2'b11 u_rtl
ERROR: Can't perform EVAL on an empty selection!
read_verilog ../top.v
proc
tee -o result.log eval u
ERROR: Failed to parse lhs set expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -set u 0 middle
ERROR: Failed to parse pattern d!
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle x d
ERROR: Failed to parse rhs set expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
ERROR: Failed to parse show expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
ERROR: Failed to parse table expression `u'.
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
ERROR: Port \\cout in module 1 has no counterpart in module 2!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
ERROR: Modules are not equivalent!
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
ERROR: No output wire (y) found in module middle!
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
ERROR: Only one module must be selected for the EVAL pass! (selected: u_rtl and middle)
read_verilog ../top.v
proc
tee -o result.log eval
ERROR: Pattern 1'b1 is to short!
read_verilog ../top_err_2.v
tee -o result.log eval -vloghammer_report mid dle x 1'b1
ERROR: Port \\o in module 1 does not match its counterpart in module 2!
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
ERROR: Right-hand-side set expression `x' is not constant.
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
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
ERROR: Found two distinct solutions to SAT problem.
read_verilog ../top_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
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
ERROR: Wire w in module middle is not an input!
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle w 1
...@@ -31,6 +31,8 @@ module middle ...@@ -31,6 +31,8 @@ module middle
output o output o
); );
wire w;
assign o = x + y; assign o = x + y;
endmodule 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
);
wire w;
assign o = x + y;
endmodule
module u_rtl
(
input x,
input y,
output o
);
assign o = x + y;
endmodule
read_verilog -sv ../top.v
proc
fmcombine top u_mid1 u_mid3
fmcombine top u_mid2 u_mid4
fmcombine top u_mid1_u_mid3 u_mid2_u_mid4
select -assert-count 1 t:$fmcombine$fmcombine\middle
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq -bwd top u_mid1 u_mid2
read_verilog -sv ../top_assert_assume.v
proc
tee -o res_a.log stat
tee -o result.log fmcombine top u_mid1 u_mid3
tee -o result.log fmcombine top u_mid2 u_mid4
tee -o result.log fmcombine top u_mid1_u_mid3 u_mid2_u_mid4
tee -o res_b.log stat
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
read_verilog -sv ../top_dff.v
proc
tee -o result.log fmcombine -initeq top u_mid1 u_mid3
tee -o result.log fmcombine -initeq top u_mid2 u_mid4
tee -o result.log fmcombine -initeq top u_mid1_u_mid3 u_mid2_u_mid4
select -assert-count 1 t:$fmcombine$fmcombine\middle
read_verilog -sv ../top_dff.v
proc
tee -o res_a.log stat
tee -o result.log fmcombine -bwd top u_mid1 u_mid3
tee -o result.log fmcombine -bwd top u_mid2 u_mid4
tee -o result.log fmcombine -bwd top u_mid1_u_mid3 u_mid2_u_mid4
tee -o res_b.log stat
read_verilog -sv ../top.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
ERROR: Gate cell u_mid8 not found in module top.
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -nomap -unset d q tee -o result.log fmcombine top u_mid1 u_mid8
ERROR: Gold cell u_mid8 not found in module top.
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -nounset -set d q tee -o result.log fmcombine top u_mid8 u_mid3
read_verilog -sv ../top.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -port $procdff$2 D d tee -o result.log fmcombine
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -set d q tee -o result.log fmcombine topp u_mid1 u_mid3
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -bwd top u_mid1 u_mid2
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd -bwd top u_mid1 u_mid2
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd top u_mid1 u_mid2
ERROR: Types of gold and gate cells do not match.
read_verilog -sv ../top_err_1.v
proc
tee -o result.log fmcombine top u_mid1 u_urtl
...@@ -10,7 +10,6 @@ module top ...@@ -10,7 +10,6 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
...@@ -20,9 +19,6 @@ middle u_mid1 (.x(x),.o(o),.y(1'b0)); ...@@ -20,9 +19,6 @@ middle u_mid1 (.x(x),.o(o),.y(1'b0));
middle u_mid2 (.x(x),.o(o),.y(1'b1)); middle u_mid2 (.x(x),.o(o),.y(1'b1));
middle u_mid3 (.x(x),.o(o),.y(1'bX)); middle u_mid3 (.x(x),.o(o),.y(1'bX));
middle u_mid4 (.x(x),.o(o),.y(1'bX)); middle u_mid4 (.x(x),.o(o),.y(1'bX));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
...@@ -10,7 +10,6 @@ module top ...@@ -10,7 +10,6 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
...@@ -20,9 +19,6 @@ middle u_mid1 (.x(x),.A(o),.y(1'b0)); ...@@ -20,9 +19,6 @@ middle u_mid1 (.x(x),.A(o),.y(1'b0));
middle u_mid2 (.x(x),.A(o),.y(1'b1)); middle u_mid2 (.x(x),.A(o),.y(1'b1));
middle u_mid3 (.x(x),.A(o),.y(1'bX)); middle u_mid3 (.x(x),.A(o),.y(1'bX));
middle u_mid4 (.x(x),.A(o),.y(1'bX)); middle u_mid4 (.x(x),.A(o),.y(1'bX));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -49,7 +45,6 @@ module middle ...@@ -49,7 +45,6 @@ module middle
end end
end end
`ifndef BUG
always @(posedge x) begin always @(posedge x) begin
if ($initstate) if ($initstate)
A <= 0; A <= 0;
...@@ -64,8 +59,5 @@ always @(negedge x) begin ...@@ -64,8 +59,5 @@ always @(negedge x) begin
assert(ASSERT); assert(ASSERT);
assert(s_eventually ASSERT); assert(s_eventually ASSERT);
end end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -10,38 +10,37 @@ module top ...@@ -10,38 +10,37 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid1 (.x(x),.o(o),.y(1'b0)); middle u_mid1 (.clk(cin),.x(x),.o(o),.y(1'b0));
middle u_mid2 (.x(x),.o(o),.y(1'b1)); middle u_mid2 (.clk(cin),.x(x),.o(o),.y(1'b1));
middle u_mid3 (.x(x),.o(o),.y(1'bX)); middle u_mid3 (.clk(cin),.x(x),.o(o),.y(1'bX));
middle u_mid4 (.x(x),.o(o),.y(1'bX)); middle u_mid4 (.clk(cin),.x(x),.o(o),.y(1'bX));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
module middle module middle
( (
input clk,
input x, input x,
input y, input y,
output o output o
); );
urtl u_urtl (.x(x),.o(o),.y(y)); urtl u_urtl (.clk(clk),.x(x),.o(o),.y(y));
endmodule endmodule
module urtl module urtl
( (
input clk,
input x, input x,
input y, input y,
output o output reg o
); );
always @(posedge clk)
assign o = x + y; o <= x + y;
endmodule endmodule
...@@ -11,7 +11,6 @@ module top ...@@ -11,7 +11,6 @@ module top
parameter U = "string"; parameter U = "string";
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
...@@ -24,9 +23,6 @@ middle u_mid4 (.x(x),.o(o),.y(1'bX)); ...@@ -24,9 +23,6 @@ middle u_mid4 (.x(x),.o(o),.y(1'bX));
urtl u_urtl (.x(x),.o(o),.y(y)); urtl u_urtl (.x(x),.o(o),.y(y));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
read_verilog ../top.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog ../top_dff.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_ffs.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog ../top_ffs.v
proc
tee -o result.log freduce -inv
synth
tee -o result.log freduce -inv
read_verilog ../top_ffs.v
proc
tee -o result.log freduce -v
synth
tee -o result.log freduce -vv
read_verilog ../top.v
proc
tee -o result.log freduce -inv
read_verilog ../top_err_1.v
tee -o result.log freduce
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog ../top_mem.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
read_verilog ../top_mem.v
proc
tee -o result.log freduce -dump dump_a
synth
tee -o result.log freduce -dump dump_b
read_verilog ../top_mem.v
proc
tee -o result.log freduce -inv
synth
tee -o result.log freduce -inv
read_verilog ../top_mem.v
proc
tee -o result.log freduce -stop 1
synth
tee -o result.log freduce -stop 3
read_verilog ../top_mem.v
proc
tee -o result.log freduce -v
synth
tee -o result.log freduce -vv
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
...@@ -5,11 +5,7 @@ module adff ...@@ -5,11 +5,7 @@ module adff
end end
always @( posedge clk, posedge clr ) always @( posedge clk, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -21,11 +17,7 @@ module adffn ...@@ -21,11 +17,7 @@ module adffn
end end
always @( posedge clk, negedge clr ) always @( posedge clk, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else else
q <= d; q <= d;
endmodule endmodule
...@@ -37,11 +29,7 @@ module dffe ...@@ -37,11 +29,7 @@ module dffe
end end
always @( posedge clk ) always @( posedge clk )
if ( en ) if ( en )
`ifndef BUG
q <= d; q <= d;
`else
q <= 1'b0;
`endif
endmodule endmodule
module dffsr module dffsr
...@@ -51,11 +39,7 @@ module dffsr ...@@ -51,11 +39,7 @@ module dffsr
end end
always @( posedge clk, posedge pre, posedge clr ) always @( posedge clk, posedge pre, posedge clr )
if ( clr ) if ( clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( pre ) else if ( pre )
q <= 1'b1; q <= 1'b1;
else else
...@@ -69,11 +53,7 @@ module ndffnsnr ...@@ -69,11 +53,7 @@ module ndffnsnr
end end
always @( negedge clk, negedge pre, negedge clr ) always @( negedge clk, negedge pre, negedge clr )
if ( !clr ) if ( !clr )
`ifndef BUG
q <= 1'b0; q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre ) else if ( !pre )
q <= 1'b1; q <= 1'b1;
else else
......
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
tee -q -o result.log help
tee -q -o result.log help -all
tee -q -o result.log help -cells
$dff (CLK, D, Q)
No help message for this cell type found.
Run 'help $dff+' to display the Verilog model for this cell type.
tee -q -o result.out help $dff
module \\$dff (CLK, D, Q);
parameter WIDTH = 0;
parameter CLK_POLARITY = 1'b1;
input CLK;
input \[WIDTH-1:0\] D;
output reg \[WIDTH-1:0\] Q;
wire pos_clk = CLK == CLK_POLARITY;
always @(posedge pos_clk) begin
Q <= D;
end
endmodule
tee -q -o result.out help $dff+
read_verilog \[options\] \[filename\]
tee -q -o result.out help read_verilog
No such command or cell type: u
tee -q -o result.out help u
read_verilog ../top.v
proc
hilomap
select -assert-count 1 t:$dffsr
select -assert-count 4 t:$mux
select -assert-count 2 t:$not
select -assert-count 2 t:dffsr
select -assert-none t:$dffsr t:$mux t:$not t:dffsr %% t:* %D
read_verilog ../top.v
proc
hilomap -hicell VCC V
select -assert-count 4 t:VCC
select -assert-count 0 t:GND
read_verilog ../top.v
proc
hilomap -locell GND G -hicell VCC V -singleton
select assert-count 1 t:VCC
select assert-count 1 t:GND
read_verilog ../top.v
proc
hilomap -hicell VCC V -singleton
select -assert-count 2 t:VCC
select -assert-count 0 t:GND
read_verilog ../top.v
proc
hilomap -locell GND G
select -assert-count 0 t:VCC
select -assert-count 6 t:GND
read_verilog ../top.v
proc
hilomap -locell GND G -singleton
select -assert-count 0 t:VCC
select -assert-count 2 t:GND
read_verilog ../top.v
proc
hilomap -singleton
...@@ -17,26 +17,16 @@ output b,b2 ...@@ -17,26 +17,16 @@ output b,b2
dffsr u_dffsr ( dffsr u_dffsr (
.clk (clk ), .clk (clk ),
`ifndef BUG
.clr (1'b0), .clr (1'b0),
.pre (1'b1), .pre (1'b1),
`else
.clr (1'b1),
.pre (1'b0),
`endif
.d (a ), .d (a ),
.q (b ) .q (b )
); );
dffsr u2_dffsr ( dffsr u2_dffsr (
.clk (clk ), .clk (clk ),
`ifndef BUG
.clr (1'b0), .clr (1'b0),
.pre (1'b1), .pre (1'b1),
`else
.clr (1'b1),
.pre (1'b0),
`endif
.d (a ), .d (a ),
.q (b2 ) .q (b2 )
); );
......
read_verilog ../top.v
proc
synth
synth_xilinx
tee -o result.out history
...@@ -8,10 +8,6 @@ ...@@ -8,10 +8,6 @@
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
read_verilog ../top.v
synth
insbuf
select -assert-count 1 t:$_BUF_
read_verilog ../top.v
synth
insbuf -buf $_NOT_ A Y
select -assert-count 1 t:$_NOT_
read_verilog ../top.v
synth
insbuf buf
read_verilog ../top_wide.v
synth
insbuf
select -assert-count 16 t:$_BUF_
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 in;
wire [7:0] f;
top uut ( .clk(clk),
.in(in),
.out(f));
always @(posedge clk) begin
#3
in <= ~in;
end
assert_expr f_test(.clk(clk), .A(f[0]));
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
module top (
out,
in
);
output [7:0] out;
input [7:0] in;
wire [7:0] o;
assign o = in;
assign out = o;
endmodule
tee -o result.log log "OK"
tee -o result.log log -n "OK"
tee -o result.log log -nolog "OK"
tee -o result.log log -stderr "OK"
tee -o result.log log -stdout "OK"
Longest topological path in top (length=3):
0: \\x
1: $add$../top.v:13$2_Y (via $add$../top.v:13$2)
2: \\A (via $procdff$4)
3: $add$../top.v:15$3_Y (via $add$../top.v:15$3)
read_verilog ../top.v
proc
tee -o result.out ltp
Warning: Detected loop at $and$../top_logic_loop.v:13$1_Y in top
Longest topological path in top (length=3):
0: \\x
1: $and$../top_logic_loop.v:13$1_Y (via $and$../top_logic_loop.v:13$1)
2: $and$../top_logic_loop.v:14$2_Y (via $and$../top_logic_loop.v:14$2)
3: $not$../top_logic_loop.v:15$3_Y (via $not$../top_logic_loop.v:15$3)
read_verilog ../top_logic_loop.v
proc
tee -o result.out ltp
Longest topological path in top (length=1):
0: \\x
1: $add$../top.v:13$2_Y (via $add$../top.v:13$2)
ff: \\A (via $procdff$4)
read_verilog ../top.v
proc
tee -o result.out ltp -noff
Warning: Ignoring module top because it contains processes (run 'proc' command first).
read_verilog ../top.v
tee -o result.out ltp
...@@ -9,25 +9,9 @@ module top ...@@ -9,25 +9,9 @@ module top
); );
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= y + x;
assign cout = cin? y : x; assign cout = cin + A;
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 endmodule
module top
(
input x,
input y,
input z,
output A,
output B
);
wire A1,B1,A2,B2;
assign A1 = x & A2;
assign A2 = A1 & y;
assign A = ~A2;
endmodule
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_assert.v
proc
tee -o result.log miter -assert -make_outputs top miter
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
ERROR: Can't find gate module \\gate!
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log connect -unset d q tee -o result.log miter -equiv top gate top
ERROR: Can't find gold module \\gold!
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log design -pop tee -o result.log miter -equiv gold gate top
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log design -copy-from first -as top_2 top tee -o result.log miter -assert t
read_verilog ../top_equiv.v
hierarchy -top dut
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
read_verilog ../top_equiv.v
hierarchy -top dut
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
memory
opt -full
miter -equiv -flatten -ignore_gold_x -make_assert -make_outputs gold gate miter
read_verilog ../top_equiv.v
hierarchy -top dut
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
memory
opt -full
miter -equiv -flatten -make_outcmp -make_assert -make_outputs gold gate miter
read_verilog -sv ../top.v read_verilog -sv ../top.v
proc proc
tee -o result.log design -import first top tee -o result.log miter
ERROR: No matching port in gate module was found for \\y!
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv middle u_rtl top1
ERROR: No matching port in gold module was found for \\y!
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv u_rtl middle top1
ERROR: There is already a module \\top!
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top middle top
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
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 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
mutate -list 512 -o mutate.yss
script mutate.yss
select -assert-count 2 t:$add
select -assert-count 9 t:$not
select -assert-count 3 t:$xnor
select -assert-count 1 t:$xor
read_verilog ../top.v
tee -o result.log mutate -mode cnot0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -ctrlbit 1 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
select -assert-count 1 t:$xnor
read_verilog ../top.v
tee -o result.log mutate -mode cnot1 -module top -cell $add$../top.v:12$2 -port A -portbit 0 -ctrlbit 1 -src top.v:12
select -assert-count 1 t:$xor
read_verilog ../top.v
tee -o result.log mutate -mode const0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
stat
read_verilog ../top.v
tee -o result.log mutate -mode const1 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
stat
read_verilog ../top.v
tee -o result.log mutate -cell $add$../top.v:12$1 -port \Y -portbit 0 -ctrlbit 0 -module top
read_verilog ../top.v
tee -o result.log mutate -mode inv -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
select -assert-count 1 t:$not
read_verilog ../top.v
tee -o result.log mutate -list 32
read_verilog ../top.v
tee -o result.log mutate -list 32 -cfg weight_cover 1
read_verilog ../top.v
tee -o result.log mutate -list 32 -ctrl A 1 1
read_verilog ../top.v
tee -o result.log mutate -list 32 -none
read_verilog ../top.v
tee -o result.log mutate -list 32 -o o.txt
read_verilog ../top.v
tee -o result.log mutate -list 32 -s s.txt
help mutate
read_verilog ../top.v
tee -o result.log mutate -list 32 -seed 5
read_verilog ../top_mem.v
mutate -list 512 -o mutate.yss
script mutate.yss
...@@ -8,11 +8,8 @@ module top ...@@ -8,11 +8,8 @@ module top
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -16,11 +16,7 @@ module top ...@@ -16,11 +16,7 @@ module top
// Port A // Port A
always @ (posedge clka) always @ (posedge clka)
begin begin
`ifndef BUG
if (we_a) if (we_a)
`else
if (we_b)
`endif
begin begin
ram[addr_a] <= data_a; ram[addr_a] <= data_a;
q_a <= data_a; q_a <= data_a;
...@@ -34,11 +30,7 @@ module top ...@@ -34,11 +30,7 @@ module top
// Port B // Port B
always @ (posedge clkb) always @ (posedge clkb)
begin begin
`ifndef BUG
if (we_b) if (we_b)
`else
if (we_a)
`endif
begin begin
ram[addr_b] <= data_b; ram[addr_b] <= data_b;
q_b <= data_b; q_b <= data_b;
......
read_verilog ../top.v
proc
select -assert-count 13 t:$mux
select -assert-count 1 t:$pmux
select -assert-count 28 t:$eq
muxpack
select -assert-count 1 t:$mux
select -assert-count 3 t:$pmux
select -assert-count 28 t:$eq
read_verilog ../top_reduce.v
proc
muxpack
select -assert-count 1 t:$pmux
select -assert-count 16 t:$eq
select -assert-count 8 t:$reduce_or
...@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y); ...@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y);
input S; input S;
input A,B; input A,B;
output reg Y; output reg Y;
`ifndef BUG
always @(*) always @(*)
Y = (S)? B : A; Y = (S)? B : A;
`else
always @(*)
Y = (~S)? B : A;
`endif
endmodule endmodule
module mux4 ( S, D, Y ); module mux4 ( S, D, Y );
...@@ -71,11 +65,7 @@ always @* ...@@ -71,11 +65,7 @@ always @*
1 : Y = D[1]; 1 : Y = D[1];
2 : Y = D[2]; 2 : Y = D[2];
3 : Y = D[3]; 3 : Y = D[3];
`ifndef BUG
4 : Y = D[4]; 4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5]; 5 : Y = D[5];
6 : Y = D[6]; 6 : Y = D[6];
7 : Y = D[7]; 7 : Y = D[7];
......
module mux (D, S, Y);
input [7:0] D;
input [3:0] S;
output Y;
reg Y;
wire[3:0] S;
wire[7:0] D;
always @*
begin
case( S )
0,1 : Y = D[0];
2,3 : Y = D[1];
4,5 : Y = D[2];
6,7 : Y = D[3];
8,9 : Y = D[4];
10,11 : Y = D[5];
12,13 : Y = D[6];
14,15 : Y = D[7];
default: Y = 1'bx;
endcase
end
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 @*
if (S != 0) Y <= D[0];
else if (S != 1) Y <= D[1];
else if (S != 2) Y <= D[2];
else if (S != 3) Y <= D[3];
else Y <= 1'bx;
endmodule
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot
tee -o result.out
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot -v
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_1.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_2.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_3.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_4.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_5.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_6.v
proc
pmux2shiftx -onehot ignore
onehot -vv
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot ignore
onehot -vv
module mux (sel, res);
input [2:0] sel;
output [7:0] res;
reg [7:0] res;
always @(sel or res)
begin
case (sel)
3'b000 : res = 8'b00000001;
3'b001 : res = 8'b00000010;
3'b010 : res = 8'b00000100;
3'b011 : res = 8'b00001000;
3'b100 : res = 8'b00010000;
3'b101 : res = 8'b00100000;
3'b110 : res = 8'b01000000;
default : res = 8'b10000000;
endcase
end
endmodule
module mux (sel, res);
input [2:0] sel;
output [7:0] res;
reg [7:0] res;
always @(sel)
begin
case (sel)
3'b000 : res = 8'b11111110;
3'b001 : res = 8'b11111101;
3'b010 : res = 8'b11111011;
3'b011 : res = 8'b11110111;
3'b100 : res = 8'b11101111;
3'b101 : res = 8'b11011111;
3'b110 : res = 8'b10111111;
default : res = 8'b01111111;
endcase
end
endmodule
module mux (sel, res);
input [2:0] sel;
output [7:0] res;
reg [7:0] res;
always @(sel)
begin
case (sel)
3'b000 : res = 8'b00000001;
// unused decoder output
3'b001 : res = 8'bxxxxxxxx;
3'b010 : res = 8'b00000100;
3'b011 : res = 8'b00001000;
3'b100 : res = 8'b00010000;
3'b101 : res = 8'b00100000;
3'b110 : res = 8'b01000000;
default : res = 8'b10000000;
endcase
end
endmodule
module mux (sel, res);
input [2:0] sel;
output [7:0] res;
reg [7:0] res;
always @(sel or res)
begin
case (sel)
3'b000 : res = 8'b00000001;
3'b001 : res = 8'b00000010;
3'b010 : res = 8'b00000100;
3'b011 : res = 8'b00001000;
3'b100 : res = 8'b00010000;
3'b101 : res = 8'b00100000;
// 110 and 111 selector values are unused
default : res = 8'bxxxxxxxx;
endcase
end
endmodule
module priority (sel, code);
input [7:0] sel;
output [2:0] code;
reg [2:0] code;
always @(sel)
begin
if (sel[0]) code <= 3'b000;
else if (sel[1]) code <= 3'b001;
else if (sel[2]) code <= 3'b010;
else if (sel[3]) code <= 3'b011;
else if (sel[4]) code <= 3'b100;
else if (sel[5]) code <= 3'b101;
else if (sel[6]) code <= 3'b110;
else if (sel[7]) code <= 3'b111;
else code <= 3'bxxx;
end
endmodule
module lshift (DI, SEL, SO);
input [7:0] DI;
input [1:0] SEL;
output [7:0] SO;
reg[7:0] SO;
always @(DI or SEL)
begin
case (SEL)
2'b00 : SO <= DI;
2'b01 : SO <= DI << 1;
2'b10 : SO <= DI << 3;
default : SO <= DI << 2;
endcase
end
endmodule
read_verilog ../top.v
read_verilog ../bc.v
read_verilog ../demux.v
read_verilog ../mux.v
prep -flatten
opt_rmdff -sat
synth
tee -o result.log select -assert-count 0 t:$_DFF_P_
tee -o result.log plugin
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
ERROR: Can't load module
read_verilog ../top.v
tee -o result.log plugin -l
plugin -i uu -a alias
tee -o result.log plugin -l
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
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
read_verilog ../top.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 1 t:$shiftx
read_verilog ../top_2.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 1 t:$shiftx
read_verilog ../top_fsm.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 2 t:$shiftx
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_choices 0
onehot
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_choices 3000
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_density 0
onehot
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_density 3000
read_verilog ../top_fsm.v
proc
pmux2shiftx -norange
onehot
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot ignore
onehot
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot pmux
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot shiftx
onehot
read_verilog ../top.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx top
select -assert-count 1 t:$shiftx
read_verilog ../top_fsm.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx -v
select -assert-count 2 t:$shiftx
read_verilog ../top_fsm.v
proc
pmux2shiftx -vv
module fsm (
clock,
reset,
req_0,
req_1,
gnt_0,
gnt_1
);
input clock,reset,req_0,req_1;
output gnt_0,gnt_1;
wire clock,reset,req_0,req_1;
reg gnt_0,gnt_1;
parameter SIZE = 3 ;
parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
reg [SIZE-1:0] state;
reg [SIZE-1:0] next_state;
always @ (posedge clock)
begin : FSM
if (reset == 1'b1) begin
state <= #1 IDLE;
gnt_0 <= 0;
gnt_1 <= 0;
end else
case(state)
IDLE : if (req_0 == 1'b1) begin
state <= #1 GNT0;
gnt_0 <= 1;
end else if (req_1 == 1'b1) begin
gnt_1 <= 1;
state <= #1 GNT0;
end else begin
state <= #1 IDLE;
end
GNT0 : if (req_0 == 1'b1) begin
state <= #1 GNT0;
end else begin
gnt_0 <= 0;
state <= #1 IDLE;
end
GNT1 : if (req_1 == 1'b1) begin
state <= #1 GNT2;
gnt_1 <= req_0;
end
GNT2 : if (req_0 == 1'b1) begin
state <= #1 GNT1;
gnt_1 <= req_1;
end
default : state <= #1 IDLE;
endcase
end
endmodule
module top (
input clk,
input rst,
input a,
input b,
output g0,
output g1
);
fsm u_fsm ( .clock(clk),
.reset(rst),
.req_0(a),
.req_1(b),
.gnt_0(g0),
.gnt_1(g1));
endmodule
read_verilog ../top.v
proc
pmuxtree
select -assert-none t:$pmuxtree
select -assert-count 3 t:$mux
read_verilog ../top_1.v
proc
pmuxtree
select -assert-none t:$pmuxtree
select -assert-count 7 t:$mux
module mux (sel, res);
input [2:0] sel;
output [7:0] res;
reg [7:0] res;
always @(sel or res)
begin
case (sel)
3'b000 : res = 8'b00000001;
3'b001 : res = 8'b00000010;
3'b010 : res = 8'b00000100;
3'b011 : res = 8'b00001000;
3'b100 : res = 8'b00010000;
3'b101 : res = 8'b00100000;
3'b110 : res = 8'b01000000;
default : res = 8'b10000000;
endcase
end
endmodule
attribute \\qwp_position
read_verilog ../top.v
proc
qwp
tee -o result.out dump
attribute \\qwp_position
read_verilog ../top.v
proc
qwp -alpha
tee -o result.out dump
attribute \\qwp_position
read_verilog ../top.v
proc
qwp -dump out.html
tee -o result.out dump
attribute \\qwp_position
read_verilog ../top.v
proc
qwp -grid 4
tee -o result.out dump
attribute \\qwp_position
read_verilog ../top.v
proc
qwp -ltr
tee -o result.out dump
> System size: 3^2
> Edge constraints: 2
> Node constraints: 3
> Solving
> Solved
> Update nodes
> System size: 3^2
> Edge constraints: 2
> Node constraints: 3
> Solving
> Solved
> Update nodes
read_verilog ../top.v
proc
tee -o result.out qwp -v
...@@ -9,16 +9,12 @@ module top ...@@ -9,16 +9,12 @@ module top
); );
wire o; wire o;
`ifndef BUG always @(posedge cin)
//always @(posedge cin) A <= o;
// A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
//middle u_mid (x,y,o); middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
module \\mid_module
read_verilog ../top.v
proc
rename middle mid_module
tee -o result.out dump
read_verilog ../top.v
proc
rename -enumerate middle mid_module
tee -o result.out dump
read_verilog ../top.v
proc
rename -enumerate -pattern '_%_top' top
tee -o result.out dump
read_verilog ../top.v
proc
rename -hide middle mid
ERROR: Invalid number of arguments!
read_verilog ../top.v
proc
tee -o result.log rename
read_verilog ../top.v
proc
tee -o result.log rename -top
read_verilog ../top.v
synth
rename low newlow
tee -o result.out dump
ERROR: Mode -output requires that there is an active module selected.
read_verilog ../top.v
proc
tee -o result.log rename -output u uu
read_verilog ../top.v
proc
tee -o result.log rename -top top
read_verilog ../top.v
proc
tee -o result.log rename u uu
cell $add \\../top.v:
read_verilog ../top.v
proc
rename -src middle mid_module
tee -o result.out dump
read_verilog ../top.v
synth -top top
rename -top new_top
tee -o result.out dump
read_verilog ../top.v
synth -top top
rename top new_top
tee -o result.out dump
read_verilog ../top.v
proc
tee -o resulta.out dump
rename -wire top/o top/t_o
tee -o result.out dump
...@@ -9,16 +9,12 @@ module top ...@@ -9,16 +9,12 @@ module top
); );
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid (x,y,o); middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
`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
);
wire dd;
assign o = x + y;
endmodule
module low ();
endmodule
read_verilog ../top.v
proc
rmports top middle
tee -o result.out dump
module top module top
( (
input x, input x,
input y, input x,
input z,
input cin, input cin,
output reg A, output reg A,
...@@ -10,16 +11,10 @@ module top ...@@ -10,16 +11,10 @@ module top
parameter X = 1; parameter X = 1;
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
//assign cout = cin? y : x; middle u_mid (.z(z),.x(x),.o(o));
middle u_mid (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -27,6 +22,7 @@ module middle ...@@ -27,6 +22,7 @@ module middle
( (
input x, input x,
input y, input y,
input z,
output o output o
); );
......
#!/bin/bash
set -x
test -d $1
test -f scripts/$2.ys
rm -rf $1/work_$2
mkdir $1/work_$2
if [ $2 == "cover_dir" ]; then
mkdir $1/work_$2/out_dir
fi
cd $1/work_$2
touch .start
# cases where 'syntax error' or other errors are expected
if echo "$1" | grep ".*_error"; then
expected_string=""
expect_fail=0
#Change checked string for check other errors
if [ "$2" = "abc_constr_no_liberty" ]; then
expected_string="ERROR: Got -constr but no -liberty!"
elif [ "$2" = "abc_cannot_open" ]; then
expected_string="ERROR: Can't open ABC output file"
elif [ "$2" = "abc_lut_liberty" ]; then
expected_string="ERROR: Got -lut and -liberty! This two options are exclusive."
elif [ "$2" = "abc_unsup_gate_type" ]; then
expected_string="ERROR: Command syntax error: Unsupported gate type:"
elif [ "$2" = "abc_inv_luts_synt" ]; then
expected_string="Invalid -luts syntax"
elif [ "$2" = "abc_dff" ]; then
expected_string="Unknown option or option in arguments"
elif [ "$2" = "abc_return_code" ]; then
expected_string="failed: return code"
elif [ "$2" = "abc_clk_domain_not_found" ]; then
expected_string="ERROR: Clock domain u not found"
elif [ "$2" = "abc_script_o" ]; then
expected_string="ERROR: Can't open ABC output file"
elif [ "$2" = "abc_script_top" ]; then
expected_string="ERROR: Can't open ABC output file"
elif [ "$2" = "add_error" ]; then
expected_string="ERROR: Found incompatible object with same name in module"
elif [ "$2" = "bugpoint_missing_script" ]; then
expected_string="ERROR: Missing -script option"
elif [ "$2" = "bugpoint_do_not_crash" ]; then
expected_string="ERROR: The provided script file and Yosys binary do not crash on this design"
elif [ "$2" = "bugpoint_grep_string_not_found" ]; then
expected_string="ERROR: The provided grep string is not found in the log file"
elif [ "$2" = "bugpoint_fully_selected_des" ]; then
expected_string="ERROR: This command only operates on fully selected designs"
elif [ "$2" = "check_error" ]; then
expected_string="ERROR: Found 1 problems in 'check -assert'"
elif [ "$2" = "chformal_error" ]; then
expected_string="ERROR: Mode option is missing"
elif [ "$2" = "chparam_error" ]; then
expected_string="ERROR: The options -set and -list cannot be used together"
elif [ "$2" = "connect_multiple_modules" ]; then
expected_string="ERROR: Multiple modules selected:"
elif [ "$2" = "connect_found_process" ]; then
expected_string="ERROR: Found processes in selected module"
elif [ "$2" = "connect_no_modules" ]; then
expected_string="ERROR: No modules selected."
elif [ "$2" = "connect_set_with_unset" ] || \
[ "$2" = "connect_set_with_port" ] || \
[ "$2" = "connect_set_with_unset_and_port" ]; then
expected_string="ERROR: Can't use -set together with -unset and/or -port."
elif [ "$2" = "connect_cannot_parse_set_lhs_expr" ]; then
expected_string="ERROR: Failed to parse set lhs expression"
elif [ "$2" = "connect_cannot_parse_set_rhs_expr" ]; then
expected_string="ERROR: Failed to parse set rhs expression"
elif [ "$2" = "connect_unset_with_nounset" ] || \
[ "$2" = "connect_unset_with_port" ] || \
[ "$2" = "connect_unset_with_nounset_and_port" ]; then
expected_string="ERROR: Can't use -unset together with -port and/or -nounset."
elif [ "$2" = "connect_failed_parse_unset" ]; then
expected_string="ERROR: Failed to parse unset expression"
elif [ "$2" = "connect_port_with_nounset" ]; then
expected_string="ERROR: Can't use -port together with -nounset."
elif [ "$2" = "connect_cant_find_cell" ]; then
expected_string="ERROR: Can't find cell"
elif [ "$2" = "connect_failed_to_parse_port_expr" ]; then
expected_string="ERROR: Failed to parse port expression"
elif [ "$2" = "connect_opt_expected" ]; then
expected_string="Expected -set, -unset, or -port."
elif [ "$2" = "cover_cant_create_file" ]; then
expected_string="ERROR: Can't create file"
elif [ "$2" = "design_no_saved_design_copy_from" ] || \
[ "$2" = "design_no_saved_design_import" ] || \
[ "$2" = "design_no_saved_design_load" ]; then
expected_string="ERROR: No saved design"
elif [ "$2" = "design_no_pushed_design" ]; then
expected_string="ERROR: No pushed designs"
elif [ "$2" = "design_no_top_module" ]; then
expected_string="ERROR: No top module found in source design."
elif [ "$2" = "eval_only_one_module" ]; then
expected_string="ERROR: Only one module must be selected for the EVAL pass!"
elif [ "$2" = "eval_failed_to_parse_lhs" ]; then
expected_string="ERROR: Failed to parse lhs set expression"
elif [ "$2" = "eval_failed_to_parse_rhs" ]; then
expected_string="ERROR: Failed to parse rhs set expression"
elif [ "$2" = "eval_rhs_expr" ]; then
expected_string="ERROR: Right-hand-side set expression"
elif [ "$2" = "eval_diff_lhs_rhs_sizes" ]; then
expected_string="ERROR: Set expression with different lhs and rhs sizes:"
elif [ "$2" = "eval_failed_to_parse_show_expr" ]; then
expected_string="ERROR: Failed to parse show expression"
elif [ "$2" = "eval_failed_to_parse_table_expr" ]; then
expected_string="ERROR: Failed to parse table expression"
elif [ "$2" = "eval_empty_selection" ]; then
expected_string="ERROR: Can't perform EVAL on an empty selection!"
elif [ "$2" = "eval_port_doesnt_match" ]; then
expected_string="in module 1 does not match its counterpart in module 2!"
elif [ "$2" = "eval_has_no_counterpart" ]; then
expected_string="in module 1 has no counterpart in module 2!"
elif [ "$2" = "eval_cant_find_mod_1" ] || \
[ "$2" = "eval_cant_find_mod_2" ]; then
expected_string="ERROR: Can't find module"
elif [ "$2" = "eval_mods_arent_equiv" ]; then
expected_string="ERROR: Modules are not equivalent!"
elif [ "$2" = "eval_cant_find_mod_in_curr_des" ]; then
expected_string="ERROR: Can't find module dle in current design!"
elif [ "$2" = "eval_no_output_wire" ]; then
expected_string="ERROR: No output wire"
elif [ "$2" = "eval_cant_find_input" ]; then
expected_string="ERROR: Can't find input s in module middle!"
elif [ "$2" = "eval_wire_isnt_an_input" ]; then
expected_string="ERROR: Wire w in module middle is not an input!"
elif [ "$2" = "eval_failed_to_parse_pattern" ]; then
expected_string="ERROR: Failed to parse pattern d!"
elif [ "$2" = "eval_pattern_is_to_short" ]; then
expected_string="ERROR: Pattern 1'b1 is to short!"
elif [ "$2" = "eval_two_distinct_solutions" ]; then
expected_string="ERROR: Found two distinct solutions to SAT problem."
elif [ "$2" = "fmcombine_invalid_number_of_param" ]; then
expected_string="ERROR: Invalid number of arguments."
elif [ "$2" = "fmcombine_module_not_found" ]; then
expected_string="ERROR: Module topp not found."
elif [ "$2" = "fmcombine_gold_cell_not_found" ]; then
expected_string="ERROR: Gold cell u_mid8 not found in module top."
elif [ "$2" = "fmcombine_gate_cell_not_found" ]; then
expected_string="ERROR: Gate cell u_mid8 not found in module top."
elif [ "$2" = "fmcombine_types_not_match" ]; then
expected_string="ERROR: Types of gold and gate cells do not match."
elif [ "$2" = "fmcombine_nop_with_fwd" ] || \
[ "$2" = "fmcombine_nop_with_bwd" ] || \
[ "$2" = "fmcombine_nop_with_fwd_bwd" ]; then
expected_string="ERROR: Option -nop can not be combined with -fwd and/or -bwd."
elif [ "$2" = "freduce_logic_loop" ]; then
expected_string="ERROR: Found logic loop:"
elif [ "$2" = "miter_cant_find_gate_module" ]; then
expected_string="ERROR: Can't find gate module"
elif [ "$2" = "miter_cant_find_gold_module" ]; then
expected_string="ERROR: Can't find gold module"
elif [ "$2" = "miter_cant_find_module" ]; then
expected_string="ERROR: Can't find module"
elif [ "$2" = "miter_missing_mode_param" ]; then
expected_string="ERROR: Missing mode parameter!"
elif [ "$2" = "miter_no_match_in_gate" ]; then
expected_string="ERROR: No matching port in gate module was found for"
elif [ "$2" = "miter_no_match_in_gold" ]; then
expected_string="ERROR: No matching port in gold module was found for"
elif [ "$2" = "miter_there_is_already_a_module" ]; then
expected_string="ERROR: There is already a module"
elif [ "$2" = "mutate_error" ]; then
expected_string="ERROR: Invalid mode:"
elif [ "$2" = "plugin_error" ]; then
expected_string="ERROR: Can't load module"
elif [ "$2" = "rename_obj_not_found" ]; then
expected_string="ERROR: Object \`u' not found!"
elif [ "$2" = "rename_no_top_module" ]; then
expected_string="ERROR: No top module found!"
elif [ "$2" = "rename_invalid_number_of_args" ] || \
[ "$2" = "rename_invalid_number_of_args_top" ]; then
expected_string="ERROR: Invalid number of arguments!"
elif [ "$2" = "rename_mode_out_requires" ]; then
expected_string="ERROR: Mode -output requires that there is an active module selected."
elif [ "$2" = "sat_show_fail" ]; then
expected_string="ERROR: Failed to parse show expression"
elif [ "$2" = "sat_provex_diff_size" ]; then
expected_string="ERROR: Proof-x expression with different lhs and rhs sizes:"
elif [ "$2" = "sat_provex_lhs_fail" ]; then
expected_string="ERROR: Failed to parse lhs proof-x expression "
elif [ "$2" = "sat_provex_rhs_fail" ]; then
expected_string="ERROR: Failed to parse rhs proof-x expression "
elif [ "$2" = "sat_prove_rhs_fail" ]; then
expected_string="ERROR: Failed to parse rhs proof expression "
elif [ "$2" = "sat_prove_lhs_fail" ]; then
expected_string="ERROR: Failed to parse lhs proof expression "
elif [ "$2" = "sat_prove_diff_size" ]; then
expected_string="ERROR: Proof expression with different lhs and rhs sizes:"
elif [ "$2" = "sat_set_all_undef_at_fail" ] || \
[ "$2" = "sat_set_any_undef_at_fail" ] || \
[ "$2" = "sat_set_def_at_fail" ] || \
[ "$2" = "sat_set_all_undef_fail" ] || \
[ "$2" = "sat_set_any_undef_fail" ] || \
[ "$2" = "sat_set_def_fail" ]; then
expected_string="ERROR: Failed to parse set-def expression "
elif [ "$2" = "sat_unset_at_fail" ]; then
expected_string="ERROR: Failed to parse lhs set expression "
elif [ "$2" = "sat_set_at_diff_size" ]; then
expected_string="ERROR: Set expression with different lhs and rhs sizes:"
elif [ "$2" = "sat_set_at_lhs_fail" ]; then
expected_string="ERROR: Failed to parse lhs set expression"
elif [ "$2" = "sat_set_at_rhs_fail" ]; then
expected_string="ERROR: Failed to parse rhs set expression"
elif [ "$2" = "sat_set_diff_size" ]; then
expected_string="ERROR: Set expression with different lhs and rhs sizes:"
elif [ "$2" = "sat_set_rhs_fail" ]; then
expected_string="ERROR: Failed to parse rhs set expression"
elif [ "$2" = "sat_set_lhs_fail" ]; then
expected_string="ERROR: Failed to parse lhs set expression"
elif [ "$2" = "sat_cnf_open_json_file" ] || \
[ "$2" = "sat_cant_open_json_file" ] || \
[ "$2" = "sat_cant_open_vcd_file" ] ; then
expected_string="ERROR: Can't open output file"
elif [ "$2" = "sat_falsify_fail" ]; then
expected_string="ERROR: Called with -falsify and found a model"
elif [ "$2" = "sat_verify_fail" ]; then
expected_string="ERROR: Called with -verify and proof did fail!"
elif [ "$2" = "sat_maxundef_with_tempinduct" ] || \
[ "$2" = "sat_max_with_tempinduct" ] || \
[ "$2" = "sat_max_max_undef_with_tempinduct" ] || \
[ "$2" = "sat_max_maxundef_with_tempinduct" ] || \
[ "$2" = "sat_max_maxundef_all_with_tempinduct" ]; then
expected_string="ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!"
elif [ "$2" = "sat_all_with_tempinduct" ] || \
[ "$2" = "sat_max_all_with_tempinduct" ]; then
expect_fail=1
expected_string="SAT temporal induction proof finished - model found for base case: FAIL!"
elif [ "$2" = "sat_maxsteps_only_for_tempinduct" ]; then
expected_string="ERROR: The options -maxsteps is only supported for temporal induction proofs!"
elif [ "$2" = "sat_si_def_zero" ] || \
[ "$2" = "sat_si_undef_zero" ] || \
[ "$2" = "sat_si_def_undef" ] || \
[ "$2" = "sat_si_def_undef_zero" ]; then
expected_string="ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!"
elif [ "$2" = "sat_failed_to_import_cell" ]; then
expected_string="ERROR: Failed to import cell "
elif [ "$2" = "sat_prove_skip_must_be_smaller_than_seq" ]; then
expected_string="ERROR: The value of -prove-skip must be smaller than the one of -seq."
elif [ "$2" = "sat_prove_and_tempinduct" ]; then
expected_string="ERROR: Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip."
elif [ "$2" = "sat_got_tempinduct_but_nothing_to_prove" ]; then
expected_string="ERROR: Got -tempinduct but nothing to prove!"
elif [ "$2" = "sat_cant_perform_sat_on_empty_sel" ]; then
expected_string="ERROR: Can't perform SAT on an empty selection!"
elif [ "$2" = "sat_only_one_module_must_be_sel" ]; then
expected_string="ERROR: Only one module must be selected for the SAT pass! "
elif [ "$2" = "scc_expect1" ]; then
expected_string="ERROR: Found 0 SCCs but expected 1"
elif [ "$2" = "select_add_with_del" ] || \
[ "$2" = "select_assert_any_with_count" ] || \
[ "$2" = "select_assert_max_with_del" ] || \
[ "$2" = "select_assert_none_with_min" ]; then
expected_string="ERROR: Options -add, -del, -assert-none, -assert-any, assert-count, -assert-max or -assert-min can not be combined"
elif [ "$2" = "select_assert_any_failed" ]; then
expected_string="ERROR: Assertion failed: selection is empty: uuu"
elif [ "$2" = "select_assert_count_failed" ]; then
expected_string="ERROR: Assertion failed: selection contains 11 elements instead of the asserted 30: top"
elif [ "$2" = "select_assert_list_with_assert_max" ] || \
[ "$2" = "select_assert_list_with_del" ] || \
[ "$2" = "select_write_with_assert_count" ] || \
[ "$2" = "select_write_with_del" ] || \
[ "$2" = "select_count_with_assert_min" ] || \
[ "$2" = "select_count_with_assert_none" ]; then
expected_string="ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min."
elif [ "$2" = "select_assert_max_failed" ]; then
expected_string="ERROR: Assertion failed: selection contains 11 elements, more than the maximum number 1: top"
elif [ "$2" = "select_assert_min_failed" ]; then
expected_string="ERROR: Assertion failed: selection contains 11 elements, less than the minimum number 30: top"
elif [ "$2" = "select_assert_none_failed" ]; then
expected_string="ERROR: Assertion failed: selection is not empty: top"
elif [ "$2" = "select_cant_open_for_reading" ]; then
expected_string="ERROR: Can't open 'txt.txt' for reading: No such file or directory"
elif [ "$2" = "select_cant_open_for_writing" ]; then
expected_string="ERROR: Can't open './tt/ot.txt' for writing: No such file or directory"
elif [ "$2" = "select_clear_with_other_opt" ]; then
expected_string="ERROR: Option -clear can not be combined with any other options."
elif [ "$2" = "select_error_in_expand_op" ]; then
expected_string="ERROR: Syntax error in expand operator '%x:'."
elif [ "$2" = "select_none_with_other_opt" ]; then
expected_string="ERROR: Option -none can not be combined with any other options."
elif [ "$2" = "select_no_sel_to_check_as_any" ] || \
[ "$2" = "select_no_sel_to_check_as_count" ] || \
[ "$2" = "select_no_sel_to_check_as_max" ] || \
[ "$2" = "select_no_sel_to_check_as_min" ] || \
[ "$2" = "select_no_sel_to_check_as_none" ]; then
expected_string="ERROR: No selection to check."
elif [ "$2" = "select_no_such_module" ]; then
expected_string="ERROR: No such module: x"
elif [ "$2" = "select_nothing_to_add" ]; then
expected_string="ERROR: Nothing to add to selection."
elif [ "$2" = "select_nothing_to_del" ]; then
expected_string="ERROR: Nothing to delete from selection."
elif [ "$2" = "select_one_elem_for__a" ] || \
[ "$2" = "select_one_elem_for__cie" ] || \
[ "$2" = "select_one_elem_for__ci" ] || \
[ "$2" = "select_one_elem_for__coe" ] || \
[ "$2" = "select_one_elem_for__co" ] || \
[ "$2" = "select_one_elem_for__C" ] || \
[ "$2" = "select_one_elem_for__c" ] || \
[ "$2" = "select_one_elem_for__m" ] || \
[ "$2" = "select_one_elem_for__M" ] || \
[ "$2" = "select_one_elem_for__n" ] || \
[ "$2" = "select_one_elem_for__R" ] || \
[ "$2" = "select_one_elem_for__s" ] || \
[ "$2" = "select_one_elem_for__xe" ] || \
[ "$2" = "select_one_elem_for__x" ]; then
expected_string="ERROR: Must have at least one element on the stack for operator"
elif [ "$2" = "select_one_elem_for__D" ] || \
[ "$2" = "select_one_elem_for__d" ] || \
[ "$2" = "select_one_elem_for__i" ] || \
[ "$2" = "select_one_elem_for__u" ]; then
expected_string="ERROR: Must have at least two elements on the stack for operator"
elif [ "$2" = "select_read_with_selection_expr" ]; then
expected_string="ERROR: Option -read can not be combined with a selection expression."
elif [ "$2" = "select_selection_isnt_defined" ]; then
expected_string="ERROR: Selection @ is not defined!"
elif [ "$2" = "select_set_with_assert_any" ] || \
[ "$2" = "select_set_with_assert_max" ] || \
[ "$2" = "select_set_with_count" ] || \
[ "$2" = "select_set_with_del" ] || \
[ "$2" = "select_set_with_list" ]; then
expected_string="ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min."
elif [ "$2" = "select_unknown_opt" ]; then
expected_string="ERROR: Unknown option -x."
elif [ "$2" = "select_unknown_selection" ]; then
expected_string="ERROR: Unknown selection operator '%xmux'"
elif [ "$2" = "select_cd_invalid_number_of_args" ]; then
expected_string="ERROR: Invalid number of arguments."
elif [ "$2" = "select_cd_no_such_module" ]; then
expected_string="ERROR: No such module \`tt/tt' found!"
elif [ "$2" = "setattr_cant_decode_value" ]; then
expected_string="ERROR: Can't decode value "
elif [ "$2" = "setundef_expose_without_undriven" ]; then
expected_string="ERROR: Option -expose must be used with option -undriven."
elif [ "$2" = "setundef_init_with_anyconst" ] || \
[ "$2" = "setundef_init_with_anyseq" ]; then
expected_string="ERROR: The options -init and -anyseq / -anyconst are exclusive."
elif [ "$2" = "setundef_one_of_options" ]; then
expected_string="ERROR: One of the options -zero, -one, -anyseq, -anyconst, or -random <seed> must be specified."
elif [ "$2" = "setundef_undriven_with_process" ]; then
expected_string="ERROR: The 'setundef' command can't operate in -undriven mode on modules with processes. Run 'proc' first."
elif [ "$2" = "show_only_one_module" ]; then
expected_string="ERROR: For formats different than 'ps' or 'dot' only one module must be selected."
elif [ "$2" = "show_cant_open_dot_file" ]; then
expected_string="ERROR: Can't open dot file "
elif [ "$2" = "show_cant_open_lib_file" ]; then
expected_string="ERROR: Can't open lib file "
elif [ "$2" = "show_nothing_there_to_show" ]; then
expected_string="ERROR: Nothing there to show."
elif [ "$2" = "splice_port_and_no_port" ]; then
expected_string="ERROR: The options -port and -no_port are exclusive!"
elif [ "$2" = "splice_sel_by_cell_and_sel_any_bit" ]; then
expected_string="ERROR: The options -sel_by_cell and -sel_any_bit are exclusive!"
elif [ "$2" = "splice_sel_by_cell_and_sel_by_wire" ]; then
expected_string="ERROR: The options -sel_by_cell and -sel_by_wire are exclusive!"
elif [ "$2" = "stat_unsupported_tech" ]; then
expected_string="ERROR: Unsupported technology: "
elif [ "$2" = "stat_cant_find_module" ]; then
expected_string="ERROR: Can't find module"
elif [ "$2" = "stat_cant_open_lib_file" ]; then
expected_string="ERROR: Can't open liberty file "
elif [ "$2" = "tee_o_cant_create_file" ] || \
[ "$2" = "tee_a_cant_create_file" ]; then
expected_string="ERROR: Can't create file"
elif [ "$2" = "test_cell_failed_to_open" ]; then
expected_string="ERROR: Failed to open output file "
elif [ "$2" = "test_cell_unexpected_opt" ]; then
expected_string="ERROR: Unexpected option: "
elif [ "$2" = "test_cell_cell_type_not_supported" ]; then
expected_string="ERROR: The cell type \`\$_XOR_' is currently not supported. Try one of these:"
elif [ "$2" = "test_cell_no_cell_t_specified" ]; then
expected_string="ERROR: No cell type to test specified."
elif [ "$2" = "test_cell_dont_spec_cell_type_with_f" ]; then
expected_string="ERROR: Do not specify any cell types when using -f."
elif [ "$2" = "write_file_missing_name" ] || \
[ "$2" = "write_file_a_missing_name" ]; then
expected_string="ERROR: Missing output filename."
elif [ "$2" = "abc9_invalid_luts_syntax" ]; then
expected_string="ERROR: Invalid -luts syntax."
elif [ "$2" = "abc9_cant_open_output_file" ]; then
expected_string="ERROR: Can't open ABC output file"
fi
if [ "$expect_fail" = "0" ]; then
if yosys -ql yosys.log ../../scripts/$2.ys; then
echo FAIL > ${1}_${2}.status
else
if grep "$expected_string" yosys.log && [ "$expected_string" != "" ]; then
echo PASS > ${1}_${2}.status
else
echo FAIL > ${1}_${2}.status
fi
fi
else
if yosys -ql yosys.log ../../scripts/$2.ys; then
echo PASS > ${1}_${2}.status
else
if grep "$expected_string" yosys.log && [ "$expected_string" != "" ]; then
echo FAIL > ${1}_${2}.status
else
echo PASS > ${1}_${2}.status
fi
fi
fi
else
yosys -ql yosys.log ../../scripts/$2.ys
if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status
touch .stamp
exit 0
fi
#cases where some object names are/aren't expected in output file (tee -o result.log in the test script)
cell_failed="0"
expected_string=""
expected="1"
if [ "$2" = "add" ]; then
expected_string="wire width 0 \\\w"
elif [ "$2" = "add_global_input" ]; then
expected_string="wire width 32000 input 6 \\\gi"
elif [ "$2" = "add_input" ]; then
expected_string="wire width 2 input 6 \\\i"
elif [ "$2" = "add_output" ]; then
expected_string="wire width 3 output 6 \\\o"
elif [ "$2" = "add_inout" ]; then
expected_string="wire width 3 inout 6 \\\34"
elif [ "$2" = "add_wire" ]; then
expected_string="wire \\\w"
elif [ "$2" = "assertpmux" ]; then
expected_string="cell \$assert"
elif [ "$2" = "assertpmux_always" ]; then
expected_string="cell \$assert"
elif [ "$2" = "assertpmux_noinit" ]; then
expected_string="cell \$assert"
elif [ "$1" = "blackbox" ]; then
expected_string="attribute \\\blackbox 1"
elif [ "$2" = "chformal" ]; then
expected_string="cell \$assert"
expected="0"
elif [ "$2" = "chformal_assert" ]; then
expected_string="cell \$assert"
expected="0"
elif [ "$2" = "chformal_assert2assume" ]; then
expected_string="cell \$assert"
expected="0"
elif [ "$2" = "chformal_assume" ]; then
expected_string="cell \$assume"
expected="0"
elif [ "$2" = "chformal_assume2assert" ]; then
expected_string="cell \$assume"
expected="0"
elif [ "$2" = "chformal_fair" ]; then
expected_string="cell \$fair"
expected="0"
elif [ "$2" = "chformal_fair2live" ]; then
expected_string="cell \$fair"
expected="0"
elif [ "$2" = "chformal_fair2live_assert2assume" ]; then
expected_string="cell \$fair"
expected="0"
elif [ "$2" = "chformal_live" ]; then
expected_string="cell \$live"
expected="0"
elif [ "$2" = "chformal_live2fair" ]; then
expected_string="cell \$live"
expected="0"
elif [ "$2" = "delete" ]; then
expected_string="module \\\middle"
expected="0"
elif [ "$2" = "delete_proc" ]; then
expected_string="process \$proc\$../top.v:13\$1"
expected="0"
elif [ "$2" = "delete_input" ]; then
expected_string="wire input 1 \\\x"
expected="0"
elif [ "$2" = "delete_output" ]; then
expected_string="wire output 3 \\\o"
expected="0"
elif [ "$2" = "delete_port" ]; then
expected_string="wire output 4 \\\A"
expected="0"
elif [ "$2" = "delete_cell" ]; then
expected_string="cell \$mux \$ternary\$../top.v:16\$2"
expected="0"
elif [ "$2" = "delete_wire" ]; then
expected_string="wire \\\o"
expected="0"
elif [ "$2" = "delete_mem" ]; then
expected_string="cell \$memrd \$memrd\$\ram\$../top.v:30\$7"
expected="0"
elif [ "$2" = "edgetypes" ]; then
expected_string="\$add"
elif [ "$1" = "fmcombine" ]; then
expected_string="Combining cells "
elif [ "$1" = "insbuf" ]; then
expected_string="cell \$_BUF_ \$auto\$insbuf"
elif [ "$1" = "ltp" ]; then
expected_string="Longest topological path in"
elif [ "$1" = "mutate" ]; then
if [ "$2" = "mutate_all" ] || \
[ "$2" = "mutate_cnot0" ] || \
[ "$2" = "mutate_cnot1" ] || \
[ "$2" = "mutate_const0" ] || \
[ "$2" = "mutate_const1" ] || \
[ "$2" = "mutate_inv" ]; then
expected_string="\$auto\$mutate"
fi
elif [ "$1" = "mutate_mem" ]; then
if [ "$2" = "mutate_all" ]; then
expected_string="\$auto\$mutate"
fi
elif [ "$2" = "pmuxtree" ]; then
expected_string="cell \$pmux"
expected="0"
elif [ "$1" = "pmux2shiftx" ]; then
if [ "$2" = "pmux2shiftx_min_choices_3000" ] || \
[ "$2" = "pmux2shiftx_min_dens_3000" ]; then
expected="0"
fi
expected_string="cell \$shiftx"
elif [ "$1" = "qwp" ]; then
expected_string="attribute \\\qwp_position"
elif [ "$2" = "rename" ]; then
expected_string="module \\\mid_module"
elif [ "$2" = "rename_low" ]; then
expected_string="module \\\newlow"
elif [ "$2" = "rename_top" ]; then
expected_string="module \\\new_top"
elif [ "$2" = "rmports" ]; then
expected_string="wire output 5 \\\cout"
expected="0"
elif [ "$2" = "scatter" ]; then
expected_string="\$auto\$scatter"
elif [ "$1" = "scc" ] || \
[ "$1" = "scc_hier_feedback" ]; then
expected_string="0 SCCs"
if [ "$1" = "scc_hier_feedback" ] && [ "$2" = "scc_all_cell_types" ]; then
expected="0"
fi
elif [ "$1" = "scc_feedback" ]; then
expected_string="0 SCCs"
expected="0"
elif [ "$1" = "setattr" ] || \
[ "$1" = "setattr_mem" ]; then
if [ "$2" = "setattr" ] || \
[ "$2" = "setattr_top" ] || \
[ "$2" = "setattr_unset" ]; then
expected_string="attribute \\\u 1"
expected="0"
else
expected_string="attribute \\\u 1"
fi
elif [ "$1" = "sim" ] || \
[ "$1" = "sim_mem" ]; then
if [ "$2" != "sim_d" ]; then
expected_string="Simulating cycle"
fi
elif [ "$1" = "splice" ]; then
expected_string="\$auto\$splice"
elif [ "$1" = "splitnets" ]; then
if [ "$2" = "splitnets_dpf" ] || \
[ "$2" = "splitnets_driver" ]; then
expected_string="wire width 8 \$memwr"
else
expected_string="wire width 8 \$memwr"
expected="0"
fi
elif [ "$1" = "stat" ]; then
expected_string="middle 1"
elif [ "$1" = "supercover" ]; then
expected_string="cell \$cover \$auto\$supercover"
elif [ "$1" = "help" ]; then
if [ "$2" = "help" ]; then
expected_string="abc use ABC for technology mapping"
elif [ "$2" = "help_all" ]; then
expected_string="abc -- use ABC for technology mapping"
elif [ "$2" = "help_cells" ]; then
expected_string="\$_ANDNOT_ (A, B, Y)"
elif [ "$2" = "help_celltype" ]; then
expected_string="\$dff (CLK, D, Q)"
elif [ "$2" = "help_celltype_plus" ]; then
expected_string="\$dff (CLK, D, Q);"
elif [ "$2" = "help_command" ]; then
expected_string="read_verilog \[options\] \[filename\]"
elif [ "$2" = "help_no_such_command" ]; then
expected_string="No such command or cell type:"
fi
fi
if [ "$expected_string" != "" ]; then
if grep "$expected_string" result.log; then
if [ $expected = "1" ]; then
cell_failed="0"
else
cell_failed="1"
fi
else
if [ $expected = "1" ]; then
cell_failed="1"
else
cell_failed="0"
fi
fi
fi
if grep 'Assert' result.log || grep 'failed in' result.log || grep 'ERROR' result.log; then
echo FAIL > ${1}_${2}.status
elif [ $cell_failed = '1' ]; then
echo FAIL > ${1}_${2}.status
else
echo PASS > ${1}_${2}.status
fi
fi
touch .stamp
read_verilog ../top.v
proc
sat middle
read_verilog ../top.v
proc
sat -ignore_unknown_cells -all top
read_verilog -sv ../top_ff.v
synth
sat -ignore_unknown_cells -all -show q adff
read_verilog ../top.v
#proc
sat -all -prove x 1 -tempinduct middle
read_verilog ../top_ff.v
synth
sat -ignore_unknown_cells -all -prove clr 1 -tempinduct adff
read_verilog -sv ../top_ff.v
#proc
sat -ignore_unknown_cells -all -prove clr 1 -set-init s 1'b1 -tempinduct adff
read_verilog -sv ../top_ff.v
synth
# sat -ignore_unknown_cells -all -prove clr 1 -set-init q 1 -tempinduct adff
tee -o result.out sat -ignore_unknown_cells -prove clr 1 -set-init q 1 -tempinduct adff
ERROR: Found -set-init bits that are not part of the initial_state: \\o
read_verilog ../top.v
#proc
sat -all -prove x 1 -set-init o 0 -tempinduct middle
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-def -tempinduct-def middle
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-undef -tempinduct-def middle
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-zero -tempinduct-def middle
ERROR: Can't open output file `dir/out.json' for writing: No such file or directory
read_verilog ../top.v
proc
sat -dump_json dir/out.json middle
ERROR: Can't open output file `dir/out.vcd' for writing: No such file or directory
read_verilog ../top.v
proc
sat -dump_vcd dir/out.vcd middle
ERROR: Can't perform SAT on an empty selection!
ERROR: Can't open output file `dir/out.cnf' for writing: No such file or directory
read_verilog ../top.v
proc
sat -dump_cnf dir/out.cnf middle
read_verilog ../top.v
proc
sat -dump_cnf cnf.cnf middle
read_verilog ../top.v
proc
sat -dump_json json.json middle
read_verilog ../top.v
proc
sat -dump_vcd vcd.vcd middle
read_verilog ../top.v
proc
sat -enable_undef middle
ERROR: Failed to import cell inst_u_rtl (type u_rtl) to SAT database.
read_verilog ../top.v
proc
sat -prove-skip 1 -prove x 1 -seq 2 top
read_verilog ../top.v
proc
sat -prove x 1 -falsify middle
ERROR: Called with -falsify and found a model!
read_verilog ../top.v
proc
sat -falsify middle
read_verilog ../top.v
proc
sat -prove x 1 -falsify-no-timeout middle
read_verilog ../top_fsm.v
proc
sat -dump_cnf cnf.cnf -ignore_unknown_cells fsm
read_verilog ../top_fsm.v
proc
sat -dump_json json.json -ignore_unknown_cells fsm
read_verilog ../top_fsm.v
proc
sat -dump_vcd vcd.vcd -ignore_unknown_cells fsm
ERROR: Got -tempinduct but nothing to prove!
read_verilog ../top.v
sat -tempinduct middle
read_verilog ../top_div_by_zery.v
proc
sat -ignore_div_by_zero middle
Warning: Failed to import cell
read_verilog ../top_fsm.v
proc
tee -o result.out sat -ignore_unknown_cells fsm
Skipping prove for this step (-initsteps 1).
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log eval middle tee -o result.out sat -initsteps 3 -tempinduct-skip 1 -prove x 0 -set-def-at 3 x -tempinduct middle
read_verilog ../top.v
proc
sat -max 3 middle
read_verilog ../top.v
proc
sat -max 5 -all -prove x 1 -tempinduct middle
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -max_undef -all -prove x 1 -tempinduct top
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -max 1 -max_undef -all -prove x 1 -tempinduct top
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -max 1 -max_undef -prove x 1 -tempinduct top
read_verilog ../top.v
proc
sat -max_undef middle
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -max 1 -prove x 1 -tempinduct top
read_verilog ../top.v
proc
sat -maxsteps 0 middle
ERROR: The options -maxsteps is only supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -maxsteps 3 middle
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
read_verilog ../top.v
proc
sat -max_undef -prove x 1 -tempinduct top
read_verilog ../top_mux.v
proc
sat mux16
ERROR: Only one module must be selected for the SAT pass! (selected: u_rtl and middle)
read_verilog ../top.v
proc
sat -ignore_unknown_cells -prove x 1 top
ERROR: Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip.
read_verilog ../top.v
proc
sat -prove-skip 365 -prove x 1 -tempinduct top
read_verilog ../top.v
proc
sat -prove-asserts middle
ERROR: Proof expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
read_verilog ../top.v
proc
sat -prove x 2'b11 middle
ERROR: Failed to parse lhs proof expression `X'.
read_verilog ../top.v
proc
sat -prove X 0 middle
ERROR: Failed to parse rhs proof expression `X'.
read_verilog ../top.v
proc
sat -prove x X middle
read_verilog ../top.v
proc
sat -prove-skip 1 -seq 2 middle
ERROR: The value of -prove-skip must be smaller than the one of -seq.
read_verilog ../top.v
proc
sat -prove-skip 365 -prove x 1 -seq 1 top
read_verilog ../top.v
proc
sat -prove-x x 1 middle
ERROR: Proof-x expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
read_verilog ../top.v
proc
sat -prove-x x 2'b11 middle
ERROR: Failed to parse lhs proof-x expression `X'.
read_verilog ../top.v
proc
sat -prove-x X 0 middle
ERROR: Failed to parse rhs proof-x expression `X'.
read_verilog ../top.v
proc
sat -prove-x x X middle
read_verilog ../top_reg.v
hierarchy -top dut
proc
memory -nomap
equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
memory
opt -full
miter -equiv -flatten -make_assert -make_outputs gold gate miter
tee -o result.out sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
Import set-constraint: \\x = 1'1
read_verilog ../top.v
proc
tee -o result.out sat -set x 3 middle
read_verilog ../top.v
proc
sat -set-all-undef x middle
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-all-undef-at 1 x -tempinduct middle
ERROR: Failed to parse set-def expression `U'.
read_verilog ../top.v
proc
sat -set-all-undef U middle
read_verilog ../top.v
proc
sat -set-any-undef x middle
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-any-undef-at 1 x -tempinduct middle
read_verilog ../top.v
proc
sat -set-assumes middle
Import set-constraint for this timestep: \\o = 1'1
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-at 1 o 3 -tempinduct middle
read_verilog ../top.v
proc
sat -set-def x middle
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-def-at 3 x -tempinduct middle
ERROR: Failed to parse set-def expression `U'.
read_verilog ../top.v
proc
sat -set-def U middle
read_verilog ../top.v
proc
sat -set-def-inputs middle
ERROR: Set expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
read_verilog ../top.v
proc
sat -set x 2'b11 middle
read_verilog ../top.v
proc
sat -set-init x 0 middle
read_verilog ../top.v
proc
sat -set-init-def middle
read_verilog ../top.v
proc
sat -set-init-undef middle
read_verilog ../top.v
proc
sat -set-init-zero middle
ERROR: Failed to parse lhs set expression
read_verilog ../top.v
proc
sat -set X 0 middle
ERROR: Failed to parse rhs set expression
read_verilog ../top.v
proc
sat -set x X middle
read_verilog ../top.v
proc
sat -show x middle
read_verilog ../top.v
proc
sat -show-all middle
ERROR: Failed to parse show expression `X'.
read_verilog ../top.v
proc
sat -show X middle
read_verilog ../top.v
proc
sat -show-inputs middle
read_verilog ../top.v
proc
sat -show-outputs middle
read_verilog ../top.v
proc
sat -show-ports middle
read_verilog ../top.v
proc
sat -show-public middle
read_verilog ../top.v
proc
sat -ignore_unknown_cells -show-regs top
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
read_verilog ../top.v
proc
sat -set-init-undef -set-init-def middle
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
read_verilog ../top.v
proc
sat -set-init-undef -set-init-def -set-init-zero middle
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
read_verilog ../top.v
proc
sat -set-init-def -set-init-zero middle
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
read_verilog ../top.v
proc
sat -set-init-undef -set-init-zero middle
Skipping prove for this step (-stepsize 2)
read_verilog ../top.v
proc
tee -o result.out sat -tempinduct-skip 1 -stepsize 2 -prove x 0 -set-def-at 3 x -tempinduct middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly middle
read_verilog ../top.v
proc
# sat -prove x 1 -tempinduct-baseonly -maxsteps 6 -dump_cnf cnf.cnf middle
tee -o result.out sat -prove x 0 -set-def-at 3 x -dump_cnf cnf.cnf -tempinduct-baseonly middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 6 -dump_vcd vcd.vcd middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 1 middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 6 middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-def middle
read_verilog ../top.v read_verilog ../top.v
proc proc
tee -o result.log eval -brute_force_equiv_checker_x top top tee -o result.out sat -tempinduct-skip 1 -prove x 0 -set-def-at 3 x -dump_cnf cnf.cnf -tempinduct middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-inductonly middle
Skipping prove for this step (-tempinduct-skip 1)
read_verilog ../top.v
proc
tee -o result.out sat -tempinduct-skip 1 -prove x 0 -set-def-at 3 x -tempinduct middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct -tempinduct-baseonly middle
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct -tempinduct-def middle
read_verilog ../top.v
proc
sat -timeout 0 -ignore_unknown_cells top
read_verilog ../top.v
proc
sat -timeout 1 -verify -ignore_unknown_cells top
Import unset-constraint for this timestep: \\o
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -unset-at 1 o -tempinduct middle
read_verilog ../top.v
proc
sat -verify -ignore_unknown_cells -show x,y -set x y -set x 1 top
ERROR: Called with -verify and proof did fail!
read_verilog ../top.v
proc
sat -verify -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
sat -verify-no-timeout -ignore_unknown_cells -show x,y -set x y -set x 1 top
...@@ -3,19 +3,17 @@ module top ...@@ -3,19 +3,17 @@ module top
input x, input x,
input y, input y,
input cin, input cin,
(* init = 1'h0 *)
output reg A, output reg A,
output cout output cout
); );
parameter X = 1; parameter X = 1;
wire o; wire o;
initial A = 0; initial A = 0;
initial cout = 0; initial cout = 0;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
...@@ -23,9 +21,6 @@ assign cout = cin? y : x; ...@@ -23,9 +21,6 @@ assign cout = cin? y : x;
middle u_mid (.x(x),.o(o)); middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o)); u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -46,5 +41,7 @@ module u_rtl ...@@ -46,5 +41,7 @@ module u_rtl
output o output o
); );
initial o = 0;
assign o = x + y; assign o = x + y;
endmodule endmodule
...@@ -3,19 +3,17 @@ module top ...@@ -3,19 +3,17 @@ module top
input x, input x,
input y, input y,
input cin, input cin,
(* init = 1'h0 *)
output reg A, output reg A,
output cout output cout
); );
parameter X = 1; parameter X = 1;
wire o; wire o;
initial A = 0; initial A = 0;
initial cout = 0; initial cout = 0;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
...@@ -23,9 +21,6 @@ assign cout = cin? y : x; ...@@ -23,9 +21,6 @@ assign cout = cin? y : x;
middle u_mid (.x(x),.o(o)); middle u_mid (.x(x),.o(o));
u_rtl inst_u_rtl (.x(x),.o(o)); u_rtl inst_u_rtl (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
...@@ -46,5 +41,7 @@ module u_rtl ...@@ -46,5 +41,7 @@ module u_rtl
output o output o
); );
assign o = x + y; initial o = 0;
assign o = x / 0;
endmodule endmodule
module adff
(d, clk, clr, q);
input d, clk, clr;
(* init = 1'h0 *)
output reg q;
initial begin
q = 0;
end
always @( posedge clk, posedge clr )
if ( clr )
q <= 1'b0;
else
q <= d;
endmodule
module fsm (
clock,
reset,
req_0,
req_1,
gnt_0,
gnt_1
);
input clock,reset,req_0,req_1;
output gnt_0,gnt_1;
wire clock,reset,req_0,req_1;
reg gnt_0,gnt_1;
parameter SIZE = 3 ;
parameter IDLE = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
reg [SIZE-1:0] state;
reg [SIZE-1:0] next_state;
always @ (posedge clock)
begin : FSM
if (reset == 1'b1) begin
state <= #1 IDLE;
gnt_0 <= 0;
gnt_1 <= 0;
end else
case(state)
IDLE : if (req_0 == 1'b1) begin
state <= #1 GNT0;
gnt_0 <= 1;
end else if (req_1 == 1'b1) begin
gnt_1 <= 1;
state <= #1 GNT0;
end else begin
state <= #1 IDLE;
end
GNT0 : if (req_0 == 1'b1) begin
state <= #1 GNT0;
end else begin
gnt_0 <= 0;
state <= #1 IDLE;
end
GNT1 : if (req_1 == 1'b1) begin
state <= #1 GNT2;
gnt_1 <= req_0;
end
GNT2 : if (req_0 == 1'b1) begin
state <= #1 GNT1;
gnt_1 <= req_1;
end
default : state <= #1 IDLE;
endcase
end
endmodule
module top (
input clk,
input rst,
input a,
input b,
output g0,
output g1
);
fsm u_fsm ( .clock(clk),
.reset(rst),
.req_0(a),
.req_1(b),
.gnt_0(g0),
.gnt_1(g1));
endmodule
module middle
(
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
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
endmodule
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];
default: Y = 1'bx;
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];
default: Y = 1'bx;
endcase
end
endmodule
module mux16 (D, S, Y);
input [15:0] D;
input [3:0] S;
output Y;
reg Y;
wire[3:0] S;
wire[15: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];
8 : Y = D[8];
9 : Y = D[9];
10 : Y = D[10];
11 : Y = D[11];
12 : Y = D[12];
13 : Y = D[13];
14 : Y = D[14];
15 : Y = D[15];
default: Y = 1'bx;
endcase
end
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
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
wire $auto$scatter
read_verilog ../top.v
proc
scatter
tee -o result.out dump
...@@ -9,16 +9,12 @@ module top ...@@ -9,16 +9,12 @@ module top
); );
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid (x,y,o); middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
Found 1 SCCs in module top.
read_verilog ../top.v
scc top
proc
scc top
synth
tee -o result.out scc top
read_verilog ../top.v
proc
scc -all_cell_types top
Found and expected 0 SCCs.
read_verilog ../top_no_feedback.v
proc
tee -o result.out scc -expect 0 top
ERROR: Found 1 SCCs but expected 0.
read_verilog ../top.v
proc
scc -expect 0 top
read_verilog ../top_hier_feedback.v
scc top
proc
scc top
synth
scc top
read_verilog ../top.v
proc
scc -max_depth 2 top
read_verilog ../top_no_feedback.v
scc top
proc
scc top
synth
scc top
read_verilog ../top.v
proc
scc -nofeedback top
read_verilog ../top.v read_verilog ../top.v
synth -top top synth -top top
tee -o result.log abc -g cmos scc -select top
read_verilog ../top.v
proc
scc -set_attr attr true top
...@@ -7,27 +7,13 @@ module top ...@@ -7,27 +7,13 @@ module top
output reg A, output reg A,
output cout output cout
); );
wire o; parameter X = 1;
wire o_mid,o_rtl;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o_mid;
assign cout = cin? y : x; assign o_mid = x & o_rtl;
assign o_rtl = y & o_mid;
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 endmodule
...@@ -9,16 +9,12 @@ module top ...@@ -9,16 +9,12 @@ module top
); );
wire o; wire o;
`ifndef BUG
always @(posedge cin) always @(posedge cin)
A <= o; A <= o;
assign cout = cin? y : x; assign cout = cin? y : x;
middle u_mid (x,y,o); middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
......
module top
(
input x,
input y,
input cin,
output reg A,
output cout
);
wire o;
`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
tee -o result.log script ../script.ys 1:3
tee -o result.log script ../script.ys
tee -o result.log script -scriptwire ../script.ys
...@@ -8,10 +8,6 @@ ...@@ -8,10 +8,6 @@
output cout output cout
); );
`ifndef BUG
assign {cout,A} = cin + y + x; assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule endmodule
tee -o result.log abc9 -box box.txt -lut 2
tee -o result.log abc9 -script box.txt -lut 2
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -grep "Simplifications exhausted"
read_verilog -sv ../top.v
design -save first
tee -o result.log design -import first
tee -q -o result.log echo
tee -q -o result.log echo off
tee -q -o result.log echo on
read_verilog ../top.v
tee -o result.log edgetypes
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle s 1
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u top
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u
read_verilog ../top.v
tee -o result.log eval -vloghammer_report middle dle x 1
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 -set x 1 -set y 2'b11 u_rtl
read_verilog ../top.v
proc
tee -o result.log eval u
read_verilog ../top.v
proc
tee -o result.log eval -set u 0 middle
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle x d
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
read_verilog ../top.v
proc
tee -o result.log eval
read_verilog ../top_err_2.v
tee -o result.log eval -vloghammer_report mid dle x 1'b1
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
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_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
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
tee -o result.log eval -vloghammer_report mid dle w 1
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine top u_mid1 u_mid3
tee -o result.log fmcombine top u_mid2 u_mid4
tee -o result.log fmcombine top u_mid1_u_mid3 u_mid2_u_mid4
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine top u_mid1 u_mid8
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine top u_mid8 u_mid3
read_verilog -sv ../top.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine topp u_mid1 u_mid3
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -bwd top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd top u_mid1 u_mid2
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd -bwd top u_mid1 u_mid2
read_verilog -sv ../top_err_1.v
proc
tee -o result.log fmcombine top u_mid1 u_urtl
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_err_1.v
tee -o result.log freduce
proc
tee -o result.log freduce
synth
tee -o result.log freduce
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
tee -q -o result.log help
tee -q -o result.log help -all
tee -q -o result.log help -cells
tee -q -o result.log help $dff
tee -q -o result.log help $dff+
tee -q -o result.log help read_verilog
read_verilog ../top.v
proc
tee -o result.log hilomap
read_verilog ../top.v
proc
tee -o result.log hilomap -hicell VCC V
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G -hicell VCC V -singleton
read_verilog ../top.v
proc
tee -o result.log hilomap -hicell VCC V -singleton
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G -singleton
read_verilog ../top.v
proc
tee -o result.log hilomap -singleton
read_verilog ../top.v
tee -o result.log history
read_verilog ../top.v
synth
insbuf
tee -o result.log dump
write_verilog synth.v
read_verilog ../top.v
synth
insbuf -buf $_BUF_ A Y
tee -o result.log dump
write_verilog synth.v
tee -o result.log log "OK"
tee -o result.log log -n "OK"
tee -o result.log log -nolog "OK"
tee -o result.log log -stderr "OK"
tee -o result.log log -stdout "OK"
read_verilog ../top.v
proc
tee -o result.log ltp
read_verilog ../top.v
proc
tee -o result.log ltp -noff
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
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top gate top
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv gold gate top
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert t
read_verilog -sv ../top.v
proc
tee -o result.log miter
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv middle u_rtl top1
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv u_rtl middle top1
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top middle top
read_verilog ../top.v
mutate -list 512 -o mutate.ys
script mutate.ys
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -mode cnot0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -ctrlbit 1 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -mode cnot1 -module top -cell $add$../top.v:12$2 -port A -portbit 0 -ctrlbit 1 -src top.v:12
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -mode const0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -mode const1 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -cell $add$../top.v:12$1 -port \Y -portbit 0 -ctrlbit 0 -module top
read_verilog ../top.v
tee -o result.log mutate -mode inv -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
tee -o result.log dump
read_verilog ../top.v
tee -o result.log mutate -list 32
read_verilog ../top.v
tee -o result.log mutate -list 32 -cfg weight_cover 1
read_verilog ../top.v
tee -o result.log mutate -list 32 -ctrl A 1 1
read_verilog ../top.v
tee -o result.log mutate -list 32 -none
read_verilog ../top.v
tee -o result.log mutate -list 32 -o o.txt
read_verilog ../top.v
tee -o result.log mutate -list 32 -s s.txt
read_verilog ../top.v
tee -o result.log mutate -list 32 -seed 5
read_verilog ../top.v
proc
tee -o result.log muxpack
read_verilog ../top.v
proc
pmux2shiftx
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx
onehot -v
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx
onehot -vv
tee -o result.log dump
read_verilog ../top.v
read_verilog ../bc.v
read_verilog ../demux.v
read_verilog ../mux.v
prep -flatten
opt_rmdff -sat
synth
tee -o result.log select -assert-count 0 t:$_DFF_P_
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 -l
plugin -i uu -a alias
tee -o result.log plugin -l
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
pmux2shiftx
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -min_choices 0
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -min_choices 3000
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -min_density 0
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -min_density 3000
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -norange
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -onehot pmux
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -onehot shiftx
onehot
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx top
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -v
tee -o result.log dump
read_verilog ../top.v
proc
pmux2shiftx -vv
tee -o result.log dump
read_verilog ../top.v
proc
pmuxtree
tee -o result.log dump
read_verilog ../top.v
proc
qwp
tee -o result.log dump
read_verilog ../top.v
proc
qwp -alpha
tee -o result.log dump
read_verilog ../top.v
proc
qwp -dump out.html
tee -o result.log dump
read_verilog ../top.v
proc
qwp -grid 4
tee -o result.log dump
read_verilog ../top.v
proc
qwp -ltr
tee -o result.log dump
read_verilog ../top.v
proc
qwp -v
tee -o result.log dump
read_verilog ../top.v
proc
tee -o result.log rename middle mid_module
tee -o result.log dump
read_verilog ../top.v
proc
tee -o result.log rename -enumerate middle mid_module
read_verilog ../top.v
proc
tee -o result.log rename -enumerate -pattern '_%_' top
read_verilog ../top.v
proc
tee -o result.log rename -hide middle mid
read_verilog ../top.v
proc
tee -o result.log rename
read_verilog ../top.v
proc
tee -o result.log rename -top
read_verilog ../top.v
synth
tee -o result.log rename low newlow
tee -o result.log dump
read_verilog ../top.v
proc
tee -o result.log rename -output u uu
read_verilog ../top.v
proc
tee -o result.log rename -top top
read_verilog ../top.v
proc
tee -o result.log rename u uu
read_verilog ../top.v
proc
tee -o result.log rename -src middle mid_module
read_verilog ../top.v
synth -top top
tee -o result.log rename -top new_top
tee -o result.log dump
read_verilog ../top.v
synth -top top
tee -o result.log rename top new_top
read_verilog ../top.v
proc
tee -o result.log rename -wire o mid_o
read_verilog ../top.v
proc
rmports
tee -o result.log dump
read_verilog ../top.v
proc
tee -o result.log sat middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -all top
read_verilog ../top.v
proc
tee -o result.log sat -all -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_json dir/out.json middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_vcd dir/out.vcd middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_cnf dir/out.cnf middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_cnf cnf.cnf middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_json json.json middle
read_verilog ../top.v
proc
tee -o result.log sat -dump_vcd vcd.vcd middle
read_verilog ../top.v
proc
tee -o result.log sat -enable_undef middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 1 -prove x 1 -seq 2 top
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify middle
read_verilog ../top.v
proc
tee -o result.log sat -falsify middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify-no-timeout middle
read_verilog ../top.v
tee -o result.log sat -tempinduct middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore-div-by-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells top
read_verilog ../top.v
proc
tee -o result.log sat -initsteps 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -max 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -max 5 -all -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
tee -o result.log sat -max_undef -all -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -max_undef -all -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -max_undef -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat -max_undef middle
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat -maxsteps 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -maxsteps 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -max_undef -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -prove x 1 top
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 365 -prove x 1 -tempinduct top
read_verilog ../top.v
proc
tee -o result.log sat -prove-asserts middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 2'b11 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove X 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x X middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 1 -seq 2 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 365 -prove x 1 -seq 1 top
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x 1 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x 2'b11 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-x X 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x X middle
read_verilog ../top.v
proc
tee -o result.log sat -seq 1 middle
read_verilog ../top.v
proc
tee -o result.log sat -set x 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef-at 3 x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef-at U 1 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef U middle
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef-at 3 x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef-at U middle
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef U middle
read_verilog ../top.v
proc
tee -o result.log sat -set-assumes middle
read_verilog ../top.v
proc
tee -o result.log sat -set-at 1 x 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-at x 2'b11 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-at X 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-at x X middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def-at 3 x middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def-at U middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def U middle
read_verilog ../top.v
proc
tee -o result.log sat -set-def-inputs middle
read_verilog ../top.v
proc
tee -o result.log sat -set x 2'b11 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init x 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-def middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -set X 0 middle
read_verilog ../top.v
proc
tee -o result.log sat -set x X middle
read_verilog ../top.v
proc
tee -o result.log sat -show x middle
read_verilog ../top.v
proc
tee -o result.log sat -show-all middle
read_verilog ../top.v
proc
tee -o result.log sat -show X middle
read_verilog ../top.v
proc
tee -o result.log sat -show-inputs middle
read_verilog ../top.v
proc
tee -o result.log sat -show-outputs middle
read_verilog ../top.v
proc
tee -o result.log sat -show-ports middle
read_verilog ../top.v
proc
tee -o result.log sat -show-public middle
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -show-regs top
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-def middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-def -set-init-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-def -set-init-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-zero middle
read_verilog ../top.v
proc
tee -o result.log sat -stepsize 3 middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-baseonly middle
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-baseonly -maxsteps 1 middle
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