If there’s ever been a knock on formal verification, it’s the
amount of time it takes to do a formal run on a full design.
Formal tools can only take in so much design data at a given
time, forcing design teams to partition the design for formal
analysis. Sure, it’ll find bugs that can’t be found any other way,
but it can take quite a while to accomplish.
In the latest revision of its flagship tool, JasperGold, Jasper
Design Automation has made strides in capacity that alleviate
those concerns. Version 5.0 of the JasperGold Verification System
incorporates new core engines that provide for a tenfold
speedup compared with earlier versions. This translates into
three times more state-space capacity, which is further fueled
by a two-times reduction in memory requirements.
Taking in either Verilog or SystemVerilog, JasperGold uses its
enhanced capacity to provide improved and interactive designspace
exploration or, as Jasper terms it, “tunneling” (see the
figure). Whereas traditional formal technologies work within
a given state space, or “cone of influence,” JasperGold looks
within the state space for the specific logic that matters to the
property being proven. Doing so requires tight integration with
formal engines, and Version 5.0 has been specifically tooled for
that integration.
In addition to its capacity and memory requirement improvements,
Version 5.0 of JasperGold can handle SystemVerilog
Assertions-like temporal expressions on its command line. This
lets users add on-the-fly constraints during simulation without
having to quit the tool and reload it.
One-year, time-based licenses range from about $60,000 for
the bare-bones JasperGold Express to $217,500 for the fully
loaded JasperGold system. The tool is available now.
JASPER DESIGN AUTOMATION
www.jasper-da.com
