Embedded systems are becoming increasingly popular due to their widespread applications.  With formal verification we verify that every possible behavior of the target system satisfies the specification. SMV is a formal verification system for hardware designs, based on a technique called "symbolic model checking".  In this report we investigate the modeling and verification of an embedded system using Cadence SMV. We constructed a Verilog model of the system by integrating the microcontroller RT level and the embedded software assembly code level. We then validate our models and verification by conducting model checking which analyzes essential aspect of the target embedded system.

Download postscript file (PS File)

Download PDF file (PDF File)

Send comments and suggestions to: tahar@ece.concordia.ca