UPF Formal Verification

Formal verification explores ALL possible behaviors mathematically, finding bugs that simulation would take billions of cycles to discover. For power management—where subtle corner cases can cause catastrophic failures—formal is essential.

Formal Verification Fundamentals

Simulation vs. Formal

How Formal Works

Formal verification tools use mathematical techniques (model checking, SAT solving) to explore the entire state space of your design:

1. You specify PROPERTIES (assertions) about correct behavior
   Example: "When domain powers down, all outputs must be isolated"

2. Formal tool explores ALL possible input sequences
   - All possible reset scenarios
   - All possible control signal combinations
   - All possible timing relationships

3. Tool attempts to prove property is always true
   OR finds a COUNTEREXAMPLE showing when property fails

4. If proven: Mathematical guarantee property holds for ALL cases
   If counterexample: Minimal trace showing how to trigger the bug

Think of formal verification as asking the tool: "Is there ANY way to violate this property?" If the tool says "no" and provides a proof, you have mathematical certainty.

Writing Power Intent Assertions (SVA)

System Verilog Assertions (SVA) specify properties that must always hold.

Basic Assertion Syntax

// Basic assertion structure
assert property (@(posedge clk) disable iff (!rst_n)
  condition |-> consequence
);

Assertion #1: Isolation Prevents X-Propagation

// Property: When GPU powers down, isolation prevents X-propagation
property iso_prevents_x_propagation;
  @(posedge clk) disable iff (!rst_n)
  ($fell(gpu_power_enable))  // GPU powers down
  |->
  ##1 !$isunknown(noc_router_input)  // Next cycle: no X on NOC input
endproperty

assert property (iso_prevents_x_propagation)
  else $error("X-propagation detected from GPU to NOC");

Assertion #2: Retention Preserves State

// Property: CPU state retained across power cycle
logic [31:0] saved_pc;

sequence power_down_sequence;
  (cpu_save_enable ##1 !cpu_save_enable ##1 !cpu_power_enable);
endsequence

sequence power_up_sequence;
  (cpu_power_enable ##[10:100] cpu_restore_enable);
endsequence

property retention_correctness;
  @(posedge clk) disable iff (!rst_n)
  (power_down_sequence, saved_pc = cpu_pc)  // Save PC value
  ##1 !cpu_power_enable [*1:$]              // Stay powered down
  ##1 power_up_sequence                     // Power back up
  |->
  ##2 (cpu_pc == saved_pc)                  // PC value preserved
endproperty

assert property (retention_correctness)
  else $error("Retention failed: PC corrupted");

Assertion #3: Power Sequencing Constraints

// Property: IO domain must be on for 10 cycles before core powers up
property io_powers_up_first;
  @(posedge clk) disable iff (!rst_n)
  $rose(core_power_enable)
  |->
  $past(io_power_enable, 10) &&  // IO was on 10 cycles ago
  $past(io_power_enable, 9) &&   // ... and 9 cycles ago
  $past(io_power_enable, 8) &&   // ... and 8 cycles ago
  // ... (or use $stable for cleaner expression)
  $stable(io_power_enable, 10)[*10]  // IO stable for 10 cycles
endproperty

assert property (io_powers_up_first)
  else $error("Core powered up before IO stable");

Assertion #4: Illegal State Transition Detection

// Property: GPU cannot go directly from DVFS to POWEROFF
property no_direct_dvfs_to_poweroff;
  @(posedge clk) disable iff (!rst_n)
  (gpu_state == DVFS) ##1 (gpu_state == POWEROFF)
  |->
  1'b0  // This transition is always illegal
endproperty

assert property (no_direct_dvfs_to_poweroff)
  else $error("Illegal power state transition: DVFS -> POWEROFF");

Using Industry Formal Tools

JasperGold (Cadence) Example

# JasperGold formal verification script
analyze -sv design.sv assertions.sv upf_assertions.sv
elaborate -top top_design

# Load UPF
upf load_upf top_level.upf

# Clock and reset setup
clock clk
reset -expression {!rst_n}

# Prove assertions
prove -all

# Check results
report -results

VC Formal (Synopsys) Example

# VC Formal script
analyze -format sverilog design.sv assertions.sv
elaborate top_design

# Load UPF for power-aware formal
upf_load_upf top_level.upf

# Setup
clock clk
reset rst_n

# Run formal verification
prove -property {iso_prevents_x_propagation}
prove -property {retention_correctness}
prove -property {io_powers_up_first}

# Generate report
report -summary

Formal Verification Flow for UPF

Step 1: Write Assertions (SVA)
  - Isolation completeness
  - Retention correctness
  - Power sequencing
  - State transition validity

Step 2: Setup Formal Tool
  - Load RTL + UPF
  - Configure clocks, resets
  - Set proof bounds (depth)

Step 3: Run Formal Analysis
  - Tool explores state space
  - Attempts to prove each assertion
  - OR finds counterexamples

Step 4: Analyze Results
  - PROVEN: Property holds (mathematical guarantee)
  - FAIL: Counterexample found (real bug)
  - INCONCLUSIVE: Need deeper bounds or constraints

Step 5: Fix Bugs and Re-verify
  - Fix RTL or UPF based on counterexample
  - Re-run formal to prove fix is correct

Example Complete Formal Session

$ jaspergold -batch formal_upf.tcl

JasperGold Formal Verification
Loading design... OK
Loading UPF... OK
Analyzing assertions... Found 8 properties

Proving properties:

1. iso_prevents_x_propagation: PROVEN (depth 15, 45 seconds)
2. retention_correctness: PROVEN (depth 25, 120 seconds)
3. io_powers_up_first: PROVEN (depth 10, 8 seconds)
4. no_direct_dvfs_to_poweroff: FAIL (counterexample found)

Counterexample for no_direct_dvfs_to_poweroff:
  Cycle 0: reset
  Cycle 5: gpu_state = ACTIVE
  Cycle 10: deep_sleep_request = 1
  Cycle 11: gpu_state = DVFS (FSM transitions to DVFS)
  Cycle 12: emergency_shutdown = 1 (unexpected signal!)
  Cycle 13: gpu_state = POWEROFF (FSM bypasses STANDBY)

ROOT CAUSE: emergency_shutdown signal bypasses normal FSM
FIX NEEDED: Add assertion or fix FSM to go through STANDBY even on emergency

5. retention_timing_save_before_powerdown: PROVEN (depth 30, 90 seconds)

Summary:
  Proven: 7/8
  Failed: 1/8
  Inconclusive: 0/8

Total runtime: 4 minutes 23 seconds

Common Formal Verification Patterns for UPF

Pattern #1: Isolation Completeness

// Verify ALL cross-domain signals have isolation
genvar i;
generate
  for (i = 0; i < NUM_GPU_OUTPUTS; i++) begin : gen_iso_check
    assert property (@(posedge clk) disable iff (!rst_n)
      !gpu_power_enable |-> !$isunknown(noc_inputs[i])
    );
  end
endgenerate

Pattern #2: Retention Coverage

// Verify all critical state is retained
genvar j;
generate
  for (j = 0; j < 32; j++) begin : gen_reg_retention
    logic [31:0] saved_reg;

    assert property (@(posedge clk) disable iff (!rst_n)
      (cpu_save_enable, saved_reg = cpu_regs[j])
      ##1 !cpu_power_enable [*1:$]
      ##1 cpu_restore_enable
      |-> ##1 (cpu_regs[j] == saved_reg)
    );
  end
endgenerate

Pattern #3: Power Sequencing

// Verify power-up sequencing: IO -> Core -> peripherals
sequence correct_powerup_sequence;
  (!io_power_enable && !core_power_enable) ##1
  (io_power_enable && !core_power_enable) [*10:$] ##1
  (io_power_enable && core_power_enable) [*5:$] ##1
  (io_power_enable && core_power_enable && peripheral_power_enable);
endsequence

assert property (@(posedge clk) disable iff (!rst_n)
  $rose(system_power_on) |-> correct_powerup_sequence
);

Common Beginner Mistakes

// WRONG: Too many constraints may hide bugs
assume property (gpio_power_enable == 1'b1);  // GPIO always on
assume property (cpu_state != DVFS);  // CPU never in DVFS

// This prevents formal from exploring the bug scenario!

// CORRECT: Only assume necessary constraints
assume property (rst_n == 0 |=> gpio_power_enable == 0);  // Only during reset

// WEAK: Doesn't catch all X-propagation
assert property (!gpu_power_enable |-> noc_input != 'x);
// Problem: Only checks if entire bus is X, not individual bits

// STRONG: Catches any X on any bit
assert property (!gpu_power_enable |-> !$isunknown(noc_input));

Property: complex_retention_property - INCONCLUSIVE (depth 50)
Reason: State space too large, proof bound reached