Component Reuse in B Using ACL2

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.

• Type: Conference
• Year: 2005
• Where: ZUM
• Authors: Yann Zimmermann, Diana Toma
• Keywords: ACL2 System, Correct Design, Formal Methods, Hardware Component, ZUM 2005