Verifying timed circuits is a complex problem even when the delays of the system are fixed. This paper deals with a more challenging problem, the formal verification of timed circuits with unspecified delays represented as symbols. The approach discovers a set of sufficient linear constraints on the symbols that guarantee the correctness of the circuit. Experimental results from the area of asynchronous circuits show the applicablity of the approach.
展开▼
