PINMUX DV document
Goals
-
DV:
- PINMUX is decided to verify in FPV only
-
FPV:
- Verify all the PINMUX 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 PINMUX design features, please see the PINMUX design specification.
Testbench architecture
PINMUX FPV testbench has been constructed based on the formal architecture.
Block diagram
TLUL assertions
- The
../fpv/tb/pinmux_bind.sv
binds thetlul_assert
assertions with pinmux to ensure TileLink interface protocol compliance - The
../fpv/tb/pinmux_bind.sv
also binds thepinmux_csr_assert_fpv
to assert the TileLink writes and reads correctly
PINMUX assertions
- The
../fpv/tb/pinmux_bind_fpv.sv
binds modulepinmux_assert_fpv
with the pinmux RTL. The assertion file ensures pinmux’s outputs (mio_out_o
,mio_oe_o
, andmio_to_periph_o
) are verified.
Symbolic variables
Due to there are large number of peripheral and muxed inputs, the symbolic variable is used to reduce the number of repeated assertions code.
In the pinmux_assert_fpv module, we declared two symbolic variables mio_sel_i
and periph_sel_i
to represent the index for muxed and peripheral IO.
Detailed explanation is listed in the Symbolic Variables section.
DV plan
Milestone | Name | Description | Tests |
---|---|---|---|
V2 | InSel0_A | When register periph_insel is set to 0, the corresponding mio_to_periph_o must be 0. | pinmux_assert |
V2 | InSel1_A | When register periph_insel is set to 1, the corresponding mio_to_periph_o must be 1. | pinmux_assert |
V2 | InSelN_A | When register periph_insel is set to any value between 2 and (2 + number of MioPads), the corresponding mio_to_periph_o must be equal to the related mio_in_i value. | pinmux_assert |
V2 | InSelOOB_A | When register periph_insel is set to any value larger than (2 + number of MioPads), the corresponding mio_to_periph_o must be 0. | pinmux_assert |
V2 | MioToPeriphO_A | This assertion checks that any changes from the mio_to_periph_o output are due to the changes from either mio_in_i or register periph_insel. | pinmux_assert |
V2 | OutSel0_A | When register mio_outsel is set to 0, the corresponding mio_out_o must be 0. | pinmux_assert |
V2 | OutSel1_A | When register mio_outsel is set to 1, the corresponding mio_out_o must be 1. | pinmux_assert |
V2 | OutSel2_A | When register mio_outsel is set to 2, the corresponding mio_out_o must be 0. | pinmux_assert |
V2 | OutSelN_A | When register mio_outsel is set to any value between 3 and (3 + Number of periph out), the corresponding mio_out_o must be equal to the related periph_to_mio_i value. | pinmux_assert |
V2 | OutSelOOB_A | When register mio_outsel is set to any value larger than (3 + Number of periph out), the corresponding mio_out_o must be 0. | pinmux_assert |
V2 | MioOutO_A | This assertion checks that any changes from the mio_out_o output are due to the changes from either periph_to_mio_i or register mio_outsel. | pinmux_assert |
V2 | OutSelOe0_A | When register mio_outsel is set to 0, the corresponding mio_oe_o must be 0. | pinmux_assert |
V2 | OutSelOe1_A | When register mio_outsel is set to 1, the corresponding mio_oe_o must be 1. | pinmux_assert |
V2 | OutSelOe2_A | When register mio_outsel is set to 2, the corresponding mio_out_o must be 0. | pinmux_assert |
V2 | OutSelOeN_A | When register mio_outsel is set to any value between 3 and (3 + Number of periph out), the corresponding mio_oe_o must be equal to the related periph_to_mio_oe_i value. | pinmux_assert |
V2 | OutSelOeOOB_A | When register mio_outsel is set to any value larger than (3 + Number of periph out), the corresponding mio_oe_o must be 0. | pinmux_assert |
V2 | MioOeO_A | This assertion checks that any changes from the mio_oe_o output are due to the changes from either periph_to_mio_oe_i or register mio_outsel. | pinmux_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. | pinmux_fpv_csr_rw |