Chair of Computer Architecture

Lecture 06

In circuit design, engineers often work with various levels of representation. You cannot go directly from a high-level to a low-level representation, such as a CNF, so additional intermediate layers of abstraction are required. This is where And-Inverter-Graphs (AIGs) play a crucial role. AIGs offer several advantages, such as structural hashing and automatic sharing of common subexpressions, making them an ideal choice.

In C++, this struct could be replaced with a class hierarchy, but in C, different nodes are represented using the same struct with different data fields. The struct contains various fields, including data representing the node’s children, a marking flag, the level (distance to the inputs), and collision chain links for a hash table. The purpose of the hash table is to store nodes and avoid generating duplicate nodes with the same children. The data fields and tags within the struct are used as keys for the hash table. Implementing a custom hash table rather than relying on external libraries is advantageous, allowing for more control and compactness. Bit stuffing is a technique to handle pointers efficiently. Bit stuffing means using pointers instead of offsets for faster access to data. Using pointers directly is more efficient than calculating offsets based on a base address. Recent processors from AMD and Intel have hardware support for bit stuffing, but the code here focuses on software implementation.

Here, “bit stuffing” refers to exploiting certain properties of pointers in C programming. The C library guarantees that any data you allocate will be “byte aligned.” For 64-bit systems, this means the data is eight-byte aligned, and for 32-bit systems, it is four-byte aligned.

Byte alignment means that the starting address of what you allocated will always be a multiple of that number of bytes (8 or 4). Therefore, for an 8-byte aligned memory, the three least significant bits in the address (which in binary representation denote multiples of 8) are always zero.

Bit stuffing comes into play when we realize we can use these least significant bits (always zero due to byte alignment) to store additional information. Because we are guaranteed these bits are zero, we can “stuff” them with other bits of data without interfering with the pointer’s ability to reference the correct memory location.

We use the least significant bit to hold a sign bit, turning the pointer into a signed one. We can also store a “parent pointer” flag with the second least significant bit. This effectively “tags” the pointer with extra information.

Bit stuffing is about cleverly using these spare bits for extra information. This technique can increase the efficiency of your code by reducing the need for extra variables or complex data structures. However, it’s also a more advanced technique that can make your code harder to understand if not properly documented.

Here, “tagging” is synonymous with “bit stuffing.” Tagging in pointers is a technique that allows embedding extra information within a pointer’s bits.

This practice takes advantage of the fact that an operating system typically uses not all bits of a pointer. To explain, modern processors generally use only the least significant 48 bits of a pointer, leaving the upper 16 bits largely unutilized. However, two upper bits are usually the same, reducing the available bits to 15. Therefore, along with the three least significant bits, you effectively have 18 bits available in each pointer for tagging purposes.

Tagging has been employed for various uses, including garbage collection and lockless programming. For instance, in the case of lockless programming, the 15 bits can serve as counters. Different copies of the same pointer could have distinct counts, allowing them to be differentiated.

However, maintaining this system requires software involvement. For example, transitioning from a tagged pointer to a genuine one requires three assembly instructions. Missteps in this process could lead to incorrect branching and increase costs.

Whether an object is on the stack or heap impacts the tagging process. On the stack, the value will be negative; on the heap, it will be positive. This tagging and untagging operation requires three assembly instructions if performed in software.

Interestingly, there is an emerging trend in modern processors that support hardware-based tagging and untagging. This advancement reduces the operation to a single assembly instruction, streamlining the process significantly.

Tagging is especially prevalent in security applications, storing additional information about a pointer. This can enable tracing data flows through an operating system, bolstering security measures.

Once perceived as outdated, tagging in pointers has seen a resurgence and is now supported by modern hardware. If you are working on security problems, you might encounter this technique again, testifying its enduring usefulness.

Modern SAT solvers often spend most computation time waiting for memory to arrive at the processor, leading to memory latency challenges. Executing other instructions such as add, XOR, and AND during this waiting period is possible. The compiler could potentially produce faster code by manipulating the sequence of memory operations in the source code. This optimization could lead to a 50% improvement in runtime and indirectly save costs when running programs on cloud servers.

Adder circuits have linear complexity.

This is a barrel shifter. Shifting is used for accessing array elements and is a $n \log n$ operation in complexity.

This is a multiplier, which is quadratic in complexity.

We can optimize circuits using structural hashing. It involves generating a unique hash value for each circuit structure and utilizing it to store, retrieve, and analyze circuit information efficiently. Structural hashing can identify and eliminate redundant or duplicate circuits, resulting in more efficient circuit designs.

We can theoretically factor large numbers using AIG multiplier circuit representation and a SAT solver to break RSA encryption. In practice, however, the computational requirements are too high. However, this study area is still of great interest due to the potential for discovering more efficient SAT-solving algorithms.

Logical constraints often need to be encoded in a suitable form for analysis or computation. One such methodology is Tseitin’s construction, which assumes simple operational semantics and generally applies to most model constraints. This method benefits small and large domains, where small domains can employ one-hot encoding and larger ones can leverage binary encoding.

However, encoding properties or additional constraints can be more challenging. This is especially true for constraints involving temporal logic, fixed points, or environmental constraints.

Fixed Points

In the context of logical systems, a “fixed point” of a function is a point that is unchanged by the function. In other words, if you apply the function to the fixed point, you return the same point. This concept is often used in various areas of computer science, including the study of program semantics and formal verification.

“Least fixed point” and “largest fixed point” arise when considering functions that operate on ordered sets, like the powerset of states in a system.

• Least Fixed Point: The least fixed point of a function $F$ is the smallest value $x$ such that $F(x) = x$, with “smallest” being defined in terms of some underlying order. The least fixed points often appear with the semantics of inductive definitions or recursion when used in the context of logical constraints and SAT. A common example is the interpretation of a while-loop in a program: the set of states that can be reached after the loop is the least fixed point of the function that describes the loop’s body.
• Largest Fixed Point: The greatest fixed point of a function $F$ is the largest value $x$ such that $F(x) = x$, again with “largest” being defined in terms of some underlying order. The largest fixed points are related to coinductive definitions and potentially infinite behaviors. For instance, the set of states from which a particular state can be reached in a system (possibly after an infinite number of steps) can be seen as the largest fixed point of the transition relation.

Let’s look at an example using fixed points and recursive equations: $x = (a \vee y)$, $y = (b \vee x)$. Here, $x$ and $y$ are mutually dependent - a scenario that can be described as recursive because each variable’s computation relies on the other’s value.

In such a context of mutual dependency, semantics are often defined as a certain fixed point. For our scenario, let us assume the semantics is defined as the least fixed point, the smallest solution satisfying these recursive equations. Upon computation, you will discover that the smallest formula which satisfies these equations is $(a \vee b)$.

You would begin the fixed point computation by setting $x$ and $y$ to 0 to achieve this. Then, you would substitute these values into the equations and continue until you reach a fixed point where $x$ and $x$ no longer change.

However, there is a caveat. If you encode these equations into a SAT problem without considering the least fixed point semantics, the SAT solver could choose $x$ or $y$ as True, irrespective of the values of $a$ or $b$. Instead of finding the least fixed point, you would find the largest one. This might not be an issue if your semantics require a largest fixed point. But if your semantics require a least fixed point, you would end up with an incorrect encoding.

This might seem theoretical, but it has practical implications when encoding puzzles like Sokoban or problems involving reachability in a graph. These situations require the least fixed point semantics. Similarly, ancestor relations in formulas (going from right to left) also require the least fixed point semantics.

An alternative is available in the form of Answer Set Programming (ASP) for scenarios that require the least fixed point semantics. ASP allows you to treat these equations as the least fixed point-defining equations. While it builds on top of SAT technology, the encoding is slightly different, enabling you to use these equations directly. Without this, it might be impossible to encode problems requiring the least fixed point semantics.

The following naive encoding is quadratic, and you use it for $n \leq 5$:

\[\sum_{i=1}^n x_i \leq 1 \equiv \bigwedge_{i<j} \overline{x_i \wedge x_j}\]

For $5 < n \leq 25$, we use the following trick, which is outlined in Knuth’s book:

\[S_{\leq 1} (x_1, \dots, x_n) = \exists t (S_{\leq 1} (x_1, \dots, x_j, t) \wedge S_{\leq 1} (\overline{t}, x_{j+1}, \dots, x_n))\]

For $n > 25$, we do the Commander encoding:

If $x_{i,j}$ is True, then $r_i$ and $c_i$ are true. You obtain two boolean clauses. Now we recursively do at-most-one constraints over the columns and the rows.

For $n=400$, we only need 40 new variables.

Check Your Knowledge

• What is bit-stuffing? How is it used in the context of AIGs?
• Explain the Commander encoding. When do we use it?
• Discuss the complexity of an adder, barrel shifter, and multiplier circuit.
• Counting as an optimization for DPLL serves which purpose?
  • To decrease the number of variables
  • To identify satisfiability more quickly
  • To decrease the complexity of constraints
  • To generate new clauses
• At-most-one encoding is used to manage:
  • Parity constraints
  • Cardinality constraints
  • Boolean constraints
  • Constraint satisfaction problems
• What are the practical implications of encoding problems into CNF that require the least fixed point semantics?

Exercises

• Draw an And-Inverter Graph (AIG) to represent the XOR operation.
• Write down an at-most-one encoding with $n$ variables as a boolean formula.
• Write down a CNF of an at-most-one encoding of variables $x_1, \dots, x_5$ using less than ten clauses.