- RV_PLIC is decided to verify in FPV only
- 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
For detailed information on RV_PLIC design features, please see the RV_PLIC design specification.
RV_PLIC FPV testbench has been constructed based on the formal architecture.
- The file
tlul_assertassertions to rv_plic to ensure TileLink interface protocol compliance.
hw/rv_plic/fpv/tb/rv_plic_bind.svalso binds the
fpv/vip/to check if TileLink writes and reads correct CSRs.
rv_plic_bind.sv binds the
The assertion file ensures RV_PLIC’s outputs (
irq_id_o) and important signals (
ip) are being asserted.
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
tgt_sel to represent the index for
interrupt source and interrupt target.
Detailed explanation is listed in the
Symbolic Variables section.