North Billerica, Mass.--Feb. 23, 1998--Chrysalis Symbolic Design, Inc. (North Billerica, Mass.) announced the industry's first commercial, full-chip formal design solution. With the release of Chrysalis's new Design Insight Assertions for model checking and full-chip equivalence checking enhancements for Design Verifyer, users can begin to "formalize" their design methodology in a practical, incremental way.
The Chrysalis family of formal design products gives customers the benefits of leading-edge formal point tools, tightly-integrated for a front-to-back formal designflow. The newly-announced Design Insight Assertions provides practical model checking for on-chip interfaces and protocols. The latest enhancements in Design Verifyer 2.3 provide full-chip RTL-to-gate hierarchical verification along with dramatic speed-ups in verification time and reductions in memory. And because Assertions works directly with Design Verifyer, engineers can move directly from designing their RTL withthe benefits of formal model checking, to verifying their gate- or switch-level implementations with equivalence checking--eliminating the need to perform gate-level functional simulation.
The Chrysalis full-chip formal design solution is a family of products that share a common database, design readers, and user interface. They also share a common method for describing design properties, which can be used both as proofs and as assumptions.
Design Insight is a family of modular products that work together for RTL design and verification. The newest module is Design Insight Assertions, a practical model checking solution for on-chip interfaces and protocols in ASIC and IC designs.
Design Verifyer 2.3 brings independent production proven equivalence checking to the full-chip level. With Design Verifyer 2.3, users can automatically perform full-chip RTL-to-gate equivalence checking on hierarchical designs, thus eliminating the need to use functional gate-level simulation.
Formal Design applies mathematical design approaches to accelerate the design and verification of complex IC's and ASICs. With traditional designmethods, users convert their top-level specification into an RTL design and a set of simulation vectors, which should show that the RTL produces the samebehavior as in the specification. With Formal Design, the specification also gets mapped into design properties. The properties capture key parts of the spec--such as: "the read and write signals should never be on at the same time." These properties serve two purposes. First, they can then be used to test the RTL design using model checking. Second, they can be used as assumptions to direct equivalence checking as part of a logic module-by-logic module hierarchical approach. This allows the designer to very rapidly create gates or switches and verify that they still preserve the intent of the original specification.
Chrysalis Symbolic Design
Return to Headlines