Abstract
The application of hardware controllers within safety critical environments is becoming ever more common and complex. With increasing complexity comes a higher potential for design errors. Hardware design tools such as Electronic Design Automation (EDA) tools, aim to expose these errors using equivalence checking between abstract and concrete designs and apply functional property verification, driven by scenarios. Determining these scenarios using test environments, is however, not always straightforward. The EDA tools aid in determining the simulation coverage of test scenarios, but finding corner cases during testing to ensure complete coverage is difficult. Current research in hardware verification aims to find methods that can discover these extremes and identify errors that reside within the design; one of these approaches employs formal methods. In this research, we determine that an existing Communicating Sequential Processes (CSP) compiler, the Shared Variable Analyser (SVA), is suitable as a basis for our work. SVA is designed for analysing threaded processes that interact with shared global variables. The systems analysed by this custom compiler reflect many of the behavioural concepts within the hardware design language, Very High Speed Integrated Circuit (VHSIC) Hardware Description Language (VHDL). A contribution of the thesis is the definition of formal approach for modelling hardware designs based on the concepts of shared signals. This approach is implemented by extending the SVA compiler; we call this augmentation of the compiler the Shared Variable Analyser for VHDL (SVA4VHDL). Another contribution of the thesis is the automatic generation from VHDL scripts to SVA4VHDL scripts, which are then provided as input to the compiler. This automatic generation ensures that scripts can be generated easily and repeatably without errors. SVA4VHDL introduces: new syntax to the compiler to model VHDL processes; replaces the SVA variable definition with a new CSP process that correctly describes the different types of VHDL signals; defines a CSP process that describes the VHDL stabilisation model for signals; and captures the design of each system as it is written, not only modelling the behaviour within a hardware design, but also the hierarchical structure used when composing the hardware description. The hierarchical compilation strategy used in our approach leads to an optimised CSP process composition, and therefore is able to accommodate hardware designs comprising multiple instantiated VHDL components. We exploit full state space exploration of hardware models compiled by SVA4VHDL that may yield counterexamples demonstrating that the system requirements have not been met. These counterexamples can form the basis of test scenarios which can then feedback into the EDA tools. The compiler proposed in the thesis is applied to two case studies, a Traffic Lights System and a Built-In Self Test. The case studies provide confirmation that SVA4VHDL is capable of producing optimised CSP models for complex VHDL hardware descriptions and support a discussion on the scalability issues and limitations of the formal approach. The Traffic Lights System was also used to perform a comparison with an existing CSP approach proposed by Evans, to model VHDL descriptions. This evaluation demonstrated that Evans' approach was not suitable to model real world hardware systems and a clearer more optimal modelling strategy was required. Furthermore, the case studies identify different styles of specification that can be applied to SVA4VHDL models, from traditional safety and liveness specifications to the use of fault injection processes. Fault injection requires the exchanging of definitions of a model’s components so that faults can be detected. If all specifications are met, the hardware designs meet their original requirements, providing the high confidence levels required for safety critical systems.