Compatible Equivalence Checking of X-Valued Circuits
Yu-Neng Wang*, Yun-Rong Luo*, Po-Chun Chien*, Ping-Lun Wang, Hao-Ren Wang, Wan-Hsuan Lin, Jie-Hong Roland Jiang, Chung-Yang Ric Huang. In International Conference On Computer Aided Design (ICCAD), 2021.
Our X-valued circuits equivalence checker won the first place of problem A in the 2020 CAD Contest. In this paper, we present our winning method based on X-value preserving dual-rail encoding and incremental identification of compatible equivalence relation.
Paper
Abstract
The X-value arises in various contexts of system design. It often represents an unknown value or a don’t-care value depending on the application. Verification of X-valued circuits is a crucial task but relatively unaddressed. The challenge of equivalence checking for X-valued circuits, named compatible equivalence checking, is posed in the 2020 ICCAD CAD Contest. In this paper, we present our winning method based on X-value preserving dual-rail encoding and incremental identification of compatible equivalence relation. Experimental results demonstrate the effectiveness of the proposed techniques and the outperformance of our approach in solving more cases than the commercial tool and the other teams among the top 3 of the contest.
Citation
@inproceedings{wang_compatible_2021,
author={Wang, Yu-Neng and Luo, Yun-Rong and Chien, Po-Chun and Wang, Ping-Lun and Wang, Hao-Ren and Lin, Wan-Hsuan and Jiang, Jie-Hong Roland and Huang, Chung-Yang Ric},
booktitle={2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)},
title={Compatible Equivalence Checking of X-Valued Circuits},
year={2021},
volume={},
number={},
pages={1-9},
keywords={Design automation;Encoding;Task analysis},
doi={10.1109/ICCAD51958.2021.9643515}}