Formal methods for embedded system design
Harry Hsieh, Alberto Luigi Sangiovanni-Vincentelli · 2000
The goal of this dissertation is to investigate how formal methods can be applied to the domain of embedded system design. The emphasis is on the specification, representation, validation, and design exploration of such systems from a high level perspective. We start by reviewing the framework upon which the theories and experiments are based, and through which our formal methods are linked to synthesis and simulation. We also review in detail the formal model of computation used to represent embedded system specification and implementation: Network of Codesign Finite State Machines. We formulate a formal verification methodology to verify general properties of CFSM networks and demonstrate that this methodology is efficient in dealing with the problem of complexity and effective in finding bugs. However, manual intervention is required. Manual intervention comes in the form of abstraction selection and separation of timing and functionality through constraints on the architectural mapping. We conjecture that for specific properties, efficient algorithms exist for completely automatic formal validation of systems. The analysis of the application of formal verification techniques to CFSM networks led us to choosing a property that is basic, but embodies the principle of separation of timing and functionality: synchronous equivalence of two different implementations. This property is analogous to functional equivalence for sequential circuits. One powerful result of this equivalence criterion is the identification of a set of delay-insensitive scheduling policies. Once a delay-insensitive scheduling policy is chosen, any variation in delay does not affect the functional behavior. For efficient equivalence checking of implementations using different delay-insensitive scheduling policies, we propose structural algorithms based on worst-case analysis of the communication among components. The events communicated between components are abstracted into a signature that is maximal in the sense that it represents all possible communication patterns of that system. By comparing the signatures of different delay-insensitive scheduling policies for a given system, we were able to determine equivalence conservatively. Lastly, we relate communication analysis to exhaustive simulation through a series of refinement and pruning operations on the communication signatures. An algorithm can choose to work at any abstraction level trading off computational efficiency with the possibility of inconclusive result due to false negatives. We provide primitives to move between different abstraction levels that exist between communication analysis and exhaustive simulation. We demonstrate with real-life examples that synchronous equivalence opens design exploration avenues uncharted before.