IDA Technical Reports: abstract

Larsson, T. (1990). The Symbolic Manipulation of Event Traces. Technical Report LiTH-IDA-R-90-28, Department of Computer and Information Science, Linköping University, Sweden. Also in Proc. of the ACM/IFIP 1991 International Workshop on Formal Methods in VLSI Design, Miami, 9-11 Jan, 1991. (bibtex),

Abstract: A method which unifies the power of formal proof and the power of simulation is proposed. The formal language, axioms and inference rules used normally for verification by proof are here used for simulation carried out by symbolic manipulation of circuit behaviour observations represented as event traces. In order to do this efficiently a delay calculus is used. The proposed method, called formal simulation, integrates static and dynamic analysis and bridges the gap between formal methods and simulation.