Cadence SMV

swMATH ID: 7795
Software Authors: McMillan K L.
Description: 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.
Homepage: http://www.kenmcmil.com/smv.html
Related Software: NuSMV; SPIN; SPOT; LTL2BA; VIS; CESAR; Uppaal; MOCHA; PRISM; MiniSat; FuncTion; Ultimate Kojak; LTLAutomizer; Ultimate; CBMC; MathSAT5; OpenSMT; AProVE; Bandera; CPAchecker
Cited in: 22 Publications

Citations by Year