Larsson, T. (1989). Mixed Functional and Temporal Hardware Verification. Technical Report LiTH-IDA-R-89-53, Department of Computer and Information Science, Linköping University, Sweden. Also in Proc. of Applied Formal Methods For Correct VLSI Design, 13-16 November 1989, Leuven, Belgium. (bibtex),
Abstract: We a present higher-order description language extended with a temporal operator. The temporal extension is defined by a set of axioms and a temporal model. We give examples on the description of hardware circuits and temporal constraints on these. Further a verification method based on transformations is presented and illustrated by an example proof of a finite impulse response filter.
CS Dept TR Overview