Skip to content

Interrupt assert fixes

Created by: silabs-robin

This PR updates 2 assertions about interrupts for 40x.

It updates p_wfi_assert_core_sleep_o by simplifying the antecedent and adding a condition that there are no outstanding transactions (otherwise formal can just delay obi indefinitely and pass vacuously). And I made p_wfi_assert_core_sleep_o_cond because the old assert seems to be a "relic" from 40p and I wanted to check the same thing just a bit different.

p_wfi_wake_to_instr_fetch was similarly updated with heed to obi, so that formal don't just delay indefinitely.

Otherwise, some minor fixes like renaming some signals and adding obi err condition to is_wfi.

Merge request reports

Loading