blob: 34e60d34a7d267fd0f161df17a2fe4e84bfba473 [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 the inputs from rstmgr react according to
// the pwrmgr outputs. The rstmgr inputs are generated by the base sequences, but
// these assertions will also be useful at full chip level.
interface pwrmgr_rstmgr_sva_if
import pwrmgr_pkg::*, pwrmgr_reg_pkg::*;
(
input logic clk_i,
input logic rst_ni,
input logic clk_slow_i,
input logic rst_slow_ni,
// The inputs from pwrmgr.
input logic [PowerDomains-1:0] rst_lc_req,
input logic [PowerDomains-1:0] rst_sys_req,
// The inputs from rstmgr.
input logic [PowerDomains-1:0] rst_lc_src_n,
input logic [PowerDomains-1:0] rst_sys_src_n
);
// Number of cycles for the LC/SYS reset handshake.
localparam int MIN_LC_SYS_CYCLES = 0;
localparam int MAX_LC_SYS_CYCLES = 150;
`define LC_SYS_CYCLES ##[MIN_LC_SYS_CYCLES:MAX_LC_SYS_CYCLES]
bit disable_sva;
bit reset_or_disable;
always_comb reset_or_disable = !rst_slow_ni || disable_sva;
// Lc and Sys handshake: pwrmgr rst_*_req causes rstmgr rst_*_src_n
for (genvar pd = 0; pd < PowerDomains; ++pd) begin : gen_assertions_per_power_domains
`ASSERT(LcHandshakeOn_A, rst_lc_req[pd] |-> `LC_SYS_CYCLES !rst_lc_req[pd] || !rst_lc_src_n[pd],
clk_i, reset_or_disable)
`ASSERT(LcHandshakeOff_A, $fell(rst_lc_req[pd])
|-> `LC_SYS_CYCLES rst_lc_req[pd] || rst_lc_src_n[pd], clk_i, reset_or_disable)
`ASSERT(SysHandshakeOn_A,
rst_sys_req[pd] |-> `LC_SYS_CYCLES !rst_sys_req[pd] || !rst_sys_src_n[pd], clk_i,
reset_or_disable)
`ASSERT(SysHandshakeOff_A,
!rst_sys_req[pd] |-> `LC_SYS_CYCLES rst_sys_req[pd] || rst_sys_src_n[pd], clk_i,
reset_or_disable)
end : gen_assertions_per_power_domains
`undef LC_SYS_CYCLES
endinterface