blob: 70304aad0d375e4307f93015ae78e08056524b26 [file] [log] [blame]
// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
// This has some assertions that check that the output clock enables correspond
// to the control CSR when transitioning into or out of the active state. In
// addition, the usb clock can change anytime when in the active state.
interface pwrmgr_clock_enables_sva_if (
input logic clk_i,
input logic rst_ni,
input pwrmgr_pkg::fast_pwr_state_e fast_state,
input pwrmgr_pkg::slow_pwr_state_e slow_state,
// The synchronized control CSR bits.
input logic main_pd_ni,
input logic io_clk_en_i,
input logic core_clk_en_i,
input logic usb_clk_en_lp_i,
input logic usb_clk_en_active_i,
input logic usb_ip_clk_status_i,
// The output enables.
input logic main_pd_n,
input logic io_clk_en,
input logic core_clk_en,
input logic usb_clk_en
);
bit disable_sva;
bit reset_or_disable;
always_comb reset_or_disable = !rst_ni || disable_sva;
sequence transitionUp_S; slow_state == pwrmgr_pkg::SlowPwrStateReqPwrUp; endsequence
sequence transitionDown_S; slow_state == pwrmgr_pkg::SlowPwrStatePwrClampOn; endsequence
bit fast_is_active;
always_comb fast_is_active = fast_state == pwrmgr_pkg::FastPwrStateActive;
// This allows the usb enable to be slower since it also depends on usb clk_status.
sequence usbActiveTransition_S;
##[0:7] !fast_is_active || usb_clk_en == (usb_clk_en_active_i | usb_ip_clk_status_i);
endsequence
`ASSERT(CoreClkPwrUp_A, transitionUp_S |=> core_clk_en == 1'b1, clk_i, reset_or_disable)
`ASSERT(IoClkPwrUp_A, transitionUp_S |=> io_clk_en == 1'b1, clk_i, reset_or_disable)
`ASSERT(UsbClkPwrUp_A, transitionUp_S |=> usb_clk_en == usb_clk_en_active_i, clk_i,
reset_or_disable)
// This deals with transitions while the fast fsm is active.
`ASSERT(UsbClkActive_A, fast_is_active && $changed(usb_clk_en_active_i) |=> usbActiveTransition_S,
clk_i, reset_or_disable)
`ASSERT(CoreClkPwrDown_A, transitionDown_S |=> core_clk_en == (core_clk_en_i && main_pd_ni),
clk_i, reset_or_disable)
`ASSERT(IoClkPwrDown_A, transitionDown_S |=> io_clk_en == (io_clk_en_i && main_pd_ni), clk_i,
reset_or_disable)
`ASSERT(UsbClkPwrDown_A, transitionDown_S |=> usb_clk_en == (usb_clk_en_lp_i && main_pd_ni),
clk_i, reset_or_disable)
endinterface