Date of Award

6-1999

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Department of Electrical and Computer Engineering

First Advisor

Thomas C. Hartrum, PhD

Abstract

Timed Logic Conformance (TLC) is used to verify the behavioral and timing properties of detailed digital circuits against abstract circuit specifications when both are modeled as Timed Safety Automata (TSA) with real-valued clocks. TLC is a bisimulation-style partial order relationship defined over TSA state space. In contrast to timed simulation, Calculus of Timed Refinement, and time-abstracted bisimulation, TLC defines when one system is an acceptable implementation of another by asymmetric action-matching requirements for specification inputs and implementation outputs. TLC intuitively and pragmatically supports writing abstract specifications and verifying them against implementations. TLC scales up by substituting verified specifications for implementations and hierarchically verifying larger systems. The TLC verification process is more efficient than the circularly dependent assumes-guarantees verification methodology. Instead of building models of the system's environment and using them in the verification process, the TLC verification methodology explicitly captures environmental timing properties in the system specification and automatically ensures they are satisfied in the TLC relation. The region-automata-based Timed Logic Conformance System (TLCS) implements TSA parallel composition and a TLC decision procedure. TLCS is used to hierarchically verify the STARI (Self-Timed at Receiver's Input) asynchronous circuit for communicating safely between clock-skewed systems.

AFIT Designator

AFIT-DS-ENG-99-02

DTIC Accession Number

ADA364388

Download

Share

COinS