Hussein, Mohamed Hamed Zaki (2008) Techniques for the formal verification of analog and mixed- signal designs. PhD thesis, Concordia University.
Preview |
Text (application/pdf)
2MBNR45663.pdf - Accepted Version |
Abstract
Embedded systems are becoming a core technology in a growing range of electronic devices. Cornerstones of embedded systems are analog and mixed signal (AMS) designs, which are integrated circuits required at the interfaces with the real world environment. The verification of AMS designs is concerned with the assurance of correct functionality, in addition to checking whether an AMS design is robust with respect to different types of inaccuracies like parameter tolerances, nonlinearities, etc. The verification framework described in this thesis is composed of two proposed methodologies each concerned with a class of AMS designs, i.e., continuous-time AMS designs and discrete-time AMS designs. The common idea behind both methodologies is built on top of Bounded Model Checking (BMC) algorithms. In BMC, we search for a counter-example for a property verified against the design model for bounded number of verification steps. If a concrete counter-example is found, then the verification is complete and reports a failure, otherwise, we need to increment the number of steps until property validation is achieved. In general, the verification is not complete because of limitations in time and memory needed for the verification. To alleviate this problem, we observed that under certain conditions and for some classes of specification properties, the verification can be complete if we complement the BMC with other methods such as abstraction and constraint based verification methods. To test and validate the proposed approaches, we developed a prototype implementation in Mathematica and we targeted analog and mixed signal systems, like oscillator circuits, switched capacitor based designs, Delta-Sigma modulators for our initial tests of this approach.
Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
---|---|
Item Type: | Thesis (PhD) |
Authors: | Hussein, Mohamed Hamed Zaki |
Pagination: | xv, 191 leaves : ill. ; 29 cm. |
Institution: | Concordia University |
Degree Name: | Ph. D. |
Program: | Electrical and Computer Engineering |
Date: | 2008 |
Thesis Supervisor(s): | Tahar, S and Bois, G |
Identification Number: | LE 3 C66E44P 2008 H87 |
ID Code: | 975213 |
Deposited By: | Concordia University Library |
Deposited On: | 22 Jan 2013 15:44 |
Last Modified: | 13 Jul 2020 20:07 |
Related URLs: |
Repository Staff Only: item control page