Comparision Between LPSAT and SMT for RTL Verification

被引：0

作者：

Kunapareddy, Sarvani ^{[1
]}

Turaga, Sriraj Dheeraj ^{[1
]}

Sajjan, Solomon Surya Tej Mano ^{[1
]}

机构：

[1] Univ Utah, Elect & Comp Engn, Salt Lake City, UT USA

来源：

2015 INTERNATIONAL CONFERENCED ON CIRCUITS, POWER AND COMPUTING TECHNOLOGIES (ICCPCT-2015) | 2015年

关键词：

LPSAT; CNF; SMT; RTL Verification; Satisfiability; Bit nibbling;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The complexity of the circuits today are making it impossible to verify those using traditional CNF-based and BDD-based SAT algorithms. They take unacceptably long run times. Circuits are so complex that bit blasting them is infeasible. A better solution to this problem is to solve SAT at word level. LP solvers and SMT solvers are more efficient to tackle such high complexity at word level. The world today has moved to SMT solvers in verification of world level RTL. Our study aims at the comparison between LP solvers and SMT solvers in verification of RTL. This comparison is made on the basis of complexity, number of iterations and run time. SMT is found to complete verification check in less number of iterations and time. It also has less code complexity and is easy to understand.

引用

页数：5

共 50 条

[1] Constraints decomposition for RTL verification by SMT
Zhao, Yanni
Bian, Jinian
Deng, Shujun
Jisuanji Fuzhu Sheji Yu Tuxingxue Xuebao/Journal of Computer-Aided Design and Computer Graphics, 2010, 22 (02): : 234 - 239
[2] LPSAT: A unified approach to RTL satisfiability
Zeng, ZH
Kalla, P
Ciesielski, M
DESIGN, AUTOMATION AND TEST IN EUROPE, CONFERENCE AND EXHIBITION 2001, PROCEEDINGS, 2001, : 398 - 402
[3] Formal Probabilistic Timing Verification in RTL
Kumar, Jayanand Asok
Vasudevan, Shobha
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2013, 32 (05) : 788 - 801
[4] Reducing Verification Overhead with RTL slicing
Ou, Jen-Chieh
Saab, Daniel G.
Qiang, Qiang
Abraham, Jacob A.
GLSVLSI'07: PROCEEDINGS OF THE 2007 ACM GREAT LAKES SYMPOSIUM ON VLSI, 2007, : 399 - 404
[5] Use of Structural Tests in RTL Verification
Hobeika, Christelle
Thibeault, Claude
Boland, Jean-Francois
2008 1ST MICROSYSTEMS AND NANOELECTRONICS RESEARCH CONFERENCE, 2008, : 133 - 136
[6] RTL formal verification of embedded processors
Bavonparadon, P
Chongstitvatana, P
IEEE ICIT' 02: 2002 IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL TECHNOLOGY, VOLS I AND II, PROCEEDINGS, 2002, : 667 - 672
[7] An automatic circuit extractor for RTL verification
Li, T
Guo, Y
Li, SK
ATS 2003: 12TH ASIAN TEST SYMPOSIUM, PROCEEDINGS, 2003, : 154 - 160
[8] Failure Triage in RTL Regression Verification
Poulos, Zissis
Veneris, Andreas
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (09) : 1893 - 1906
[9] Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
Daly, Ross
Donovick, Caleb
Melchert, Jackson
Setaluri, Rajsekhar
Bullock, Nestan Tsiskaridze
Raina, Priyanka
Barrett, Clark
Hanrahan, Pat
2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 : 139 - 150
[10] Workflow Nets Verification: SMT or CLP?
Bride, Hadrien
Kouchnarenko, Olga
Peureux, Fabien
Voiron, Guillaume
CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION, 2016, 9933 : 39 - 55

← 1 2 3 4 5 →