Formal techniques tackle the SoC verification challenge

Dan Benua is a principal corporate applications engineer with the Synopsys Verification Group. Dan started his career as a design and verification tool developer, but for the last 14 years he has been helping customers adopt formal and static verification technologies. Dan has an MSEE degree from Stanford University.

Formal verification techniques are finding wider applicability as verification needs increase in response to customer pressure to produce very complex SoCs quickly, especially for the mobile market. Reducing verification costs while reaching ever more challenging verification objectives as the size and complexity of SoCs increases drives the need for new formal techniques and methodologies.

To achieve the necessary design productivity, creating an SoC now means integrating large blocks of existing semiconductor IP with smaller blocks of new functionality.

From a verification point of view, modern SoCs have become so complex that simulation alone cannot verify enough of a design’s state space to provide the confidence necessary to tape it out. Engineers must use multiple verification strategies in concert to achieve that confidence.

From an economic point of view, it has long been the case that verifying a design takes a lot more effort than creating it. As the complexity of SoCs grows, and especially with the introduction of advanced lithography and finFETs at the 20nm node, the cost of verification is rising increasingly quickly. If companies have to keep adding verification staff, servers and tool licenses in line with increasing SoC complexity, while facing static or shrinking schedules, whole classes of design may simply become uneconomic.

Design teams need more effective tools – and ones that can address the verification issues that come with the shift to ever more complex SoCs. Increasingly, formal verification is being pressed into service because the efficiency and thoroughness with which it addresses some specific SoC verification issues is becoming more important in today’s pressurized design time-to-market windows.

How is design changing? First, the number of IP blocks that are integrated in today’s SoCs is rising dramatically. Second, these IP blocks have to be treated as pre-verified, in order to realize the promised productivity gains, although designers still need to understand how internal clock, reset, test and power-management domains will interact with systemic strategies. Third, an increasing proportion of the design task is about integration issues, such as making sure the interconnect is correct, implementing standard protocols, and ensuring that chip-wide clocking, test and power-management strategies work.

How can formal techniques help? No formal tool has the capacity to exhaustively verify a modern SoC, but formal verification can address important verification issues that, if left unchecked, could lead to unforced errors. Sequential equivalence checking, for example, is a relatively new formal technique that helps ensure that the logic introduced to implement chip-wide power, clocking and test strategies do not alter the logical function of the circuits to which they are applied.

In power management, switchable power domains add complexity to SoC design. At the micro level, turning a block on or off changes the logic of the design. At the macro level, each change in the way the chip’s blocks are powered creates a new state of the design to check. With multiple IP blocks with independent power-management strategies, the number of states to be checked rises rapidly.

Formal techniques can address some of these issues by ensuring that a power-aware design follows the right protocols for power state sequencing. The impact of low-power design techniques, such as the introduction of isolation cells between power-managed blocks, can be assessed using static structural checking, and the way the cells are used can be formally verified as part of a power-sequencing analysis.

Another place in which formal techniques can help in SoC verification is in ensuring that all the IP blocks are interconnected correctly and that they remain correctly connected during the transition in and out of test states and under multiple operating modes.

An SoC’s interconnect scheme may use fairly simple circuitry, apart from some multiplexing for reconfigurability, but the verification challenge is to show that the interconnections between a pin and a block or between several blocks are properly made and remain so in all states.

Interconnects can be checked using functional simulation, but it can be extremely complex to set up the logical state of the relevant IP blocks so that a particular interconnect can be toggled at a particular time, with good observability of that transition.

The increasing use of standard interface protocols, both on and off chip, is easing another part of the verification task. Protocols are usually expressed as a set of properties that can be formally verified, and the blocks that implement these protocols are often replicated many times across a chip. Formal verification is an effective approach here because the problem is within the capacity of the tools and is replicated as it scales with the SoC.

Clocking issues, such as what happens when a clock or other signal moves from one clock-management domain to another, can be verified with a combination of static structural and formal verification techniques. Here formal is one component of an integrated verification approach involving multiple verification technologies. Each addresses a category of bugs for which it is most effective. The combination of technologies ensures a bug-free result.

In the absence of a magic-wand solution to exhaustively verify every possible state of a multi-clock, multi-block, power-managed SoC in a reasonable amount of time, formal techniques are proving an increasingly powerful part of the diverse toolkit that designers must employ to ensure that their chips don’t suffer the ultimate verification issue – a failure in the field.

Author

Dan Benua is a Principal Corporate Applications Engineer with the Synopsys Verification Group.  Dan started his career as a design and verification tool developer, but for the last 14 years he has been helping customers adopt  formal and static verification technologies.  Dan has an MSEE degree from Stanford University.