Verification of timed circuits with symbolic delays

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 applicability of the approach.Peer ReviewedPostprint (published version