Low Power Verification

## upf/top.upf  — Minimal UPF for a two-domain SoC

# ---- Supply network for Always-On (AO) domain ----
create_supply_port  VDD_AO     -direction in
create_supply_port  VSS        -direction in
create_supply_net   VDD_AO_net -domain AO_domain
connect_supply_net  VDD_AO_net -ports VDD_AO

# ---- Always-On domain covers the PMU and boot logic ----
create_power_domain AO_domain  -elements {u_pmu u_boot_rom}
create_pst          top_pst    -supply_nets {VDD_AO_net VDD_PD_net}

# ---- Switchable domain for DSP core ----
create_supply_port  VDD_PD     -direction in
create_supply_net   VDD_PD_net -domain PD_domain
connect_supply_net  VDD_PD_net -ports VDD_PD

create_power_domain PD_domain  -elements {u_dsp}

# ---- Power State Table rows ----
# Each row names the state of every supply net in order
add_pst_state       NORMAL     -pst top_pst  \
    -state {VDD_AO_net FULL_ON  VDD_PD_net FULL_ON}

add_pst_state       DSP_OFF    -pst top_pst  \
    -state {VDD_AO_net FULL_ON  VDD_PD_net OFF}

# ---- Port states control what value each supply takes ----
add_port_state      VDD_PD \
    -state {FULL_ON  0.9} \
    -state {OFF      0.0}

## UPF isolation rule declaration
create_isolation_rule iso_dsp_to_ao \
    -from          PD_domain \
    -to            AO_domain \
    -isolation_sense high \       # enable=1 → isolate
    -clamp_value   0 \             # outputs held LOW when isolated
    -isolation_signal u_pmu.iso_en \
    -location      parent          # cell placed in AO_domain

## Map to a real library isolation cell
map_isolation_cell iso_dsp_to_ao \
    -domain   PD_domain \
    -lib_cell ISO_AND_X2       # output = IN & ~ISO_EN (sense=high, clamp=0)

// File: tb/isolation_checks.sv
// Bind into the DUT top so $root hierarchy is accessible

module isolation_checks #(parameter int NPORTS = 8) (
  input  logic              clk,
  input  logic              vdd_pd_on,   // 1 = domain powered, 0 = off
  input  logic              iso_en,      // 1 = isolation active
  input  logic [NPORTS-1:0] dsp_out,     // signals crossing from PD→AO
  input  logic [NPORTS-1:0] iso_cell_out // post-isolation values
);

  // When domain is off, iso_en must be asserted
  ISO_ENABLE_WHEN_OFF: assert property (
    @(posedge clk)
    !vdd_pd_on |-> iso_en
  ) else $error("[ISOLATION] Domain off but iso_en=0 — X propagation risk");

  // When isolated, each output must be clamped to 0 (clamp_value=0)
  ISO_CLAMP_VALUE: assert property (
    @(posedge clk)
    iso_en |-> (iso_cell_out === {NPORTS{1'b0}})
  ) else $error("[ISOLATION] Clamp value mismatch — expected all-0 when iso_en=1");

  // iso_en must be asserted BEFORE power drops (1 cycle lead)
  ISO_LEAD_TIME: assert property (
    @(posedge clk)
    $fell(vdd_pd_on) |-> $past(iso_en, 1)
  ) else $error("[ISOLATION] iso_en not asserted before vdd_pd_on fell");

  // Cover: domain powers off at least once (completeness)
  ISO_COV_POWEROFF: cover property (
    @(posedge clk) $fell(vdd_pd_on)
  );

endmodule

## UPF retention rule
create_retention_rule ret_dsp \
    -domain          PD_domain \
    -retention_power_net  VDD_RET_net \
    -save_signal    {u_pmu.ret_save   high} \
    -restore_signal {u_pmu.ret_restore high}

map_retention_cell ret_dsp \
    -domain   PD_domain \
    -lib_cell DFFR_X2        # retention FF from std-cell library

// Retention sequence verification — SVA
// Check that restore fires only AFTER power-good is stable

ISO_RET_RESTORE_AFTER_PG: assert property (
  @(posedge clk)
  $rose(ret_restore) |-> $past(pg_vdd_pd, 2)
) else $error("[RETENTION] restore asserted before power-good stabilised");

// Check that save fires while domain supply is still ON
RET_SAVE_WHILE_ON: assert property (
  @(posedge clk)
  $rose(ret_save) |-> vdd_pd_on
) else $error("[RETENTION] save asserted after domain power dropped");

// Functional check: data survives a save-poweroff-restore cycle
// (done in the UVM scoreboard)
task automatic check_retention_cycle(
  input logic [31:0] expected_val
);
  // 1. sample DUT register value before save
  logic [31:0] pre_save = dut.u_dsp.cfg_reg;
  assert(pre_save === expected_val) else
    $error("pre-save mismatch: got %0h exp %0h", pre_save, expected_val);

  // 2. drive save sequence
  @(posedge clk); ret_save = 1;
  @(posedge clk); ret_save = 0;

  // 3. power down
  vdd_pd_force = 0.0;
  #100ns;

  // 4. power up, wait PG, then restore
  vdd_pd_force = 0.9;
  @(posedge pg_vdd_pd);
  repeat(2) @(posedge clk);
  ret_restore = 1;
  @(posedge clk); ret_restore = 0;

  // 5. verify restored value
  @(posedge clk);
  logic [31:0] post_restore = dut.u_dsp.cfg_reg;
  assert(post_restore === expected_val) else
    $error("[RETENTION] data corrupted: got %0h exp %0h", post_restore, expected_val);
endtask

// Power State Table functional coverage
typedef enum logic [1:0] {
  NORMAL      = 2'b00,
  DSP_SLEEP   = 2'b01,
  MEM_RETAIN  = 2'b10,
  DEEP_SLEEP  = 2'b11
} pst_state_t;

covergroup pst_coverage @(posedge clk);
  // Every legal PST state must be hit
  cp_state: coverpoint current_pst {
    bins normal_op  = {NORMAL};
    bins dsp_off    = {DSP_SLEEP};
    bins mem_retain = {MEM_RETAIN};
    bins deep_sleep = {DEEP_SLEEP};
  }

  // All legal transitions must be exercised
  cp_transition: coverpoint current_pst {
    bins to_dsp_sleep[]  = (NORMAL     => DSP_SLEEP);
    bins to_mem_retain[] = (DSP_SLEEP  => MEM_RETAIN);
    bins to_deep_sleep[] = (MEM_RETAIN => DEEP_SLEEP);
    bins wakeup_fast[]   = (DSP_SLEEP  => NORMAL);
    bins full_wakeup[]   = (DEEP_SLEEP => MEM_RETAIN => DSP_SLEEP => NORMAL);

    // Illegal: skip retention save — must NEVER be covered
    illegal_bins skip_retention = (NORMAL => DEEP_SLEEP);
    illegal_bins mem_skip       = (DSP_SLEEP => DEEP_SLEEP);
  }

  // Cross: ensure both DSP and memory domains reach OFF state
  cx_domain_off: cross vdd_pd_on, vdd_mem_on;
endgroup

// Instantiate and sample
pst_coverage pst_cov_i = new();
always @(posedge clk) pst_cov_i.sample();

// X-propagation containment check — assert no X escapes the isolation boundary
property p_no_x_on_ao_input;
  @(posedge clk)
  !$isunknown(ao_input_bus);  // ao_input_bus = post-isolation signals
endproperty

NO_X_CROSSING: assert property(p_no_x_on_ao_input)
  else $error("[XPROP] X value detected on AO domain input — isolation cell failure");

// Complementary: when domain IS powered and NOT isolated,
// signal must NOT be stuck at the clamp value
property p_not_stuck_clamped;
  @(posedge clk)
  (vdd_pd_on && !iso_en) |-> !$stable(ao_input_bus);  // data should toggle
endproperty
// (Use cover, not assert, for this — it is a coverage goal)
COVER_DATA_TOGGLING: cover property(p_not_stuck_clamped);

## Questa PA simulation Makefile recipe

# Step 1 — Compile RTL (SystemVerilog + UPF simultaneously)
vlog  -sv \
      -work    work \
      rtl/top.sv rtl/pmu.sv rtl/dsp_core.sv \
      tb/top_tb.sv tb/isolation_checks.sv

# Step 2 — Elaborate with UPF loaded
vopt  work.top_tb \
      -upf         upf/top.upf \
      -upf_mode    abstract \     # or 'full' for gate-level
      -pa_upf_analyze \          # structural check during elab
      -access      rw+/acc=rn \
      -o           top_tb_opt

# Step 3 — Simulate with PA checks enabled
vsim  top_tb_opt \
      -upf         upf/top.upf \
      -pa \                       # enable Power Aware mode
      -pa_upf_check on \         # runtime UPF rule checking
      -sv_seed     random \
      -xprop       xprop.cfg \   # extended X propagation
      +UVM_TESTNAME=low_power_test \
      -do          "run -all; quit -f"

# xprop.cfg — tell Questa which X-propagation mode to use
# File: xprop.cfg
#   xprop_mode  = fuzzy
#   latch_mode  = X
#   enable_x_check = 1

// Bug example: polarity inversion in RTL vs UPF

// RTL (DFF_RET behavioural model — active LOW save)
always @(posedge clk or negedge rst_n) begin
  if (!rst_n)       Q   <= 0;
  else if (!save_n) shadow <= D;   // saves when save_n=0 (ACTIVE LOW)
  else              Q   <= D;
end

// UPF (incorrectly written as active HIGH)
// create_retention_rule ret_r -save_signal {pmu.ret_save HIGH}
//                                                        ^^^^
// UPF thinks save occurs when ret_save=1
// RTL saves when ret_save=0 → save never happens at right time

// FIX: match UPF to RTL polarity
// create_retention_rule ret_r -save_signal {pmu.ret_save LOW}