Cover property erroneously getting refuted under bounded model checking

[ShashankVM]

Here is my project:

https://github.com/ShashankVM/hamming_encoder_decoder_bmc

The cover property here on line 65 is getting refuted. https://github.com/ShashankVM/hamming_encoder_decoder_bmc/blob/master/dut.sv#L65

Run command:
ebmc -D FORMAL --bound 100 --top dut dut.sv cc_encoder.sv piso.sv lfsr_encoder.sv cc_decoder_ht.sv lfsr_decoder.sv buffer_reg.sv error_correction_and_detection.sv channel.sv --reset reset==1 --vcd wave.vcd

It is expected to be covered as there is no constraint on the input signal message that prevents it from being zero. I've not been successful in generating a waveform via VCD file that can visualize the design behaviour using the HW-CBMC tool.

k-induction and bdd also fails.

[kroening]

Can you confirm whether this is now fixed?

[ShashankVM]

Thank you, Dr. Daniel. Yes it's fixed for the bounded model checking. K-induction and BDD does not work. You may close this issue.

[kroening]

cover properties are existential. k-induction or BDDs can only refute them, not prove them.

[kroening]

Closing as fixed

[ShashankVM]

Closing as fixed

Hi Dr. Daniel, this bug is back again. I installed ebmc 5.7 from releases page Debian package.
Steps to reproduce the bug:

1. git clone https://github.com/ShashankVM/hamming_encoder_decoder_bmc
2. ebmc -D FORMAL --bound 100 --top dut dut.sv cc_encoder.sv piso.sv lfsr_encoder.sv cc_decoder_ht.sv lfsr_decoder.sv buffer_reg.sv error_correction_and_detection.sv channel.sv --reset reset==1 --trace --vcd wave.vcd

Output:

SAT checker inconsistent: instance is UNSATISFIABLE
UNSAT: No path found within bound

** Results:
[dut.ASSUME_STABLE_MESSAGE] always (disable iff (dut.reset) ($fell(dut.encoder_ready) or !dut.encoder_ready) |-> $stable(dut.message)): ASSUMED
[dut.ASSUME_STABLE_ERROR_INJECT] always (disable iff (dut.reset) ($fell(dut.encoder_ready) or !dut.encoder_ready) |-> $stable(dut.error_inject)): ASSUMED
[dut.ASSUME_STABLE_ERROR_POSITION1] always (disable iff (dut.reset) ($fell(dut.encoder_ready) or !dut.encoder_ready) |-> $stable(dut.error_pos1)): ASSUMED
[dut.ASSUME_STABLE_ERROR_POSITION2] always (disable iff (dut.reset) ($fell(dut.encoder_ready) or !dut.encoder_ready) |-> $stable(dut.error_pos2)): ASSUMED
[dut.ASSUME_VALID_ERROR_POSITION1] always (disable iff (dut.reset) dut.error_pos1 < 3'b111): ASSUMED
[dut.ASSUME_VALID_ERROR_POSITION2] always (disable iff (dut.reset) dut.error_pos2 < 3'b111): ASSUMED
[dut.ASSERT_RX_EQUAL_TX_NO_INJECTION] always (disable iff (dut.reset) dut.rx_valid && !dut.error_inject_reg |-> dut.tx_final == dut.rx): PROVED up to bound 100
[dut.ASSERT_RX_EQUAL_TX_SINGLE_ERROR_WITH_INJECTION] always (disable iff (dut.reset) dut.rx_valid && $past(dut.error_pos1) == $past(dut.error_pos2) && dut.error_inject_reg |-> dut.tx_final == dut.rx): PROVED up to bound 100
[dut.ASSERT_RX_NOT_EQUAL_TX_FOR_DOUBLE_ERROR] always (disable iff (dut.reset) dut.rx_valid && $past(dut.error_pos1) != $past(dut.error_pos2) && dut.error_inject_reg |-> dut.tx_final != dut.rx): PROVED up to bound 100
[dut.ASSERT_ENCODER_LATENCY] always (disable iff (dut.reset) $rose(dut.encoder_ready) |-> (##7 dut.encoder_ready)): PROVED up to bound 100
[dut.ASSERT_DECODER_LATENCY] always (disable iff (dut.reset) $rose(dut.rx_valid) |-> (##7 dut.rx_valid)): PROVED up to bound 100
[dut.ASSERT_ERROR_DET_IF_ERROR_INJECT] always (disable iff (dut.reset) dut.rx_valid && dut.error_inject_reg |-> dut.error_det): PROVED up to bound 100
[dut.ASSERT_ERROR_DET_IMPLIES_ERROR_INJECT] always (disable iff (dut.reset) dut.error_det |-> dut.error_inject_reg): PROVED up to bound 100
[dut.ASSERT_RX_EVENTUALLY] always (disable iff (dut.reset) s_eventually dut.rx_valid): PROVED up to bound 100
[dut.COVER_ZERO_MESSAGE] cover (disable iff (dut.reset) dut.message == 4'b0000): REFUTED up to bound 100
[dut.COVER_NON_ZERO_MESSAGE] cover (disable iff (dut.reset) dut.message != 4'b0000): REFUTED up to bound 100
[dut.COVER_ERROR_INJECT_OFF] cover (disable iff (dut.reset) !dut.error_inject ##9 dut.error_inject): REFUTED up to bound 100
[dut.COVER_ERROR_DET] cover (disable iff (dut.reset) dut.error_det): REFUTED up to bound 100
[dut.COVER_NO_VACUOUS_PASS] cover (disable iff (dut.reset) dut.rx_valid && dut.error_inject_reg && dut.error_pos1 == dut.error_pos2 && dut.tx_final == dut.rx): REFUTED up to bound 100

[kroening]

This appears to have happened with #1271 -- I'll investigate.