Fast RTL-to-RTL LEC API — rtl_lec
We introduce an API for fast RTL-to-RTL Logic Equivalence Checking (LEC). It is especially useful for generating Golden RTL and Golden Spec. The generated spec can be converted back to RTL that is logically equivalent to the original implementation.
API documentation: https://nandigits.co/apis_gof.htm#rtl_lec
What it does
This workflow leverages large language models (LLMs) to extract a clear, machine-readable specification from Verilog code, then regenerates RTL from that specification. The rtl_lec tool compares the regenerated RTL (Golden RTL) with the original implementation to verify semantic equivalence. You can build a valuable dataset of specification and Verilog pairs by converting and verifying RTL files from sources like GitHub.
rtl_lec compare.Usage
rtl_lec
RTL to RTL logic equivalence checking
Usage:
rtl_lec($imp_rtl, $ref_rtl, $module_name, @options);
$imp_rtl: Implementation RTL
$ref_rtl: Reference RTL
$module_name: Top module name
@options:
-help: Print this information
-debug: Debug mode
Example
#1. Compare g1_rtl.v vs g2_rtl.v with module name chip_top
set_define("AGHCD", '12345');
set_inc_dirs("../include", "include2");
rtl_lec("g1_rtl.v", "g2_rtl.v", "chip_top");
Tip: Use the generated spec as a human-readable golden specification for design review, documentation, and regression automation. Because the spec can be converted back to RTL and re-checked, the round-trip guarantees semantic equivalence when the LLM conversion steps are configured properly.