Operation Properties

Concept

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.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 2 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

2 connections

Architectural Style Properties ← extends 90% 2e

Architectural style properties are a reformulation of operation properties that enable automatic ISS generation.

Mapping Function ← part of 90% 1e

Mapping functions are used in operation properties to relate implementation state to architectural state.

LINKED ENTITIES

2 links

Architectural State describes_state_using Operation properties describe the DUV state in terms of a high-level or architectural state corresponding to the programmer's view of visible registers.

Architectural Style Properties can_be_reformulated_as The evidence describes reformulating operation properties into an architectural style to make ISS generation straightforward.

CITATIONS

6 sources

6 citations — click to expand

[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