Parametric circuit representation using inductive boolean functions

Aarti Gupta, Allan L. Fisher

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

16 Scopus citations

Abstract

We have developed a methodology based on symbolic manipulation of inductive Boolean functions (IBFs) for formal verification of inductively-defined hardware. This methodology combines the techniques of reasoning by induction and symbolic tautologychecking in an automated and potentially efficient way. In this paper, we describe a component of this methodology that regards various mechanisms used to represent inductivelydefined circuits in the form of IBFs. The focus is on general parameterization issues, such as multiple parameter functions, multiple output functions, interaction of different parameters for supporting compositions etc. These mechanisms, which may be useful in other applications involving parametric circuit descriptions, are illustrated through practical circuit examples along with preliminary results. We also describe an application of our formal verification methodology, where a proof by induction is performed by automatic symbolic manipulation of parametric circuit representations.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 5th International Conference, CAV 1993, Proceedings
EditorsCostas Courcoubetis
PublisherSpringer Verlag
Pages15-28
Number of pages14
ISBN (Print)9783540569220
DOIs
StatePublished - 1993
Externally publishedYes
Event5th International Conference on Computer Aided Verification, CAV 1993 - Elounda, Greece
Duration: Jun 28 1993Jul 1 1993

Publication series

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

Other

Other5th International Conference on Computer Aided Verification, CAV 1993
CountryGreece
CityElounda
Period6/28/937/1/93

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Parametric circuit representation using inductive boolean functions'. Together they form a unique fingerprint.

  • Cite this

    Gupta, A., & Fisher, A. L. (1993). Parametric circuit representation using inductive boolean functions. In C. Courcoubetis (Ed.), Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings (pp. 15-28). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 697 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_3