Formal validation detects late stage bugs
"Veritable's formal validation tools offer a promising way of increasing confidence that
complex high performance CPU designs function according to their specification. Veritable's Design Verity software is an important part of
our verification flow and has detected many issues. Just a few weeks from planned tape-out on a 500 MHz pipeline CPU, the
Design Verity software detected a late stage architectural bug that had been present in the design for many
months but had escaped detection by other methods." Yukio Sakaguchi, senior vice president of Design Engineering, Arcadia Design Systems Inc. Experience the power of formal validationVeritable's innovative
Design Verity formal validation tools can help you bridge the
design verification productivity gap. The usability of lint, the power of formal verification
Verity-Check, the Design Verity
static property checker, combines the usability of lint with the power of formal verification to provide you with a single high performance, high capacity property checking solution. Design Verity-Check OverviewVerity-Check is offered at three levels: i. Verity-Check Designer Level
ii. Verity-Check Professional Level iii. Verity-Check Expert Level Verity-Check Designer
The Designer Level Verity-Check product gives you the push-button ease of use of a super-lint style RTL analysis and rule-checking tool but offers sophisticated
"look-ahead" analysis techniques, which are more accurate than those used by traditional HDL lint tools, to detect hundreds of potential issues such as unsynchronised
clock domain boundary crossings, races, gated clocks, asynchronous clocks, implied latches, asynchronous sets-resets, potential glitches, redundant logic, mismatching
assignments, register-transfer level (RTL) scan DFT/ATPG issues, and X-source problems at the full-chip level. In addition, Verity-Check at the Designer Level allows
you to check for compliance to the RMM design re-usability rules, design verifiability rules and design for testability rules.
Verity-Check Professional Verity-Check at the Professional Level provides the power of formal verification
state-space search technology with the ease-of-use of rule checking. In addition to traditional lint and rule based checking, it automatically performs search-based property
checking for a set of pre-defined or built-in properties such as tri-state conflicts, floating buses, set-reset conflicts, branch possible and synchronous initialization. In addition, it
performs FSM analysis to identify unreachable and dead-end states. Search based property checking involves an exhaustive search of the design's state space to verify
that no input vector sequence exists that would result in a violation of the property. Verity-Check at the Professional Level also allows you to add your own rules using Perl. Verity-Check Expert Verity-Check at the Expert Level gives you powerful built-in property checks (such as
one-hot checks) for signals that you specify and state space search-based temporal checks of properties specific to your design (for example, a persistent request must be
acknowledged within a specified number of cycles). In addition to user specified assertion based verification checks, all checks at the designer level and professional level are included. The scalability of simulation, the power of formal verification Verity-Validation represents a new breed of dynamic property checking tool that uses static formal analysis techniques to generate a test-bench that is simulated dynamically
using a traditional logic simulator. Verity-Validation statically analyzes RTL design descriptions and automatically extracts
properties from classes of pre-defined, time-invariant, functional properties. The extracted properties are formally targeted during test-bench generation resulting in a
test-bench that is formally proven to cover targeted properties. Unlike previous "intelligent random" or simulation vector based approaches, formal state-space search,
rather than random or semi-formal, techniques are used. The new approach is deterministic and formally proves that extracted properties are covered by the test-bench. Verity-CPU, the Design Verity
processor instruction stream generator, is an innovative formal validation tool that simplifies and speeds up design verification of CPUs.
Verity-CPU combines the ease-of-use methodology of traditional biased random instruction stream generation tools and the power of formal analysis technology into a single solution, .
Experience the power of formal validation. For more information, or an evaluation, contact us at:
info@veritable.com. |
