Verification of digital circuits based on formal semantics of a hardware description language

Reasoning about properties of hardware behuviour needs u formal method. The more this process can be nu’chanized the more practicable is it. In this paper, basic concepts qf u special verification system for the formal ver~jication of digital circuits are presented. Higher-order Logic serves as the formalist to define the underlying theory.