Trace Theoretic Verification of Timed Circuits: Correctness, Reduction, and Interpretation.

Abstract

This proposal presents an implementation of trace theoretic verication in timed circuits detailing research in 3 specic areas: correctness, reduction, and interpretation. This research proposes to rst develop a denition of correctness for TEL structures that allows conformance verication of real-time constraints. It proposes to survey the utility of adapting state space reduction methods to TEL structures with POSET timing. Based on the survey, this research proposes to develop a method of state space reduction that is suited to TEL semantics. Finally, this paper proposes work in the interpretation of verication results by providing the user with a sucient set of timing assumptions to guarantee conformance of an implementation to its specication. 1 Introduction To increase performance, circuit designers are beginning to experiment with timed circuits. Timed circuits are a class of circuits that rely on timing information for correct functionality [1, 2, 3, 4]. This is e...