Enabling FV and Simulation using Functional Specifications: The Open-Source ILA Methodology
TimeMonday, December 6th1:30pm - 5:00pm PST
DescriptionA major challenge in hardware design and verification (either FV or simulation based) is the lack of a functional specification that can be used in a consistent way for verification at different stages. In current flows, high-level C/C++/SystemC executable models are manually developed for early functional verification using simulation. However, these are based on informal specifications and often there is no way to guarantee that the final RTL matches these higher-level models. Further, it is hard to use formal verification (FV) with the RTL designs as the properties to be checked are difficult for the designers to manually provide and often far from complete.
Recent work has developed the Instruction-Level Abstraction (ILA) as a functional specification for modules that addresses the above gaps in the design and verification flow. The ILA model of a component is a functional model that defines the response of the component to commands at its interface. It is inspired by the Instruction Set Architecture (ISA) for processors which specifies the processor’s functional response to each instruction in the form of updates to its architectural state. For a processor the architectural state is the state that is persistent across instructions. Similar to a processor, the ILA model specifies the architectural state of a component as the state that is persistent across its commands, and the response to a command (which is treated as an instruction for this component) in terms of the updates to this state. The ILA model is then used to automatically generate (i) a functional simulator and (ii) a set of properties for FV that checks the component’s response to each command – and is thus complete in its coverage of the functional specification. This fills in important gaps in existing design and verification flows. One of the challenges in using FV for property verification is the scalability of the property-checking tools. We will then discuss the open-source, word-level, SMT-based model checker Pono which addresses this. This tutorial will walk through the ILA model specification and FV and simulation flows using this ILA model. We will demonstrate the use of the open-source ILA and Pono tools and design repository that have been developed to support these flows (https://upscale.stanford.edu/).