|
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 advanced formal engines with the strengths of a built-in VCS® simulation engine to verify properties on large and complex Verilog and VHDL designs.
- Key Benefits
- Increases design quality by finding corner-case design bugs, early in the verification cycle
- Raises verification productivity by enabling reuse of assertions between simulation and formal verification
- Easy to use with built-in checker library of frequently used assertions
- Increases verification confidence by proving complex properties
- Finds hard-to-reach bugs and proves properties with built in VCS engine and formal engines
- 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
Challenges
Control-logic blocks such as arbiters, memory/cache controllers, resource allocation algorithms, and bus controllers that have complex data-transport functionality are becoming larger, more complex, and harder to verify. These blocks have corner-case behaviors that traditionally have been hard to define and exercise, leading to bugs that elude the most sophisticated simulation-based and emulation-based verification methods.
Although formal techniques have been applied somewhat successfully to these blocks in the past, capacity and ease-of-use limitations have prevented formal tools from delivering the benefits expected by mainstream users.
Solution
Magellan delivers higher-capacity formal property verification for SystemVerilog, Verilog, and VHDL designs by employing a unique hybrid architecture. This architecture combines the ability of the VCS simulation engine to rapidly reach deep into the design with advanced formal engines to perform exhaustive analysis and either prove design behavior or expose deep, corner-case bugs. Magellan fits easily into a verification environment by reusing assertions currently running in dynamic simulation or using custom assertions written by the user. Assertions can be written in Verilog, VHDL, Open Verification Library (OVL), OpenVera™ Assertions (OVA) or SystemVerilog Assertions (SVA) and are verified by Magellan without manual intervention. Additionally, Magellan can also use assertions from OVA and SVA checker libraries.
Related Products
For more information about this product, please contact your local Synopsys representative or call 1-800-388-9125.
Back to Discovery Verification Platform.
|
