More Web Proxy on the site http://driver.im/

article

An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator

Authors:

Muhammad Osama,

Aziza I. Hussein,

Hanafy MahmoudAuthors Info & Claims

Journal of Electronic Testing: Theory and Applications, Volume 34, Issue 5

Pages 511 - 527

https://doi.org/10.1007/s10836-018-5747-4

Published: 01 October 2018 Publication History

Abstract

This paper presents a novel framework comprises of a Propositional Satisfiability (SAT) encoder and solver. The framework responsible for generating and proving a simplified SAT-based formula of digital circuits for Automatic Test Pattern Generation (ATPG) proposes. The parallel algorithms introduced in this work are aimed at both combinational and sequential circuits and optimized on NVIDIA General-Purpose Graphics Processing Unit (GPGPU) paradigm. The SAT encoder presents an efficient method to apply the Boolean Constraint Propagation (BCP) on-the-fly while the generation is running on the GPU. The simplified formula is further proved for satisfiability using an improved parallel solver on GPU. The proposed encoder executes 93 times faster compared to the sequential counterpart. The test generation algorithm using the GPU-accelerated framework delivers about 5.86 speedup on an average compared to the state-of-the-art Lingeling solver. Moreover, the SAT encoder reduced the run time for fault detection by 6.53 and 11.42% on an average when applied to the proposed and the conventional CUD@SAT solvers, respectively, offering promising related work for the future research.

References

[1]

Ali LG, Hussein AI and Ali HM (2016) "Parallelization of unit propagation algorithm for SAT-based ATPG of digital circuits," in Proc. 2016 28th international conference on microelectronics (ICM), pp. 184---188

[2]

Arora R and Hsiao MS (2003) "Enhancing sat-based equivalence checking with static logic implications," in Proc Eighth IEEE International High-Level Design Validation and Test Workshop, pp. 63---68: IEEE

Digital Library

[3]

Balcarek J, Fiser P, Schmidt J (2013) Techniques for SAT-based constrained test pattern generation. Microprocess Microsyst 37(2):185---195

Digital Library

[4]

Biere A (2015) "Lingeling SAT Solver," SAT Competitions 2014---2016, no. January

[5]

Bjesse P, Leonard T and Mokkedem A (2001) Finding bugs in an alpha microprocessor using satisfiability solvers, in Computer Aided Verification, pp. 454---464: Springer

Digital Library

[6]

Brglez F (1985) "a neutral netlist of 10 combinational benchmark circuits and a target translation in FORTRAN," in ISCAS-85

[7]

Brglez F, Bryan D, and Ko?miński K (1989) "Combinational profiles of sequential benchmark circuits," in Proc IEEE International Symposium on Circuits and Systems, pp. 1929---1934: IEEE

[8]

Brglez F, Bryan D, and Ko?miński K ISCAS 85---89 Circuits Benchmark Suite {Online}. Available: http://www.cbl.ncsu.edu:16080/benchmarks/

[9]

Cai X, Wohl P, Waicukauski JA, and Notiyath P (2010) "Highly efficient parallel ATPG based on shared memory," in Proc. 2010 IEEE international test conference, pp. 1---7

[10]

Chakradhar ST, Agrawal VD, Rothweiler SG (1993) A transitive closure algorithm for test generation. IEEE Trans Comput-Aided Des Integrated Circ Systs 12(7):1015---1028

Digital Library

[11]

Corno F, Reorda MS, Squillero G (2000) RT-level ITC'99 benchmarks and first ATPG results. 17(3):44---53

Digital Library

[12]

Corno F, Reorda MS, and Squillero G Collection of Digital Design Benchmarks - ITC'99 Test Suite {Online}. Available: http://ddd.fit.cvut.cz/prj/Benchmarks/

[13]

Czutro A, Polian I, Lewis M, Engelke P, Reddy SM, and Becker B (2009) "Tiguan: Thread-parallel integrated test pattern generator utilizing satisfiability analysis," in Proc. 22nd International Conference on VLSI Design, pp. 227---232: IEEE

Digital Library

[14]

Dal Palù A, Dovier A, Formisano A, Pontelli E (2015) CUD@SAT: SAT solving on GPUs. J Exp Theor Artif Intelligence 27(3):293---316

[15]

Dechter R (2003) Constraint processing. Morgan Kaufmann Publishers Inc, p. 450

Digital Library

[16]

Djemal R, Dhouib MA, Dellacherie S, Tourki R (2005) A novel formal verification approach for RTL hardware IP cores. Comput Standards Interfaces 27(6):637---651

Digital Library

[17]

Eén N and Biere A (2005) "Effective preprocessing in SAT through variable and clause elimination," in Proc Theory and Applications of Satisfiability Testing, pp. 61---75: Springer

Digital Library

[18]

Eén N and Sörensson N (2003) "An extensible SAT-solver," in Proc. International conference on theory and applications of satisfiability testing, pp. 502---518: Springer

[19]

Fujiwara H (1985) "Fan: a fanout-oriented test pattern generation algorithm," in Proc. IEEE international symposium on circuits and systems, pp. 671---674

[20]

Goel P (1995) "An implicit enumeration algorithm to generate tests for combinational logic circuits," in Fault-Tolerant Computing, p. 337

[21]

Goldberg E, Novikov Y (2007) BerkMin: a fast and robust SAT-solver. Discret Appl Math 155(12):1549---1561

Digital Library

[22]

E. Goldberg, M. Prasad, and R. Brayton (2001) Using SAT for combinational equivalence checking, in Proc of the conference on Design, automation and test in Europe, pp. 114---121: IEEE Press

Digital Library

[23]

Gupta A, Ganai MK, Wang C (2006) SAT-based verification methods and applications in hardware verification. In: Bernardo M, Cimatti A (eds) Formal methods for hardware verification: 6th international school on formal methods for the Design of Computer, communication, and software systems, SFM 2006, Bertinoro, Italy, may 22---27, 2006, Advanced Lectures. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 108---143

Digital Library

[24]

Ivană?ić F, Yang Z, Ganai MK, Gupta A, Ashar P (2008) Efficient SAT-based bounded model checking for software verification. Theor Comput Sci 404(3):256---274

Digital Library

[25]

Järvisalo M, Niemelä I (2008) The effect of structural branching on the efficiency of clause learning SAT solving: an experimental study. J Algoritm 63(1):90---113

Digital Library

[26]

Kemper S (2012) SAT-based verification for timed component connectors. Sci Comput Program 77(7---8):779---798

Digital Library

[27]

Larrabee T (1992) Test pattern generation using Boolean satisfiability. Comput-Aided Des Integrated Circuits Syst, IEEE Trans on 11(1):4---15

Digital Library

[28]

Lewis M, Schubert T, and Becker B (2007) "Multithreaded SAT solving," in Proc Design Automation Conference. ASP-DAC'07. Asia and South Pacific, pp. 926---931: IEEE

Digital Library

[29]

Liao KY, Chang CY, Li JCM (2011) A parallel test pattern generation algorithm to meet multiple quality objectives. IEEE Trans Comput-Aided Des Integrated Circ Syst 30(11):1767---1772

Digital Library

[30]

Liao KY, Sheng-Chang H, and Li JCM (2013) "GPU-based N-detect transition fault ATPG," in Proc. 2013 50th ACM/EDAC/IEEE design automation conference (DAC), pp. 1---8

Digital Library

[31]

Liffiton MH, Previti A, Malik A, Marques-Silva J (2016) Fast, flexible MUS enumeration. Constraints 21(2):223---250

Digital Library

[32]

Lingappan L, Jha NK (2007) Satisfiability-based automatic test program generation and design for testability for microprocessors, Very Large Scale Integration (VLSI) Systems. IEEE Trans on 15(5):518---530

Digital Library

[33]

Marques-Silva J and Glass T (1999) "Combinational equivalence checking using satisfiability and recursive learning," in Proc Design, Automation and Test in Europe Conference and Exhibition, pp. 145---149: IEEE

Digital Library

[34]

Marques-Silva JP, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506---521

Digital Library

[35]

Micikevicius P (2012) "GPU performance analysis and optimization," in GPU Technology Conference (GTC'12), NVIDIA, vol. 84. Available: http://developer.download.nvidia.com/GTC/PDF/GTC2012/PresentationPDF/S0514-GTC2012-GPU-Performance-Analysis.pdf

[36]

Morgado A, Liffiton M, Marques-Silva J (2013) MaxSAT-based MCS enumeration. In: Biere A, Nahir A, Vos T (eds) Hardware and software: verification and testing: 8th international Haifa verification conference, HVC 2012, Haifa, Israel, November 6---8, 2012. Revised Selected Papers. Springer Berlin Heidelberg, Berlin, pp 86---101

Digital Library

[37]

Moskewicz MW, Madigan CF, Zhao Y, Zhang L, and Malik S (2001) "Chaff: Engineering an efficient SAT solver," in Proc. 38th annual Design Automation Conference, pp. 530---535: ACM

Digital Library

[38]

Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL (T). J ACM (JACM) 53(6):937---977

Digital Library

[39]

Noureddine MA, Zaraket FA (2016) Model checking software with first order logic specifications using AIG solvers. IEEE Trans Softw Eng 42(8):741---763

Digital Library

[40]

Novikov Y (2003) "Local search for boolean relations on the basis of unit propagation," in Proc. of the conference on Design, Automation and Test in Europe-Volume 1, p. 10810: IEEE Computer Society

Digital Library

[41]

NVIDIA (2015) CUDA C Programming Guide. Available: http://docs.nvidia.com/cuda/cuda-c-programming-guide/

[42]

Roth JP, Bouricius WG, Schneider PR (1967) Programmed algorithms to compute tests to detect and distinguish between failures in logic circuits. IEEE Trans Electron Comput EC-16(5):567---580

[43]

Safarpour S, Mangassarian H, Veneris A, Liffiton MH and Sakallah K (2007) "Improved design debugging using maximum satisfiability," in Proc Formal Methods in Computer Aided Design, FMCAD'07, pp. 13---19: IEEE

Digital Library

[44]

Shi J, Fey G, Drechsler R, Glowatz A, Hapke F and Schlöffel J (2005) "PASSAT: efficient SAT-based test pattern generation for industrial circuits," in Proc IEEE Computer Society Annual Symposium on VLSI, pp. 212---217: IEEE

Digital Library

[45]

Smith A, Veneris A, Ali MF, Viglas A (2005) Fault diagnosis and logic debugging using Boolean satisfiability. Comput-Aided Des Integrated Circ Syst, IEEE Trans on 24(10):1606---1621

Digital Library

[46]

Sohanghpurwala AA, Hassan MW and Athanas P "Hardware accelerated SAT solvers--a survey," Journal of Parallel and Distributed ComputingIEEE Des Test Comput

[47]

Wu B, Zhao Z, Zhang EZ, Jiang Y, Shen X (2013) Complexity analysis and algorithm design for reorganizing data to minimize non-coalesced memory accesses on gpu. ACM SIGPLAN Not 48(8):57---68

Digital Library

[48]

Xie H and Luo J (2016) "An algorithm to compute minimal Unsatisfiable subsets for a decidable fragment of first-order formulas," in Proc. 2016 IEEE 28th international conference on tools with artificial intelligence (ICTAI), pp. 444---451

[49]

Youness H, Ibraheim A, Moness M and Osama M (2015) "An efficient implementation of ant colony optimization on GPU for the satisfiability problem," in Proc 2015 23rd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 230---235: IEEE

Digital Library

[50]

Zhang H and Stickel ME (1996) "An efficient algorithm for unit propagation," in Proc. of the Fourth International Symposium on Artificial Intelligence and Mathematics (AI-MATH'96). Florida, USA: Citeseer

Cited By

Osama MWijs ABiere A(2024)Certified SAT solving with GPU accelerated inprocessingFormal Methods in System Design10.1007/s10703-023-00432-z62:1-3(79-118)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10703-023-00432-z
Osama MWijs A(2024)Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model CheckingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_2(23-43)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_2
van Eerd JGroote JHijma PMartens JOsama MWijs A(2023)Innermost many-sorted term rewriting on GPUsScience of Computer Programming10.1016/j.scico.2022.102910225:COnline publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1016/j.scico.2022.102910
Show More Cited By

An Efficient SAT-Based Test Generation Algorithm with GPU Accelerator
1. Hardware

Recommendations

Boosting CUDA Applications with CPU---GPU Hybrid Computing

This paper presents a cooperative heterogeneous computing framework which enables the efficient utilization of available computing resources of host CPU cores for CUDA kernels, which are designed to run only on GPU. The proposed system exploits at ...
Pervasive massively multithreaded GPU processors
CF '09: Proceedings of the 6th ACM conference on Computing frontiers

This talk presents an overview of NVIDIA's SIMT architecture and some brief insights on how some CUDA programming paradigms map onto it. A brief history of SIMT is provided to explain how NVIDIA ended up implementing a unified SIMT processor core in its ...
Constructing a Bioinformatics Platform with Web and Mobile Services Based on NVIDIA Jetson TK1

Current high-end graphics processing units abbreviate to GPUs, such as NVIDIA Tesla, Fermi, Kepler series cards which contain up to thousand cores per-chip, are widely used in the high performance computing fields. These GPU cards called desktop GPUs ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Electronic Testing: Theory and Applications

Journal of Electronic Testing: Theory and Applications Volume 34, Issue 5

October 2018

104 pages

ISSN:0923-8174

Issue’s Table of Contents

Copyright © Copyright © 2018 Springer Science+Business Media, LLC, part of Springer Nature.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 October 2018

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Osama MWijs ABiere A(2024)Certified SAT solving with GPU accelerated inprocessingFormal Methods in System Design10.1007/s10703-023-00432-z62:1-3(79-118)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10703-023-00432-z
Osama MWijs A(2024)Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model CheckingTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_2(23-43)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57249-4_2
van Eerd JGroote JHijma PMartens JOsama MWijs A(2023)Innermost many-sorted term rewriting on GPUsScience of Computer Programming10.1016/j.scico.2022.102910225:COnline publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1016/j.scico.2022.102910
Wijs AOsama M(2023)GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with DataModel Checking Software10.1007/978-3-031-32157-3_11(188-197)Online publication date: 26-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-32157-3_11
Moness MGaber LHussein AAli H(2022)Automated Design Error Debugging of Digital VLSI CircuitsJournal of Electronic Testing: Theory and Applications10.1007/s10836-022-06020-z38:4(395-417)Online publication date: 1-Aug-2022
https://dl.acm.org/doi/10.1007/s10836-022-06020-z
Osama MWijs A(2021)GPU Acceleration of Bounded Model Checking with ParaFROSTComputer Aided Verification10.1007/978-3-030-81688-9_21(447-460)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81688-9_21
Osama MWijs A(2019)Parallel SAT Simplification on GPU ArchitecturesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-17462-0_2(21-40)Online publication date: 6-Apr-2019
https://dl.acm.org/doi/10.1007/978-3-030-17462-0_2

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents