Parallel Combinational Equivalence Checking

被引:1
作者
Possani, Vinicius N. [1 ]
Mishchenko, Alan [2 ]
Ribas, Renato P. [1 ]
Reis, Andre I. [1 ]
机构
[1] Univ Fed Rio Grande do Sul, Inst Informat, BR-91501970 Porto Alegre, RS, Brazil
[2] Univ Calif Berkeley, Dept EECS, Berkeley, CA 94720 USA
关键词
Parallel processing; Engines; Runtime; Tools; Integrated circuit modeling; Solid modeling; Computational modeling; Combinational equivalence checking (CEC); digital integrated circuit (IC) design; graph partitioning; parallel computing; verification; SAT; VERIFICATION; EDA;
D O I
10.1109/TCAD.2019.2946254
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Combinational equivalence checking (CEC) has been widely applied to ensure design correctness after logic synthesis and technology-dependent optimization in digital integrated circuit design. CEC runtime is often critical for large designs, even when advanced techniques are employed. Three complementary ways for enabling parallelism in CEC are proposed, addressing different design and verification scenarios. The experimental results have demonstrated the speedups up to 63x when comparing the proposed approach to a single-threaded implementation of a similar CEC engine. A practical impact of such a speedup, for instance, is the runtime reduction from 19 h to only 18 min when checking equivalence of AND-inverter graphs comprising more than 20 million nodes. Therefore, the proposed solution presents great potential for improving current electronic design automation environments.
引用
收藏
页码:3081 / 3092
页数:12
相关论文
共 54 条
[1]  
Amaru L., 2015, PROC 24 INT WORKSHOP, P57
[2]   Exploiting Circuit Duality to Speed Up SAT [J].
Amaru, Luca ;
Gaillardon, Pierre-Emmanuel ;
Mishchenko, Alan ;
Ciesielski, Maciej ;
De Micheli, Giovanni .
2015 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI, 2015, :101-106
[3]  
[Anonymous], ABC: A System for Sequential Synthesis and Verification, Release 90215
[4]  
[Anonymous], 2003, Electronic Notes in Theoretical Computer Science, DOI DOI 10.1016/S1571-0661(05)82542-3
[5]  
Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[6]  
Balyo T., 2018, PARALLEL SATISFIABIL, P31
[7]   HordeSat: A Massively Parallel Portfolio SAT Solver [J].
Balyo, Tomas ;
Sanders, Peter ;
Sinz, Carsten .
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2015, 2015, 9340 :156-172
[8]  
Biere A., 2010, FMV REPORT SERIES TE, V10, P1
[9]  
Biere A., 2018, SAT-Based Model Checking, P277
[10]  
Biere A., 2002, ELECTRON NOTES THEOR, V66, P160, DOI DOI 10.1016/S1571-0661(04)80410-9