40x assertions maintenance (!1113) · Merge requests · OpenHW Group / backup-20241120 / core-v-verif

Eclipse Webmaster requested to merge github/fork/silabs-robin/assert_fixes_mpu into cv32e40x/dev Jan 16, 2022

Created by: silabs-robin

This PR fixes some CEXes discovered in formal for "interrupt_assert" and "debug_assert" and it refactors two ebreak exception asserts.

The CEXes in interrupt_assert/debug_assert were caused by MPU errors, where some signals needed to be qualified with "MPU_OK" to be considered valid. The refactor of ebreak exception asserts should fix the duplicate code issue reported in https://github.com/openhwgroup/core-v-verif/issues/1084. Passes ci_check, reduces the number of CEXes in formal.

NB! This PR only fixes some of the CEXes. Since cv32e40x/dev is progressing so much while I am busy with other tasks, and I had to manually resolve merge conflicts for this branch (twice), I thought it could be best to get in a PR in for this now instead of waiting for a time to get the all those CEXes 100% green.

40x assertions maintenance

Merge request reports