You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When running formal verification of an instruction on a risc-v core, not all assertions in the rvfi_insn_check.sv file are relevant, and can cause a lot of noise in the form of unmet related covers. A good example of this is rs2-related assertions when checking a I-type instruction, as there is no rs2-field, the preconditions can not be met, which shows as an error in the formal verification run.
I propose that these assertions are filtered by ifdef/generate based on instruction type, so the assertion only gets generated if the assertion is relevant for the instruction that is being checked.
The text was updated successfully, but these errors were encountered:
When running formal verification of an instruction on a risc-v core, not all assertions in the rvfi_insn_check.sv file are relevant, and can cause a lot of noise in the form of unmet related covers. A good example of this is rs2-related assertions when checking a I-type instruction, as there is no rs2-field, the preconditions can not be met, which shows as an error in the formal verification run.
I propose that these assertions are filtered by ifdef/generate based on instruction type, so the assertion only gets generated if the assertion is relevant for the instruction that is being checked.
The text was updated successfully, but these errors were encountered: