PINMUX DV document

Goals

DV:
- TODO: Add a UVM testbench to reuse auto-generated common tests for TLUL and alerts.
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 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 the tlul_assert assertions with pinmux to ensure TileLink interface protocol compliance.
The ../fpv/tb/pinmux_bind.sv also binds the pinmux_csr_assert_fpv to assert the TileLink writes and reads correctly.

PINMUX assertions

The ../fpv/tb/pinmux_bind_fpv.sv binds module pinmux_assert_fpv with the pinmux RTL. The assertion file ensures all pinmux’s outputs are verified based on the testplan.

In the pinmux design, it includes usbdev logic because it operates on an always-on domain. Pinmux FPV assertions will only cover the connectivities between usbdev IOs and pinmux IOs. All functional checks will be implemented in the usbdev testbench.

Symbolic variables

Due to the large number of peripheral, muxed, dedicated IOs, and wakeup causes, symbolic variables are used to reduce the number of repeated assertions code. In the pinmux_assert_fpv module, we declared four symbolic variables (mio_sel_i, periph_sel_i, dio_sel_i, wkup_sel_i) to represent the index for muxed IOs, peripheral IOs, dedicated IOs, and wakeup causes. Detailed explanation is listed in the Symbolic Variables section.

Testplan

Testpoints

Milestone	Name	Tests	Description
V1	InSel0_A	pinmux_assert	When register `periph_insel` is set to 0, which means the selected input is constant zero, the corresponding `mio_to_periph_o` must be 0.
V1	InSel1_A	pinmux_assert	When register `periph_insel` is set to 1, which means the selected input is constant one, the corresponding `mio_to_periph_o` must be 1.
V1	InSelN_A	pinmux_assert	When register `periph_insel` is set to any value between 2 and (2 + number of MioPads) and the select index is not jtag, the corresponding `mio_to_periph_o` must be equal to the related `mio_in_i` value.
V1	InSelOOB_A	pinmux_assert	When register `periph_insel` is set to any value larger than (2 + number of MioPads), the corresponding `mio_to_periph_o` must be 0.
V1	DioInSelN_A	pinmux_assert	This assertion checks that `dio_to_periph_o` is directly connected to `dio_in_i`.
V1	OutSel0_A	pinmux_assert	When register `mio_outsel` is set to 0 and is not in sleep mode or jtag, which means the selected output is constant zero, the corresponding `mio_out_o` must be 0.
V1	OutSel1_A	pinmux_assert	When register `mio_outsel` is set to 1 and is not in sleep mode or jtag, which means the selected output is constant one, the corresponding `mio_out_o` must be 1.
V1	OutSel2_A	pinmux_assert	When register `mio_outsel` is set to 2 and is not in sleep mode or jtag, which means the selected output is driving high-Z, the corresponding `mio_out_o` must be 0.
V1	OutSelN_A	pinmux_assert	When register `mio_outsel` is set to any value between 3 and (3 + Number of periph out) and is not in sleep mode or jtag, the corresponding `mio_out_o` must be equal to the related `periph_to_mio_i` value.
V1	OutSelOOB_A	pinmux_assert	When register `mio_outsel` is set to any value larger than (3 + Number of periph out) and is not in sleep mode, the corresponding `mio_out_o` must be 0.
V1	OutSelOe0_A	pinmux_assert	When register `mio_outsel` is set to 0 and is not in sleep mode or jtag, the corresponding `mio_oe_o` must be 1.
V1	OutSelOe1_A	pinmux_assert	When register `mio_outsel` is set to 1 and is not in sleep mode or jtag, the corresponding `mio_oe_o` must be 1.
V1	OutSelOe2_A	pinmux_assert	When register `mio_outsel` is set to 2 and is not in sleep mode or jtag, which indicates driving high-Z to the selected output, the corresponding `mio_oe_o` must be 0.
V1	OutSelOeN_A	pinmux_assert	When register `mio_outsel` is set to any value between 3 and (3 + Number of periph out) and is not in sleep mode or jtag, the corresponding `mio_oe_o` must be equal to the related `periph_to_mio_oe_i` value.
V1	OutSelOeOOB_A	pinmux_assert	When register `mio_outsel` is set to any value larger than (3 + Number of periph out) and is not in sleep mode, the corresponding `mio_oe_o` must be 0.
V1	MioSleepMode0_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 0, which means the pad is driven zero in deep sleep mode. If, in the meantime, register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_out_o` must be 0.
V1	MioSleepMode1_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 1, which means the pad is driven one in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_out_o` must be 1.
V1	MioSleepMode2_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 2, which means the pad is driven high-Z in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_out_o` must be 0.
V1	MioSleepMode3_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 3, which means the pad keeps last driven value in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_out_o` should be stable.
V1	MioSleepStable_A	pinmux_assert	If not at posedge of `sleep_en_i`, and in the meantime register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_out_o` should be stable.
V1	MioOeSleepMode0_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 0, which means the pad is driven zero in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_oe_o` must be 1.
V1	MioOeSleepMode1_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 1, which means the pad is driven one in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_oe_o` must be 1.
V1	MioOeSleepMode2_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 2, which means the pad is driven high-Z in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_oe_o` must be 0.
V1	MioOeSleepMode3_A	pinmux_assert	At posedge of `sleep_en_i`, if register `mio_pad_sleep_en` is 1 and `mio_pad_sleep_mode` is 3, which means the pad keeps last driven value in deep sleep mode. In the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_oe_o` should be stable.
V1	MioOeSleepStable_A	pinmux_assert	If not at posedge of `sleep_en_i`, and in the meantime, if register `mio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `mio_oe_o` should be stable.
V1	DOutSelN_A	pinmux_assert	`dio_out_o` is connected to `periph_to_dio_i` if not in sleep mode.
V1	DOutSelOeN_A	pinmux_assert	`dio_oe_o` is connected to `periph_to_dio_oe_i` if not in sleep mode.
V1	DioSleepMode0_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 0, which means the pad is driven zero in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_out_o` must be 0.
V1	DioSleepMode1_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 1, which means the pad is driven one in deep sleep mode. In the meantime, if register `dmio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_out_o` must be 1.
V1	DioSleepMode2_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 2, which means the pad is driven high-Z in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_out_o` must be 0.
V1	DioSleepMode3_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 3, which means the pad keeps last driven value in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_out_o` should be stable.
V1	DioSleepStable_A	pinmux_assert	If not at posedge of `sleep_en_i`, and in the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_out_o` should be stable.
V1	DioOeSleepMode0_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 0, which means the pad is driven zero in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_oe_o` must be 1.
V1	DioOeSleepMode1_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 1, which means the pad is driven one in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_oe_o` must be 1.
V1	DioOeSleepMode2_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 2, which means the pad is driven high-Z in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_oe_o` must be 0.
V1	DioOeSleepMode3_A	pinmux_assert	At posedge of `sleep_en_i`, if register `dio_pad_sleep_en` is 1 and `dio_pad_sleep_mode` is 3, which means the pad keeps last driven value in deep sleep mode. In the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_oe_o` should be stable.
V1	DioOeSleepStable_A	pinmux_assert	If not at posedge of `sleep_en_i`, and in the meantime, if register `dio_pad_sleep_status` is not written via TLUL interface to clear the sleep status, the corresponding `dio_oe_o` should be stable.
V1	MioAttrO_A	pinmux_assert	`mio_attr_o` should be equal to corresponding `mio_pad_attr` register value and TargetCfg's mio_pad_type configuration.
V1	MioJtagAttrO_A	pinmux_assert	If jtag is enabled, the jtag `mio_attr_o` index should be equal to 0.
V1	DioAttrO_A	pinmux_assert	`dio_attr_o` should be equal to corresponding `dio_pad_attr` register value and TargetCfg's dio_pad_type configuration.
V1	WkupPosedge_A	pinmux_assert	When register `wkup_detector_en` is set to 1 and `wkup_detector.mode` is set to 0, which means rising edge is used to detect wakeup. If variable `final_pin_val` is at posedge then `wkup_cause` register's `de` attribute should be set to 1.
V1	WkupNegedge_A	pinmux_assert	When register `wkup_detector_en` is set to 1 and `wkup_detector.mode` is set to 1, which means falling edge is used to detect wakeup. If variable `final_pin_val` is at negedge, then `wkup_cause` register's `de` attribute should be set to 1.
V1	WkupEdge_A	pinmux_assert	When register `wkup_detector_en` is set to 1 and `wkup_detector.mode` is set to 2, which means either rising or falling edge is used to detect wakeup. If variable `final_pin_val` is at posedge or negedge, then `wkup_cause` register's `de` attribute should be set to 1.
V1	WkupTimedHigh_A	pinmux_assert	When register `wkup_detector_en` is set to 1 and `wkup_detector.mode` is set to 3, which means postive pulse cycles are used to detect wakeup. If variable `final_pin_val` stays high longer than the threshold, then `wkup_cause` register's `de` attribute should be set to 1.
V1	WkupTimedLow_A	pinmux_assert	When register `wkup_detector_en` is set to 1 and `wkup_detector.mode` is set to 4, which means negative pulse cycles are used to detect wakeup. If variable `final_pin_val` stays low longer than the threshold, then `wkup_cause` register's `de` attribute should be set to 1.
V1	WkupCauseQ_A	pinmux_assert	When `wkup_cause` register's `de` attribute is set to 1 and user is not writing to `wkup_cause` at the same cycle, then `wkup_cause.q` should be set to 1.
V1	AonWkupO_A	pinmux_assert	When register `wkup_cause` is 1, `pin_wkup_req_o` should also be 1. `pin_wkup_req_o` is 0 only when all `wkup_cause` registers are 0.
V1	LcJtagWoScanmode_A	pinmux_assert	Not in scanmode, when tap_strap select LC_tap, `lc_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration.
V1	LcJtagWScanmode_A	pinmux_assert	In scanmode, when tap_strap select LC_tap, `lc_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration except the `jtag_trst` pin, which must be equal to `rst_ni`.
V1	LcJtagODefault_A	pinmux_assert	`lc_jtag_o` should stay 0 if tap_strap did not select LC_tap.
V1	RvJtagWoScanmode_A	pinmux_assert	Not in scanmode, when tap_strap select RV_tap and `lc_hw_debug_en_i` input is On for the past two clock cycles due to the synchronizer, then `rv_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration.
V1	RvJtagWScanmode_A	pinmux_assert	In scanmode, When tap_strap select RV_tap and `lc_hw_debug_en_i` is On for the past two clock cycles due to the synchronizer, then `rv_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration except the `jtag_trst` pin, which must be equal to `rst_ni`.
V1	RvJtagODefault_A	pinmux_assert	`rv_jtag_o` should stay 0 if tap_strap did not select RV_tap or `lc_hw_debug_en_i` input is Off for the past two clock cycles due to the synchronizer.
V1	DftJtagWoScanmode_A	pinmux_assert	Not in scanmode, when tap_strap select DFT_tap and `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, `lc_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration.
V1	DftJtagWScanmode_A	pinmux_assert	In scanmode, when tap_strap select DFT_tap and `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, `lc_jtag_o` must be equal to the corresponding `mio_in_i` pins based on the `TargetCfg` configuration except the `jtag_trst` pin, which must be equal to `rst_ni`.
V1	DftJtagODefault_A	pinmux_assert	`dft_jtag_o` should stay 0 if tap_strap did not select DFT_tap or the `lc_dft_en_i` input is Off for the past two clock cycles due to the synchronizer.
V1	TapStrap_A	pinmux_assert	If `dft_hold_tap_sel_i` is 0 and `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, or `strap_en_i` is 1. And in the meantime, if `lc_hw_debug_en_i` is On for the past two clock cycles due to the synchronizer, then tap_strap must be equal to the past value of corresponding `mio_in_i`.
V1	TapStrap0_A	pinmux_assert	If `dft_hold_tap_sel_i` is 0 and `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, or `strap_en_i` is 1. Then tap_strap[0] must be equal to the past value of corresponding `mio_in_i`.
V1	LcJtagI_A	pinmux_assert	When Lc tap is selected, the corresponding `mio_out_o` and `mio_out_oe` should be equal to `lc_jtag_i`.
V1	RvJtagI_A	pinmux_assert	When Rv tap is selected and `lc_hw_debug_en_i` is On for the past two clock cycles due to the synchronizer, the corresponding `mio_out_o` and `mio_out_oe` should be equal to `rv_jtag_i`.
V1	DftJtagI_A	pinmux_assert	When Dft tap is selected and `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, the corresponding `mio_out_o` and `mio_out_oe` should be equal to `dft_jtag_i`.
V1	DftStrapTestO_A	pinmux_assert	When `lc_dft_en_i` is On for the past two clock cycles due to the synchronizer, `dft_strap_test_o.valid` must be 1, and `dft_strap_test_o.straps` should be equal to the corresponding `mio_in_i` index.
V1	DftStrapTestOValidStable_A	pinmux_assert	`dft_strap_test_o.valid` once set to 1 will stay high until reset.
V1	DftStrapTestOStrapStable_A	pinmux_assert	`dft_strap_test_o.valid` once set, `dft_strap_test_o.straps` should stay stable.
V1	UsbSleepEnI_A	pinmux_assert	`sleep_en_i` should be connected directly to usbdev's `low_power_alw_i`.
V1	UsbDppullupEnUpwrI_A	pinmux_assert	`usb_dppullup_en_upwr_i` should be connected directly to usbdev's `usb_dppullup_en_upwr_i`.
V1	UsbDnpullupEnUpwrI_A	pinmux_assert	`usb_dnpullup_en_upwr_i` should be connected directly to usbdev's `usb_dnpullup_en_upwr_i`.
V1	UsbDppullupEnO_A	pinmux_assert	`usb_dppullup_en_o` should be connected directly to usbdev's `usb_dppullup_en_o`.
V1	UsbDnpullupEnO_A	pinmux_assert	`usb_dnpullup_en_o` should be connected directly to usbdev's `usb_dnpullup_en_o`.
V1	UsbOutOfRstI_A	pinmux_assert	`usb_out_of_rst_i` should be connected directly to usbdev's `usb_out_of_rst_upwr_i`.
V1	UsbAonWakeEnUpwrI_A	pinmux_assert	`usb_aon_wake_en_i` should be connected directly to usbdev's `usb_aon_wake_en_upwr_i`.
V1	UsbAonWakeAckUpwrI_A	pinmux_assert	`usb_aon_wake_ack_i` should be connected directly to usbdev's `usb_aon_woken_upwr_i`.
V1	UsbSuspendI_A	pinmux_assert	`usb_suspend_i` should be connected directly to usbdev's `usb_suspended_upwr_i`.
V1	UsbWkupReqO_A	pinmux_assert	`usb_wkup_req_o` should be connected directly to usbdev's `wake_rep_alw_o`.
V1	UsbBusResetO_A	pinmux_assert	`usb_bus_reset_o` should be connected directly to usbdev's `bus_reset_alw_o`.
V1	UsbSenseLostO_A	pinmux_assert	`usb_sense_lost_o` should be connected directly to usbdev's `bus_lost_alw_o`.
V1	UsbStateDebugO_A	pinmux_assert	`usb_state_debug_o` should be connected directly to usbdev's `bus_debug_o`.
V2	MioToPeriph0Backward_A	pinmux_assert	`mio_to_periph_o` should output 0 only if one of the following conditions meets: Register `periph_insel` is set to 0. The corresponding `mio_in_i` is 0. Jtag is enabled.
V2	MioToPeriph1Backward_A	pinmux_assert	`mio_to_periph_o` should output 1 only if one of the following conditions meets: Register `periph_insel` is set to 1. The corresponding `mio_in_i` is 1. Jtag is enabled.
V2	MioOut0Backward_A	pinmux_assert	`mio_out_o` should output 0 only if one of the following conditions meets: Register `mio_insel` is set to 0 or 2. The corresponding `periph_to_mio_i` is 0. Sleep mode is enabled.
V2	MioOut1Backward_A	pinmux_assert	`mio_out_o` should output 1 only if one of the following conditions meets: Register `mio_insel` is set to 1. The corresponding `periph_to_mio_i` is 1. Sleep mode is enabled.
V2	MioOe0Backward_A	pinmux_assert	`mio_oe_o` should output 0 only if one of the following conditions meets: Register `mio_insel` is set to 2. The corresponding `periph_to_mio_oe_i` is 0. Sleep mode is enabled.
V2	MioOe1Backward_A	pinmux_assert	`mio_oe_o` should output 1 only if one of the following conditions meets: Register `mio_insel` is set to 0 or 1. The corresponding `periph_to_mio_oe_i` is 1. Sleep mode is enabled.
V2	MioSleep0Backward_A	pinmux_assert	`mio_out_o` should output 0 only if one of the following conditions meets: In sleep mode, register `mio_pad_sleep_mode` is set to 0 or 2. In sleep mode, previous `mio_out_o` is 0 and `mio_pad_sleep_mode` is set to 3. In sleep mode, previous `mio_out_o` is 0 and input `sleep_en_i` is not at posedge.
V2	MioSleep1Backward_A	pinmux_assert	`mio_out_o` should output 1 only if one of the following conditions meets: In sleep mode, register `mio_pad_sleep_mode` is set to 1. In sleep mode, previous `mio_out_o` is 1 and `mio_pad_sleep_mode` is set to 3. In sleep mode, previous `mio_out_o` is 1 and input `sleep_en_i` is not at posedge.
V2	MioOeSleep0Backward_A	pinmux_assert	`mio_oe_o` should output 0 only if one of the following conditions meets: In sleep mode, register `mio_pad_sleep_mode` is set to 2. In sleep mode, previous `mio_oe_o` is 0 and `mio_pad_sleep_mode` is set to 3. In sleep mode, previous `mio_oe_o` is 0 and input `sleep_en_i` is not at posedge.
V2	MioOeSleep1Backward_A	pinmux_assert	`mio_oe_o` should output 1 only if one of the following conditions meets: In sleep mode, register `mio_pad_sleep_mode` is set to 0 or 1. In sleep mode, previous `mio_oe_o` is 1 and `mio_pad_sleep_mode` is set to 3. In sleep mode, previous `mio_oe_o` is 1 and input `sleep_en_i` is not at posedge.
V2	Dio0Backward_A	pinmux_assert	`dio_out_o` should output 0 only if one of the following conditions meets: The corresponding `periph_to_dio_i` is 0. In sleep mode, register `dio_pad_sleep_mode` is set to 0 or 2. In sleep mode, previous `dio_out_o` is 0 and `dio_pad_sleep_mode` is set to 3. In sleep mode, previous `dio_out_o` is 0 and input `sleep_en_i` is not at posedge.
V2	Dio1Backward_A	pinmux_assert	`dio_out_o` should output 1 only if one of the following conditions meets: The corresponding `periph_to_dio_i` is 1. In sleep mode, register `dio_pad_sleep_mode` is set to 1. In sleep mode, previous `dio_out_o` is 1 and `dio_pad_sleep_mode` is set to 3. In sleep mode, previous `dio_out_o` is 1 and input `sleep_en_i` is not at posedge.
V2	DioOe0Backward_A	pinmux_assert	`dio_oe_o` should output 0 only if one of the following conditions meets: The corresponding `periph_to_dio_i` is 0. In sleep mode, register `dio_pad_sleep_mode` is set to 2. In sleep mode, previous `dio_oe_o` is 0 and `dio_pad_sleep_mode` is set to 3. In sleep mode, previous `dio_oe_o` is 0 and input `sleep_en_i` is not at posedge.
V2	DioOe1Backward_A	pinmux_assert	`dio_oe_o` should output 1 only if one of the following conditions meets: The corresponding `periph_to_dio_i` is 1. In sleep mode, register `dio_pad_sleep_mode` is set to 0 or 1. In sleep mode, previous `dio_oe_o` is 1 and `dio_pad_sleep_mode` is set to 3. In sleep mode, previous `dio_oe_o` is 1 and input `sleep_en_i` is not at posedge.
V2	WkupCause0_A	pinmux_assert	Register `wkup_cause` is 0 only when none of the above wakeup conditions is met.
V2	WkupCause1_A	pinmux_assert	Register `wkup_cause` is 1 when at least one of the above wakeup conditions is met.
V2	LcJtagOBackward_A	pinmux_assert	`lc_jtag_o` pins are equal to the corresponding `mio_in_i` inputs if one of the following conditions are met: Lc Jtag is disabled and the corresponding pins are 0. Lc Jtag is enabled.
V2	RvJtagOBackward_A	pinmux_assert	`rv_jtag_o` pins are equal to the corresponding `mio_in_i` inputs if one of the following conditions are met: Rv Jtag is disabled and the corresponding pins are 0. Rv Jtag is enabled.
V2	DftJtagOBackward_A	pinmux_assert	`dft_jtag_o` pins are equal to the corresponding `mio_in_i` inputs if one of the following conditions are met: Dft Jtag is disabled and the corresponding pins are 0. Dft Jtag is enabled.
V2	DftJtagO1Backward_A	pinmux_assert	`dft_jtag_o` pins are ones if one of the following conditions are met: Dft Jtag is enabled and the corresponding pins are 1.
V2	fpv_csr_rw	pinmux_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.