BHDL: Principles and tools for generating proven hardware

Abstract

In this chapter we discuss modeling of hardware and translation to VHDL. Translation to SystemC or Verilog is similar. However VHDL is easier to read and we use VHDL synthesis tools. Translation is path complete path from formal models to a circuit. Equally important we need a refinement method to arrive at a formal circuit description that can be translated. This method has some significant differences to the refinement method for software. As one would expect, they are virtually not present at system level but become more and more implementation is approached. This means that the initial visible as an actual implementation is approached. This means that the initial refinement steps ued in hardware are, in principle, also pplicable to software, and vice versa.

The subset of the B-language that serves to describe hardware is called BHDL. The definition of the BHDL subset is oriented at the register level for hardware description.