| V2 | LevelTriggeredIp_A | rv_plic_assert | If interrupt pending (ip) is triggered, and the level indicator is set to
level triggered (le=0), then in the prvious clock cycle, the interrupt source
(`intr_src_i) should be set to 1. |
| V2 | EdgeTriggeredIp_A | rv_plic_assert | If interrupt pending (ip) is triggered, and the level indicator is set to
edge triggered (le=1), then in the prvious clock cycle, the interrupt source
(`intr_src_i) should be at the rising edge. |
| V2 | LevelTriggeredIpWithClaim_A | rv_plic_assert | If intr_src_i is set to 1, level indicator is set to level triggered, and claim
signal is not set, then at the next clock cycle ip will be triggered. |
| V2 | EdgeTriggeredIpWithClaim_A | rv_plic_assert | If intr_src_i is at the rising edge, level indicator is set to edge triggered, and claim
signal is not set, then at the next clock cycle ip will be triggered. |
| V2 | IpStableAfterTriggered_A | rv_plic_assert | Once ip is set, it stays stable until is being claimed. |
| V2 | IpClearAfterClaim_A | rv_plic_assert | Once ip is set and being claimed, its value is cleared to 0. |
| V2 | IpStableAfterClaimed_A | rv_plic_assert | Once ip is cleared to 0, it stays stable until completed and being triggered
again. |
| V2 | TriggerIrqForwardCheck_A | rv_plic_assert | If interrupt is enabled (ie=1), interrupt pending is set (ip=1), interrupt
input has the highest priority among the rest of the inputs, and its priority is
above the threshold. Then in the next clock clcye, the irq_o should be triggered,
and the irq_id_o will reflect the input ID. |
| V2 | TriggerIrqBackwardCheck_A | rv_plic_assert | If irq_o is set to 1, then in the previous clock cycle, the corresponding
ip should be set, ie should be enabled, and the interrupt source should above the
threshold and have the highest priority. |
| V2 | IdChangeWithIrq_A | rv_plic_assert | If irq_id_o signal is changed and the signal does not change to 0 (value 0 does
not represent any interrupt source ID). Then either of the two condition should have
happened:
irq_o is triggered- No interrupt triggered,
ip is set and ie is enabled, interrupt source priority is the
largest among the rest of the interrupt, but the interrupt source
priority is smaller than the threshold
|
| V2 | fpv_csr_rw | rv_plic_fpv_csr_rw | Write assertions to verify all the CSRs from the TileLink. Each CSR will include a read
assertion to ensure the read value from the TileLink is expected, and a write assertion
to ensure the write value is updated correctly to DUT according to the register's access. |