Formal Scoreboard, Model RAM, and Model Multiplier Proof Accelerators
Jasper Design Automation launched three new Proof Accelerators: Formal Scoreboard, Model RAM, and Model Multiplier. Proof Accelerators increase the power, the capacity and the performance of formal verification by significantly reducing the state-space of a design through optimized modeling of common design functions. Proof Accelerators are ideal for data transfer integrity, FIFO and memory modeling, data synchronization across clock domains, and cache verification.
Formal Scoreboard 2
The latest version of Formal Scoreboard is used to prove the integrity of data transfers across a design. Its multiple input and output ports make it possible to verify many different types of data transfers, such as transfers relying on byte enables and bus-width conversion, or serial-to-parallel conversion. To further improve performance and usability, Formal Scoreboard 2 has an updated and more versatile user interface.
Model RAM
Model RAM makes memories tractable, providing a means of achieving full, unbounded proofs on properties that involve logic containing memories. It achieves this goal by providing a flexible abstraction that enables the formal engines to abstract the majority of the specified memory while preserving those parts of its behavior that are needed to achieve the proof.
Model Multiplier
Multiplier verification can affect the state-space of a design, but this component provides a “formal safe” method for modeling multipliers ideally suited for complex designs such as DSPs and graphics/video/network processors.
More info: About Jasper Design Automation
If you are familiar with RSS feeds, you can also sign up for our free blog feed. Our RSS feed is updated in real-time while our newsletter is updated daily.