Larsson, T. (1988). Hardware Verification based on Algebraic Manipulation and Partial Evaluation. Technical Report LiTH-IDA-R-88-41, Department of Computer and Information Science, Linköping University, Sweden. Also in Proc of IFIP WG 10.2 International Working Conference on "The Fusion of Hardware Design and Verification", Glasgow, Scotland, July 3-6, 1988. (bibtex),
Abstract: A verification method based on algebraic manipulation of behaviour and structure describing expressions is presented. As a framework for this method a set of canonization rules for boolean, arithmetic, relational and conditional expressions are proposed. A temporal function is associated with a set of demurral canonization rules and used to organize temporal reasoning. These rules are collected into a set of decision procedures that can be applied by a partial evaluator or by the user.
CS Dept TR Overview