The latest release of Jasper Design Automation's JasperGold formal verification suite includes the InFormal Design Analyst, a tool aimed at designer "sandbox" verification without need for development of properties or a testbench for simulation. JasperGold v4.3 also sports performance gains as well as advances in property modeling and ease of use.
A new parallel-engine, multiprocessing architecture in v4.3 maximizes verification performance. Users with fast and/or multicore machines can benefit from the ability to launch multiple proof engines, with differing and complementary strengths, on each property to be verified. The first engine to complete a proof then terminates the other engines and the process moves on to other properties.
There's also formal support for SystemVerilog local variables, which gives users a means of handling complex data and design constructs. SystemVerilog allows variables to be defined locally within sequences and properties. These local variables are then used to maintain states within the pipeline of events described by the sequence. Local variables are particularly useful for capturing and comparing the flow of transactions through the pipeline, and provide SystemVerilog users with powerful modeling capabilities that can enable transaction-level formal verification.
Without requiring any properties or even a testbench, the InFormal Design Analyst lets users statically demonstrate the behavior of their designs by manipulating automatically generated waveforms. This application of formal techniques reduces dependence on simulation and testbenches for so-called "sandbox" verification. It requires no property development or experience with formal tools.
The JasperGold v4.3 verification system is available now. The parallel-engine, multiprocessing option is priced at $25,000 for a one-year, floating time-based license. For more information, visit Jasper Design Automation.