Author(s)

J-L Boulanger, A Aljer & G Mariano

Abstract

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 (secure in this paper means more than correct, the design performe what the client wants, furthermore it garantees to note achieve the unwanted cases) digital circuits that may be easily developed and does not need a design test. The circuit design may be based on the libraries of well-known circuit design language like VHDL. Our goal is to make use of B method to produce the electronic or numeric circuits. 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 constuct 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 tanslated 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 which all the specification parts has already been proven to be correct.

Keywords