# 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

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

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