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. Incisive Formal Verifier exposes coverageassociated functional problems that cannot be found using simulation, acceleration, or emulation, and it gives you a complete coverage picture. months before meaningful testbench simulation begins. With this approach, functional bugs are detected much earlier in the design cycle and are easier to fix at a significantly lower cost. [. . . ] Cadence, the Cadence logo, Conformal, Incisive, and SourceLink are registered trademarks and Encounter is a trademark of Cadence Design Systems, Inc. SystemC is a registered trademark of Open SystemC Initiative, Inc. in the United States and other countries and is used with permission. [. . . ]