Exploiting Dual-Rail Register Invariants for Equivalence Verification of NCL Circuits

Equivalence checking is one of the most scalable and useful verification techniques in industry. NULL Convention Logic (NCL) circuits utilize dual-rail signals (i.e., two wires to represent one bit of DATA), where the wires are inverses of each other during a DATA wavefront. In this paper, a techniq...

Full description

Saved in:
Bibliographic Details
Main Authors: Le, Son N., Srinivasan, Sudarshan K., Smith, Scott C.
Format: Conference Proceeding
Language:English
Subjects:
asynchronous circuits
equivalence checking
formal methods
Formal verification
Industries
Logic gates
NULL Convention Logic
Rails
Registers
Synchronization
Wires
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Equivalence checking is one of the most scalable and useful verification techniques in industry. NULL Convention Logic (NCL) circuits utilize dual-rail signals (i.e., two wires to represent one bit of DATA), where the wires are inverses of each other during a DATA wavefront. In this paper, a technique that exploits this invariant at NCL register boundaries is proposed to improve the efficiency of equivalence verification of NCL circuits.
ISSN:1558-3899
DOI:10.1109/MWSCAS48704.2020.9184477