Formal verification of the correctness of properties implemented in digital systems entails nontrivial algorithmic puzzles. Verifying consistencies between the realizations and intended behaviors of digital machines requires specifications for capturing the semantics of hardware description languages. Manual specification of formal properties for designing machines is cumbersome. Specifications of machines designed using hardware description languages, with properties expressed in standard assertion languages, must be translated into a format suitable for a generalized theorem-proving system.

Theories of rewriting systems for proving theorems, simulation-based environments, and rule-based models for property specification languages exist in the literature [1]. However, the formalization of assertions as predicates of time for relating the semantics of property specification languages to multiple cycles of time is nontrivial. Kim et al. present generic assertion templates for the automatic extraction of formal models implicit in the design of digital machines. The paper outlines a design model consisting of quintuple time domain, functions mapping time to signal values, a set of combinational assignments, and a set of sequential assignments. The correctness of properties implicit in selected benchmark circuits was successfully verified by a theorem-proving system. Although the verification system is restricted to the static property validation of assertions, the paper provides a useful framework for integrating models of heterogeneous machine designs and assert!ion languages.