Hardware verification tool for checking functional equivalence between two RTL designs (Verilog). Use when users need to: (1) Verify if two RTL versions are functionally equivalent, (2) Compare original vs. refactored RTL code, (3) Validate design changes or optimizations, (4) Identify semantic vs. cosmetic differences, (5) Generate counterexamples for non-equivalent designs. Analyzes interface alignment, state variables, logic differences, and produces detailed equivalence verdicts with plain language explanations. Particularly effective for design verification, code reviews, and regression testing of RTL modifications.
Verify functional equivalence between two RTL designs with detailed analysis and counterexample generation.
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.
Compare two RTL designs:
python3 scripts/check_equivalence.py design_a.v design_b.v
Output includes:
Specify clock and reset behavior:
python3 scripts/check_equivalence.py design_a.v design_b.v \
--clock clk \
--reset rst_n \
--reset-active low
Write results to file:
python3 scripts/check_equivalence.py design_a.v design_b.v -o results.txt
Focus on functional behavior, ignore naming differences:
python3 scripts/check_equivalence.py design_a.v design_b.v --ignore-names
The checker performs five steps:
[1/5] Parsing RTL designs
[2/5] Aligning interfaces and state variables
[3/5] Analyzing behavioral differences
[4/5] Determining equivalence
[5/5] Generating counterexample (if not equivalent)
======================================================================
EQUIVALENCE CHECKING RESULTS
======================================================================
Verdict: EQUIVALENT
Explanation:
----------------------------------------------------------------------
The two RTL designs are functionally equivalent. All differences are
cosmetic (naming, formatting, or structurally equivalent refactoring).
Cosmetic Differences (non-functional):
----------------------------------------------------------------------
- module_name: Module names differ: 'counter_v1' vs 'counter_v2'
- signal_name: Signal 'cnt' renamed to 'count_value'
======================================================================
======================================================================
EQUIVALENCE CHECKING RESULTS
======================================================================
Verdict: NOT EQUIVALENT
Explanation:
----------------------------------------------------------------------
The logic in always block 0 differs between the two designs, which
will result in different behavior. The sensitivity list for always
block 0 differs, which may cause the block to trigger at different
times.
Semantic Differences (functional):
----------------------------------------------------------------------
- sensitivity_list: Block 0: Different sensitivity: 'posedge clk
or posedge rst' vs 'posedge clk'
Location: always block 0
- logic_difference: Block 0: Logic differs
Location: always block 0
Counterexample Trace:
----------------------------------------------------------------------
Length: 3 cycles
Cycle 0:
Inputs: {'clk': 0, 'rst': 1, 'enable': 0}
Output A: output_a_01
Output B: output_b_02
MISMATCH: Outputs differ: A=output_a_01, B=output_b_02
======================================================================
Scenario: Refactored RTL for readability, need to verify functionality unchanged.
Approach:
Example:
python3 scripts/check_equivalence.py original.v refactored.v
Scenario: Optimized design for area/timing, need to verify correctness.
Approach:
Scenario: Fixed a bug, want to understand impact on behavior.
Approach:
Scenario: Reviewing RTL changes in pull request.
Approach:
These don't affect behavior:
These change behavior:
See: equivalence_patterns.md for detailed examples
Designs are functionally equivalent. Safe to:
Designs differ functionally. Actions:
Counterexample shows:
Specify non-standard signal names:
python3 scripts/check_equivalence.py design_a.v design_b.v \
--clock sys_clk \
--reset async_rst \
--reset-active high
Control trace length:
python3 scripts/check_equivalence.py design_a.v design_b.v \
--max-depth 50
This skill provides pre-analysis before running formal verification tools.
Workflow:
See: formal_tools.md for formal tool integration
This skill provides heuristic analysis. For rigorous proof:
Limitations:
Best for:
Interface mismatch: Ports don't align between designs.
Too many differences: Hard to understand results.
No counterexample: Semantic difference found but no trace.
False positive: Reports difference but designs seem equivalent.