Introduction
Verification of today's system-on-chip (SoC) designs is a hard problem that keeps getting harder. Design size and complexity continually increase, while the market demands ever-tighter development schedules. Multiple approaches such as directed and coverage-driven random simulations, assertion-based verification, and formal analysis are needed to most effectively verify a chip. This article focuses specifically on the technique of formal analysis and discusses how to adopt it efficiently on SoC projects.
Assertion-Based Verification
The goal of functional verification is to find all functional bugs before tape-out while getting the best return on investment (ROI) for the verification effort. In order to achieve this goal, there are several verification milestones along the way. It is important to meet these milestones on schedule so that time-to-market is not compromised. These milestones typically include completion of a verification plan, reaching coverage goals, and a bug discovery rate that asymptotically approaches zero.
Traditionally creating testbench environments and running a large set of simulation test cases have reached these goals. These were originally hand-written directed tests but today are more likely automated constrained-random and coverage-driven tests. This approach works in many cases but still more than 50% of chip re-spins are caused by functional problems. The ability to find bugs can be greatly improved by adopting an assertion based verification (ABV) methodology.
ABV is a methodology that uses assertions to increase the productivity and quality of functional verification. ABV provides methods to specify properties and cover points. These properties can often be used in a consistent fashion with full reuse across formal analysis, simulation, acceleration, and emulation. As shown in Figure 1, this flow allows engineers to leverage the best technologies at each particular point in the design and verification process.
Properties are statements, derived from the design specification, about the intended behavior of the design and its environment. They can be used as assertions or as constraints depending on context. Assertions are checks that specify the behavior of outputs and internal signals in the design. Constraints specify the behavior of the inputs to the design and thereby define its environment.
In simulation, assertions increase the observability of bugs by monitoring for illegal behavior within the design or on its interfaces. Assertions are especially valuable in full-chip simulations since they help isolate each bug at its source. This often reduces debugging time from days down to hours.
The Role of Formal Analysis
In order to fully reap the benefits of ABV, the use of formal analysis is required. Formal analysis improves the controllability of the design under verification. It uses mathematical techniques to target each assertion and either prove it correct or find a way to violate it. The constraints ensure that only legal input sequences are used when proving assertions.
Assertions in simulation, sometimes with follow-on re-use in acceleration and emulation, are also valuable. However, use of assertions in simulation does not necessarily lead to adoption of a full ABV flow mainly due to limited use at the block/module level. Formal analysis, by its very nature, fosters more comprehensive ABV adoption, which in turn benefits both simulation and hardware-based verification methods.
1. An Assertion-Based Verification Flow Spans Block, Cluster, and Chip.
Click here for a larger version
In the past, use of formal analysis has faced three major barriers: proprietary assertion specification formats, formal tools that were hard to use, and the lack of a pragmatic methodology. As a result, past usage of formal analysis has been almost entirely limited to experts who were willing to learn abstruse academic property languages or be confined to vendor-specific assertion formats. Recent changes in the industry and advances in formal technology have changed this situation dramatically.
The introduction of assertion standards that work across formal, simulation, acceleration, and emulation has removed the historical specification barrier. The Property Specification Language (PSL), SystemVerilog Assertions (SVA), and the Open Verification Library (OVL) are all Accellera-endorsed formats for specifying assertions; PSL and SystemVerilog also have been ratified as IEEE standards. With support for these assertion formats built directly into many tools, it's easy to get started using formal analysis.
Improvements in ease-of-use, robustness, and automation for algorithm selection and abstraction techniques in many formal tools have effectively removed the second barrier. These improvements have moved formal analysis usage beyond the experts; mainstream design and verification engineers are now reaping its benefits. This, in turn, is helping to eliminate the final barrier. Broad deployment of formal analysis requires tool vendors to provide pragmatic guidelines for users as well as integration into standard verification flows.
|
