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