Challenges and Goals of VerSys

The VerSys project conducts research on formal verification techniques for Systems-on-Chip (SoCs). It innovates on previous approaches by leveraging newly developed methods of computer algebra. The project is focussed on proving functional correctness of highly optimized data paths that comprise the computational heart of today's SoC designs.

Modern design flows for Systems-on-Chip (SoCs) pursue a correctness-by-integration strategy when verifying the functionality of the overall system. This requires a very high design quality for the individual modules to be integrated into the SoC. Today, functional verification accounts for 60-80 percent of the total design costs. As SoC modules become more and more complex traditional simulation-based verification techniques have become the bottleneck for the overall productivity of the SoC design process.

In this project, we employ highly automated techniques for formal property checking. The current technology is mostly based on satisfiability solving (SAT) and SAT modulo theory solving (SMT). Commercial tools are available that have the capacity to handle a wide spectrum of modules as it can be found in today's SoCs. Nonetheless, some pathological cases remain. In particular, data paths are often a challenge. This is true, especially, if not only the correctness of the control flow but also correctness of the computed data needs to be proved. For complex arithmetic data paths simulation is therefore still the prevailing technique in industrial verification environments.

In VerSys we pursue a completely new approach to formal data path verification. We extract the arithmetic sub-problems raised by the proof goals of property checking and model them as algebraic problems. It is an important objective of this project to identify appropriate algebraic models for digital SoC components such that maximum benefit is obtained from modern and powerful methods of computer algebra. In particular, by our models well-known algorithms such as the computation of Gröbner bases for polynomial ideals are made applicable and offer entirely new ways to handle formal SoC verification tasks. On the other hand, the application domain of formal SoC verification has provided important impulses for new theoretical contributions and new algorithms for computer algebra. In particular, the engineering problems considered in this project have spurred extensions to our computer algebra system SINGULAR (www.singular.uni-kl.de) as well as the development of our new tool PolyBoRi (polybori.sourceforge.net). Our new developments have been made accessible via a common computer algebra suite; see e.g. SAGE (www.sagemath.org).

With our new techniques we have been able to solve various industrial verification problems that have previously been considered as intractable. The results of this project suggest that computer algebra is a promising new pillar in the basic tool set of Electronic Design Automation (EDA) for microelectronics circuits and systems.