Freeze Variable

Concept

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.

First seen 5/29/2026

Last seen 5/29/2026

Evidence 2 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

1 connections

ITL ← uses 100% 1e

ITL uses freeze variables to capture signal values at specific time points.

LINKED ENTITIES

1 links

ITL USES Extracted graph relationship

CITATIONS

4 sources

4 citations — click to collapse

[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*)