A Demonstration of Specifying and Synthesising Hardware using

Hardware development is complex and the cost of er-rors extremely high. The use of specification and ver-ification technologies is critical to managing the cor-rectness and complexity of the systems being devel-oped. Bluespec is a declarative hardware description language (HDL) that solves a number of the problems associated with translating a specification to a synthe-sisable form for hardware implementation. Combining Bluespec development with formal specification with B offers a sophisticated verification environment with the associated reduction in development errors.