Magellan 

Hybrid RTL Formal Verification 

Overview
Magellan™ is a hybrid RTL formal verification product that allows engineers to find deep, corner-case bugs, quickly, resulting in shortened functional verification cycles and high-quality designs. Magellan’s unique hybrid architecture combines the strengths of new, advanced formal engines with the strengths of a built-in VCS® simulation engine to verify properties on large and complex designs.

Key Benefits
  • Increases design quality by finding
  • corner-case functional bugs
  • Reduces verification cost by finding functional bugs early in the verification cycle
  • Raises verification productivity by enabling reuse of assertions between dynamic and formal verification environments

    Key Features
    • High-capacity formal verification using hybrid architecture
    • Formal verification of user-specified properties
    • Formal verification of automatically extracted structural properties
    • Elimination of false-negative errors
    • Support for hierarchical verification of assertions

      Figure 1. Property verification using Magellan
      Figure 1. Property verification using Magellan

      Finding Bugs on Large Designs
      Magellan performs hybrid RTL formal verification by using a built-in VCS simulation engine that reaches deep into the design and uses multiple formal engines to verify whether or not the design satisfies a given set of properties. This enables engineers to find deep corner-case bugs. Traditional formal verification products only use formal engines to find bugs and hence are useful only for very small designs. Moreover, Magellan utilizes its built-in VCS engine to reach deep into large designs quickly, while performing formal analysis to find design bugs. This automatic and transparent orchestration between VCS and formal engines enables Magellan to work efficiently on large designs.

      Figure 2. Magellan’s hybrid architecture
      Figure 2. Magellan’s hybrid architecture

      Eliminating False-Negative Errors
      False-negative errors are caused when formal tools report design bugs that cannot be reproduced in target-operating conditions of the design. For example, a traditional formal tool could report a design bug based on analysis from an incorrect initial state of the design. Magellan eliminates false-negative errors. It ensures that violations detected by its formal engines can be reproduced in real-life operating environments by automatically verifying them with the built-in VCS engine before reporting the violation. This prevents the need for an engineer to manually verify false-negative reports and further raises verification productivity.

      Table 1. List of automatically extracted properties
      Table 1. List of automatically extracted properties

      Formal Verification of Properties
      Magellan formally verifies user-specified properties or automatically extracted properties for a given design. In addition to the RTL, the user may provide assertions and assumptions for the design. Magellan’s formal analysis will yield one of the following outcomes.

      • Proven. Guarantees correct behavior of the design for the given assertion and input assumptions.
      • Falsified. Represents a scenario in which the design violates the given property. Magellan creates a debug trace that can be simulated and verified by an engineer.
      • Inconclusive. The property could neither be proven nor falsified. This property can be used in dynamic simulation as a monitor. It could also be formally verified to be true or false in a time window.

      Figure 3. Assumptions used at block level verification
      Figure 3. Assumptions used at block level verification with Magellan

      Figure 4. Reuse of block-level assumptions as chip-level monitors
      Figure 4. Reuse of block-level assumptions as chip-level monitors

      Advancing Design-for-Verification Methodology
      Magellan advances design-for-verification (DFV) methodology supported by Synopsys’ Discovery™ Verification Platform. Properties and assumptions used with Magellan can be reused as monitors in a dynamic-verification environment, with Synopsys’ VCS and Pioneer-NTB products. Also, assumptions written for verifying a design block with Magellan can be used as assertions for verification of the succeeding block. This ensures that assumptions made during verification of a block are further validated and guaranteed to be true for the design.

      Synopsys Discovery Verification Platform
      The Discovery Verification Platform is a unified environment that provides high performance and efficiency of interaction among all platform components, including mixed-HDL simulation, mixed-signal, system-level verification, assertions, DesignWare verification IP, code coverage, functional coverage, testbenches and formal analysis. Combined with support for industry-standard hardware design and verification languages, including Verilog, VHDL, SystemVerilog, SystemC and OpenVera, and Synopsys’ proven VMM methodology, the Discovery Verification Platform helps designers achieve higher levels of verification productivity by contributing to first-time silicon success within required project cycles.

      Language Support
      Magellan can be used to verify design RTL written in SystemVerilog, Verilog or VHDL. For maximum flexibility, properties and assumptions can be specified in SystemVerilog, OpenVera Assertions, Verilog or VHDL. Magellan can also use the predefined checks from the Open Verification Library.



      NewsArticlesBlogsSuccess StoriesWhite PapersWebinarsVideosTraining Courses