An analysis of ATPG and SAT algorithms for formal verification

被引：14

作者：

Parthasarathy, G ^{[1
]}

Huang, CY ^{[1
]}

Cheng, KT ^{[1
]}

机构：

[1] Univ Calif Santa Barbara, Santa Barbara, CA 93106 USA

来源：

SIXTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS | 2001年

关键词：

D O I：

10.1109/HLDVT.2001.972826

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We analyze the performance of satisfiability (SAT) and Automatic Test Pattern Generation (ATPG) algorithms in two state-of-the-art solvers. The goal is to best understand how features of each solver are suited for hardware verification. For ATPG, we analyze depth-first and breadth-first decision orderings and effects of two weighting heuristics in the decision ordering, and also study the effect of randomization of decisions. Features of ATPG and SAT that affect their robustness and flexibility on real circuits are studied, and the two solvers are compared on 24 industrial circuits. We further analyze the results to identify the strengths and shortcomings of each solver. This will enable incorporation of features from each solver in order to optimize performance, since they both operate on the same principles.

引用

页码：177 / 182

页数：6

共 50 条

[1] SAT and ATPG: Boolean engines for formal hardware verification
Biere, A
Kunz, W
[J]. IEEE/ACM INTERNATIONAL CONFERENCE ON CAD-02, DIGEST OF TECHNICAL PAPERS, 2002, : 782 - 785
[2] Formal verification using bounded model checking: SAT versus sequential ATPG engines
Saab, DG
Abraham, JA
Vedula, VM
[J]. 16TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 2003, : 243 - 248
[3] Neural Fault Analysis for SAT-based ATPG
Huang, Junhua
Zhen, Hui-Ling
Wang, Naixing
Mao, Hui
Yuan, Mingxuan
Huang, Yu
[J]. 2022 IEEE INTERNATIONAL TEST CONFERENCE (ITC), 2022, : 36 - 45
[4] Formal verification of the UltraSPARC(TM) family of processors via ATPG methods
Levitt, ME
[J]. INTERNATIONAL TEST CONFERENCE 1996, PROCEEDINGS, 1996, : 849 - 856
[5] Formal Verification of Financial Algorithms
Passmore, Grant Olney
Ignatovich, Denis
[J]. AUTOMATED DEDUCTION - CADE 26, 2017, 10395 : 26 - 41
[6] Verilog transformation for an RTL SAT solver in formal verification
Yang, Xiaoqing
Bian, Jinian
Deng, Shujun
Zhao, Yanni
[J]. 2007 INTERNATIONAL CONFERENCE ON COMMUNICATIONS, CIRCUITS AND SYSTEMS PROCEEDINGS, VOLS 1 AND 2: VOL 1: COMMUNICATION THEORY AND SYSTEMS; VOL 2: SIGNAL PROCESSING, COMPUTATIONAL INTELLIGENCE, CIRCUITS AND SYSTEMS, 2007, : 1339 - +
[7] Eiffel: Extending Formal Verification of Distributed Algorithms to Utility Analysis
Baloochestani, Arian
Jehl, Leander
[J]. 2023 5TH CONFERENCE ON BLOCKCHAIN RESEARCH & APPLICATIONS FOR INNOVATIVE NETWORKS AND SERVICES, BRAINS, 2023,
[8] Incremental SAT instance generation for SAT-based ATPG
Tille, Daniel
Drechsler, Rolf
[J]. 2008 IEEE WORKSHOP ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS, PROCEEDINGS, 2008, : 68 - 73
[9] Formal verification of iterative algorithms in microprocessors
Aagaard, MD
Jones, RB
Kaivola, R
Kohatsu, KR
Seger, CJH
[J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 201 - 206
[10] Formal verification of conflict detection algorithms
César Muñoz
Víctor Carreño
Gilles Dowek
Ricky Butler
[J]. International Journal on Software Tools for Technology Transfer, 2003, 4 (3) : 371 - 380

← 1 2 3 4 5 →