The Cadence SMV Model Checker Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal logic properties of finite state systems, such as computer hardware designs. That means that instead of writing a simulation vectors or a simulation test bench, you verify your design for all possible input sequences. While formal verification is often equated with equivalence checking, model checking is substantially more general. It allows you to verify that that your specifications are correct very early in the design process by building abstract system level models. Its use continues through the design refinement process, allowing you to verify that your RTL level design correctly implements your high level model. How is Cadence SMV different from SMV from Carnegie Mellon? Cadence SMV is an extension of SMV from Carnegie Mellon university. It has a more expressive mode description language (though it is backward compatible with CMU SMV), and also supports synthesizable verilog as a modeling language, allowing RTL designs to be verified. In addition, Cadence SMV supports a variety of techniques for compositional verification, allowing it to be applied to large designs, with user guidance. It allows several forms of specification, including the temporal logics CTL and LTL, finite automata, embedded assertions, and refinement specifications. It also includes an easy-to-use graphical user interface and source level debugging capabilities. What can I do with SMV? You can use this free research version of SMV from Cadence Berkeley Labs to learn about model checking and its applications, and to find out some of what is going on in formal verification research at CBL. You are free to use it for research purposes, but the license agreement does not permit commercial application. If you are interested in using model checking in a production environment for your next development project, consider using Cadence's Incisive Formal Analysis (TM) tool. How does SMV relate to Incisive? Incisive Formal Analysis is a commercial offering, while SMV is a research tool. We will continue to use SMV as a research platform, for trying out new algorithms and methodologies. For this purpose, we will continue to make SMV available on the web. How can I get SMV? If you download SMV, please read the license agreement carefully. Note in particular the second paragraph of the agreement, which relates to commercial development.  After reviewing the license agreement, if you agree with its terms, complete the registration form. Make sure to select your operating system and processor configuration. The Windows version of the software is self installing and runs on PCs under Windows XP or 2000. The Unix version runs under Sparc/Solaris, Sparc/SunOS, HPUX, MIPS/Irix and i386/Linux.  Questions or comments? Send mail to mcmillan@cadence.com.  READ THE SMV LICENSE AGREEMENT THEN DOWNLOAD SMV