Model transformation case study using ATL :
Truth tables to Binary Decision Diagrams
Guillaume Savaton, ESEO

Summary

These files provide a case study for model transformation applied to digital logic circuits.
Engineers can use various formalisms to represent combinatorial or sequential logic.
The most widespread representations for combinatorial logic are truth tables and boolean equations.
In many EDA tools, combinatorial logic is represented in a canonical form using Binary Decision
Diagrams (BDD).
BDDs are manly used for model checking and logic optimization.
The purpose here is to use model transformation to transform a truth table into
a binary decision diagram.

Truth tables

The test files provided correspond to the following example.
Files TT/examples/Test.tt and Test.ttmodel contain representations of this truth table :
A B C D  S

0 0    0
0 1 0 0  1
0 1 0 1  0
0 1 1   0
1 0 0 0  0
1 0 1 0  1
1   1  0
1 1 0 0  1
1 1 1 0  0
A truth table (class TruthTable of the metamodel) has ports (class Port).
Ports are either
 input ports (class InputPort) such as A, B, C, D in the example ;
 or output ports (class OutputPort) such as S in the example.
A truth table is composed of rows (class Row of the metamodels) that can appear in any order.
A row provides a mapping between an input pattern (a detected set of values of input ports)
and an output pattern (values assigned to output ports).
A row is made of cells (class Cell) : each cell associates a boolean value to a given port.
Usually, boolean values are represented using symbols "0" (false) and "1" (true).
In file Test.tt, the symbols used are "F" (false) and "T" (true).
In a given row, the absence of a cell for a given input port means that the value of this port is
indifferent with respect to the result. In the example, this is the case for ports C and D in the first row.
However, in each row, all output ports must have a corresponding cell.

Binary decision diagrams

Here is a BDD representation for the example truth table :
(A)

0  1
 
(B) (D)
 
0  1 0  1
   
 (C) (B) 
   
 0  1 01 
     
 (D)  (C) (C) 
     
 0  1  0  1 0  1 
        
S = [0] [1] [0][0][0] [1] [1] [0][0]
Usually, edges are distinguished by a line style :
 dashed lines represent 0 (or false) decisions
 continuouse lines represent 1 (or true) decisions.
In file Test.bdd, edges are labelled with a symbol : "F" (false) or "T" (true).
The evaluation process in a BDD is recursive and can be easily translated into an ifthenelse
hierarchy :
if A=0 then
if B=0 then
S := 0;
else
if C=0 then
if D=0 then
S := 1;
else
S := 0;
endif
else
S := 0;
endif
endif
else
if D=0 then
if B=0 then
if C=0 then
S := 0;
else
S := 1;
endif
else
if C=0 then
S := 1;
else
S := 0;
endif
endif
else
S := 0;
endif
endif
In our metamodel, a binary decision diagram (class BDD of the metamodel) has input and output ports in
the same sense as truth tables.
A BDD is composed of a tree (class Tree).
A tree can be either a leaf node (class Leaf) or a subtree (class Subtree).
A subtree has a reference to an input port (see nodes labeled A, B, C and D on the example).
Upon the value of this port, two edges can be followed :
 one corresponding to a 0 (false) value (reference subtreeForZero in the metamodel)
 one corresponding to a 1 (true) value (reference subtreeForOne in the metamodel)
Leaf nodes represent values assigned to output ports.
In this example there is only one output port but the provided metamodel supports
multiple output ports if needed.
As a result, a leaf node is composed of one or several assignments (class Assignment).

File index

Folders :
TT/  All files related to truth tables (metamodel, models, diagrams)
BDD/  All files related to Binary Decision Diagrams (metamodel, models, diagrams)
TT2BDD/  The transformation from truth table to BDD
Files :
TT/TT.km3  The Truth Table metamodel in text form (KM3 notation)
TT/TT.ecore  The Truth Table metamodel in XMI format
TT/diagrams/TT.png  Graphical representation of the Truth Table metamodel
TT/examples/Test.tt  An example truth table in text form
TT/examples/Test.ttmodel  The same example in XMI format
BDD/BDD.km3  The BDD metamodel in text form (KM3 notation)
BDD/BDD.ecore  The BDD metamodel in XMI format
BDD/diagrams/BDD.png 
BDD/diagrams/Tree.png  Graphical representation of the BDD metamodel
BDD/diagrams/Nodes.png 
BDD/examples/Test.bdd  An example BDD in text form
BDD/examples/Test.bddmodel  The same example BDD in XMI format
TT2BDD/TT2BDD.atl  The transformation from Truth Table to BDD, in ATL