الفهرس 
coverOnly 14 pages are availabe for public view
 |  | from | 131 |  |  |
| | | from | 131 | | |
Abstract
The most common procedure to ensure the reliability of a design is simulation. Unfortunately simulation cannot fully inspect all the execution states of the system. The significant increase in the complexity and size of digital systems together with the nature of real time systems boosted up the need for a different approach for the validation of the behavior of a system in the early design stages. Formal verification is an approach to validate a system by formally reasoning the system behavior. In formal verification the system implementation is checked against the requirements or the properties to be satisfied. B method is one of the common paradigms used in formal verification. B method offers strong verification domain as it based on a mathematical and logical approach. The proof obligations (properties that must be satisfied) are automatically generated from the model, also the available tools provides both automatic and interactive proofs.
VHDL is a mature implementation domain where many synthesis and simulation tools are available.
The work in this thesis presents a technique to convert B machines into the corresponding VHDL implementation in order to implement a correct by construction system, benefit from the advantages of both strong domains, and maintain the properties of the verified model.
Challenges in going from B domain to VHDL domain:
• Not all constructs of B are available in VHDL.
• Completely different Semantics.
• Different approaches of handling design modules.
• Variables and signals are represented in completely different ways.
We reached for a method to cross the gap and converted the B machines into VHDL implementations. The unavailable B constructs are described by VHDL code constructing the required part of the model. The developed tool starts by an initial step to handle the connected modules in a way that can be converted into VHDL code. The B machine is investigated to find the way each variable is used and indicate how it can be handled in the generated VHDL code. Five popular models were used as workbenches where we applied the developed technique. Simulation at some critical points was used to ensure that the generated VHDL satisfy the verified properties in the originalB machine