Skip to content

Y
yosys-tests
Unverified Commit 98d6a5fa by Miodrag Milanović Committed by GitHub
Options

Merge pull request #82 from SergeyDegtyar/review_misc_group 

Review misc group
parents 3f099e58 ee7949ea
Showing with 2547 additions and 2534 deletions

Too many changes to show.
Plain diff Email patch

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

misc/.gitignore
*/work_*/
/.stamp
/run-test.mk
misc/Makefile
all: work
touch .stamp
PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
clean::
rm -f .stamp
all::
define template
$(foreach design,$(1),
$(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))
run-test.mk: ../generate.py
@$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
include run-test.mk
.PHONY: all clean
misc/scripts/abc_g_simple.ys → misc/abc/abc.ys
......@@ -2,4 +2,9 @@ read_verilog ../top.v
proc
dff2dffe
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
misc/scripts/abc9_D.ys → misc/abc/abc_D.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -D 2 -lut 2
tee -o result.out abc -D 2
misc/abc/abc_cannot_open_fail.pat 0 → 100644
ERROR: Can't open ABC output file
misc/scripts/abc_cannot_open.ys → misc/abc/abc_cannot_open_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -liberty -constr
tee -o result.out abc -liberty -constr
abc -liberty -constr
misc/abc/abc_clk_domain_not_found_fail.pat 0 → 100644
ERROR: Clock domain u not found.
misc/scripts/abc_clk_domain_not_found.ys → misc/abc/abc_clk_domain_not_found_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -dff -clk u
tee -o result.out abc -dff -clk u
abc -dff -clk u
misc/scripts/abc_constr_liberty.ys → misc/abc/abc_constr_liberty.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -liberty -constr top.lib
tee -o result.out abc -liberty -constr top.lib
misc/abc/abc_constr_no_liberty_fail.pat 0 → 100644
ERROR: Got -constr but no -liberty!
misc/scripts/abc_constr_no_liberty.ys → misc/abc/abc_constr_no_liberty_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -constr -liberty
tee -o result.out abc -constr -liberty
abc -constr -liberty
misc/abc/abc_dff.ys 0 → 100644
read_verilog ../top_dff.v
synth -top top
dff2dffe
tee -o result.log abc -dff
abc -dff
misc/abc/abc_dff_keepff.ys 0 → 100644
read_verilog ../top_dff.v
synth -top top
tee -o result.log abc -keepff
abc -dff
misc/abc/abc_div_mul.ys 0 → 100644
read_verilog ../top_div_mul.v
proc
dff2dffe
synth -top top
tee -o result.out abc
misc/abc/abc_ffs.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc
misc/abc/abc_ffs_clk.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -clk clk
misc/abc/abc_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc
misc/abc/abc_fsm_all.disable 0 → 100644
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
misc/abc/abc_fsm_all.ys 0 → 100644
read_verilog ../top_fsm.v
synth -top top
tee -o result.out abc -g all
misc/abc/abc_fsm_cmos4.ys 0 → 100644
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_
misc/abc/abc_fsm_gates.ys 0 → 100644
read_verilog ../top_fsm.v
synth -top top
abc -g gates
misc/abc/abc_g_aig.ys 0 → 100644
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_
misc/abc/abc_g_cmos.ys 0 → 100644
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_
misc/abc/abc_g_cmos2.ys 0 → 100644
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_
misc/abc/abc_g_simple.ys 0 → 100644
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_
misc/scripts/abc_dff.ys → misc/abc/abc_i.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -dff
tee -o result.log abc -I 4
abc -dff
misc/abc/abc_inv_luts_synt_fail.pat 0 → 100644
ERROR: Invalid -luts syntax.
misc/scripts/abc_inv_luts_synt.ys → misc/abc/abc_inv_luts_synt_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -luts :
tee -o result.out abc -luts :
abc -liberty -luts :
misc/abc/abc_logic.ys 0 → 100644
read_verilog ../top_logic.v
proc
synth -top top
tee -o result.out abc
misc/abc/abc_logic_loop.ys 0 → 100644
read_verilog ../top_logic_loop.v
proc
synth -top top
tee -o result.out abc
misc/abc/abc_lut.ys 0 → 100644
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut 4
abc -lut 3
stat
misc/abc/abc_lut_liberty_fail.pat 0 → 100644
ERROR: Got -lut and -liberty! This two options are exclusive.
misc/scripts/abc_lut_liberty.ys → misc/abc/abc_lut_liberty_fail.ys
read_verilog ../top.v
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
misc/abc/abc_lut_neg.ys 0 → 100644
read_verilog ../top.v
synth -top top
tee -o result.log abc -lut -4
abc -lut -3:1
misc/scripts/abc_g_aig.ys → misc/abc/abc_luts.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -g aig
tee -o result.log abc -luts 3:4
misc/abc/abc_markgroups.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
tee -o result.out abc -markgroups
misc/abc/abc_mux.ys 0 → 100644
read_verilog ../top_mux.v
proc
synth -top top
abc
select -assert-count 139 t:$_MUX_
misc/abc/abc_mux16.ys 0 → 100644
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux16
stat
misc/abc/abc_mux4.ys 0 → 100644
read_verilog ../top_mux.v
synth -top top
abc -mux4
select -assert-count 75 t:$_MUX4_
misc/abc/abc_mux8.ys 0 → 100644
read_verilog ../top_mux.v
synth -top top
tee -o result.log abc -mux8
stat
misc/abc/abc_mux_cmos3.ys 0 → 100644
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_
misc/abc/abc_mux_cmos4.ys 0 → 100644
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_
misc/scripts/abc9_cant_open_output_file.ys → misc/abc/abc_no_proc.ys
read_verilog ../top.v
tee -o result.log abc9 -luts uu
tee -o result.out abc
misc/scripts/abc9_wo_synth.ys → misc/abc/abc_no_synth.ys
read_verilog ../top.v
proc
tee -o result.log abc9 -lut 2
tee -o result.out abc
misc/abc/abc_p.ys 0 → 100644
read_verilog ../top.v
synth -top top
tee -o result.log abc -P 4
abc -dff
misc/abc/abc_return_code_fail.pat 0 → 100644
failed: return code 134.
misc/scripts/abc_return_code.ys → misc/abc/abc_return_code_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -g XOR
tee -o result.out abc -g XOR
abc -g XOR
misc/abc/abc_script_o_fail.pat 0 → 100644
ERROR: Can't open ABC output file
misc/scripts/abc_script_o.ys → misc/abc/abc_script_o_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -script o
tee -o result.out abc -script o
abc -script o
misc/abc/abc_script_top_fail.pat 0 → 100644
ERROR: Can't open ABC output file
misc/abc/abc_script_top_fail.ys 0 → 100644
read_verilog ../top.v
synth -top top
tee -o result.out abc -script top.yss
abc -script top.yss
misc/abc/abc_skip_module.ys 0 → 100644
read_verilog ../top_dff.v
tee -o result.out abc
misc/abc/abc_unsup_gate_type_fail.pat 0 → 100644
ERROR: Command syntax error: Unsupported gate type: XO
misc/scripts/abc_unsup_gate_type.ys → misc/abc/abc_unsup_gate_type_fail.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -g XO
tee -o result.out abc -g XO
abc -g XO
misc/abc/top.v
......@@ -8,10 +8,6 @@
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/abc9_dff/top.v → misc/abc/top_dff.v
......@@ -5,11 +5,7 @@ module adff
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -21,11 +17,7 @@ module adffn
end
always @( posedge clk, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -37,11 +29,7 @@ module dffe
end
always @( posedge clk )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
endmodule
module dffsr
......@@ -51,11 +39,7 @@ module dffsr
end
always @( posedge clk, posedge pre, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else
......@@ -69,11 +53,7 @@ module ndffnsnr
end
always @( negedge clk, negedge pre, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else
......@@ -95,7 +75,7 @@ dffsr u_dffsr (
.d (a ),
.q (b )
);
ndffnsnr u_ndffnsnr (
.clk (clk ),
.clr (clr),
......@@ -103,21 +83,21 @@ ndffnsnr u_ndffnsnr (
.d (a ),
.q (b1 )
);
adff u_adff (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b2 )
);
adffn u_adffn (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
......
misc/abc_error/top.v → misc/abc/top_div_mul.v
......@@ -8,10 +8,6 @@ module top
output cout
);
`ifndef BUG
assign cout = x / y * cin;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/abc/top_fsm.v 0 → 100644
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
misc/abc/top_logic.v 0 → 100644
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
misc/abc/top_logic_loop.v 0 → 100644
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
misc/scripts/abc9_W.ys → misc/abc9/abc9_D.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -W -lut 2
abc9 -D 2 -lut 2
misc/scripts/abc9_fast.ys → misc/abc9/abc9_W.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -fast -lut 2
abc9 -W -lut 2
misc/abc9/abc9_box.ys 0 → 100644
abc9 -box box.txt -lut 2
misc/abc9/abc9_cant_open_output_file_fail.pat 0 → 100644
ERROR: Can't open ABC output file
misc/abc9/abc9_dff.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5
abc9 -lut 5
misc/abc9/abc9_dff_nomfs.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
synth -top top
abc9 -lut 5 -nomfs
abc9 -lut 5
misc/abc9/abc9_dff_techmap.ys 0 → 100644
read_verilog ../top_dff.v
proc
dff2dffe
techmap
abc9 -lut 5
abc9 -lut 5
misc/scripts/abc9_lut.ys → misc/abc9/abc9_fast.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -lut 2
abc9 -fast -lut 2
misc/scripts/abc9_wo_proc.ys → misc/abc9/abc9_invalid_luts_syntax_fail.ys
read_verilog ../top.v
tee -o result.log abc9 -lut 2
abc9 -luts 2:2:2:/2
misc/scripts/abc9_luts.ys → misc/abc9/abc9_lut.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -luts 2,3,4
abc9 -lut 2
misc/scripts/abc9_markgroups.ys → misc/abc9/abc9_luts.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -markgroups -lut 2
abc9 -luts 2,3,4
misc/scripts/abc9_nocleanup.ys → misc/abc9/abc9_markgroups.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -nocleanup -lut 2
abc9 -markgroups -lut 2
misc/abc9/abc9_mem.ys 0 → 100644
read_verilog ../top_mem.v
proc
dff2dffe
synth -top top
abc9 -D 2 -lut 2
misc/abc9/abc9_mux.ys 0 → 100644
read_verilog ../top_mux.v
proc
synth -top top
abc9 -lut 2
misc/scripts/abc9_showtmp.ys → misc/abc9/abc9_nocleanup.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc9 -showtmp -lut 2
abc9 -nocleanup -lut 2
misc/abc9/abc9_script.ys 0 → 100644
abc9 -script box.txt -lut 2
misc/scripts/abc_D.ys → misc/abc9/abc9_showtmp.ys
......@@ -2,4 +2,4 @@ read_verilog ../top.v
proc
dff2dffe
synth -top top
tee -o result.log abc -D 2
abc9 -showtmp -lut 2
misc/abc9/abc9_techmap.ys 0 → 100644
read_verilog ../top_mux.v
proc
techmap
abc9 -lut 2
misc/abc9/abc9_wo_proc.ys 0 → 100644
read_verilog ../top_dff.v
abc9 -lut 2
misc/abc9/abc9_wo_synth.ys 0 → 100644
read_verilog ../top_mux.v
proc
abc9 -lut 2
misc/abc9/top.v
......@@ -8,10 +8,6 @@
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/abc_dff/top.v → misc/abc9/top_dff.v
......@@ -5,11 +5,7 @@ module adff
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -21,11 +17,7 @@ module adffn
end
always @( posedge clk, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -37,11 +29,7 @@ module dffe
end
always @( posedge clk )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
endmodule
module dffsr
......@@ -51,11 +39,7 @@ module dffsr
end
always @( posedge clk, posedge pre, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else
......@@ -69,11 +53,7 @@ module ndffnsnr
end
always @( negedge clk, negedge pre, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else
......@@ -95,7 +75,7 @@ dffsr u_dffsr (
.d (a ),
.q (b )
);
ndffnsnr u_ndffnsnr (
.clk (clk ),
.clr (clr),
......@@ -103,21 +83,21 @@ ndffnsnr u_ndffnsnr (
.d (a ),
.q (b1 )
);
adff u_adff (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b2 )
);
adffn u_adffn (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
......
misc/mutate_mem/top.v → misc/abc9/top_mem.v
......@@ -7,38 +7,30 @@ module top
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
......@@ -48,5 +40,5 @@ module top
q_b <= ram[addr_b];
end
end
endmodule
endmodule
misc/abc_mux/top.v → misc/abc9/top_mux.v
......@@ -3,6 +3,7 @@ input [7:0] S,
input [255:0] D,
output M256
);
parameter i = 3;
assign M256 = D[S];
......
misc/abc9_error/top.v deleted 100644 → 0
(* black_box *) module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/add/add.pat 0 → 100644
wire width 0 \\w
misc/scripts/add.ys → misc/add/add.ys
read_verilog ../top.v
add -wire w 0
tee -o result.log dump
tee -o result.out dump
misc/add/add_error_fail.pat 0 → 100644
ERROR: Found incompatible object with same name in module \\top2!
misc/add/add_global_input.pat 0 → 100644
wire width 32000 input 6 \\gi
misc/scripts/add_global_input.ys → misc/add/add_global_input.ys
read_verilog ../top.v
add -global_input gi 32000
tee -o result.log dump
tee -o result.out dump
misc/add/add_inout.pat 0 → 100644
wire width 3 inout 6 \\34
misc/scripts/add_inout.ys → misc/add/add_inout.ys
read_verilog ../top.v
add -inout \34 3
tee -o result.log dump
tee -o result.out dump
misc/add/add_input.pat 0 → 100644
wire width 2 input 6 \\i
misc/scripts/add_input.ys → misc/add/add_input.ys
read_verilog ../top.v
add -input i 2
add -input i 2
tee -o result.log dump
tee -o result.out dump
misc/add/add_mod.ys 0 → 100644
read_verilog ../top.v
add -mod top3 -wire w 0
tee -o result.out dump
misc/add/add_output.pat 0 → 100644
wire width 3 output 6 \\o
misc/scripts/add_output.ys → misc/add/add_output.ys
read_verilog ../top.v
add -output o 3
tee -o result.log dump
tee -o result.out dump
misc/scripts/add_wire.ys → misc/add/add_wire.ys
read_verilog ../top.v
add -wire w 1
tee -o result.log dump
tee -o result.out dump
misc/add/top.v
(* black_box *) module top
module top
(
input x,
input y,
......@@ -8,10 +8,20 @@
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
);
assign {cout,A} = cin * y / x;
endmodule
misc/add_error/top.v deleted 100644 → 0
(* black_box *) module top
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/assertpmux/assertpmux_mux.ys 0 → 100644
read_verilog ../top_mux.v
proc
assertpmux
tee -o result.log dump
misc/assertpmux_mux/top.v → misc/assertpmux/top_mux.v
......@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
`ifndef BUG
always @(*)
Y = (S)? B : A;
`else
always @(*)
Y = (~S)? B : A;
`endif
endmodule
module mux4 ( S, D, Y );
......@@ -53,11 +47,7 @@ always @*
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
`ifndef BUG
4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
......@@ -83,11 +73,7 @@ always @*
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
`ifndef BUG
4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
......
misc/blackbox/blackbox.pat 0 → 100644
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:1"
module \\bb
misc/scripts/blackbox.ys → misc/blackbox/blackbox.ys
read_verilog ../top.v
blackbox bb
tee -o result.log dump
tee -o result.out dump
misc/scripts/blackbox_top.ys → misc/blackbox/blackbox_mem.ys
read_verilog ../top.v
read_verilog ../top_mem.v
blackbox top
tee -o result.log dump
misc/blackbox/blackbox_top.pat 0 → 100644
attribute \\blackbox 1
attribute \\cells_not_processed 1
attribute \\src "../top.v:15"
module \\top
misc/blackbox/blackbox_top.ys 0 → 100644
read_verilog ../top.v
blackbox top
tee -o result.out dump
misc/blackbox/top.v
......@@ -8,11 +8,7 @@ module bb
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
......
misc/blackbox/top_mem.v 0 → 100644
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
misc/bugpoint/bugpoint_cells_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -cells
misc/scripts/bugpoint_cells.ys → misc/bugpoint/bugpoint_clean_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -cells
tee -o result.log bugpoint -script ../script.yss -clean
misc/scripts/bugpoint_clean.ys → misc/bugpoint/bugpoint_connections_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -clean
tee -o result.log bugpoint -script ../script.yss -connections
misc/bugpoint/bugpoint_do_not_crash_fail.pat 0 → 100644
ERROR: The provided script file and Yosys binary do not crash on this design!
misc/scripts/bugpoint_connections.ys → misc/bugpoint/bugpoint_do_not_crash_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -connections
tee -o result.log bugpoint -script ../script.yss -connections
misc/scripts/bugpoint_do_not_crash.ys → misc/bugpoint/bugpoint_fast_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -connections
tee -o result.log bugpoint -script ../script.yss -fast
misc/bugpoint/bugpoint_fully_selected_des_fail.pat 0 → 100644
ERROR: This command only operates on fully selected designs!
misc/scripts/bugpoint_fully_selected_des.ys → misc/bugpoint/bugpoint_fully_selected_des_fail.ys
read_verilog ../top.v
select bb
tee -o result.log bugpoint -script ../script.ys
tee -o result.log bugpoint -script ../script.yss
misc/bugpoint/bugpoint_grep_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.yss -grep "Simplifications exhausted"
misc/scripts/bugpoint_fast.ys → misc/bugpoint/bugpoint_grep_string_not_found_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -fast
tee -o result.log bugpoint -script ../script.yss -grep "SSS"
misc/scripts/bugpoint_grep_string_not_found.ys → misc/bugpoint/bugpoint_modules_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -grep "SSS"
tee -o result.log bugpoint -script ../script.yss -modules
misc/scripts/bugpoint_missing_script.ys → misc/bugpoint/bugpoint_ports_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint
tee -o result.log bugpoint -script ../script.yss -ports
misc/scripts/bugpoint_modules.ys → misc/bugpoint/bugpoint_script_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -modules
tee -o result.log bugpoint -script ../script.yss
misc/scripts/bugpoint_ports.ys → misc/bugpoint/bugpoint_yosys.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -ports
tee -o result.log bugpoint -script script.ys -yosys yosys.yss
misc/bugpoint_error/script.ys deleted 100644 → 0
read_verilog ../top2.v
abc -g cmos4
misc/bugpoint_error/top.v deleted 100644 → 0
module bb
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top
(
input x,
input y,
input cin,
output A,
output cout
);
bb u_bb (x,y,cin,A,cout);
endmodule
misc/bugpoint_error/top2.v deleted 100644 → 0
module bb2
(
input x,
input y,
input cin,
output A,
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output A,
output cout
);
bb2 u_bb2 (x,y,cin,A,cout);
endmodule
misc/scripts/check.ys → misc/check/check.ys
read_verilog -sv ../top.v
proc
tee -o result.log check
tee -o result.out check
misc/scripts/check_assert.ys → misc/check/check_assert.ys
read_verilog -sv ../top.v
proc
tee -o result.log check -assert
tee -o result.out check -assert
misc/check/check_error_fail.pat 0 → 100644
ERROR: Found 1 problems in 'check -assert'.
misc/scripts/check_initdrv.ys → misc/check/check_error_fail.ys
read_verilog -sv ../top1.v
proc
tee -o result.log check -initdrv
check -assert
misc/scripts/check_noinit.ys → misc/check/check_initdrv.ys
read_verilog -sv ../top1.v
proc
tee -o result.log check -noinit
tee -o result.out check -initdrv
misc/check/check_logic_loop.ys 0 → 100644
read_verilog -sv ../top_logic_loop.v
proc
tee -o result.out check
misc/check/check_noinit.ys 0 → 100644
read_verilog -sv ../top1.v
proc
tee -o result.out check -noinit
misc/check/top_logic_loop.v 0 → 100644
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
misc/check_error/top.v deleted 100644 → 0
module top
( input d, clk, output reg q );
wire u;
wire s;
assign u = s;
assign u = d;
assign u = clk;
always @( posedge clk )
q <= u;
endmodule
misc/chformal/chformal_dff.ys 0 → 100644
read_verilog -sv ../top_dff.v
chformal -remove
tee -o result.log dump
misc/chformal/chformal_error_fail.pat 0 → 100644
ERROR: Mode option is missing.
misc/chformal/chformal_lat.ys 0 → 100644
read_verilog -sv ../top_lat.v
chformal -remove
tee -o result.log dump
misc/chformal/top.v
......@@ -21,7 +21,6 @@ module top
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
......@@ -36,8 +35,5 @@ always @(negedge x) begin
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/chformal_ff/top.v → misc/chformal/top_lat.v
......@@ -5,11 +5,7 @@ module alat
end
always @(*)
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if (en)
q <= d;
endmodule
......@@ -21,11 +17,7 @@ module alatn
end
always @(*)
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if (!en)
q <= d;
endmodule
......@@ -37,11 +29,7 @@ module latsr
end
always @(*)
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else if ( en )
......@@ -55,11 +43,7 @@ module nlatsr
end
always @(*)
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else if ( !en )
......
misc/chparam/chparam_error_fail.pat 0 → 100644
ERROR: The options -set and -list cannot be used together.
misc/chparam/chparam_list.ys 0 → 100644
read_verilog ../top.v
proc
chparam -set X 2 top
tee -o result.out chparam -list
misc/scripts/chparam_set.ys → misc/chparam/chparam_set.ys
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 top
tee -o result.out chparam -set X 2 top
misc/chparam/top.v
......@@ -10,16 +10,12 @@ module top
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
......
misc/chparam_error/top.v deleted 100644 → 0
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
misc/scripts/check_error.ys → misc/chtype/chtype.ys
read_verilog -sv ../top.v
proc
tee -o result.log check -assert
chtype
misc/scripts/chtype.ys → misc/chtype/chtype_map.ys
read_verilog -sv ../top.v
proc
tee -o result.log chtype
chtype -map $dff $adff $2
misc/scripts/chtype_map.ys → misc/chtype/chtype_selection.ys
read_verilog -sv ../top.v
proc
tee -o result.log chtype -map $dff $adff $2
chtype $2
misc/scripts/chtype_set.ys → misc/chtype/chtype_set.ys
read_verilog -sv ../top.v
proc
tee -o d.txt dump
tee -o result.log chtype -set $adff $2
tee -o d1.txt dump
misc/connect/connect_cannot_parse_set_lhs_expr_fail.pat 0 → 100644
ERROR: Failed to parse set lhs expression `sdf'.
misc/connect/connect_cannot_parse_set_rhs_expr_fail.pat 0 → 100644
ERROR: Failed to parse set rhs expression `sdf'.
misc/connect/connect_cant_find_cell_fail.pat 0 → 100644
ERROR: Can't find cell $procddff$2.
misc/connect/connect_failed_parse_unset_fail.pat 0 → 100644
ERROR: Failed to parse unset expression `sdf'.
misc/connect/connect_failed_to_parse_port_expr_fail.pat 0 → 100644
ERROR: Failed to parse port expression `dd'.
misc/connect/connect_found_process_fail.pat 0 → 100644
ERROR: Found processes in selected module.
misc/connect/connect_multiple_modules_fail.pat 0 → 100644
ERROR: Multiple modules selected: top2, top
misc/connect/connect_nomap_port.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -nomap -port $procdff$2 D d1
tee -o result.out dump
misc/connect/connect_nomap_set.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -nomap -set d1 q
tee -o result.out dump
misc/connect/connect_nomap_unset.pat 0 → 100644
wire $auto$connect.cc:33:unset_drivers$3
misc/connect/connect_nomap_unset.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -nomap -unset d q
tee -o result.out dump
misc/connect/connect_nounset_set.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -nounset -set d1 q
tee -o result.out dump
misc/connect/connect_opt_expected_fail.pat 0 → 100644
ERROR: Expected -set, -unset, or -port.
misc/connect/connect_port.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -port $procdff$2 D d1
tee -o result.out dump
misc/connect/connect_port_with_nounset_fail.pat 0 → 100644
ERROR: Can't use -port together with -nounset.
misc/connect/connect_set.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -set d1 q
tee -o result.out dump
misc/connect/connect_set_with_port_fail.pat 0 → 100644
ERROR: Can't use -set together with -unset and/or -port.
misc/connect/connect_set_with_unset_and_port_fail.pat 0 → 100644
ERROR: Can't use -set together with -unset and/or -port.
misc/connect/connect_set_with_unset_fail.pat 0 → 100644
ERROR: Can't use -set together with -unset and/or -port.
misc/connect/connect_unset.pat 0 → 100644
connect $auto$connect.cc:33:unset_drivers$4 \\q
misc/connect/connect_unset.ys 0 → 100644
read_verilog -sv ../top.v
proc
connect -set d1 q
connect -unset d1 q
tee -o result.out dump
misc/connect/connect_unset_with_nounset_and_port_fail.pat 0 → 100644
ERROR: Can't use -unset together with -port and/or -nounset.
misc/connect/connect_unset_with_nounset_fail.pat 0 → 100644
ERROR: Can't use -unset together with -port and/or -nounset.
misc/connect/connect_unset_with_port_fail.pat 0 → 100644
ERROR: Can't use -unset together with -port and/or -nounset.
misc/connect/top.v
module top
( input d, clk, output reg q );
( input d, d1, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
misc/scripts/connwrappers.ys → misc/connwrappers/connwrappers.ys
read_verilog ../top.v
proc
tee -o result.log connwrappers
connwrappers
misc/scripts/connwrappers_port.ys → misc/connwrappers/connwrappers_port.ys
read_verilog ../top.v
proc
tee -o result.log connwrappers -port $dff d 32000 1
connwrappers -port $dff d1 32000 1
misc/scripts/connwrappers_signed.ys → misc/connwrappers/connwrappers_signed.ys
read_verilog ../top.v
proc
tee -o result.log connwrappers -signed $dff d 3
connwrappers -signed $dff d 3
misc/scripts/connwrappers_unsigned.ys → misc/connwrappers/connwrappers_unsigned.ys
read_verilog ../top.v
proc
tee -o result.log connwrappers -unsigned $dff d 0
connwrappers -unsigned $dff d 0
misc/cover/cover_cant_create_file_fail.pat 0 → 100644
ERROR: Can't create file aa/out.txt.
misc/scripts/bugpoint_script.ys → misc/cover/cover_dir.ys
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys
tee -o result.log cover -d ../test
misc/cover/cover_dir_fail.pat 0 → 100644
ERROR: Can't create file in directory test.
misc/scripts/bugpoint_yosys.ys → misc/cover/cover_dir_fail.ys
read_verilog ../top.v
tee -o result.log bugpoint -script script.ys -yosys yosys.ys
tee -o result.log cover -d test
misc/cover/top.v
......@@ -8,10 +8,6 @@ module top
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/cutpoint/cutpoint_asserts.ys 0 → 100644
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
misc/cutpoint/top.v
......@@ -8,11 +8,8 @@ module bb
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
......
misc/chformal_error/top.v → misc/cutpoint/top_asserts.v
......@@ -21,7 +21,6 @@ module top
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
......@@ -36,8 +35,5 @@ always @(negedge x) begin
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/debug/top.v
......@@ -8,10 +8,6 @@ module top
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/scripts/delete_mem.ys → misc/delete/delete_mem.ys
read_verilog ../top.v
read_verilog ../top_mem.v
delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump
misc/delete/delete_memory.ys 0 → 100644
read_verilog ../top_mem.v
proc
memory
delete top/$memrd$\ram$../top.v:30$7
tee -o result.log dump
misc/delete_mem/top.v → misc/delete/top_mem.v
......@@ -7,38 +7,30 @@ module top
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
......@@ -48,5 +40,5 @@ module top
q_b <= ram[addr_b];
end
end
endmodule
endmodule
misc/scripts/design_as.ys → misc/design/design_as.ys
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-from first -as top_2 top
tee -o result.log design -copy-to first -as top_2 top
design -copy-from first -as top_2 top
design -copy-to first -as top_2 top
misc/scripts/design_copy_to.ys → misc/design/design_copy_from.ys
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-to first top
design -reset
design -copy-from first top
misc/scripts/design_import.ys → misc/design/design_copy_to.ys
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -import first top
design -reset
design -copy-to first top
misc/scripts/design_copy_from.ys → misc/design/design_import.ys
read_verilog -sv ../top.v
proc
design -save first
tee -o result.log design -copy-from first top
design -import first top
misc/scripts/chtype_selection.ys → misc/design/design_no_pushed_design_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log chtype $2
design -pop
misc/design/design_no_saved_design_copy_from_fail.pat 0 → 100644
ERROR: No saved design 'first' found!
misc/scripts/connect_nomap_port.ys → misc/design/design_no_saved_design_copy_from_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -port $procdff$2 D d
design -copy-from first -as top_2 top
misc/design/design_no_saved_design_import_fail.pat 0 → 100644
ERROR: No saved design 'first' found!
misc/scripts/connect_nomap_set.ys → misc/design/design_no_saved_design_import_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -set d q
design -import first top
misc/design/design_no_saved_design_load_fail.pat 0 → 100644
ERROR: No saved design 'first' found!
misc/design/design_no_top_module_fail.pat 0 → 100644
ERROR: No top module found in source design.
misc/design/design_no_top_module_fail.ys 0 → 100644
read_verilog -sv ../top.v
design -save first
design -import first
misc/design/top.v
......@@ -10,17 +10,12 @@ module top
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
......
misc/edgetypes/edgetypes.pat 0 → 100644
$_DFF_P_.Q $_XOR_.A
$_XOR_.Y $_DFF_N_.D
$_XOR_.Y $_DFF_P_.D
misc/edgetypes/edgetypes.ys 0 → 100644
read_verilog ../top.v
synth
tee -o result.out edgetypes
misc/edgetypes/edgetypes_fulladder.pat 0 → 100644
$_ANDNOT_.Y $_OR_.A
$_AND_.Y $_OR_.B
$_XNOR_.Y $_ANDNOT_.B
$_XNOR_.Y $_XNOR_.A
misc/edgetypes/edgetypes_fulladder.ys 0 → 100644
read_verilog ../top_fulladder.v
edgetypes
synth
tee -o result.out edgetypes
misc/edgetypes/top.v
......@@ -4,14 +4,22 @@ module top
input y,
input cin,
output A,
output cout
output reg A,
output reg cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
initial begin
begin
A = 0;
cout = 0;
end
end
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
endmodule
misc/scripts/chparam_list.ys → misc/eval/eval.ys
read_verilog ../top.v
proc
tee -o result.log chparam -set X 2 top
tee -o result.log chparam -list
tee -o result.log eval middle
misc/eval/eval_brute_force_equiv_checker.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker_x top top
misc/eval/eval_cant_find_input_fail.pat 0 → 100644
ERROR: Can't find input s in module middle!
misc/eval/eval_cant_find_input_fail.ys 0 → 100644
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle s 1
misc/eval/eval_cant_find_mod_1_fail.pat 0 → 100644
ERROR: Can't find module `\\u'!
misc/eval/eval_cant_find_mod_1_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u top
misc/eval/eval_cant_find_mod_2_fail.pat 0 → 100644
ERROR: Can't find module `\\u'!
misc/eval/eval_cant_find_mod_2_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u
misc/eval/eval_cant_find_mod_in_curr_des_fail.pat 0 → 100644
ERROR: Can't find module dle in current design!
misc/scripts/cover_dir.ys → misc/eval/eval_cant_find_mod_in_curr_des_fail.ys
read_verilog ../top.v
tee -o result.log cover -d out_dir
tee -o result.log eval -vloghammer_report middle dle x 1
misc/eval/eval_diff_lhs_rhs_sizes_fail.pat 0 → 100644
ERROR: Set expression with different lhs and rhs sizes:
misc/eval/eval_diff_lhs_rhs_sizes_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 2'b11 u_rtl
misc/eval/eval_empty_selection_fail.pat 0 → 100644
ERROR: Can't perform EVAL on an empty selection!
misc/eval/eval_empty_selection_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval u
misc/eval/eval_failed_to_parse_lhs_fail.pat 0 → 100644
ERROR: Failed to parse lhs set expression `u'.
misc/eval/eval_failed_to_parse_lhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set u 0 middle
misc/eval/eval_failed_to_parse_pattern_fail.pat 0 → 100644
ERROR: Failed to parse pattern d!
misc/eval/eval_failed_to_parse_pattern_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle x d
misc/eval/eval_failed_to_parse_rhs_fail.pat 0 → 100644
ERROR: Failed to parse rhs set expression `u'.
misc/eval/eval_failed_to_parse_rhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
misc/eval/eval_failed_to_parse_show_expr_fail.pat 0 → 100644
ERROR: Failed to parse show expression `u'.
misc/eval/eval_failed_to_parse_show_expr_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
misc/eval/eval_failed_to_parse_table_expr_fail.pat 0 → 100644
ERROR: Failed to parse table expression `u'.
misc/eval/eval_failed_to_parse_table_expr_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
misc/eval/eval_has_no_counterpart_fail.pat 0 → 100644
ERROR: Port \\cout in module 1 has no counterpart in module 2!
misc/eval/eval_has_no_counterpart_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
misc/eval/eval_mods_arent_equiv_fail.pat 0 → 100644
ERROR: Modules are not equivalent!
misc/eval/eval_mods_arent_equiv_fail.ys 0 → 100644
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
misc/eval/eval_no_output_wire_fail.pat 0 → 100644
ERROR: No output wire (y) found in module middle!
misc/eval/eval_no_output_wire_fail.ys 0 → 100644
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
misc/eval/eval_only_one_module_fail.pat 0 → 100644
ERROR: Only one module must be selected for the EVAL pass! (selected: u_rtl and middle)
misc/eval/eval_only_one_module_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval
misc/eval/eval_pattern_is_to_short_fail.pat 0 → 100644
ERROR: Pattern 1'b1 is to short!
misc/eval/eval_pattern_is_to_short_fail.ys 0 → 100644
read_verilog ../top_err_2.v
tee -o result.log eval -vloghammer_report mid dle x 1'b1
misc/eval/eval_port_doesnt_match_fail.pat 0 → 100644
ERROR: Port \\o in module 1 does not match its counterpart in module 2!
misc/eval/eval_port_doesnt_match_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
misc/eval/eval_rhs_expr_fail.pat 0 → 100644
ERROR: Right-hand-side set expression `x' is not constant.
misc/eval/eval_rhs_expr_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
misc/eval/eval_set.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 middle
misc/eval/eval_set_undef.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set-undef middle
misc/eval/eval_show.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 -show o middle
misc/eval/eval_show_not_set.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -show o middle
misc/eval/eval_table.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -table o middle
misc/eval/eval_table_set.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -set-undef -table o middle
misc/eval/eval_two_distinct_solutions_fail.pat 0 → 100644
ERROR: Found two distinct solutions to SAT problem.
misc/eval/eval_two_distinct_solutions_fail.ys 0 → 100644
read_verilog ../top_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
misc/eval/eval_vloghammer_report.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report mid dle x 1
misc/eval/eval_vloghammer_report_rtl.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report u_ rtl y 1
misc/eval/eval_wire_isnt_an_input_fail.pat 0 → 100644
ERROR: Wire w in module middle is not an input!
misc/eval/eval_wire_isnt_an_input_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle w 1
misc/eval/top.v
......@@ -31,6 +31,8 @@ module middle
output o
);
wire w;
assign o = x + y;
endmodule
......
misc/eval_error/top_err_3.v deleted 100644 → 0
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
misc/fmcombine/fmcombine.ys 0 → 100644
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
misc/fmcombine/fmcombine_anyeq.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
misc/fmcombine/fmcombine_anyeq_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
misc/fmcombine/fmcombine_anyeq_bwd.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq -bwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_assert_assume.ys 0 → 100644
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
misc/fmcombine/fmcombine_bwd.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
misc/fmcombine/fmcombine_bwd_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_bwd_fwd.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_bwd_fwd_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_dff.ys 0 → 100644
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
misc/fmcombine/fmcombine_dff_bwd.ys 0 → 100644
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
misc/fmcombine/fmcombine_fwd.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
misc/fmcombine/fmcombine_fwd_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_gate_cell_not_found_fail.pat 0 → 100644
ERROR: Gate cell u_mid8 not found in module top.
misc/scripts/connect_nomap_unset.ys → misc/fmcombine/fmcombine_gate_cell_not_found_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -nomap -unset d q
tee -o result.log fmcombine top u_mid1 u_mid8
misc/fmcombine/fmcombine_gold_cell_not_found_fail.pat 0 → 100644
ERROR: Gold cell u_mid8 not found in module top.
misc/scripts/connect_nounset_set.ys → misc/fmcombine/fmcombine_gold_cell_not_found_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -nounset -set d q
tee -o result.log fmcombine top u_mid8 u_mid3
misc/fmcombine/fmcombine_initeq.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
misc/fmcombine/fmcombine_initeq_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
misc/scripts/connect_port.ys → misc/fmcombine/fmcombine_invalid_number_of_param_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -port $procdff$2 D d
tee -o result.log fmcombine
misc/scripts/connect_set.ys → misc/fmcombine/fmcombine_module_not_found_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -set d q
tee -o result.log fmcombine topp u_mid1 u_mid3
misc/fmcombine/fmcombine_nop.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
select -assert-count 1 t:$fmcombine\middle
misc/fmcombine/fmcombine_nop_assert_assume.ys 0 → 100644
read_verilog -sv ../top_assert_assume.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
misc/fmcombine/fmcombine_nop_with_bwd_fail.pat 0 → 100644
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
misc/fmcombine/fmcombine_nop_with_bwd_fail.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -bwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_nop_with_fwd_bwd_fail.pat 0 → 100644
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
misc/fmcombine/fmcombine_nop_with_fwd_bwd_fail.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd -bwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_nop_with_fwd_fail.pat 0 → 100644
ERROR: Option -nop can not be combined with -fwd and/or -bwd.
misc/fmcombine/fmcombine_nop_with_fwd_fail.ys 0 → 100644
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd top u_mid1 u_mid2
misc/fmcombine/fmcombine_types_not_match_fail.pat 0 → 100644
ERROR: Types of gold and gate cells do not match.
misc/fmcombine/fmcombine_types_not_match_fail.ys 0 → 100644
read_verilog -sv ../top_err_1.v
proc
tee -o result.log fmcombine top u_mid1 u_urtl
misc/fmcombine/top.v
......@@ -10,7 +10,6 @@ module top
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
......@@ -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_mid3 (.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
......
misc/fmcombine_assert_assume/top.v → misc/fmcombine/top_assert_assume.v
......@@ -10,7 +10,6 @@ module top
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
......@@ -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_mid3 (.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
......@@ -49,7 +45,6 @@ module middle
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
......@@ -64,8 +59,5 @@ always @(negedge x) begin
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/fmcombine_error/top.v → misc/fmcombine/top_dff.v
......@@ -10,38 +10,37 @@ module top
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
middle u_mid1 (.x(x),.o(o),.y(1'b0));
middle u_mid2 (.x(x),.o(o),.y(1'b1));
middle u_mid3 (.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
middle u_mid1 (.clk(cin),.x(x),.o(o),.y(1'b0));
middle u_mid2 (.clk(cin),.x(x),.o(o),.y(1'b1));
middle u_mid3 (.clk(cin),.x(x),.o(o),.y(1'bX));
middle u_mid4 (.clk(cin),.x(x),.o(o),.y(1'bX));
endmodule
module middle
(
input clk,
input x,
input y,
output o
);
urtl u_urtl (.x(x),.o(o),.y(y));
urtl u_urtl (.clk(clk),.x(x),.o(o),.y(y));
endmodule
module urtl
(
input clk,
input x,
input y,
output o
output reg o
);
assign o = x + y;
always @(posedge clk)
o <= x + y;
endmodule
misc/fmcombine_error/top_err_1.v → misc/fmcombine/top_err_1.v
......@@ -11,7 +11,6 @@ module top
parameter U = "string";
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
......@@ -24,9 +23,6 @@ middle u_mid4 (.x(x),.o(o),.y(1'bX));
urtl u_urtl (.x(x),.o(o),.y(y));
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
......
misc/freduce/freduce.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/freduce/freduce_dff.ys 0 → 100644
read_verilog ../top_dff.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/freduce/freduce_dump.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce -dump fred
misc/freduce/freduce_ffs.ys 0 → 100644
read_verilog ../top_ffs.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/freduce/freduce_ffs_inv.ys 0 → 100644
read_verilog ../top_ffs.v
proc
tee -o result.log freduce -inv
synth
tee -o result.log freduce -inv
misc/freduce/freduce_ffs_v.ys 0 → 100644
read_verilog ../top_ffs.v
proc
tee -o result.log freduce -v
synth
tee -o result.log freduce -vv
misc/freduce/freduce_inv.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce -inv
misc/freduce/freduce_logic_loop_fail.ys 0 → 100644
read_verilog ../top_err_1.v
tee -o result.log freduce
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/freduce/freduce_mem.ys 0 → 100644
read_verilog ../top_mem.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/freduce/freduce_mem_dump.ys 0 → 100644
read_verilog ../top_mem.v
proc
tee -o result.log freduce -dump dump_a
synth
tee -o result.log freduce -dump dump_b
misc/freduce/freduce_mem_inv.ys 0 → 100644
read_verilog ../top_mem.v
proc
tee -o result.log freduce -inv
synth
tee -o result.log freduce -inv
misc/freduce/freduce_mem_stop.ys 0 → 100644
read_verilog ../top_mem.v
proc
tee -o result.log freduce -stop 1
synth
tee -o result.log freduce -stop 3
misc/freduce/freduce_mem_v.ys 0 → 100644
read_verilog ../top_mem.v
proc
tee -o result.log freduce -v
synth
tee -o result.log freduce -vv
misc/freduce/freduce_stop.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce -stop 1
misc/freduce/freduce_v.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce -v
misc/freduce/freduce_vv.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log freduce -vv
misc/freduce_ffs/top.v → misc/freduce/top_ffs.v
......@@ -5,11 +5,7 @@ module adff
end
always @( posedge clk, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -21,11 +17,7 @@ module adffn
end
always @( posedge clk, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else
q <= d;
endmodule
......@@ -37,11 +29,7 @@ module dffe
end
always @( posedge clk )
if ( en )
`ifndef BUG
q <= d;
`else
q <= 1'b0;
`endif
endmodule
module dffsr
......@@ -51,11 +39,7 @@ module dffsr
end
always @( posedge clk, posedge pre, posedge clr )
if ( clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( pre )
q <= 1'b1;
else
......@@ -69,11 +53,7 @@ module ndffnsnr
end
always @( negedge clk, negedge pre, negedge clr )
if ( !clr )
`ifndef BUG
q <= 1'b0;
`else
q <= d;
`endif
else if ( !pre )
q <= 1'b1;
else
......@@ -95,7 +75,7 @@ dffsr u_dffsr (
.d (a ),
.q (b )
);
ndffnsnr u_ndffnsnr (
.clk (clk ),
.clr (clr),
......@@ -103,21 +83,21 @@ ndffnsnr u_ndffnsnr (
.d (a ),
.q (b1 )
);
adff u_adff (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b2 )
);
adffn u_adffn (
.clk (clk ),
.clr (clr),
.d (a ),
.q (b3 )
);
dffe u_dffe (
.clk (clk ),
.en (clr),
......
misc/freduce_dff/top.v deleted 100644 → 0
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
misc/freduce_error/top.v deleted 100644 → 0
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
misc/help/help.ys 0 → 100644
tee -q -o result.log help
misc/help/help_all.ys 0 → 100644
tee -q -o result.log help -all
misc/help/help_cells.ys 0 → 100644
tee -q -o result.log help -cells
misc/help/help_celltype.pat 0 → 100644
$dff (CLK, D, Q)
No help message for this cell type found.
Run 'help $dff+' to display the Verilog model for this cell type.
misc/help/help_celltype.ys 0 → 100644
tee -q -o result.out help $dff
misc/help/help_celltype_plus.pat 0 → 100644
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
misc/help/help_celltype_plus.ys 0 → 100644
tee -q -o result.out help $dff+
misc/help/help_command.pat 0 → 100644
read_verilog \[options\] \[filename\]
misc/help/help_command.ys 0 → 100644
tee -q -o result.out help read_verilog
misc/help/help_no_such_command.pat 0 → 100644
No such command or cell type: u
misc/help/help_no_such_command.ys 0 → 100644
tee -q -o result.out help u
misc/hilomap/hilomap.ys 0 → 100644
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
misc/hilomap/hilomap_hicell.ys 0 → 100644
read_verilog ../top.v
proc
hilomap -hicell VCC V
select -assert-count 4 t:VCC
select -assert-count 0 t:GND
misc/hilomap/hilomap_hicell_locell_singleton.ys 0 → 100644
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
misc/hilomap/hilomap_hicell_singleton.ys 0 → 100644
read_verilog ../top.v
proc
hilomap -hicell VCC V -singleton
select -assert-count 2 t:VCC
select -assert-count 0 t:GND
misc/hilomap/hilomap_locell.ys 0 → 100644
read_verilog ../top.v
proc
hilomap -locell GND G
select -assert-count 0 t:VCC
select -assert-count 6 t:GND
misc/hilomap/hilomap_locell_singleton.ys 0 → 100644
read_verilog ../top.v
proc
hilomap -locell GND G -singleton
select -assert-count 0 t:VCC
select -assert-count 2 t:GND
misc/hilomap/hilomap_singleton.ys 0 → 100644
read_verilog ../top.v
proc
hilomap -singleton
misc/hilomap/top.v
......@@ -17,26 +17,16 @@ output b,b2
dffsr u_dffsr (
.clk (clk ),
`ifndef BUG
.clr (1'b0),
.pre (1'b1),
`else
.clr (1'b1),
.pre (1'b0),
`endif
.d (a ),
.q (b )
);
dffsr u2_dffsr (
.clk (clk ),
`ifndef BUG
.clr (1'b0),
.pre (1'b1),
`else
.clr (1'b1),
.pre (1'b0),
`endif
.d (a ),
.q (b2 )
);
......
misc/history/history.ys 0 → 100644
read_verilog ../top.v
proc
synth
synth_xilinx
tee -o result.out history
misc/history/top.v
......@@ -8,10 +8,6 @@
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/insbuf/insbuf.ys 0 → 100644
read_verilog ../top.v
synth
insbuf
select -assert-count 1 t:$_BUF_
misc/insbuf/insbuf_cell.ys 0 → 100644
read_verilog ../top.v
synth
insbuf -buf $_NOT_ A Y
select -assert-count 1 t:$_NOT_
misc/insbuf/insbuf_unknown_arg.ys 0 → 100644
read_verilog ../top.v
synth
insbuf buf
misc/insbuf/insbuf_wide.ys 0 → 100644
read_verilog ../top_wide.v
synth
insbuf
select -assert-count 16 t:$_BUF_
misc/insbuf/testbench.v deleted 100644 → 0
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
misc/insbuf/top_wide.v 0 → 100644
module top (
out,
in
);
output [7:0] out;
input [7:0] in;
wire [7:0] o;
assign o = in;
assign out = o;
endmodule
misc/log/log.ys 0 → 100644
tee -o result.log log "OK"
misc/log/log_n.ys 0 → 100644
tee -o result.log log -n "OK"
misc/log/log_nolog.ys 0 → 100644
tee -o result.log log -nolog "OK"
misc/log/log_stderr.ys 0 → 100644
tee -o result.log log -stderr "OK"
misc/log/log_stdout.ys 0 → 100644
tee -o result.log log -stdout "OK"
misc/ltp/ltp.pat 0 → 100644
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)
misc/ltp/ltp.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out ltp
misc/ltp/ltp_loop.pat 0 → 100644
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)
misc/ltp/ltp_loop.ys 0 → 100644
read_verilog ../top_logic_loop.v
proc
tee -o result.out ltp
misc/ltp/ltp_noff.pat 0 → 100644
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)
misc/ltp/ltp_noff.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out ltp -noff
misc/ltp/ltp_noproc.pat 0 → 100644
Warning: Ignoring module top because it contains processes (run 'proc' command first).
misc/ltp/ltp_noproc.ys 0 → 100644
read_verilog ../top.v
tee -o result.out ltp
misc/ltp/top.v
......@@ -9,25 +9,9 @@ module top
);
wire o;
`ifndef BUG
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
misc/ltp/top_logic_loop.v 0 → 100644
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
misc/miter/miter_assert.ys 0 → 100644
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -make_outputs top
tee -o result.log miter -assert -make_outputs middle
misc/miter/miter_assert_assert.ys 0 → 100644
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
misc/miter/miter_assert_flatten.ys 0 → 100644
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -flatten top
tee -o result.log miter -assert -flatten middle
misc/miter/miter_cant_find_gate_module_fail.pat 0 → 100644
ERROR: Can't find gate module \\gate!
misc/scripts/connect_unset.ys → misc/miter/miter_cant_find_gate_module_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log connect -unset d q
tee -o result.log miter -equiv top gate top
misc/miter/miter_cant_find_gold_module_fail.pat 0 → 100644
ERROR: Can't find gold module \\gold!
misc/scripts/design_no_pushed_design.ys → misc/miter/miter_cant_find_gold_module_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log design -pop
tee -o result.log miter -equiv gold gate top
misc/scripts/design_no_saved_design_copy_from.ys → misc/miter/miter_cant_find_module_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log design -copy-from first -as top_2 top
tee -o result.log miter -assert t
misc/miter/miter_equiv.ys 0 → 100644
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
misc/miter/miter_equiv_ignore_gold_x.ys 0 → 100644
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
misc/miter/miter_equiv_outcmp.ys 0 → 100644
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
misc/scripts/design_no_saved_design_import.ys → misc/miter/miter_missing_mode_param_fail.ys
read_verilog -sv ../top.v
proc
tee -o result.log design -import first top
tee -o result.log miter
misc/miter/miter_no_match_in_gate_fail.pat 0 → 100644
ERROR: No matching port in gate module was found for \\y!
misc/miter/miter_no_match_in_gate_fail.ys 0 → 100644
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv middle u_rtl top1
misc/miter/miter_no_match_in_gold_fail.pat 0 → 100644
ERROR: No matching port in gold module was found for \\y!
misc/miter/miter_no_match_in_gold_fail.ys 0 → 100644
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv u_rtl middle top1
misc/miter/miter_there_is_already_a_module_fail.pat 0 → 100644
ERROR: There is already a module \\top!
misc/miter/miter_there_is_already_a_module_fail.ys 0 → 100644
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top middle top
misc/miter/top_equiv.v 0 → 100644
module dut(
input fast_clk, slow_clk,
input [3:0] waddr, raddr,
input [3:0] wdata,
input wen,
output [3:0] rdata
);
reg [3:0] mem[0:15];
reg [3:0] raddr_reg;
always @(posedge fast_clk) begin
if (wen)
mem[waddr] <= wdata;
end
always @(posedge slow_clk)
raddr_reg <= raddr;
assign rdata = mem[raddr_reg];
endmodule
misc/miter_assert/top.v deleted 100644 → 0
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
misc/miter_error/top.v deleted 100644 → 0
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
misc/mutate/mutate_all.ys 0 → 100644
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
misc/mutate/mutate_cnot0.ys 0 → 100644
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
misc/mutate/mutate_cnot1.ys 0 → 100644
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
misc/mutate/mutate_const0.ys 0 → 100644
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
misc/mutate/mutate_const1.ys 0 → 100644
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
misc/mutate/mutate_error_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -cell $add$../top.v:12$1 -port \Y -portbit 0 -ctrlbit 0 -module top
misc/mutate/mutate_inv.ys 0 → 100644
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
misc/mutate/mutate_list.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32
misc/mutate/mutate_list_cfg.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -cfg weight_cover 1
misc/mutate/mutate_list_ctrl.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -ctrl A 1 1
misc/mutate/mutate_list_none.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -none
misc/mutate/mutate_list_o.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -o o.txt
misc/mutate/mutate_list_s.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -s s.txt
help mutate
misc/mutate/mutate_list_seed.ys 0 → 100644
read_verilog ../top.v
tee -o result.log mutate -list 32 -seed 5
misc/mutate/mutate_mem.ys 0 → 100644
read_verilog ../top_mem.v
mutate -list 512 -o mutate.yss
script mutate.yss
misc/mutate/top.v
......@@ -8,11 +8,8 @@ module top
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/freduce_mem/top.v → misc/mutate/top_mem.v
......@@ -7,38 +7,30 @@ module top
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
if (we_a)
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
if (we_b)
begin
ram[addr_b] <= data_b;
q_b <= data_b;
......@@ -48,5 +40,5 @@ module top
q_b <= ram[addr_b];
end
end
endmodule
endmodule
misc/muxpack/muxpack.ys 0 → 100644
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
misc/muxpack/muxpack_reduce.ys 0 → 100644
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
misc/muxpack/top.v
......@@ -2,15 +2,9 @@ module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
`ifndef BUG
always @(*)
Y = (S)? B : A;
`else
always @(*)
Y = (~S)? B : A;
`endif
endmodule
module mux4 ( S, D, Y );
......@@ -71,11 +65,7 @@ always @*
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
`ifndef BUG
4 : Y = D[4];
`else
4 : Y = D[7];
`endif
5 : Y = D[5];
6 : Y = D[6];
7 : Y = D[7];
......
misc/muxpack/top_reduce.v 0 → 100644
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
misc/onehot/onehot.ys 0 → 100644
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot
tee -o result.out
misc/onehot/onehot_v.ys 0 → 100644
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot -v
misc/onehot/onehot_vv.ys 0 → 100644
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_1.ys 0 → 100644
read_verilog ../top_1.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_2.ys 0 → 100644
read_verilog ../top_2.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_3.ys 0 → 100644
read_verilog ../top_3.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_4.ys 0 → 100644
read_verilog ../top_4.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_5.ys 0 → 100644
read_verilog ../top_5.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_6.ys 0 → 100644
read_verilog ../top_6.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/onehot_vv_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot ignore
onehot -vv
misc/onehot/top_1.v 0 → 100644
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
misc/onehot/top_2.v 0 → 100644
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
misc/onehot/top_3.v 0 → 100644
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
misc/onehot/top_4.v 0 → 100644
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
misc/onehot/top_5.v 0 → 100644
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
misc/onehot/top_6.v 0 → 100644
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
misc/opt_rmdff_sat/opt_rmdff_sat.ys 0 → 100644
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_
misc/plugin/plugin.ys 0 → 100644
tee -o result.log plugin
misc/plugin/plugin_a.ys 0 → 100644
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
misc/plugin/plugin_error_fail.pat 0 → 100644
ERROR: Can't load module
misc/plugin/plugin_error_fail.ys 0 → 100644
read_verilog ../top.v
tee -o result.log plugin -l
plugin -i uu -a alias
tee -o result.log plugin -l
misc/plugin/plugin_i.ys 0 → 100644
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so
misc/plugin/plugin_l.ys 0 → 100644
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
misc/plugin_error/top.v deleted 100644 → 0
module top
( input d, clk, output reg q );
always @( posedge clk )
q <= d;
endmodule
misc/pmux2shiftx/pmux2shiftx.ys 0 → 100644
read_verilog ../top.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 1 t:$shiftx
misc/pmux2shiftx/pmux2shiftx_2.ys 0 → 100644
read_verilog ../top_2.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 1 t:$shiftx
misc/pmux2shiftx/pmux2shiftx_fsm.ys 0 → 100644
read_verilog ../top_fsm.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx
select -assert-count 2 t:$shiftx
misc/pmux2shiftx/pmux2shiftx_min_choices_0.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_choices 0
onehot
misc/pmux2shiftx/pmux2shiftx_min_choices_3000.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_choices 3000
misc/pmux2shiftx/pmux2shiftx_min_dens_0.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_density 0
onehot
misc/pmux2shiftx/pmux2shiftx_min_dens_3000.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -min_density 3000
misc/pmux2shiftx/pmux2shiftx_norange.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -norange
onehot
misc/pmux2shiftx/pmux2shiftx_onehot_ignore.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot ignore
onehot
misc/pmux2shiftx/pmux2shiftx_onehot_pmux.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot pmux
misc/pmux2shiftx/pmux2shiftx_onehot_shiftx.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -onehot shiftx
onehot
misc/pmux2shiftx/pmux2shiftx_top.ys 0 → 100644
read_verilog ../top.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx top
select -assert-count 1 t:$shiftx
misc/pmux2shiftx/pmux2shiftx_v.ys 0 → 100644
read_verilog ../top_fsm.v
proc
select -assert-count 0 t:$shiftx
pmux2shiftx -v
select -assert-count 2 t:$shiftx
misc/pmux2shiftx/pmux2shiftx_vv.ys 0 → 100644
read_verilog ../top_fsm.v
proc
pmux2shiftx -vv
misc/pmux2shiftx/top_fsm.v 0 → 100644
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
misc/pmuxtree/pmuxtree.ys 0 → 100644
read_verilog ../top.v
proc
pmuxtree
select -assert-none t:$pmuxtree
select -assert-count 3 t:$mux
misc/pmuxtree/pmuxtree_1.ys 0 → 100644
read_verilog ../top_1.v
proc
pmuxtree
select -assert-none t:$pmuxtree
select -assert-count 7 t:$mux
misc/pmuxtree/top_1.v 0 → 100644
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
misc/qwp/qwp.pat 0 → 100644
attribute \\qwp_position
misc/qwp/qwp.ys 0 → 100644
read_verilog ../top.v
proc
qwp
tee -o result.out dump
misc/qwp/qwp_alpha.pat 0 → 100644
attribute \\qwp_position
misc/qwp/qwp_alpha.ys 0 → 100644
read_verilog ../top.v
proc
qwp -alpha
tee -o result.out dump
misc/qwp/qwp_dump.pat 0 → 100644
attribute \\qwp_position
misc/qwp/qwp_dump.ys 0 → 100644
read_verilog ../top.v
proc
qwp -dump out.html
tee -o result.out dump
misc/qwp/qwp_grid.pat 0 → 100644
attribute \\qwp_position
misc/qwp/qwp_grid.ys 0 → 100644
read_verilog ../top.v
proc
qwp -grid 4
tee -o result.out dump
misc/qwp/qwp_ltr.pat 0 → 100644
attribute \\qwp_position
misc/qwp/qwp_ltr.ys 0 → 100644
read_verilog ../top.v
proc
qwp -ltr
tee -o result.out dump
misc/qwp/qwp_v.pat 0 → 100644
> 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
misc/qwp/qwp_v.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out qwp -v
misc/qwp/top.v
......@@ -9,16 +9,12 @@ module top
);
wire o;
`ifndef BUG
//always @(posedge cin)
// A <= o;
always @(posedge cin)
A <= o;
assign cout = cin? y : x;
//middle u_mid (x,y,o);
`else
assign {cout,A} = cin - y * x;
`endif
middle u_mid (x,y,o);
endmodule
......
misc/rename/rename.pat 0 → 100644
module \\mid_module
misc/rename/rename.ys 0 → 100644
read_verilog ../top.v
proc
rename middle mid_module
tee -o result.out dump
misc/rename/rename_enumerate.ys 0 → 100644
read_verilog ../top.v
proc
rename -enumerate middle mid_module
tee -o result.out dump
misc/rename/rename_enumerate_pat.ys 0 → 100644
read_verilog ../top.v
proc
rename -enumerate -pattern '_%_top' top
tee -o result.out dump
misc/rename/rename_hide.ys 0 → 100644
read_verilog ../top.v
proc
rename -hide middle mid
misc/rename/rename_invalid_number_of_args_fail.pat 0 → 100644
ERROR: Invalid number of arguments!
misc/rename/rename_invalid_number_of_args_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log rename
misc/rename/rename_invalid_number_of_args_top_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log rename -top
misc/rename/rename_low.ys 0 → 100644
read_verilog ../top.v
synth
rename low newlow
tee -o result.out dump
misc/rename/rename_mode_out_requires_fail.pat 0 → 100644
ERROR: Mode -output requires that there is an active module selected.
misc/rename/rename_mode_out_requires_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log rename -output u uu
misc/rename/rename_no_top_module_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log rename -top top
misc/rename/rename_obj_not_found_fail.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.log rename u uu
misc/rename/rename_src.pat 0 → 100644
cell $add \\../top.v:
misc/rename/rename_src.ys 0 → 100644
read_verilog ../top.v
proc
rename -src middle mid_module
tee -o result.out dump
misc/rename/rename_top.ys 0 → 100644
read_verilog ../top.v
synth -top top
rename -top new_top
tee -o result.out dump
misc/rename/rename_top_top.ys 0 → 100644
read_verilog ../top.v
synth -top top
rename top new_top
tee -o result.out dump
misc/rename/rename_wire.ys 0 → 100644
read_verilog ../top.v
proc
tee -o resulta.out dump
rename -wire top/o top/t_o
tee -o result.out dump
misc/rename/top.v
......@@ -9,16 +9,12 @@ module top
);
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
......
misc/rename_error/top.v deleted 100644 → 0
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
misc/rmports/rmports.ys 0 → 100644
read_verilog ../top.v
proc
rmports top middle
tee -o result.out dump
misc/rmports/top.v
module top
(
input x,
input y,
input x,
input z,
input cin,
output reg A,
......@@ -10,16 +11,10 @@ module top
parameter X = 1;
wire o;
`ifndef BUG
always @(posedge cin)
A <= o;
//assign cout = cin? y : x;
middle u_mid (.x(x),.o(o));
`else
assign {cout,A} = cin - y * x;
`endif
middle u_mid (.z(z),.x(x),.o(o));
endmodule
......@@ -27,6 +22,7 @@ module middle
(
input x,
input y,
input z,
output o
);
......
misc/run.sh deleted 100644 → 0
#!/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
misc/sat/sat.ys 0 → 100644
read_verilog ../top.v
proc
sat middle
misc/sat/sat_all.ys 0 → 100644
read_verilog ../top.v
proc
sat -ignore_unknown_cells -all top
misc/sat/sat_all_with_show.ys 0 → 100644
read_verilog -sv ../top_ff.v
synth
sat -ignore_unknown_cells -all -show q adff
misc/sat/sat_all_with_tempinduct.ys 0 → 100644
read_verilog ../top.v
#proc
sat -all -prove x 1 -tempinduct middle
misc/sat/sat_all_with_tempinduct_ff.ys 0 → 100644
read_verilog ../top_ff.v
synth
sat -ignore_unknown_cells -all -prove clr 1 -tempinduct adff
misc/sat/sat_all_with_tempinduct_setinit.disable 0 → 100644
read_verilog -sv ../top_ff.v
#proc
sat -ignore_unknown_cells -all -prove clr 1 -set-init s 1'b1 -tempinduct adff
misc/sat/sat_all_with_tempinduct_setinit.ys 0 → 100644
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
misc/sat/sat_all_with_tempinduct_setinit_fail.pat 0 → 100644
ERROR: Found -set-init bits that are not part of the initial_state: \\o
misc/sat/sat_all_with_tempinduct_setinit_fail.ys 0 → 100644
read_verilog ../top.v
#proc
sat -all -prove x 1 -set-init o 0 -tempinduct middle
misc/sat/sat_all_with_tempinduct_setinitdef.ys 0 → 100644
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-def -tempinduct-def middle
misc/sat/sat_all_with_tempinduct_setinitundef.ys 0 → 100644
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-undef -tempinduct-def middle
misc/sat/sat_all_with_tempinduct_setinitzero.ys 0 → 100644
read_verilog -sv ../top_initstate.v
#proc
sat -ignore_unknown_cells -all -prove x 1 -set-init-zero -tempinduct-def middle
misc/sat/sat_cant_open_json_file_fail.pat 0 → 100644
ERROR: Can't open output file `dir/out.json' for writing: No such file or directory
misc/sat/sat_cant_open_json_file_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_json dir/out.json middle
misc/sat/sat_cant_open_vcd_file_fail.pat 0 → 100644
ERROR: Can't open output file `dir/out.vcd' for writing: No such file or directory
misc/sat/sat_cant_open_vcd_file_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_vcd dir/out.vcd middle
misc/sat/sat_cant_perform_sat_on_empty_sel_fail.pat 0 → 100644
ERROR: Can't perform SAT on an empty selection!
misc/sat/sat_cnf_open_json_file_fail.pat 0 → 100644
ERROR: Can't open output file `dir/out.cnf' for writing: No such file or directory
misc/sat/sat_cnf_open_json_file_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_cnf dir/out.cnf middle
misc/sat/sat_dump_cnf.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_cnf cnf.cnf middle
misc/sat/sat_dump_json.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_json json.json middle
misc/sat/sat_dump_vcd.ys 0 → 100644
read_verilog ../top.v
proc
sat -dump_vcd vcd.vcd middle
misc/sat/sat_enable_undef.ys 0 → 100644
read_verilog ../top.v
proc
sat -enable_undef middle
misc/sat/sat_failed_to_import_cell_fail.pat 0 → 100644
ERROR: Failed to import cell inst_u_rtl (type u_rtl) to SAT database.
misc/sat/sat_failed_to_import_cell_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-skip 1 -prove x 1 -seq 2 top
misc/sat/sat_falsify.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -falsify middle
misc/sat/sat_falsify_fail.pat 0 → 100644
ERROR: Called with -falsify and found a model!
misc/sat/sat_falsify_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -falsify middle
misc/sat/sat_falsify_no_timeout.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -falsify-no-timeout middle
misc/sat/sat_fsm_dump_cnf.ys 0 → 100644
read_verilog ../top_fsm.v
proc
sat -dump_cnf cnf.cnf -ignore_unknown_cells fsm
misc/sat/sat_fsm_dump_json.ys 0 → 100644
read_verilog ../top_fsm.v
proc
sat -dump_json json.json -ignore_unknown_cells fsm
misc/sat/sat_fsm_dump_vcd.ys 0 → 100644
read_verilog ../top_fsm.v
proc
sat -dump_vcd vcd.vcd -ignore_unknown_cells fsm
misc/sat/sat_got_tempinduct_but_nothing_to_prove_fail.pat 0 → 100644
ERROR: Got -tempinduct but nothing to prove!
misc/sat/sat_got_tempinduct_but_nothing_to_prove_fail.ys 0 → 100644
read_verilog ../top.v
sat -tempinduct middle
misc/sat/sat_ignore_div_by_zero.ys 0 → 100644
read_verilog ../top_div_by_zery.v
proc
sat -ignore_div_by_zero middle
misc/sat/sat_ignore_unknown_cells.pat 0 → 100644
Warning: Failed to import cell
misc/sat/sat_ignore_unknown_cells.ys 0 → 100644
read_verilog ../top_fsm.v
proc
tee -o result.out sat -ignore_unknown_cells fsm
misc/sat/sat_initsteps.pat 0 → 100644
Skipping prove for this step (-initsteps 1).
misc/scripts/eval.ys → misc/sat/sat_initsteps.ys
read_verilog ../top.v
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
misc/sat/sat_max.ys 0 → 100644
read_verilog ../top.v
proc
sat -max 3 middle
misc/sat/sat_max_all_with_tempinduct.ys 0 → 100644
read_verilog ../top.v
proc
sat -max 5 -all -prove x 1 -tempinduct middle
misc/sat/sat_max_max_undef_with_tempinduct_fail.pat 0 → 100644
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
misc/sat/sat_max_max_undef_with_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -max_undef -all -prove x 1 -tempinduct top
misc/sat/sat_max_maxundef_all_with_tempinduct_fail.pat 0 → 100644
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
misc/sat/sat_max_maxundef_all_with_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -max 1 -max_undef -all -prove x 1 -tempinduct top
misc/sat/sat_max_maxundef_with_tempinduct_fail.pat 0 → 100644
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
misc/sat/sat_max_maxundef_with_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -max 1 -max_undef -prove x 1 -tempinduct top
misc/sat/sat_max_undef.ys 0 → 100644
read_verilog ../top.v
proc
sat -max_undef middle
misc/sat/sat_max_with_tempinduct_fail.pat 0 → 100644
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
misc/sat/sat_max_with_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -max 1 -prove x 1 -tempinduct top
misc/sat/sat_maxsteps.ys 0 → 100644
read_verilog ../top.v
proc
sat -maxsteps 0 middle
misc/sat/sat_maxsteps_only_for_tempinduct_fail.pat 0 → 100644
ERROR: The options -maxsteps is only supported for temporal induction proofs!
misc/sat/sat_maxsteps_only_for_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -maxsteps 3 middle
misc/sat/sat_maxundef_with_tempinduct_fail.pat 0 → 100644
ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!
misc/sat/sat_maxundef_with_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -max_undef -prove x 1 -tempinduct top
misc/sat/sat_mux.ys 0 → 100644
read_verilog ../top_mux.v
proc
sat mux16
misc/sat/sat_only_one_module_must_be_sel_fail.pat 0 → 100644
ERROR: Only one module must be selected for the SAT pass! (selected: u_rtl and middle)
misc/sat/sat_prove.ys 0 → 100644
read_verilog ../top.v
proc
sat -ignore_unknown_cells -prove x 1 top
misc/sat/sat_prove_and_tempinduct_fail.pat 0 → 100644
ERROR: Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip.
misc/sat/sat_prove_and_tempinduct_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-skip 365 -prove x 1 -tempinduct top
misc/sat/sat_prove_asserts.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-asserts middle
misc/sat/sat_prove_diff_size_fail.pat 0 → 100644
ERROR: Proof expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
misc/sat/sat_prove_diff_size_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 2'b11 middle
misc/sat/sat_prove_lhs_fail.pat 0 → 100644
ERROR: Failed to parse lhs proof expression `X'.
misc/sat/sat_prove_lhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove X 0 middle
misc/sat/sat_prove_rhs_fail.pat 0 → 100644
ERROR: Failed to parse rhs proof expression `X'.
misc/sat/sat_prove_rhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x X middle
misc/sat/sat_prove_skip.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-skip 1 -seq 2 middle
misc/sat/sat_prove_skip_must_be_smaller_than_seq_fail.pat 0 → 100644
ERROR: The value of -prove-skip must be smaller than the one of -seq.
misc/sat/sat_prove_skip_must_be_smaller_than_seq_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-skip 365 -prove x 1 -seq 1 top
misc/sat/sat_prove_x.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-x x 1 middle
misc/sat/sat_provex_diff_size_fail.pat 0 → 100644
ERROR: Proof-x expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
misc/sat/sat_provex_diff_size_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-x x 2'b11 middle
misc/sat/sat_provex_lhs_fail.pat 0 → 100644
ERROR: Failed to parse lhs proof-x expression `X'.
misc/sat/sat_provex_lhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-x X 0 middle
misc/sat/sat_provex_rhs_fail.pat 0 → 100644
ERROR: Failed to parse rhs proof-x expression `X'.
misc/sat/sat_provex_rhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove-x x X middle
misc/sat/sat_seq.ys 0 → 100644
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
misc/sat/sat_set.pat 0 → 100644
Import set-constraint: \\x = 1'1
misc/sat/sat_set.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -set x 3 middle
misc/sat/sat_set_all_undef.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-all-undef x middle
misc/sat/sat_set_all_undef_at.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-all-undef-at 1 x -tempinduct middle
misc/sat/sat_set_all_undef_fail.pat 0 → 100644
ERROR: Failed to parse set-def expression `U'.
misc/sat/sat_set_all_undef_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-all-undef U middle
misc/sat/sat_set_any_undef.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-any-undef x middle
misc/sat/sat_set_any_undef_at.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-any-undef-at 1 x -tempinduct middle
misc/sat/sat_set_assumes.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-assumes middle
misc/sat/sat_set_at.pat 0 → 100644
Import set-constraint for this timestep: \\o = 1'1
misc/sat/sat_set_at.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-at 1 o 3 -tempinduct middle
misc/sat/sat_set_def.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-def x middle
misc/sat/sat_set_def_at.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -set-def-at 3 x -tempinduct middle
misc/sat/sat_set_def_fail.pat 0 → 100644
ERROR: Failed to parse set-def expression `U'.
misc/sat/sat_set_def_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-def U middle
misc/sat/sat_set_def_inputs.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-def-inputs middle
misc/sat/sat_set_diff_size_fail.pat 0 → 100644
ERROR: Set expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)
misc/sat/sat_set_diff_size_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set x 2'b11 middle
misc/sat/sat_set_init.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init x 0 middle
misc/sat/sat_set_init_def.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-def middle
misc/sat/sat_set_init_undef.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-undef middle
misc/sat/sat_set_init_zero.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-zero middle
misc/sat/sat_set_lhs_fail.pat 0 → 100644
ERROR: Failed to parse lhs set expression
misc/sat/sat_set_lhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set X 0 middle
misc/sat/sat_set_rhs_fail.pat 0 → 100644
ERROR: Failed to parse rhs set expression
misc/sat/sat_set_rhs_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set x X middle
misc/sat/sat_show.ys 0 → 100644
read_verilog ../top.v
proc
sat -show x middle
misc/sat/sat_show_all.ys 0 → 100644
read_verilog ../top.v
proc
sat -show-all middle
misc/sat/sat_show_fail.pat 0 → 100644
ERROR: Failed to parse show expression `X'.
misc/sat/sat_show_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -show X middle
misc/sat/sat_show_inputs.ys 0 → 100644
read_verilog ../top.v
proc
sat -show-inputs middle
misc/sat/sat_show_outputs.ys 0 → 100644
read_verilog ../top.v
proc
sat -show-outputs middle
misc/sat/sat_show_ports.ys 0 → 100644
read_verilog ../top.v
proc
sat -show-ports middle
misc/sat/sat_show_public.ys 0 → 100644
read_verilog ../top.v
proc
sat -show-public middle
misc/sat/sat_show_regs.ys 0 → 100644
read_verilog ../top.v
proc
sat -ignore_unknown_cells -show-regs top
misc/sat/sat_si_def_undef_fail.pat 0 → 100644
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
misc/sat/sat_si_def_undef_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-undef -set-init-def middle
misc/sat/sat_si_def_undef_zero_fail.pat 0 → 100644
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
misc/sat/sat_si_def_undef_zero_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-undef -set-init-def -set-init-zero middle
misc/sat/sat_si_def_zero_fail.pat 0 → 100644
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
misc/sat/sat_si_def_zero_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-def -set-init-zero middle
misc/sat/sat_si_undef_zero_fail.pat 0 → 100644
ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!
misc/sat/sat_si_undef_zero_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -set-init-undef -set-init-zero middle
misc/sat/sat_stepsize.pat 0 → 100644
Skipping prove for this step (-stepsize 2)
misc/sat/sat_stepsize.ys 0 → 100644
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
misc/sat/sat_tempinduct.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct middle
misc/sat/sat_tempinduct_baseonly.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly middle
misc/sat/sat_tempinduct_baseonly_dump_cnf.ys 0 → 100644
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
misc/sat/sat_tempinduct_baseonly_dump_vcd.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 6 -dump_vcd vcd.vcd middle
misc/sat/sat_tempinduct_baseonly_maxsteps.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 1 middle
misc/sat/sat_tempinduct_baseonly_maxsteps_6.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-baseonly -maxsteps 6 middle
misc/sat/sat_tempinduct_def.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-def middle
misc/scripts/eval_brute_force_equiv_checker.ys → misc/sat/sat_tempinduct_dump_cnf.ys
read_verilog ../top.v
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
misc/sat/sat_tempinduct_inductonly.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct-inductonly middle
misc/sat/sat_tempinduct_skip.pat 0 → 100644
Skipping prove for this step (-tempinduct-skip 1)
misc/sat/sat_tempinduct_skip.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -tempinduct-skip 1 -prove x 0 -set-def-at 3 x -tempinduct middle
misc/sat/sat_tempinduct_tempinduct_baseonly.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct -tempinduct-baseonly middle
misc/sat/sat_tempinduct_tempinduct_def.ys 0 → 100644
read_verilog ../top.v
proc
sat -prove x 1 -tempinduct -tempinduct-def middle
misc/sat/sat_timeout.ys 0 → 100644
read_verilog ../top.v
proc
sat -timeout 0 -ignore_unknown_cells top
misc/sat/sat_timeout_verify.ys 0 → 100644
read_verilog ../top.v
proc
sat -timeout 1 -verify -ignore_unknown_cells top
misc/sat/sat_unset_at.pat 0 → 100644
Import unset-constraint for this timestep: \\o
misc/sat/sat_unset_at.ys 0 → 100644
read_verilog ../top.v
proc
tee -o result.out sat -prove x 0 -unset-at 1 o -tempinduct middle
misc/sat/sat_verify.ys 0 → 100644
read_verilog ../top.v
proc
sat -verify -ignore_unknown_cells -show x,y -set x y -set x 1 top
misc/sat/sat_verify_fail.pat 0 → 100644
ERROR: Called with -verify and proof did fail!
misc/sat/sat_verify_fail.ys 0 → 100644
read_verilog ../top.v
proc
sat -verify -prove x 1 -tempinduct middle
misc/sat/sat_verify_no_timeout.ys 0 → 100644
read_verilog ../top.v
proc
sat -verify-no-timeout -ignore_unknown_cells -show x,y -set x y -set x 1 top
misc/sat/top.v
......@@ -3,19 +3,17 @@ module top
input x,
input y,
input cin,
(* init = 1'h0 *)
output reg A,
output cout
);
parameter X = 1;
wire o;
initial A = 0;
initial cout = 0;
`ifndef BUG
always @(posedge cin)
A <= o;
......@@ -23,9 +21,6 @@ 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
......@@ -46,5 +41,7 @@ module u_rtl
output o
);
initial o = 0;
assign o = x + y;
endmodule
misc/sat_error/top.v → misc/sat/top_div_by_zery.v
......@@ -3,19 +3,17 @@ module top
input x,
input y,
input cin,
(* init = 1'h0 *)
output reg A,
output cout
);
parameter X = 1;
wire o;
initial A = 0;
initial cout = 0;
`ifndef BUG
always @(posedge cin)
A <= o;
......@@ -23,9 +21,6 @@ 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
......@@ -46,5 +41,7 @@ module u_rtl
output o
);
assign o = x + y;
initial o = 0;
assign o = x / 0;
endmodule
misc/sat/top_ff.v 0 → 100644
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
misc/sat/top_fsm.v 0 → 100644
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
misc/sat/top_initstate.v 0 → 100644
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
misc/sat/top_mux.v 0 → 100644
module mux2 (S,A,B,Y);
input S;
input A,B;
output reg Y;
always @(*)
Y = (S)? B : A;
endmodule
module mux4 ( S, D, Y );
input[1:0] S;
input[3:0] D;
output Y;
reg Y;
wire[1:0] S;
wire[3:0] D;
always @*
begin
case( S )
0 : Y = D[0];
1 : Y = D[1];
2 : Y = D[2];
3 : Y = D[3];
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
misc/sat/top_reg.v 0 → 100644
module dut(
input fast_clk, slow_clk,
input [3:0] waddr, raddr,
input [3:0] wdata,
input wen,
output [3:0] rdata
);
reg [3:0] mem[0:15];
reg [3:0] raddr_reg;
always @(posedge fast_clk) begin
if (wen)
mem[waddr] <= wdata;
end
always @(posedge slow_clk)
raddr_reg <= raddr;
assign rdata = mem[raddr_reg];
endmodule
misc/scatter/scatter.pat 0 → 100644
wire $auto$scatter
misc/scatter/scatter.ys 0 → 100644
read_verilog ../top.v
proc
scatter
tee -o result.out dump
misc/scatter/top.v
......@@ -9,16 +9,12 @@ module top
);
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
......
misc/scc/scc.pat 0 → 100644
Found 1 SCCs in module top.
misc/scc/scc.ys 0 → 100644
read_verilog ../top.v
scc top
proc
scc top
synth
tee -o result.out scc top
misc/scc/scc_all_cell_types.ys 0 → 100644
read_verilog ../top.v
proc
scc -all_cell_types top
misc/scc/scc_expect.pat 0 → 100644
Found and expected 0 SCCs.
misc/scc/scc_expect.ys 0 → 100644
read_verilog ../top_no_feedback.v
proc
tee -o result.out scc -expect 0 top
misc/scc/scc_expect_fail.pat 0 → 100644
ERROR: Found 1 SCCs but expected 0.
misc/scc/scc_expect_fail.ys 0 → 100644
read_verilog ../top.v
proc
scc -expect 0 top
misc/scc/scc_hier_feedback.ys 0 → 100644
read_verilog ../top_hier_feedback.v
scc top
proc
scc top
synth
scc top
misc/scc/scc_max_depth.ys 0 → 100644
read_verilog ../top.v
proc
scc -max_depth 2 top
misc/scc/scc_no_feedback.ys 0 → 100644
read_verilog ../top_no_feedback.v
scc top
proc
scc top
synth
scc top
misc/scc/scc_nofeedback.ys 0 → 100644
read_verilog ../top.v
proc
scc -nofeedback top
misc/scripts/abc_g_cmos.ys → misc/scc/scc_select.ys
read_verilog ../top.v
synth -top top
tee -o result.log abc -g cmos
scc -select top
misc/scc/scc_set_attr.ys 0 → 100644
read_verilog ../top.v
proc
scc -set_attr attr true top
misc/scc/top.v
......@@ -7,27 +7,13 @@ module top
output reg A,
output cout
);
wire o;
parameter X = 1;
wire o_mid,o_rtl;
`ifndef BUG
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
misc/help/top.v → misc/scc/top_no_feedback.v
......@@ -9,16 +9,12 @@ module top
);
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
......
misc/scc_error/top.v deleted 100644 → 0
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
misc/script/script_from_to.ys 0 → 100644
tee -o result.log script ../script.ys 1:3
misc/script/script_no_opt.ys 0 → 100644
tee -o result.log script ../script.ys
misc/script/script_scriptwire.ys 0 → 100644
tee -o result.log script -scriptwire ../script.ys
misc/script/top.v
......@@ -8,10 +8,6 @@
output cout
);
`ifndef BUG
assign {cout,A} = cin + y + x;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
misc/scripts/abc9_box.ys deleted 100644 → 0
tee -o result.log abc9 -box box.txt -lut 2
misc/scripts/abc9_script.ys deleted 100644 → 0
tee -o result.log abc9 -script box.txt -lut 2
misc/scripts/bugpoint_grep.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log bugpoint -script ../script.ys -grep "Simplifications exhausted"
misc/scripts/design_no_top_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
design -save first
tee -o result.log design -import first
misc/scripts/echo.ys deleted 100644 → 0
tee -q -o result.log echo
misc/scripts/echo_off.ys deleted 100644 → 0
tee -q -o result.log echo off
misc/scripts/echo_on.ys deleted 100644 → 0
tee -q -o result.log echo on
misc/scripts/edgetypes.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log edgetypes
misc/scripts/eval_cant_find_input.ys deleted 100644 → 0
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle s 1
misc/scripts/eval_cant_find_mod_1.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u top
misc/scripts/eval_cant_find_mod_2.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u
misc/scripts/eval_cant_find_mod_in_curr_des.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log eval -vloghammer_report middle dle x 1
misc/scripts/eval_cant_find_mod_in_curr_dess.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report mid dle x 1
misc/scripts/eval_diff_lhs_rhs_sizes.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 2'b11 u_rtl
misc/scripts/eval_empty_selection.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval u
misc/scripts/eval_failed_to_parse_lhs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set u 0 middle
misc/scripts/eval_failed_to_parse_pattern.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle x d
misc/scripts/eval_failed_to_parse_rhs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set x u middle
misc/scripts/eval_failed_to_parse_show_expr.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -show u middle
misc/scripts/eval_failed_to_parse_table_expr.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -table u middle
misc/scripts/eval_has_no_counterpart.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker top u_rtl
misc/scripts/eval_mods_arent_equiv.ys deleted 100644 → 0
read_verilog ../top_err_1.v
proc
tee -o result.log eval -brute_force_equiv_checker middle u_rtl
misc/scripts/eval_no_output_wire.ys deleted 100644 → 0
read_verilog ../top_err_1.v
tee -o result.log eval -vloghammer_report mid dle x 1
misc/scripts/eval_only_one_module.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval
misc/scripts/eval_pattern_is_to_short.ys deleted 100644 → 0
read_verilog ../top_err_2.v
tee -o result.log eval -vloghammer_report mid dle x 1'b1
misc/scripts/eval_port_doesnt_match.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -brute_force_equiv_checker u_rtl top
misc/scripts/eval_rhs_expr.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y x u_rtl
misc/scripts/eval_set.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 middle
misc/scripts/eval_set_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set-undef middle
misc/scripts/eval_show.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set x 1 -set y 0 -show o middle
misc/scripts/eval_show_not_set.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -show o middle
misc/scripts/eval_table.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -table o middle
misc/scripts/eval_table_set.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -set-undef -table o middle
misc/scripts/eval_two_distinct_solutions.ys deleted 100644 → 0
read_verilog ../top_err_3.v
tee -o result.log eval -vloghammer_report u_ rtl x 1'b1
misc/scripts/eval_vloghammer_report.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report mid dle x 1
misc/scripts/eval_vloghammer_report_rtl.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log eval -vloghammer_report u_ rtl y 1
misc/scripts/eval_wire_isnt_an_input.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log eval -vloghammer_report mid dle w 1
misc/scripts/fmcombine.ys deleted 100644 → 0
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
misc/scripts/fmcombine_anyeq.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -anyeq top u_mid1 u_mid2
misc/scripts/fmcombine_bwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd top u_mid1 u_mid2
misc/scripts/fmcombine_bwd_fwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -bwd -fwd top u_mid1 u_mid2
misc/scripts/fmcombine_fwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -fwd top u_mid1 u_mid2
misc/scripts/fmcombine_gate_cell_not_found.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine top u_mid1 u_mid8
misc/scripts/fmcombine_gold_cell_not_found.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine top u_mid8 u_mid3
misc/scripts/fmcombine_initeq.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -initeq top u_mid1 u_mid2
misc/scripts/fmcombine_invalid_number_of_param.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine
misc/scripts/fmcombine_module_not_found.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log fmcombine topp u_mid1 u_mid3
misc/scripts/fmcombine_nop.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop top u_mid1 u_mid2
misc/scripts/fmcombine_nop_with_bwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -bwd top u_mid1 u_mid2
misc/scripts/fmcombine_nop_with_fwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd top u_mid1 u_mid2
misc/scripts/fmcombine_nop_with_fwd_bwd.ys deleted 100644 → 0
read_verilog -sv ../top.v
tee -o result.log fmcombine -nop -fwd -bwd top u_mid1 u_mid2
misc/scripts/fmcombine_types_not_match.ys deleted 100644 → 0
read_verilog -sv ../top_err_1.v
proc
tee -o result.log fmcombine top u_mid1 u_urtl
misc/scripts/freduce.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/scripts/freduce_dump.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce -dump fred
misc/scripts/freduce_inv.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce -inv
misc/scripts/freduce_logic_loop.ys deleted 100644 → 0
read_verilog ../top_err_1.v
tee -o result.log freduce
proc
tee -o result.log freduce
synth
tee -o result.log freduce
misc/scripts/freduce_stop.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce -stop 1
misc/scripts/freduce_v.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce -v
misc/scripts/freduce_vv.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log freduce -vv
misc/scripts/help.ys deleted 100644 → 0
tee -q -o result.log help
misc/scripts/help_all.ys deleted 100644 → 0
tee -q -o result.log help -all
misc/scripts/help_cells.ys deleted 100644 → 0
tee -q -o result.log help -cells
misc/scripts/help_celltype.ys deleted 100644 → 0
tee -q -o result.log help $dff
misc/scripts/help_celltype_plus.ys deleted 100644 → 0
tee -q -o result.log help $dff+
misc/scripts/help_command.ys deleted 100644 → 0
tee -q -o result.log help read_verilog
misc/scripts/hilomap.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap
misc/scripts/hilomap_hicell.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -hicell VCC V
misc/scripts/hilomap_hicell_locell_singleton.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G -hicell VCC V -singleton
misc/scripts/hilomap_hicell_singleton.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -hicell VCC V -singleton
misc/scripts/hilomap_locell.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G
misc/scripts/hilomap_locell_singleton.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -locell GND G -singleton
misc/scripts/hilomap_singleton.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log hilomap -singleton
misc/scripts/history.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log history
misc/scripts/insbuf.ys deleted 100644 → 0
read_verilog ../top.v
synth
insbuf
tee -o result.log dump
write_verilog synth.v
misc/scripts/insbuf_cell.ys deleted 100644 → 0
read_verilog ../top.v
synth
insbuf -buf $_BUF_ A Y
tee -o result.log dump
write_verilog synth.v
misc/scripts/log.ys deleted 100644 → 0
tee -o result.log log "OK"
misc/scripts/log_n.ys deleted 100644 → 0
tee -o result.log log -n "OK"
misc/scripts/log_nolog.ys deleted 100644 → 0
tee -o result.log log -nolog "OK"
misc/scripts/log_stderr.ys deleted 100644 → 0
tee -o result.log log -stderr "OK"
misc/scripts/log_stdout.ys deleted 100644 → 0
tee -o result.log log -stdout "OK"
misc/scripts/ltp.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log ltp
misc/scripts/ltp_noff.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log ltp -noff
misc/scripts/miter_assert.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -make_outputs top
tee -o result.log miter -assert -make_outputs middle
misc/scripts/miter_assert_flatten.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert -flatten top
tee -o result.log miter -assert -flatten middle
misc/scripts/miter_cant_find_gate_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top gate top
misc/scripts/miter_cant_find_gold_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv gold gate top
misc/scripts/miter_cant_find_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -assert t
misc/scripts/miter_missing_mode_param.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter
misc/scripts/miter_no_match_in_gate.ys deleted 100644 → 0
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv middle u_rtl top1
misc/scripts/miter_no_match_in_gold.ys deleted 100644 → 0
read_verilog -sv ../top_err_1.v
proc
tee -o result.log miter -equiv u_rtl middle top1
misc/scripts/miter_there_is_already_a_module.ys deleted 100644 → 0
read_verilog -sv ../top.v
proc
tee -o result.log miter -equiv top middle top
misc/scripts/mutate_all.ys deleted 100644 → 0
read_verilog ../top.v
mutate -list 512 -o mutate.ys
script mutate.ys
tee -o result.log dump
misc/scripts/mutate_cnot0.ys deleted 100644 → 0
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
misc/scripts/mutate_cnot1.ys deleted 100644 → 0
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
misc/scripts/mutate_const0.ys deleted 100644 → 0
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
misc/scripts/mutate_const1.ys deleted 100644 → 0
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
misc/scripts/mutate_error.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -cell $add$../top.v:12$1 -port \Y -portbit 0 -ctrlbit 0 -module top
misc/scripts/mutate_inv.ys deleted 100644 → 0
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
misc/scripts/mutate_list.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32
misc/scripts/mutate_list_cfg.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -cfg weight_cover 1
misc/scripts/mutate_list_ctrl.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -ctrl A 1 1
misc/scripts/mutate_list_none.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -none
misc/scripts/mutate_list_o.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -o o.txt
misc/scripts/mutate_list_s.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -s s.txt
misc/scripts/mutate_list_seed.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log mutate -list 32 -seed 5
misc/scripts/muxpack.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log muxpack
misc/scripts/onehot.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx
onehot
tee -o result.log dump
misc/scripts/onehot_v.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx
onehot -v
tee -o result.log dump
misc/scripts/onehot_vv.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx
onehot -vv
tee -o result.log dump
misc/scripts/opt_rmdff_sat.ys deleted 100644 → 0
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_
misc/scripts/plugin.ys deleted 100644 → 0
tee -o result.log plugin
misc/scripts/plugin_a.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
misc/scripts/plugin_error.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log plugin -l
plugin -i uu -a alias
tee -o result.log plugin -l
misc/scripts/plugin_i.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so
misc/scripts/plugin_l.ys deleted 100644 → 0
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
misc/scripts/pmux2shiftx.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx
tee -o result.log dump
misc/scripts/pmux2shiftx_min_choices_0.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -min_choices 0
onehot
tee -o result.log dump
misc/scripts/pmux2shiftx_min_choices_3000.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -min_choices 3000
tee -o result.log dump
misc/scripts/pmux2shiftx_min_dens_0.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -min_density 0
onehot
tee -o result.log dump
misc/scripts/pmux2shiftx_min_dens_3000.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -min_density 3000
tee -o result.log dump
misc/scripts/pmux2shiftx_norange.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -norange
onehot
tee -o result.log dump
misc/scripts/pmux2shiftx_onehot_ignore.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -onehot ignore
onehot
tee -o result.log dump
misc/scripts/pmux2shiftx_onehot_pmux.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -onehot pmux
tee -o result.log dump
misc/scripts/pmux2shiftx_onehot_shiftx.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -onehot shiftx
onehot
tee -o result.log dump
misc/scripts/pmux2shiftx_top.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx top
tee -o result.log dump
misc/scripts/pmux2shiftx_v.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -v
tee -o result.log dump
misc/scripts/pmux2shiftx_vv.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmux2shiftx -vv
tee -o result.log dump
misc/scripts/pmuxtree.ys deleted 100644 → 0
read_verilog ../top.v
proc
pmuxtree
tee -o result.log dump
misc/scripts/qwp.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp
tee -o result.log dump
misc/scripts/qwp_alpha.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp -alpha
tee -o result.log dump
misc/scripts/qwp_dump.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp -dump out.html
tee -o result.log dump
misc/scripts/qwp_grid.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp -grid 4
tee -o result.log dump
misc/scripts/qwp_ltr.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp -ltr
tee -o result.log dump
misc/scripts/qwp_v.ys deleted 100644 → 0
read_verilog ../top.v
proc
qwp -v
tee -o result.log dump
misc/scripts/rename.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename middle mid_module
tee -o result.log dump
misc/scripts/rename_enumerate.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -enumerate middle mid_module
misc/scripts/rename_enumerate_pat.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -enumerate -pattern '_%_' top
misc/scripts/rename_hide.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -hide middle mid
misc/scripts/rename_invalid_number_of_args.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename
misc/scripts/rename_invalid_number_of_args_top.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -top
misc/scripts/rename_low.ys deleted 100644 → 0
read_verilog ../top.v
synth
tee -o result.log rename low newlow
tee -o result.log dump
misc/scripts/rename_mode_out_requires.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -output u uu
misc/scripts/rename_no_top_module.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -top top
misc/scripts/rename_obj_not_found.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename u uu
misc/scripts/rename_src.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -src middle mid_module
misc/scripts/rename_top.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
tee -o result.log rename -top new_top
tee -o result.log dump
misc/scripts/rename_top_top.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
tee -o result.log rename top new_top
misc/scripts/rename_wire.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log rename -wire o mid_o
misc/scripts/rmports.ys deleted 100644 → 0
read_verilog ../top.v
proc
rmports
tee -o result.log dump
misc/scripts/sat.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat middle
misc/scripts/sat_all.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -all top
misc/scripts/sat_all_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -all -prove x 1 -tempinduct middle
misc/scripts/sat_cant_open_json_file.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_json dir/out.json middle
misc/scripts/sat_cant_open_vcd_file.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_vcd dir/out.vcd middle
misc/scripts/sat_cnf_open_json_file.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_cnf dir/out.cnf middle
misc/scripts/sat_dump_cnf.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_cnf cnf.cnf middle
misc/scripts/sat_dump_json.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_json json.json middle
misc/scripts/sat_dump_vcd.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -dump_vcd vcd.vcd middle
misc/scripts/sat_enable_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -enable_undef middle
misc/scripts/sat_failed_to_import_cell.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 1 -prove x 1 -seq 2 top
misc/scripts/sat_falsify.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify middle
misc/scripts/sat_falsify_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -falsify middle
misc/scripts/sat_falsify_no_timeout.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -falsify-no-timeout middle
misc/scripts/sat_got_tempinduct_but_nothing_to_prove.ys deleted 100644 → 0
read_verilog ../top.v
tee -o result.log sat -tempinduct middle
misc/scripts/sat_ignore_div_by_zero.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -ignore-div-by-zero middle
misc/scripts/sat_ignore_unknown_cells.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells top
misc/scripts/sat_initsteps.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -initsteps 3 middle
misc/scripts/sat_max.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max 3 middle
misc/scripts/sat_max_all_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max 5 -all -prove x 1 -tempinduct middle
misc/scripts/sat_max_max_undef_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max_undef -all -prove x 1 -tempinduct top
misc/scripts/sat_max_maxundef_all_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -max_undef -all -prove x 1 -tempinduct top
misc/scripts/sat_max_maxundef_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -max_undef -prove x 1 -tempinduct top
misc/scripts/sat_max_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max_undef middle
misc/scripts/sat_max_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max 1 -prove x 1 -tempinduct top
misc/scripts/sat_maxsteps.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -maxsteps 0 middle
misc/scripts/sat_maxsteps_only_for_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -maxsteps 3 middle
misc/scripts/sat_maxundef_with_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -max_undef -prove x 1 -tempinduct top
misc/scripts/sat_only_one_module_must_be_sel.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat
misc/scripts/sat_prove.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -prove x 1 top
misc/scripts/sat_prove_and_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 365 -prove x 1 -tempinduct top
misc/scripts/sat_prove_asserts.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-asserts middle
misc/scripts/sat_prove_diff_size.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x 2'b11 middle
misc/scripts/sat_prove_lhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove X 0 middle
misc/scripts/sat_prove_rhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x X middle
misc/scripts/sat_prove_skip.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 1 -seq 2 middle
misc/scripts/sat_prove_skip_must_be_smaller_than_seq.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-skip 365 -prove x 1 -seq 1 top
misc/scripts/sat_prove_x.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x 1 middle
misc/scripts/sat_provex_diff_size.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x 2'b11 middle
misc/scripts/sat_provex_lhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-x X 0 middle
misc/scripts/sat_provex_rhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove-x x X middle
misc/scripts/sat_seq.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -seq 1 middle
misc/scripts/sat_set.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set x 3 middle
misc/scripts/sat_set_all_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef x middle
misc/scripts/sat_set_all_undef_at.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef-at 3 x middle
misc/scripts/sat_set_all_undef_at_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef-at U 1 middle
misc/scripts/sat_set_all_undef_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-all-undef U middle
misc/scripts/sat_set_any_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef x middle
misc/scripts/sat_set_any_undef_at.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef-at 3 x middle
misc/scripts/sat_set_any_undef_at_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef-at U middle
misc/scripts/sat_set_any_undef_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-any-undef U middle
misc/scripts/sat_set_assumes.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-assumes middle
misc/scripts/sat_set_at.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-at 1 x 3 middle
misc/scripts/sat_set_at_diff_size.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-at x 2'b11 middle
misc/scripts/sat_set_at_lhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-at X 0 middle
misc/scripts/sat_set_at_rhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-at x X middle
misc/scripts/sat_set_def.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-def x middle
misc/scripts/sat_set_def_at.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-def-at 3 x middle
misc/scripts/sat_set_def_at_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-def-at U middle
misc/scripts/sat_set_def_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-def U middle
misc/scripts/sat_set_def_inputs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-def-inputs middle
misc/scripts/sat_set_diff_size.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set x 2'b11 middle
misc/scripts/sat_set_init.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init x 0 middle
misc/scripts/sat_set_init_def.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-def middle
misc/scripts/sat_set_init_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef middle
misc/scripts/sat_set_init_zero.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-zero middle
misc/scripts/sat_set_lhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set X 0 middle
misc/scripts/sat_set_rhs_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set x X middle
misc/scripts/sat_show.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show x middle
misc/scripts/sat_show_all.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show-all middle
misc/scripts/sat_show_fail.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show X middle
misc/scripts/sat_show_inputs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show-inputs middle
misc/scripts/sat_show_outputs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show-outputs middle
misc/scripts/sat_show_ports.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show-ports middle
misc/scripts/sat_show_public.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -show-public middle
misc/scripts/sat_show_regs.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -ignore_unknown_cells -show-regs top
misc/scripts/sat_si_def_undef.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-def middle
misc/scripts/sat_si_def_undef_zero.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-def -set-init-zero middle
misc/scripts/sat_si_def_zero.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-def -set-init-zero middle
misc/scripts/sat_si_undef_zero.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -set-init-undef -set-init-zero middle
misc/scripts/sat_stepsize.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -stepsize 3 middle
misc/scripts/sat_tempinduct.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct middle
misc/scripts/sat_tempinduct_baseonly.ys deleted 100644 → 0
read_verilog ../top.v
proc
tee -o result.log sat -prove x 1 -tempinduct-baseonly middle
misc/scripts/sat_tempinduct_baseonly_maxsteps.ys deleted 100644 → 0
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