// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0

// Enables coverage on the entire DUT. Limits the port only toggle coverage to
// the DUT IOs.

+tree tb.dut
-module pins_if     // DV construct.
-module clk_rst_if  // DV construct.
// Prim_alert/esc pairs are verified in FPV and DV testbenches.
-moduletree prim_alert_sender
-moduletree prim_alert_receiver
-moduletree prim_esc_sender
-moduletree prim_esc_receiver
-moduletree prim_prince // prim_prince is verified in a separate DV environment.
-moduletree prim_lfsr // prim_lfsr is verified in FPV.

begin tgl
  -tree tb
  +tree tb.dut 1
  +module prim_alert_sender
  +module prim_alert_receiver
  +module prim_esc_sender
  +module prim_esc_receiver
  +module prim_prince
  +module prim_lfsr
end

begin assert
  // These three assertions in prim_lc_sync and prim_mubi* check when `lc_ctrl_pkg::lc_tx_t` or
  // `mubi*_t` input are neither `On` or `Off`, it is interrupted to the correct `On` or `Off`
  // after one clock cycle. This behavior is implemented outside of IP level design thus these
  // assertions are not covered in IP level testbenchs.
  // TODO: check these assertions in top-level or FPV.
  -assert PrimLcSyncCheckTransients_A
  -assert PrimLcSyncCheckTransients0_A
  -assert PrimLcSyncCheckTransients1_A

  -assert PrimMubi4SyncCheckTransients_A
  -assert PrimMubi4SyncCheckTransients0_A
  -assert PrimMubi4SyncCheckTransients1_A

  -assert PrimMubi8SyncCheckTransients_A
  -assert PrimMubi8SyncCheckTransients0_A
  -assert PrimMubi8SyncCheckTransients1_A

  -assert PrimMubi12SyncCheckTransients_A
  -assert PrimMubi12SyncCheckTransients0_A
  -assert PrimMubi12SyncCheckTransients1_A

  -assert PrimMubi16SyncCheckTransients_A
  -assert PrimMubi16SyncCheckTransients0_A
  -assert PrimMubi16SyncCheckTransients1_A
end
