Modern SoC Verification

• 60–70% of SoC development effort is spent on verification — more engineers verify than design
• State-space explosion — a modern SoC with 10¹⁰ transistors has 2¹⁰¹⁰ possible states; exhaustive testing is mathematically impossible
• Bug escape cost — a bug found in silicon costs 1000× more to fix than one caught in RTL simulation
• Schedule pressure — verification is almost always on the critical path to tape-out

Cost of Bug Escape

Event-Driven Simulation

• Principle — evaluate only signals that change; maintain an event queue sorted by simulation time
• Languages — Verilog/SystemVerilog for RTL and testbench; VHDL in aerospace/defense and European designs
• 4-state logic — 0, 1, X, Z model unknown and high-impedance states critical for reset and bus behavior
• Scheduling — Active, Inactive, NBA, Observed, Reactive regions per IEEE 1800 semantics

VCS

Synopsys — compiled sim, fastest single-threaded

Xcelium

Cadence — multi-core parallel simulation

Questa

Siemens — strong debug, UVM integration

Verilator

Open-source — 2-state, cycle-accurate, ~10× faster for synthesizable code

Simulation Speed Hierarchy

// Simple directed test in SystemVerilog
module tb_counter;
  logic clk, rst_n, en;
  logic [7:0] count;

  counter dut(.clk, .rst_n, .en, .count);

  initial begin
    clk = 0;
    forever #5ns clk = ~clk;
  end

  initial begin
    rst_n = 0; en = 0;
    #20ns rst_n = 1;
    #10ns en = 1;
    repeat(256) @(posedge clk);
    $finish;
  end
endmodule

UVM Architecture

• Sequencer — generates stimulus transactions
• Driver — converts transactions to pin-level signals
• Monitor — observes interface, creates transactions
• Scoreboard — reference model comparison

Constrained Random Verification

class axi_transaction extends uvm_sequence_item;
  rand bit [31:0] addr;
  rand bit [7:0]  data[];
  rand axi_burst_e burst_type;
  rand bit [3:0]  len;

  // Constraints focus stimulus on corners
  constraint c_aligned {
    addr[1:0] == 2'b00;  // word-aligned
  }
  constraint c_burst {
    burst_type dist {
      FIXED := 10, INCR := 60, WRAP := 30
    };
  }
  constraint c_len {
    len inside {[0:3], 7, 15};  // AXI legal
  }

  `uvm_object_utils_begin(axi_transaction)
    `uvm_field_int(addr, UVM_ALL_ON)
    `uvm_field_array_int(data, UVM_ALL_ON)
    `uvm_field_enum(axi_burst_e,
                    burst_type, UVM_ALL_ON)
  `uvm_object_utils_end
endclass

Immediate vs Concurrent

// Immediate assertion
always_comb begin
  assert (onehot(grant))
    else $error("Grant not one-hot!");
end

// Concurrent: AXI handshake protocol
property axi_handshake;
  @(posedge clk) disable iff (!rst_n)
  valid |-> s_eventually ready;
endproperty
assert property (axi_handshake)
  else $error("AXI handshake timeout");

// Concurrent: data stability
property axi_stable;
  @(posedge clk) disable iff (!rst_n)
  (valid && !ready) |=>
    ($stable(addr) && $stable(data));
endproperty
assert property (axi_stable);

Property & Sequence Syntax

// Sequence: request followed by grant
sequence req_grant_seq;
  req ##[1:5] gnt;  // 1-5 cycle delay
endsequence

// Property: grant must be followed by ack
property grant_ack_p;
  @(posedge clk) disable iff (!rst_n)
  gnt |-> ##[1:3] ack;
endproperty

// Cover property for functional coverage
cover property (
  @(posedge clk)
  req ##1 gnt ##1 ack
);

Assertion-Based Verification Methodology

• White-box — assertions inside RTL modules; designers write them during coding
• Black-box — interface protocol monitors; verification engineers author
• Formal — same SVA properties proven exhaustively by formal tools
• Coverage — cover property tracks when specific scenarios occur

Coverage Types

covergroup axi_cg @(posedge clk);
  cp_burst: coverpoint burst_type {
    bins fixed = {FIXED};
    bins incr  = {INCR};
    bins wrap  = {WRAP};
  }
  cp_size: coverpoint size {
    bins byte   = {0};
    bins hword  = {1};
    bins word   = {2};
    bins dword  = {3};
  }
  // Cross: all burst x size combos
  bxs: cross cp_burst, cp_size;
endgroup

Coverage Closure Process

Unreachable code/states must be formally proven unreachable and waivered — never silently excluded.

Model Checking Fundamentals

• Bounded — proves properties hold for N clock cycles (e.g., N=50); cannot guarantee behavior beyond bound
• Unbounded — proves property holds for all reachable states forever; uses induction, k-induction, interpolation, or IC3/PDR
• Counterexample — if property fails, tool provides minimal waveform trace to reproduce the bug
• Complexity — state space is 2^N where N = number of state bits; formal typically effective on blocks ≤500K gates

Jasper

Cadence — market leader in formal apps

VC Formal

Synopsys — tight VCS/Verdi integration

Questa Formal

Siemens — strong CDC/formal combo

SymbiYosys

Open-source — Yosys + SMT solvers

Property Types

// Formal assumptions + assertions
// Prove FIFO never overflows
module fifo_formal #(DEPTH=16) (
  input logic clk, rst_n, push, pop
);
  logic [$clog2(DEPTH):0] count;

  // Assumption: environment constraint
  assume property (@(posedge clk)
    disable iff (!rst_n)
    (count == DEPTH) |-> !push);

  // Assertion: count never exceeds DEPTH
  assert property (@(posedge clk)
    disable iff (!rst_n)
    count <= DEPTH);

  // Liveness: FIFO eventually drains
  assert property (@(posedge clk)
    disable iff (!rst_n)
    (count > 0) |-> s_eventually (count == 0));
endmodule

Lint — RTL Code Quality

• Spyglass (Synopsys) — industry standard for lint + CDC + power
• Ascent (Real Intent) — advanced X-analysis and reset checking
• Catches: width mismatches, undriven nets, incomplete sensitivity lists, inferred latches, multi-driven signals, naming convention violations
• Mandatory step before synthesis; clean lint = fewer downstream surprises

CDC — Clock Domain Crossing

• Single biggest cause of silicon respins — metastability bugs are non-deterministic, nearly impossible to catch in simulation
• Structural checks: synchronizer detection, FIFO depth adequacy, convergence, reconvergence
• Formal CDC: prove data coherency and no data loss across domains using formal methods

RDC — Reset Domain Crossing

• Similar to CDC but for asynchronous reset release across domains
• Verify reset sequencing, ordered de-assertion, and no glitches during reset release
• Critical in power-managed SoCs with many reset domains

Power-Aware Checks

Emulation Platforms

Compile Flow

Use Cases

• Software-driven verification — boot real firmware, RTOS, Linux kernel; find HW/SW co-design bugs
• Long-sequence tests — run billions of cycles: PCIe link training, DDR initialization, USB enumeration
• Power estimation — FSDB/VCD activity dumped from emulator fed to power analysis tools (Joules/PrimeTime PX)
• Low-power verification — UPF-aware emulation validates power domain transitions at speed

ICE Mode

In-Circuit Emulation — real external interfaces (PCIe, Ethernet)

SCE Mode

Simulation Co-Emulation — testbench in simulator, DUT in emulator

Speed

1–10 MHz (design dependent)

Cost

$5M–$50M+ per system

Compile

Hours to days for full SoC (incremental: minutes)

FPGA Prototyping Platforms

Partitioning Challenges

• Multi-FPGA partitioning — large SoCs span 4–16+ FPGAs; inter-FPGA routing adds latency and reduces frequency
• Memory mapping — on-chip SRAMs must be mapped to FPGA block RAMs or external DRAM
• Clock conversion — multi-clock designs require careful PLL configuration across FPGAs
• Hard IP — SerDes, analog blocks, and custom memory macros need behavioral models or bypass

Emulation vs FPGA Prototyping

Integration Checklist

1. IP connectivity — all ports wired, no dangling nets, correct polarity (active-high/low), width matching
2. Address map — decode logic matches spec; no aliasing or holes; all CSRs accessible from correct masters
3. Interrupt routing — all IRQ lines reach GIC/PLIC; edge/level sensitivity correct; no missed or spurious interrupts
4. Clock & reset topology — each IP gets correct clock and reset; gating/ungating sequences verified
5. Power domain mapping — isolation/retention cells correctly inserted; power sequencing validated
6. DMA paths — all DMA channels reach intended memory regions through correct NoC routes

Integration Verification Methods

SoC Verification Architecture

DFT Techniques

Scan Architecture

JTAG / IEEE 1149.1

• TAP Controller — 4-wire interface (TCK, TMS, TDI, TDO) + optional TRST
• Boundary Scan — test board-level connectivity without physical probes; each pin has a boundary scan cell
• IJTAG (IEEE 1687) — hierarchical access to on-chip instruments (MBIST, sensors, debug) through scan infrastructure
• IEEE 1838 — 3D test access for die-to-die testing in stacked packages

Manufacturing Test Economics

Test time

100ms–2s per die (cost: $0.01–$0.10/sec on ATE)

DPPM

Target <10 Defective Parts Per Million

Test cost

5–15% of total chip manufacturing cost

Pattern count

10K–1M+ patterns (compressed on-chip)

Traffic Generation & Analysis

• Synthetic traffic generators — programmable AXI/CHI masters that inject controlled read/write patterns with configurable burst size, outstanding transactions, and address distribution
• Trace-driven replay — capture real workload traces (from FPGA prototype or architecture sim) and replay on RTL
• Performance monitors — on-chip counters for latency histograms, bandwidth measurement, queue occupancy, stall cycles

Key Performance Metrics

Read Latency

Cycles from AXI AR to R-last (target: <100 cycles to DDR)

BW Utilization

Achieved / theoretical peak (target: >80%)

QoS Violation

% transactions exceeding deadline (target: 0%)

Interconnect Contention

NoC link saturation under worst-case traffic

NoC Performance Validation

Memory Subsystem Verification

• DDR protocol verification — VIP checks timing (tRCD, tRP, tRFC), command sequencing, refresh, and training
• Cache coherency — ACE/CHI protocol checks; coherence race conditions; snoop filter correctness
• End-to-end data integrity — ECC injection, poison propagation, and error reporting paths

Systolic Array Verification

• Matrix multiply correctness — verify NxN PE arrays against golden reference for all supported precisions (FP32, FP16, BF16, FP8, INT8, INT4)
• Dataflow validation — weight-stationary, output-stationary, and row-stationary patterns; verify data movement matches architecture spec
• Boundary conditions — non-square matrices, partial tiles, zero padding, accumulator overflow/underflow
• Numerical precision — FP8 (E4M3/E5M2) rounding modes, denormal handling, NaN/Inf propagation, mixed-precision accumulation (e.g., FP8 multiply → FP32 accumulate)

DMA Engine Challenges

• Multi-dimensional tensor DMA: strided access, transpose, tiling
• Outstanding transaction management across multiple channels
• Coherency with CPU caches when sharing data buffers
• Descriptor chain verification: linked-list DMA, scatter-gather

Multi-Clock NPU Domains

End-to-End Inference Validation

• Golden model — PyTorch/TensorFlow reference output (bit-accurate after quantization)
• Compiler verification — verify that the NPU compiler's generated command stream produces correct layer-by-layer outputs
• Full-network tests — run ResNet-50, BERT, GPT inference on emulator; compare output tensors against golden (tolerance: ≤1 ULP for INT, ≤0.1% relative for FP)

Regression Management

• Nightly regressions — 10K–100K+ test seeds run across server farm; results triaged by morning
• Seed management — failed seeds saved and replayed for debug; passing seeds archived for coverage
• Coverage merging — aggregate coverage across all tests, seeds, and platforms (sim + emulation + formal)
• Incremental regressions — only re-run tests affected by RTL changes (dependency tracking)

Bug Rate Curves

• Bug discovery rate plotted over time — must show clear declining trend before signoff
• Weibull model — project remaining bugs from observed bug-find rate; predict when target bug density is reached
• All P0/P1 bugs must be resolved; P2 bugs waivered with documented risk

Tape-Out Verification Checklist