Compatible Equivalence Checking of X-Valued Circuits

Published in Proceedings of the International Conference on Computer-Aided Design (ICCAD), 2021

Recommended citation: Y.-N. Wang, Y.-R. Luo, P.-C. Chien, P.-L. Wang, H.-R. Wang, W.-H. Lin, J.-H. R. Jiang and C.-Y. R. Huang, "Compatible Equivalence Checking of X-Valued Circuits," in Proc. ICCAD, 2021. To appear.

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.

To cite the paper, you may use the following BibTex entry.

@inproceedings{Chien:ICCAD:2021,
    author      = {Yu-Neng Wang and Yun-Rong Luo and Po-Chun Chien and Ping-Lun Wang and Hao-Ren Wang and Wan-Hsuan Lin and Jie-Hong Roland Jiang and Chung-Yang Ric Huang},
    title       = {Compatible Equivalence Checking of X-Valued Circuits},
    booktitle   = {Proc. ICCAD},
    year        = {2021},
    note        = {To appear}
}