blob: e7f9291d77310425d58de980c95b1a32c34f9e55 [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 assertions that check the reset outputs of rstmgr cascade properly.
// This means higher level resets always cause the lower level ones to assert.
// The hierarchy is
// por > lc > sys > specific peripherals
// In addition, a scan reset is at the same level as por.
//
// Local terminology: A cascading relationship is between an "above" and a "below" reset.
//
// Some individual reset outputs will always be off. Allowing for this in general would
// weaken the property that some resets MUST rise following other rise.
//
// Peripheral resets cascade from sys, and are checked in rstmgr_sw_rst_sva_if since they
// require additional inputs.
interface rstmgr_cascading_sva_if (
input logic clk_i,
input logic clk_aon_i,
input logic clk_io_div2_i,
input logic clk_io_div4_i,
input logic clk_io_i,
input logic clk_main_i,
input logic clk_usb_i,
input [rstmgr_pkg::PowerDomains-1:0] por_n_i,
input rstmgr_pkg::rstmgr_out_t resets_o,
input [rstmgr_pkg::PowerDomains-1:0] rst_lc_req,
input [rstmgr_pkg::PowerDomains-1:0] rst_sys_req,
input [rstmgr_pkg::PowerDomains-1:0] rst_lc_src_n,
input [rstmgr_pkg::PowerDomains-1:0] rst_sys_src_n,
input logic scan_rst_ni,
input prim_mubi_pkg::mubi4_t scanmode_i
);
// The min and max bounds on the number of cycles for an edge to occur.
typedef struct {
int min;
int max;
} bounds_t;
// The bounds for a fall and rise edge to occur.
typedef struct {
bounds_t fall;
bounds_t rise;
} edge_bounds_t;
// This is used to check por_n_i active high leads to a rising edge of rst_por_aon_n[0].
// The number of cycles with por_n_i stable is 32 plus synchronizers and some filter stages.
localparam edge_bounds_t PorCycles = '{fall: '{min: 0, max: 4}, rise: '{min: 35, max: 40}};
// This is used to check for regular synchronizing delay. Reset falls asynchronously so the
// fall min cycles is zero.
localparam edge_bounds_t SyncCycles = '{fall: '{min: 0, max: 3}, rise: '{min: 1, max: 3}};
// Cycles are counted from the output rst_por_aon_n or scan reset edges. The rise times can be
// higher since in the chip the aon reset goes through the pwrmgr slow fsm where it causes an
// lc rise request and there may be multiple synchronizers in the path.
localparam edge_bounds_t LcCycles = '{fall: '{min: 0, max: 4}, rise: '{min: 1, max: 4}};
// In the real system the rise of rst_lc_src_n is triggered by the pwr_i.rst_lc_req input,
// which can take a few cycles since it comes from the pwrmgr after it gets reset,
// is generated with the aon clock, and gets synchronized before it triggers
// a rise in rst_lc_src_n. There is an SVA for the rise in pwrmgr_rstmgr_sva_if.
// The cycles are counted from Lc edges.
localparam edge_bounds_t SysCycles = '{fall: '{min: 0, max: 3}, rise: '{min: 1, max: 5}};
// The different peripheral edges are synchronized to their respective clocks,
// so these counts assume synchronization and are triggered on the correct clock.
localparam edge_bounds_t PeriCycles = '{fall: '{min: 0, max: 4}, rise: '{min: 2, max: 8}};
bit disable_sva;
// Macros to avoid excessive boiler-plate code below.
`define FALL_ASSERT(_name, _from, _to, _cycles, _clk) \
`ASSERT(_name``AboveFall_A, \
$fell(_from) |-> ##[_cycles.fall.min:_cycles.fall.max] _from || !_to, _clk, \
disable_sva)
`define RISE_ASSERTS(_name, _from, _to, _cycles, _clk) \
`ASSERT(_name``AboveRise_A, \
$rose(_from) ##1 _from [* _cycles.rise.min] |=> ##[0:_cycles.rise.max-_cycles.rise.min] (!_from || _to), _clk, \
disable_sva) \
`define CASCADED_ASSERTS(_name, _from, _to, _cycles, _clk) \
`FALL_ASSERT(_name, _from, _to, _cycles, _clk) \
`RISE_ASSERTS(_name, _from, _to, _cycles, _clk)
// A fall in por_n_i leads to a fall in rst_por_aon_n[0].
`FALL_ASSERT(CascadePorToAon, por_n_i[rstmgr_pkg::DomainAonSel],
resets_o.rst_por_aon_n[rstmgr_pkg::DomainAonSel], PorCycles, clk_aon_i)
// A number of consecutive cycles with por_n_i inactive (high) should cause the aon resets to
// become inactive. This checks POR stretching.
// The antecedent: por_n_i rising and being active for enough cycles.
logic scanmode;
always_comb scanmode = prim_mubi_pkg::mubi4_test_true_strict(scanmode_i);
logic scan_reset_n;
always_comb scan_reset_n = !scanmode || scan_rst_ni;
// In scanmode only scan_rst_ni controls reset, so por_n_i is ignored.
logic aon_por_n_i;
always_comb aon_por_n_i = por_n_i[rstmgr_pkg::DomainAonSel] && !scanmode;
sequence PorStable_S;
$rose(
aon_por_n_i
) ##1 aon_por_n_i [* PorCycles.rise.min];
endsequence
// The reset stretching assertion.
`ASSERT(StablePorToAonRise_A,
PorStable_S |-> ##[0:(PorCycles.rise.max-PorCycles.rise.min)]
!aon_por_n_i || resets_o.rst_por_aon_n[0],
clk_aon_i, disable_sva)
// The scan reset to Por.
`ASSERT(ScanRstToAonRise_A, scan_reset_n && scanmode |-> resets_o.rst_por_aon_n[0], clk_aon_i,
disable_sva)
logic [rstmgr_pkg::PowerDomains-1:0] effective_aon_rst_n;
always_comb
effective_aon_rst_n = resets_o.rst_por_aon_n & {rstmgr_pkg::PowerDomains{scan_reset_n}};
// The AON reset triggers the various POR reset for the different clock domains through
// synchronizers.
// The current system doesn't have any consumers of domain 1 por_io_div4, and thus only domain 0
// cascading is checked here.
`CASCADED_ASSERTS(CascadeEffAonToRstPorIoDiv4, effective_aon_rst_n[0],
resets_o.rst_por_io_div4_n[0], SyncCycles, clk_io_div4_i)
// The internal reset is triggered by one of synchronized por.
logic [rstmgr_pkg::PowerDomains-1:0] por_rst_n;
always_comb por_rst_n = resets_o.rst_por_aon_n;
logic [rstmgr_pkg::PowerDomains-1:0] local_rst_or_lc_req_n;
always_comb local_rst_or_lc_req_n = por_rst_n & ~rst_lc_req;
logic [rstmgr_pkg::PowerDomains-1:0] lc_rst_or_sys_req_n;
always_comb lc_rst_or_sys_req_n = por_rst_n & ~rst_sys_req;
for (genvar pd = 0; pd < rstmgr_pkg::PowerDomains; ++pd) begin : g_power_domains
// The root lc reset is triggered either by the internal reset, or by the pwr_i.rst_lc_req
// input. The latter is checked independently in pwrmgr_rstmgr_sva_if.
`CASCADED_ASSERTS(CascadeLocalRstToLc, local_rst_or_lc_req_n[pd], rst_lc_src_n[pd], LcCycles,
clk_i)
// The root sys reset is triggered by the lc reset, or independently by external requests.
// The latter is checked independently in pwrmgr_rstmgr_sva_if.
`CASCADED_ASSERTS(CascadeLcToSys, lc_rst_or_sys_req_n[pd], rst_sys_src_n[pd], SysCycles, clk_i)
// Controlled by rst_sys_src_n.
if (pd == rstmgr_pkg::DomainAonSel) begin : gen_sys_io_div4_chk
`CASCADED_ASSERTS(CascadeSysToSysIoDiv4, rst_sys_src_n[pd], resets_o.rst_sys_io_div4_n[pd],
SysCycles, clk_io_div4_i)
end
end
// Aon to POR
`CASCADED_ASSERTS(CascadeEffAonToRstPor, effective_aon_rst_n[rstmgr_pkg::DomainAonSel],
resets_o.rst_por_n[rstmgr_pkg::DomainAonSel], SyncCycles, clk_main_i)
`CASCADED_ASSERTS(CascadeEffAonToRstPorIo, effective_aon_rst_n[rstmgr_pkg::DomainAonSel],
resets_o.rst_por_io_n[rstmgr_pkg::DomainAonSel], SyncCycles, clk_io_i)
`CASCADED_ASSERTS(CascadeEffAonToRstPorIoDiv2, effective_aon_rst_n[rstmgr_pkg::DomainAonSel],
resets_o.rst_por_io_div2_n[rstmgr_pkg::DomainAonSel], SyncCycles, clk_io_div2_i)
`CASCADED_ASSERTS(CascadeEffAonToRstPorUcb, effective_aon_rst_n[rstmgr_pkg::DomainAonSel],
resets_o.rst_por_usb_n[rstmgr_pkg::DomainAonSel], SyncCycles, clk_usb_i)
// Controlled by rst_lc_src_n.
`CASCADED_ASSERTS(CascadeLcToLcAon, rst_lc_src_n[rstmgr_pkg::DomainAonSel],
resets_o.rst_lc_aon_n[rstmgr_pkg::DomainAonSel], SysCycles, clk_aon_i)
`CASCADED_ASSERTS(CascadeLcToLc, rst_lc_src_n[rstmgr_pkg::Domain0Sel],
resets_o.rst_lc_n[rstmgr_pkg::Domain0Sel], SysCycles, clk_main_i)
// Controlled by rst_sys_src_n.
`CASCADED_ASSERTS(CascadeSysToSys, rst_sys_src_n[rstmgr_pkg::Domain0Sel],
resets_o.rst_sys_n[rstmgr_pkg::Domain0Sel], PeriCycles, clk_main_i)
`CASCADED_ASSERTS(CascadeLcToLcShadowed, rst_lc_src_n[rstmgr_pkg::Domain0Sel],
resets_o.rst_lc_shadowed_n[rstmgr_pkg::Domain0Sel], SysCycles, clk_main_i)
`undef FALL_ASSERT
`undef RISE_ASSERTS
`undef CASCADED_ASSERTS
endinterface