Skip to content
STIMSMITH

Approximate Union Operation

Concept

The Approximate Union Operation (denoted ∪∼) is a bitwise combination operator defined on data set expressions in symbolic ternary simulation. It produces a conservative (over-approximating) result when the exact set-theoretic union of two data sets cannot be represented precisely in ternary form, and it is the mechanism by which the Efficient Memory Model (EMM) merges data from possibly-overlapping memory list entries during a Read operation.

First seen 6/18/2026
Last seen 6/18/2026
Evidence 3 chunks
Wiki v1

WIKI

Overview

In the symbolic ternary simulation framework used to verify pipelined microprocessors by correspondence checking, memory contents are represented as data set expressions (DSExpr) whose bits are pairs drawn from {0, 1, X} (low and high Boolean halves). Because the X value denotes uncertainty over both 0 and 1, the bitwise-OR of two data set expressions is not in general equal to the exact set-theoretic union of the two sets. To obtain a value that is guaranteed to be a conservative (super-set) approximation, the framework defines a dedicated operator called the approximate union, written with a tilde over the union symbol:

[d1 ∪∼ d2]i = [d1.hi ∨ d2.hi, d1.li ∨ d2.li],   i = 1, ..., w
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
Read Operation (EMM) ← uses 90% 1e
The Read operation uses approximate union to combine data set expressions.
Efficient Memory Model (EMM) part of → 85% 1e
The approximate union operation is defined and used within the EMM's data operations.

LINKED ENTITIES

2 links
Read Operation (EMM) USES Extracted graph relationship
Efficient Memory Model (EMM) PART_OF Extracted graph relationship

CITATIONS

5 sources
5 citations — click to expand
[1] The Approximate Union Operation is defined element-wise as [d1 ∪∼ d2]i = [d1.hi ∨ d2.hi, d1.li ∨ d2.li] for i = 1, ..., w, where d.hi and d.li are the high and low Boolean halves of each bit. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[2] The operation is approximate rather than exact because ternary bitwise combination yields X-bits that over-approximate the union; e.g., d1 = ⟨0,1⟩ combined with d2 = ⟨1,0⟩ yields ⟨X,X⟩ which also admits ⟨0,0⟩ and ⟨1,1⟩. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[3] The Read operation of the EMM uses the approximate union in the soft_match branch as rd ← ITE(soft_match, (ed ∪∼ rd), rd) when scanning the memory list from head to tail. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[4] The approximate union is the mechanism by which the EMM provides a conservative approximation of the replaced memory array, ensuring that the reported read data soundly covers all possible values. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation
[5] Boolean expressions (including those used in the approximate union) are represented with Ordered Binary Decision Diagrams (OBDDs) in the implementation, though any Boolean representation supporting a Valid() test can be substituted. Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation