Sequential Equivalence Checking with Jasper

When new restaurants open they sometimes have what is called a ‘soft opening’ where they open a few days earlier than the official opening night. They are less busy since nobody knows they are open yet, maybe the whole menu isn’t available and expectations may be lower. Of course, Broadway productions also often open off-Broadway (although that usually means a long way from Broadway these days, like Chicago). And anyone who has ever raised money for a startup knows that you don’t do the first run-through of your pitch with a big name like Sequoia. You polish it with a couple of people who are not likely to invest but at least are prepared to spend the time with you.

Of course EDA products often have soft openings too, sometimes known as beta-testing. If this is done properly then a handful of lead customers use the product, help debug it, and hopefully show up to praise it in the official launch. I’ve said before that one of the hardest problems in EDA these days is getting test data to test your new tool. Leading edge companies are not going to send you their latest microprocessor or modem. Or any 20nm design for that matter. It is not just a data problem, you have to solve a problem that a customer really feels pain about, or never mind the data they won’t give you the time. However, somehow you need both data and engineers to test a state-of-the-art tool that solves a critical problem. In EDA anything else won’t sell anyway, so why bother to develop it.

One big problem is verifying RTL to RTL, known as sequential equivalence checking or SEC. Combinational equivalence checking (“normal” equivalence checking) assumes that all the registers in both sets of RTL always hold the same values. In some cases they may even assume the registers are named the same. Perhaps they can cope with some simple cases such as register retiming. Here logic is moved from after a register to before (or v.v.) to balance timing during synthesis; if you move an inverter then the register value is inverted, but then it is always inverted so not too hard to cope with. This also copes fine with the type of clock gating added automatically in synthesis: if the register value is not going to change (usually because the old value is being recirculated) then don’t clock the register instead (and take out the unused muxes).

SEC handles more complex cases, where the register values might not always match. Why would you want to do something like that? The biggest reason these days is power. Isn’t power always the biggest reason in any SoC today? It can also be architectural optimization. But the main reason for doing architectural optimization is power, so I repeat myself.

I mentioned one case where you might not clock a register, which is when you can detect the value is not going to change. In effect, it already holds the “right” value. But another more subtle case is when you can detect that the value is not going to get used downstream. In that case you can avoid clocking the register, but now it holds a “wrong” value. But that doesn’t matter since the wrong value goes straight into a multiplexor (say) that selects some other value and you can know that the wrong value will never be seen. If you can see that the value of the register is only used occasionally then a lot of power can be saved by only clocking in the value when it is about to be used.

You can further reduce power. If a register is not gated on this clock cycle and feeds another register, then it does not need to be gated on the next clock cycle since the old value is already correct. This requires adding flops to the clock nets (also a change in sequential behavior) to capture whether the previous stage was clocked the cycle before. There are other cases like this too, but you get the idea. A lot of this optimization is done by hand, but there are also at least 2 or 3 automated solutions that cover some of the cases (not from Jasper, they are focused on formal verification of designs and are not too concerned about how you got there).

If this sounds like it might generate a lot of weird corner cases then you are right. One technology is especially good with corner cases though: formal verification. Jaspers SEC App can handle these cases and prove you didn’t get them wrong and let an occasion slip through where the value is used but the register is not clocked. But it’s an App that doesn’t exist yet except off-Broadway.

Joe Hupcey, director of product development at Jasper has a blog entry showing in a more detail just how the SEC App can be used to verify that power optimizations only reduce power and don’t screw up the design. The blog is here.

Vigyan Signal of Oski (who are specialists in performing formal verification as a service and generally helping customers with formal verification methodology) has a video about using the SEC App with a lot of practical details about flow and methodology. It is less than 8 minutes long.

Jasper’s User Group is October 22-23rd in Cupertino. I’m sure there will be more on SEC there. Indeed, it is second on the list of topics that will be covered. More details and to register are here or click on the banner below.