Login | Register

Towards the automated modelling and formal verification of analog designs

Title:

Towards the automated modelling and formal verification of analog designs

Denman, William (2009) Towards the automated modelling and formal verification of analog designs. Masters thesis, Concordia University.

[thumbnail of MR63248.pdf]
Preview
Text (application/pdf)
MR63248.pdf - Accepted Version
1MB

Abstract

The verification of analog circuits remains a very time consuming and expensive part of the design process. Complete simulation of the state space is not possible; a line is drawn by the designer when it is deemed that enough sets of inputs and outputs have been covered and therefore the circuit is "verified". Unfortunately, bugs could still exist and for safety critical applications this is not acceptable. As well, a bug in the design could lead to costly recalls and a loss of revenue. Formal methods, which use mathematical logic to prove correctness of a design have been developed. However, available techniques for the formal verification of analog circuits are plagued by inaccuracies and a high level of user effort and interaction. We propose in this thesis a complete methodology for the modelling and formal verification of analog circuits. Bond graphs, which are based on the flow of power, are used to automatically extract the circuit's system of Ordinary Differential Equations. Subsequently, two formal verification methods, one based on automated theorem proving with MetiTarski, the other on predicate abstraction based model checking with HybridSal, are then used to verify functional properties on the extracted models. The methodology proposed is mechanical in nature and can be made completely automated. We apply this modelling and verification methodology on a set of analog designs that exhibit complex non-linear behaviour.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Denman, William
Pagination:xiii, 88 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:2009
Thesis Supervisor(s):Tahar, Sofiène
Identification Number:LE 3 C66E44M 2009 D46
ID Code:976431
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:25
Last Modified:13 Jul 2020 20:10
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

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top