EBMC: basic engine selection heuristic

This adds a trivial engine selection heuristic, as follows:

1) First, try 1-induction, which may refute (base case) or prove (step case)
the property.

2) If still unresolved, try BMC with bound 5.

The heuristic is activated when no engine is specified on the command line.

Author: kroening

CHANGELOG

@@ -1,5 +1,7 @@
 # EBMC 5.5
 
+* If no engine is given, EBMC now selects an engine heuristically, instead
+  of doing BMC with k=1
 * Verilog: bugfix for $onehot0
 * Verilog: fix for primitive gates with more than two inputs
 * Verilog: Support $past when using AIG-based engines

regression/ebmc/example1/test.desc

@@ -1,6 +1,6 @@
 CORE
 example1.sv
---bound 10
-PROVED up to bound 10$
+
+^\[.*\] always 2'\(main\.a\) \+ main\.b == main\.result: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$

regression/smv/smv/bmc_unsupported_property1.desc

@@ -1,6 +1,6 @@
 CORE
 bmc_unsupported_property1.smv
-
+--bound 1
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$

regression/smv/smv/bmc_unsupported_property2.desc

@@ -1,6 +1,6 @@
 CORE
 bmc_unsupported_property2.smv
-
+--bound 1
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$

regression/verilog/SVA/immediate2.desc

@@ -1,8 +1,8 @@
 CORE
 immediate2.sv
---bound 0
+
 ^\[main\.assume\.1\] assume always 0: ASSUMED$
-^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
+^\[main\.assert\.2\] always main\.index < 10: PROVED$
 ^\[main\.assert\.3\] always 0: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/SVA/immediate3.desc

@@ -1,7 +1,7 @@
 CORE
 immediate3.sv
---bound 0
-^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/named_property1.desc

@@ -1,7 +1,7 @@
 CORE
 named_property1.sv
---bound 0
-^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
+
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/named_sequence1.desc

@@ -1,7 +1,7 @@
 CORE
 named_sequence1.sv
---bound 0
-^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 0$
+
+^\[main\.assert\.1\] always main\.x_is_ten: PROVED up to bound 5$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sequence5.desc

@@ -1,7 +1,7 @@
 CORE
 sequence5.sv
---bound 0
-^\[main\.p0\] 1: PROVED up to bound 0$
+
+^\[main\.p0\] 1: PROVED up to bound 5$
 ^\[main\.p1\] 0: REFUTED$
 ^\[main\.p2\] 1'bx: REFUTED$
 ^\[main\.p3\] 1'bz: REFUTED$

regression/verilog/SVA/sequence_first_match1.desc

@@ -1,6 +1,6 @@
 CORE
 sequence_first_match1.sv
-
+--bound 5
 ^\[.*\] first_match\(main\.x == 0\): FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/SVA/sequence_within1.desc

@@ -1,6 +1,6 @@
 CORE
 sequence_within1.sv
-
+--bound 5
 ^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/SVA/static_final1.desc

@@ -1,7 +1,7 @@
 CORE
 static_final1.sv
---bound 0
-^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+
+^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_and1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_and1.sv
---bound 0
-^\[main\.p0\] always \(1 and 1\): PROVED up to bound 0$
+
+^\[main\.p0\] always \(1 and 1\): PROVED$
 ^\[main\.p1\] always \(1 and 0\): REFUTED$
 ^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/SVA/sva_iff1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_iff1.sv
---bound 0
-^\[main\.p0\] always \(1 iff 1\): PROVED up to bound 0$
+
+^\[main\.p0\] always \(1 iff 1\): PROVED$
 ^\[main\.p1\] always \(1 iff 0\): REFUTED$
 ^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/SVA/sva_implies1.desc

@@ -1,7 +1,7 @@
 CORE
 sva_implies1.sv
---bound 0
-^\[main\.p0\] always \(1 implies 1\): PROVED up to bound 0$
+
+^\[main\.p0\] always \(1 implies 1\): PROVED$
 ^\[main\.p1\] always \(1 implies 0\): REFUTED$
 ^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$
 ^EXIT=10$

regression/verilog/SVA/sva_until1.desc

@@ -1,6 +1,6 @@
 CORE
 sva_until1.sv
---bound 1
+
 ^\[main\.p0\] always \(main.a until_with main.b\): REFUTED$
 ^\[main\.p1\] always \(main.a until main.b\): REFUTED$
 ^\[main\.p2\] always \(main.a s_until main.b\): REFUTED$

regression/verilog/SVA/system_verilog_assertion3.desc

@@ -1,6 +1,6 @@
 CORE
 system_verilog_assertion3.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/UDPs/multiplexer1.desc

@@ -1,6 +1,6 @@
 CORE
 multiplexer1.sv
---bound 0 --module main
+--module main
 ^no properties$
 ^EXIT=10$
 ^SIGNAL=0$

regression/verilog/arrays/array1.desc

@@ -1,6 +1,6 @@
 CORE
 array1.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/arrays/packed_real1.desc

@@ -1,6 +1,6 @@
 CORE
 packed_real1.sv
---module main --bound 0
+--module main
 ^file .* line 6: packed array must use packed element type$
 ^EXIT=2$
 ^SIGNAL=0$

regression/verilog/arrays/packed_typedef1.desc

@@ -1,6 +1,6 @@
 CORE
 packed_typedef1.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/assignments/procedural_assignments1.desc

@@ -1,6 +1,6 @@
 CORE
 procedural_assignments1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/case/nested_case1.desc

@@ -1,8 +1,8 @@
 CORE
 nested_case1.v
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.property.p1\] .* PROVED up to bound 0$
+^\[main.property.p1\] .* PROVED$
 --
 ^warning: ignoring

regression/verilog/case/riscv-alu.desc

@@ -1,16 +1,16 @@
 CORE
 riscv-alu.sv
---module alu --bound 0
-^\[alu\.pADD\] always alu\.op == \{ 7'b0000000, 3'b000 \} -> alu\.out == alu\.a \+ alu\.b: PROVED up to bound 0$
-^\[alu\.pSUB\] always alu\.op == \{ 7'b0100000, 3'b000 \} -> alu\.out == alu\.a - alu\.b: PROVED up to bound 0$
-^\[alu\.pSLL\] always alu\.op == \{ 7'b0000000, 3'b001 \} -> alu\.out == alu\.a << alu\.b\[4:0\]: PROVED up to bound 0$
-^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == \$signed\(alu\.a\) < \$signed\(alu\.b\): PROVED up to bound 0$
-^\[alu\.pSLTU\] always alu\.op == \{ 7'b0000000, 3'b011 \} -> alu\.out == alu\.a < alu\.b: PROVED up to bound 0$
-^\[alu\.pXOR\] always alu\.op == \{ 7'b0000000, 3'b100 \} -> alu\.out == \(alu\.a \^ alu\.b\): PROVED up to bound 0$
-^\[alu\.pSRL\] always alu\.op == \{ 7'b0000000, 3'b101 \} -> alu\.out == alu\.a >> alu\.b\[4:0\]: PROVED up to bound 0$
-^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == \$signed\(alu\.a\) >>> alu\.b\[4:0\]: PROVED up to bound 0$
-^\[alu\.pOR\] always alu\.op == \{ 7'b0000000, 3'b110 \} -> alu\.out == \(alu\.a | alu\.b\): PROVED up to bound 0$
-^\[alu\.pAND\] always alu\.op == \{ 7'b0000000, 3'b111 \} -> alu\.out == \(alu\.a & alu\.b\): PROVED up to bound 0$
+--module alu
+^\[alu\.pADD\] always alu\.op == \{ 7'b0000000, 3'b000 \} -> alu\.out == alu\.a \+ alu\.b: PROVED$
+^\[alu\.pSUB\] always alu\.op == \{ 7'b0100000, 3'b000 \} -> alu\.out == alu\.a - alu\.b: PROVED$
+^\[alu\.pSLL\] always alu\.op == \{ 7'b0000000, 3'b001 \} -> alu\.out == alu\.a << alu\.b\[4:0\]: PROVED$
+^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == \$signed\(alu\.a\) < \$signed\(alu\.b\): PROVED$
+^\[alu\.pSLTU\] always alu\.op == \{ 7'b0000000, 3'b011 \} -> alu\.out == alu\.a < alu\.b: PROVED$
+^\[alu\.pXOR\] always alu\.op == \{ 7'b0000000, 3'b100 \} -> alu\.out == \(alu\.a \^ alu\.b\): PROVED$
+^\[alu\.pSRL\] always alu\.op == \{ 7'b0000000, 3'b101 \} -> alu\.out == alu\.a >> alu\.b\[4:0\]: PROVED$
+^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == \$signed\(alu\.a\) >>> alu\.b\[4:0\]: PROVED$
+^\[alu\.pOR\] always alu\.op == \{ 7'b0000000, 3'b110 \} -> alu\.out == \(alu\.a | alu\.b\): PROVED$
+^\[alu\.pAND\] always alu\.op == \{ 7'b0000000, 3'b111 \} -> alu\.out == \(alu\.a & alu\.b\): PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/associative_array1.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 associative_array1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/chandle1.desc

@@ -1,8 +1,8 @@
 CORE
 chandle1.sv
---bound 0
-^\[main\.p0\] always main\.some_handle == null: PROVED up to bound 0$
-^\[main\.p1\] always \$typename\(main\.some_handle\) == "chandle": PROVED up to bound 0$
+
+^\[main\.p0\] always main\.some_handle == null: PROVED$
+^\[main\.p1\] always \$typename\(main\.some_handle\) == "chandle": PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/integer_atom_types1.desc

@@ -1,6 +1,6 @@
 CORE
 integer_atom_types1.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/queue1.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 queue1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/signed1.desc

@@ -1,6 +1,6 @@
 CORE
 signed1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/signed2.desc

@@ -1,6 +1,6 @@
 CORE
 signed2.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/type_operator.desc

@@ -1,6 +1,6 @@
 CORE
 type_operator.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/vector_types1.desc

@@ -1,6 +1,6 @@
 CORE
 vector_types1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/data-types/vector_types2.desc

@@ -1,7 +1,7 @@
 CORE
 vector_types2.sv
---bound 0
-^\[.*\] always \$bits\(main\.x\) == \(1 << main\.p\) \+ 1: PROVED up to bound 0$
+
+^\[.*\] always \$bits\(main\.x\) == \(1 << main\.p\) \+ 1: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/elaboration/type_operator.desc

@@ -1,6 +1,6 @@
 CORE
 type_operator.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/elaboration/var_bits.desc

@@ -1,6 +1,6 @@
 CORE
 var_bits.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/elaboration/wire_bits.desc

@@ -1,6 +1,6 @@
 CORE
 wire_bits.v
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/enums/enum4.desc

@@ -1,7 +1,7 @@
 CORE
 enum4.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main\.A == \[7:0\]'\(1\): PROVED up to bound 0$
+^\[main\.p1\] always main\.A == \[7:0\]'\(1\): PROVED$
 --

regression/verilog/enums/enum5.desc

@@ -1,6 +1,6 @@
 CORE
 enum5.sv
---bound 0
+
 ^file .* line 6: expected constant expression, but got `main\.some_wire'$
 ^EXIT=2$
 ^SIGNAL=0$

regression/verilog/enums/enum_base_type1.desc

@@ -1,7 +1,7 @@
 CORE
 enum_base_type1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \$bits\(main\.A\) == 8: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == 8: PROVED$
 --

regression/verilog/enums/enum_base_type2.desc

@@ -1,7 +1,7 @@
 CORE
 enum_base_type2.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED up to bound 0$
+^\[.*\] always \$bits\(main\.A\) == main\.p: PROVED$
 --

regression/verilog/enums/enum_cast1.desc

@@ -1,8 +1,8 @@
 CORE
 enum_cast1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main.A == signed \[31:0\]'\(1\): PROVED up to bound 0$
-^\[main\.p2\] always main.B == signed \[31:0\]'\(2\): PROVED up to bound 0$
+^\[main\.p1\] always main.A == signed \[31:0\]'\(1\): PROVED$
+^\[main\.p2\] always main.B == signed \[31:0\]'\(2\): PROVED$
 --

regression/verilog/enums/enum_initializers1.desc

@@ -1,8 +1,8 @@
 CORE
 enum_initializers1.sv
---bound 0
-^\[main\.pA\] always main.A == 1: PROVED up to bound 0$
-^\[main\.pB\] always main.B == 11: PROVED up to bound 0$
+
+^\[main\.pA\] always main.A == 1: PROVED$
+^\[main\.pB\] always main.B == 11: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --