User manual CADENCE DESIGN SYSTEMS INCISIVE FORMAL VERIFIER DATASHEET

[. . . ] INC I S I VE FO R M A L VE R I FI E R DATASHEET INCISIVE VERIFICATION PLATFORM The functional verification of nanometerscale ICs requires speed and efficiency. Yet today's fragmented methodologies make it impossible to optimize either. Each verification stage has its own methodology, tools, models, and user interface. [. . . ] The net result is a significant gain in productivity, which minimizes the risk of re-spins, improves design quality, and accelerates time-tomarket. A AA A AA A A A AA AA AA AA A A A A A A AA A A A AA AA A AA AA A A AA A A A AA A A A A · Simulation · Acceleration · Emulation Integrated design AA AA A A A A AA · Formal analysis · Simulation · Acceleration Cluster/block A A AA AA AA · Formal analysis Block/module Figure 2: Formal analysis at the entry point of the Incisive platform's complete assertion-based verification flow · Providesdesignteamswithanadvanced debug environment with simulation synergies for ease-of-adoption FEATURES LEADING-EDGE FORMAL ENGINES WITH SMART AUTOMATION A set of complementary, state-of-art formal engines from production-proven technologies and world-renowned researchers combine to deliver the industry's highest performance and capacity. To ensure ease-of-use and maximize performance, a strategy engine automates the engine selection process by selecting optimal engines for each run. To optimize formal analysis performance even further, built-in distributed processing allows you to leverage the broad engine assortment by running them in parallel for multi-fold performance gains. your company. Using mature and robust front-end parsers proven on thousands of designs provides you with improved reliability when deploying Incisive Formal Verifier into your flow. BROAD ASSERTION SUPPORT AND INTEROPERABILITY Incisive Formal Verifier supports the same set of assertions as Incisive simulation, acceleration, and emulation support. This includes assertions written in Property Specification Language (PSL), SystemVerilog Assertions (SVA), Open Verification Library (OVL), and the open source Incisive Assertion Library (IAL). BENEFITS · Speedstime-to-marketwithlowerrisk and higher predictability · Increasesproductivitybyenabling verification to start months earlier, before testbench development and simulation · Improvesqualityandreducesriskof re-spins by exposing corner-case functional bugs that are difficult or impossible to find using conventional methods · Reducesblockdesigneffortanddebug time, and shortens integration time AUTOMATIC ASSERTION EXTRACTION Incisive Formal Verifier automates assertion creation for common design structures, with the extraction of assertions for FSM states and arcs, branching deadcode, and synthesis pragma assumptions. Such automation of the simpler assertions allows you to focus on design-specific assertion creation, maximizing your productivity while at the same time ensuring that all functional problems related to common design structures are exposed automatically. BROAD DESIGN LANGUAGE SUPPORT Incisive Formal Verifier provides extensive design language support, including Verilog®, SystemVerilog, VHDL, and mixedlanguage, to leverage formal analysis across all design teams and groups within www. ca de nce . com I NC I SI VE FO RMAL VERI FI ER 2 SIMULATION SYNERGY Incisive Formal Verifier integrates seamlessly with Incisive Unified Simulator and works great with third-party simulators as well. The Incisive platform environment uses common parsers, assertions, linting, analysis, coverage, and debug. Moreover, Incisive Formal Verifier has built-in initialization capabilities for blocklevel verification. It also leverages the industry-standard VCD interface, supported by all simulators, to use simulation traces when deep or complex initialization is required. COMPREHENSIVE, EASY-TOUSE 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 the Incisive Unified Simulator and similar to 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. When Incisive Formal Verifier detects an assertion violation, it generates a simulated counter-example waveform for easy debugging. You can also generate a simple testbench for use in any simulator to validate the exposed functional bug or for regression runs. Together, these capabilities allow design teams to instantly deploy and use Incisive Formal Verifier in their production flows. Figure 3: Incisive Formal Verifier provides advanced debug and diagnostics features common to simulation for ease-of-use and ease-of-adoption of formal analysis Incisive Formal Verifier includes another set of capabilities, including reachability analysis to verify simulation coverage holes. Synergy exists for functional coverage using assertions and for code coverage constructs such as FSM states, FSM arcs, and branching deadcode. [. . . ] Formal analysis is deployed at the beginning of the verification flow as the designers write RTL and assertions -- COMPLETE FORMAL COVERAGE Users of formal analysis software frequently need to find out if they have written sufficient assertions to verify the design blocks, to understand how much has been formally verified, and to determine the proof radius. Incisive Formal Verifier supports all these features to ensure efficient verification. SPECIFICATIONS DESIGN LANGUAGE SUPPORT · Verilog(IEEE1364-1995, IEEE 1364-2001) · SystemVerilog(IEEE1800) · VHDL(IEEE1076-1987, IEEE 1076-1993) · Mixed-languageenvironments www. ca de nce . com I NC I SI VE FO RMAL VERI FI ER 3 ASSERTION LANGUAGE SUPPORT · PropertySpecificationLanguage(PSL) · SystemVerilogAssertions(SVA) INTERFACES · Tclcommandinterface · VCDandSST2interfaces · Compilesupto30Mgatesperhouron a single workstation · Expandableto256Mgates · Allowsupto32simultaneoususers · LeaderinmicroprocessorandIPsupport ASSERTION LIBRARY SUPPORT · OpenVerificationLibrary(OVL) · IncisiveAssertionLibrary(IAL) PLATFORMS · SunSolaris · HP-UX · Linux RELATED PRODUCTS ENCOUNTERTM CONFORMAL® EQUIVALENCE CHECKER · Equivalencecheckingcapability · Clockdomaincrossingchecks HDL ANALYSIS · 500+checkstolintandanalyze ­ Synthesizability ­ Race conditions ­ Code reusability ­ FSM coding ­ Verilog, VHDL, and mixed-language support ­ Design subset INCISIVE PRODUCT LINE-UP INCISIVE UNIFIED SIMULATOR · Unifiedsimulatorwithheterogeneous single-kernel architecture · NativeVerilog, SystemVerilog, VHDL, and SystemC® support · NativeSystemCVerificationLibrary · PSL, SVA, andOVLsupport · Fast, unifiedtestgeneration · AccelerationpolicychecksandHDLanalysis · Unifiedsimulationanddebug environment · Unifiedkernelsupportsanalog/mixedsignal and algorithm design ENCOUNTER CONFORMAL CONSTRAINT DESIGNER · Functionalvalidationandgenerationof design constraints RESULT ANALYSIS · DebugandGUI ­ Assertion manager ­ Waveform viewer ­ Source code browser ­ Source code value annotation ­ Driver and receiver tracing ­ Vacuity and sanity checks ­ Assertion triggering · Reporting ­ Status and proof radius reporting ­ Assertion coverage reporting ­ Formal coverage reporting ­ Cone-of-influence analysis CADENCE SERVICES AND SUPPORT · Cadenceapplicationsengineerscan answer your technical questions by telephone, email, or internet-they can also provide technical assistance and custom training · SourceLink® online customer support gives you answers to your technical questions--24hoursaday, 7daysa week -- including the latest in quarterly software rollups, product release information, technical documentation, software updates, and more · Cadencecertifiedinstructorsteachmore than80coursesandbringtheirrealworld experience into the classroom · Morethan25InternetLearningSeries (iLS) online course allow you the flexibility of training at your own computer via the Internet INCISIVE PALLADIUM FAMILY OF ACCELERATORS/EMULATORS · Simulationaccelerationandin-circuit emulation in one system · Providesupto100x-10, 000xRTL performance ·Assertion-basedacceleration · Run-timeperformancewithupto 750KHzspeed For more information, contact Cadence sales at: 1. 800. 746. 6223 or log on to: www. cadence. com © 2005 Cadence Design Systems, Inc. Cadence, the Cadence logo, Conformal, Incisive, and SourceLink are registered trademarks and Encounter is a trademark of Cadence Design Systems, Inc. [. . . ]