Timing verification of interface specifications and controllers

Microelectronic systems are normally composed of components such as Application Specific Integrated Circuits (ASICs), custom integrated circuits and other intellectual properties. These components are generally designed by different teams from different organizations. In the systems, components are connected and communicated with each other through interfaces. To make the systems work, it is very important to verify that the interface specifications of components are compatible with each other and the implementations of interfaces are correct with respect to their specifications.; This work deals with timing verification of interface specifications and the verification of the interface controller implementations against their specifications.; The timing verification of interface specifications includes compatibility and the verification of the safety timing property. In this work, we solve the timing verification problems using maximum time separation between events in constraint graphs transformed from the specifications. The interested interfaces are specified as loops over a leaf Hierarchical Annotated Action Diagram (HAAD) language. We apply our solution technique in verifying several safety timing properties of a specification modeling a repeated READ operation of a microprocessor from a memory.; The verification of interface controllers against their specification consists in making sure that the implementation will produce correct events on time as given in the specification, under the assumption that the inputs events fed to the controller are on time as also stated in the specification. In this work, we present a method for verifying whether a pseudosynchronous (sampled input) finite-state machine implementation of a real-time controller satisfies its timing diagram specification.; We apply our method to a bus controller from an industrial design and check against its timing diagram specification modeling two consecutive asynchronous cycles.; All the algorithms and verification methods in this work are implemented in a Constraint Logic Programming environment based on Relational Interval Arithmetic.