From 4b73053abc712fa044b05a6d06b2be9d4fda7ae0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 22 Dec 2024 15:58:59 +0000 Subject: [PATCH] EBMC: basic engine selection heuristic This adds a trivial engine selection heuristic, as follows: 1) First, try 1-induction, which may refute (base case) or prove (step case) the property. 2) If still unresolved, try BMC with bound 5. The heuristic is activated when no engine is specified on the command line. --- CHANGELOG | 2 + regression/ebmc/example1/test.desc | 4 +- .../smv/smv/bmc_unsupported_property1.desc | 2 +- .../smv/smv/bmc_unsupported_property2.desc | 2 +- regression/verilog/SVA/immediate2.desc | 4 +- regression/verilog/SVA/immediate3.desc | 4 +- regression/verilog/SVA/named_property1.desc | 4 +- regression/verilog/SVA/named_sequence1.desc | 4 +- regression/verilog/SVA/sequence5.desc | 4 +- .../verilog/SVA/sequence_first_match1.desc | 2 +- regression/verilog/SVA/sequence_within1.desc | 2 +- regression/verilog/SVA/static_final1.desc | 4 +- regression/verilog/SVA/sva_and1.desc | 4 +- regression/verilog/SVA/sva_iff1.desc | 4 +- regression/verilog/SVA/sva_implies1.desc | 4 +- regression/verilog/SVA/sva_until1.desc | 2 +- .../SVA/system_verilog_assertion3.desc | 2 +- regression/verilog/UDPs/multiplexer1.desc | 2 +- regression/verilog/arrays/array1.desc | 2 +- regression/verilog/arrays/packed_real1.desc | 2 +- .../verilog/arrays/packed_typedef1.desc | 2 +- .../assignments/procedural_assignments1.desc | 2 +- regression/verilog/case/nested_case1.desc | 4 +- regression/verilog/case/riscv-alu.desc | 22 +++---- .../data-types/associative_array1.desc | 2 +- regression/verilog/data-types/chandle1.desc | 6 +- .../data-types/integer_atom_types1.desc | 2 +- regression/verilog/data-types/queue1.desc | 2 +- regression/verilog/data-types/signed1.desc | 2 +- regression/verilog/data-types/signed2.desc | 2 +- .../verilog/data-types/type_operator.desc | 2 +- .../verilog/data-types/vector_types1.desc | 2 +- .../verilog/data-types/vector_types2.desc | 4 +- .../verilog/elaboration/type_operator.desc | 2 +- regression/verilog/elaboration/var_bits.desc | 2 +- regression/verilog/elaboration/wire_bits.desc | 2 +- regression/verilog/enums/enum4.desc | 4 +- regression/verilog/enums/enum5.desc | 2 +- regression/verilog/enums/enum_base_type1.desc | 4 +- regression/verilog/enums/enum_base_type2.desc | 4 +- regression/verilog/enums/enum_cast1.desc | 6 +- .../verilog/enums/enum_initializers1.desc | 6 +- .../verilog/enums/enum_with_hierarchy1.desc | 2 +- .../verilog/expressions/bit-extract3.desc | 12 ++-- .../verilog/expressions/bit-extract4.desc | 2 +- .../verilog/expressions/bit-extract5.desc | 10 +-- .../verilog/expressions/bit-extract6.desc | 6 +- .../verilog/expressions/cast_from_real1.desc | 2 +- .../verilog/expressions/cast_to_real1.desc | 2 +- .../verilog/expressions/cast_to_real2.desc | 2 +- .../verilog/expressions/cast_to_real3.desc | 2 +- .../verilog/expressions/concatenation1.desc | 2 +- .../verilog/expressions/concatenation2.desc | 6 +- .../verilog/expressions/concatenation3.desc | 4 +- .../verilog/expressions/concatenation4.desc | 2 +- .../verilog/expressions/concatenation5.desc | 2 +- .../verilog/expressions/concatenation6.desc | 4 +- .../verilog/expressions/constants2.desc | 2 +- regression/verilog/expressions/equality1.desc | 26 ++++---- regression/verilog/expressions/equality2.desc | 26 ++++---- regression/verilog/expressions/equality3.desc | 2 +- regression/verilog/expressions/iff1.desc | 2 +- regression/verilog/expressions/implies1.desc | 2 +- regression/verilog/expressions/inside1.desc | 14 ++-- regression/verilog/expressions/mod2.desc | 2 +- regression/verilog/expressions/negation1.desc | 2 +- .../expressions/part-select-constant1.desc | 4 +- regression/verilog/expressions/power1.desc | 2 +- regression/verilog/expressions/power2.desc | 2 +- .../verilog/expressions/reduction1.desc | 2 +- .../verilog/expressions/reduction2.desc | 2 +- .../verilog/expressions/replication1.desc | 2 +- .../verilog/expressions/replication2.desc | 2 +- .../verilog/expressions/replication3.desc | 2 +- regression/verilog/expressions/shr2.desc | 2 +- regression/verilog/expressions/signed1.desc | 18 +++--- regression/verilog/expressions/signed2.desc | 2 +- .../verilog/expressions/signing_cast1.desc | 14 ++-- .../verilog/expressions/size_cast1.desc | 10 +-- .../verilog/expressions/static_cast1.desc | 4 +- .../expressions/streaming_concatenation1.desc | 10 +-- .../expressions/streaming_concatenation2.desc | 2 +- .../expressions/wildcard_equality1.desc | 20 +++--- .../expressions/wildcard_equality2.desc | 2 +- regression/verilog/for/break1.desc | 2 +- regression/verilog/for/continue1.desc | 2 +- regression/verilog/for/for_with_reg.desc | 2 +- .../verilog/functioncall/function_ports1.desc | 4 +- .../verilog/functioncall/functioncall1.desc | 4 +- .../verilog/functioncall/functioncall3.desc | 2 +- .../verilog/functioncall/functioncall4.desc | 2 +- .../verilog/functioncall/functioncall5.desc | 2 +- .../verilog/functioncall/functioncall6.desc | 4 +- .../verilog/functioncall/functioncall7.desc | 2 +- .../functioncall_as_constant1.desc | 2 +- .../functioncall/functioncall_as_input1.desc | 2 +- regression/verilog/functioncall/return1.desc | 2 +- .../verilog/functioncall/void_function1.desc | 2 +- .../verilog/generate/generate-for2.desc | 2 +- .../verilog/generate/generate-inst2.desc | 2 +- .../generate/generate-localparam1.desc | 2 +- .../verilog/generate/generate-reg1.desc | 2 +- .../verilog/generate/generate-reg2.desc | 2 +- .../hierarchical_identifiers1.desc | 2 +- regression/verilog/let/let1.desc | 2 +- regression/verilog/let/let_ports1.desc | 2 +- regression/verilog/modules/localparam2.desc | 2 +- regression/verilog/modules/localparam3.desc | 2 +- .../verilog/modules/parameter_ports1.desc | 2 +- .../verilog/modules/parameter_ports2.desc | 2 +- .../verilog/modules/parameter_ports3.desc | 2 +- .../verilog/modules/parameter_ports4.desc | 2 +- regression/verilog/modules/parameters10.desc | 2 +- regression/verilog/modules/parameters4.desc | 2 +- regression/verilog/modules/parameters5.desc | 2 +- regression/verilog/modules/ports3.desc | 2 +- regression/verilog/modules/ports4.desc | 2 +- regression/verilog/modules/ports5.desc | 2 +- regression/verilog/modules/ports6.desc | 2 +- regression/verilog/modules/ports7.desc | 2 +- regression/verilog/modules/ports8.desc | 2 +- .../verilog/modules/type_parameters1.desc | 6 +- .../modules/variable_module_port1.desc | 2 +- regression/verilog/nets/implicit1.desc | 2 +- regression/verilog/nets/implicit2.desc | 2 +- regression/verilog/nets/implicit3.desc | 2 +- regression/verilog/nets/implicit4.desc | 2 +- regression/verilog/nets/implicit5.desc | 2 +- regression/verilog/nets/implicit6.desc | 2 +- regression/verilog/nets/implicit7.desc | 2 +- .../part-select/indexed-part-select1.desc | 2 +- .../part-select/indexed-part-select3.desc | 2 +- .../part-select/indexed-part-select4.desc | 2 +- .../part-select/indexed-part-select5.desc | 2 +- regression/verilog/primitive_gates/nand1.desc | 2 +- regression/verilog/primitive_gates/nand2.desc | 6 +- regression/verilog/primitive_gates/nand4.desc | 2 +- regression/verilog/primitive_gates/nor1.desc | 2 +- regression/verilog/primitive_gates/nor2.desc | 6 +- regression/verilog/primitive_gates/nor4.desc | 2 +- regression/verilog/primitive_gates/not1.desc | 2 +- regression/verilog/primitive_gates/or1.desc | 2 +- regression/verilog/primitive_gates/xnor1.desc | 6 +- regression/verilog/primitive_gates/xnor2.desc | 6 +- regression/verilog/primitive_gates/xnor3.desc | 4 +- regression/verilog/primitive_gates/xnor4.desc | 6 +- .../verilog/string/string_literals1.desc | 2 +- regression/verilog/structs/structs1.desc | 10 +-- regression/verilog/structs/structs2.desc | 2 +- regression/verilog/structs/structs3.desc | 2 +- regression/verilog/structs/structs4.desc | 4 +- regression/verilog/structs/structs5.desc | 8 +-- .../verilog/synthesis/always_comb1.desc | 2 +- .../verilog/synthesis/always_comb2.desc | 8 +-- .../synthesis/continuous_assignment1.desc | 2 +- .../synthesis/continuous_assignment2.desc | 2 +- .../synthesis/continuous_assignment3.desc | 2 +- ...inuous_assignment_to_net_part_select1.desc | 4 +- ..._assignment_to_variable_systemverilog.desc | 4 +- ...assignment_to_variable_systemverilog3.desc | 2 +- ...inuous_assignment_to_variable_verilog.desc | 2 +- .../system-functions/array_functions1.desc | 32 +++++----- .../verilog/system-functions/bits1.desc | 2 +- .../verilog/system-functions/bitstoreal1.desc | 2 +- .../system-functions/bitstoshortreal1.desc | 2 +- .../verilog/system-functions/clog2.desc | 14 ++-- .../verilog/system-functions/countones1.desc | 2 +- .../verilog/system-functions/itor1.desc | 2 +- regression/verilog/system-functions/low1.desc | 2 +- .../verilog/system-functions/realtobits1.desc | 2 +- .../verilog/system-functions/rtoi1.desc | 2 +- .../system-functions/shortrealtobits1.desc | 2 +- .../verilog/system-functions/signed1.desc | 2 +- .../verilog/system-functions/signed2.desc | 10 +-- regression/verilog/system-functions/test.desc | 2 +- .../verilog/system-functions/typename1.desc | 16 ++--- .../verilog/typedef/global_typedef.desc | 2 +- regression/verilog/typedef/typedef1.desc | 2 +- regression/verilog/unions/unions1.desc | 2 +- regression/verilog/unions/unions2.desc | 2 +- regression/verilog/unions/unions3.desc | 2 +- regression/verilog/unions/unions4.desc | 2 +- src/ebmc/ebmc_properties.h | 7 ++ src/ebmc/property_checker.cpp | 64 ++++++++++++++++++- 184 files changed, 422 insertions(+), 353 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 77f8ec1a0..758a0ef44 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)