Split up formal ALU tests into smaller .sby files

configure.ac

@@ -276,7 +276,24 @@ fi
 
 AC_CONFIG_FILES([
 src/config.vh
-tests/alu.sby
+tests/alu_add.sby
+tests/alu_sub.sby
+tests/alu_xor.sby
+tests/alu_and.sby
+tests/alu_or.sby
+tests/alu_neg.sby
+tests/alu_cpl.sby
+tests/alu_sla.sby
+tests/alu_rl.sby
+tests/alu_srl.sby
+tests/alu_rr.sby
+tests/alu_sra.sby
+tests/alu_rlc.sby
+tests/alu_rrc.sby
+tests/alu_swap.sby
+tests/alu_set.sby
+tests/alu_res.sby
+tests/alu_bit.sby
 src/Makefile
 tests/Makefile
 sim/Makefile

tests/Makefile.am

@@ -1,5 +1,22 @@
 FORMAL_TESTS = \
-alu.sby
+alu_add.sby \
+alu_sub.sby \
+alu_xor.sby \
+alu_and.sby \
+alu_or.sby \
+alu_neg.sby \
+alu_cpl.sby \
+alu_sla.sby \
+alu_rl.sby \
+alu_srl.sby \
+alu_rr.sby \
+alu_sra.sby \
+alu_rlc.sby \
+alu_rrc.sby \
+alu_swap.sby \
+alu_set.sby \
+alu_res.sby \
+alu_bit.sby
 
 ALU_TESTS = \
 alu.svh \

tests/alu_add.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+add_bmc add bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+add_bmc: depth 128
+
+[engines]
+smtbmc
+
+[script]
+add: read_verilog -sv -formal alu_add.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+add: @srcdir@/alu_add.sv

tests/alu_and.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+and_bmc and bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+and_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+and: read_verilog -sv -formal alu_and.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+and: @srcdir@/alu_and.sv

tests/alu_bit.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+bit_bmc bit bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+bit_bmc: depth 128
+
+[engines]
+smtbmc
+
+[script]
+bit: read_verilog -sv -formal alu_bit.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+bit: @srcdir@/alu_bit.sv

tests/alu_cpl.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+cpl_bmc cpl bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+cpl_bmc: depth 88
+
+[engines]
+smtbmc
+
+[script]
+cpl: read_verilog -sv -formal alu_cpl.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+cpl: @srcdir@/alu_cpl.sv

tests/alu_neg.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+neg_bmc neg bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+neg_bmc: depth 88
+
+[engines]
+smtbmc
+
+[script]
+neg: read_verilog -sv -formal alu_neg.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+neg: @srcdir@/alu_neg.sv

tests/alu_or.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+or_bmc or bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+or_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+or: read_verilog -sv -formal alu_or.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+or: @srcdir@/alu_or.sv

tests/alu_res.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+res_bmc res bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+res_bmc: depth 128
+
+[engines]
+smtbmc
+
+[script]
+res: read_verilog -sv -formal alu_res.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+res: @srcdir@/alu_res.sv

tests/alu_rl.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+rl_bmc rl bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+rl_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+rl: read_verilog -sv -formal alu_rl.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+rl: @srcdir@/alu_rl.sv

tests/alu_rlc.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+rlc_bmc rlc bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+rlc_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+rlc: read_verilog -sv -formal alu_rlc.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+rlc: @srcdir@/alu_rlc.sv

tests/alu_rr.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+rr_bmc rr bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+rr_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+rr: read_verilog -sv -formal alu_rr.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+rr: @srcdir@/alu_rr.sv

tests/alu_rrc.sby.in

@@ -0,0 +1,22 @@
+[tasks]
+rrc_bmc rrc bmc
+
+[options]
+bmc: mode bmc
+append 10
+expect pass
+multiclock on
+rrc_bmc: depth 72
+
+[engines]
+smtbmc
+
+[script]
+rrc: read_verilog -sv -formal alu_rrc.sv sm83_alu.sv
+prep -top testbench
+assertpmux
+
+[files]
+@top_srcdir@/src/cpu/sm83_alu.sv
+@srcdir@/alu.svh
+rrc: @srcdir@/alu_rrc.sv