| // 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 |