| // Copyright lowRISC contributors. |
| // Licensed under the Apache License, Version 2.0, see LICENSE for details. |
| // SPDX-License-Identifier: Apache-2.0 |
| // |
| // Assertions for pinmux. |
| // Intended to be used with a formal tool. |
| |
| `include "prim_assert.sv" |
| |
| module pinmux_assert_fpv |
| import pinmux_pkg::*; |
| import pinmux_reg_pkg::*; |
| import prim_pad_wrapper_pkg::*; |
| #( |
| parameter target_cfg_t TargetCfg = DefaultTargetCfg, |
| parameter logic [NumAlerts-1:0] AlertAsyncOn = {NumAlerts{1'b1}} |
| ) ( |
| input clk_i, |
| input rst_ni, |
| input prim_mubi_pkg::mubi4_t scanmode_i, |
| input clk_aon_i, |
| input rst_aon_ni, |
| input logic pin_wkup_req_o, |
| input logic usb_wkup_req_o, |
| input sleep_en_i, |
| input strap_en_i, |
| input lc_ctrl_pkg::lc_tx_t lc_dft_en_i, |
| input lc_ctrl_pkg::lc_tx_t lc_hw_debug_en_i, |
| input dft_strap_test_req_t dft_strap_test_o, |
| input dft_hold_tap_sel_i, |
| input jtag_pkg::jtag_req_t lc_jtag_o, |
| input jtag_pkg::jtag_rsp_t lc_jtag_i, |
| input jtag_pkg::jtag_req_t rv_jtag_o, |
| input jtag_pkg::jtag_rsp_t rv_jtag_i, |
| input jtag_pkg::jtag_req_t dft_jtag_o, |
| input jtag_pkg::jtag_rsp_t dft_jtag_i, |
| input usb_out_of_rst_i, |
| input usb_aon_wake_en_i, |
| input usb_aon_wake_ack_i, |
| input usb_suspend_i, |
| input usbdev_pkg::awk_state_t usb_state_debug_o, |
| input tlul_pkg::tl_h2d_t tl_i, |
| input tlul_pkg::tl_d2h_t tl_o, |
| input prim_alert_pkg::alert_rx_t[NumAlerts-1:0] alert_rx_i, |
| input prim_alert_pkg::alert_tx_t[NumAlerts-1:0] alert_tx_o, |
| input [NMioPeriphOut-1:0] periph_to_mio_i, |
| input [NMioPeriphOut-1:0] periph_to_mio_oe_i, |
| input logic[NMioPeriphIn-1:0] mio_to_periph_o, |
| input [NDioPads-1:0] periph_to_dio_i, |
| input [NDioPads-1:0] periph_to_dio_oe_i, |
| input logic[NDioPads-1:0] dio_to_periph_o, |
| input prim_pad_wrapper_pkg::pad_attr_t[NMioPads-1:0] mio_attr_o, |
| input logic[NMioPads-1:0] mio_out_o, |
| input logic[NMioPads-1:0] mio_oe_o, |
| input [NMioPads-1:0] mio_in_i, |
| input prim_pad_wrapper_pkg::pad_attr_t[NDioPads-1:0] dio_attr_o, |
| input logic[NDioPads-1:0] dio_out_o, |
| input logic[NDioPads-1:0] dio_oe_o, |
| input [NDioPads-1:0] dio_in_i |
| ); |
| |
| /////////////////////////////// |
| // Declarations & Parameters // |
| /////////////////////////////// |
| |
| ///////////////// |
| // Assumptions // |
| ///////////////// |
| |
| // Symbolic inputs for FPV |
| logic [$clog2(pinmux_reg_pkg::NMioPeriphIn)-1:0] periph_sel_i; |
| logic [$clog2(pinmux_reg_pkg::NMioPads)-1:0] mio_sel_i; |
| logic [$clog2(pinmux_reg_pkg::NDioPads)-1:0] dio_sel_i; |
| logic [$clog2(pinmux_reg_pkg::NWkupDetect)-1:0] wkup_sel_i; |
| |
| `ASSUME(PeriphSelRange_M, periph_sel_i < pinmux_reg_pkg::NMioPeriphIn) |
| `ASSUME(PeriphSelStable_M, ##1 $stable(periph_sel_i)) |
| |
| `ASSUME(MioSelRange_M, mio_sel_i < pinmux_reg_pkg::NMioPads && !(mio_sel_i inside |
| {TargetCfg.tck_idx, TargetCfg.tms_idx, TargetCfg.trst_idx, TargetCfg.tdi_idx, |
| TargetCfg.tdo_idx})) |
| `ASSUME(MioSelStable_M, ##1 $stable(mio_sel_i)) |
| |
| `ASSUME(DioSelRange_M, dio_sel_i < pinmux_reg_pkg::NDioPads) |
| `ASSUME(DioSelStable_M, ##1 $stable(dio_sel_i)) |
| |
| `ASSUME(WkupSelRange_M, wkup_sel_i < pinmux_reg_pkg::NWkupDetect) |
| `ASSUME(WkupSelStable_M, ##1 $stable(wkup_sel_i)) |
| |
| // ------ Input mux assertions ------ |
| pinmux_reg_pkg::pinmux_reg2hw_mio_periph_insel_mreg_t periph_insel; |
| assign periph_insel = pinmux.reg2hw.mio_periph_insel[periph_sel_i]; |
| |
| `ASSERT(InSel0_A, periph_insel.q == 0 |-> mio_to_periph_o[periph_sel_i] == 1'b0) |
| `ASSERT(InSel1_A, periph_insel.q == 1 |-> mio_to_periph_o[periph_sel_i] == 1'b1) |
| `ASSERT(InSelN_A, periph_insel.q > 1 && periph_insel.q < (pinmux_reg_pkg::NMioPads + 2) && |
| !((periph_insel.q - 2) inside {TargetCfg.tck_idx, TargetCfg.tms_idx, TargetCfg.trst_idx, |
| TargetCfg.tdi_idx, TargetCfg.tdo_idx}) |-> |
| mio_to_periph_o[periph_sel_i] == mio_in_i[periph_insel.q - 2]) |
| `ASSERT(InSelOOB_A, periph_insel.q >= (pinmux_reg_pkg::NMioPads + 2) |-> |
| mio_to_periph_o[periph_sel_i] == 0) |
| // TODO: fix and uncomment the assertion below |
| //`ASSERT(MioToPeriphO_A, ##1 !$stable(mio_to_periph_o[periph_sel_i]) |-> |
| // !$stable(mio_in_i[periph_insel.q - 2]) || !$stable(periph_insel.q)) |
| |
| `ASSERT(DioInSelN_A, dio_to_periph_o == dio_in_i) |
| |
| // ------ Output mux assertions ------ |
| pinmux_reg_pkg::pinmux_reg2hw_mio_outsel_mreg_t mio_outsel; |
| assign mio_outsel = pinmux.reg2hw.mio_outsel[mio_sel_i]; |
| |
| pinmux_reg_pkg::pinmux_reg2hw_mio_pad_sleep_status_mreg_t mio_pad_sleep_status; |
| assign mio_pad_sleep_status = pinmux.reg2hw.mio_pad_sleep_status[mio_sel_i]; |
| |
| |
| `ASSERT(OutSel0_A, mio_outsel.q == 0 && !mio_pad_sleep_status.q |-> mio_out_o[mio_sel_i] == 1'b0) |
| `ASSERT(OutSel1_A, mio_outsel.q == 1 && !mio_pad_sleep_status.q |-> mio_out_o[mio_sel_i] == 1'b1) |
| `ASSERT(OutSel2_A, mio_outsel.q == 2 && !mio_pad_sleep_status.q |-> mio_out_o[mio_sel_i] == 1'b0) |
| `ASSERT(OutSelN_A, mio_outsel.q > 2 && mio_outsel.q < (pinmux_reg_pkg::NMioPeriphOut + 3) && |
| !mio_pad_sleep_status.q |-> mio_out_o[mio_sel_i] == periph_to_mio_i[mio_outsel.q - 3]) |
| `ASSERT(OutSelOOB_A, mio_outsel.q >= (pinmux_reg_pkg::NMioPeriphOut + 3) && |
| !mio_pad_sleep_status.q |-> mio_out_o[mio_sel_i] == 0) |
| // TODO: fix and uncomment the assertion below |
| //`ASSERT(MioOutO_A, ##1 !$stable(mio_out_o[mio_sel_i]) |-> |
| // !$stable(mio_outsel.q) || !$stable(periph_to_mio_i[mio_outsel.q - 3])) |
| |
| `ASSERT(OutSelOe0_A, mio_outsel.q == 0 && !mio_pad_sleep_status.q |-> |
| mio_oe_o[mio_sel_i] == 1'b1) |
| `ASSERT(OutSelOe1_A, mio_outsel.q == 1 && !mio_pad_sleep_status.q |-> |
| mio_oe_o[mio_sel_i] == 1'b1) |
| `ASSERT(OutSelOe2_A, mio_outsel.q == 2 && !mio_pad_sleep_status.q |-> |
| mio_oe_o[mio_sel_i] == 1'b0) |
| `ASSERT(OutSelOeN_A, mio_outsel.q > 2 && mio_outsel.q < (pinmux_reg_pkg::NMioPeriphOut + 3) && |
| !mio_pad_sleep_status.q |-> mio_oe_o[mio_sel_i] == periph_to_mio_oe_i[mio_outsel.q - 3]) |
| `ASSERT(OutSelOeOOB_A, mio_outsel.q >= (pinmux_reg_pkg::NMioPeriphOut + 3) && |
| !mio_pad_sleep_status.q |-> mio_oe_o[mio_sel_i] == 0) |
| // TODO: fix and uncomment the assertion below |
| //`ASSERT(MioOeO_A, ##1 !$stable(mio_oe_o[mio_sel_i]) |-> |
| // !$stable(mio_outsel.q) || !$stable(periph_to_mio_oe_i[mio_outsel.q - 3])) |
| |
| // ------ Mio sleep behavior assertions ------ |
| pinmux_reg_pkg::pinmux_reg2hw_mio_pad_sleep_en_mreg_t mio_pad_sleep_en; |
| assign mio_pad_sleep_en = pinmux.reg2hw.mio_pad_sleep_en[mio_sel_i]; |
| pinmux_reg_pkg::pinmux_reg2hw_mio_pad_sleep_mode_mreg_t mio_pad_sleep_mode; |
| assign mio_pad_sleep_mode = pinmux.reg2hw.mio_pad_sleep_mode[mio_sel_i]; |
| |
| `ASSERT(MioSleepMode0_A, ##1 mio_pad_sleep_mode.q == 0 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| mio_out_o[mio_sel_i] == 1'b0) |
| `ASSERT(MioSleepMode1_A, ##1 mio_pad_sleep_mode.q == 1 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| mio_out_o[mio_sel_i] == 1'b1) |
| `ASSERT(MioSleepMode2_A, ##1 mio_pad_sleep_mode.q == 2 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| mio_out_o[mio_sel_i] == 1'b0) |
| `ASSERT(MioSleepMode3_A, ##1 mio_pad_sleep_mode.q == 3 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| $stable(mio_out_o[mio_sel_i])) |
| `ASSERT(MioSleepStable_A, ##1 !$rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| $stable(mio_out_o[mio_sel_i])) |
| |
| `ASSERT(MioOeSleepMode0_A, ##1 mio_pad_sleep_mode.q == 0 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q && sleep_en_i|-> |
| mio_oe_o[mio_sel_i] == 1'b1) |
| `ASSERT(MioOeSleepMode1_A, ##1 mio_pad_sleep_mode.q == 1 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| mio_oe_o[mio_sel_i] == 1'b1) |
| `ASSERT(MioOeSleepMode2_A, ##1 mio_pad_sleep_mode.q == 2 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| mio_oe_o[mio_sel_i] == 1'b0) |
| `ASSERT(MioOeSleepMode3_A, ##1 mio_pad_sleep_mode.q == 3 && mio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| $stable(mio_oe_o[mio_sel_i])) |
| `ASSERT(MioOeSleepStable_A, ##1 !$rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 mio_pad_sleep_status.q |-> |
| $stable(mio_oe_o[mio_sel_i])) |
| |
| // ------ Mio_attr_o ------ |
| pinmux_reg_pkg::pinmux_reg2hw_mio_pad_attr_mreg_t mio_pad_attr; |
| assign mio_pad_attr = pinmux.mio_pad_attr_q[mio_sel_i]; |
| |
| pad_attr_t mio_pad_attr_mask; |
| pad_type_e bid_pad_types[4] = {BidirStd, BidirTol, DualBidirTol, BidirOd}; |
| assign mio_pad_attr_mask.invert = TargetCfg.mio_pad_type[mio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign mio_pad_attr_mask.virt_od_en = TargetCfg.mio_pad_type[mio_sel_i] inside {bid_pad_types} ? |
| 1 : 0; |
| assign mio_pad_attr_mask.pull_en = TargetCfg.mio_pad_type[mio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign mio_pad_attr_mask.pull_select = TargetCfg.mio_pad_type[mio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign mio_pad_attr_mask.keep_en = TargetCfg.mio_pad_type[mio_sel_i] inside {bid_pad_types} ? |
| 1 : 0; |
| assign mio_pad_attr_mask.drive_strength[0] = TargetCfg.mio_pad_type[mio_sel_i] inside |
| {bid_pad_types} ? 1 : 0; |
| assign mio_pad_attr_mask.schmitt_en = 0; |
| assign mio_pad_attr_mask.od_en = 0; |
| assign mio_pad_attr_mask.slew_rate = '0; |
| assign mio_pad_attr_mask.drive_strength[3:1] = '0; |
| |
| `ASSERT(MioAttrO_A, mio_attr_o[mio_sel_i] == (mio_pad_attr & mio_pad_attr_mask)) |
| |
| // ------ Dio_attr_o ------ |
| pinmux_reg_pkg::pinmux_reg2hw_dio_pad_attr_mreg_t dio_pad_attr; |
| assign dio_pad_attr = pinmux.dio_pad_attr_q[dio_sel_i]; |
| |
| pad_attr_t dio_pad_attr_mask; |
| assign dio_pad_attr_mask.invert = TargetCfg.dio_pad_type[dio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign dio_pad_attr_mask.virt_od_en = TargetCfg.dio_pad_type[dio_sel_i] inside {bid_pad_types} ? |
| 1 : 0; |
| assign dio_pad_attr_mask.pull_en = TargetCfg.dio_pad_type[dio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign dio_pad_attr_mask.pull_select = TargetCfg.dio_pad_type[dio_sel_i] == AnalogIn0 ? 0 : 1; |
| assign dio_pad_attr_mask.keep_en = TargetCfg.dio_pad_type[dio_sel_i] inside {bid_pad_types} ? |
| 1 : 0; |
| assign dio_pad_attr_mask.drive_strength[0] = TargetCfg.dio_pad_type[dio_sel_i] inside |
| {bid_pad_types} ? 1 : 0; |
| assign dio_pad_attr_mask.schmitt_en = 0; |
| assign dio_pad_attr_mask.od_en = 0; |
| assign dio_pad_attr_mask.slew_rate = '0; |
| assign dio_pad_attr_mask.drive_strength[3:1] = '0; |
| |
| `ASSERT(DioAttrO_A, dio_attr_o[dio_sel_i] == (dio_pad_attr & dio_pad_attr_mask)) |
| |
| // ------ Output dedicated output assertions ------ |
| pinmux_reg_pkg::pinmux_reg2hw_dio_pad_sleep_status_mreg_t dio_pad_sleep_status; |
| assign dio_pad_sleep_status = pinmux.reg2hw.dio_pad_sleep_status[dio_sel_i]; |
| |
| `ASSERT(DOutSelN_A, !dio_pad_sleep_status.q |-> |
| dio_out_o[dio_sel_i] == periph_to_dio_i[dio_sel_i]) |
| |
| `ASSERT(DOutSelOeN_A, !dio_pad_sleep_status.q |-> |
| dio_oe_o[dio_sel_i] == periph_to_dio_oe_i[dio_sel_i]) |
| |
| // ------ Dio sleep behavior assertions ------ |
| pinmux_reg_pkg::pinmux_reg2hw_dio_pad_sleep_en_mreg_t dio_pad_sleep_en; |
| assign dio_pad_sleep_en = pinmux.reg2hw.dio_pad_sleep_en[dio_sel_i]; |
| pinmux_reg_pkg::pinmux_reg2hw_dio_pad_sleep_mode_mreg_t dio_pad_sleep_mode; |
| assign dio_pad_sleep_mode = pinmux.reg2hw.dio_pad_sleep_mode[dio_sel_i]; |
| |
| `ASSERT(DioSleepMode0_A, ##1 dio_pad_sleep_mode.q == 0 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_out_o[dio_sel_i] == 1'b0) |
| `ASSERT(DioSleepMode1_A, ##1 dio_pad_sleep_mode.q == 1 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_out_o[dio_sel_i] == 1'b1) |
| `ASSERT(DioSleepMode2_A, ##1 dio_pad_sleep_mode.q == 2 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_out_o[dio_sel_i] == 1'b0) |
| `ASSERT(DioSleepMode3_A, ##1 dio_pad_sleep_mode.q == 3 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| $stable(dio_out_o[dio_sel_i])) |
| `ASSERT(DioSleepStable_A, ##1 !$rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| $stable(dio_out_o[dio_sel_i])) |
| |
| `ASSERT(DioOeSleepMode0_A, ##1 dio_pad_sleep_mode.q == 0 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_oe_o[dio_sel_i] == 1'b1) |
| `ASSERT(DioOeSleepMode1_A, ##1 dio_pad_sleep_mode.q == 1 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_oe_o[dio_sel_i] == 1'b1) |
| `ASSERT(DioOeSleepMode2_A, ##1 dio_pad_sleep_mode.q == 2 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| dio_oe_o[dio_sel_i] == 1'b0) |
| `ASSERT(DioOeSleepMode3_A, ##1 dio_pad_sleep_mode.q == 3 && dio_pad_sleep_en.q == 1 && |
| $rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| $stable(dio_oe_o[dio_sel_i])) |
| `ASSERT(DioOeSleepStable_A, ##1 !$rose(sleep_en_i) |
| // Ensure SW does not write to sleep status register to clear sleep status. |
| ##1 dio_pad_sleep_status.q |-> |
| $stable(dio_oe_o[dio_sel_i])) |
| |
| // ------Dio backward assertions ------ |
| `ASSERT(Dio0Backward_A, dio_out_o[dio_sel_i] == 0 |-> |
| // Input is 0. |
| periph_to_dio_i[dio_sel_i] == 0 || |
| // Sleep mode set to 0 and 2. |
| $past(dio_pad_sleep_mode.q) inside {0, 2} || |
| // Previous value is 0 and sleep mode is set to 3. |
| ($past(dio_out_o[dio_sel_i]) == 0) && |
| ($past(dio_pad_sleep_mode.q) == 3 || |
| // Previous value is 0 and sleep mode selection is disabled either by sleep_en_i input |
| // or sleep_en CSR. |
| ($past(!$rose(sleep_en_i) || !dio_pad_sleep_en.q) && dio_pad_sleep_status.q))) |
| |
| `ASSERT(Dio1Backward_A, dio_out_o[dio_sel_i] == 1 |-> |
| // input is 1. |
| periph_to_dio_i[dio_sel_i] == 1 || |
| // Sleep mode set to 1. |
| $past(dio_pad_sleep_mode.q) == 1 || |
| // Previous value is 1 and sleep mode is set to 3. |
| ($past(dio_out_o[dio_sel_i]) == 1) && |
| ($past(dio_pad_sleep_mode.q) == 3 || |
| // Previous value is 1 and sleep mode selection is disabled either by sleep_en_i input |
| // or sleep_en CSR. |
| ($past(!$rose(sleep_en_i) || !dio_pad_sleep_en.q) && dio_pad_sleep_status.q))) |
| |
| `ASSERT(DioOe0Backward_A, dio_oe_o[dio_sel_i] == 0 |-> |
| // Input is 0. |
| periph_to_dio_oe_i[dio_sel_i] == 0 || |
| // Sleep mode set to 2. |
| $past(dio_pad_sleep_mode.q) == 2 || |
| // Previous value is 0 and sleep mode is set to 3. |
| ($past(dio_oe_o[dio_sel_i]) == 0) && |
| ($past(dio_pad_sleep_mode.q) == 3 || |
| // Previous value is 0 and sleep mode selection is disabled either by sleep_en_i input |
| // or sleep_en CSR. |
| ($past(!$rose(sleep_en_i) || !dio_pad_sleep_en.q) && dio_pad_sleep_status.q))) |
| |
| `ASSERT(DioOe1Backward_A, dio_oe_o[dio_sel_i] == 1 |-> |
| // input is 1. |
| periph_to_dio_oe_i[dio_sel_i] == 1 || |
| // Sleep mode set to 0 or 1. |
| $past(dio_pad_sleep_mode.q) inside {0, 1} || |
| // Previous value is 1 and sleep mode is set to 3. |
| ($past(dio_oe_o[dio_sel_i]) == 1) && |
| ($past(dio_pad_sleep_mode.q) == 3 || |
| // Previous value is 1 and sleep mode selection is disabled either by sleep_en_i input |
| // or sleep_en CSR. |
| ($past(!$rose(sleep_en_i) || !dio_pad_sleep_en.q) && dio_pad_sleep_status.q))) |
| |
| // ------ Wakeup assertions ------ |
| pinmux_reg2hw_wkup_detector_en_mreg_t wkup_detector_en; |
| assign wkup_detector_en = pinmux.reg2hw.wkup_detector_en[wkup_sel_i]; |
| pinmux_reg2hw_wkup_detector_mreg_t wkup_detector; |
| assign wkup_detector = pinmux.reg2hw.wkup_detector[wkup_sel_i]; |
| pinmux_reg2hw_wkup_detector_cnt_th_mreg_t wkup_detector_cnt_th; |
| assign wkup_detector_cnt_th = pinmux.reg2hw.wkup_detector_cnt_th[wkup_sel_i]; |
| pinmux_reg2hw_wkup_detector_padsel_mreg_t wkup_detector_padsel; |
| assign wkup_detector_padsel = pinmux.reg2hw.wkup_detector_padsel[wkup_sel_i]; |
| pinmux_reg2hw_wkup_cause_mreg_t wkup_cause; |
| assign wkup_cause = pinmux.reg2hw.wkup_cause[wkup_sel_i]; |
| |
| // Get pin value based on Mio and Dio selection. |
| logic pin_val; |
| assign pin_val = wkup_detector.miodio.q ? |
| (wkup_detector_padsel.q >= pinmux_reg_pkg::NDioPads ? 0 : |
| dio_in_i[wkup_detector_padsel.q]) : |
| (wkup_detector_padsel.q >= (pinmux_reg_pkg::NMioPads + 2) ? 0 : |
| wkup_detector_padsel == 0 ? 0 : |
| wkup_detector_padsel == 1 ? 1 : |
| mio_in_i[wkup_detector_padsel.q - 2]); |
| |
| // Get filterd pin value. |
| logic [3:0] filter_vals; |
| always_ff @(posedge clk_aon_i or negedge rst_aon_ni) begin |
| if (!rst_aon_ni) begin |
| filter_vals <= 4'b0; |
| end else if (pin_val == filter_vals[0]) begin |
| filter_vals <= (filter_vals << 1) | pin_val; |
| end else begin |
| filter_vals <= {filter_vals[3], filter_vals[3], filter_vals[3], pin_val}; |
| end |
| end |
| |
| logic final_pin_val = wkup_detector.filter.q ? filter_vals[3] : pin_val; |
| |
| // Threshold counters. |
| // Adding one more bit for the counters to check overflow case. |
| bit [WkupCntWidth:0] high_cnter, low_cnter; |
| always_ff @(posedge clk_aon_i or negedge rst_aon_ni) begin |
| if (!rst_aon_ni || !wkup_detector_en.q) begin |
| high_cnter <= 0; |
| low_cnter <= 0; |
| end else if (wkup_detector.mode.q == 3) begin |
| low_cnter <= 0; |
| if ($past(final_pin_val, 2) && (high_cnter < wkup_detector_cnt_th.q)) begin |
| high_cnter <= high_cnter + 1; |
| end else begin |
| high_cnter <= 0; |
| end |
| end else if (wkup_detector.mode.q == 4) begin |
| high_cnter <= 0; |
| if (!$past(final_pin_val, 2) && (low_cnter < wkup_detector_cnt_th.q)) begin |
| low_cnter <= low_cnter + 1; |
| end else begin |
| low_cnter <= 0; |
| end |
| end else begin |
| high_cnter <= 0; |
| low_cnter <= 0; |
| end |
| end |
| |
| `ASSERT(WkupPosedge_A, wkup_detector_en.q && wkup_detector.mode.q == 0 && |
| $rose($past(final_pin_val, 2)) |=> |
| wkup_cause.q || $past(u_reg.aon_wkup_cause_we), |
| clk_aon_i, !rst_aon_ni) |
| `ASSERT(WkupNegedge_A, wkup_detector_en.q && wkup_detector.mode.q == 1 && |
| $fell($past(final_pin_val, 2)) |=> |
| wkup_cause.q || $past(u_reg.aon_wkup_cause_we), |
| clk_aon_i, !rst_aon_ni) |
| `ASSERT(WkupEdge_A, wkup_detector_en.q && wkup_detector.mode.q == 2 && |
| ($fell($past(final_pin_val, 2)) || $rose($past(final_pin_val, 2))) |=> |
| wkup_cause.q || $past(u_reg.aon_wkup_cause_we), |
| clk_aon_i, !rst_aon_ni) |
| `ASSERT(WkupTimedHigh_A, (high_cnter >= wkup_detector_cnt_th.q) && wkup_detector_en.q && |
| wkup_detector.mode.q == 3 |=> |
| wkup_cause.q || $past(u_reg.aon_wkup_cause_we), |
| clk_aon_i, !rst_aon_ni) |
| `ASSERT(WkupTimedLow_A, (low_cnter >= wkup_detector_cnt_th.q) && wkup_detector_en.q && |
| wkup_detector.mode.q == 4 |=> |
| wkup_cause.q || $past(u_reg.aon_wkup_cause_we), |
| clk_aon_i, !rst_aon_ni) |
| |
| `ASSERT(AonWkupO_A, wkup_cause.q |-> pin_wkup_req_o, clk_aon_i, !rst_aon_ni) |
| |
| // ------ JTAG pinmux input assertions ------ |
| `ASSERT(LcJtagOWoScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::LcTapSel && |
| !prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) |-> |
| lc_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| mio_in_i[TargetCfg.trst_idx], |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(LcJtagOWScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::LcTapSel && |
| prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) |-> |
| lc_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| rst_ni, |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(LcJtagOStable_A, u_pinmux_strap_sampling.tap_strap != pinmux_pkg::LcTapSel && |
| $past(u_pinmux_strap_sampling.tap_strap) != pinmux_pkg::LcTapSel |-> |
| $stable(lc_jtag_o)) |
| `ASSERT(LcJtagODefault_A, u_pinmux_strap_sampling.tap_strap != pinmux_pkg::LcTapSel |-> |
| lc_jtag_o == '0) |
| |
| // Lc_hw_debug_en_i signal goes through a two clock cycle synchronizer. |
| `ASSERT(RvJtagOWoScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::RvTapSel && |
| !prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 2) |-> |
| rv_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| mio_in_i[TargetCfg.trst_idx], |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(RvJtagOWScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::RvTapSel && |
| prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 2) |-> |
| rv_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| rst_ni, |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(RvJtagOStable_A, (u_pinmux_strap_sampling.tap_strap != pinmux_pkg::RvTapSel && |
| $past(u_pinmux_strap_sampling.tap_strap) != pinmux_pkg::RvTapSel) || |
| (!$past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 2) && |
| !$past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 3)) |-> |
| $stable(rv_jtag_o)) |
| `ASSERT(RvJtagODefault_A, u_pinmux_strap_sampling.tap_strap != pinmux_pkg::RvTapSel || |
| !$past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 2) |-> |
| rv_jtag_o == '0) |
| |
| // Lc_dft_en_i signal goes through a two clock cycle synchronizer. |
| `ASSERT(DftJtagOWoScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::DftTapSel && |
| !prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) |-> |
| dft_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| mio_in_i[TargetCfg.trst_idx], |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(DftJtagOWScanmode_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::DftTapSel && |
| prim_mubi_pkg::mubi4_test_true_strict(scanmode_i) && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) |-> |
| dft_jtag_o == {mio_in_i[TargetCfg.tck_idx], |
| mio_in_i[TargetCfg.tms_idx], |
| rst_ni, |
| mio_in_i[TargetCfg.tdi_idx]}) |
| `ASSERT(DftJtagOStable_A, (u_pinmux_strap_sampling.tap_strap != pinmux_pkg::DftTapSel && |
| $past(u_pinmux_strap_sampling.tap_strap) != pinmux_pkg::DftTapSel) || |
| (!$past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) && |
| !$past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 3)) |-> |
| $stable(dft_jtag_o)) |
| `ASSERT(DftJtagODefault_A, u_pinmux_strap_sampling.tap_strap != pinmux_pkg::DftTapSel || |
| !$past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) |-> |
| dft_jtag_o == '0) |
| |
| `ASSERT(TapStrap_A, ##2 ((!dft_hold_tap_sel_i && $past(lc_dft_en_i, 2) == lc_ctrl_pkg::On) || |
| strap_en_i) && $past(lc_hw_debug_en_i, 2) == lc_ctrl_pkg::On |=> |
| u_pinmux_strap_sampling.tap_strap == |
| $past({mio_in_i[TargetCfg.tap_strap1_idx], mio_in_i[TargetCfg.tap_strap0_idx]})) |
| |
| `ASSERT(TapStrap0_A, ##2 ((!dft_hold_tap_sel_i && $past(lc_dft_en_i, 2) == lc_ctrl_pkg::On) || |
| strap_en_i) |=> |
| u_pinmux_strap_sampling.tap_strap[0] == $past(mio_in_i[TargetCfg.tap_strap0_idx])) |
| |
| `ASSERT(TapStrapStable_A, dft_hold_tap_sel_i && !strap_en_i |=> |
| $stable(u_pinmux_strap_sampling.tap_strap)) |
| |
| // ------ JTAG pinmux output assertions ------ |
| `ASSERT(LcJtagI_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::LcTapSel |-> |
| lc_jtag_i == {mio_out_o[TargetCfg.tdo_idx], |
| mio_oe_o[TargetCfg.tdo_idx]}) |
| `ASSERT(RvJtagI_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::RvTapSel && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_hw_debug_en_i), 2) |-> |
| rv_jtag_i == {mio_out_o[TargetCfg.tdo_idx], |
| mio_oe_o[TargetCfg.tdo_idx]}) |
| `ASSERT(DftJtagI_A, u_pinmux_strap_sampling.tap_strap == pinmux_pkg::DftTapSel && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) |-> |
| dft_jtag_i == {mio_out_o[TargetCfg.tdo_idx], |
| mio_oe_o[TargetCfg.tdo_idx]}) |
| |
| // ------ DFT strap_test_o assertions ------ |
| `ASSERT(DftStrapTestO_A, ##2 strap_en_i && |
| $past(prim_mubi_pkg::mubi4_test_true_strict(lc_dft_en_i), 2) |=> |
| dft_strap_test_o.valid && |
| dft_strap_test_o.straps == $past({mio_in_i[TargetCfg.dft_strap1_idx], |
| mio_in_i[TargetCfg.dft_strap0_idx]})) |
| `ASSERT(DftStrapTestOValidStable_A, dft_strap_test_o.valid |=> dft_strap_test_o.valid) |
| `ASSERT(DftStrapTestOStrapStable_A, dft_strap_test_o.valid |-> |
| $stable(dft_strap_test_o.straps) || |
| (dft_strap_test_o.straps == $past({mio_in_i[TargetCfg.dft_strap1_idx], |
| mio_in_i[TargetCfg.dft_strap0_idx]}))) |
| |
| endmodule : pinmux_assert_fpv |
