Increasingly at DAC and other shows, EDA companies such as Jasper are having their customers present their experiences with the products. Everyone has seen marketing people present wonderful visions of the future that turn out not to materialize. But a customer speaking about their own experiences has a credibility that an EDA marketing person (and I speak as one myself) do not. In fact EDA marketing doesn’t exactly have a great reputation (what’s the difference between an EDA marketing person and second-hand car salesman? the car salesman knows when he is lying).
At DAC Jasper had 3 companies present their experiences using various facets of formal verification using JasperGold. These are in-depth presentations about exactly what designs were analyzed and how, and what bugs they found using formal versus simulation.
The presentations were videoed and are available here (registration required).
ARM
Alan Hunter from Austin (which based on his accent is a suburb of Glasgow) talked about using JasperGold for validating the Cortex-R7. It turns out that a lot of RTL was available before the simulation testbench environment was set up so designers started to use formal early (for once). They found that it was easier to get formal set up than simulation and, when something failed, the formal results were easier to debug than a simulation fail.
He then discussed verifying the Cortex A15 L2 cache. They had an abstract model of the cache as well as the actual RTL. The results were that they discovered a couple of erros in the specification using the formal model. They could also use the formal model to work out quickly how to get the design into certain states quickly. And they found one serious hardware error.
With A7, where formal was used early, they focused on bug-chasing and were less concerned about having full proof coverage. But with A15 they were more disciplined and more focused on proving both the protocol itself and the reference implementation were rock solid under all the corner cases.
NVIDIA
NVIDIA talked about using JasperGold for Sequential Equivalence Checking (SEC). Equivalance Checking (EC), I suppose I should say Combination Equivalence Checking to distinguish it from Sequential, is much simpler. It identifies all the registers in the RTL and finds them in the netlist and then verifies that the rest of the circuit matches the RTL. The basic assumption is that the register behaviour in the RTL is the same as in the netlist. SEC relaxes that because, for example, a register might be clock-gated if its input is the same as its output. For example, if a register in a pipeline is not clocked on a clock cycle, the downstream register does not need to be clocked on the next clock cycle since we know the input has not changed. In effect, the RTL has been changed. This type of optimization is common for power reduction, either done manually or by Calypto (who I think have the only automatic solution in the space). Half the bugs found in one design were from simulation but the other half came from FV. About half of the bugs found by FV would eventually have been discovered by simulation…but would have taken another 9 months of verification.
But wait, JasperGold doesn’t do sequential equivalence checking does it? No, it doesn’t but it will. NVIDIA is an early customer of the technology and have been using it on some very advanced designs to verify complex clock gating. Watch out for the Jasper SEC App.
ST Microelectronics
ST talked about how they use JasperGold for verification of low power chips. The power policy is captured in CPF and the two real alternatives to verification are power-aware RTL simulation and FV. Power-aware RTL simulation is very slow, still suffers from the well-known X-optimism or X-pessimism problem, along with an explosion of coverage due to the power management alternatives. And, like all simulation, it is incomplete.
Alternatively they can create a power-aware model, in the sense that the appropriate parts of CPF (such as power domains, isolation cells and retention cells) are all included in the model. This way they can debug the power optimization and even analyze power-up and power-down processes, in particular to ensure that no X values are propagated to the rest of the system.
Real men have fabs!