Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Properties erroneously getting refuted #638

Open
ShashankVM opened this issue Aug 15, 2024 · 0 comments
Open

Properties erroneously getting refuted #638

ShashankVM opened this issue Aug 15, 2024 · 0 comments

Comments

@ShashankVM
Copy link

In this project: https://github.com/ShashankVM/formal_verif_ecc

Results as follows:

** Results:
[top.ASSUME_VALID_ERROR_POS1] always top.error_pos1 <= 38 && top.error_pos1 >= 0: ASSUMED
[top.ASSUME_VALID_ERROR_POS2] always top.error_pos2 <= 38 && top.error_pos2 >= 0 && top.error_pos1 != top.error_pos2: ASSUMED
[top.ASSUME_DECODER_ENABLE] always top.decoder_en == 1'b1: ASSUMED
[top.ASSERT_ERROR_PRESENT] always top.encoded_data != top.received_data: PROVED up to bound 1
[top.ASSERT_DATA_RECOVERED] always (!top.sed_ded |-> top.corrected_data == top.encoded_data): REFUTED
[top.ASSERT_SINGLE_ECC] always (!top.sed_ded |-> top.single_ecc_error == 1'b1): REFUTED
[top.ASSERT_NO_DOUBLE_ED] always (!top.sed_ded |-> top.double_ecc_error == 1'b0): REFUTED
[top.ASSERT_DATA_NOT_RECOVERED] always (top.sed_ded |-> top.corrected_data != top.encoded_data): REFUTED
[top.ASSERT_NO_SINGLE_ECC] always (top.sed_ded |-> top.single_ecc_error == 1'b0): PROVED up to bound 1
[top.ASSERT_DOUBLE_ED] always (top.sed_ded |-> top.double_ecc_error == 1'b1): REFUTED
[top.COVER_ALL_0] cover top.encoded_data == 0: PROVED
[top.COVER_NON_0] cover top.encoded_data != 0: PROVED
[top.COVER_ERROR_0_POS] cover top.error_pos1 == 6'b0: PROVED
[top.COVER_ERROR_38_POS] cover top.error_pos1 == 6'b100110: PROVED
[top.COVER_ERROR_9_POS] cover top.error_pos1 == 6'b1001: PROVED
[top.COVER_ERROR_24_POS] cover top.error_pos1 == 6'b11000: PROVED
[top.COVER_SED_DED_ZERO] cover top.sed_ded == 1'b0: PROVED
[top.COVER_SED_DED_ONE] cover top.sed_ded == 1'b1: PROVED

Command used:
ebmc --systemverilog --top top top.sv rvecc_encode.sv channel_model.sv rvecc_decode.sv --vcd wave.vcd
Although all properties are expected to be proven, some are getting refuted. I've verified this using a proprietary tool and it's proven using that tool.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant