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
- 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 thetlul_assert
assertions to rv_plic to ensure TileLink interface protocol compliance. - The
hw/rv_plic/fpv/tb/rv_plic_bind.sv
also binds therv_plic_csr_assert_fpv
underhw/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 ( | rv_plic_assert |
V2 | EdgeTriggeredIp_A | If interrupt pending ( | rv_plic_assert |
V2 | LevelTriggeredIpWithClaim_A | If | rv_plic_assert |
V2 | EdgeTriggeredIpWithClaim_A | If | rv_plic_assert |
V2 | IpStableAfterTriggered_A | Once | rv_plic_assert |
V2 | IpClearAfterClaim_A | Once | rv_plic_assert |
V2 | IpStableAfterClaimed_A | Once | rv_plic_assert |
V2 | TriggerIrqForwardCheck_A | If interrupt is enabled ( | rv_plic_assert |
V2 | TriggerIrqBackwardCheck_A | If | rv_plic_assert |
V2 | IdChangeWithIrq_A | If
| 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 |