Skip to content

Pma assertions

Created by: silabs-robin

This PR adds assertions for the PMA.

It adds a IS_INSTR_SIDE parameter to the sva module and also a few signals for connecting to the obi bus. Then it adds the assertions themselves (according to the PMA vPlan) plus some helper logic. Covers were added to make sure formal isn't overconstrained, to guide simulation testing, and for the insight they provide.

NB. I did not get anyone else to review the assertions (neither the assertions alone or compared to the vPlan).

NB. Formal fails because all coverage is not reachable from all pma configs. I did not figure out a solution to this.

Merge request reports

Loading