A Comprehensive Automated Assertion Based Verification

Using an assertion is a sure shot method to detect an error at its source, which may be buried deep within a design. It does not depend on a test bench or checker, and can fire automatically as soon as a violation occurs. However, writing assertions manually is very difficult and time consuming. To do so require deep design and coding knowledge, whereas verification engineers neither have such deep coding expertise nor a comprehensive knowledgeof the design to embed assertions for complex functionalities. Moreover, with rising SoC size and complexity, the design and verification engineers are hard pressed with their core tasks. The result is lack of enough assertions in the code for white-box level testing. The verification engineers typically write only high-level assertions for key interfaces, registers and data buses, which are good for black-box level testing. These high-level assertions do not usually cover the interior of the design.

Considering today’s situation where IP blocks from multiple sources are integrated together in an SoC, quality of verification cannot be assured without a comprehensive white-box as well as black-box level testing. An undetected bug appearing in the field or late in the design cycle can cause a large number of unnecessary debug cycles. What if there was an automated tool that can create white-box assertions automatically? Additionally, what if this tool can also complement all types of verification methodologies while providing comprehensive design coverage at the IP level as well as the SoC level?

‘Automated Assertion Synthesis’ is an innovative technique by which the complete functional behaviour of a design is captured during its regression testing. This behaviour is then analysed and optimized to create a minimal set of properties that fully describe the valid state space of the design. For example, at the IP level simulation of a design having 16 entries FIFO, an ALU and a memory controller, we might observe following properties:

FIFO_Full == 1’b0; FIFO never Full
FIFO_CNT <= 4’d11; FIFO entry count < 12
ALU_Mode[1:0] <= 2'b11 ALU Mode "11" (Multiply) never seen
MemCtrState[2:0] !=2’b100 State “100” (cache miss) never reached
!(RegRd & RegWr) Simultaneous register read & write never observed

The FIFO entry count never exceeded 12 entries; a multiply operation was never tested; the memory controller state machine never encountered a cache miss; and simultaneous read and write was never observed on any register. These properties can be used to create assertions that alert the verification engineer whenever the design goes out of this state.

A comprehensive set of properties, thus created for an IP, can be used as an ‘executable specification’ by automatically converting them into assertions. These assertions can then be passed along with the “golden RTL” of the IP to the SoC team.

MARS (Methodology for Assertion Reuse in SoC) is an innovative approach where the IP level assertions are re-used at the SoC level to catch anything new which was not observed at the IP level. The reasons for an assertion to trigger can be integration or interface error, illegal use-model or mode of IP, coverage holes in the IP verification, or actual hardware bugs. By using the MARS methodology, significant time is saved by knowing the root cause of the problems when they occur and helping to uncover many different kinds of bugs in the design.

The ‘automated assertion synthesis’ provides sufficient assertions to comprehensively capture functional behaviour, and measure functional coverage at the IP level.

MARS also complements the HW/SW co-emulation process. Emulation is well proven at finding corner case bugs. However HW/SW co-emulation may process billions of cycles of random stimulus at the system level in order to find a bug. In the MARS flow, the automatically generated assertions work easily with emulators and immediately trigger when a corresponding error is observed in the emulator. This immediate notification saves weeks of debugging time when the error requires millions or even billions of cycles to propagate out to the observable points of the design.

Configuration errors in modern IP such as USB, PCI Express, SATA and others can be detected automatically if assertions are embedded along with the IP core in the emulator.

The whole of this novel methodology for full-chip automatic assertion synthesis is captured in a tool called BugScopefrom Atrenta. It helps in catching IP configuration and design issues at the SoC level along with critical coverage issues missed at the IP level. The assertions are optimized to minimize simulation times. Temporal operators are used to capture sequential behaviours and identify issues among multiple clock cycles. The properties are generated in IEEE standard formats such as SVA (SystemVerilog Assertions), PSL (Property Specification Language), or synthesizable Verilog.

Finally, BugScope can be used in a progressive flow for verification that provides direct visibility into how verification closure is progressing. It measures whether verification is targeting the complex logic sufficiently, and whether it is distributed well across the critical functions of the design. This brings a more accurate definition and reality to verification closure.

There is a whitepaperon the Atrenta website which describes BugScope and the automated assertion based verification methodology in much greater detail. There are also interesting customer case studies that illustrate huge benefits of using this methodology.

Automated assertion synthesis is a practical and proven approach that enables a targeted verification methodology spanning the entire design flow, from early IP development to SoC integration and system-level HW/SW co-verification.