Skip to content
STIMSMITH

Freeze Variable

Concept WIKI v1 · 5/29/2026

A freeze variable is a temporal-logic variable bound to the value of an expression at a specified time point. In ITL, freeze variables are declared in a property’s freeze section and can then be used in assume/prove temporal expressions while retaining the frozen time reference.

Freeze Variable

A freeze variable is a variable in a temporal-logic property that is assigned the value of an expression at a specified time point and then keeps that time-point reference wherever it is used. In ITL, expressions are assigned to freeze variables in a property’s freeze section; for example, c1 = c@t+1 makes c1 refer to the value of signal c at time t + 1, regardless of the later temporal context in which c1 appears.

Role in ITL

ITL properties describe synchronous sequential systems, with discrete time steps corresponding to clock cycles. A typical ITL property has an implication-like structure: when the expressions in the assume part evaluate to true, the expressions in the prove part must hold. Freeze variables support this style by naming values at fixed time points so they can be reused in temporal expressions.

ITL temporal expressions may use standard VHDL or Verilog operators, as well as next and prev, which shift an enclosed expression one cycle into the future or past, respectively. In the cited ITL example, a proof obligation stating that c at t + 1 equals the previous value plus one is shown alongside an equivalent expression using the freeze variable c1.

Example uses

A simple ITL property can freeze a future signal value:

freeze:
  c1 = c@t+1;

The variable c1 can then be used at another point in the property while still denoting c at t + 1.

In a processor instruction property, the freeze section can also capture decoded fields from an instruction word at the current time. One example freezes opcode, regA, regB, and regD from slices of instr@t; the assume section then checks that the opcode is ADD_op and the processor is ready, and the prove section specifies the corresponding register-file update.

Related terminology

The broader temporal-logic literature also uses value-freezing operators. Public context for STL* describes it as Signal Temporal Logic augmented with a value-freezing operator, introduced to express engineering properties not expressible in STL. That work also discusses monitoring formulas with nested freeze variables.

LINKED ENTITIES

1 links
ITL USES

CITATIONS

4 sources
4 citations
[1] In ITL, expressions can be assigned in a freeze section to variables fixed to a certain time point; the example c1 = c@t+1 makes c1 refer to the value of signal c at time t+1 regardless of temporal context. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] ITL properties describe synchronous sequential systems with discrete time steps corresponding to clock cycles, commonly using assume/prove structure; next and prev shift expressions one cycle into the future or past. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] An ITL instruction property can use the freeze section to decompose an instruction word into opcode and register fields at time t, then use those frozen values in assumptions and proof obligations for an ADD instruction. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] STL* is described as Signal Temporal Logic augmented with a value-freezing operator; public context also reports work on monitoring formulas with nested freeze variables. Fast Robust Monitoring for Signal Temporal Logic with Value Freezing Operators (STL*)