Merge pull request #896 from diffblue/engine-heuristic

EBMC: basic engine selection heuristic

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$