SAT-based verification methods and applications in hardware

Aarti Gupta, Malay K. Ganai, Chao Wang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Scopus citations

Abstract

Verification methods based on Boolean Satisfiability (SAT) have emerged as a promising alternative to HDD-based symbolic model checking methods. This paper provides a tutorial on various SAT-based verification methods we have developed for verifying large hardware designs. We focus separately on methods for finding bugs and for finding proofs for correctness properties, along with highlighting the many common themes that benefit these methods. We also describe practical experiences with these methods implemented in our verification platform called VeriSol (formerly DiVer), which has been used successfully in industry practice.

Original languageEnglish (US)
Title of host publicationFormal Methods for Hardware Verification - 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006
PublisherSpringer Verlag
Pages108-143
Number of pages36
ISBN (Print)3540343040, 9783540343042
DOIs
StatePublished - 2006
Event6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006 - Bertinoro, Italy
Duration: May 22 2006May 27 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3965 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006
Country/TerritoryItaly
CityBertinoro
Period5/22/065/27/06

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'SAT-based verification methods and applications in hardware'. Together they form a unique fingerprint.

Cite this