[VLSI CAD] kbdd - MiniSAT - Espresso - SIS?

When you take an EDA or VLSI CAD class, all of a sudden these tools pop up:

• kbdd
• MiniSAT
• Espresso
• SIS

At first, they all seem similar: "Isn't this all about logic expressions?"
"Do we ever use this in practice?"

The bottom line is that these are tools from the "chip-fit world."

These basic concepts are used in many digital EDA tools, such as Logic Synthesis and DFT.

1. The big picture: the real topic of this lesson

The core of this lesson is how to work with Boolean Functions.

"Does this logic circuit make sense mathematically?"

There are three different approaches we use to do this:

"Does this logic circuit make sense mathematically?2. kbdd - "Same logic, same graph"What kbdd does

kbdd is a logic calculator based on Binary Decision Diagram (BDD).

The key property of BDD is this:The same Boolean function always has the same graph structure.

That is:No matter how different the logical expressions areNo matter how different the circuit structure isIf the functions are the same → BDD is the same

So the main thing you can do with kbdd is:Verify logic coherence (verify)Find possible input combinations (satisfy)Remove variables (quantify)Automatically repair circuits (logic repair)When is kbdd usedRTL vs Spec verificationGate-level logic debuggingFormal verification theory

👉 "Are these two circuits really the same?"
It is a tool to answer this question mathematically.



An example of BDD is shown below:

BDD is a question tree representation of the "simple rule of 0/1".

For more information, see the documentation below:

https://www.sciencedirect.com/topics/computer-science/binary-decision-diagramExample: XOR f(x1,x2)=x1⊕x2Truth table of XOR:x1=0,x2=0→f=0x1=0,x2=1→f=1x1=1,x2=0→f=1x1=1,x2=1→f=0

If we make this into a BDD, given the variable order x1→x2:There is one x1 node at the root (root node).From x1,if x1=0, we go down to the left (0-edge)if x1=1, we go down to the right (1-edge)There are two nodes below it, one for each of the x2nodes.From each x2 node, we go down againleft if x2=0, right if x2=1,and finally, we arrive at the leaf.

We can draw a picture of this.

In other words, it is a structure that "goes down 0/1 branches along the input value, and the value of the leaf at the end is the value of the boolean function".Why is BDD good:Truth tables have 2^n rows, so they become complex as n grows.BDD reduces the complexity of Big(n) because it can reuse nodes by sharing the same patterns.

To summarize:BDD = "For a Boolean function, a directed graph variable → yes/no(0/1) ", so you can put in an input, walk down the branches, and automatically arrive at the result.BDD is a structure that allows you to do this.