B/HDL: design of safety circuit

The goal of this paper is to show how it is possible to combine the advantages of the B method in order to design secure digital circuit that may be easily developed and does not need a design test. At the beginning, the circuit specifications are written in the abstract machine. The refinement direction is determined by the basic elements which are used to construct the desired circuit. So the designer can orient the development to the needed level. This level can be found as a basic library in B. We demonstrate how VHDL packages can be translated as B circuit components for giving to the designer a high-level view. Using this approach, one can develop a circuit of which each part of the specification has proved to be correct. From the B model it is possible to generate the VHDL code