- Takes a “formal first” approach, so properties and subsequent verification is truly exhaustive vs. simulation-based approaches
- Allows the capture of register specifications in familiar textual formats
- Expedites debug using absolute minimum-length waveforms to show erroneous behaviors
Enhanced with a customized GUI for results analysis, the JasperGold® Control & Status Register App allows the specifications of control and status register (CSR) configurations and behavioral descriptions in open, familiar formats–either Excel and OpenOffice spreadsheets, common-separated values (CSV) files, or an IP-XACT xml. You won’t need to know or learn SystemVerilog Assertions (SVA). In a matter of hours, the app then automatically generates register checks from the definition table, and proceeds to exhaustively verify that the register-transfer level (RTL) implementation of the registers behaves as specified. Using this app, you’ll be able to find deep bugs weeks and months sooner than simulation-based flows can.
A modern system on chip (SoC) has a large number of CSRs—even small intellectual property (IP) blocks can have hundred(s) of such registers. Writing testbenches to verify even the most basic read/write behaviors is a time-consuming chore that doesn’t scale easily. While some engineers may think it is straightforward to verify read operations and write operations to a CSR, the verification complexity increases exponentially when advanced features are used, such as register aliasing, bit masks and byte enable, concurrent hardware and software accesses, access latencies, register remapping according to operation modes, protected vs. unprotected transactions, locking conditions, modified write semantic, and read actions.
The JasperGold Control & Status Register App automatically generates properties capturing the complex semantic related to register interactions, latencies, and read/write semantics, designed such that you won’t have to learn formal or SVA. The properties the tool automatically generates are optimized for formal, providing faster wall clock runtime and better proof performance. When used in concert with our Visualize™ and QuietTrace™ technologies, debug is significantly easier and faster.
- Ability to create and edit register specifications in open, human, and machine-readable Excel/OpenOffice spreadsheets, CSV files, or IP-XACT xml files
- Enables productivity and throughput by allowing multiple proofs to be kicked off in parallel with ProofGrid, while proof jobs can be managed and tracked using ProofGrid Manager in a regression mode