Improved Validation

Overview

Dramatic decrease in validation time and cost is essential for productive hardware construction. Validation results are required for designers to evaluate their choices and drive decisions for the next iteration of the design space exploration cycle. Our research strives to simplify the functional verification of designs, so that designers can spend more time reasoning about the performance characteristics. In an ideal world, designs are correct by construction, so a designer can purely focus on performance evaluation. In practice, designers are integrating components from various sources that cannot be formally proven to be correct. Therefore, our research efforts are focused on the rapid verification of modular systems that integrate components from many sources. There are two major thrusts of this research: (1) the development of better formal tools for proving properties of complex modular systems, and (2) the development of better user interfaces, in the form of a domain specific programming language, for the construction of hardware verification components. These are described in more detail in the following section:

Pono Model Checker

Pono is our solver-agnostic model checker. The name is derived from the Hawaiian word for “correct”, “moral”, or “excellence”. Pono is implemented in C++ and provides a command line interface, C++ API, and Python API. It utilizes Satisfiability Modulo Theories (SMT) solvers for automated formal verification of transition systems modeled in various background theories such as bit-vectors and arrays. There are three main design goals for this system: i) performance; ii) flexibility; and iii) extensibility. Performance is important for push-button use of verification engines. Flexibility allows knowledgable users to tailor the tool for their specific goals. Finally, extensibility allows algorithm developers to prototype new ideas within an existing framework. These three goals are in service of advancing state-of-the-art SMT-based model checking techniques and their application to real systems. Specifically within the hardware domain, using SMT preserves higher level design information that is lost when producing a bit-level netlist. We are currently focused on clever design abstractions, symmetry breaking techniques, and proof techniques for the SMT theory of arrays, which is useful for modeling large memories. This system also benefits from the impressive annual improvements in SMT and SAT solving, as demonstrated by the annual competitions. For this reason Pono is implemented modularly to easily incorporate the latest solver enhancements in underlying SMT solvers, by leveraging the open-source SMT solving C++ API, Smt-Switch. Furthermore, many SMT solvers are built to interface with arbitrary SAT solvers. Thus, solver improvements anywhere in the toolchain can quickly propagate through the system by updating or swapping solvers, resulting in faster verification times. 

Fault

Fault is a domain specific language for hardware verification embedded in Python.  The design of the system draws inspiration from many ideas in software engineering and testing, namely abstraction design for productivity, portability, and performance.  A major goal of Fault is to develop a unified interface to execution-based (simulation, emulation, silicon) and formal verification using an interface inspired by traditional constrained random verification methodologies.  This design leverages the fact that many design teams are already applying constrained random verification for execution-based verification and thus would enable these teams to easily pick up powerful formal techniques without having to learn a new methodology. As part of this effort, Fault has been designed to enable the construction of portable test bench components that can be used in various simulation, emulation, silicon, and formal environments. This enables a level of reuse that is not possible using the traditional methods that have been designed to work in just one of these environments.  Fault aims to enable the rapid specification of tests, inspired by software methodologies including test driven development and property based testing.  These techniques have proven effective for the productive development and testing of complex software systems and thus present viable solutions for the domain of hardware verification.  Fault also uses staged meta-programming to enable the development of test generators, which allows test developers to incorporate the same flexibility and reuse as the hardware generators they are testing.