Skip to Main content Skip to Navigation
Conference papers

Component Reuse in B Using ACL2

Yann Zimmermann 1, 2 Diana Toma 3
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 KEESDA SA - Knowledge Environment for Eelectronic Systems Design Automation SA
3 TIMA - Techniques de l'Informatique et de la Microélectronique pour l'Architecture des systèmes intégrés
Abstract : We present a new methodology that permits to reuse an existing hardware component that has not been developed within the B framework while maintaining a correct design flow. It consists of writing a specification of the component in B and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the B specification into ACL2.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
https://hal.inria.fr/inria-00000755
Contributor : Yann Zimmermann <>
Submitted on : Wednesday, November 16, 2005 - 2:44:34 PM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM
Long-term archiving on: : Friday, April 2, 2010 - 7:28:24 PM

File

Vignette du document
34550281.pdf

Identifiers

Collections

INRIA | TIMA | CNRS | LORIA | UNIV-LORRAINE | UGA

Citation

Yann Zimmermann, Diana Toma. Component Reuse in B Using ACL2. ZB Formal Specification and Development in Z and B - 4th International Conference of B and Z Users - ZB 2005, Apr 2005, University of Surrey, Guildford, UK, pp.280-299, ⟨10.1007/b135596⟩. ⟨inria-00000755⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

1354

Files downloads

1802

 

Contact                    Legal Notice                    Personal Data