RV_PLIC DV document

Goals

DV:
- RV_PLIC is decided to verify in FPV only
FPV:
- Verify all the RV_PLIC outputs by writing assumptions and assertions with a FPV based testbench
- Verify TileLink device protocol compliance with a FPV based testbench

Current status

Design & verification stage
- HW development stages
FPV dashboard (link TBD)

Design features

For detailed information on RV_PLIC design features, please see the RV_PLIC design specification.

Testbench architecture

RV_PLIC FPV testbench has been constructed based on the formal architecture.

Block diagram

TLUL assertions

The hw/rv_plic/fpv/tb/rv_plic_bind.sv binds the tlul_assert assertions to rv_plic to ensure TileLink interface protocol compliance.
The hw/rv_plic/fpv/tb/rv_plic_bind.sv also binds the rv_plic_csr_assert_fpv under hw/rv_plic/fpv/vip/ to check if TileLink writes and reads correct CSRs.

RV_PLIC assertions

The hw/rv_plic/fpv/tb/rv_plic_bind.sv binds the rv_plic_assert under hw/rv_plic/fpv/vip/rv_plic_assert.sv. The assertion file ensures RV_PLIC’s outputs (irq_o and irq_id_o) and important signals (ip) are being asserted.

Symbolic variables

Due to there are large number of input interrupt sources, the symbolic variable is used to reduce the number of repeated assertions code. In RV_PLIC, we declared two symbolic variables src_sel and tgt_sel to represent the index for interrupt source and interrupt target. Detailed explanation is listed in the Symbolic Variables section.

DV plan

Milestone	Name	Description	Tests
V2	LevelTriggeredIp_A	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.	rv_plic_assert
V2	EdgeTriggeredIp_A	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.	rv_plic_assert
V2	LevelTriggeredIpWithClaim_A	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.	rv_plic_assert
V2	EdgeTriggeredIpWithClaim_A	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.	rv_plic_assert
V2	IpStableAfterTriggered_A	Once `ip` is set, it stays stable until is being claimed.	rv_plic_assert
V2	IpClearAfterClaim_A	Once `ip` is set and being claimed, its value is cleared to 0.	rv_plic_assert
V2	IpStableAfterClaimed_A	Once `ip` is cleared to 0, it stays stable until completed and being triggered again.	rv_plic_assert
V2	TriggerIrqForwardCheck_A	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.	rv_plic_assert
V2	TriggerIrqBackwardCheck_A	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.	rv_plic_assert
V2	IdChangeWithIrq_A	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	rv_plic_assert
V2	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.	rv_plic_fpv_csr_rw