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 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

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