Verification and analysis of system designs with functional and performance constraints

With the increasing complexity and heterogeneity of today's embedded systems, design methodologies at higher levels of abstraction become a necessity. It is expected that the next major productivity gain will come in the form of system level design since designing at the register transfer level or sequential C-code level is no longer efficient. It follows that new verification and analysis technologies have to be developed in each and every step of the design flow in order to catch design errors as early as possible and to reduce the overall design cost.; Simulation remains a major means of verification for complex system level designs, especially when designs are refined with more design details realized. In this work, a simulation verification methodology is proposed based on trace analysis and automatic trace checker generation. From formal specification of design constraints with mathematical logics such as Linear Temporal Logic (LTL) and Logic of Constraints (LOC), i.e. formal assertions, monitors or checkers are automatically generated and used to verify simulation traces during or after simulation. As a major contribution, LOC formalism is extensively studied, and an efficient checking algorithm is proposed. LOC is also used in automatic generation of distribution analysis tools, which have been exercised on low power techniques in network processor architectures. By utilizing formal assertions, a designer can easily verify both functional and performance constraints of a design in simulation. In addition, a deadlock analysis mechanism is proposed with built-in simulation monitors. This approach is demonstrated in the Metropolis design framework.; For small but important designs or library modules that will be instantiated many times, exhaustive verification is possible and useful. A formal verification methodology for system level design is therefore proposed, where an existing software formal verification tool (e.g. Spin) is utilized as the back-end verification engine, and an automatic translation mechanism from system specifications to verification models is developed. Furthermore, automatic abstraction propagation algorithms can be used to simplify the verification models. In this study, Metropolis is used as a major experiment platform, where a designer is allowed to formally verify design constraints specified with LTL and LOC within the integrated design framework.