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$