BHDL

BHDL is method of correct design of digital circuit. It combines the advantages of VHDL, the well-known language of circuit design, with the power of B method that guarantees the correct design with regard to a formal specification. This allows avoiding the design test since it is ”correct by proven construction”.

Relation between VHDL and B method

The relation between the abstract machine and the refinement in B method in a B project seems like the Entity-Architecture relation in a VHDL project. In BHDL, from an enriched VHDL notation, the main structure is captured and communicated to the main formal model in order to prove the consistency of the structure and the coherence in relation to the abstract architecture and with the other components of the system. From the graphical tool, VGUI, the main structure of the system is created. Then, two different notations are generated VHDL and B. The produced B method code contains the main features of VHDL one. After that, design may be separated in relation to the techno-logic choices. For more flexibility, designer may write directly the enriched VHDL notation.

References

• Ammar Aljer, Philippe Devienne, Sophie Tison (LIFL),Jean-Louis Boulanger (HDS),Georges Mariano (INRETS). BHDL: Circuit design in B . 2003 IEEE
• A. Aljer & J. L. Boulanger (Heudiasyc, Compiegne, France),P. Devienne (LIFL, Villeneuve d’Ascq, France). B-HDL circuit and safety properties
• Aljer A. 2004, Co-Design and Refinement in B. PhD Thesis. USTL: Lille.

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.