Why So Formal?

By Bhanu Kapoor
Let’s take a look at the types of power management verification issues that are most suited for formal verification and how formal techniques complement dynamic simulation-based verification in some of the challenging tasks associated with validating SoC power management architectures.

There are three main categories of formal tools in use today: Equivalence Checkers, Assertion Checkers, and Model Checkers. These tools have important roles in the verification of a power-managed low-power design.

Equivalence checking: The formal equivalence checking process is a part of EDA that is commonly used during the development of digital integrated circuits to formally prove that two representations of a circuit design exhibit exactly the same behavior. In many design flows, power management-related modifications with functional implications are done late in the design cycle. Ensuring that the netlist modified for power management still maintains the original behavior in absence of power shutdowns is critical.

A power-aware equivalence requires the equivalence checker to be power-aware and be able work with power architecture description of the design in a format such as IEEE p1801 (UPF). Power management cells such as isolation cells, retention registers, power switches, and level-shifters have power supplies associated with them.

When turned off, the power supplies associated with power domains introduce floating nodes in the design and cause unknown values to propagate to active regions. As a result, power connectivity issues can lead to functional problems in the chip. Utilizing the power architecture knowledge of the system, power-aware equivalence checkers such as Formality from Synopsys can help a great deal in ensuring equivalence of RTL, gate-level, and PG netlists. Many of the complex power-connectivity issues can thus be eliminated. However, equivalence checking is a well known NP-complete problem and time and/or memory requirements can grow exponentially with the number of inputs. You need to be careful about how the system-level design is partitioned to leverage equivalence checking effectively.

Assertion checking: The use of assertion checking can be very helpful in validating a power management architecture. An assertion is a predicate (i.e., a true–false statement) placed in design code to indicate that the predicate should always be true during the operation of the design. These assertions can be validated during the course of simulation and formally proven using assertion checkers.

Each power domain typically observes a timing-based protocol in sequencing power to it. For example, turning off the clock, isolating the domain, saving the contents of retention registers, switching off the supply, and doing the reverse of each of these when bringing the power back to the domain follow a well-defined timing protocol. The behavior of this protocol is well suited for assertion-checking utilities. There are many system-level assertions that are ideal for assertion checking, as well. For example, when a domain shuts down it causes some other domain to shut down within a specified number of cycles.

Model checking: Given a model of a system, a model checker will test automatically whether this model meets a given specification. Multicore and many-core systems use dynamic power management to manage power and performance. Dynamic power management refers to the scaling of frequency and voltage to meet power and performance requirements for different cores in the system. You must ensure that the dynamic power management scheme is both safe (power or thermal issues) and efficient in meeting performance goals under power constraints. Model checking of a high-level power scheme model can give estimates for verification efforts and provide insights into how design parameters impact this effort.

All of these approaches can help provide some insights into the tradeoffs of power, performance, and verification effort.

–Bhanu Kapoor is the president and founder of Mimasic, a low-power consultancy.