Component Reuse in B Using ACL2

Yann Zimmermann (1, 2) , Diana Toma (3)

1 MOSEL - Proof-oriented development of computer-based systems
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

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.

Domaines: Logique en informatique [cs.LO]

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⟩