Skip to content

Y
yosys-tests
Commit 21ce1bed by SergeyDegtyar
Options

Add tests for error messages to 'backends' test group.

parent 5a8c478b
Showing with 2070 additions and 19 deletions
backends/Makefile
...@@ -19,9 +19,11 @@ endef ...@@ -19,9 +19,11 @@ endef
#write_aiger #write_aiger
$(eval $(call template,write_aiger,write_aiger write_aiger_ascii write_aiger_zinit write_aiger_miter write_aiger_symbols write_aiger_map write_aiger_vmap write_aiger_I write_aiger_O write_aiger_B )) $(eval $(call template,write_aiger,write_aiger write_aiger_ascii write_aiger_zinit write_aiger_miter write_aiger_symbols write_aiger_map write_aiger_vmap write_aiger_I write_aiger_O write_aiger_B ))
$(eval $(call template,write_aiger_error, write_aiger_cant_find_top_module write_aiger_cant_open_file write_aiger_miter_and_asserts write_aiger_unsupported_cell_type ))
#write_blif #write_blif
$(eval $(call template,write_blif,write_blif write_blif_top write_blif_buf write_blif_unbuf write_blif_true write_blif_false write_blif_undef write_blif_noalias write_blif_icells write_blif_gates write_blif_conn write_blif_attr write_blif_param write_blif_cname write_blif_iname write_blif_iattr write_blif_blackbox write_blif_impltf)) $(eval $(call template,write_blif,write_blif write_blif_top write_blif_buf write_blif_unbuf write_blif_true write_blif_false write_blif_undef write_blif_noalias write_blif_icells write_blif_gates write_blif_conn write_blif_attr write_blif_param write_blif_cname write_blif_iname write_blif_iattr write_blif_blackbox write_blif_impltf))
$(eval $(call template,write_blif_error, write_blif_unmapped_mem write_blif_cant_find_top_module write_blif_unmapped_proc))
#write_btor #write_btor
$(eval $(call template,write_btor,write_btor write_btor_v write_btor_s)) $(eval $(call template,write_btor,write_btor write_btor_v write_btor_s))
...@@ -33,22 +35,21 @@ $(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor ...@@ -33,22 +35,21 @@ $(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor
$(eval $(call template,write_btor_pmux,write_btor_pmux)) $(eval $(call template,write_btor_pmux,write_btor_pmux))
$(eval $(call template,write_btor_and_or,write_btor_and_or)) $(eval $(call template,write_btor_and_or,write_btor_and_or))
$(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s)) $(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s))
$(eval $(call template,write_btor_error, write_btor_no_top_module write_btor_unsupported_cell_type write_btor_no_driver))
#write_edif #write_edif
$(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc write_edif_pvector_par write_edif_pvector_bra write_edif_pvector_ang write_edif_attrprop )) $(eval $(call template,write_edif,write_edif write_edif_top write_edif_nogndvcc write_edif_pvector_par write_edif_pvector_bra write_edif_pvector_ang write_edif_attrprop ))
$(eval $(call template,write_edif_error, write_edif_cyclic_dependency write_edif_constant_nodes write_edif_unmapped_mem write_edif_unmapped_proc write_edif_no_module_found ))
#write_firrtl #write_firrtl
$(eval $(call template,write_firrtl,write_firrtl)) $(eval $(call template,write_firrtl,write_firrtl))
#write_firrtl_mem_wr - issue #938 $(eval $(call template,write_firrtl_mem,write_firrtl_mem write_firrtl_mem_wr))
#terminate called after throwing an instance of 'std::out_of_range'
# what(): dict::at()
#run.sh: line 11: 9808 Aborted (core dumped)
$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
$(eval $(call template,write_firrtl_logic,write_firrtl )) $(eval $(call template,write_firrtl_logic,write_firrtl ))
$(eval $(call template,write_firrtl_reduce,write_firrtl )) $(eval $(call template,write_firrtl_reduce,write_firrtl ))
$(eval $(call template,write_firrtl_shift,write_firrtl )) $(eval $(call template,write_firrtl_shift,write_firrtl ))
$(eval $(call template,write_firrtl_shiftx,write_firrtl )) $(eval $(call template,write_firrtl_shiftx,write_firrtl ))
$(eval $(call template,write_firrtl_paramod,write_firrtl)) $(eval $(call template,write_firrtl_paramod,write_firrtl))
$(eval $(call template,write_firrtl_error, write_firrtl_fully_selected write_firrtl_negative_edge_ff write_firrtl_inout_port write_firrtl_unclocked_write_port write_firrtl_complex_write_enable ))
#write_ilang #write_ilang
$(eval $(call template,write_ilang,write_ilang write_ilang_selected)) $(eval $(call template,write_ilang,write_ilang write_ilang_selected))
...@@ -56,17 +57,21 @@ $(eval $(call template,write_ilang_mem,write_ilang_mem)) ...@@ -56,17 +57,21 @@ $(eval $(call template,write_ilang_mem,write_ilang_mem))
$(eval $(call template,write_ilang_mux,write_ilang write_ilang_selected)) $(eval $(call template,write_ilang_mux,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_fsm,write_ilang write_ilang_selected)) $(eval $(call template,write_ilang_fsm,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected)) $(eval $(call template,write_ilang_tri,write_ilang write_ilang_selected))
$(eval $(call template,write_ilang_error,write_ilang_error))
#write_intersynth #write_intersynth
$(eval $(call template,write_intersynth,write_intersynth write_intersynth_selected write_intersynth_lib write_intersynth_notypes)) $(eval $(call template,write_intersynth,write_intersynth write_intersynth_selected write_intersynth_lib write_intersynth_notypes))
$(eval $(call template,write_intersynth_error, write_intersynth_cant_export write_intersynth_unprocessed_proc write_intersynth_cant_open_lib_file))
#write_json #write_json
$(eval $(call template,write_json,write_json write_json_aig json json_o json_o_aig json_aig)) $(eval $(call template,write_json,write_json write_json_aig json json_o json_o_aig json_aig))
$(eval $(call template,write_json_error,write_json_error))
#write_simplec #write_simplec
$(eval $(call template,write_simplec,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64)) $(eval $(call template,write_simplec,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_mux,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64)) $(eval $(call template,write_simplec_mux,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_logic,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64)) $(eval $(call template,write_simplec_logic,write_simplec write_simplec_cmos3 write_simplec_cmos4 write_simplec_verbose write_simplec_i8 write_simplec_i16 write_simplec_i32 write_simplec_i64))
$(eval $(call template,write_simplec_error,write_simplec_no_c_model write_simplec_not_top_module ))
#write_smt2 #write_smt2
$(eval $(call template,write_smt2,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv)) $(eval $(call template,write_smt2,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
...@@ -76,6 +81,7 @@ $(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_ver ...@@ -76,6 +81,7 @@ $(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_ver
$(eval $(call template,write_smt2_init_assert,write_smt2_init_assert)) $(eval $(call template,write_smt2_init_assert,write_smt2_init_assert))
$(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv)) $(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv)) $(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
$(eval $(call template,write_smt2_error, write_smt2_cyclic_dependency write_smt2_cant_open_tpl write_smt2_multiple_drivers write_smt2_logic_loop ))
#write_smv #write_smv
$(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl)) $(eval $(call template,write_smv,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
...@@ -87,9 +93,11 @@ $(eval $(call template,write_smv_logic,write_smv write_smv_synth write_smv_nopro ...@@ -87,9 +93,11 @@ $(eval $(call template,write_smv_logic,write_smv write_smv_synth write_smv_nopro
$(eval $(call template,write_smv_init_assert,write_smv_init_assert)) $(eval $(call template,write_smv_init_assert,write_smv_init_assert))
$(eval $(call template,write_smv_cmos4,write_smv_cmos4)) $(eval $(call template,write_smv_cmos4,write_smv_cmos4))
$(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl)) $(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
$(eval $(call template,write_smv_error,write_smv_cant_open_template write_smv_unsupported_cell))
#write_spice #write_spice
$(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_endian write_spice_neg_i write_spice_pos_i write_spice_nc_prefix write_spice_inames )) $(eval $(call template,write_spice,write_spice write_spice_top write_spice_big_endian write_spice_neg_i write_spice_pos_i write_spice_nc_prefix write_spice_inames ))
$(eval $(call template,write_spice_error, write_spice_cant_find_top_module write_spice_unmapped_mem write_spice_unmapped_proc))
#write_table #write_table
$(eval $(call template,write_table,write_table )) $(eval $(call template,write_table,write_table ))
......
backends/run.sh
...@@ -10,34 +10,128 @@ cd $1/work_$2 ...@@ -10,34 +10,128 @@ cd $1/work_$2
touch .start touch .start
yosys -ql yosys.log ../../scripts/$2.ys # cases where 'syntax error' or other errors are expected
if [ $? != 0 ] ; then if echo "$1" | grep ".*_error"; then
expected_string=""
#Change checked string for check other errors
if [ "$2" = "write_aiger_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module in current design!"
elif [ "$2" = "write_aiger_cant_open_file" ]; then
expected_string="ERROR: Can't open file "
elif [ "$2" = "write_aiger_miter_and_asserts" ]; then
expected_string="ERROR: Running AIGER back-end in -miter mode, but design contains \$assert, \$assume, \$live and/or \$fair cells!"
elif [ "$2" = "write_aiger_unsupported_cell_type" ]; then
expected_string="ERROR: Unsupported cell type: "
elif [ "$2" = "write_blif_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_blif_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module "
elif [ "$2" = "write_blif_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module "
elif [ "$2" = "write_btor_no_top_module" ]; then
expected_string="ERROR: No top module found."
elif [ "$2" = "write_btor_unsupported_cell_type" ]; then
expected_string="ERROR: Unsupported cell type: "
elif [ "$2" = "write_btor_no_driver" ]; then
expected_string="ERROR: No driver for signal bit "
elif [ "$2" = "write_edif_cyclic_dependency" ]; then
expected_string="ERROR: Cyclic dependency between modules found! Cycle includes module "
elif [ "$2" = "write_edif_constant_nodes" ]; then
expected_string="ERROR: Design contains constant nodes (map with \"hilomap\" first)."
elif [ "$2" = "write_edif_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_edif_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module "
elif [ "$2" = "write_edif_no_module_found" ]; then
expected_string="ERROR: No module found in design!"
elif [ "$2" = "write_firrtl_fully_selected" ]; then
expected_string="ERROR: This command only operates on fully selected designs!"
elif [ "$2" = "write_firrtl_negative_edge_ff" ]; then
expected_string="ERROR: Negative edge clock on FF "
elif [ "$2" = "write_firrtl_inout_port" ]; then
expected_string="ERROR: Module port top.q_a is inout!"
elif [ "$2" = "write_firrtl_unclocked_write_port" ]; then
expected_string="ERROR: Unclocked write port "
elif [ "$2" = "write_firrtl_complex_write_enable" ]; then
expected_string="ERROR: Complex write enable on port "
elif [ "$2" = "write_ilang_error" ]; then
expected_string="ERROR: Can't open file \`tt/file1.il' for writing: No such file or directory"
elif [ "$2" = "write_intersynth_cant_export" ]; then
expected_string="ERROR: Can't export composite or non-word-wide signal "
elif [ "$2" = "write_intersynth_unprocessed_proc" ]; then
expected_string="ERROR: Can't generate a netlist for a module with unprocessed memories or processes!"
elif [ "$2" = "write_intersynth_cant_open_lib_file" ]; then
expected_string="ERROR: Can't open lib file "
elif [ "$2" = "write_json_error" ]; then
expected_string="ERROR: Can't open file "
elif [ "$2" = "write_simplec_no_c_model" ]; then
expected_string="ERROR: No C model for \$lut available at the moment (FIXME)."
elif [ "$2" = "write_simplec_not_top_module" ]; then
expected_string="ERROR: Current design has no top module."
elif [ "$2" = "write_smt2_cyclic_dependency" ]; then
expected_string="ERROR: Cyclic dependency between modules found! Cycle includes module "
elif [ "$2" = "write_smt2_cant_open_tpl" ]; then
expected_string="ERROR: Can't open template file "
elif [ "$2" = "write_smt2_multiple_drivers" ]; then
expected_string="ERROR: Found multiple drivers for "
elif [ "$2" = "write_smt2_logic_loop" ]; then
expected_string="ERROR: Found logic loop in module "
elif [ "$2" = "write_smv_cant_open_template" ]; then
expected_string="ERROR: Can't open template file "
elif [ "$2" = "write_smv_unsupported_cell" ]; then
expected_string="ERROR: Found currently unsupported cell type "
elif [ "$2" = "write_spice_cant_find_top_module" ]; then
expected_string="ERROR: Can't find top module "
elif [ "$2" = "write_spice_unmapped_mem" ]; then
expected_string="ERROR: Found unmapped memories in module "
elif [ "$2" = "write_spice_unmapped_proc" ]; then
expected_string="ERROR: Found unmapped processes in module"
fi
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
yosys -ql yosys.log ../../scripts/$2.ys
if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status echo FAIL > ${1}_${2}.status
touch .stamp touch .stamp
exit 0 exit 0
fi fi
sed -i 's/reg =/dummy =/' ./synth.v sed -i 's/reg =/dummy =/' ./synth.v
if [ -f "../../../../../techlibs/common/simcells.v" ]; then if [ -f "../../../../../techlibs/common/simcells.v" ]; then
COMMON_PREFIX=../../../../../techlibs/common COMMON_PREFIX=../../../../../techlibs/common
else else
COMMON_PREFIX=/usr/local/share/yosys COMMON_PREFIX=/usr/local/share/yosys
fi fi
iverilog -o testbench ../testbench.v synth.v ../../common.v $COMMON_PREFIX/simcells.v $COMMON_PREFIX/simlib.v iverilog -o testbench ../testbench.v synth.v ../../common.v $COMMON_PREFIX/simcells.v $COMMON_PREFIX/simlib.v
if [ $? != 0 ] ; then if [ $? != 0 ] ; then
echo FAIL > ${1}_${2}.status echo FAIL > ${1}_${2}.status
touch .stamp touch .stamp
exit 0 exit 0
fi fi
if ! vvp -N testbench > testbench.log 2>&1; then if ! vvp -N testbench > testbench.log 2>&1; then
grep 'ERROR' testbench.log grep 'ERROR' testbench.log
echo FAIL > ${1}_${2}.status echo FAIL > ${1}_${2}.status
elif grep 'ERROR' testbench.log || ! grep 'OKAY' testbench.log; then elif grep 'ERROR' testbench.log || ! grep 'OKAY' testbench.log; then
echo FAIL > ${1}_${2}.status echo FAIL > ${1}_${2}.status
else else
echo PASS > ${1}_${2}.status echo PASS > ${1}_${2}.status
fi
fi fi
touch .stamp touch .stamp
backends/scripts/write_aiger_cant_find_top_module.ys 0 → 100644
read_verilog -sv ../top.v
aigmap
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_cant_open_file.ys 0 → 100644
read_verilog -sv ../top2.v
aigmap
write_aiger -map tt/tt.map aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_miter_and_asserts.ys 0 → 100644
read_verilog -sv ../top2.v
aigmap
write_aiger -miter aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_aiger_unsupported_cell_type.ys 0 → 100644
read_verilog -sv ../top2.v
synth
write_aiger aiger.aiger
design -reset
read_verilog -sv ../top_clean.v
aigmap
write_aiger aiger.aiger
synth -top top
write_verilog synth.v
backends/scripts/write_blif_cant_find_top_module.ys 0 → 100644
read_verilog -sv ../top.v
proc
write_blif -top u blif1.blif
backends/scripts/write_blif_unmapped_mem.ys 0 → 100644
read_verilog -sv ../top2.v
proc
write_blif -top u blif1.blif
backends/scripts/write_blif_unmapped_proc.ys 0 → 100644
read_verilog -sv ../top.v
write_blif blif1.blif
backends/scripts/write_btor_no_driver.ys 0 → 100644
read_verilog ../top.v
memory
write_btor btor.btor
backends/scripts/write_btor_no_top_module.ys 0 → 100644
read_verilog ../top3.v
memory
proc
write_btor btor.btor
backends/scripts/write_btor_unsupported_cell_type.ys 0 → 100644
read_verilog ../top3.v
synth_ice40
write_btor btor.btor
backends/scripts/write_edif_constant_nodes.ys 0 → 100644
read_verilog -sv ../top3.v
proc
write_edif -nogndvcc blif1.blif
backends/scripts/write_edif_cyclic_dependency.ys 0 → 100644
read_verilog -sv ../top4.v
proc
write_edif blif1.blif
backends/scripts/write_edif_no_module_found.ys 0 → 100644
write_edif edif.edif
write_verilog synth.v
backends/scripts/write_edif_unmapped_mem.ys 0 → 100644
read_verilog ../top2.v
proc
write_edif -top top edif.edif
write_verilog synth.v
backends/scripts/write_edif_unmapped_proc.ys 0 → 100644
read_verilog ../top.v
write_edif -top top edif.edif
write_verilog synth.v
backends/scripts/write_firrtl_complex_write_enable.ys 0 → 100644
read_verilog ../top1.v
proc
memory
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_firrtl_fully_selected.ys 0 → 100644
read_verilog ../top1.v
proc
memory_dff -nordff
memory_collect
opt_reduce
clean
select top22
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_firrtl_inout_port.ys 0 → 100644
read_verilog ../top2.v
proc
memory_dff -nordff
memory_collect
opt_reduce
clean
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_firrtl_mem_wr.ys
read_verilog ../top.v read_verilog ../top.v
proc proc
memory_dff -nordff memory_dff -nordff
memory_collect
opt_reduce opt_reduce
clean clean
write_firrtl firrtl.firrtl write_firrtl firrtl.firrtl
......
backends/scripts/write_firrtl_negative_edge_ff.ys 0 → 100644
read_verilog ../top3.v
proc
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_firrtl_unclocked_write_port.ys 0 → 100644
read_verilog ../top.v
memory
proc
write_firrtl firrtl.firrtl
write_verilog synth.v
backends/scripts/write_ilang.ys
...@@ -2,7 +2,7 @@ read_verilog ../top.v ...@@ -2,7 +2,7 @@ read_verilog ../top.v
write_ilang ilang.ilang write_ilang ilang.ilang
proc proc
dump -o file.il dump -o file.il
write_ilang ilang.ilang write_ilang -o file.ilang ilang.ilang
dump -n -o file1.il dump -n -o file1.il
synth synth
write_verilog synth.v write_verilog synth.v
backends/scripts/write_ilang_error.ys 0 → 100644
read_verilog ../top.v
write_ilang ilang.ilang
proc
dump -o file.il
write_ilang ilang.ilang
dump -n -o tt/file1.il
synth
write_verilog synth.v
backends/scripts/write_intersynth_cant_export.ys 0 → 100644
read_verilog ../top.v
proc
synth
abc -lut 4
write_intersynth intersynth.intersynth
write_verilog synth.v
backends/scripts/write_intersynth_cant_open_lib_file.ys 0 → 100644
read_verilog ../top.v
proc
write_intersynth -lib u intersynth.intersynth
write_verilog synth.v
backends/scripts/write_intersynth_unprocessed_proc.ys 0 → 100644
read_verilog ../top.v
write_intersynth intersynth.intersynth
write_verilog synth.v
backends/scripts/write_json_error.ys 0 → 100644
read_verilog ../top.v
proc
json -o tt/json.json
write_verilog synth.v
backends/scripts/write_simplec_no_c_model.ys 0 → 100644
read_verilog ../top.v
synth -top top
abc -lut 4
write_simplec c.c
write_verilog synth.v
backends/scripts/write_simplec_not_top_module.ys 0 → 100644
read_verilog ../top.v
write_simplec c.c
write_verilog synth.v
backends/scripts/write_smt2_cant_open_tpl.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smt2 -tpl u smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_cyclic_dependency.ys 0 → 100644
read_verilog ../top3.v
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_logic_loop.ys 0 → 100644
read_verilog ../top1.v
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smt2_multiple_drivers.ys 0 → 100644
read_verilog ../top2.v
proc
memory
write_smt2 smt2.smt2
write_verilog synth.v
backends/scripts/write_smv_cant_open_template.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smv -tpl t smv.smv
write_verilog synth.v
backends/scripts/write_smv_unsupported_cell.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_smv smv.smv
write_verilog synth.v
backends/scripts/write_spice_cant_find_top_module.ys 0 → 100644
read_verilog ../top.v
proc
memory
write_spice -top u sp.sp
write_verilog synth.v
backends/scripts/write_spice_unmapped_mem.ys 0 → 100644
read_verilog ../top.v
proc
write_spice sp.sp
write_verilog synth.v
backends/scripts/write_spice_unmapped_proc.ys 0 → 100644
read_verilog ../top.v
write_spice sp.sp
write_verilog synth.v
backends/write_aiger_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out;
wire carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_aiger_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
module top2
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_aiger_error/top2.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output X
);
reg ASSERT = 1'bX;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 1'bX;
cout = 1'bZ;
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 1'bX;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 1'bZ;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
assign X = 1'bX;
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_aiger_error/top_clean.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_blif_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
reg patt_out1 = 0;
reg patt_carry_out1 = 0;
wire out;
wire carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
always @(posedge in[0]) begin
patt_out1 <= ~in[1] + &in[2];
end
always @(negedge in[0]) begin
patt_carry_out1 <= in[2] ? |in[1] : patt_out;
end
always @(*) begin
if (in[0])
patt_out <= patt_out|in[1]~&in[2];
end
always @(*) begin
if (~in[0])
patt_carry_out <= patt_carry_out1&in[2]~|in[1];
end
assert_Z out_test(.A(out));
endmodule
backends/write_blif_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg A1,cout1;
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A1 <= ~y + &cin;
end
always @(negedge x) begin
cout1 <= cin ? |y : ^A;
end
always @(*) begin
if (x)
A <= A1|y~&cin;
end
always @(*) begin
if (~x)
cout <= cout1&cin~|y;
end
`else
assign {cout,A} = 1'bZ;
`endif
bb ubb (cin,y,x,A);
endmodule
(* black_box *) module bb(in1, in2, clk, out1);
input in1;
input in2;
input clk;
output reg out1;
always @(posedge clk)
out1 <= in1 & in2;
endmodule
backends/write_blif_error/top2.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, clk,
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 clk)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_btor_error/top.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, clk,
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 clk, posedge re_b)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_btor_error/top2.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, clk,
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 clk)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_btor_error/top3.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, clk,
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 clk)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
module top2
(
input [7:0] data_a, data_b,
input [6:1] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clk,
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 clk)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_edif_error/edif.edif 0 → 100644
(edif (rename id00001 "u/u")
(edifVersion 2 0 0)
(edifLevel 0)
(keywordMap (keywordLevel 0))
(comment "Generated by Yosys 0.8+553 (git sha1 c9949dba, gcc 8.3.0-6ubuntu1~18.10.1 -Og -fPIC)")
(external LIB
(edifLevel 0)
(technology (numberDefinition))
(cell GND
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface (port G (direction OUTPUT)))
)
)
(cell VCC
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface (port P (direction OUTPUT)))
)
)
(cell (rename id00002 "$and")
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface
(port A (direction INPUT))
(port B (direction INPUT))
(port Y (direction OUTPUT))
)
)
)
(cell (rename id00003 "$add")
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface
(port A (direction INPUT))
(port B (direction INPUT))
(port Y (direction OUTPUT))
)
)
)
(cell (rename id00004 "$dff")
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface
(port CLK (direction INPUT))
(port Q (direction OUTPUT))
(port D (direction INPUT))
)
)
)
)
(library DESIGN
(edifLevel 0)
(technology (numberDefinition))
(cell bb
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface
(port out1 (direction OUTPUT))
(port clk (direction INPUT))
(port in2 (direction INPUT))
(port in1 (direction INPUT))
)
(contents
(instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))
(instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))
(instance (rename id00005 "$procdff$8")
(viewRef VIEW_NETLIST (cellRef id00004 (libraryRef LIB)))
(property CLK_POLARITY (integer 1))
(property WIDTH (integer 1)))
(instance (rename id00006 "$and$top.v:40$7")
(viewRef VIEW_NETLIST (cellRef id00002 (libraryRef LIB)))
(property Y_WIDTH (integer 1))
(property B_WIDTH (integer 1))
(property A_WIDTH (integer 1))
(property B_SIGNED (integer 0))
(property A_SIGNED (integer 0)))
(net out1 (joined
(portRef Q (instanceRef id00005))
(portRef out1)
))
(net clk (joined
(portRef CLK (instanceRef id00005))
(portRef clk)
))
(net (rename id00007 "$and$top.v:40$7_Y") (joined
(portRef D (instanceRef id00005))
(portRef Y (instanceRef id00006))
))
(net in2 (joined
(portRef B (instanceRef id00006))
(portRef in2)
))
(net in1 (joined
(portRef A (instanceRef id00006))
(portRef in1)
))
)
)
)
(cell top
(cellType GENERIC)
(view VIEW_NETLIST
(viewType NETLIST)
(interface
(port cout (direction OUTPUT))
(port A (direction OUTPUT))
(port cin (direction INPUT))
(port y (direction INPUT))
(port x (direction INPUT))
)
(contents
(instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))
(instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))
(instance (rename id00008 "$procdff$10")
(viewRef VIEW_NETLIST (cellRef id00004 (libraryRef LIB)))
(property CLK_POLARITY (integer 1))
(property WIDTH (integer 1)))
(instance (rename id00009 "$procdff$9")
(viewRef VIEW_NETLIST (cellRef id00004 (libraryRef LIB)))
(property CLK_POLARITY (integer 0))
(property WIDTH (integer 1)))
(instance ubb
(viewRef VIEW_NETLIST (cellRef bb)))
(instance (rename id00014 "$add$top.v:23$4")
(viewRef VIEW_NETLIST (cellRef id00003 (libraryRef LIB)))
(property Y_WIDTH (integer 1))
(property B_WIDTH (integer 1))
(property A_WIDTH (integer 1))
(property B_SIGNED (integer 0))
(property A_SIGNED (integer 0)))
(instance (rename id00015 "$add$top.v:20$2")
(viewRef VIEW_NETLIST (cellRef id00003 (libraryRef LIB)))
(property Y_WIDTH (integer 1))
(property B_WIDTH (integer 1))
(property A_WIDTH (integer 1))
(property B_SIGNED (integer 0))
(property A_SIGNED (integer 0)))
(net y (joined
(portRef A (instanceRef id00014))
(portRef A (instanceRef id00015))
(portRef id00012 (instanceRef ubb))
(portRef y)
))
(net x (joined
(portRef CLK (instanceRef id00008))
(portRef CLK (instanceRef id00009))
(portRef id00011 (instanceRef ubb))
(portRef x)
))
(net cout (joined
(portRef Q (instanceRef id00009))
(portRef cout)
))
(net cin (joined
(portRef B (instanceRef id00015))
(portRef cin)
(portRef id00013 (instanceRef ubb))
))
(net bb_out (joined
(portRef id00010 (instanceRef ubb))
))
(net (rename id00016 "$add$top.v:20$2_Y") (joined
(portRef D (instanceRef id00008))
(portRef Y (instanceRef id00015))
))
(net (rename id00017 "$add$top.v:23$4_Y") (joined
(portRef D (instanceRef id00009))
(portRef Y (instanceRef id00014))
))
(net A (joined
(portRef A)
(portRef B (instanceRef id00014))
(portRef Q (instanceRef id00008))
))
)
)
)
)
(design (rename id00001 "u/u")
(cellRef id00001 (libraryRef DESIGN))
)
)
backends/write_edif_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out;
wire carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_edif_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
wire bb_out;
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
bb ubb (cin,y,x,bb_out);
endmodule
(* black_box *) module bb(in1, in2, clk, out1);
input in1;
input in2;
input clk;
output reg out1;
always @(posedge clk)
out1 <= in1 & in2;
endmodule
backends/write_edif_error/top2.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, clk,
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 clk)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clk)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_edif_error/top3.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output X
);
wire bb_out;
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
assign X = 1'bX;
bb ubb (cin,y,x,bb_out);
endmodule
(* black_box *) module bb(in1, in2, clk, out1);
input in1;
input in2;
input clk;
output reg out1;
always @(posedge clk)
out1 <= in1 & in2;
endmodule
backends/write_edif_error/top4.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout,
output X
);
wire bb_out;
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
assign X = 1'bX;
bb ubb (cin,y,x,bb_out);
endmodule
(* black_box *) module bb(in1, in2, clk, out1);
input in1;
input in2;
input clk;
output reg out1;
always @(posedge clk)
out1 <= in1 & in2;
top utop (in1,in2,clk,out1);
endmodule
backends/write_firrtl_error/top.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
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_firrtl_error/top1.v 0 → 100644
module top
(
input [7:0] data_a, data_b,
input [0:0] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clka, clkb,
output reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_firrtl_error/top2.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,
inout reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[0:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_firrtl_error/top3.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_ilang_error/testbench.v 0 → 100644
module testbench;
reg [0:7] in;
reg patt_B = 0;
wire B;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[1:2]),
.y(in[3:4]),
.z(in[5:6]),
.clk(in[0]),
.A(in[7]),
.B(B)
);
always @(negedge in[0]) begin
if (in[1:2] || in[3:4] && in[5:6])
patt_B <= in[7] & in[5:6];
if (in[1:2] || in[3:4] && !in[5:6])
patt_B <= in[7] | in[1:2];
end
assert_comb out_test(.A(patt_B), .B(B));
endmodule
backends/write_ilang_error/top.v 0 → 100644
module top
(
input [1:0] x,
input [1:0] y,
input [1:0] z,
input clk,
input A,
output reg B
);
initial begin
B = 0;
end
`ifndef BUG
always @(posedge clk) begin
if (x || y && z)
B <= A & z;
if (x || y && !z)
B <= A | x;
end
`else
always @(posedge clk) begin
B = z - y + x;
end
`endif
endmodule
backends/write_intersynth_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_intersynth_error/top2.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
reg ASSERT = 1;
(* anyconst *) reg foo;
(* anyseq *) reg too;
initial begin
begin
A = 0;
cout = 0;
end
end
`ifndef BUG
always @(posedge x) begin
if ($initstate)
A <= 0;
A <= y + cin + too;
assume(too);
assume(s_eventually too);
end
always @(negedge x) begin
if ($initstate)
cout <= 0;
cout <= y + A + foo;
assert(ASSERT);
assert(s_eventually ASSERT);
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_json_error/testbench.v 0 → 100644
module testbench;
reg [2:0] in;
reg patt_out = 0;
reg patt_carry_out = 0;
wire out;
wire carryout;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 in = 0;
repeat (10000) begin
#5 in = in + 1;
end
$display("OKAY");
end
top uut (
.x(in[0]),
.y(in[1]),
.cin(in[2]),
.A(out),
.cout(carryout)
);
always @(posedge in[0])
patt_out <= in[1] + in[2];
always @(negedge in[0])
patt_carry_out <= in[1] + patt_out;
assert_comb out_test(.A(patt_out), .B(out));
assert_comb carry_test(.A(patt_carry_out), .B(carryout));
endmodule
backends/write_json_error/top.v 0 → 100644
module top
(
input x,
input y,
input cin,
output reg A,
output reg cout
);
initial begin
A = 0;
cout = 0;
end
`ifndef BUG
always @(posedge x) begin
A <= y + cin;
end
always @(negedge x) begin
cout <= y + A;
end
`else
assign {cout,A} = cin - y * x;
`endif
endmodule
backends/write_simplec_error/testbench.v 0 → 100644
module testbench;
reg en;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#5 en = 0;
repeat (10000) begin
#5 en = 1;
#5 en = 0;
end
$display("OKAY");
end
reg dinA = 0;
wire [1:0] dioB;
wire [1:0] doutC;
top uut (
.en (en ),
.a (dinA ),
.b (dioB ),
.c (doutC )
);
always @(posedge en) begin
#3;
dinA <= !dinA;
end
assert_equal b_test(.clk(en), .test(dinA), .pat(dioB[0]));
assert_equal c_test(.clk(en), .test(dinA), .pat(doutC[0]));
assert_equal cz_test(.clk(!en), .test(1'bZ), .pat(doutC[0]));
endmodule
backends/write_simplec_error/top.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = i & ~en;
assign io[1] = i ? en : ~en;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends/write_smt2_error/top.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends/write_smt2_error/top1.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? o[1] : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends/write_smt2_error/top2.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign io[0] = (~en)? ~i : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends/write_smt2_error/top3.v 0 → 100644
module tristate (en, i, o);
input en;
input i;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
top utop (en,i,o,io);
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.o (c )
);
endmodule
backends/write_smv_error/top.tpl 0 → 100644
asdfsfSmodule u
(
input [7:0] data_a, data_b,
input [6:1] addr_a, addr_b,
input we_a, we_b, re_a, re_b, clka, clkb,
output reg [7:0] q_a, q_b
);
// Declare the RAM variable
reg [7:0] ram[63:0];
initial begin
q_a <= 8'h00;
q_b <= 8'd0;
end
// Port A
always @ (posedge clka)
begin
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_smv_error/top.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
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
backends/write_smv_error/top1.v 0 → 100644
module tristate (en, i, io, o);
input en;
input i;
inout [1:0] io;
output [1:0] o;
wire [1:0] io;
`ifndef BUG
assign io[0] = (en)? i : 1'bZ;
assign io[1] = (i)? en : 1'bZ;
assign o = io;
`else
assign io[0] = (en)? ~i : 1'bZ;
assign io[1] = (i)? ~en : 1'bZ;
assign o = ~io;
`endif
endmodule
module top (
input en,
input a,
inout [1:0] b,
output [1:0] c
);
tristate u_tri (
.en (en ),
.i (a ),
.io (b ),
.o (c )
);
endmodule
backends/write_spice_error/top.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
`ifndef BUG
if (we_a)
`else
if (we_b)
`endif
begin
ram[addr_a] <= data_a;
q_a <= data_a;
end
if (re_b)
begin
q_a <= ram[addr_a];
end
end
// Port B
always @ (posedge clkb)
begin
`ifndef BUG
if (we_b)
`else
if (we_a)
`endif
begin
ram[addr_b] <= data_b;
q_b <= data_b;
end
if (re_b)
begin
q_b <= ram[addr_b];
end
end
endmodule
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