Verification of timed circuits with symbolic delays

When time is incorporated in the specification of discrete systems, the complexity of verification grows exponentially. When the temporal behavior is specified with symbols, the verification problem becomes even more difficult. This paper presents a formal verification technique for timed circuits with symbolic delays. The approach is able to provide a set of sufficient linear constraints on the symbols that guarantee the correctness of the circuit. The applicability of the technique is shown by solving the problem of automatic discovery of linear constraints on input and gate delays that guarantee the correct behavior of asynchronous circuits.

• Type: Conference
• Year: 2004
• Where: ASPDAC
• Authors: Robert Clarisó, Jordi Cortadella
• Keywords: ASPDAC 2004, Formal Verification Technique, Hardware, Linear Constraints, Sufficient Linear Constraints