Login | Register

Techniques for the formal verification of analog and mixed- signal designs

Title:

Techniques for the formal verification of analog and mixed- signal designs

Hussein, Mohamed Hamed Zaki (2008) Techniques for the formal verification of analog and mixed- signal designs. PhD thesis, Concordia University.

[img]
Preview
Text (application/pdf)
NR45663.pdf - Accepted Version
2MB

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
ID Code:975213
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 15:44
Last Modified:18 Jan 2018 17:39
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top