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