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 条

[21] Case Study: SoC Performance Verification and Static Verification of RTL Parameters
Ghosh, Prokash
Srivastava, Rohit
2019 20TH INTERNATIONAL WORKSHOP ON MICROPROCESSOR/SOC TEST, SECURITY AND VERIFICATION (MTV 2019), 2019, : 65 - 72
[22] RTL emulation: The next leap in system verification
Sawant, S
Giordano, P
33RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 1996, 1996, : 233 - 235
[23] Verification methods for VHDL RTL-subroutines
Ecker, W
JOURNAL OF SYSTEMS ARCHITECTURE, 1996, 42 (02) : 117 - 128
[24] Semantics of RTL and validation of synthesized RTL designs using formal verification in reconfigurable computing systems
Vinh, PC
Bowen, JP
12TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2005, : 247 - 254
[25] A methodology to take credit for high-level verification during RTL verification
Frederic Doucet
Robert Kurshan
Formal Methods in System Design, 2017, 51 : 395 - 418
[26] A methodology to take credit for high-level verification during RTL verification
Doucet, Frederic
Kurshan, Robert
FORMAL METHODS IN SYSTEM DESIGN, 2017, 51 (02) : 395 - 418
[27] Common reusable verification environment for BCA and RTL models
Falconeri, G
Naifer, W
Romdhane, N
DESIGNERS' FORUM: DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, 2005, : 272 - 277
[28] Design for verification in system-level models and RTL
Mathur, Anmol
Krishnaswamy, Venkat
2007 44TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2007, : 193 - 198
[29] Lattice-based SMT for Program Verification
Even-Mendoza, Karine
Hyvarinen, Antti E. J.
Chockler, Hana
Sharygina, Natasha
17TH ACM-IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2019,
[30] SMT-Based Verification of Parameterized Systems
Gurfinkel, Arie
Shoham, Sharon
Meshman, Yuri
FSE'16: PROCEEDINGS OF THE 2016 24TH ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON FOUNDATIONS OF SOFTWARE ENGINEERING, 2016, : 338 - 348

← 1 2 3 4 5 →