Merge pull request #896 from diffblue/engine-heuristic

EBMC: basic engine selection heuristic
diffblue · Jan 3, 2025 · bc38997 · bc38997
2 parents ed80f2e + 4b73053
commit bc38997
Show file tree

Hide file tree

Showing 184 changed files with 422 additions and 353 deletions.
diff --git a/CHANGELOG b/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

diff --git a/regression/ebmc/example1/test.desc b/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$
diff --git a/regression/smv/smv/bmc_unsupported_property1.desc b/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$

diff --git a/regression/smv/smv/bmc_unsupported_property2.desc b/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$

diff --git a/regression/verilog/SVA/immediate2.desc b/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$

diff --git a/regression/verilog/SVA/immediate3.desc b/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$
 --

diff --git a/regression/verilog/SVA/named_property1.desc b/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$
 --

diff --git a/regression/verilog/SVA/named_sequence1.desc b/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$
 --

diff --git a/regression/verilog/SVA/sequence5.desc b/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$

diff --git a/regression/verilog/SVA/sequence_first_match1.desc b/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$

diff --git a/regression/verilog/SVA/sequence_within1.desc b/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$

diff --git a/regression/verilog/SVA/static_final1.desc b/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$
 --

diff --git a/regression/verilog/SVA/sva_and1.desc b/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$

diff --git a/regression/verilog/SVA/sva_iff1.desc b/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$

diff --git a/regression/verilog/SVA/sva_implies1.desc b/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$

diff --git a/regression/verilog/SVA/sva_until1.desc b/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$

diff --git a/regression/verilog/SVA/system_verilog_assertion3.desc b/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$
 --

diff --git a/regression/verilog/UDPs/multiplexer1.desc b/regression/verilog/UDPs/multiplexer1.desc
@@ -1,6 +1,6 @@
 CORE
 multiplexer1.sv
---bound 0 --module main
+--module main
 ^no properties$
 ^EXIT=10$
 ^SIGNAL=0$

diff --git a/regression/verilog/arrays/array1.desc b/regression/verilog/arrays/array1.desc
@@ -1,6 +1,6 @@
 CORE
 array1.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/arrays/packed_real1.desc b/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$

diff --git a/regression/verilog/arrays/packed_typedef1.desc b/regression/verilog/arrays/packed_typedef1.desc
@@ -1,6 +1,6 @@
 CORE
 packed_typedef1.sv
---module main --bound 0
+--module main
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/assignments/procedural_assignments1.desc b/regression/verilog/assignments/procedural_assignments1.desc
@@ -1,6 +1,6 @@
 CORE
 procedural_assignments1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/case/nested_case1.desc b/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
diff --git a/regression/verilog/case/riscv-alu.desc b/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$
 --

diff --git a/regression/verilog/data-types/associative_array1.desc b/regression/verilog/data-types/associative_array1.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 associative_array1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/data-types/chandle1.desc b/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$
 --
diff --git a/regression/verilog/data-types/integer_atom_types1.desc b/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$
 --

diff --git a/regression/verilog/data-types/queue1.desc b/regression/verilog/data-types/queue1.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 queue1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/data-types/signed1.desc b/regression/verilog/data-types/signed1.desc
@@ -1,6 +1,6 @@
 CORE
 signed1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/data-types/signed2.desc b/regression/verilog/data-types/signed2.desc
@@ -1,6 +1,6 @@
 CORE
 signed2.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/data-types/type_operator.desc b/regression/verilog/data-types/type_operator.desc
@@ -1,6 +1,6 @@
 CORE
 type_operator.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/data-types/vector_types1.desc b/regression/verilog/data-types/vector_types1.desc
@@ -1,6 +1,6 @@
 CORE
 vector_types1.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/data-types/vector_types2.desc b/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$
 --
diff --git a/regression/verilog/elaboration/type_operator.desc b/regression/verilog/elaboration/type_operator.desc
@@ -1,6 +1,6 @@
 CORE
 type_operator.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/elaboration/var_bits.desc b/regression/verilog/elaboration/var_bits.desc
@@ -1,6 +1,6 @@
 CORE
 var_bits.sv
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/elaboration/wire_bits.desc b/regression/verilog/elaboration/wire_bits.desc
@@ -1,6 +1,6 @@
 CORE
 wire_bits.v
---bound 0
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

diff --git a/regression/verilog/enums/enum4.desc b/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$
 --
diff --git a/regression/verilog/enums/enum5.desc b/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$

diff --git a/regression/verilog/enums/enum_base_type1.desc b/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$
 --
diff --git a/regression/verilog/enums/enum_base_type2.desc b/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$
 --
diff --git a/regression/verilog/enums/enum_cast1.desc b/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$
 --
diff --git a/regression/verilog/enums/enum_initializers1.desc b/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$
 --