Article

Free access

Verification and Synthesis of Counters Based on Symbolic Techniques

Authors:

G. Cabodi,

P. Camurati,

L. Lavagno,

S. QuerAuthors Info & Claims

EDTC '97: Proceedings of the 1997 European conference on Design and Test

Page 176

Published: 17 March 1997 Publication History

PDF eReader

Abstract

Symbolic Techniques have undergone major improvements but extending their applicability to new fields is still a key issue. A great limitation on standard Symbolic Traversals is represented by Finite State Machines with a very high sequential depth. A typical example of this behaviour are counters. On the other hand systems containing counters, e.g. embedded systems, are of great practical importance in several fields. Iterative squaring can produce solutions with a logarithmic execution time with respect to the sequential depth but a few drawbacks usually limit its application. We successfully tailored iterative squaring to allow its application for symbolic verification and synthesis of circuits containing counters. Experiments on large and complex home-made and industrials circuits containing counters show the feasibility of the approach.

References

[1]

{1} M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, A. Sangiovanni-Vincentelli, "Hard-ware/software co-design of embedded systems," IEEE Micro, August 1994, Vol. 3. 4(4), pp. 26-36.

Digital Library

Google Scholar

[2]

{2} S. Campos, E. Clarke, W. Marrero, M. Minea, "Verus: a tool for quantitative analysis of finite-state real-time systems," in Proc. ACM SIGPLAN'95 Workshop on Languages, Compilers, and Tools for Real-Time Systems , June 1995.

Digital Library

Google Scholar

[3]

{3} R. Hojati, H. Touati, R.P. Kurshan, R.K. Brayton, "Efficient omega-regular language containment," in Proc. CAV'94, June 1994.

Digital Library

Google Scholar

[4]

{4} E. Macii, B. Plessier, F. Somenzi, "Verification of systems containing counters, in Proc. IEEE ICCAD'92, November 1992, pp. 179-182.

Digital Library

Google Scholar

[5]

{5} J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, "Sequential Circuit Verification Using Symbolic Model Checking," in Proc. ACM/IEEE DAC'90, June 1990, pp. 46-51.

Digital Library

Google Scholar

[6]

{6} Y. Matsunaga, P.C. McGeer, R.K. Brayton, "On computing the Transitive Closure of a State Transition Relation," in Proc. ACM/IEEE DAC'93, June 1993, pp. 260-265.

Digital Library

Google Scholar

[7]

{7} J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Transactions on CAD, Vol. 13, No. 4, April 1994, pp. 401-424.

Digital Library

Google Scholar

[8]

{8} C. Pixley, "A computational theory and implementation of sequential hardware equivalence," in AMS/DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 293- 320.

Crossref

Google Scholar

[9]

{9} C. Pixley, S.-W. Jeong, G.D. Hachtel, "Exact Calculation of Synchronization Sequences Based on Binary Decision Diagrams," in Proc. ACM/IEEE DAC'92, June 1992, pp. 620-623.

Digital Library

Google Scholar

[10]

{10} F. Somenzi, "CUDD: CU Decision Diagram Package - Release 1.0.4," Technical Report, Dept. of Electrical and Computer Engineering, University of California, Boulder, November 1995.

Google Scholar

[11]

{11} M68HC11 Reference Manual, Motorola inc., 1991.

Google Scholar

[12]

{12} G. Cabodi, P. Camurati, S. Quer, "Improved Reachability Analysis of Large Finite State Machine," in Proc. IEEE/ACM ICCAD'96, November 1996, pp. 354-360.

Digital Library

Google Scholar

Cited By

View all

Logothetis GSchneider KBolsens I(2000)Abstraction from countersProceedings of the conference on Design, automation and test in Europe10.1145/343647.343828(486-493)Online publication date: 1-Jan-2000
https://dl.acm.org/doi/10.1145/343647.343828
Cabodi GCamurati PPasserone CQuer S(1999)Computing timed transition relations for sequential cycle-based simulationProceedings of the conference on Design, automation and test in Europe10.1145/307418.307427(4-es)Online publication date: 1-Jan-1999
https://dl.acm.org/doi/10.1145/307418.307427
Cabodi GCamurati PLavagno LQuer SYoffa EDe Micheli GRabaey J(1997)Disjunctive partitioning and partial iterative squaringProceedings of the 34th annual Design Automation Conference10.1145/266021.266355(728-733)Online publication date: 13-Jun-1997
https://dl.acm.org/doi/10.1145/266021.266355

Recommendations

Template-based program verification and program synthesis

Program verification is the task of automatically generating proofs for a program's compliance with a given specification. Program synthesis is the task of automatically generating a program that meets a given specification. Both program verification ...
Synthesis and optimization of multiple-valued combinational and sequential reversible circuits with don't cares

In this paper, a synthesis method for combinational multiple-valued reversible logic (MVRL) circuits is proposed. This algorithm can use the don't care values in the synthesis process to obtain the optimal circuit with respect to quantum cost. The ...
Synthesis of skewed logic circuits

Skewed logic circuits belong to a noise-tolerant high-performance static circuit family. Skewed logic circuits can achieve performance comparable to that of Domino logic circuits but with much lower power consumption. Two factors contribute to the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

EDTC '97: Proceedings of the 1997 European conference on Design and Test

March 1997

596 pages

ISBN:0818677864

Publisher

IEEE Computer Society

United States

Publication History

Published: 17 March 1997

Check for updates

Author Tags

Qualifiers

Article

Conference

EDTC96

Sponsor:

SIGDA

EDTC96: European Design and Test Conference

March 17 - 20, 1997

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
88
Total Downloads

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

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Logothetis GSchneider KBolsens I(2000)Abstraction from countersProceedings of the conference on Design, automation and test in Europe10.1145/343647.343828(486-493)Online publication date: 1-Jan-2000
https://dl.acm.org/doi/10.1145/343647.343828
Cabodi GCamurati PPasserone CQuer S(1999)Computing timed transition relations for sequential cycle-based simulationProceedings of the conference on Design, automation and test in Europe10.1145/307418.307427(4-es)Online publication date: 1-Jan-1999
https://dl.acm.org/doi/10.1145/307418.307427
Cabodi GCamurati PLavagno LQuer SYoffa EDe Micheli GRabaey J(1997)Disjunctive partitioning and partial iterative squaringProceedings of the 34th annual Design Automation Conference10.1145/266021.266355(728-733)Online publication date: 13-Jun-1997
https://dl.acm.org/doi/10.1145/266021.266355

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Template-based program verification and program synthesis

Synthesis and optimization of multiple-valued combinational and sequential reversible circuits with don't cares

Synthesis of skewed logic circuits