@techreport{R-88-41, TITLE = {Hardware Verification based on Algebraic Manipulation and Partial Evaluation}, AUTHOR = {Tony Larsson}, YEAR = {1988}, NUMBER = {R-88-41}, INSTITUTION = ida, ADDRESS = idaaddr, ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-88-41+abstr}, 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.}, IDANR = {LiTH-IDA-R-88-41}, NOTE = {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}