Property unsupported by k-induction

[ShashankVM]

Project link: https://github.com/ShashankVM/hamming_encoder_decoder_bmc

K-induction run command:
ebmc -D FORMAL --k-induction --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

Here is the output for k-induction:

[dut.ASSUME_STABLE_MESSAGE] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.message)): FAILURE: property unsupported by k-induction
[dut.ASSUME_STABLE_ERROR_INJECT] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_inject)): FAILURE: property unsupported by k-induction
[dut.ASSUME_STABLE_ERROR_POSITION1] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_pos1)): FAILURE: property unsupported by k-induction
[dut.ASSUME_STABLE_ERROR_POSITION2] always (disable iff (dut.reset) $fell(dut.encoder_ready) or !dut.encoder_ready |-> $stable(dut.error_pos2)): FAILURE: property unsupported by k-induction
[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): INCONCLUSIVE
[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): INCONCLUSIVE
[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): INCONCLUSIVE
[dut.ASSERT_ENCODER_LATENCY] always (disable iff (dut.reset) $rose(dut.encoder_ready) |-> (##7 dut.encoder_ready)): FAILURE: property unsupported by k-induction
[dut.ASSERT_DECODER_LATENCY] always (disable iff (dut.reset) $rose(dut.rx_valid) |-> (##7 dut.rx_valid)): FAILURE: property unsupported by k-induction
[dut.ASSERT_ERROR_DET_IF_ERROR_INJECT] always (disable iff (dut.reset) dut.rx_valid && dut.error_inject_reg |-> dut.error_det): INCONCLUSIVE
[dut.ASSERT_ERROR_DET_IMPLIES_ERROR_INJECT] always (disable iff (dut.reset) dut.error_det |-> dut.error_inject_reg): INCONCLUSIVE
[dut.ASSERT_RX_EVENTUALLY] always (disable iff (dut.reset) s_eventually dut.rx_valid): FAILURE: property unsupported by k-induction

Note: I later added an ifdef so covers are not included by default.