More Web Proxy on the site http://driver.im/

Article

SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS

Authors:

Mauricio Ayala-Rincón,

Thomas M. Sant'AnaAuthors Info & Claims

SBCCI '06: Proceedings of the 19th annual symposium on Integrated circuits and systems design

Pages 125 - 130

https://doi.org/10.1145/1150343.1150379

Published: 28 August 2006 Publication History

Abstract

Rewriting and Rewriting-Logic have been used in several applications, including specification, formal verification and construction of proof assistants. Previous works explored hardware specification and modeling using the rewriting-logic system ELA. Experiences proved this to be very effective, but certainly restricted as a tool for formal verification of the correctness of the given hardware specifications. Although simple, verification had to be done exhaustively and manually, which indicated the need of automating this process. We present SAEPTUM, a methodology and tool for the verification of rewrite specifications created in ELAN, via the translation to the proof assistant PVS and automatic generation of critical pair based correction criteria.

References

[1]

M. Archer, B. D. Vito, and C. Muñoz. Developing user strategies in PVS: A tutorial. In Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics STRATA'03, NASA/CP-2003-212448, 2003.

[2]

Arvind and X. Shen. Using term rewriting systems to design and verify processors. IEEE Micro Special Issue on "Modeling and Validation of Microprocessors", 19(3):36--46, 1999.

Digital Library

[3]

M. Ayala-Rincón, C. Llanos, R. P. Jacobi, and R. Hartenstein. Prototyping Time and Space Efficient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic. ACM Trans. on Design Automation of Electronic Systems, 11(2):231--251, 2006.

Digital Library

[4]

M. Ayala-Rincón, R. M. Neto, R. P. Jacobi, C. Llanos, and R. Hartenstein. Applying ELAN strategies in simulation processors over simple architectures. In 2nd Int.Workshop on Reduction Strategies in Rewriting And Programming, volume 70(6) of ENTCS, pages 127--141. Elsevier, 2002.

[5]

J. Becker and R. Hartenstein. Configware and morphware going mainstream. J. of Sys. Arch., 49:127--142, 2003.

Digital Library

[6]

H. K. P. Borovanskỳ, C. Kirchner and C. Ringeissen. Rewriting with strategies in elan: a functional semantics. Int. J. of Foundations of Computer Science, 12(1):69--95, March 2001.

[7]

S. Eker, J. Meseguer, and A. Sridharanarayanan. The Maude LTL model checker. In F. Gadducci and U. Montanari, editors, Fourth Workshop on Rewriting Logic and its Applications, WRLA '02, volume~71 of ENTCS. Elsevier, 2002.

[8]

J. C. Hoe and Arvind. Open-Centric Hardware Description and Synthesis. IEEE T. on CAD of Integrated Circuits and Systems, 23(9):1277--1288, 2004.

Digital Library

[9]

R. P. Jacobi, M. Ayala-Rincón, L. G. A. Carvalho, C. Llanos, and R. Hartenstein. Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming. Genetics and Mol. Research, 4(3):543--552, 2005.

[10]

D. Kapur and M. Subramaniam. Mechanizing Verification of Arithmetic Circuits: SRT Division. In Proc. 17th FSTTCS, volume 1346 of LNCS, pages 103--122. Springer, 1997.

Digital Library

[11]

D. Kapur and M. Subramaniam. Using an Induction Prover for Verifying Arithmetic Circuits. J. of Software Tools for Technology Transfer, 3(1):32--65, 2000.

[12]

H. Kirchner and P.-E. Moreau. Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative commutative theories. Journal of Functional Programming, 11(2):207--251, 2001.

Digital Library

[13]

M. P. M. Clavel. The ITP Tool's Manual. U. Complutense de Madrid, http://maude.sip.ucm.es/itp/, April 2005.

[14]

T. McCombs. MAUDE 2.0 Primer Version 1.0. Technical report, University of Illinois at Urbana-Champaign, 2003. Available: http://maude.cs.uiuc.edu/primer.

[15]

S. P. Miller and M. Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In Works. on Industrial-Strength Formal Specification Tech., pages 2--16. IEEE CS, 1995.

Digital Library

[16]

C. Morra, J. Becker, M. Ayala-Rincón, and R. Hartenstein. FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations. In 15th Int. Conf. on Field Programmable Logic and App., pages 25--30. IEEE CS, 2005.

[17]

C. Muñoz. Rapid prototyping in PVS. Report NIA No. 2003-03 and NASA/CR-2003-212418, NIA-NASA Langley, National Institute of Aerospace, Hampton, VA, May 2003.

[18]

J. M. N. Martí-Oliet and M. Palomino. Notes on Model Checking and Abstraction in Rewriting Logic. Technical report, U. of Illinois at Urbana-Champaign, 2003. Available: http://maude.cs.uiuc.edu/papers/.

[19]

S. Owre, J. M. Rushby, N. Shankar, and M. K. Srivas. A tutorial on using PVS for hardware verification. In Theorem Provers in Circuit Design (TPCD '94), volume 901 of LNCS, pages 258--279. Springer, 1994.

Digital Library

[20]

R. Hosabettu and G. Gopalakrishnan and M. Srivas. Formal verification of a complex pipelined processor. Formal Methods in System Design, 23:171--213, 2003.

Digital Library

[21]

N. Shankar. Using decision procedures with a higher-order logic. In Proc. of the 14th Int. Conf. on Theorem Proving in Higher Order Logics, volume 2152 of LNCS, pages 5--26, 2001.

Digital Library

[22]

X. Shen and Arvind. Design and verification of speculative processors. In Workshop on Formal Techniques for Hardware and Hardware-like Systems, Marstrand, Sweden, June 1998.

Cited By

Almeida ALlanos CArias-García JAyala-Rincón MDavid EOrdonez Mde Azevedo RKinget P(2014)Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVSProceedings of the 27th Symposium on Integrated Circuits and Systems Design10.1145/2660540.2660982(1-8)Online publication date: 1-Sep-2014
https://dl.acm.org/doi/10.1145/2660540.2660982
Galdino AAyala-Rincón M(2010)A Formalization of the Knuth---Bendix(---Huet) Critical Pair TheoremJournal of Automated Reasoning10.1007/s10817-010-9165-245:3(301-325)Online publication date: 1-Oct-2010
https://dl.acm.org/doi/10.1007/s10817-010-9165-2

Index Terms

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SBCCI '06: Proceedings of the 19th annual symposium on Integrated circuits and systems design

August 2006

248 pages

ISBN:1595934790

DOI:10.1145/1150343

General Chair:
Claudionor Coelho
Universidade de Minas Gerais, Brazil
,
Program Chairs:
Ricardo Jacobi
Universidade de Brasilia, Brazil
,
Juergen Becker
Universitaet Karlsruhe (TH), Germany

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 August 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SBCCI06

Sponsor:

SBCCI06: 19th Symposium on Integrated Circuits and System Design

August 28 - September 1, 2006

MG, Ouro Preto, Brazil

Acceptance Rates

Overall Acceptance Rate 133 of 347 submissions, 38%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
118
Total Downloads

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

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Almeida ALlanos CArias-García JAyala-Rincón MDavid EOrdonez Mde Azevedo RKinget P(2014)Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVSProceedings of the 27th Symposium on Integrated Circuits and Systems Design10.1145/2660540.2660982(1-8)Online publication date: 1-Sep-2014
https://dl.acm.org/doi/10.1145/2660540.2660982
Galdino AAyala-Rincón M(2010)A Formalization of the Knuth---Bendix(---Huet) Critical Pair TheoremJournal of Automated Reasoning10.1007/s10817-010-9165-245:3(301-325)Online publication date: 1-Oct-2010
https://dl.acm.org/doi/10.1007/s10817-010-9165-2

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents