The Impending Verification Revolution

Raul Camposano, Chief Technology Officer Senior Vice President Synopsys, Inc.

Abstract

The functional verification of a complex digital design is one of the most time-consuming design tasks. It is based mainly on simulation. Simulation requires that the designer develops three essential models: the design being simulated, the environment generating the valid simulation input vectors for that design, and a reference for what are considered correct simulation results. In addition, a measurement of which parts of the design have been simulated („coverage“) helps to evaluate the progress of the simulation.

In spite of its significant progress to date, functional verification continues to undergo a profound transformation. First, the practice of automating the environment generating the simulation vectors is being automated. Second, the modeling of correct simulation results is being changed to assertions (also called properties) that can be described formally. Assertions can be checked during simulation time. In some cases, assertions can be proved formally for a given environment (property checking). Assertions can also be stored as IP for a given design: for example, the properties of a bus protocol can be stored as assertions and can be reused for every design using that particular bus. Some assertions must be stated by the designer, e.g. the maximum time allowed between two signals, while others can be derived automatically from the RTL description, e.g. prohibiting a given state that would lead to an unspecified branch in a case statement. Third, the verification environment can be automatically derived from constraints that formally describe the restrictions on the input vectors. Again, formally-described constraints for given designs can be stored as IP and reused, a trend that continues to move us closer towards a more complete suite of reusable verification components.

This talk describes the above constraint/assertion-based functional verification, shows how simulation and formal techniques work together in such a methodology, assesses the complexity and current limitations of formal techniques, and examines what we expect in the future.

Curriculum Vitae

Raul Camposano joined Synopsys in January 1994 and currently serves as Chief Technology Officer, Senior Vice President. He previously served as the General Manager of all Synopsys Design Tools Business Units and was also Vice president of Engineering. Prior to joining Synopsys, Dr. Camposano directed the German National Research Center for Computer Science Design Technology Center and was a Professor of Computer Science at the University of Paderborn, Germany. Between 1986 and 1991, Dr. Camposano led the project on high-level synthesis at the IBM T.J. Watson Research Center. Active in the EDA professional community, he also serves on various technical program committees and editorial boards worldwide and has published over 70 articles and three books on electronic design automation. He was elected an IEEE fellow in 1999. Dr. Camposano holds a B.S. and an M.S. in E.E. from the University of Chile, and a Ph.D. in computer science from the University of Karlsruhe.