Merge branch 'master' into xc7srl_cleanup

architecture/Makefile

@@ -71,6 +71,7 @@ $(eval $(call template,synth_xilinx,synth_xilinx synth_xilinx_top synth_xilinx_b
 $(eval $(call template,synth_xilinx_error,synth_xilinx_fully_selected synth_xilinx_invalid_arch ))
 ifeq ($(ENABLE_HEAVY_TESTS),1)
 $(eval $(call template,synth_xilinx_srl,synth_xilinx_srl))
+$(eval $(call template,synth_xilinx_mux,synth_xilinx_mux))
 endif
 
 #greenpak4

architecture/run.sh

@@ -2,7 +2,6 @@
 
 set -x
 test -d $1
-test -f scripts/$2.ys
 
 rm -rf $1/work_$2
 mkdir $1/work_$2
@@ -25,7 +24,6 @@ if echo "$1" | grep ".*_error"; then
 		expected_string="ERROR: Invalid Xilinx -family setting: "
 	fi
 
-
 	if yosys -ql yosys.log ../../scripts/$2.ys; then
 		echo FAIL > ${1}_${2}.status
 	else
@@ -41,10 +39,13 @@ else
 		../run-test.sh
 		if [ $? != 0 ] ; then
 			echo FAIL > ${1}_${2}.status
+		else
+			echo PASS > ${1}_${2}.status
 		fi
 		touch .stamp
-		exit 0
+		exit
 	else
+		test -f scripts/$2.ys
 		yosys -ql yosys.log ../../scripts/$2.ys
 		if [ $? != 0 ] ; then
 			echo FAIL > ${1}_${2}.status

architecture/synth_xilinx_mux/assert_area.py

+#!/usr/bin/python3
+
+import glob
+import re
+import os
+
+re_mux = re.compile(r'mux_(index|case|if_bal|if_unbal)_(\d+)_(\d+)\.v')
+
+area = {}
+#             1  2  3  4  5  6 F7 F8
+area[2]   = [ 0, 0, 1, 0, 0, 0, 0, 0 ]
+area[3]   = [ 0, 0, 0, 0, 1, 0, 0, 0 ]
+area[4]   = [ 0, 0, 0, 0, 0, 0, 2, 1 ]
+area[5]   = [ 0, 0, 1, 0, 0, 0, 2, 1 ]
+area[7]   = [ 0, 0, 3, 0, 0, 0, 2, 1 ]
+area[8]   = [ 0, 0, 4, 0, 0, 0, 2, 1 ]
+area[9]   = [ 0, 0, 3, 0, 1, 0, 2, 1 ]
+area[15]  = [ 0, 0, 0, 0, 1, 3, 2, 1 ]
+area[16]  = [ 0, 0, 0, 0, 0, 4, 2, 1 ]
+area[17]  = [ 0, 0, 1, 0, 0, 4, 2, 1 ]
+area[31]  = [ 0, 0, 1, 0, 1, 7, 4, 2 ]
+area[32]  = [ 0, 0, 1, 0, 0, 8, 4, 2 ]
+area[33]  = [ 0, 0, 0, 0, 1, 8, 4, 2 ]
+area[63]  = [ 0, 0, 0, 0, 1,15,10, 5 ]
+area[64]  = [ 0, 0, 0, 0, 0,16,10, 5 ]
+area[65]  = [ 0, 0, 1, 0, 0,16,10, 5 ]
+area[127] = [ 0, 0, 4, 0, 1,31,18, 9 ]
+area[128] = [ 0, 0, 4, 0, 0,32,18, 9 ]
+area[129] = [ 0, 0, 3, 0, 1,32,18, 9 ]
+area[255] = [ 0, 0, 0, 0, 1,67,34,17 ]
+area[256] = [ 0, 0, 0, 0, 0,68,34,17 ]
+area[257] = [ 0, 0, 1, 0, 0,68,34,17 ]
+
+for fn in glob.glob('*.v'):
+    m = re_mux.match(fn)
+    if not m: continue
+
+    N,W = map(int, m.group(2,3))
+    assert N in area
+
+    bn,_ = os.path.splitext(fn)
+
+    with open(fn, 'a') as f:
+        assert_area = ['select t:{0} -assert-count {1}'.format(r,v*W) for r,v in zip(['LUT1','LUT2','LUT3','LUT4','LUT5','LUT6','MUXF7','MUXF8'], area[N])]
+        print('''
+`ifndef _AUTOTB
+module __test ;
+    wire [4095:0] assert_area = "cd; %s";
+endmodule
+`endif
+''' % '; '.join(assert_area), file=f)

architecture/synth_xilinx_mux/run-test.sh

+#!/bin/bash
+set -e
+
+OPTIND=1
+seed=""    # default to no seed specified
+while getopts "S:" opt
+do
+    case "$opt" in
+	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+	   seed="SEED=$arg" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
+# check for Icarus Verilog
+if ! which iverilog > /dev/null ; then
+  echo "$0: Error: Icarus Verilog 'iverilog' not found."
+  exit 1
+fi
+
+wget https://raw.githubusercontent.com/YosysHQ/yosys-bench/master/verilog/benchmarks_small/mux/generate.py -O generate_small.py -o /dev/null
+wget https://raw.githubusercontent.com/YosysHQ/yosys-bench/master/verilog/benchmarks_small/mux/common.py -O common.py -o /dev/null
+wget https://raw.githubusercontent.com/YosysHQ/yosys-bench/master/verilog/benchmarks_large/mux/generate.py -O generate_large.py -o /dev/null
+python3 generate_small.py
+python3 generate_large.py
+python3 ../assert_area.py
+${MAKE:-make} -f ../../../../tools/autotest.mk $seed *.v EXTRA_FLAGS="\
+    -p 'design -copy-to __test __test; \
+        synth_xilinx -abc9 -widemux 4; \
+        design -copy-from __test *; \
+        select -assert-any __test; \
+        script -scriptwire __test/w:assert_area'\
+    -l ../../../../../techlibs/xilinx/cells_sim.v"
+
+# Spot tests for -widemux thresholds
+set +e
+../../../../../yosys -qp "synth_xilinx -widemux 1" 2> /dev/null
+if [ $? -eq 0 ]; then
+    echo "Expected error"
+    exit 1
+fi
+set -e
+
+../../../../../yosys -qp "synth_xilinx -widemux 5; select -assert-none t:MUXF*" mux_if_bal_2_1.v
+../../../../../yosys -qp "synth_xilinx -widemux 4; select -assert-none t:MUXF*" mux_if_bal_2_1.v
+../../../../../yosys -qp "synth_xilinx -widemux 3; select -assert-none t:MUXF*" mux_if_bal_2_1.v
+../../../../../yosys -qp "synth_xilinx -widemux 2; select -assert-count 1 t:MUXF7" mux_if_bal_2_1.v
+
+../../../../../yosys -qp "synth_xilinx -widemux 5; select -assert-none t:MUXF*" mux_case_3_3.v
+../../../../../yosys -qp "synth_xilinx -widemux 4; select -assert-none t:MUXF*" mux_case_3_3.v
+../../../../../yosys -qp "synth_xilinx -widemux 3; select -assert-count 6 t:MUXF*" mux_case_3_3.v
+../../../../../yosys -qp "synth_xilinx -widemux 2; select -assert-count 6 t:MUXF*" mux_case_3_3.v
+
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 9; select -assert-none t:MUXF*" mux_index_7_5.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 8; select -assert-none t:MUXF*" mux_index_7_5.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 7; select -assert-count 15 t:MUXF*" mux_index_7_5.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 6; select -assert-count 15 t:MUXF*" mux_index_7_5.v
+
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 18; select -assert-none t:MUXF*" mux_if_unbal_16_8.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 17; select -assert-none t:MUXF*" mux_if_unbal_16_8.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 16; select -assert-count 24 t:MUXF*" mux_if_unbal_16_8.v
+../../../../../yosys -qp "synth_xilinx -nowidelut -widemux 15; select -assert-count 24 t:MUXF*" mux_if_unbal_16_8.v

backends/Makefile

@@ -19,9 +19,11 @@ endef
 
 #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_error, write_aiger_cant_find_top_module write_aiger_cant_open_file write_aiger_miter_and_asserts write_aiger_unsupported_cell_type ))
 
 #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_error, write_blif_unmapped_mem write_blif_cant_find_top_module write_blif_unmapped_proc))
 
 #write_btor
 $(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
 $(eval $(call template,write_btor_pmux,write_btor_pmux))
 $(eval $(call template,write_btor_and_or,write_btor_and_or))
 $(eval $(call template,write_btor_shiftx,write_btor write_btor_v write_btor_s))
+$(eval $(call template,write_btor_error, write_btor_no_top_module write_btor_unsupported_cell_type))
 
 #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_error, write_edif_cyclic_dependency write_edif_constant_nodes write_edif_unmapped_mem write_edif_unmapped_proc write_edif_no_module_found ))
 
 #write_firrtl
 $(eval $(call template,write_firrtl,write_firrtl))
-#write_firrtl_mem_wr - issue #938
-#terminate called after throwing an instance of 'std::out_of_range'
-#  what():  dict::at()
-#run.sh: line 11:  9808 Aborted                 (core dumped)
-$(eval $(call template,write_firrtl_mem,write_firrtl_mem ))
+$(eval $(call template,write_firrtl_mem,write_firrtl_mem write_firrtl_mem_wr))
 $(eval $(call template,write_firrtl_logic,write_firrtl ))
 $(eval $(call template,write_firrtl_reduce,write_firrtl ))
 $(eval $(call template,write_firrtl_shift,write_firrtl ))
 $(eval $(call template,write_firrtl_shiftx,write_firrtl ))
 $(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
 $(eval $(call template,write_ilang,write_ilang write_ilang_selected))
@@ -56,26 +57,31 @@ $(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_fsm,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
 $(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
 $(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
 $(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_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
 $(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_logic,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_mem,write_smt2 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_mem_memtest write_smt2_memtest write_smt2_stbv_memtest))
+$(eval $(call template,write_smt2_mem,write_smt2 write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_mem_memtest write_smt2_memtest write_smt2_stbv_memtest))
 $(eval $(call template,write_smt2_fsm,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
 $(eval $(call template,write_smt2_init_assert,write_smt2_init_assert))
 $(eval $(call template,write_smt2_reduce,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
 $(eval $(call template,write_smt2_shiftx,write_smt2 write_smt2_synth write_smt2_verbose write_smt2_stbv write_smt2_stdt write_smt2_nomem write_smt2_wires write_smt2_tpl write_smt2_bv write_smt2_mem write_smt2_nobv))
+$(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
 $(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
 $(eval $(call template,write_smv_init_assert,write_smv_init_assert))
 $(eval $(call template,write_smv_cmos4,write_smv_cmos4))
 $(eval $(call template,write_smv_shiftx,write_smv write_smv_synth write_smv_noproc write_smv_verbose write_smv_tpl))
+$(eval $(call template,write_smv_error,write_smv_cant_open_template write_smv_unsupported_cell))
 
 #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_error, write_spice_cant_find_top_module write_spice_unmapped_mem write_spice_unmapped_proc))
 
 #write_table
 $(eval $(call template,write_table,write_table ))

backends/run.sh

@@ -10,34 +10,126 @@ cd $1/work_$2
 
 touch .start
 
-yosys -ql yosys.log ../../scripts/$2.ys
-if [ $? != 0 ] ; then
+# cases where 'syntax error' or other errors are expected
+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_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
 		touch .stamp
 		exit 0
-fi
-sed -i 's/reg =/dummy =/' ./synth.v
+	fi
+	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
-else
+	else
 		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
-if [ $? != 0 ] ; then
+	iverilog -o testbench  ../testbench.v synth.v ../../common.v $COMMON_PREFIX/simcells.v $COMMON_PREFIX/simlib.v
+	if [ $? != 0 ] ; then
 		echo FAIL > ${1}_${2}.status
 		touch .stamp
 		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
 		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
-else
+	else
 		echo PASS > ${1}_${2}.status
+	fi
+
 fi
 
 touch .stamp

backends/scripts/write_aiger_cant_find_top_module.ys

+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

+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

+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

+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

+read_verilog -sv ../top.v
+proc
+write_blif -top u blif1.blif

backends/scripts/write_blif_unmapped_mem.ys

+read_verilog -sv ../top2.v
+proc
+write_blif -top u blif1.blif

backends/scripts/write_blif_unmapped_proc.ys

+read_verilog -sv ../top.v
+write_blif blif1.blif

backends/scripts/write_btor.ys

@@ -8,6 +8,7 @@ synth -top top
 write_btor btor1.btor
 design -reset
 read_verilog -sv ../top.v
+proc_prune
 proc_init
 proc_mux
 proc_dff

backends/scripts/write_btor_no_top_module.ys

+read_verilog ../top3.v
+memory
+proc
+write_btor btor.btor

backends/scripts/write_btor_s.ys

@@ -7,6 +7,7 @@ synth -top top
 write_btor -s btor1.btor
 design -reset
 read_verilog -sv ../top.v
+proc_prune
 proc_init
 proc_mux
 proc_dff

backends/scripts/write_btor_unsupported_cell_type.ys

+read_verilog ../top3.v
+synth_ice40
+write_btor btor.btor

backends/scripts/write_btor_v.ys

@@ -7,6 +7,7 @@ synth -top top
 write_btor -v btor1.btor
 design -reset
 read_verilog -sv ../top.v
+proc_prune
 proc_init
 proc_mux
 proc_dff

backends/scripts/write_edif_constant_nodes.ys

+read_verilog -sv ../top3.v
+proc
+write_edif -nogndvcc blif1.blif

backends/scripts/write_edif_cyclic_dependency.ys

+read_verilog -sv ../top4.v
+proc
+write_edif blif1.blif

backends/scripts/write_edif_no_module_found.ys

+write_edif edif.edif
+write_verilog synth.v

backends/scripts/write_edif_unmapped_mem.ys

+read_verilog ../top2.v
+proc
+write_edif -top top edif.edif
+write_verilog synth.v

backends/scripts/write_edif_unmapped_proc.ys

+read_verilog ../top.v
+write_edif -top top edif.edif
+write_verilog synth.v

backends/scripts/write_firrtl_complex_write_enable.ys

+read_verilog ../top1.v
+proc
+memory
+write_firrtl firrtl.firrtl
+write_verilog synth.v

backends/scripts/write_firrtl_fully_selected.ys

+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

+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
 proc
 memory_dff -nordff
+memory_collect
 opt_reduce
 clean
 write_firrtl firrtl.firrtl

backends/scripts/write_firrtl_negative_edge_ff.ys

+read_verilog ../top3.v
+proc
+write_firrtl firrtl.firrtl
+write_verilog synth.v

backends/scripts/write_firrtl_unclocked_write_port.ys

+read_verilog ../top.v
+
+memory
+proc
+write_firrtl firrtl.firrtl
+write_verilog synth.v

backends/scripts/write_ilang_error.ys

+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

+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

+read_verilog ../top.v
+proc
+write_intersynth -lib u intersynth.intersynth
+write_verilog synth.v

backends/scripts/write_intersynth_unprocessed_proc.ys

+read_verilog ../top.v
+write_intersynth intersynth.intersynth
+write_verilog synth.v

backends/scripts/write_json_error.ys

+read_verilog ../top.v
+proc
+json -o tt/json.json
+write_verilog synth.v

backends/scripts/write_simplec_no_c_model.ys

+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

+read_verilog ../top.v
+write_simplec c.c
+write_verilog synth.v

backends/scripts/write_smt2_cant_open_tpl.ys

+read_verilog ../top.v
+proc
+memory
+write_smt2 -tpl u smt2.smt2
+write_verilog synth.v

backends/scripts/write_smt2_cyclic_dependency.ys

+read_verilog ../top3.v
+proc
+memory
+write_smt2 smt2.smt2
+write_verilog synth.v

backends/scripts/write_smt2_logic_loop.ys

+read_verilog ../top1.v
+proc
+memory
+write_smt2 smt2.smt2
+write_verilog synth.v

backends/scripts/write_smt2_multiple_drivers.ys

+read_verilog ../top2.v
+proc
+memory
+write_smt2 smt2.smt2
+write_verilog synth.v

backends/scripts/write_smv_cant_open_template.ys

+read_verilog ../top.v
+proc
+memory
+write_smv -tpl t smv.smv
+write_verilog synth.v

backends/scripts/write_smv_unsupported_cell.ys

+read_verilog ../top.v
+proc
+memory
+write_smv smv.smv
+write_verilog synth.v

backends/scripts/write_spice_cant_find_top_module.ys

+read_verilog ../top.v
+proc
+memory
+write_spice -top u sp.sp
+write_verilog synth.v

backends/scripts/write_spice_unmapped_mem.ys

+read_verilog ../top.v
+proc
+write_spice sp.sp
+write_verilog synth.v

backends/scripts/write_spice_unmapped_proc.ys

+read_verilog ../top.v
+write_spice sp.sp
+write_verilog synth.v

backends/write_aiger_error/testbench.v

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+(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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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

+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								 

equiv/Makefile

@@ -20,6 +20,8 @@ endef
 #equiv_make
 $(eval $(call template,equiv_make,equiv_make equiv_make_inames equiv_make_blacklist equiv_make_encfile))
 $(eval $(call template,equiv_make_fsm,equiv_make_encfile equiv_make_encfile_fsm))
+$(eval $(call template,equiv_make_error,equiv_make_synth_error equiv_make_cant_open_encfile equiv_make_cant_open_blacklist equiv_make_cant_find_gate_mod equiv_make_cant_find_gold_mod equiv_make_invalid_num_of_args equiv_make_cant_match equiv_make_cant_match_gold_to_gate equiv_make_equiv_mod_already_exists equiv_make_gold_mod_contains_proc equiv_make_gate_mod_contains_proc))
+$(eval $(call template,equiv_make_fsm_error,equiv_make_redefenition_of_signal))
 
 #equiv_simple
 $(eval $(call template,equiv_simple,equiv_simple equiv_simple_v equiv_simple_undef equiv_simple_short equiv_simple_seq equiv_simple_nogroup))
@@ -27,18 +29,22 @@ $(eval $(call template,equiv_simple_fsm,equiv_simple equiv_simple_v equiv_simple
 
 #equiv_status
 $(eval $(call template,equiv_status,equiv_status))
+$(eval $(call template,equiv_status_error,equiv_status_assert))
 
 #equiv_struct
 $(eval $(call template,equiv_struct,equiv_struct equiv_struct_fwd equiv_struct_fwonly equiv_struct_icells equiv_struct_maxiter))
 
 #equiv_remove
 $(eval $(call template,equiv_remove,equiv_remove equiv_remove_gold equiv_remove_gate ))
+$(eval $(call template,equiv_remove_error,equiv_remove_gold_gate ))
 
 #equiv_purge
 $(eval $(call template,equiv_purge,equiv_purge ))
 
 #equiv_miter
+#equiv_miter_invalid_num_of_args - no error
 $(eval $(call template,equiv_miter,equiv_miter equiv_miter_trigger equiv_miter_cmp equiv_miter_assert equiv_miter_undef))
+$(eval $(call template,equiv_miter_error,equiv_miter_miter_module_already_exists equiv_miter_one_module_must_be_selected))
 
 #equiv_mark
 $(eval $(call template,equiv_mark,equiv_mark ))
@@ -48,8 +54,12 @@ $(eval $(call template,equiv_induct,equiv_induct equiv_induct_undef equiv_induct
 
 #equiv_add
 $(eval $(call template,equiv_add,equiv_add equiv_add_try ))
+# ERROR: This command must be executed in module context!
+#equiv_add_cant_find_gold_cell equiv_add_cant_find_gate_cell equiv_add_invalid_number_of_args
+$(eval $(call template,equiv_add_error,equiv_add_module_context ))
 
 #equiv_opt
 $(eval $(call template,equiv_opt,equiv_opt equiv_opt_run equiv_opt_map))
+$(eval $(call template,equiv_opt_error,equiv_opt_unknown_option equiv_opt_no_opt equiv_opt_fully_selected_des))
 
 .PHONY: all clean

equiv/equiv_add_error/logic.v

+
+`timescale 1ns/10ps
+`celldefine
+module NOR2_X0X2 (A, B, Y);
+input  A ;
+input  B ;
+output Y ;
+wire I0_out;
+
+   or  (I0_out, A, B);
+   not (Y, I0_out);
+
+endmodule
+`endcelldefine
+
+
+`timescale 1ns/10ps
+`celldefine
+module DFFARAS_X2X2(Q,QN,D,CLK,SN,RN);
+
+input D,CLK,SN,RN;
+output Q,QN;
+reg Q,QN;
+
+
+always @ (posedge CLK or negedge RN or negedge SN)
+
+begin
+if (!RN) begin
+Q<=1'b0; 
+QN<=1'b1;
+end
+else if (!SN) begin
+Q<=1'b1;
+QN<=1'b0;
+end
+else begin 
+Q<=D;
+QN<=!D;
+end
+end
+endmodule
+`endcelldefine
+
+
+`timescale 1ns/10ps
+`celldefine
+module TIEHL (tiehi, tielo);
+output  tiehi ;
+output  tielo ;
+
+assign tiehi = 1'b1;
+assign tielo = 1'b0;
+endmodule
+`endcelldefine
+
+`timescale 1ns/10ps
+`celldefine
+
+module INV_X2X2 (A, Y);
+input  A ;
+output Y ;
+
+   not (Y, A);
+/*
+   specify
+     // delay parameters
+     specparam
+       tplhl$A$Y = 0.23:0.23:0.23,
+       tphlh$A$Y = 0.33:0.33:0.33;
+
+     // path delays
+     (A *> Y) = (tphlh$A$Y, tplhl$A$Y);
+
+   endspecify
+*/
+endmodule
+`endcelldefine

equiv/equiv_add_error/synth_top.v

+/* Generated by Yosys 0.7 (git sha1 UNKNOWN, clang 3.4.2 -fPIC -Os) */
+
+(* src = "top.v:1" *)
+module top(clk, rst, count);
+  (* src = "top.v:3" *)
+  wire _0_;
+  wire _1_;
+  wire _2_;
+  (* src = "top.v:1" *)
+  input clk;
+  (* src = "top.v:1" *)
+  output count;
+  (* src = "top.v:1" *)
+  input rst;
+  INV_X2X2 _3_ (
+    .A(rst),
+    .Y(_1_)
+  );
+  TIEHL _4_ (
+    .tiehi(_2_)
+  );
+  DFFARAS_X2X2 _5_ (
+    .CLK(clk),
+    .D(_0_),
+    .Q(count),
+    .QN(_0_),
+    .RN(_1_),
+    .SN(_2_)
+  );
+endmodule

equiv/equiv_add_error/testbench.v

+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 rst;
+    wire f;
+
+    top uut ( .clk(clk),
+              .rst(rst),
+              .count(f));
+
+    initial begin
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+
+
+	assert_expr f_test(.clk(clk), .A(f));
+
+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

equiv/equiv_add_error/top.v

+module top(input wire clk,rst,output reg count);
+
+always @(posedge clk or posedge rst)begin
+	if(rst)
+		count <= 0;
+	else
+		count <= count + 1'b1;
+end
+
+endmodule

equiv/equiv_make_error/blacklist.txt

+NOR2_X0X2

equiv/equiv_make_error/encfile_redef.fsm

+.fsm FSM st
+.map 0000 -------------1
+.map 1000 ------------1-
+.map 1010 ------------1-
+.map 1010 -------------1
+.map 0100 -----------1--
+.map 1100 ----------1---
+.map 0010 ---------1----
+.map 1010 --------1-----
+.map 0110 -------1------
+.map 0001 ------1-------
+.map 1001 -----1--------
+.map 0101 ----1---------
+.map 1101 ---1----------
+.map 0011 --1-----------
+.map 1011 -1------------
+.map 0111 1-------------
+.map 1000 1-----1-------

equiv/equiv_make_error/encfile_synth_error.fsm

+.fsm FSM st
+.map 0000 -------------1
+.map 1000 ------------1-
+.maap 0100 -----------1--
+.map 1100 ----------1---
+.map 0010 ---------1----
+.map 1010 --------1-----
+.map 0110 -------1------
+.map 0001 ------1-------
+.map 1001 -----1--------
+.map 0101 ----1---------
+.map 1101 ---1----------
+.map 0011 --1-----------
+.map 1011 -1------------
+.map 0111 1-------------

equiv/equiv_make_error/logic.v

+
+`timescale 1ns/10ps
+`celldefine
+module NOR2_X0X2 (A, B, Y);
+input  A ;
+input  B ;
+output Y ;
+wire I0_out;
+
+   or  (I0_out, A, B);
+   not (Y, I0_out);
+
+endmodule
+`endcelldefine
+
+
+`timescale 1ns/10ps
+`celldefine
+module DFFARAS_X2X2(Q,QN,D,CLK,SN,RN);
+
+input D,CLK,SN,RN;
+output Q,QN;
+reg Q,QN;
+
+
+always @ (posedge CLK or negedge RN or negedge SN)
+
+begin
+if (!RN) begin
+Q<=1'b0; 
+QN<=1'b1;
+end
+else if (!SN) begin
+Q<=1'b1;
+QN<=1'b0;
+end
+else begin 
+Q<=D;
+QN<=!D;
+end
+end
+endmodule
+`endcelldefine
+
+
+`timescale 1ns/10ps
+`celldefine
+module TIEHL (tiehi, tielo);
+output  tiehi ;
+output  tielo ;
+
+assign tiehi = 1'b1;
+assign tielo = 1'b0;
+endmodule
+`endcelldefine
+
+`timescale 1ns/10ps
+`celldefine
+
+module INV_X2X2 (A, Y);
+input  A ;
+output Y ;
+
+   not (Y, A);
+/*
+   specify
+     // delay parameters
+     specparam
+       tplhl$A$Y = 0.23:0.23:0.23,
+       tphlh$A$Y = 0.33:0.33:0.33;
+
+     // path delays
+     (A *> Y) = (tphlh$A$Y, tplhl$A$Y);
+
+   endspecify
+*/
+endmodule
+`endcelldefine

equiv/equiv_make_error/synth_top.v

+/* Generated by Yosys 0.7 (git sha1 UNKNOWN, clang 3.4.2 -fPIC -Os) */
+
+(* src = "top.v:1" *)
+module top(clk, rst, count);
+  (* src = "top.v:3" *)
+  wire _0_;
+  wire _1_;
+  wire _2_;
+  (* src = "top.v:1" *)
+  input clk;
+  (* src = "top.v:1" *)
+  output count;
+  (* src = "top.v:1" *)
+  input rst;
+  INV_X2X2 _3_ (
+    .A(rst),
+    .Y(_1_)
+  );
+  TIEHL _4_ (
+    .tiehi(_2_)
+  );
+  DFFARAS_X2X2 _5_ (
+    .CLK(clk),
+    .D(_0_),
+    .Q(count),
+    .QN(_0_),
+    .RN(_1_),
+    .SN(_2_)
+  );
+endmodule

equiv/equiv_make_error/testbench.v

+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 rst;
+    wire f;
+
+    top uut ( .clk(clk),
+              .rst(rst),
+              .count(f));
+
+    initial begin
+        rst <= 1;
+        #5
+        rst <= 0;
+    end
+
+
+	assert_expr f_test(.clk(clk), .A(f));
+
+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

equiv/equiv_make_error/top.v

+module top(input wire clk,rst,output reg count);
+
+always @(posedge clk or posedge rst)begin
+	if(rst)
+		count <= 0;
+	else
+		count <= count + 1'b1;
+end
+
+endmodule

equiv/equiv_make_error/top1.v

+module top(input wire clk,output reg count);
+
+always @(posedge clk)begin
+	count <= count + 1'b1;
+end
+
+endmodule

equiv/equiv_make_error/top2.v

+module top(input wire clk,rst,set,output reg count);
+
+always @(posedge clk or posedge rst)begin
+	if(rst)
+		count <= 0;
+	else
+		count <= count + 1'b1;
+end
+
+endmodule

equiv/equiv_make_fsm_error/blacklist.txt

+NOR2_X0X2

equiv/equiv_make_fsm_error/encfile.fsm

+.fsm FSM st
+.map 0000 -------------1
+.map 1000 ------------1-
+.map 1010 ------------1-
+.map 1010 -------------1
+.map 0100 -----------1--
+.map 1100 ----------1---
+.map 0010 ---------1----
+.map 1010 --------1-----
+.map 0110 -------1------
+.map 0001 ------1-------
+.map 1001 -----1--------
+.map 0101 ----1---------
+.map 1101 ---1----------
+.map 0011 --1-----------
+.map 1011 -1------------
+.map 0111 1-------------
+.map 1000 1-----1-------

equiv/equiv_make_fsm_error/encfile_redef.fsm

+.fsm FSM st
+.map 0000 -------------1
+.map 1000 ------------1-
+.map 1010 ------------1-
+.map 1010 -------------1
+.map 0100 -----------1--
+.map 1100 ----------1---
+.map 0010 ---------1----
+.map 1010 --------1-----
+.map 0110 -------1------
+.map 0001 ------1-------
+.map 1001 -----1--------
+.map 0101 ----1---------
+.map 1101 ---1----------
+.map 0011 --1-----------
+.map 1011 -1------------
+.map 0111 1-------------
+.map 1000 1-----1-------

equiv/equiv_make_fsm_error/logic.v

+module \$fsm (CLK, ARST, CTRL_IN, CTRL_OUT);
+
+parameter NAME = "";
+
+parameter CLK_POLARITY = 1'b1;
+parameter ARST_POLARITY = 1'b1;
+
+parameter CTRL_IN_WIDTH = 1;
+parameter CTRL_OUT_WIDTH = 1;
+
+parameter STATE_BITS = 1;
+parameter STATE_NUM = 1;
+parameter STATE_NUM_LOG2 = 1;
+parameter STATE_RST = 0;
+parameter STATE_TABLE = 1'b0;
+
+parameter TRANS_NUM = 1;
+parameter TRANS_TABLE = 4'b0x0x;
+
+input CLK, ARST;
+input [CTRL_IN_WIDTH-1:0] CTRL_IN;
+output reg [CTRL_OUT_WIDTH-1:0] CTRL_OUT;
+
+wire pos_clk = CLK == CLK_POLARITY;
+wire pos_arst = ARST == ARST_POLARITY;
+
+reg [STATE_BITS-1:0] state;
+reg [STATE_BITS-1:0] state_tmp;
+reg [STATE_BITS-1:0] next_state;
+
+reg [STATE_BITS-1:0] tr_state_in;
+reg [STATE_BITS-1:0] tr_state_out;
+reg [CTRL_IN_WIDTH-1:0] tr_ctrl_in;
+reg [CTRL_OUT_WIDTH-1:0] tr_ctrl_out;
+
+integer i;
+
+task tr_fetch;
+	input [31:0] tr_num;
+	reg [31:0] tr_pos;
+	reg [STATE_NUM_LOG2-1:0] state_num;
+	begin
+		tr_pos = (2*STATE_NUM_LOG2+CTRL_IN_WIDTH+CTRL_OUT_WIDTH)*tr_num;
+		tr_ctrl_out = TRANS_TABLE >> tr_pos;
+		tr_pos = tr_pos + CTRL_OUT_WIDTH;
+		state_num = TRANS_TABLE >> tr_pos;
+		tr_state_out = STATE_TABLE >> (STATE_BITS*state_num);
+		tr_pos = tr_pos + STATE_NUM_LOG2;
+		tr_ctrl_in = TRANS_TABLE >> tr_pos;
+		tr_pos = tr_pos + CTRL_IN_WIDTH;
+		state_num = TRANS_TABLE >> tr_pos;
+		tr_state_in = STATE_TABLE >> (STATE_BITS*state_num);
+		tr_pos = tr_pos + STATE_NUM_LOG2;
+	end
+endtask
+/*
+
+always @(posedge pos_clk, posedge pos_arst) begin
+	if (pos_arst) begin
+		state_tmp = STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
+		for (i = 0; i < STATE_BITS; i = i+1)
+			if (state_tmp[i] === 1'bz)
+				state_tmp[i] = 0;
+		state <= state_tmp;
+	end else begin
+		state_tmp = next_state;
+		for (i = 0; i < STATE_BITS; i = i+1)
+			if (state_tmp[i] === 1'bz)
+				state_tmp[i] = 0;
+		state <= state_tmp;
+	end
+end
+
+always @(state, CTRL_IN) begin
+	next_state <= STATE_TABLE[STATE_BITS*(STATE_RST+1)-1:STATE_BITS*STATE_RST];
+	CTRL_OUT <= 'bx;
+	// $display("---");
+	// $display("Q: %b %b", state, CTRL_IN);
+	for (i = 0; i < TRANS_NUM; i = i+1) begin
+		tr_fetch(i);
+		// $display("T: %b %b -> %b %b [%d]", tr_state_in, tr_ctrl_in, tr_state_out, tr_ctrl_out, i);
+		casez ({state, CTRL_IN})
+			{tr_state_in, tr_ctrl_in}: begin
+				// $display("-> %b %b <-   MATCH", state, CTRL_IN);
+				{next_state, CTRL_OUT} <= {tr_state_out, tr_ctrl_out};
+			end
+		endcase
+	end
+end
+*/
+endmodule

equiv/equiv_make_fsm_error/synth_top.v

+/* Generated by Yosys 0.8+96 (git sha1 2d73e1b6, gcc 8.2.0-7ubuntu1 -Og -fPIC) */
+
+(* cells_not_processed =  1  *)
+(* src = "top.v:1" *)
+module FSM(clk, rst, en, ls, rs, stop, busy, finish);
+  (* src = "top.v:71" *)
+  wire [2:0] _00_;
+  (* src = "top.v:19" *)
+  (* unused_bits = "0 1 2 3" *)
+  wire [3:0] _01_;
+  (* src = "top.v:80" *)
+  wire [31:0] _02_;
+  (* src = "top.v:43" *)
+  wire _03_;
+  (* src = "top.v:76" *)
+  wire _04_;
+  (* src = "top.v:85" *)
+  wire _05_;
+  (* src = "top.v:85" *)
+  wire _06_;
+  (* src = "top.v:87" *)
+  wire _07_;
+  (* src = "top.v:89" *)
+  wire _08_;
+  (* src = "top.v:89" *)
+  wire _09_;
+  (* src = "top.v:39" *)
+  wire _10_;
+  (* src = "top.v:53" *)
+  wire _11_;
+  (* src = "top.v:60" *)
+  wire _12_;
+  (* src = "top.v:85" *)
+  wire _13_;
+  (* src = "top.v:89" *)
+  wire _14_;
+  wire [2:0] _15_;
+  wire [2:0] _16_;
+  (* unused_bits = "0" *)
+  wire _17_;
+  (* unused_bits = "0" *)
+  wire _18_;
+  (* unused_bits = "0" *)
+  wire _19_;
+  (* unused_bits = "0" *)
+  wire _20_;
+  (* unused_bits = "0" *)
+  wire _21_;
+  (* unused_bits = "0" *)
+  wire _22_;
+  (* unused_bits = "0" *)
+  wire _23_;
+  (* unused_bits = "0" *)
+  wire _24_;
+  (* unused_bits = "0" *)
+  wire _25_;
+  (* unused_bits = "0" *)
+  wire _26_;
+  (* unused_bits = "0" *)
+  wire _27_;
+  (* unused_bits = "0" *)
+  wire _28_;
+  (* unused_bits = "0" *)
+  wire _29_;
+  (* unused_bits = "0" *)
+  wire _30_;
+  (* unused_bits = "0" *)
+  wire _31_;
+  (* unused_bits = "0" *)
+  wire _32_;
+  (* unused_bits = "0" *)
+  wire _33_;
+  (* unused_bits = "0" *)
+  wire _34_;
+  (* unused_bits = "0" *)
+  wire _35_;
+  (* unused_bits = "0" *)
+  wire _36_;
+  (* src = "top.v:9" *)
+  output busy;
+  (* src = "top.v:2" *)
+  input clk;
+  (* src = "top.v:16" *)
+  reg [2:0] count;
+  (* src = "top.v:4" *)
+  input en;
+  (* src = "top.v:10" *)
+  output finish;
+  (* src = "top.v:5" *)
+  input ls;
+  (* src = "top.v:6" *)
+  input rs;
+  (* src = "top.v:3" *)
+  input rst;
+  (* src = "top.v:8" *)
+  output stop;
+  assign _02_ = count + (* src = "top.v:80" *) 32'd1;
+  assign _03_ = ~ (* src = "top.v:43" *) ls;
+  (* fsm_encoding = "auto" *)
+  (* src = "top.v:14" *)
+  \$fsm  #(
+    .ARST_POLARITY(1'h1),
+    .CLK_POLARITY(1'h1),
+    .CTRL_IN_WIDTH(32'd7),
+    .CTRL_OUT_WIDTH(32'd6),
+    .NAME("\\st"),
+    .STATE_BITS(32'd14),
+    .STATE_NUM(32'd14),
+    .STATE_NUM_LOG2(32'd4),
+    .STATE_RST(32'd0),
+    .STATE_TABLE(196'b1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1zzzzzzzzzzzzzz1),
+    .TRANS_NUM(32'd34),
+    .TRANS_TABLE(714'b1101zzz0z0z10100000001101zzz1z0z10010000001101zzzzz1z00000000001100zzzzz0z00110000001100zzzzz1z00000000001011zzzzz0z01110000011011zzzzz1z00000000011010zzzzz0z10101000001010zzzzz1z000010000010010zzzz0z101100000010011zzzz0z01100000001001zzzzz1z00000000001000zzzzz0z00010010001000zzzzz1z00000010000111zzzzz0z01000000000111zzzzz1z00000000000110zzzz10z11010000000110zzzz00z00010000000110zzzzz1z00000000000101zzzzz0111000000000101zzzzz0000100000000101zzzzz1z00000000000100zz1zz0z10110000000100zz0zz0z00100000000100zzzzz1z00000000000011zzzzz0z01010000100011zzzzz1z00000000100010z0zzz0z10010100000010z1zzz0z01010100000010zzzzz1z00000100000001zzzzz0z10000001000001zzzzz1z00000001000000zzzzz0z01110000000000zzzzz1z0000000000)
+  ) _39_ (
+    .ARST(1'h0),
+    .CLK(clk),
+    .CTRL_IN({ _03_, _10_, rs, _11_, ls, rst, _12_ }),
+    .CTRL_OUT({ _07_, _04_, _09_, _08_, _06_, _05_ })
+  );
+  assign _10_ = count > (* src = "top.v:39" *) 32'd7;
+  assign _11_ = ls && (* src = "top.v:53" *) rs;
+  assign _12_ = ls || (* src = "top.v:60" *) rs;
+  assign _13_ = _05_ || (* src = "top.v:85" *) _06_;
+  assign _14_ = _08_ || (* src = "top.v:89" *) _09_;
+  always @(posedge clk)
+      count <= _00_;
+  assign _15_ = _10_ ? (* src = "top.v:77" *) 3'h0 : _02_[2:0];
+  assign _16_ = _04_ ? (* src = "top.v:76" *) _15_ : count;
+  assign _00_ = rst ? (* src = "top.v:72" *) _16_ : 3'h0;
+  assign stop = _13_ ? (* src = "top.v:85" *) 1'h1 : 1'h0;
+  assign finish = _07_ ? (* src = "top.v:87" *) 1'h1 : 1'h0;
+  assign busy = _14_ ? (* src = "top.v:89" *) 1'h1 : 1'h0;
+endmodule
+
+(* cells_not_processed =  1  *)
+(* src = "top.v:94" *)
+module top(clk, rst, en, a, b, s, bs, f);
+  (* src = "top.v:98" *)
+  input a;
+  (* src = "top.v:99" *)
+  input b;
+  (* src = "top.v:101" *)
+  output bs;
+  (* src = "top.v:95" *)
+  input clk;
+  (* src = "top.v:97" *)
+  input en;
+  (* src = "top.v:102" *)
+  output f;
+  (* src = "top.v:96" *)
+  input rst;
+  (* src = "top.v:100" *)
+  output s;
+  (* module_not_derived = 32'd1 *)
+  (* src = "top.v:105" *)
+  FSM u_FSM (
+    .busy(bs),
+    .clk(clk),
+    .en(en),
+    .finish(f),
+    .ls(a),
+    .rs(b),
+    .rst(rst),
+    .stop(s)
+  );
+endmodule