The Saga of Synchronous Bus Arbiter: On Model Checking Quantitative Timing Properties of Synchronous Programs

AbstractQuantified Discrete-time Duration Calculus, (QDDC), is a form of interval temporal logic [14]. It is well suited to specify quantitative timing properties of synchronous systems. An automata theoretic decision procedure for QDDC allows converting a QDDC formula into a finite state automaton recognising precisely the models of the formula. The automaton can be used as a synchronous observer for model checking the property of a synchronous program. This theory has been implemented into a tool called DCVALID which permits model checking QDDC properties of synchronous programs written in Esterel, Verilog and SMV notations.In this paper, we consider two well-known synchronous bus arbiter circuits (programs) from the literature. We 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 (with some surprising results)