HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Circuit Design by Refinement in EventB

Stefan Hallerstede Yann Zimmermann 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present the design of a synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear system in eventB, a synthesizable pipelined implementation is developed. Formal refinement is used to prove each development step correct. Thus, at the end we achieve a fully proven hardware description and circuit, provided the circuit is correct.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:14:39 AM
Last modification on : Friday, February 4, 2022 - 3:23:18 AM


  • HAL Id : inria-00100145, version 1



Stefan Hallerstede, Yann Zimmermann. Circuit Design by Refinement in EventB. Forum on Specification and Design Languages - FDL'04, Pierre Boulet, 2004, Lille, France, 13 p. ⟨inria-00100145⟩



Record views