BDD based procedures for a theory of equality with uninterpreted functions

Anuj Goel*, Khurram Sajid, Hai Zhou, Adnan Aziz, Vigyan Singhal

*Corresponding author for this work

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

47 Scopus citations

Abstract

The logic of equality with uninterpreted functions has been proposed for verifying abstract hardware designs. The ability to perform fast satisfiability checking over this logic is imperative for this verification paradigin to be successful. We present symbolic methods for satisfiability checking for this logic. The first procedure is based on restricting analysis to finite instantiations of the design. The second procedure directly reasons about equality by introducing Boolean-valued indicator variables for equality. Theoretical and experimental evidence shows the superiority of the second approach.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 10th International Conference, CAV'98, Proceedings
Pages244-255
Number of pages12
StatePublished - Dec 1 1998
Event10th International Conference on Computer-Aided Verification, CAV'98 - Vancouver, BC, Canada
Duration: Jun 28 1998Jul 2 1998

Publication series

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

Other

Other10th International Conference on Computer-Aided Verification, CAV'98
CountryCanada
CityVancouver, BC
Period6/28/987/2/98

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'BDD based procedures for a theory of equality with uninterpreted functions'. Together they form a unique fingerprint.

Cite this