Abstract
Equivalence checking tools often use a flip-flop matching step to avoid the state space traversal. Due to sequential optimizations performed during synthesis (merge, replication, redundancy removal, dots) and don't care conditions, the matching step can be very complex as well as incomplete. If the matching is incomplete, even the use of a fast and efficient SAT solver during the combinational equivalence-checking step may not prevent the failure of this approach. In this paper, we present a flip-flop matching engine, which is able to verify optimized circuits and handle don't care conditions.
Keywords
- Equivalence checking
- synthesis
- matching
- combinational equivalence checking
- sequential optimizations
- redundancy removal
- don't care conditions
Cite this article
@article{cai-1502,
author = {Solaiman Rahim and Bruno Rouzeyre and Lionel Torres},
title = {A Flip-Flop Matching Engine to Verify Sequential Optimizations},
journal = {Computing and Informatics},
volume = {23},
number = {5-6},
pages = {437--460},
year = {2004},
issn = {1335-9150},
url = {https://cai.type.sk/content/2004/5-6/a-flip-flop-matching-engine-to-verify-sequential-optimizations/}
}
TY - JOUR AU - Solaiman Rahim AU - Bruno Rouzeyre AU - Lionel Torres TI - A Flip-Flop Matching Engine to Verify Sequential Optimizations JO - Computing and Informatics VL - 23 IS - 5-6 SP - 437 EP - 460 PY - 2004 SN - 1335-9150 UR - https://cai.type.sk/content/2004/5-6/a-flip-flop-matching-engine-to-verify-sequential-optimizations/ KW - Equivalence checking KW - synthesis KW - matching KW - combinational equivalence checking KW - sequential optimizations KW - redundancy removal KW - don't care conditions ER -
Rahim, S., Rouzeyre, B., & Torres, L. (2004). A Flip-Flop Matching Engine to Verify Sequential Optimizations. Computing and Informatics, 23(5-6), 437–460. https://cai.type.sk/content/2004/5-6/a-flip-flop-matching-engine-to-verify-sequential-optimizations/