User manual CADENCE DESIGN SYSTEMS INCISIVE ENTERPRISE VERIFIER DATASHEET

[. . . ] Additionally, with the ability to automatically translate formal results into dynamic simulation terms, Incisive Enterprise Verifier seamlessly combines the strengths of each technology in true a metric-driven verification flow. Since Incisive Enteprise Verifier does not require a testbench, you can bring up your design much sooner and begin verification months earlier when designing RTL blocks. It also provides support for metricdriven verification across the enterprise, with verification planning, regression With dual power from integrated formal analysis and simulation engines, Cadence® Incisive® Enterprise Verifier allows designers, formal verification experts, and dynamic simulation verification engineers to bring up designs faster, begin bug hunting earlier, and gather more metrics toward verification closure by simultaneously leveraging SVA, PSL, code, and functional coverage analysis. Verification Environment "vPlan" Executable Specification Assertion-Based Verification IP Multi-Language, IEEE Standard Testbench and Libraries Applications Incisive Enterprise Verifier - XL Desktop Manager Plan-Driven, Multi-Run Control with Total Coverage Analysis Multiple solvers, distributable across multiple CPU cores e, Verilog, VHDL, SystemC, SystemVerilog, PSL, OVL, SVA Simulation Code, Assertion, Functional, and Transaction Coverage Dual-Engine Integration Assertion-Driven Simulation, Guide Pointing, Search Pointing, Cover Point Targeting, Automatic Formal Analysis Sim Vision Formal Analysis Engines Specman and Simulator Core Constraint-Driven Test Generation Single Run Data & Assertion Checking UVC Builder, HDL Analysis, and Lint Witness Tracing, Debug, and Analysis Device Under Test HDLs Assertions Embedded Software Incisive Acceleration and Emulation Figure 1: Incisive Enterprise Verifier combines unique multi-engine formal and dynamic simuation capabilities with Incisive Formal Verifier, Incisive Enterprise Simulator XL, SimVision, Desktop Manager, and built-in support for assertion-based verification, the Universal Verification Methodology, and metric-driven verification operations on server farms, consolidated formal and simulation metrics, and multicore performance capabilities The pure formal verification engines inside Incisive Enterprise Verifier use the industry's most advanced formal analysis technology to offer teams superior performance, capacity, and ease of adoption, which leads to reduced block debug and integration time. [. . . ] Incisive Enterprise Verifier then uses formal analysis to hit these intermediate states (guide points) specified in sequence. In effect, guide points are a sequence of covers, where the tool proves reachability to each guide point. As each guide point is hit, the design is initialized by simulation to this state to start exploration to hit the next guide point in the sequence. Once the final guide point is hit, Incisive Enterprise Verifier formally explores all the active assertions present in the environment. auToMaTIC FoRMal aNalySIS Incisive Enterprise Verifier's automatic formal analysis capability automatically extracts from the design common assertions that can easily be overlooked or that are just plain tedious to write by hand. Either way, because the checks are automatically created, they are generated consistently across the entire RTL code base, and the correctness of the assertions is guaranteed. The bonus here is that no time will be required to debug these assertions themselves. Instead, you are free to focus solely on debugging failures or incorrect RTL behavior. Anyone on a design or verification team can and should run automatic formal analysis on all designs in the same way you run code coverage in dynamic simulations; i. e. , just turn it on and let the machine do the work. It's a simple and low-effort verification activity that can catch bugs "for free. " aSSERTIoN-dRIVEN SIMulaTIoN The same assertions used in formal analysis can be automatically reused by Incisive Enterprise Verifier to generate new dynamic simulation stimulus for the design. You can replay these automatically generated HDL tests--in effect, a "synthetic testbench"--to recreate the assertion or failure behavior using dynamic, simulation-based ABV. CoVER PoINT TaRGETING This capability is a unique application of Incisive Enterprise Verifier`s constraint solver and formal engines in combination with dynamic simulation. Users can select a cover point of interest, the formal engines figure out an optimal way to reach the selected state, and then Incisive Enterprise Verifier automatically creates and drives required stimulus back into the simulator. This speeds verification of designs faster than possible with the traditional application of trivial directed tests. SEaRCh PoINTING With search pointing, you can run a dynamic simulation to a point of interest and then apply the formal engines to explore the state space from that point in time. This process can be repeated to alternate runs of simulation and formal analysis. This enables verification of much larger designs/state spaces than possible with standalone formal methods. lEadING-EdGE FoRMal ENGINES WITh SMaRT auToMaTIoN A combination of complementary, state-of-the-art formal engines from production-proven technologies and world-renowned researchers deliver the industry's highest performance and capacity. To optimize formal analysis performance even further, built-in www. cadence. com INCISIVE ENTERPRISE VERIFIER 3 distributed processing allows you to leverage the broad engine assortment by running them in parallel for multi-fold performance gains. BRoad aSSERTIoN SuPPoRT aNd INTERoPERaBIlITy Incisive Enterprise Verifier supports the same set of assertions as Incisive simulation, acceleration, and emulation tools support. This includes assertions written in Property Specification Language (PSL), SystemVerilog Assertions (SVA), Open Verification Library (OVL), and the open source Incisive Assertion Library. Incisive Enterprise Simulator XL, the engine behind Incisive Enterprise Verifier's dynamic simulation capabilities, supports all IEEE-standard languages. SIMVISIoN dEBuG aNd aNalySIS ENVIRoNMENT An integrated GUI environment and Tcl interface provides you with an easy-toadopt debug and analysis environment-- the same as that in Incisive Enterprise Simulator XL, and similar to that of other simulators. The complete environment includes built-in linting, waveform viewing with source code linking, source code value annotation and tracing, structural analysis, vacuity and sanity checks, coverage reporting, and overall verification management. [. . . ] All scenarios are written out into a reusable format, supporting the creation of portable libraries of protocol Comprensive standards support · Supports all IEEE-standard languages and interfaces, enabling full legacy and third-party IP usage · Supports the Si2 Common Power Format (CPF), an open specification language that captures all powerspecific design intent aSSERTIoN SuPPoRT · PSL and SVA (the IEEE-standard assertion languages) · Open Verification Library (OVL) · e testbench assertions · Incisive Assertion Library (included) · Common compile and elaboration mechanism with the Incisive platform INCISIVE ENTERPRISE SIMulaToR Xl FEaTuRE hIGhlIGhTS hETERoGENEouS SINGlE-KERNEl aRChITECTuRE The Incisive heterogeneous single-kernel architecture enables unified simulation through behavioral, transaction, register- www. cadence. com INCISIVE ENTERPRISE VERIFIER 5 · Common user interface with the Incisive platform · Dynamic assertion evaluation ­ Natively compiled with HDL for highest performance ­ Can be embedded in the HDL or in separate file(s) ­ Recorded as transactions for direct display in waveform window ­ PSL and SVA assertions treated as first-class simulation objects for easy debugging SIMulaToN aNd MIXEd FoRMal/ SIMulaTIoN RESulTS aNalySIS · Debug and GUI ­ Waveform window ­ Register window ­ Unified transaction/signal viewing ­ Schematic tracer ­ Expression calculator ­ Signal flow browser ­ Source viewer ­ Error browser ­ Tcl/Tk scripting for customizable displays ­ Log signal and transaction data to SST database · Performance analysis software outlines areas of code where most simulation time is spent · Code coverage ­ Supports Verilog, SystemVerilog, VHDL, and mixed-language designs ­ Automatic FSM extraction ­ Coverage attributes supported include blocks, paths, expressions, variables, gates, FSM (states, sequences), and toggle ­ Coverage reuse ­ Rank order coverage contributions ­ Bit-wise expression scoring · Functional coverage analysis ­ Supports Verilog, SystemVerilog, VHDL, e, SystemC, SCV, PSL, SVA, and OVL ­ Logs data to SST2 database ­ Tcl/Tk scripting for custom analysis hdl aNalySIS · 500+ checks to lint and analyze code for: ­ Synthesizability ­ Race conditions ­ Code reusability ­ Clock domain synchronization ­ FSM coding ­ Acceleration policy checks · Gate-level netlist analysis for any DFT errors introduced during synthesis · Verilog, SystemVerilog, VHDL, and mixed-language support · Powerful customization capability using VPI/VHPI · Graphical interface to sort, filter, and analyze messages with source code dyNaMIC SIMulaTIoN · Single-kernel simulation engine ­ Verilog (IEEE 1364-1995 and IEEE 1364-2001 extensions) ­ SystemVerilog (IEEE 1800) ­ e (IEEE 1647) ­ VHDL (IEEE 1076-1987, IEEE 10761993, IEEE 1076. 4-2000 (VITAL 2000)) ­ SystemC (IEEE 1666, OSCI SystemC v2. 2) ® e TESTBENCh aNalySIS · 200+ checks to lint and analyze code for: ­ Code reusability as per Universal Reuse Methodology (URM) compliance rules ­ Performance analysis ­ Race conditions ­ Pre-defined coding style rules ­ Generation constraints · Graphical interface to sort, filter, and analyze messages with source code ­ PSL (IEEE 1850) ­ SVA (IEEE 1800) ­ CPF · Compile ­ Native compilation technology goes directly to host processor machine code, which maximizes performance ­ Intelligent incremental compile reduces compile times · Capacity ­ Typical 10M gate equivalents in 32-bit OS (4GB addressable) ­ Typical 100M gate equivalents in 64-bit OS · Server farm ­ Platform computing LSF ­ Sun Microsystems Gridware VERIFICaTIoN BuIldER · GUI support for configuration of UVM-compliant Universal Verification Components (UVCs) · Outputs UVCs in either e (IEEE 1647) or SystemVerilog (IEEE 1800) www. cadence. com INCISIVE ENTERPRISE VERIFIER 6 CadENCE IP SuPPoRT · Design IP ­ Functional Verification Kit for ARM® processor-based designs · Verification IP (VIP) ­ Supports assertion-based VIP included in the Cadence VIP portfolio ­ Supports all simulation-based UVCs, transaction-based VIP, assertionbased VIP, and SpeedBridge® rate adapters used in emulation ­ Supports the full portfolio of Cadence UVCs* *Cadence UVCs include a comprehensive Compliance Management System that leverages vPlans to exhaustively verify protocol compliance. INTERFaCES · Tcl command interface · PLI (IEEE 1364) · DPI (IEEE 1800) · VPI (PLI 2. 0, IEEE 1364) · OMI (IEEE 1499) · VHPI · Compiled SDF · VCD and SST2 interfaces CadENCE SERVICES aNd SuPPoRT · Cadence application engineers can answer your technical questions by telephone, email, or Internet--they can also provide technical assistance and custom training · Cadence certified instructors teach more than 70 courses and bring their real-world experience into the classroom · More than 25 Internet Learning Series (iLS) online courses allow you the flexibility of training at your own computer via the Internet · Cadence Online Support gives you 24x7 online access to a knowledgebase of the latest solutions, technical documentation, software downloads, and more PlaTFoRMS · Sun Solaris · Linux ThIRd-PaRTy SuPPoRT · ASIC libraries ­ 30+ ASIC vendors have certified their libraries for the Incisive platform ­ 150+ unique libraries · Models ­ Third-party model support through the Cadence VIP partner program · Software ­ Third-party software support through the Connections® program with 30+ verification company partners © 2010 Cadence design Systems, Inc. Cadence, the Cadence logo, Connections, Incisive, Palladium, SpeedBridge, and Verilog are registetred trademarks of Cadence design Systems, Inc. aRM is a registered trademark of aRM ltd. [. . . ]