Because formal tools examine the state space of your logic design they can run a long time and take up lots of RAM, so Jasper did something about it. Today they announced support for multi-core CPUs, clusters and networked computers with a feature called ProofGrid inside a new product named JasperCore. JasperCore is used by both JasperGold and ActiveDesign products.
You’ll see reduced run times when using up to 64 licenses. Pricing is not published so you’ll have to contact your Jasper account manager directly to get updated pricing and packaging numbers. I’m a big fan of full disclosure for EDA tool pricing.
From an RTL designer point of view I was also impressed with their ActiveDesign tool because it really helps a designer see the behavior of a new block by viewing familiar waveforms, then creating assertions for me. This new feature is called QuietTrace.
In formal verification I think that Jasper is still the market leader, or gorilla vendor with this new release. If you go to DAC then check out their suite, papers and activities.