RV_PLIC DV Plan

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.

Testplan

Milestone Name Description Tests
V2 LevelTriggeredIp_A <p>If interrupt pending (<code>ip</code>) is triggered, and the level indicator is set to level triggered (<code>le=0</code>), then in the prvious clock cycle, the interrupt source (`intr_src_i) should be set to 1.</p> rv_plic_assert<br>
V2 EdgeTriggeredIp_A <p>If interrupt pending (<code>ip</code>) is triggered, and the level indicator is set to edge triggered (<code>le=1</code>), then in the prvious clock cycle, the interrupt source (`intr_src_i) should be at the rising edge.</p> rv_plic_assert<br>
V2 LevelTriggeredIpWithClaim_A<p>If <code>intr_src_i</code> is set to 1, level indicator is set to level triggered, and claim signal is not set, then at the next clock cycle <code>ip</code> will be triggered.</p> rv_plic_assert<br>
V2 EdgeTriggeredIpWithClaim_A <p>If <code>intr_src_i</code> is at the rising edge, level indicator is set to edge triggered, and claim signal is not set, then at the next clock cycle <code>ip</code> will be triggered.</p> rv_plic_assert<br>
V2 IpStableAfterTriggered_A <p>Once <code>ip</code> is set, it stays stable until is being claimed.</p> rv_plic_assert<br>
V2 IpClearAfterClaim_A <p>Once <code>ip</code> is set and being claimed, its value is cleared to 0.</p>rv_plic_assert<br>
V2 IpStableAfterClaimed_A <p>Once <code>ip</code> is cleared to 0, it stays stable until completed and being triggered again.</p> rv_plic_assert<br>
V2 TriggerIrqForwardCheck_A <p>If interrupt is enabled (<code>ie=1</code>), interrupt pending is set (<code>ip=1</code>), 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 <code>irq_o</code> should be triggered, and the <code>irq_id_o</code> will reflect the input ID.</p> rv_plic_assert<br>
V2 TriggerIrqBackwardCheck_A <p>If <code>irq_o</code> is set to 1, then in the previous clock cycle, the corresponding <code>ip</code> should be set, <code>ie</code> should be enabled, and the interrupt source should above the threshold and have the highest priority.</p> rv_plic_assert<br>
V2 IdChangeWithIrq_A <p>If <code>irq_id_o</code> 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:</p> <ul> <li><code>irq_o</code> is triggered</li> <li>No interrupt triggered, <code>ip</code> is set and <code>ie</code> is enabled, interrupt source priority is the largest among the rest of the interrupt, but the interrupt source priority is smaller than the threshold</li> </ul> rv_plic_assert<br>
V2 fpv_csr_rw <p>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.</p> rv_plic_fpv_csr_rw<br>