// Copyright lowRISC contributors (OpenTitan project).
// 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 #(
  parameter int unsigned PowerDomains = 2
) (
  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 MinLcSysCycles = 0;
  localparam int MaxLcSysCycles = 150;
  `define LC_SYS_CYCLES ##[MinLcSysCycles:MaxLcSysCycles]

  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