Rtl Property Inference

RTL Property Inference

Overview

This skill analyzes Verilog/SystemVerilog RTL code and automatically infers implicit correctness properties, generating formal SystemVerilog Assertions (SVA). The skill identifies common hardware patterns and generates appropriate safety, liveness, and fairness properties with clear explanations.

Workflow

Step 1: Parse and Understand RTL Structure

Analyze the input RTL code to extract key components:

1. Identify signals and their roles:

   • Clock and reset signals
   • Control signals (valid, ready, enable, grant, request)
   • Data signals
   • State variables (FSM states, counters, flags)

2. Recognize structural patterns:

   • State machines (one-hot, binary encoded)
   • Handshake protocols (valid-ready, req-ack)
   • Pipelines (with/without stalls)
   • FIFOs and buffers
   • Arbiters and mutual exclusion logic
   • Counters (saturating, wraparound)
   • Memory interfaces

3. Extract clock/reset conventions:

   • Clock signal name and edge (posedge/negedge)
   • Reset signal name, polarity (active high/low), and type (sync/async)
   • Reset values for state variables

Step 2: Identify Control-Flow Invariants

Systematically analyze the design for common invariant patterns:

1. Mutual Exclusion:

   • Grant signals from arbiters
   • Mutually exclusive enable signals
   • One-hot state encodings
   • Look for: Multiple signals that should never be active simultaneously

2. Valid-Ready Handshakes:

   • Data stability during valid-without-ready
   • Valid persistence until handshake completes
   • No data loss (eventual completion)
   • Look for: Pairs of valid/ready signals with associated data

3. Pipeline Ordering:

   • Valid bit propagation through stages
   • Data stability in pipeline stages
   • Stall behavior (freezing pipeline state)
   • Look for: Arrays of valid signals, stage indices, pipeline registers

4. Safety Properties (bad things never happen):

   • Buffer overflow/underflow prevention
   • Invalid state detection
   • Address conflict prevention
   • Counter bounds
   • Look for: Boundary conditions, error states, conflict scenarios

Step 3: Identify Liveness Properties

Look for patterns indicating "good things eventually happen":

1. Request-Response Patterns:

   • Request eventually gets grant
   • Valid eventually gets ready
   • Transaction eventually completes
   • Look for: Request signals paired with acknowledgment/grant signals

2. Progress Properties:

   • FSM eventually leaves certain states
   • Counters eventually reach targets
   • Pipelines eventually drain
   • Look for: Temporary states, countdown logic, completion conditions

3. Fairness Constraints:

   • All requesters eventually get service
   • Round-robin behavior
   • Starvation freedom
   • Look for: Arbitration logic, scheduling mechanisms

Note: Liveness properties require careful analysis. Only infer when there's clear evidence of intended eventual behavior. Use bounded liveness (with timeouts) when unbounded liveness may not hold.

Step 4: Map Patterns to Properties

Use the pattern library in common_patterns.md to generate appropriate assertions:

1. Match identified patterns to known property templates
2. Instantiate properties with actual signal names from the design
3. Adjust timing parameters based on design characteristics (e.g., pipeline depth, timeout values)
4. Add appropriate disable conditions (typically reset)

Refer to sva_syntax.md for SVA syntax details.