Checking Clock Gating Equivalence the Easy Way

Synopsys just delivered a Webinar on using the sequential equivalence app (SEQ) in their VC Formal product to check that clock-gating didn’t mess up the functional intent of your RTL. This webinar is one in a series on VC Formal, designed to highlight the wide range of capabilities Synopsys has to offer in formal verification. They are obviously determined to have the design world understand that they are a serious contender for the formal verification crown (see also my write-up on their InFormal Chat blog).

I’ll deal with some basic questions first because I’ve heard these questions from at least some designers and others around semiconductor design who need some understanding but don’t need the gory details (sales, marketing, support, …). Starting with the easiest – why gate clocks? Because that’s a good way to reduce dynamic power consumption. Every power-sensitive design in the world gates clocks, to extend battery life, to reduce cooling costs, for reliability or for regulatory reasons.

That was a softball; answering the next question takes a little more thought. I use Power Compiler which allows me to infer clock gating from the RTL structure along with a little guidance from me to hint that it should insert clock gating here but not there). So I can let the tool take care of inserting the right gating logic. But I’m careful to check that synthesis didn’t make any mistakes so I use Formality Ultra to do equivalence checking between the original RTL and the generated gates. Formality Ultra will check the correctness of inserted clock gating along with correspondence of Boolean logic between the RTL and the gates. So why do I need a different tool to check clock gating equivalence?

I confess this also had me a bit puzzled until I thought about it harder and checked with Sean Safarpour at Synopsys. The flow I described above works fine for basic clock gating but there are reasons many design teams want to go beyond this capability, which require them to do their own clock gate insertion.

An important reason is that a lot more power can be saved if you are willing to put more thought into where you gate clocks. Automated gating is inevitably at a very low level since it looks at low-level structures around registers or register banks for opportunities to transform logic to add clock gating. This may still be valuable in some cases as a second-order saving but gating a larger block of logic can often save more power, and at lower area cost. As an obvious example, gating the clock on an IP block can disable clock toggling in the entire block at a cost of just one clock gate structure. This also shuts off toggling in the clock tree for that block, which is important since clock tree toggling contributes significantly to total dynamic power. Whether this is a workable option or not requires design use-case understanding to construct an appropriate enable signal so this is not automatable, at least today.

The other reason is that clock gating is part of the functional realization of your design so must necessarily be included in the verification plan. If clock gating is inferred in synthesis and therefore first appears in the gate-level netlist, that implies some part of your verification plan will have to be run on that gate-level netlist, which is not an attractive option for most of us.

So given you want to hand-craft clock gating in your design, VC Formal SEQ can help by formally comparing the pre-instrumented RTL netlist (before you insert clock gating) with the instrumented RTL netlist to verify that the two RTLs are functionally equivalent (apart, of course, from the fact that one allows for clock gating and the other doesn’t). The webinar walks you through the essentials of the flow – compile, initialization, solving and debug in Verdi where you can compare pre- and post-instrumented designs through generated waveforms and temporal flow diagrams for mismatch and un-converged cases.

Since this is sequential formal proving, there’s always the possibility of non-convergence in bounded proof attempts. It looks like Synopsys has put quite a bit of work into simplifying analysis in these cases. One such example is in building internal equivalence points in hard problems, helping you to reduce what remains to be analyzed to simpler problems or to see where changing effort level, or a little help with constraints or some blackboxing might bring a proof to closure. All this analysis and debug is naturally supported through the Verdi interface.

You can watch the webinar for the real details HERE.