SLEC is Not LEC

One of the questions that Calypto is asked all the time is what is the difference between sequential logical equivalence checking (SLEC) and logical equivalence checking (LEC).

LEC is the type of equivalence checking that has been around for 20 years, although like all EDA technologies gradually getting more powerful. LEC is typically used to verify that a netlist implementation of a design corresponds to the RTL implementation (although more rarely it can be used for RTL to RTL, and netlist to netlist verification). However, LEC suffers from a major restriction: the sequential behavior of the design must remain unchanged. Every register and every flop in one of the designs must correspond exactly to an equivalent one in the other. Tools vary as to how restrictive they are about whether the registers need to be named the same. And this is not quite true, there are a few simple transformation that RTL synthesis does that a typical LEC tool can handle, such as register retiming (whereby logic is moved across registers and might invert the register contents in a very predictable way).

SLEC is used when the sequential behavior is not the same or when the high level description is completely untimed C++ or SystemC and so the sequential behavior is not fully described. The three most common cases where this can happen are:

• a tool such as Calpyto’s PowerPro is used to do sequential power optimization. It does this by suppressing register transfers when the results are not going to be used, but this completely changes the sequential behavior at the register level, although if everything is done correctly it should not change the behavior of the block at the outputs. SLEC is used to confirm that this is indeed the case
• a high level synthesis (HLS) tool such as Catapult is used to transform a design from a C/C++ description to RTL. SLEC can check that the HLS tool created functionally correct RTL from the high level input
• a high level C/C++ description of the design is automatically or manually transformed into another C/C++ description (perhaps to make it synthesize better) and SLEC can be used to ensure this transformation did not introduce any errors

So stepping back to the 50,000 foot level, LEC is used to check that logic synthesis tools have done their job correctly (and these days logic synthesis is buried inside place and route so it is not just the pure front end tools that are involved). It can also be used to check that manual changes made at that level (such as hand optimizing some gates) is done correctly.

SLEC is used to check that high level synthesis tools have done their job correctly or that other tools such as PowerPro that make sequential changes have done their job correctly.

By combining both technologies gives you complete end to end verification from high level description through the various tools that change the design, all the way down to netlist.

More articles by Paul McLellan…