Visualize binary decision diagrams online | BDD Workbench

BDD WorkbenchA BDD visualizer in the browser: turn Boolean expressions into binary decision diagrams, and inspect their size, minterms and shared nodes.Modes

Build — A BDD visualizer in the browser: turn Boolean expressions into binary decision diagrams, and inspect their size, minterms and shared nodes.

Order — See how the variable order changes a binary decision diagram's size, and watch sifting reorder it.

Reduce — Reduce a decision tree to a reduced ordered binary decision diagram, one rule at a time.

Apply — Trace the recursive Apply algorithm and quantification, and see what the computed table saves.

Circuit — Build binary decision diagrams from Verilog, and check two designs for equivalence.

Reach — Compute the reachable states of a small sequential design, and check an invariant.

How do I use the Workbench?Write a program, or a Verilog design in Circuit and Reach modes, and the Workbench builds its functions as binary decision diagrams with CUDD.How do I write a program?Write one definition per line, as name = expression;. A definition may use the names defined above it; any other name is a variable. A // starts a comment that runs to the end of its line, and an optional first statement order: a b c; sets the variable order. It must list every variable the program uses.The table lists the operators from the most tightly binding (level 1) to the least (level 8). Operators on the same level bind equally; ? :, -> and <-> group to the right.

Level

Write

Meaning

~a, !a

not a

a & b

a and b

a ^ b

a exclusive-or b

a ~^ b, a ^~ b

a exclusive-nor b (a equals b)

a | b

a or b

a && b

a and b

a || b

a or b

c ? a : b

a when c is 1, else b

a -> b

a implies b

a <-> b

a if and only if b

The constants are 0, 1, 1'b0 and 1'b1.Quantifiers are written exists(x, y: expression) and forall(x: expression). exists(x: f) is 1 when f is 1 with x set to 0 or with x set to 1; forall(x: f) is 1 when it is 1 with both. Each quantified variable must occur in the expression, or in a function the expression uses.Which Verilog do Circuit and Reach modes accept?Paste every module of the design into the editor: the include directive is not supported. The site's proof runner converts the design with Yosys, which finds the top module; when the design has several modules, a list lets you choose it. A design with a memory, such as an array of registers or $readmemh, or with a latch is refused. An undefined value (x) becomes 0, and an asynchronous reset is modelled as a synchronous one.Circuit mode takes a combinational design with at most 64 input bits and 64 output bits, and builds one BDD for each output bit, named port[i], or port for a 1-bit port. With a design in each of its two tabs, it checks the two for equivalence, output bit by output bit.Reach mode takes a sequential design with at most 16 state bits and 32 input bits. Each step is one clock cycle. A flip-flop with an initial value, as in reg [1:0] q = 2'd0;, starts at it; a flip-flop without one may start at either value. A reset input is an input like any other.How do I read the diagram?Each row is one of the variables the diagram uses, top to bottom in the current order. The table says what each mark means.

Circle with a variable

A decision on that variable.

Square 1 (and 0)

A terminal: the function's value. The CUDD view has the single terminal 1.

Solid arrow

The then edge: the variable is 1.

Dashed arrow

The else edge: the variable is 0.

Dotted arrow with an open circle

A complemented else edge (CUDD view): the function below it is negated.

Label with a short arrow

A root: the output's name. Dotted with an open circle when the root is complemented.

How do I compare two outputs?Choose two outputs under “Compare two outputs” and select Compare. Equivalent outputs are the same function, and CUDD stores them as one node. Different outputs come with one assignment on which they differ, and each output's value on it.What does the CUDD view show?It shows the diagram as CUDD stores it, with a single terminal, 1. An else edge may be complemented, which negates the function below it, so a function and its negation share every node. This is why CUDD's diagram is never larger than the textbook's, and often smaller.What does the textbook view show?It shows the reduced ordered BDD of the textbooks, with the terminals 0 and 1 and no complemented edges. It is the same function as the CUDD view, drawn without CUDD's sharing of negations. Its size counts every terminal it reaches.