A logic-based approach for hardware/software co-design
Honey Ahmed Zedan · 2000
In the hardware industry, simulation is still all too frequently considered synonymous with verification. The design process usually consists of developing an implementation from a specification without the use of any formal proof techniques. Both are then simulated for a number of inputs (an approach known as co-simulation). Bugs discovered are removed and the simulation process is repeated over again. However, formal verification cannot completely replace the existing simulation approach. This is because simulation provides powerful and more accessible tools for rapid prototyping and testing. What is needed is an approach where the design process is soundly based upon formal techniques, but includes integrated support for simulation. This combination would bring more reliability within an environment which does not require a complete changeover from current practice. In this paper we describe a sound technique with a supporting tool, AnaTempura, for hardware/software co-design. Using our technique, we can validate and analyse system's behaviours of interest. The validation and analysis are performed within a single logical framework using Interval Temporal Logic (ITL) and its executable subset, Tempura. Behavioral properties such as safety, liveness, timeliness, are expressed in ITL as theorems which can then be validated and tested compositionally. (6 pages)