Divide and Conquer – Formal for Large Designs

As we have discussed in several of the blogs on this forum, successful deployment of Formal verification requires knowing where and how to use it. Building up an arsenal of techniques that can be applied to deal with complexity and knowing how to use them safely is a necessity for every expert Formal engineer.

So what should we do when we come across larger designs than we have been traditionally tacking with Formal? The first thing to remember with Formal is that it’s an exponential problem and you will not win with brute force alone. If you can see that the design is just too big and that your properties aren’t making progress then don’t just keep upping that timeout, you’re bringing a cup of water to a gunfight.

One very straightforward and intuitive method for large designs is divide and conquer. Dividing the design into separate parts to verify separately can be a great technique to reduce the complexity for the Formal engines, but this comes with its own risks. When we split a design up we are creating new primary inputs which require new constraints. How can we know that by doing this we aren’t masking any bugs by blocking the upstream incorrectly? This is where we can use power of Formal verification by deploying a technique known as assume-guarantee.

Assume-guarantee is a technique which allows us to ‘guarantee’ that our constraints are correct by asserting them on the driving logic. In the figure above we have taken the top level and divided it into two smaller blocks: A and B. When we create this division we create a midpoint in the design at which something needs testing – these are the outputs of A. Because of the exhaustive nature of Formal, if we can prove something about the outputs of A, it then becomes safe to convert it into a constraint on the driving logic of B. We are proving that a wire which once connected A to B will always behave in a particular way. Once we have this proof we can safely force the behavior onto B.

This allows us to safely divide a design into smaller sections that can be verified independently and guarantee our constraints are correct. Although we may have broken the top level problem down, we are still verifying all the functionality of the entire design. In addition, the properties we have developed to check the divided sections of the design can be pulled back in and used as invariant properties at the top level. This can help to assist the overall top level check, though with careful assume-guarantee usage this becomes a ‘nice to have’ rather than a must have.

There are a number of techniques we can use to deal with complexity when using Formal on designs, but divide and conquer, when supported with assume-guarantee, can be an extremely effective method to tackle large designs.