[1-28]Verifying Digital Circuits using Continu...
Date:2008-01-27
Title:Verifying Digital Circuits using Continuous Models
Speaker:Prof. Mark Greenstreet
Department of Computer Science
University of British Columbia
Time: 3.30pm, Monday Jan 28
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5,
Institute of Software, CAS
Abstract:This is our approach for reachability analysis for systems with continuous spaces. We have a working implementation of the "projectagon" methods that Ian Mitchell and I proposed in some of the early HSCC workshops. While the approach is mathematically simple, the numerical methods suffered from problems of severe ill conditioning. We have now tamed those. We’ve applied our prototype tool to verify a toggle flip-flop circuit (seven dimensional, non-linear, ODE model) and are currently working on other circuits.
We could also describe related work we’ve done for analysing synchronizer failure probabilities, noise-margin analysis, and verifying start-up conditions for ring oscillator circuits.