Seminar by Dr. Paritosh Pandya
The saga of synchronous bus arbiter: On model checking quantitative timing properties of synchronous programs
Dr. Paritosh Pandya
Dr. Paritosh Pandya
School of Technology and Computer Science
Tata Institute of Fundamental Research
Mumbai, India
Date: Monday, October 7, 2003
Time: 4:00 PM
Venue: CS-103
Abstract
Quantified Discrete-time Duration Calculus, (QDDC), is a form of interval temporal logic. It is well suited for specifying quantitative timing properties of synchronous systems. An automata theoretic decision procedure for QDDC allows converting a QDDC formula into a finite state automaton recognizing precisely the models of the formula. The automaton can be used as a synchronous observer for model checking the property for a synchronous program. This theory has been implemented into a tool called DCVALID which permits model checking QDDC properties of synchronous programs written in Verilog, Esterel, Lustre and SMV notations. In this talk, we will consider two well known synchronous bus arbiter circuits (programs) from the literature. We will specify some complex quantitative properties of these arbiters, including their response time and loss time, using QDDC. We show how the tool DCVALID can be used to effectively model check these properties.