Formal Verification of Safety Properties in Timed Circuits

The incorporation of timing makes system verification computationally expensive. This work proposes a new approach for the verification of timed circuits. Rather than calculating the exact timed state space, a conservative overestimation that fulfills the property under verification is derived. Timing analysis with absolute delays is efficiently performed at the level of event structures and transformed into a set of relative timing constraints. With this approach, conventional symbolic techniques for reachability analysis can be efficiently combined with timing analysis. Moreover, the set of timing constraints used to prove the correctness of the circuit can also be reported for backannotation purposes.

The correctness of speed-independent and delay-insensitive circuits can be proved by only considering the sequencing of events and abstracting time as nondeterministic delays. However, the correctness of timed circuits depends on the actual values of event delays. Typically, timing behavior is specified by a set of delays that determine the time duration between the initiation and the completion of an event. This is the valid model for the gates in a circuit, in which gate delays denote the time between the enabledness of the gate and the actual change at the output.

The calculation of the language generated by a timed system has been proven to be PSPACE-complete, and demonstrated to be highly complex in several contexts such as real-time systems and asynchronous circuits. Geometric regions combined with partially ordered sets have been recently used to verify highly concurrent systems.

Although geometric regions can represent clock zones efficiently, they still suffer from the problem of dealing with a large number of untimed states.

This work proposes a novel approach that extends the applicability of the conventional methods based on symbolic reachability analysis to timed systems.
The approach is based on the following observation: the set of traces of a transition system can be covered by a set of marked graphs. Rather than calculating the exact timed state space, our approach performs an off-line timing analysis on a set of events structures that covers the traces leading to system failures. This timing analysis can be efficiently performed by using McMillan and Dill's algorithm. If some of the failure traces cannot be proven to be timing inconsistent, then the system is incorrect.

The approach not only verifies the system, but also provides a set of timing constraints required for its correctness. For speed-independent circuits, the application of the method does not involve any additional overhead with regard to the conventional symbolic methods. Negulescu proposed an approach with similar goals, but limited to the comparison of circuit paths that start at the same point.


We believe that the conventional symbolic methods for reachability analysis can be efficiently extended for timed systems. Although timed systems have an inherent delay for each event, it is evident that, in practice, many of the timing constraints imposed by these delays are not required for the correctness of a system. The proposed approach is not only useful to verify correctness, but also to backannotate the set of timing constraints that have been used to prove it. This information is crucial in frameworks in which synthesis and verification are iteratively invoked to design systems that must meet functional and non-functional constraints.

The fact that timing analysis is performed by event structures, while verification can be performed in systems with any type of causality relation, opens the door to symbolic analysis. 

Some preliminary results obtained by a naive implementation of the approach show that systems with more than 10⁵ untimed states can be verified in few minutes of CPU time.