rtl-equivalence-checker

RTL Equivalence Checker

Verify functional equivalence between two RTL designs with detailed analysis and counterexample generation.

Overview

This skill compares two Verilog RTL designs to determine if they are functionally equivalent. It aligns interfaces and state variables, distinguishes semantic differences from cosmetic refactoring, and generates minimal counterexample traces when designs differ.

Workflow

1. Basic Equivalence Check

Compare two RTL designs:

python3 scripts/check_equivalence.py design_a.v design_b.v

Output includes:

• Equivalence verdict (EQUIVALENT or NOT EQUIVALENT)
• Explanation of differences
• Counterexample trace (if not equivalent)

2. With Assumptions

Specify clock and reset behavior:

python3 scripts/check_equivalence.py design_a.v design_b.v \
  --clock clk \
  --reset rst_n \
  --reset-active low

3. Save Results

Write results to file:

python3 scripts/check_equivalence.py design_a.v design_b.v -o results.txt

4. Ignore Signal Names

Focus on functional behavior, ignore naming differences:

python3 scripts/check_equivalence.py design_a.v design_b.v --ignore-names

Analysis Process

The checker performs five steps:

[1/5] Parsing RTL designs

• Extracts module structure
• Identifies ports, signals, and state elements
• Parses always blocks and assignments

[2/5] Aligning interfaces and state variables

• Matches ports by name and type
• Aligns state elements (registers)
• Reports unmatched signals

[3/5] Analyzing behavioral differences

• Identifies cosmetic differences (naming, formatting)
• Identifies semantic differences (logic changes)
• Categorizes difference types

[4/5] Determining equivalence

• Verdict: EQUIVALENT or NOT EQUIVALENT
• Based on semantic differences only
• Cosmetic differences don't affect equivalence

[5/5] Generating counterexample (if not equivalent)

• Creates minimal test sequence
• Shows input values that expose difference
• Traces outputs from both designs