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

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

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

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 with Magellan

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.