Transaction-based verification is a recent trend in hardware verification. The system is considered at higher levels of abstraction that model the data transfers and input/output (I/O) events between computational blocks, and functional verification is based on assertions that describe the expected behavior.

In this paper, the authors attempt a comparison of transaction-level modeling (TLM) verification with a full register transfer level (RTL) verification methodology. They also present an approach for deriving logical consequences of properties that becomes important in detecting redundant properties.

The technique presented in the paper is based on a functional fault model, and considers witness coverage that indicates the percentage of faults covered by fault-simulating witnesses of the property.

The presentation of the methodology is lucid and the terminology is well defined. The fact that relevant background material is provided in detail makes the paper easy to read and understand. However, the theoretical contribution is somewhat weak, as the theorems and corollaries follow trivially from the definitions.

The suggested property optimization methodology cannot fully eliminate the burden of theorem proving, as the mechanism based on fault simulation can only provide a necessary condition for property redundancy. However, the presented ideas can be explored further to enhance the performance of model-checking tools.