Address Set Expression (ASExpr)

Concept

An Address Set Expression (ASExpr) is a symbolic representation of a set of memory addresses used in symbolic ternary simulation, structured as a vector of control expressions (each encoded with high and low Boolean bits) of width n for a memory with N = 2^n locations. ASExprs support symbolic predicates for equality, subset, overlap, and uniqueness, and are used as inputs to Write and Read operations on the Effective Memory Model (EMM).

First seen 6/18/2026

Last seen 6/18/2026

Evidence 4 chunks

Wiki v1

WIKI

Address Set Expression (ASExpr)

Definition

An Address Set Expression (ASExpr) denotes a set of memory addresses in symbolic ternary simulation [chunk: cffce784-0b18-4f73-93c4-91e7a6bf1a39]. Because a memory address input receives ternary values from circuit nodes, addresses are represented as vectors of control expressions of width n for a memory with N = 2^n locations. An X at any bit position represents an "unknown" bit, meaning the bit can be either 0 or 1, so a single ASExpr can represent many distinct addresses.

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

Write Operation (EMM) ← uses 100% 1e

The Write operation takes an address set expression as argument.

Read Operation (EMM) ← uses 100% 1e

The Read operation takes an address set expression as argument.

LINKED ENTITIES

2 links

Write Operation (EMM) USES Extracted graph relationship

Read Operation (EMM) USES Extracted graph relationship

CITATIONS

11 sources

11 citations — click to expand

[1] ASExpr denotes a set of memory addresses represented as a vector of control expressions of width n for a memory with N = 2^n locations. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[2] ASExpr equality is defined as ¬ ⋁_{i=1..n} [(a1.h_i ⊕ a2.h_i) ∨ (a1.l_i ⊕ a2.l_i)]. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[3] ASExpr subset a1 ⊆ a2 is ¬ ⋁_{i=1..n} (a1.h_i ∧ ¬a2.h_i ∨ a1.l_i ∧ ¬a2.l_i). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[4] ASExpr overlap is ⋁_{i=1..n} (a1.l_i ∧ a2.l_i ∨ a1.h_i ∧ a2.h_i). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[5] Unique(a) is the condition for an ASExpr to represent a single address, defined as ¬ ⋁_{i=1..n} Soft(a_i). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[6] The ITE selection over ASExprs selects corresponding high and low bits per address position under a Boolean condition. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[7] The Write operation inserts an entry into the tail of the memory list with h ← Hard(c) ∧ Unique(a) and s ← Soft(c) ∨ Hard(c) ∧ ¬Unique(a). Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[8] The Read operation scans the memory list computing hard_match ← e_h ∧ (e_a = a) and soft_match ← [e_s ∨ e_h ∧ ¬(e_a = a)] ∧ Overlap(e_a, a), and is precise only when the address is unique, returning UD otherwise. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[9] Symbolic predicates cannot be used as control decisions; Valid() is used to test whether a symbolic Boolean expression is true for all contexts. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[10] After a Write, the software interface updates on-going reads on overlapping addresses with rd ∪ d to maintain a conservative EMM approximation. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation

[11] In correspondence checking, ASExprs are used so that initial symbolic values are assigned under matching contexts in both memories. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation