[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.