Skip to content
STIMSMITH

Operation Properties

Concept WIKI v1 · 5/26/2026

Operation properties are high-level verification properties that describe a design under verification through an operation view. For processors, an operation typically corresponds to a single instruction, and each property specifies the resulting architectural-state changes and output behavior.

Overview

Operation properties express a high-level operation view of a design under verification (DUV). Rather than reimplementing complex circuit logic in the verification language ITL, they are formulated compactly using abstraction techniques. For a processor, an operation naturally corresponds to the execution of a single instruction. Each operation property describes how the processor's internal state changes and how its output signals behave when that instruction is executed. [C1]

Architectural abstraction

In operation properties, the DUV state is described in terms of a high-level or architectural state, corresponding to the programmer's view of visible registers. This abstraction is achieved through mapping functions. For example, in a pipelined processor, a mapping function can link the architectural register file to implementation registers while capturing pipeline forwarding logic. [C2]

Completeness expectations

Operation properties are expected to cover not only the updated state element for an operation, but also unchanged state and output behavior. In the cited ADD-instruction example, the property must state that the remaining registers do not change value and must specify the processor's output behavior. [C3]

Relationship to architectural-style properties

A set of operation properties may contain an architecture description only implicitly. Because of this, generically and fully automatically extracting an instruction set simulator (ISS) from operation properties is described as difficult. The cited work therefore reformulates operation properties into an architectural style, where the architectural state, interface behavior, reset state, and a next_state macro are made explicit. [C4]

Role in ISS generation

When verification is performed in architectural style, an ISS can be generated from the verification without manual steps. Reformulating operation properties into that style does not require new detailed consideration of the design behavior, because the architectural-state components and instruction semantics are already identified during verification. [C5]

Consistency checking

The reformulated architectural-style property is checked against the RTL, and automatic gap detection is also executed. This process is used to identify discrepancies between the architectural and operation properties, while preserving equivalence of the reformulated property set to the design. [C6]

LINKED ENTITIES

2 links
Architectural State describes_state_using
Architectural Style Properties can_be_reformulated_as

CITATIONS

6 sources
6 citations
[1] Operation properties express a high-level operation view of a DUV; for processors, an operation corresponds to a single instruction, and each property describes internal-state changes and output-signal behavior during instruction execution. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] Operation properties describe DUV state through a high-level architectural state, and this abstraction is achieved using mapping functions such as a register-file mapping that can capture pipeline forwarding logic. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] Completeness requirements for an operation property include stating that unaffected registers remain unchanged and specifying processor output behavior. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] For operation properties, the architecture description is implicit, making generic fully automatic ISS extraction difficult; the cited work therefore reformulates them into architectural style with explicit architectural state, interfaces, reset state, and next_state behavior. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[5] If verification is carried out in architectural style, an ISS can be generated from the verification without manual steps, and reformulating operation properties does not require new detailed consideration of the design behavior. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[6] The reformulated property is checked against RTL and automatic gap detection is executed to identify discrepancies between architectural and operation properties while maintaining equivalence to the design. Generating an Efficient Instruction Set Simulator from a Complete Property Suite