OBI Assert - Parity (!1776) · Merge requests · OpenHW Group / backup-20241120 / core-v-verif

Eclipse Webmaster requested to merge github/fork/silabs-robin/obi_parity into cv32e40s/dev Mar 30, 2023

Created by: silabs-robin

This PR adds parity asserts (reqpar, etc) to the OBI assertion set, according to OBI v1.2.

Test status:

ci_check - Passes
Internal formal - N/A, not used (passes when enabled)
Cvverif formal - Works as expected (core-side pass, env-side fail)

I did not expect to write this today, but I wanted to see if one of the latest RVFI bug fixes were reproducable with the core-v-verif formal setup and this is the only piece missing that I'm aware of. (OBI parity assumes were already in cvverif fv, but lazily used xsecure asserts.)

OBI Assert - Parity

Merge request reports