diff --git a/CHANGELOG b/CHANGELOG index 6cabeda50..0f4f3e153 100644 --- 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 index dca6824b9..b7d5f7b13 100644 --- 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 index 0e6d424c9..075e96785 100644 --- 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 index 8680f5235..01a10d79c 100644 --- 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 index 56b14e1ff..0c429e7b3 100644 --- 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 index 8d5d8df0e..1179a40a5 100644 --- 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 index 09adbafda..5577d0b89 100644 --- 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 index 97b51302f..24a00cdac 100644 --- 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 index 90d633ca5..d4b5bc5fb 100644 --- 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 index 731f0ef5b..1ef10fc0d 100644 --- 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 index dc58d4062..60b676baa 100644 --- 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 index dea304e14..768df3e2e 100644 --- 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 index 36e6b99f8..2facd225b 100644 --- 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 index b61633d2a..ed75e00d7 100644 --- 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 index 412f331e0..53284a212 100644 --- 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 index 7c43408d0..a0fbae8b7 100644 --- 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 index 38ce84e04..8c95561f2 100644 --- 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 index 3efdf2eda..c191e8d1a 100644 --- 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 index 118f8da95..ae748955c 100644 --- 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 index d932815ca..8b882564b 100644 --- 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 index 4d08740e0..9ee438d1a 100644 --- 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 index b4a4aa9e2..8ae42578d 100644 --- 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 index 63cc96523..9a38264e2 100644 --- 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 index c7db48814..b88afd892 100644 --- 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 index 7c08b3c1a..a36a59960 100644 --- 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 index 97ea5bd82..a840983e1 100644 --- 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 index 8410a37f9..6c5ceea8b 100644 --- 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 index 24313e793..92e35926c 100644 --- 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 index 893d20965..7fa900ac6 100644 --- 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 index dac62393f..470f88d39 100644 --- 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 index 45cf876ca..f9c865be7 100644 --- 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 index e00678269..02b2de0c3 100644 --- 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 index 19095016a..acaf22221 100644 --- 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 index 45cf876ca..f9c865be7 100644 --- 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 index 5260668af..c096fd370 100644 --- 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 index 03dc2da1c..a6b01c614 100644 --- 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 index b9919492d..febeea473 100644 --- 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 index 89f0db6b6..9ee9d6ffa 100644 --- 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 index e06de749c..a766c9db6 100644 --- 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 index 25bb47977..8f0c073eb 100644 --- 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 index 5c0fc968e..2880369f7 100644 --- 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 index 77900bc5c..c3bc0081d 100644 --- 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$ -- diff --git a/regression/verilog/enums/enum_with_hierarchy1.desc b/regression/verilog/enums/enum_with_hierarchy1.desc index 0a2c043bc..5cc2d7c31 100644 --- a/regression/verilog/enums/enum_with_hierarchy1.desc +++ b/regression/verilog/enums/enum_with_hierarchy1.desc @@ -1,6 +1,6 @@ KNOWNBUG enum_with_hierarchy1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/bit-extract3.desc b/regression/verilog/expressions/bit-extract3.desc index e555d229d..408addae2 100644 --- a/regression/verilog/expressions/bit-extract3.desc +++ b/regression/verilog/expressions/bit-extract3.desc @@ -1,12 +1,12 @@ CORE bit-extract3.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property1\] .*: PROVED up to bound 0$ -^\[main\.property2\] .*: PROVED up to bound 0$ -^\[main\.property3\] .*: PROVED up to bound 0$ -^\[main\.property4\] .*: PROVED up to bound 0$ -^\[main\.property5\] .*: PROVED up to bound 0$ +^\[main\.property1\] .*: PROVED$ +^\[main\.property2\] .*: PROVED$ +^\[main\.property3\] .*: PROVED$ +^\[main\.property4\] .*: PROVED$ +^\[main\.property5\] .*: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/expressions/bit-extract4.desc b/regression/verilog/expressions/bit-extract4.desc index 9d2cd7d40..71960277b 100644 --- a/regression/verilog/expressions/bit-extract4.desc +++ b/regression/verilog/expressions/bit-extract4.desc @@ -1,6 +1,6 @@ CORE bit-extract4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/bit-extract5.desc b/regression/verilog/expressions/bit-extract5.desc index 2d9bb1845..1c1fb0a92 100644 --- a/regression/verilog/expressions/bit-extract5.desc +++ b/regression/verilog/expressions/bit-extract5.desc @@ -1,10 +1,10 @@ CORE bit-extract5.sv ---module main --bound 0 -^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED up to bound 0$ -^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED up to bound 0$ -^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED up to bound 0$ -^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED up to bound 0$ +--module main +^\[main\.p0\] always main\.w1\[0\] && !main\.w1\[31\]: PROVED$ +^\[main\.p1\] always main\.w2\[0\] && !main\.w2\[31\]: PROVED$ +^\[main\.p2\] always main\.w3\[0\] && !main\.w3\[31\]: PROVED$ +^\[main\.p3\] always main\.w4\[0\] && !main\.w4\[31\]: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/bit-extract6.desc b/regression/verilog/expressions/bit-extract6.desc index 7461c5d2c..3f83ddb7f 100644 --- a/regression/verilog/expressions/bit-extract6.desc +++ b/regression/verilog/expressions/bit-extract6.desc @@ -1,8 +1,8 @@ CORE bit-extract6.sv ---module main --bound 0 -^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED up to bound 0$ -^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED up to bound 0$ +--module main +^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED$ +^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/cast_from_real1.desc b/regression/verilog/expressions/cast_from_real1.desc index 685e4a115..d9a7c197c 100644 --- a/regression/verilog/expressions/cast_from_real1.desc +++ b/regression/verilog/expressions/cast_from_real1.desc @@ -1,6 +1,6 @@ KNOWNBUG cast_from_real1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/cast_to_real1.desc b/regression/verilog/expressions/cast_to_real1.desc index 546ca5099..0772e6f83 100644 --- a/regression/verilog/expressions/cast_to_real1.desc +++ b/regression/verilog/expressions/cast_to_real1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend cast_to_real1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/cast_to_real2.desc b/regression/verilog/expressions/cast_to_real2.desc index 62688441e..a27529d39 100644 --- a/regression/verilog/expressions/cast_to_real2.desc +++ b/regression/verilog/expressions/cast_to_real2.desc @@ -1,6 +1,6 @@ KNOWNBUG cast_to_real2.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/cast_to_real3.desc b/regression/verilog/expressions/cast_to_real3.desc index eba513385..b0a1fef69 100644 --- a/regression/verilog/expressions/cast_to_real3.desc +++ b/regression/verilog/expressions/cast_to_real3.desc @@ -1,6 +1,6 @@ KNOWNBUG cast_to_real3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/concatenation1.desc b/regression/verilog/expressions/concatenation1.desc index 44e0b6b9e..dfcfcf54a 100644 --- a/regression/verilog/expressions/concatenation1.desc +++ b/regression/verilog/expressions/concatenation1.desc @@ -1,6 +1,6 @@ CORE concatenation1.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/concatenation2.desc b/regression/verilog/expressions/concatenation2.desc index 54bdc6300..b3365b081 100644 --- a/regression/verilog/expressions/concatenation2.desc +++ b/regression/verilog/expressions/concatenation2.desc @@ -1,9 +1,9 @@ CORE concatenation2.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.pA\] always main\.A == -1: PROVED up to bound 0$ -^\[main\.property\.pB\] always main\.B == 15: PROVED up to bound 0$ +^\[main\.property\.pA\] always main\.A == -1: PROVED$ +^\[main\.property\.pB\] always main\.B == 15: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/expressions/concatenation3.desc b/regression/verilog/expressions/concatenation3.desc index 114a0a9b0..6dde1e1c3 100644 --- a/regression/verilog/expressions/concatenation3.desc +++ b/regression/verilog/expressions/concatenation3.desc @@ -1,8 +1,8 @@ CORE concatenation3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -^\[.*\] always \{ 5'bxz01\?, 4'b10zx \} === 9'bxz01\?10zx: PROVED up to bound 0$ +^\[.*\] always \{ 5'bxz01\?, 4'b10zx \} === 9'bxz01\?10zx: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/expressions/concatenation4.desc b/regression/verilog/expressions/concatenation4.desc index a0aec9491..b31ed524a 100644 --- a/regression/verilog/expressions/concatenation4.desc +++ b/regression/verilog/expressions/concatenation4.desc @@ -1,6 +1,6 @@ KNOWNBUG concatenation4.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/concatenation5.desc b/regression/verilog/expressions/concatenation5.desc index ec1e4ef33..1c6799eeb 100644 --- a/regression/verilog/expressions/concatenation5.desc +++ b/regression/verilog/expressions/concatenation5.desc @@ -1,6 +1,6 @@ CORE concatenation5.v ---bound 0 + ^file .* line 4: operand 1.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/concatenation6.desc b/regression/verilog/expressions/concatenation6.desc index 28ba6bfe8..22845f9f7 100644 --- a/regression/verilog/expressions/concatenation6.desc +++ b/regression/verilog/expressions/concatenation6.desc @@ -1,7 +1,7 @@ CORE concatenation6.sv ---bound 0 -^\[.*\] always main\.x == \{ 0, 1 \}: PROVED up to bound 0$ + +^\[.*\] always main\.x == \{ 0, 1 \}: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/constants2.desc b/regression/verilog/expressions/constants2.desc index 44dd1d18e..33bc0963a 100644 --- a/regression/verilog/expressions/constants2.desc +++ b/regression/verilog/expressions/constants2.desc @@ -1,6 +1,6 @@ CORE constants2.sv ---bound 0 + ^no properties$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/equality1.desc b/regression/verilog/expressions/equality1.desc index b9478a37a..ae31d7857 100644 --- a/regression/verilog/expressions/equality1.desc +++ b/regression/verilog/expressions/equality1.desc @@ -1,18 +1,18 @@ CORE broken-smt-backend equality1.v ---bound 0 -^\[.*\] always 10 == 10 === 1: PROVED up to bound 0$ -^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$ -^\[.*\] always 10 != 20 === 1: PROVED up to bound 0$ -^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$ -^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED up to bound 0$ -^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED up to bound 0$ -^\[.*\] always 1\.1 == 1\.1 == 1: PROVED up to bound 0$ -^\[.*\] always 1\.1 == 1 == 0: PROVED up to bound 0$ + +^\[.*\] always 10 == 10 === 1: PROVED$ +^\[.*\] always 10 == 20 === 0: PROVED$ +^\[.*\] always 10 != 20 === 1: PROVED$ +^\[.*\] always 10 == 20 === 0: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED$ +^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED$ +^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED$ +^\[.*\] always 1\.1 == 1\.1 == 1: PROVED$ +^\[.*\] always 1\.1 == 1 == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/equality2.desc b/regression/verilog/expressions/equality2.desc index f3db2490b..06b945da5 100644 --- a/regression/verilog/expressions/equality2.desc +++ b/regression/verilog/expressions/equality2.desc @@ -1,18 +1,18 @@ CORE equality2.v ---bound 0 -^\[.*\] always 10 === 10 == 1: PROVED up to bound 0$ -^\[.*\] always 10 === 20 == 0: PROVED up to bound 0$ -^\[.*\] always 10 !== 10 == 0: PROVED up to bound 0$ -^\[.*\] always 10 !== 20 == 1: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED up to bound 0$ -^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED up to bound 0$ -^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$ -^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED up to bound 0$ -^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED up to bound 0$ + +^\[.*\] always 10 === 10 == 1: PROVED$ +^\[.*\] always 10 === 20 == 0: PROVED$ +^\[.*\] always 10 !== 10 == 0: PROVED$ +^\[.*\] always 10 !== 20 == 1: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED$ +^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED$ +^\[.*\] always 1 === 1 == 1: PROVED$ +^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED$ +^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/equality3.desc b/regression/verilog/expressions/equality3.desc index e73073616..9b823fb06 100644 --- a/regression/verilog/expressions/equality3.desc +++ b/regression/verilog/expressions/equality3.desc @@ -1,6 +1,6 @@ CORE equality3.v ---bound 0 + ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/iff1.desc b/regression/verilog/expressions/iff1.desc index 4c90c997a..1b6dc3574 100644 --- a/regression/verilog/expressions/iff1.desc +++ b/regression/verilog/expressions/iff1.desc @@ -1,6 +1,6 @@ CORE iff1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/implies1.desc b/regression/verilog/expressions/implies1.desc index a4ebb2bc4..67c0a9eff 100644 --- a/regression/verilog/expressions/implies1.desc +++ b/regression/verilog/expressions/implies1.desc @@ -1,6 +1,6 @@ CORE implies1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/inside1.desc b/regression/verilog/expressions/inside1.desc index 790697973..2fcb31e5a 100644 --- a/regression/verilog/expressions/inside1.desc +++ b/regression/verilog/expressions/inside1.desc @@ -1,12 +1,12 @@ CORE broken-smt-backend inside1.sv ---bound 0 -^\[.*\] always 2 inside \{1, 2, 3\}: PROVED up to bound 0$ -^\[.*\] always 2 inside \{3'b0\?0\}: PROVED up to bound 0$ -^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED up to bound 0$ -^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED up to bound 0$ -^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED up to bound 0$ -^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED up to bound 0$ + +^\[.*\] always 2 inside \{1, 2, 3\}: PROVED$ +^\[.*\] always 2 inside \{3'b0\?0\}: PROVED$ +^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED$ +^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED$ +^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED$ +^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/mod2.desc b/regression/verilog/expressions/mod2.desc index 87d22d748..329be47ba 100644 --- a/regression/verilog/expressions/mod2.desc +++ b/regression/verilog/expressions/mod2.desc @@ -1,6 +1,6 @@ CORE mod2.v ---bound 0 + ^file .* line 4: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/negation1.desc b/regression/verilog/expressions/negation1.desc index 5592e7853..7563fc25a 100644 --- a/regression/verilog/expressions/negation1.desc +++ b/regression/verilog/expressions/negation1.desc @@ -1,6 +1,6 @@ CORE negation1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/part-select-constant1.desc b/regression/verilog/expressions/part-select-constant1.desc index 942379003..1508484de 100644 --- a/regression/verilog/expressions/part-select-constant1.desc +++ b/regression/verilog/expressions/part-select-constant1.desc @@ -1,7 +1,7 @@ CORE part-select-constant1.sv ---bound 0 -^\[.*\] .* PROVED up to bound 0$ + +^\[.*\] .* PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/power1.desc b/regression/verilog/expressions/power1.desc index c3a0d1fa7..3d7fea3b1 100644 --- a/regression/verilog/expressions/power1.desc +++ b/regression/verilog/expressions/power1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend power1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/power2.desc b/regression/verilog/expressions/power2.desc index f17da1400..c8eff8c8e 100644 --- a/regression/verilog/expressions/power2.desc +++ b/regression/verilog/expressions/power2.desc @@ -1,6 +1,6 @@ CORE power2.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/reduction1.desc b/regression/verilog/expressions/reduction1.desc index a6bca9ac8..e2232b34a 100644 --- a/regression/verilog/expressions/reduction1.desc +++ b/regression/verilog/expressions/reduction1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend reduction1.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/reduction2.desc b/regression/verilog/expressions/reduction2.desc index 46a884dd3..740909c3e 100644 --- a/regression/verilog/expressions/reduction2.desc +++ b/regression/verilog/expressions/reduction2.desc @@ -1,6 +1,6 @@ CORE reduction2.v ---bound 0 + ^file .* line 4: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/replication1.desc b/regression/verilog/expressions/replication1.desc index 364027370..1828bb661 100644 --- a/regression/verilog/expressions/replication1.desc +++ b/regression/verilog/expressions/replication1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend replication1.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/replication2.desc b/regression/verilog/expressions/replication2.desc index 95e4de9f4..2679fcd18 100644 --- a/regression/verilog/expressions/replication2.desc +++ b/regression/verilog/expressions/replication2.desc @@ -1,6 +1,6 @@ KNOWNBUG replication2.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/replication3.desc b/regression/verilog/expressions/replication3.desc index 73c59cd20..bdf6fde7e 100644 --- a/regression/verilog/expressions/replication3.desc +++ b/regression/verilog/expressions/replication3.desc @@ -1,6 +1,6 @@ CORE replication3.v ---bound 0 + ^file .* line 3: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/shr2.desc b/regression/verilog/expressions/shr2.desc index a83a5c432..e2957ddb1 100644 --- a/regression/verilog/expressions/shr2.desc +++ b/regression/verilog/expressions/shr2.desc @@ -1,6 +1,6 @@ CORE shr2.v ---bound 0 + ^file .* line 4: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/signed1.desc b/regression/verilog/expressions/signed1.desc index 0f529b156..119daeba5 100644 --- a/regression/verilog/expressions/signed1.desc +++ b/regression/verilog/expressions/signed1.desc @@ -1,14 +1,14 @@ CORE signed1.sv ---module main --bound 0 -^\[main\.p1\] always main\.wire1 == main.wire2: PROVED up to bound 0$ -^\[main\.p2\] always main\.wire1 >>> 1 == -1: PROVED up to bound 0$ -^\[main\.p3\] always main\.wire2 >> 1 != -1: PROVED up to bound 0$ -^\[main\.p4\] always main\.wire1\[31:0\] >> 1 != -1: PROVED up to bound 0$ -^\[main\.p5\] always \$unsigned\(main\.wire1\) >> 1 != -1: PROVED up to bound 0$ -^\[main\.p6\] always \$signed\(main\.wire2\) >>> 1 == -1: PROVED up to bound 0$ -^\[main\.p7\] always -1 >> 1 != -1: PROVED up to bound 0$ -^\[main\.p8\] always -1 >>> 1 == -1: PROVED up to bound 0$ +--module main +^\[main\.p1\] always main\.wire1 == main.wire2: PROVED$ +^\[main\.p2\] always main\.wire1 >>> 1 == -1: PROVED$ +^\[main\.p3\] always main\.wire2 >> 1 != -1: PROVED$ +^\[main\.p4\] always main\.wire1\[31:0\] >> 1 != -1: PROVED$ +^\[main\.p5\] always \$unsigned\(main\.wire1\) >> 1 != -1: PROVED$ +^\[main\.p6\] always \$signed\(main\.wire2\) >>> 1 == -1: PROVED$ +^\[main\.p7\] always -1 >> 1 != -1: PROVED$ +^\[main\.p8\] always -1 >>> 1 == -1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/signed2.desc b/regression/verilog/expressions/signed2.desc index e72f44f3d..f823c76d7 100644 --- a/regression/verilog/expressions/signed2.desc +++ b/regression/verilog/expressions/signed2.desc @@ -1,6 +1,6 @@ CORE signed2.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/signing_cast1.desc b/regression/verilog/expressions/signing_cast1.desc index 9d8866326..b8731bb59 100644 --- a/regression/verilog/expressions/signing_cast1.desc +++ b/regression/verilog/expressions/signing_cast1.desc @@ -1,12 +1,12 @@ CORE broken-smt-backend signing_cast1.sv ---module main --bound 0 -^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED up to bound 0$ -^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED up to bound 0$ -^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED up to bound 0$ -^\[main\.p3\] always signed'\(!0\) == -1: PROVED up to bound 0$ -^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED up to bound 0$ -^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$ +--module main +^\[main\.p0\] always signed'\(1'b1\) == -1: PROVED$ +^\[main\.p1\] always signed'\(4'b1110\) == -2: PROVED$ +^\[main\.p2\] always signed'\(4'b0111\) == 7: PROVED$ +^\[main\.p3\] always signed'\(!0\) == -1: PROVED$ +^\[main\.p4\] always unsigned'\(!0\) == 1: PROVED$ +^\[main\.p5\] always unsigned'\(-1\) == 32'hFFFFFFFF: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/size_cast1.desc b/regression/verilog/expressions/size_cast1.desc index 8e3697c39..8afe24233 100644 --- a/regression/verilog/expressions/size_cast1.desc +++ b/regression/verilog/expressions/size_cast1.desc @@ -1,10 +1,10 @@ CORE size_cast1.sv ---module main --bound 0 -^\[main\.p0\] always \$bits\(10'\(1\)\) == 10: PROVED up to bound 0$ -^\[main\.p1\] always \$bits\(20'\(1\)\) == 20: PROVED up to bound 0$ -^\[main\.p2\] always 10'\(-1\) == -1: PROVED up to bound 0$ -^\[main\.p3\] always 2'\(1 == 1\) == 1: PROVED up to bound 0$ +--module main +^\[main\.p0\] always \$bits\(10'\(1\)\) == 10: PROVED$ +^\[main\.p1\] always \$bits\(20'\(1\)\) == 20: PROVED$ +^\[main\.p2\] always 10'\(-1\) == -1: PROVED$ +^\[main\.p3\] always 2'\(1 == 1\) == 1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/static_cast1.desc b/regression/verilog/expressions/static_cast1.desc index b5ec51dfe..838ec3718 100644 --- a/regression/verilog/expressions/static_cast1.desc +++ b/regression/verilog/expressions/static_cast1.desc @@ -1,7 +1,7 @@ CORE static_cast1.sv ---module main --bound 0 -^\[main\.p0\] always \[7:0\]'\(32'hFFFF\) == 255: PROVED up to bound 0$ +--module main +^\[main\.p0\] always \[7:0\]'\(32'hFFFF\) == 255: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/streaming_concatenation1.desc b/regression/verilog/expressions/streaming_concatenation1.desc index 2c6516b59..6b0d09766 100644 --- a/regression/verilog/expressions/streaming_concatenation1.desc +++ b/regression/verilog/expressions/streaming_concatenation1.desc @@ -1,10 +1,10 @@ CORE streaming_concatenation1.sv ---bound 0 -^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED up to bound 0$ -^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED up to bound 0$ -^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED up to bound 0$ -^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED up to bound 0$ + +^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED$ +^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED$ +^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED$ +^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/streaming_concatenation2.desc b/regression/verilog/expressions/streaming_concatenation2.desc index 7cb342eb8..ac3c6d7f1 100644 --- a/regression/verilog/expressions/streaming_concatenation2.desc +++ b/regression/verilog/expressions/streaming_concatenation2.desc @@ -1,6 +1,6 @@ CORE streaming_concatenation2.sv ---bound 0 + ^file .* line 4: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc index 36081a0a8..c7efea341 100644 --- a/regression/verilog/expressions/wildcard_equality1.desc +++ b/regression/verilog/expressions/wildcard_equality1.desc @@ -1,16 +1,16 @@ CORE wildcard_equality1.sv ---bound 0 -^\[main\.property01\] always 10 ==\? 10 === 1: PROVED up to bound 0$ -^\[main\.property02\] always 10 ==\? 20 === 0: PROVED up to bound 0$ -^\[main\.property03\] always 10 !=\? 20 === 1: PROVED up to bound 0$ -^\[main\.property04\] always 10 ==\? 20 === 0: PROVED up to bound 0$ -^\[main\.property05\] always 2'b00 ==\? 2'b0x === 1: PROVED up to bound 0$ -^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED up to bound 0$ -^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED up to bound 0$ -^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED up to bound 0$ + +^\[main\.property01\] always 10 ==\? 10 === 1: PROVED$ +^\[main\.property02\] always 10 ==\? 20 === 0: PROVED$ +^\[main\.property03\] always 10 !=\? 20 === 1: PROVED$ +^\[main\.property04\] always 10 ==\? 20 === 0: PROVED$ +^\[main\.property05\] always 2'b00 ==\? 2'b0x === 1: PROVED$ +^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED$ +^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED$ +^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED$ ^\[main\.property09\] always 2'b11 ==\? 2'b11 === 0: REFUTED$ -^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED up to bound 0$ +^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/wildcard_equality2.desc b/regression/verilog/expressions/wildcard_equality2.desc index c2ad5e192..ecfe995c4 100644 --- a/regression/verilog/expressions/wildcard_equality2.desc +++ b/regression/verilog/expressions/wildcard_equality2.desc @@ -1,6 +1,6 @@ CORE wildcard_equality2.v ---bound 0 + ^file .* line 4: operand 1\.1 must be integral$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/for/break1.desc b/regression/verilog/for/break1.desc index c24199eea..ef08f1137 100644 --- a/regression/verilog/for/break1.desc +++ b/regression/verilog/for/break1.desc @@ -1,6 +1,6 @@ CORE break1.sv ---bound 0 + ^file .* line 7: synthesis of break not supported$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/for/continue1.desc b/regression/verilog/for/continue1.desc index da8a68340..586015cb1 100644 --- a/regression/verilog/for/continue1.desc +++ b/regression/verilog/for/continue1.desc @@ -1,6 +1,6 @@ CORE continue1.sv ---bound 0 + ^file .* line 8: synthesis of continue not supported$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/for/for_with_reg.desc b/regression/verilog/for/for_with_reg.desc index 09470d6f8..663999ab2 100644 --- a/regression/verilog/for/for_with_reg.desc +++ b/regression/verilog/for/for_with_reg.desc @@ -1,6 +1,6 @@ CORE for_with_reg.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/functioncall/function_ports1.desc b/regression/verilog/functioncall/function_ports1.desc index 6cae1cb8d..f4c3bc1c7 100644 --- a/regression/verilog/functioncall/function_ports1.desc +++ b/regression/verilog/functioncall/function_ports1.desc @@ -1,8 +1,8 @@ CORE function_ports1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.test16\] always .*: PROVED up to bound 0$ +^\[main\.property\.test16\] always .*: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/functioncall/functioncall1.desc b/regression/verilog/functioncall/functioncall1.desc index 154ae84a9..deb64858d 100644 --- a/regression/verilog/functioncall/functioncall1.desc +++ b/regression/verilog/functioncall/functioncall1.desc @@ -1,8 +1,8 @@ CORE functioncall1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.test1\] always .*: PROVED up to bound 0$ +^\[main\.property\.test1\] always .*: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/functioncall/functioncall3.desc b/regression/verilog/functioncall/functioncall3.desc index 0edd47a6f..80c1146d9 100644 --- a/regression/verilog/functioncall/functioncall3.desc +++ b/regression/verilog/functioncall/functioncall3.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend functioncall3.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ ^UNSAT: .*$ diff --git a/regression/verilog/functioncall/functioncall4.desc b/regression/verilog/functioncall/functioncall4.desc index 564d66096..3822db168 100644 --- a/regression/verilog/functioncall/functioncall4.desc +++ b/regression/verilog/functioncall/functioncall4.desc @@ -1,6 +1,6 @@ CORE functioncall4.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ ^UNSAT: .*$ diff --git a/regression/verilog/functioncall/functioncall5.desc b/regression/verilog/functioncall/functioncall5.desc index d6ae3b311..5d2bd7d8c 100644 --- a/regression/verilog/functioncall/functioncall5.desc +++ b/regression/verilog/functioncall/functioncall5.desc @@ -1,6 +1,6 @@ CORE functioncall5.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/functioncall/functioncall6.desc b/regression/verilog/functioncall/functioncall6.desc index c00d9d899..eb0326034 100644 --- a/regression/verilog/functioncall/functioncall6.desc +++ b/regression/verilog/functioncall/functioncall6.desc @@ -1,8 +1,8 @@ CORE functioncall6.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p1\] always .*: PROVED up to bound 0$ +^\[main\.property\.p1\] always .*: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/functioncall/functioncall7.desc b/regression/verilog/functioncall/functioncall7.desc index aebcd15d8..d913ae47f 100644 --- a/regression/verilog/functioncall/functioncall7.desc +++ b/regression/verilog/functioncall/functioncall7.desc @@ -1,6 +1,6 @@ CORE functioncall7.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/functioncall/functioncall_as_constant1.desc b/regression/verilog/functioncall/functioncall_as_constant1.desc index 85083a7dd..24b79658e 100644 --- a/regression/verilog/functioncall/functioncall_as_constant1.desc +++ b/regression/verilog/functioncall/functioncall_as_constant1.desc @@ -1,6 +1,6 @@ CORE functioncall_as_constant1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/functioncall/functioncall_as_input1.desc b/regression/verilog/functioncall/functioncall_as_input1.desc index bfae3fe5c..c2ff2e754 100644 --- a/regression/verilog/functioncall/functioncall_as_input1.desc +++ b/regression/verilog/functioncall/functioncall_as_input1.desc @@ -1,6 +1,6 @@ CORE functioncall_as_input1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/functioncall/return1.desc b/regression/verilog/functioncall/return1.desc index d9de09a83..be3278ec9 100644 --- a/regression/verilog/functioncall/return1.desc +++ b/regression/verilog/functioncall/return1.desc @@ -1,6 +1,6 @@ CORE return1.sv ---bound 0 + ^file .* line 4: synthesis of return not supported$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/functioncall/void_function1.desc b/regression/verilog/functioncall/void_function1.desc index adeb287df..3f049359b 100644 --- a/regression/verilog/functioncall/void_function1.desc +++ b/regression/verilog/functioncall/void_function1.desc @@ -1,6 +1,6 @@ CORE void_function1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/generate/generate-for2.desc b/regression/verilog/generate/generate-for2.desc index 168a17e6e..5817a7c78 100644 --- a/regression/verilog/generate/generate-for2.desc +++ b/regression/verilog/generate/generate-for2.desc @@ -1,6 +1,6 @@ CORE generate-for2.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/generate/generate-inst2.desc b/regression/verilog/generate/generate-inst2.desc index 498ef3c5f..41bb119ce 100644 --- a/regression/verilog/generate/generate-inst2.desc +++ b/regression/verilog/generate/generate-inst2.desc @@ -1,6 +1,6 @@ CORE generate-inst2.v ---module main --bound 0 +--module main ^EXIT=10$ ^SIGNAL=0$ ^no properties$ diff --git a/regression/verilog/generate/generate-localparam1.desc b/regression/verilog/generate/generate-localparam1.desc index 00bf567c7..d4edaba4b 100644 --- a/regression/verilog/generate/generate-localparam1.desc +++ b/regression/verilog/generate/generate-localparam1.desc @@ -1,6 +1,6 @@ CORE generate-localparam1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/generate/generate-reg1.desc b/regression/verilog/generate/generate-reg1.desc index 60a3c80a2..6c301d35d 100644 --- a/regression/verilog/generate/generate-reg1.desc +++ b/regression/verilog/generate/generate-reg1.desc @@ -1,6 +1,6 @@ CORE generate-reg1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/generate/generate-reg2.desc b/regression/verilog/generate/generate-reg2.desc index 17121c552..8963cce17 100644 --- a/regression/verilog/generate/generate-reg2.desc +++ b/regression/verilog/generate/generate-reg2.desc @@ -1,6 +1,6 @@ CORE generate-reg2.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/hierarchical_identifiers/hierarchical_identifiers1.desc b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers1.desc index 6c6b81dca..e34d110f9 100644 --- a/regression/verilog/hierarchical_identifiers/hierarchical_identifiers1.desc +++ b/regression/verilog/hierarchical_identifiers/hierarchical_identifiers1.desc @@ -1,6 +1,6 @@ CORE hierarchical_identifiers1.v ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/let/let1.desc b/regression/verilog/let/let1.desc index 63d72dae7..da1179030 100644 --- a/regression/verilog/let/let1.desc +++ b/regression/verilog/let/let1.desc @@ -1,6 +1,6 @@ CORE let1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/let/let_ports1.desc b/regression/verilog/let/let_ports1.desc index f8078ed46..564f572bc 100644 --- a/regression/verilog/let/let_ports1.desc +++ b/regression/verilog/let/let_ports1.desc @@ -1,6 +1,6 @@ CORE let_ports1.sv ---bound 0 + ^file .* line 5: let ports not supported yet$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/modules/localparam2.desc b/regression/verilog/modules/localparam2.desc index 5c7c05c53..15dfd1194 100644 --- a/regression/verilog/modules/localparam2.desc +++ b/regression/verilog/modules/localparam2.desc @@ -1,6 +1,6 @@ CORE localparam2.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/localparam3.desc b/regression/verilog/modules/localparam3.desc index 2f7d293c7..e34e0d78e 100644 --- a/regression/verilog/modules/localparam3.desc +++ b/regression/verilog/modules/localparam3.desc @@ -1,6 +1,6 @@ CORE localparam3.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameter_ports1.desc b/regression/verilog/modules/parameter_ports1.desc index af74a9899..a341acf9e 100644 --- a/regression/verilog/modules/parameter_ports1.desc +++ b/regression/verilog/modules/parameter_ports1.desc @@ -1,6 +1,6 @@ CORE parameter_ports1.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameter_ports2.desc b/regression/verilog/modules/parameter_ports2.desc index c5b5ff8b5..858774ed3 100644 --- a/regression/verilog/modules/parameter_ports2.desc +++ b/regression/verilog/modules/parameter_ports2.desc @@ -1,6 +1,6 @@ KNOWNBUG parameter_ports2.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameter_ports3.desc b/regression/verilog/modules/parameter_ports3.desc index ea9781376..3bcd3a6bb 100644 --- a/regression/verilog/modules/parameter_ports3.desc +++ b/regression/verilog/modules/parameter_ports3.desc @@ -1,6 +1,6 @@ CORE parameter_ports3.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameter_ports4.desc b/regression/verilog/modules/parameter_ports4.desc index 6163170fc..64ef929a0 100644 --- a/regression/verilog/modules/parameter_ports4.desc +++ b/regression/verilog/modules/parameter_ports4.desc @@ -1,6 +1,6 @@ KNOWNBUG parameter_ports4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameters10.desc b/regression/verilog/modules/parameters10.desc index 1209f79a4..f7d20e169 100644 --- a/regression/verilog/modules/parameters10.desc +++ b/regression/verilog/modules/parameters10.desc @@ -1,6 +1,6 @@ CORE parameters10.v ---bound 0 + ^file .* line 6: expected constant expression, but got `main\.x'$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/modules/parameters4.desc b/regression/verilog/modules/parameters4.desc index 4d5355943..722f084a0 100644 --- a/regression/verilog/modules/parameters4.desc +++ b/regression/verilog/modules/parameters4.desc @@ -1,6 +1,6 @@ CORE parameters4.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/parameters5.desc b/regression/verilog/modules/parameters5.desc index 07bdf42d5..1d7ff54e6 100644 --- a/regression/verilog/modules/parameters5.desc +++ b/regression/verilog/modules/parameters5.desc @@ -1,6 +1,6 @@ KNOWNBUG parameters5.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports3.desc b/regression/verilog/modules/ports3.desc index 1232e5a53..d473b9fe6 100644 --- a/regression/verilog/modules/ports3.desc +++ b/regression/verilog/modules/ports3.desc @@ -1,6 +1,6 @@ CORE ports3.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports4.desc b/regression/verilog/modules/ports4.desc index c2ef42ade..010c97880 100644 --- a/regression/verilog/modules/ports4.desc +++ b/regression/verilog/modules/ports4.desc @@ -1,6 +1,6 @@ CORE ports4.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports5.desc b/regression/verilog/modules/ports5.desc index 18a4fa264..99642ad27 100644 --- a/regression/verilog/modules/ports5.desc +++ b/regression/verilog/modules/ports5.desc @@ -1,6 +1,6 @@ CORE ports5.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports6.desc b/regression/verilog/modules/ports6.desc index 26fc63af5..74fc0c9dd 100644 --- a/regression/verilog/modules/ports6.desc +++ b/regression/verilog/modules/ports6.desc @@ -1,6 +1,6 @@ CORE ports6.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports7.desc b/regression/verilog/modules/ports7.desc index 483a217b7..ce173b3db 100644 --- a/regression/verilog/modules/ports7.desc +++ b/regression/verilog/modules/ports7.desc @@ -1,6 +1,6 @@ CORE ports7.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/ports8.desc b/regression/verilog/modules/ports8.desc index 9520cc2de..8308c5129 100644 --- a/regression/verilog/modules/ports8.desc +++ b/regression/verilog/modules/ports8.desc @@ -1,6 +1,6 @@ CORE ports8.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc index 717142427..361671b40 100644 --- a/regression/verilog/modules/type_parameters1.desc +++ b/regression/verilog/modules/type_parameters1.desc @@ -1,8 +1,8 @@ CORE type_parameters1.sv ---bound 0 -^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED up to bound 0$ -^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED up to bound 0$ + +^\[main\.p1\] always \$bits\(main\.T1\) == 1: PROVED$ +^\[main\.p2\] always \$bits\(main\.T2\) == 32: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/modules/variable_module_port1.desc b/regression/verilog/modules/variable_module_port1.desc index adf2591d1..e8e5dd410 100644 --- a/regression/verilog/modules/variable_module_port1.desc +++ b/regression/verilog/modules/variable_module_port1.desc @@ -1,6 +1,6 @@ CORE variable_module_port1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/nets/implicit1.desc b/regression/verilog/nets/implicit1.desc index b6302adda..962dff516 100644 --- a/regression/verilog/nets/implicit1.desc +++ b/regression/verilog/nets/implicit1.desc @@ -1,6 +1,6 @@ CORE implicit1.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^file .* line 4: implicit wire main\.O$ ^file .* line 4: implicit wire main\.A$ ^file .* line 4: implicit wire main\.B$ diff --git a/regression/verilog/nets/implicit2.desc b/regression/verilog/nets/implicit2.desc index caa69518e..11a81c19f 100644 --- a/regression/verilog/nets/implicit2.desc +++ b/regression/verilog/nets/implicit2.desc @@ -1,6 +1,6 @@ CORE implicit2.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/nets/implicit3.desc b/regression/verilog/nets/implicit3.desc index 6f4846bd0..6291ce692 100644 --- a/regression/verilog/nets/implicit3.desc +++ b/regression/verilog/nets/implicit3.desc @@ -1,6 +1,6 @@ CORE implicit3.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^file .* line 6: implicit wire main\.O$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/verilog/nets/implicit4.desc b/regression/verilog/nets/implicit4.desc index 155fba94d..a92a284fe 100644 --- a/regression/verilog/nets/implicit4.desc +++ b/regression/verilog/nets/implicit4.desc @@ -1,6 +1,6 @@ CORE implicit4.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/nets/implicit5.desc b/regression/verilog/nets/implicit5.desc index 4ca0dfde3..b010e838f 100644 --- a/regression/verilog/nets/implicit5.desc +++ b/regression/verilog/nets/implicit5.desc @@ -1,6 +1,6 @@ CORE implicit5.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^file .* line 4: unknown identifier A$ ^EXIT=2$ ^SIGNAL=0$ diff --git a/regression/verilog/nets/implicit6.desc b/regression/verilog/nets/implicit6.desc index 472b00703..069d5e4b6 100644 --- a/regression/verilog/nets/implicit6.desc +++ b/regression/verilog/nets/implicit6.desc @@ -1,6 +1,6 @@ CORE implicit6.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/nets/implicit7.desc b/regression/verilog/nets/implicit7.desc index 9b625d528..9d73d6984 100644 --- a/regression/verilog/nets/implicit7.desc +++ b/regression/verilog/nets/implicit7.desc @@ -1,6 +1,6 @@ KNOWNBUG implicit7.sv ---bound 0 --warn-implicit-nets +--warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/part-select/indexed-part-select1.desc b/regression/verilog/part-select/indexed-part-select1.desc index 5990bdc0d..909331121 100644 --- a/regression/verilog/part-select/indexed-part-select1.desc +++ b/regression/verilog/part-select/indexed-part-select1.desc @@ -1,6 +1,6 @@ CORE indexed-part-select1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/part-select/indexed-part-select3.desc b/regression/verilog/part-select/indexed-part-select3.desc index 021729201..ba8f96095 100644 --- a/regression/verilog/part-select/indexed-part-select3.desc +++ b/regression/verilog/part-select/indexed-part-select3.desc @@ -1,6 +1,6 @@ CORE indexed-part-select3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/part-select/indexed-part-select4.desc b/regression/verilog/part-select/indexed-part-select4.desc index 961b7e879..7c669952b 100644 --- a/regression/verilog/part-select/indexed-part-select4.desc +++ b/regression/verilog/part-select/indexed-part-select4.desc @@ -1,6 +1,6 @@ CORE indexed-part-select4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/part-select/indexed-part-select5.desc b/regression/verilog/part-select/indexed-part-select5.desc index 6a336c9cd..7238cf604 100644 --- a/regression/verilog/part-select/indexed-part-select5.desc +++ b/regression/verilog/part-select/indexed-part-select5.desc @@ -1,6 +1,6 @@ CORE indexed-part-select5.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nand1.desc b/regression/verilog/primitive_gates/nand1.desc index da1db3f8c..c7cd25bdc 100644 --- a/regression/verilog/primitive_gates/nand1.desc +++ b/regression/verilog/primitive_gates/nand1.desc @@ -1,6 +1,6 @@ CORE nand1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nand2.desc b/regression/verilog/primitive_gates/nand2.desc index 86c66eff0..d11be3eaa 100644 --- a/regression/verilog/primitive_gates/nand2.desc +++ b/regression/verilog/primitive_gates/nand2.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend nand2.sv ---bound 0 -^\[main\.nand_ok\] always !main\.nand_in1 == main\.nand_out: PROVED up to bound 0$ -^\[main\.nand_is_reduction_nand\] always ~\&\{ main\.nand_in1 \} == main\.nand_out: PROVED up to bound 0$ + +^\[main\.nand_ok\] always !main\.nand_in1 == main\.nand_out: PROVED$ +^\[main\.nand_is_reduction_nand\] always ~\&\{ main\.nand_in1 \} == main\.nand_out: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nand4.desc b/regression/verilog/primitive_gates/nand4.desc index e2d2646f9..0cd4d2565 100644 --- a/regression/verilog/primitive_gates/nand4.desc +++ b/regression/verilog/primitive_gates/nand4.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend nand4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nor1.desc b/regression/verilog/primitive_gates/nor1.desc index 3149bb985..6ce760a9a 100644 --- a/regression/verilog/primitive_gates/nor1.desc +++ b/regression/verilog/primitive_gates/nor1.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend nor1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nor2.desc b/regression/verilog/primitive_gates/nor2.desc index e0aa1f086..8a51a6c05 100644 --- a/regression/verilog/primitive_gates/nor2.desc +++ b/regression/verilog/primitive_gates/nor2.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend nor2.sv ---bound 0 -^\[main\.nor_ok\] always !main\.nor_in1 == main\.nor_out: PROVED up to bound 0$ -^\[main\.nor_is_reduction_nor\] always ~\|\{ main\.nor_in1 \} == main\.nor_out: PROVED up to bound 0$ + +^\[main\.nor_ok\] always !main\.nor_in1 == main\.nor_out: PROVED$ +^\[main\.nor_is_reduction_nor\] always ~\|\{ main\.nor_in1 \} == main\.nor_out: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/nor4.desc b/regression/verilog/primitive_gates/nor4.desc index 5ae5809ee..763cb7749 100644 --- a/regression/verilog/primitive_gates/nor4.desc +++ b/regression/verilog/primitive_gates/nor4.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend nor4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/not1.desc b/regression/verilog/primitive_gates/not1.desc index 8bfe426ba..35f9f94b4 100644 --- a/regression/verilog/primitive_gates/not1.desc +++ b/regression/verilog/primitive_gates/not1.desc @@ -1,6 +1,6 @@ CORE not1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/or1.desc b/regression/verilog/primitive_gates/or1.desc index 076071b4f..311611d62 100644 --- a/regression/verilog/primitive_gates/or1.desc +++ b/regression/verilog/primitive_gates/or1.desc @@ -1,6 +1,6 @@ CORE or1.sv ---bound 0 + ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/xnor1.desc b/regression/verilog/primitive_gates/xnor1.desc index 5157b0fc3..02c8b75f0 100644 --- a/regression/verilog/primitive_gates/xnor1.desc +++ b/regression/verilog/primitive_gates/xnor1.desc @@ -1,9 +1,9 @@ CORE broken-smt-backend xnor1.sv ---bound 0 -^\[main\.xnor_ok\] always !\(xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\)\) == main\.xnor_out: PROVED up to bound 0$ + +^\[main\.xnor_ok\] always !\(xor\(xor\(main\.xnor_in1, main\.xnor_in2\), main\.xnor_in3\)\) == main\.xnor_out: PROVED$ ^\[main\.xnor_fail\] always main\.xnor_in1 == main\.xnor_in2 == main\.xnor_in3 == main\.xnor_out: REFUTED$ -^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED up to bound 0$ +^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1, main\.xnor_in2, main\.xnor_in3 \} == main\.xnor_out: PROVED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/xnor2.desc b/regression/verilog/primitive_gates/xnor2.desc index 2ef667e2e..cd90f0c8a 100644 --- a/regression/verilog/primitive_gates/xnor2.desc +++ b/regression/verilog/primitive_gates/xnor2.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend xnor2.sv ---bound 0 -^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED up to bound 0$ -^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED up to bound 0$ + +^\[main\.xnor_ok\] always !main\.xnor_in1 == main\.xnor_out: PROVED$ +^\[main\.xnor_is_reduction_xnor\] always ~\^\{ main\.xnor_in1 \} == main\.xnor_out: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/xnor3.desc b/regression/verilog/primitive_gates/xnor3.desc index 7f4836cde..465a26c4a 100644 --- a/regression/verilog/primitive_gates/xnor3.desc +++ b/regression/verilog/primitive_gates/xnor3.desc @@ -1,7 +1,7 @@ CORE xnor3.sv ---bound 0 -^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$ + +^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/primitive_gates/xnor4.desc b/regression/verilog/primitive_gates/xnor4.desc index e249c0f18..5020f9ded 100644 --- a/regression/verilog/primitive_gates/xnor4.desc +++ b/regression/verilog/primitive_gates/xnor4.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend xnor4.sv ---bound 0 -^\[main\.xnor_x1_ok\] always ~\(main\.xnor_in1 \^ main\.xnor_in2 \^ main.xnor_in3\) == main.xnor_out: PROVED up to bound 0$ -^\[main\.xnor_x2_ok\] always ~main\.xnor_in1 == main.xnor_out: PROVED up to bound 0$ + +^\[main\.xnor_x1_ok\] always ~\(main\.xnor_in1 \^ main\.xnor_in2 \^ main.xnor_in3\) == main.xnor_out: PROVED$ +^\[main\.xnor_x2_ok\] always ~main\.xnor_in1 == main.xnor_out: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/string/string_literals1.desc b/regression/verilog/string/string_literals1.desc index 29806126e..4e77fb0a4 100644 --- a/regression/verilog/string/string_literals1.desc +++ b/regression/verilog/string/string_literals1.desc @@ -1,6 +1,6 @@ CORE string_literals1.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/structs/structs1.desc b/regression/verilog/structs/structs1.desc index c17dc1492..8a017cb59 100644 --- a/regression/verilog/structs/structs1.desc +++ b/regression/verilog/structs/structs1.desc @@ -1,10 +1,10 @@ CORE structs1.sv ---bound 0 -^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED up to bound 0$ -^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$ -^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$ -^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$ + +^\[main\.p0\] always \$bits\(main\.s\) == 9: PROVED$ +^\[main\.p1\] always main\.s\.field1 == 1: PROVED$ +^\[main\.p2\] always main\.s\.field2 == 0: PROVED$ +^\[main\.p3\] always main\.s\.field3 == 115: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/structs/structs2.desc b/regression/verilog/structs/structs2.desc index 68ec61bbe..9d1229906 100644 --- a/regression/verilog/structs/structs2.desc +++ b/regression/verilog/structs/structs2.desc @@ -1,6 +1,6 @@ CORE structs2.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/structs/structs3.desc b/regression/verilog/structs/structs3.desc index ccf2f5ef5..7d9a390bb 100644 --- a/regression/verilog/structs/structs3.desc +++ b/regression/verilog/structs/structs3.desc @@ -1,6 +1,6 @@ CORE structs3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/structs/structs4.desc b/regression/verilog/structs/structs4.desc index b9fcac7a8..83b3684c6 100644 --- a/regression/verilog/structs/structs4.desc +++ b/regression/verilog/structs/structs4.desc @@ -1,7 +1,7 @@ CORE structs4.sv ---bound 0 -^\[main\.p0\] always main\.w == 32'h173: PROVED up to bound 0$ + +^\[main\.p0\] always main\.w == 32'h173: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/structs/structs5.desc b/regression/verilog/structs/structs5.desc index 366d29391..ae3ba0123 100644 --- a/regression/verilog/structs/structs5.desc +++ b/regression/verilog/structs/structs5.desc @@ -1,9 +1,9 @@ CORE structs5.sv ---bound 0 -^\[main\.p1\] always main\.s\.field1 == 1: PROVED up to bound 0$ -^\[main\.p2\] always main\.s\.field2 == 0: PROVED up to bound 0$ -^\[main\.p3\] always main\.s\.field3 == 115: PROVED up to bound 0$ + +^\[main\.p1\] always main\.s\.field1 == 1: PROVED$ +^\[main\.p2\] always main\.s\.field2 == 0: PROVED$ +^\[main\.p3\] always main\.s\.field3 == 115: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/always_comb1.desc b/regression/verilog/synthesis/always_comb1.desc index 53f4bf918..71d01902e 100644 --- a/regression/verilog/synthesis/always_comb1.desc +++ b/regression/verilog/synthesis/always_comb1.desc @@ -1,6 +1,6 @@ CORE always_comb1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/always_comb2.desc b/regression/verilog/synthesis/always_comb2.desc index cf435a6af..523cc7505 100644 --- a/regression/verilog/synthesis/always_comb2.desc +++ b/regression/verilog/synthesis/always_comb2.desc @@ -1,9 +1,9 @@ CORE always_comb2.sv ---bound 0 -^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED up to bound 0$ -^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED up to bound 0$ -^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED up to bound 0$ + +^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED$ +^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED$ +^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment1.desc b/regression/verilog/synthesis/continuous_assignment1.desc index f13825ecf..ce65964fb 100644 --- a/regression/verilog/synthesis/continuous_assignment1.desc +++ b/regression/verilog/synthesis/continuous_assignment1.desc @@ -1,6 +1,6 @@ CORE continuous_assignment1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment2.desc b/regression/verilog/synthesis/continuous_assignment2.desc index 896207d97..dec8181cc 100644 --- a/regression/verilog/synthesis/continuous_assignment2.desc +++ b/regression/verilog/synthesis/continuous_assignment2.desc @@ -1,6 +1,6 @@ CORE continuous_assignment2.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment3.desc b/regression/verilog/synthesis/continuous_assignment3.desc index d6e722ac8..839b846c9 100644 --- a/regression/verilog/synthesis/continuous_assignment3.desc +++ b/regression/verilog/synthesis/continuous_assignment3.desc @@ -1,6 +1,6 @@ CORE continuous_assignment3.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment_to_net_part_select1.desc b/regression/verilog/synthesis/continuous_assignment_to_net_part_select1.desc index d9e6b6896..551c098fb 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_net_part_select1.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_net_part_select1.desc @@ -1,7 +1,7 @@ KNOWNBUG continuous_assignment_to_net_part_select1.sv ---bound 0 -^\[main\.p0\] always main\.some_wire\[1:0\] == 1: PROVED up to bound 0$ + +^\[main\.p0\] always main\.some_wire\[1:0\] == 1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc index a4b74babe..1541189bf 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc @@ -1,7 +1,7 @@ CORE continuous_assignment_to_variable_systemverilog.sv ---bound 0 -^\[main\.p1\] always main\.some_reg == main\.i: PROVED up to bound 0$ + +^\[main\.p1\] always main\.some_reg == main\.i: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog3.desc b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog3.desc index 86201ac9c..ecaec5790 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog3.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog3.desc @@ -1,6 +1,6 @@ CORE continuous_assignment_to_variable_systemverilog3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_verilog.desc b/regression/verilog/synthesis/continuous_assignment_to_variable_verilog.desc index 409fa6f90..85b6b8131 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable_verilog.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_variable_verilog.desc @@ -1,6 +1,6 @@ KNOWNBUG continuous_assignment_to_variable_verilog.v ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/array_functions1.desc b/regression/verilog/system-functions/array_functions1.desc index fa264c47e..b3b7fe187 100644 --- a/regression/verilog/system-functions/array_functions1.desc +++ b/regression/verilog/system-functions/array_functions1.desc @@ -1,21 +1,21 @@ CORE array_functions1.sv ---module main --bound 0 -^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED up to bound 0$ -^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED up to bound 0$ -^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED up to bound 0$ -^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED up to bound 0$ -^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED up to bound 0$ -^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED up to bound 0$ -^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED up to bound 0$ -^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED up to bound 0$ -^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED up to bound 0$ -^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED up to bound 0$ -^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED up to bound 0$ -^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED up to bound 0$ -^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED up to bound 0$ -^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED up to bound 0$ -^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED up to bound 0$ +--module main +^\[main\.pP0\] always \$left\(main\.packed1\) == 32 && \$right\(main\.packed1\) == 1: PROVED$ +^\[main\.pP1\] always \$left\(main\.packed2\) == 0 && \$right\(main\.packed2\) == 31: PROVED$ +^\[main\.pP2\] always \$low\(main\.packed1\) == 1 && \$high\(main\.packed1\) == 32: PROVED$ +^\[main\.pP3\] always \$low\(main\.packed2\) == 0 && \$high\(main\.packed2\) == 31: PROVED$ +^\[main\.pP4\] always \$increment\(main\.packed1\) == 1: PROVED$ +^\[main\.pP5\] always \$increment\(main\.packed2\) == -1: PROVED$ +^\[main\.pU0\] always \$left\(main\.unpacked1\) == 32 && \$right\(main\.unpacked1\) == 1: PROVED$ +^\[main\.pU1\] always \$left\(main\.unpacked2\) == 0 && \$right\(main\.unpacked2\) == 31: PROVED$ +^\[main\.pU2\] always \$left\(main\.unpacked3\) == 31 && \$right\(main\.unpacked3\) == 0: PROVED$ +^\[main\.pU3\] always \$low\(main\.unpacked1\) == 1 && \$high\(main\.unpacked1\) == 32: PROVED$ +^\[main\.pU4\] always \$low\(main\.unpacked2\) == 0 && \$high\(main\.unpacked2\) == 31: PROVED$ +^\[main\.pU5\] always \$low\(main\.unpacked3\) == 0 && \$high\(main\.unpacked3\) == 31: PROVED$ +^\[main\.pU6\] always \$increment\(main\.unpacked1\) == 1: PROVED$ +^\[main\.pU7\] always \$increment\(main\.unpacked2\) == -1: PROVED$ +^\[main\.pU8\] always \$increment\(main\.unpacked3\) == 1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/bits1.desc b/regression/verilog/system-functions/bits1.desc index 301de1487..d22a09698 100644 --- a/regression/verilog/system-functions/bits1.desc +++ b/regression/verilog/system-functions/bits1.desc @@ -1,6 +1,6 @@ CORE bits1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/bitstoreal1.desc b/regression/verilog/system-functions/bitstoreal1.desc index e8ce6ead8..7574dbce0 100644 --- a/regression/verilog/system-functions/bitstoreal1.desc +++ b/regression/verilog/system-functions/bitstoreal1.desc @@ -1,6 +1,6 @@ CORE bitstoreal1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/bitstoshortreal1.desc b/regression/verilog/system-functions/bitstoshortreal1.desc index 4ca90c29e..2594ca652 100644 --- a/regression/verilog/system-functions/bitstoshortreal1.desc +++ b/regression/verilog/system-functions/bitstoshortreal1.desc @@ -1,6 +1,6 @@ CORE bitstoshortreal1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/clog2.desc b/regression/verilog/system-functions/clog2.desc index 9727692b7..5eda64e9c 100644 --- a/regression/verilog/system-functions/clog2.desc +++ b/regression/verilog/system-functions/clog2.desc @@ -3,12 +3,12 @@ clog2.v ^EXIT=0$ ^SIGNAL=0$ -^\[main.property.p0\] .* PROVED up to bound 1$ -^\[main.property.p1\] .* PROVED up to bound 1$ -^\[main.property.p2\] .* PROVED up to bound 1$ -^\[main.property.p3\] .* PROVED up to bound 1$ -^\[main.property.p4\] .* PROVED up to bound 1$ -^\[main.property.p5\] .* PROVED up to bound 1$ -^\[main.property.p6\] .* PROVED up to bound 1$ +^\[main.property.p0\] .* PROVED$ +^\[main.property.p1\] .* PROVED$ +^\[main.property.p2\] .* PROVED$ +^\[main.property.p3\] .* PROVED$ +^\[main.property.p4\] .* PROVED$ +^\[main.property.p5\] .* PROVED$ +^\[main.property.p6\] .* PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/system-functions/countones1.desc b/regression/verilog/system-functions/countones1.desc index 163f089cc..71e35f586 100644 --- a/regression/verilog/system-functions/countones1.desc +++ b/regression/verilog/system-functions/countones1.desc @@ -1,6 +1,6 @@ CORE countones1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/itor1.desc b/regression/verilog/system-functions/itor1.desc index c920f6c3b..a1290c143 100644 --- a/regression/verilog/system-functions/itor1.desc +++ b/regression/verilog/system-functions/itor1.desc @@ -1,6 +1,6 @@ CORE itor1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/low1.desc b/regression/verilog/system-functions/low1.desc index 81145fc4a..bd8e6d321 100644 --- a/regression/verilog/system-functions/low1.desc +++ b/regression/verilog/system-functions/low1.desc @@ -1,6 +1,6 @@ CORE low1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/realtobits1.desc b/regression/verilog/system-functions/realtobits1.desc index a9bcf247a..a52a4cf30 100644 --- a/regression/verilog/system-functions/realtobits1.desc +++ b/regression/verilog/system-functions/realtobits1.desc @@ -1,6 +1,6 @@ CORE realtobits1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/rtoi1.desc b/regression/verilog/system-functions/rtoi1.desc index af39174a1..e7cb42715 100644 --- a/regression/verilog/system-functions/rtoi1.desc +++ b/regression/verilog/system-functions/rtoi1.desc @@ -1,6 +1,6 @@ CORE rtoi1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/shortrealtobits1.desc b/regression/verilog/system-functions/shortrealtobits1.desc index 785671a82..0a9b80c17 100644 --- a/regression/verilog/system-functions/shortrealtobits1.desc +++ b/regression/verilog/system-functions/shortrealtobits1.desc @@ -1,6 +1,6 @@ CORE shortrealtobits1.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/signed1.desc b/regression/verilog/system-functions/signed1.desc index 1ba64d600..2e0be1ec6 100644 --- a/regression/verilog/system-functions/signed1.desc +++ b/regression/verilog/system-functions/signed1.desc @@ -1,6 +1,6 @@ CORE signed1.v ---bound 0 + ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/signed2.desc b/regression/verilog/system-functions/signed2.desc index 9eff5979b..db8b85fe0 100644 --- a/regression/verilog/system-functions/signed2.desc +++ b/regression/verilog/system-functions/signed2.desc @@ -1,10 +1,10 @@ CORE signed2.sv ---bound 0 -^\[main\.p0\] always \$signed\(1\) == 1: PROVED up to bound 0$ -^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED up to bound 0$ -^\[main\.p2\] always \$signed\(-1\) == -1: PROVED up to bound 0$ -^\[main\.p3\] always \$signed\(!0\) == -1: PROVED up to bound 0$ + +^\[main\.p0\] always \$signed\(1\) == 1: PROVED$ +^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED$ +^\[main\.p2\] always \$signed\(-1\) == -1: PROVED$ +^\[main\.p3\] always \$signed\(!0\) == -1: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/test.desc b/regression/verilog/system-functions/test.desc index 8a8b7e056..62e70b697 100644 --- a/regression/verilog/system-functions/test.desc +++ b/regression/verilog/system-functions/test.desc @@ -1,6 +1,6 @@ CORE main.sv ---module main --bound 0 +--module main ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/typename1.desc b/regression/verilog/system-functions/typename1.desc index e27a32bea..db332884d 100644 --- a/regression/verilog/system-functions/typename1.desc +++ b/regression/verilog/system-functions/typename1.desc @@ -1,13 +1,13 @@ CORE typename1.sv ---module main --bound 0 -^\[.*\] always \$typename\(main\.some_bit\) == "bit": PROVED up to bound 0$ -^\[.*\] always \$typename\(main\.vector1\) == "bit\[31:0\]": PROVED up to bound 0$ -^\[.*\] always \$typename\(main\.vector2\) == "bit\[0:31\]": PROVED up to bound 0$ -^\[.*\] always \$typename\(main\.vector3\) == "bit signed\[31:0\]": PROVED up to bound 0$ -^\[.*\] always \$typename\(real'\(1\)\) == "real": PROVED up to bound 0$ -^\[.*\] always \$typename\(shortreal'\(1\)\) == "shortreal": PROVED up to bound 0$ -^\[.*\] always \$typename\(realtime'\(1\)\) == "realtime": PROVED up to bound 0$ +--module main +^\[.*\] always \$typename\(main\.some_bit\) == "bit": PROVED$ +^\[.*\] always \$typename\(main\.vector1\) == "bit\[31:0\]": PROVED$ +^\[.*\] always \$typename\(main\.vector2\) == "bit\[0:31\]": PROVED$ +^\[.*\] always \$typename\(main\.vector3\) == "bit signed\[31:0\]": PROVED$ +^\[.*\] always \$typename\(real'\(1\)\) == "real": PROVED$ +^\[.*\] always \$typename\(shortreal'\(1\)\) == "shortreal": PROVED$ +^\[.*\] always \$typename\(realtime'\(1\)\) == "realtime": PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/typedef/global_typedef.desc b/regression/verilog/typedef/global_typedef.desc index 92dad4abc..15827368f 100644 --- a/regression/verilog/typedef/global_typedef.desc +++ b/regression/verilog/typedef/global_typedef.desc @@ -1,6 +1,6 @@ KNOWNBUG global_typedef.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/typedef/typedef1.desc b/regression/verilog/typedef/typedef1.desc index 42dd771c8..af9466ab3 100644 --- a/regression/verilog/typedef/typedef1.desc +++ b/regression/verilog/typedef/typedef1.desc @@ -1,6 +1,6 @@ CORE typedef1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/unions/unions1.desc b/regression/verilog/unions/unions1.desc index 892169c99..d6a297ea4 100644 --- a/regression/verilog/unions/unions1.desc +++ b/regression/verilog/unions/unions1.desc @@ -1,6 +1,6 @@ CORE unions1.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/unions/unions2.desc b/regression/verilog/unions/unions2.desc index c483905b0..87a667678 100644 --- a/regression/verilog/unions/unions2.desc +++ b/regression/verilog/unions/unions2.desc @@ -1,6 +1,6 @@ CORE unions2.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/unions/unions3.desc b/regression/verilog/unions/unions3.desc index 7af55b1d4..964675a2d 100644 --- a/regression/verilog/unions/unions3.desc +++ b/regression/verilog/unions/unions3.desc @@ -1,6 +1,6 @@ CORE unions3.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/unions/unions4.desc b/regression/verilog/unions/unions4.desc index aa69bcb21..4d405ff38 100644 --- a/regression/verilog/unions/unions4.desc +++ b/regression/verilog/unions/unions4.desc @@ -1,6 +1,6 @@ CORE unions4.sv ---bound 0 + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h index 4023f5d7b..8ebd1c861 100644 --- a/src/ebmc/ebmc_properties.h +++ b/src/ebmc/ebmc_properties.h @@ -208,6 +208,13 @@ class ebmc_propertiest result.emplace(p.identifier, p.normalized_expr); return result; } + + void reset_failure_to_unknown() + { + for(auto &p : properties) + if(p.is_failure()) + p.unknown(); + } }; #endif // CPROVER_EBMC_PROPERTIES_H diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 584012331..39b5ee9cd 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -356,6 +356,59 @@ property_checker_resultt bit_level_bmc( } } +property_checker_resultt engine_heuristic( + const cmdlinet &cmdline, + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + messaget message(message_handler); + + if(properties.properties.empty()) + { + message.error() << "no properties" << messaget::eom; + return property_checker_resultt::error(); + } + + auto solver_factory = ebmc_solver_factory(cmdline); + + if(!properties.has_unknown_property()) + return property_checker_resultt{properties}; // done + + message.status() << "No engine given, attempting heuristic engine selection" + << messaget::eom; + + // First try 1-induction, word-level + message.status() << "Attempting 1-induction" << messaget::eom; + + k_induction( + 1, transition_system, properties, solver_factory, message_handler); + + properties.reset_failure_to_unknown(); + + if(!properties.has_unknown_property()) + return property_checker_resultt{properties}; // done + + // Now try BMC with bound 5, word-level + + bmc( + 5, // bound + false, // convert_only + cmdline.isset("bmc-with-assumptions"), + transition_system, + properties, + solver_factory, + message_handler); + + properties.reset_failure_to_unknown(); + + if(!properties.has_unknown_property()) + return property_checker_resultt{properties}; // done + + // Give up + return property_checker_resultt{properties}; // done +} + property_checker_resultt property_checker( const cmdlinet &cmdline, transition_systemt &transition_system, @@ -371,6 +424,7 @@ property_checker_resultt property_checker( } else if(cmdline.isset("aig") || cmdline.isset("dimacs")) { + // bit-level BMC return bit_level_bmc( cmdline, transition_system, properties, message_handler); } @@ -388,12 +442,18 @@ property_checker_resultt property_checker( cmdline, transition_system, properties, message_handler); #endif } - else + else if(cmdline.isset("bound")) { - // default engine is word-level BMC + // word-level BMC return word_level_bmc( cmdline, transition_system, properties, message_handler); } + else + { + // heuristic engine selection + return engine_heuristic( + cmdline, transition_system, properties, message_handler); + } }(); if(result.status == property_checker_resultt::statust::VERIFICATION_RESULT)