Cadence SMV

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.

References in zbMATH (referenced in 23 articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Koo, T.John; Li, Rongqing; Quottrup, Michael M.; Clifton, Charles A.; Izadi-Zamanabadi, Roozbeh; Bak, Thomas: A framework for multi-robot motion planning from temporal logic specifications (2012)
  2. Rozier, Kristin Y.: Linear temporal logic symbolic model checking (2011)
  3. Chen, Mingsong; Mishra, Prabhat; Kalita, Dhrubajyoti: Efficient test case generation for validation of UML activity diagrams (2010) ioport
  4. Rozier, Kristin Y.; Vardi, Moshe Y.: LTL satisfiability checking (2010) ioport
  5. Calder, M.; Miller, A.: An automatic abstraction technique for verifying featured, parameterised systems (2008)
  6. Clarke, Edmund; Talupur, Murali; Veith, Helmut: Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems (2008)
  7. Gupta, Anubhav; McMillan, K.L.; Fu, Zhaohui: Automated assumption generation for compositional verification (2008)
  8. Feng, L.; Wonham, W.M.; Thiagarajan, P.S.: Designing communicating transaction processes by supervisory control theory (2007)
  9. Loer, Karsten; Harrison, Michael D.: An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation (2006) ioport
  10. Pan, Hong; Lin, Hui-Min; Lv, Yi: Model checking data consistency for cache coherence protocols (2006) ioport
  11. Tverdyshev, Sergey: Combination of Isabelle/HOL with automatic tools (2005)
  12. Barbuti, Roberto; Bernardeschi, Cinzia; de Francesco, Nicoletta: Analyzing information flow properties in assembly code by abstract interpretation (2004)
  13. Chou, Ching-Tsun; Mannava, Phanindra K.; Park, Seungjoon: A simple method for parameterized verification of cache coherence protocols (2004)
  14. Lahiri, Shuvendu K.; Bryant, Randal E.: Indexed predicate discovery for unbounded system verification (2004)
  15. Win, Toh Ne; Ernst, Michael D.; Garland, Stephen J.; Kırlı, Dilsun; Lynch, Nancy A.: Using simulated execution in verifying distributed algorithms (2004) ioport
  16. Zuck, Lenore; Pnueli, Amir: Model checking and abstraction to the aid of parameterized systems (a survey) (2004)
  17. Glusman, Marcelo; Katz, Shmuel: Model checking conformance with scenario-based specifications . (2003)
  18. Bjesse, Per; Leonard, Tim; Mokkedem, Abdel: Finding bugs in an alpha microprocessor using satisfiability solvers (2001)
  19. Kwiatkowska, Marta; Norman, Gethin; Segala, Roberto: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM (2001)
  20. Plath, Malte; Ryan, Mark: Feature integration using a feature construct (2001)

1 2 next