Merge pull request #55 from SergeyDegtyar/master

 Add new tests to makefile in 'backends' group.

backends/Makefile

@@ -21,6 +21,13 @@ endef
 $(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_xaiger
+$(eval $(call template,write_xaiger,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
+$(eval $(call template,write_xaiger_fsm,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
+$(eval $(call template,write_xaiger_mem,write_xaiger write_xaiger_ascii write_xaiger_map write_xaiger_vmap ))
+$(eval $(call template,write_xaiger_error, write_xaiger_cant_find_top_module write_xaiger_cant_open_file ))
+
 #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))
@@ -29,12 +36,14 @@ $(eval $(call template,write_blif_error, write_blif_unmapped_mem write_blif_cant
 $(eval $(call template,write_btor,write_btor write_btor_v write_btor_s))
 $(eval $(call template,write_btor_shift,write_btor write_btor_v write_btor_s))
 $(eval $(call template,write_btor_div_mod,write_btor write_btor_v write_btor_s))
-$(eval $(call template,write_btor_fsm,write_btor write_btor_v write_btor_s))
+$(eval $(call template,write_btor_fsm,write_btor write_btor_v write_btor_s write_btor_shift))
+$(eval $(call template,write_btor_shift_shiftx,write_btor_shift))
 $(eval $(call template,write_btor_logic,write_btor write_btor_v write_btor_s))
 $(eval $(call template,write_btor_mem,write_btor_mem write_btor_mem_v write_btor_mem_s))
 $(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_init_assert,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
@@ -43,6 +52,7 @@ $(eval $(call template,write_edif_error, write_edif_cyclic_dependency write_edif
 
 #write_firrtl
 $(eval $(call template,write_firrtl,write_firrtl))
+$(eval $(call template,write_firrtl_fsm,write_firrtl_fsm))
 $(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 ))
@@ -76,7 +86,7 @@ $(eval $(call template,write_simplec_error,write_simplec_no_c_model write_simple
 #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_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 write_smt2_anyseq))
 $(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))
@@ -103,12 +113,13 @@ $(eval $(call template,write_spice_error, write_spice_cant_find_top_module write
 $(eval $(call template,write_table,write_table ))
 
 #write_verilog
-$(eval $(call template,write_verilog,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v write_verilog_slice write_verilog_lut))
 $(eval $(call template,write_verilog_tri,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
 $(eval $(call template,write_verilog_ffs,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
 $(eval $(call template,write_verilog_latch,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
 $(eval $(call template,write_verilog_concat,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
 $(eval $(call template,write_verilog_shiftx,write_verilog write_verilog_nostr write_verilog_siminit write_verilog_v ))
+$(eval $(call template,write_verilog_shift_shiftx,write_verilog_shift ))
 
 
 

backends/run.sh

@@ -23,6 +23,10 @@ if echo "$1" | grep ".*_error"; 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_xaiger_cant_find_top_module" ]; then
+		expected_string="ERROR: Can't find top module in current design!"
+	elif [ "$2" = "write_xaiger_cant_open_file" ]; then
+		expected_string="ERROR: Can't open file "
 	elif [ "$2" = "write_blif_unmapped_mem" ]; then
 		expected_string="ERROR: Found unmapped memories in module "
 	elif [ "$2" = "write_blif_cant_find_top_module" ]; then
@@ -33,6 +37,8 @@ if echo "$1" | grep ".*_error"; 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

backends/write_btor_init_assert/top.v

@@ -29,8 +29,8 @@ always @(posedge x) begin
     assume(too);    
     assume(s_eventually too);
 end
-always @(negedge x) begin
-    if ($initstate) 
+always @(posedge x) begin
+    if ($initstate)
         cout <= 0;
         cout <=  y + A + foo;
     assert(ASSERT);