Parametric circuit representation using inductive boolean functions

Aarti Gupta; Allan L. Fisher

doi:10.1007/3-540-56922-7_3

Parametric circuit representation using inductive boolean functions

Aarti Gupta, Allan L. Fisher

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

17 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 language	English (US)
Title of host publication	Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings
Editors	Costas Courcoubetis
Publisher	Springer Verlag
Pages	15-28
Number of pages	14
ISBN (Print)	9783540569220
DOIs	https://doi.org/10.1007/3-540-56922-7_3
State	Published - 1993
Externally published	Yes
Event	5th International Conference on Computer Aided Verification, CAV 1993 - Elounda, Greece Duration: Jun 28 1993 → Jul 1 1993

Publication series

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

Other

Other	5th International Conference on Computer Aided Verification, CAV 1993
Country/Territory	Greece
City	Elounda
Period	6/28/93 → 7/1/93

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-56922-7_3

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

Gupta, Aarti ; Fisher, Allan L. / Parametric circuit representation using inductive boolean functions. Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings. editor / Costas Courcoubetis. Springer Verlag, 1993. pp. 15-28 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b06c973eb50e429eb331ecf8391919e3,

title = "Parametric circuit representation using inductive boolean functions",

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.",

author = "Aarti Gupta and Fisher, {Allan L.}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1993.; 5th International Conference on Computer Aided Verification, CAV 1993 ; Conference date: 28-06-1993 Through 01-07-1993",

year = "1993",

doi = "10.1007/3-540-56922-7_3",

language = "English (US)",

isbn = "9783540569220",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "15--28",

editor = "Costas Courcoubetis",

booktitle = "Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings",

address = "Germany",

}

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

Parametric circuit representation using inductive boolean functions. / Gupta, Aarti; Fisher, Allan L.
Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings. ed. / Costas Courcoubetis. Springer Verlag, 1993. p. 15-28 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 697 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Parametric circuit representation using inductive boolean functions

AU - Gupta, Aarti

AU - Fisher, Allan L.

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1993.

PY - 1993

Y1 - 1993

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84931086116&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84931086116&partnerID=8YFLogxK

U2 - 10.1007/3-540-56922-7_3

DO - 10.1007/3-540-56922-7_3

M3 - Conference contribution

AN - SCOPUS:84931086116

SN - 9783540569220

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 15

EP - 28

BT - Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings

A2 - Courcoubetis, Costas

PB - Springer Verlag

T2 - 5th International Conference on Computer Aided Verification, CAV 1993

Y2 - 28 June 1993 through 1 July 1993

ER -

Gupta A, Fisher AL. Parametric circuit representation using inductive boolean functions. In Courcoubetis C, editor, Computer Aided Verification - 5th International Conference, CAV 1993, Proceedings. Springer Verlag. 1993. p. 15-28. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-56922-7_3

Parametric circuit representation using inductive boolean functions

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this