Experience The Power of Formal Validation Is your RTL design true to specification? Veritable's Design Verity software offers high performance, high capacity design validation solutions that significantly
reduce the effort required to check. The usability of lint, the power of formal verification Verity-Check, the Design Verity property checker, is an innovative formal validation tool that simplifies and speeds up design
checking. Verity-Check uniquely combines the easy to use, almost push-button, methodology of traditional rule checking / lint tools and the power of formal verification technology into a single solution,
putting powerful property checking capability at your fingertips. Automatically extract design properties
Verity-Check quickly analyzes your RTL design code and automatically extracts numerous design properties such as
three-state bus contention, floating buses, multi-cycle register initialization, set-reset register conflicts, full case and parallel case. In addition, you can specify properties such as nets or groups of
nets that should be one hot. Verity-Check automatically verifies these design properties using sophisticated formal validation techniques that are not available in traditional lint-style tools. It performs
an exhaustive search of the design's state space using symbolic simulation and powerful constraint analysis techniques to verify that no input vector sequence exists that would result in a violation of the
property. You can set-up additional constraints to guide the search with ease using the Verity-Check graphical user interface (GUI). Verity-Check speeds up debugging by providing accurate feedback for
property violations, taking you to the source of the error in your RTL code, and automatically generating a counter example (in the form of a test bench) that proves the property is violated. Exhaustively verify specific properties Verity-Check offers powerful formal validation technology that allows you to check properties specific to your design. You can define your own properties such as:
a request must be acknowledged within a set number of cycles or that two signals must always be equivalent or complementary. The use of time-bound, cycle based, checking techniques combined with powerful
constraint analysis methods significantly increases the size of design modules that can be checked compared to current model checking techniques. Specify your properties using the Accellera PSL (Sugar)
standard, in Verilog or using the intuitive Verity-Check graphical user interface (GUI).
Extend Dynamic Assertion Based Verification Verity-Check 's formal state-space search technology can start design property
verification from any specified state, allowing you to extend your dynamic assertion based verification methodology. As in "deep dynamic" based formal verification, after running dynamic simulations to reach
interesting states, you can use these states as initial seeds from which search is started. Specifying initial states can drastically reduce the amount of search that has to be performed, so increasing
the probability that a bug will be found if it exists. Detect races before simulation
Race conditions are a major cause of critical design errors that can take significant amounts of time and effort to debug. Verity-Check's powerful
static analysis techniques reduce design debug time and effort by detecting potential race conditions before simulation and synthesis.Verity-Check identifies race conditions, such as write-write,
read-write, and combinational loop races, and automatically pin-points the lines of source code that are the cause of the race conditions. Automatically check design re-usability Verity-Check includes the following types
of traditional built-in rules checks: Reuse Methodology Manual (RMM), coding style, design for testability (DFT), simulation, synthesis, syntax, and lint. These checks help you catch errors before you
get to simulation and synthesis, and provide a way of ensuring that design teams follow a consistent design style and methodology that enables design re-use. In addition, Verity-Check allows user-defined
checks making it easy for you to add your own rules and messages to its already extensive library of built-in checks. Detect clock domain synchronization errors Verity-Check supports multiple
clock designs. Formal clock domain boundary checking ensures that data that crosses clock domain boundaries is synchronized. Verity-Check recognizes double register buffering, memory/register file and
customized synchronization schemes. For custom schemes, you can specify allowed synchronization cells. Verity-Check also identifies data that is generated and consumed by different edges of the same clock
and checks for the appropriate use of lock-up latches. Automatically analyze FSMs Verity-Check analyzes your RTL code and automatically extracts finite-state machines (FSMs), without requiring user directives. You can
check for terminal or dead-end state, self-loop terminal states and unreachable states. You can also verify that all expected state transitions occur and that illegal state transitions do not happen. Enforce your design methodology
Verity-Check's support for user re-configurable rules and rule packages allows you to customize rule packages that address your design checking requirements. Predefined packages simplify the enforcement of
design methodologies such as design for re-usability, design for testability and design for verifiability. You can also add your own rules using Perl. Find design for testability errors at RTL stage Verity-Check allows you to check
that your RTL complies with design for testability (DFT) rules so reducing the amount of time and effort spent at the gate level finding and fixing scan DFT violations. You can perform scan-path integrity
and ATPG checks, and you can check that your JTAG 1149.1 boundary scan test controller or custom test controller operates correctly, all at the register transfer level before you synthesize to gates.
Eliminate design errors earlier Verity-Check eliminates complex design errors at all stages of your design implementation cycle from RTL to gate level, from module level to full chip. Deploy
Verity-Check early in your design cycle to drastically reduce the amount of effort you spend finding bugs later using time-consuming traditional test-bench methods. |
