Event-B for the synthesizable VHDL
| Success Story|
|Keywords||EventB, micro-electronic circuit, VHDL|
|Credit||reproduced with permission of ClearSy|
The Forcoment project (FORmal COdevelopMENT) is a French project, grouping together STMicroelectronics and ClearSy, with the aim of showing that an Event-B model of a functionality can be transformed into description hardware expressed in VHDL. It is directly integrated into a classic electronic circuit development cycle, such as that of the STMicroelectronics microcontrollers.
The work carried out consisted of:
- The study and determination of abstractions used for modelling microelectronic circuits
- The specification of Event-B translation plans around the VHDL subset used by STMicroelectronics, and the development of the associated code generator
- The full-scale application on a functionality for controlling access to embedded memory, Memory Protection Unit (MPU)
- formal assurance to conform to its specification and design through computerised mathematical proof, which can be the subject of an audit.
- similar effort, VHDL size and number of generated gates
- highly parameterized coding is encouraged resulting lower number of modules with less coupling
- validation on an experimental flow only: not yet ready for industry (both method & tool)
- no composition mechanism to assemble units
A formal development cycle
The current circuit development process (see figure No.1) of the microcontroller type at STMicroelectronics requires intensive testing for the verification stages, which precedes the physical elaboration of the circuit (founding). These stages represent the bulk of the time needed for this part of the development. The elaboration of test plans is based on the expertise of the engineers in charge of the verification and validation.
Within the context of this project, we were keen to adapt the use of formal development in successive stages promoted by the B Language, whose software development for rail systems is an obvious success in the microelectronic domain. Indeed this domain only uses formal methods after the event, to perform several verifications, both to the source code and to its transformations into logic gate networks, the final representation prior to entry onto the production line. However, the most costly functional errors are often introduced in the phases prior to the cycle, well before the writing of the source code, particularly as regards the functional specifications, the general design and detailed design specifications, said to be the setting-up specifications. The verification tools are practically inexistent as regards all these "paper" representations and solely the vigilance of the re-readers enables the locating of these "seeds of error" which go on to become "forests of failure" once they’re embedded in the silicon.
The Forcoment project has enabled an alternative development cycle to be built (see figure No.2), which integrates the formal and hence exhaustive verification of the VHDL code in relation to the functional and interface specifications, whilst remaining compatible with the rest of the development flow. This development cycle is based on the formal Event-B modelling, with the aim of correctly constructing digital functions and analogical functions, which are outside the scope of the techniques used as they are simply integrated into the development via their digital interfaces.
This new cycle begins with the writing of a very simple Event-B model containing a few events representing an abstraction of the functionality. The operation details linked to its embedding in a microcircuit are introduced gradually. It is said that the enriched model of these details is refined. The process that enables you to switch from one model to another, enriched with details, clarifying the conditions which make it conform to the former model, is referred to as refinement. The refinement and verification of the conformity conditions are carried out, at each step of the development, by using basic mathematics such as the sets and their operations, predicate logic, or even relations and functions. These concepts prove to be a lot closer to the binary logic of a circuit than it would appear.
The most detailed Event-B model was finally transformed into a VHDL module thanks to the use of the code generator developed ex professo, entitled B4SYN for B for Synthesis. The VHDL module produced by B4SYN is then injected into the rest of the traditional flow. The test campaign conducted on the VHDL module from the traditional flow was successfully conducted on that produced by B4SYN, which enabled the new flow to be validated.
This new flow, though experimental, is already capable of covering up a vast number of errors with total confidence. However, it should integrate the solutions outlined and explored during this project, before being extended to enable the composition of functionalities and be industrially deployed.
The development cycle described above was implemented in a case study, an embedded memory access controller, Memory Protection Unit (MPU), see figure No.3.
The metric measurements collected during the development of this module, both in the traditional flow and the new experimental flow, enable an initial comparison to be made (see figure No.4). Although the latter is in no way standardised, we can observe that the VHDL modules from the two flows represent an equivalent development effort. Even more interesting is the fact that after synthesis, these modules give rise to a number of virtually identical gates. This fact allows us to imagine that the formal proof developed in this way, certainly doesn’t encroach on the freedom of conception necessary for the optimisation of some of the most demanding microcircuits in terms of surface, and which traditionally call upon "hand made" development techniques. Furthermore, the "hand made" element obtained by this new flow is completely guaranteed to conform to its specification and design through computerised mathematical proof, which can be the subject of an audit.
Specific Deploy Contributions
N/A - not a Deploy project
<ref> tag defined in
<references> has group attribute "" which does not appear in prior text.