src/aig/ivy/ivyDsd.c File Reference

#include "ivy.h"
Include dependency graph for ivyDsd.c:

Go to the source code of this file.

Data Structures

struct  Ivy_Dec_t_

Typedefs

typedef struct Ivy_Dec_t_ Ivy_Dec_t

Enumerations

enum  Ivy_DecType_t {
  IVY_DEC_PI, IVY_DEC_CONST1, IVY_DEC_BUF, IVY_DEC_AND,
  IVY_DEC_EXOR, IVY_DEC_MUX, IVY_DEC_MAJ, IVY_DEC_PRIME
}

Functions

static int Ivy_DecToInt (Ivy_Dec_t Node)
static Ivy_Dec_t Ivy_IntToDec (int Node)
static void Ivy_DecClear (Ivy_Dec_t *pNode)
static int Ivy_TruthWordCountOnes (unsigned uWord)
static int Ivy_TruthCofactorIsConst (unsigned uTruth, int Var, int Cof, int Const)
static int Ivy_TruthCofactorIsOne (unsigned uTruth, int Var)
static unsigned Ivy_TruthCofactor (unsigned uTruth, int Var)
static unsigned Ivy_TruthCofactor2 (unsigned uTruth, int Var0, int Var1)
static int Ivy_TruthDepends (unsigned uTruth, int Var)
static void Ivy_DecSetVar (Ivy_Dec_t *pNode, int iNum, unsigned Var)
static unsigned Ivy_DecGetVar (Ivy_Dec_t *pNode, int iNum)
static int Ivy_TruthDecompose_rec (unsigned uTruth, Vec_Int_t *vTree)
static int Ivy_TruthRecognizeMuxMaj (unsigned uTruth, int *pSupp, int nSupp, Vec_Int_t *vTree)
int Ivy_TruthDsd (unsigned uTruth, Vec_Int_t *vTree)
unsigned Ivy_TruthDsdCompute_rec (int iNode, Vec_Int_t *vTree)
unsigned Ivy_TruthDsdCompute (Vec_Int_t *vTree)
void Ivy_TruthDsdPrint_rec (FILE *pFile, int iNode, Vec_Int_t *vTree)
void Ivy_TruthDsdPrint (FILE *pFile, Vec_Int_t *vTree)
Ivy_Obj_t * Ivy_ManDsdConstruct_rec (Ivy_Man_t *p, Vec_Int_t *vFront, int iNode, Vec_Int_t *vTree)
Ivy_Obj_t * Ivy_ManDsdConstruct (Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vTree)
void Ivy_TruthDsdComputePrint (unsigned uTruth)
void Ivy_TruthTestOne (unsigned uTruth)
void Ivy_TruthTest ()
void Ivy_TruthTest3 ()
void Ivy_TruthTest5 ()

Variables

static unsigned s_Masks [6][2]

Typedef Documentation

typedef struct Ivy_Dec_t_ Ivy_Dec_t

Definition at line 39 of file ivyDsd.c.

Enumeration Type Documentation

enum Ivy_DecType_t

CFile****************************************************************

FileName [ivyDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Disjoint-support decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

] DECLARATIONS ///

Enumerator:
IVY_DEC_PI 
IVY_DEC_CONST1 
IVY_DEC_BUF 
IVY_DEC_AND 
IVY_DEC_EXOR 
IVY_DEC_MUX 
IVY_DEC_MAJ 
IVY_DEC_PRIME 

Definition at line 28 of file ivyDsd.c.

00028              { 
00029     IVY_DEC_PI,             // 0: var
00030     IVY_DEC_CONST1,         // 1: CONST1
00031     IVY_DEC_BUF,            // 2: BUF
00032     IVY_DEC_AND,            // 3: AND
00033     IVY_DEC_EXOR,           // 4: EXOR
00034     IVY_DEC_MUX,            // 5: MUX
00035     IVY_DEC_MAJ,            // 6: MAJ
00036     IVY_DEC_PRIME           // 7: undecomposable
00037 } Ivy_DecType_t;

Function Documentation

static void Ivy_DecClear ( Ivy_Dec_t *  pNode  )  [inline, static]

Definition at line 55 of file ivyDsd.c.

00055 { *((int *)pNode) = 0;          }

static unsigned Ivy_DecGetVar ( Ivy_Dec_t *  pNode,
int  iNum 
) [inline, static]

Definition at line 123 of file ivyDsd.c.

00124 {
00125     assert( iNum >= 0 && iNum <= 5 );
00126     switch( iNum )
00127     {
00128         case 0: return pNode->Fan0;
00129         case 1: return pNode->Fan1;
00130         case 2: return pNode->Fan2;
00131         case 3: return pNode->Fan3;
00132         case 4: return pNode->Fan4;
00133         case 5: return pNode->Fan5;
00134     }
00135     return ~0;
00136 }

static void Ivy_DecSetVar ( Ivy_Dec_t *  pNode,
int  iNum,
unsigned  Var 
) [inline, static]

Definition at line 109 of file ivyDsd.c.

00110 {
00111     assert( iNum >= 0 && iNum <= 5 );
00112     switch( iNum )
00113     {
00114         case 0: pNode->Fan0 = Var; break;
00115         case 1: pNode->Fan1 = Var; break;
00116         case 2: pNode->Fan2 = Var; break;
00117         case 3: pNode->Fan3 = Var; break;
00118         case 4: pNode->Fan4 = Var; break;
00119         case 5: pNode->Fan5 = Var; break;
00120     }
00121 }

static int Ivy_DecToInt ( Ivy_Dec_t  Node  )  [inline, static]

Definition at line 53 of file ivyDsd.c.

00053 { return *((int *)&Node);       }

static Ivy_Dec_t Ivy_IntToDec ( int  Node  )  [inline, static]

Definition at line 54 of file ivyDsd.c.

00054 { return *((Ivy_Dec_t *)&Node); }

Ivy_Obj_t* Ivy_ManDsdConstruct ( Ivy_Man_t *  p,
Vec_Int_t *  vFront,
Vec_Int_t *  vTree 
)

Function*************************************************************

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file ivyDsd.c.

00649 {
00650     int Entry, i;
00651     // implement latches on the frontier (TEMPORARY!!!)
00652     Vec_IntForEachEntry( vFront, Entry, i )
00653         Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
00654     // recursively construct the tree
00655     return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
00656 }

Ivy_Obj_t* Ivy_ManDsdConstruct_rec ( Ivy_Man_t *  p,
Vec_Int_t *  vFront,
int  iNode,
Vec_Int_t *  vTree 
)

Function*************************************************************

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file ivyDsd.c.

00580 {
00581     Ivy_Obj_t * pResult, * pChild, * pNodes[16];
00582     int Var, i;
00583     // get the node
00584     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
00585     // compute the node function
00586     if ( Node.Type == IVY_DEC_CONST1 )
00587         return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl );
00588     if ( Node.Type == IVY_DEC_PI )
00589     {
00590         pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) );
00591         return Ivy_NotCond( pResult, Node.fCompl );
00592     }
00593     if ( Node.Type == IVY_DEC_BUF )
00594     {
00595         pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree );
00596         return Ivy_NotCond( pResult, Node.fCompl );
00597     }
00598     if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR )
00599     {
00600         for ( i = 0; i < (int)Node.nFans; i++ )
00601         {
00602             Var = Ivy_DecGetVar( &Node, i );
00603             assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 );
00604             pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree );
00605             pChild = Ivy_NotCond( pChild, (Var & 1) );
00606             pNodes[i] = pChild;
00607         }
00608 
00609 //        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
00610 
00611         pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
00612         return Ivy_NotCond( pResult, Node.fCompl );
00613     }
00614     assert( Node.fCompl == 0 );
00615     if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
00616     {
00617         int VarC, Var1, Var0;
00618         VarC = Ivy_DecGetVar( &Node, 0 );
00619         Var1 = Ivy_DecGetVar( &Node, 1 );
00620         Var0 = Ivy_DecGetVar( &Node, 2 );
00621         pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree );
00622         pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree );
00623         pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree );
00624         assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
00625         pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) );
00626         pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
00627         pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
00628         if ( Node.Type == IVY_DEC_MUX )
00629             return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
00630         else
00631             return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
00632     }
00633     assert( 0 );
00634     return 0;
00635 }

static unsigned Ivy_TruthCofactor ( unsigned  uTruth,
int  Var 
) [inline, static]

Definition at line 89 of file ivyDsd.c.

00090 {
00091     unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0];
00092     int Shift = (1 << (Var >> 1));
00093     if ( Var & 1 )
00094         return uCofactor | (uCofactor << Shift);
00095     return uCofactor | (uCofactor >> Shift);
00096 }

static unsigned Ivy_TruthCofactor2 ( unsigned  uTruth,
int  Var0,
int  Var1 
) [inline, static]

Definition at line 98 of file ivyDsd.c.

00099 {
00100     return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 );
00101 }

static int Ivy_TruthCofactorIsConst ( unsigned  uTruth,
int  Var,
int  Cof,
int  Const 
) [inline, static]

Definition at line 76 of file ivyDsd.c.

00077 {
00078     if ( Const == 0 )
00079         return (uTruth & s_Masks[Var][Cof]) == 0;
00080     else
00081         return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof];
00082 }

static int Ivy_TruthCofactorIsOne ( unsigned  uTruth,
int  Var 
) [inline, static]

Definition at line 84 of file ivyDsd.c.

00085 {
00086     return (uTruth & s_Masks[Var][0]) == 0;
00087 }

int Ivy_TruthDecompose_rec ( unsigned  uTruth,
Vec_Int_t *  vTree 
) [static]

Function*************************************************************

Synopsis [Computes DSD of truth table.]

Description [Returns the number of topmost decomposition node.]

SideEffects []

SeeAlso []

Definition at line 212 of file ivyDsd.c.

00213 {
00214     Ivy_Dec_t Node;
00215     int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars;
00216     int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, i;
00217     unsigned uTruthCof, uCof0, uCof1;
00218 
00219     // get constant confactors
00220     Count0 = Count1 = Count2 = nSupp = 0;
00221     for ( i = 0; i < 5; i++ )
00222     {
00223         if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) )
00224             Vars0[Count0++] = (i << 1) | 0;
00225         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) )
00226             Vars0[Count0++] = (i << 1) | 1;
00227         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) )
00228             Vars1[Count1++] = (i << 1) | 0;
00229         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) )
00230             Vars1[Count1++] = (i << 1) | 1;
00231         else
00232         {
00233             uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 );
00234             uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 );
00235             if ( uCof0 == ~uCof1 )
00236                 Vars2[Count2++] = (i << 1) | 0;
00237             else if ( uCof0 != uCof1 )
00238                 Supp[nSupp++] = i;
00239         }
00240     }
00241     assert( Count0 == 0 || Count1 == 0 );
00242     assert( Count0 == 0 || Count2 == 0 );
00243     assert( Count1 == 0 || Count2 == 0 );
00244 
00245     // consider the case of a single variable
00246     if ( Count0 == 1 && nSupp == 0 )
00247         return Vars0[0];
00248 
00249     // consider more complex decompositions
00250     if ( Count0 == 0 && Count1 == 0 && Count2 == 0 )
00251         return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree );
00252 
00253     // extract the nodes
00254     Ivy_DecClear( &Node );
00255     if ( Count0 > 0 )
00256         nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND,  fCompl = 0;
00257     else if ( Count1 > 0 )
00258         nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND,  fCompl = 1, uTruth = ~uTruth;
00259     else if ( Count2 > 0 )
00260         nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0;
00261     else 
00262         assert( 0 );
00263     Node.nFans = nVars+(nSupp>0);
00264 
00265     // compute cofactor
00266     uTruthCof = uTruth;
00267     for ( i = 0; i < nVars; i++ )
00268     {
00269         uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] );
00270         Ivy_DecSetVar( &Node, i, pVars[i] );
00271     }
00272 
00273     if ( Node.Type == IVY_DEC_EXOR )
00274         fCompl ^= ((Node.nFans & 1) == 0);
00275 
00276     if ( nSupp > 0 )
00277     {
00278         assert( uTruthCof != 0 && ~uTruthCof != 0 );
00279         // call recursively
00280         RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree );
00281         // quit if non-decomposable
00282         if ( RetValue == -1 )
00283             return -1;
00284         // remove the complement from the child if the node is EXOR
00285         if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) )
00286         {
00287             fCompl ^= 1;
00288             RetValue ^= 1;
00289         }
00290         // set the new decomposition
00291         Ivy_DecSetVar( &Node, nVars, RetValue );
00292     }
00293     else if ( Node.Type == IVY_DEC_EXOR )
00294         fCompl ^= (uTruthCof == 0);
00295 
00296     Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00297     return ((Vec_IntSize(vTree)-1) << 1) | fCompl;
00298 }

static int Ivy_TruthDepends ( unsigned  uTruth,
int  Var 
) [inline, static]

Definition at line 104 of file ivyDsd.c.

00105 {
00106     return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1);
00107 }

int Ivy_TruthDsd ( unsigned  uTruth,
Vec_Int_t *  vTree 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Computes DSD of truth table of 5 variables or less.]

Description [Returns 1 if the function is a constant or is fully DSD decomposable using AND/EXOR/MUX gates.]

SideEffects []

SeeAlso []

Definition at line 159 of file ivyDsd.c.

00160 {
00161     Ivy_Dec_t Node;
00162     int i, RetValue;
00163     // set the PI variables
00164     Vec_IntClear( vTree );
00165     for ( i = 0; i < 5; i++ )
00166         Vec_IntPush( vTree, 0 );
00167     // check if it is a constant
00168     if ( uTruth == 0 || ~uTruth == 0 )
00169     {
00170         Ivy_DecClear( &Node );
00171         Node.Type = IVY_DEC_CONST1;
00172         Node.fCompl = (uTruth == 0);
00173         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00174         return 1;
00175     }
00176     // perform the decomposition
00177     RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
00178     if ( RetValue == -1 )
00179         return 0;
00180     // get the topmost node
00181     if ( (RetValue >> 1) < 5 )
00182     { // add buffer
00183         Ivy_DecClear( &Node );
00184         Node.Type = IVY_DEC_BUF;
00185         Node.fCompl = (RetValue & 1);
00186         Node.Fan0 = ((RetValue >> 1) << 1);
00187         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00188     }
00189     else if ( RetValue & 1 )
00190     { // check if the topmost node has to be complemented
00191         Node = Ivy_IntToDec( Vec_IntPop(vTree) );
00192         assert( Node.fCompl == 0 );
00193         Node.fCompl = (RetValue & 1);
00194         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00195     }
00196     if ( uTruth != Ivy_TruthDsdCompute(vTree) )
00197         printf( "Verification failed.\n" );
00198     return 1;
00199 }

unsigned Ivy_TruthDsdCompute ( Vec_Int_t *  vTree  ) 

Function*************************************************************

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file ivyDsd.c.

00472 {
00473     return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
00474 }

unsigned Ivy_TruthDsdCompute_rec ( int  iNode,
Vec_Int_t *  vTree 
)

Function*************************************************************

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 397 of file ivyDsd.c.

00398 {
00399     unsigned uTruthChild, uTruthTotal;
00400     int Var, i;
00401     // get the node
00402     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
00403     // compute the node function
00404     if ( Node.Type == IVY_DEC_CONST1 )
00405         return s_Masks[5][ !Node.fCompl ];
00406     if ( Node.Type == IVY_DEC_PI )
00407         return s_Masks[iNode][ !Node.fCompl ];
00408     if ( Node.Type == IVY_DEC_BUF )
00409     {
00410         uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree );
00411         return Node.fCompl? ~uTruthTotal : uTruthTotal;
00412     }
00413     if ( Node.Type == IVY_DEC_AND )
00414     {
00415         uTruthTotal = s_Masks[5][1];
00416         for ( i = 0; i < (int)Node.nFans; i++ )
00417         {
00418             Var = Ivy_DecGetVar( &Node, i );
00419             uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
00420             uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild;
00421         }
00422         return Node.fCompl? ~uTruthTotal : uTruthTotal;
00423     }
00424     if ( Node.Type == IVY_DEC_EXOR )
00425     {
00426         uTruthTotal = 0;
00427         for ( i = 0; i < (int)Node.nFans; i++ )
00428         {
00429             Var = Ivy_DecGetVar( &Node, i );
00430             uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
00431             assert( (Var & 1) == 0 );
00432         }
00433         return Node.fCompl? ~uTruthTotal : uTruthTotal;
00434     }
00435     assert( Node.fCompl == 0 );
00436     if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
00437     {
00438         unsigned uTruthChildC, uTruthChild1, uTruthChild0;
00439         int VarC, Var1, Var0;
00440         VarC = Ivy_DecGetVar( &Node, 0 );
00441         Var1 = Ivy_DecGetVar( &Node, 1 );
00442         Var0 = Ivy_DecGetVar( &Node, 2 );
00443         uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree );
00444         uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree );
00445         uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree );
00446         assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
00447         uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC;
00448         uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1;
00449         uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0;
00450         if ( Node.Type == IVY_DEC_MUX )
00451             return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0);
00452         else
00453             return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0);
00454     }
00455     assert( 0 );
00456     return 0;
00457 }

void Ivy_TruthDsdComputePrint ( unsigned  uTruth  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 671 of file ivyDsd.c.

00672 {
00673     static Vec_Int_t * vTree = NULL;
00674     if ( vTree == NULL )
00675         vTree = Vec_IntAlloc( 12 );
00676     if ( Ivy_TruthDsd( uTruth, vTree ) )
00677         Ivy_TruthDsdPrint( stdout, vTree );
00678     else
00679         printf( "Undecomposable\n" );
00680 }

void Ivy_TruthDsdPrint ( FILE *  pFile,
Vec_Int_t *  vTree 
)

Function*************************************************************

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 561 of file ivyDsd.c.

00562 {
00563     fprintf( pFile, "F = " );
00564     Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
00565     fprintf( pFile, "\n" );
00566 }

void Ivy_TruthDsdPrint_rec ( FILE *  pFile,
int  iNode,
Vec_Int_t *  vTree 
)

Function*************************************************************

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 487 of file ivyDsd.c.

00488 {
00489     int Var, i;
00490     // get the node
00491     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
00492     // compute the node function
00493     if ( Node.Type == IVY_DEC_CONST1 )
00494         fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") );
00495     else if ( Node.Type == IVY_DEC_PI )
00496         fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") );
00497     else if ( Node.Type == IVY_DEC_BUF )
00498     {
00499         Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree );
00500         fprintf( pFile, "%s", (Node.fCompl? "\'" : "") );
00501     }
00502     else if ( Node.Type == IVY_DEC_AND )
00503     {
00504         fprintf( pFile, "AND(" );
00505         for ( i = 0; i < (int)Node.nFans; i++ )
00506         {
00507             Var = Ivy_DecGetVar( &Node, i );
00508             Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
00509             fprintf( pFile, "%s", (Var & 1)? "\'" : "" );
00510             if ( i != (int)Node.nFans-1 )
00511                 fprintf( pFile, "," );
00512         }
00513         fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
00514     }
00515     else if ( Node.Type == IVY_DEC_EXOR )
00516     {
00517         fprintf( pFile, "EXOR(" );
00518         for ( i = 0; i < (int)Node.nFans; i++ )
00519         {
00520             Var = Ivy_DecGetVar( &Node, i );
00521             Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
00522             if ( i != (int)Node.nFans-1 )
00523                 fprintf( pFile, "," );
00524             assert( (Var & 1) == 0 );
00525         }
00526         fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
00527     }
00528     else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
00529     {
00530         int VarC, Var1, Var0;
00531         assert( Node.fCompl == 0 );
00532         VarC = Ivy_DecGetVar( &Node, 0 );
00533         Var1 = Ivy_DecGetVar( &Node, 1 );
00534         Var0 = Ivy_DecGetVar( &Node, 2 );
00535         fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" );
00536         Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree );
00537         fprintf( pFile, "%s", (VarC & 1)? "\'" : "" );
00538         fprintf( pFile, "," );
00539         Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree );
00540         fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" );
00541         fprintf( pFile, "," );
00542         Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree );
00543         fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" );
00544         fprintf( pFile, ")" );
00545     }
00546     else assert( 0 );
00547 }

int Ivy_TruthRecognizeMuxMaj ( unsigned  uTruth,
int *  pSupp,
int  nSupp,
Vec_Int_t *  vTree 
) [static]

Function*************************************************************

Synopsis [Returns a non-negative number if the truth table is a MUX.]

Description [If the truth table is a MUX, returns the variable as follows: first, control variable; second, positive cofactor; third, negative cofactor.]

SideEffects []

SeeAlso []

Definition at line 312 of file ivyDsd.c.

00313 {
00314     Ivy_Dec_t Node;
00315     int i, k, RetValue0, RetValue1;
00316     unsigned uCof0, uCof1, Num;
00317     char Count[3];
00318     assert( nSupp >= 3 );
00319     // start the node
00320     Ivy_DecClear( &Node );
00321     Node.Type = IVY_DEC_MUX;
00322     Node.nFans = 3;
00323     // try each of the variables
00324     for ( i = 0; i < nSupp; i++ )
00325     {
00326         // get the cofactors with respect to these variables
00327         uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 );
00328         uCof1 = Ivy_TruthCofactor( uTruth,  pSupp[i] << 1 );
00329         // go through all other variables and make sure 
00330         // each of them belongs to the support of one cofactor
00331         for ( k = 0; k < nSupp; k++ )
00332         {
00333             if ( k == i )
00334                 continue;
00335             if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) )
00336                 break;
00337         }
00338         if ( k < nSupp )
00339             continue;
00340         // MUX decomposition exists
00341         RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree );
00342         if ( RetValue0 == -1 )
00343             break;
00344         RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree );
00345         if ( RetValue1 == -1 )
00346             break;
00347         // both of them exist; create the node
00348         Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 );
00349         Ivy_DecSetVar( &Node, 1, RetValue1 );
00350         Ivy_DecSetVar( &Node, 2, RetValue0 );
00351         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00352         return ((Vec_IntSize(vTree)-1) << 1) | 0;
00353     }
00354     // check majority gate
00355     if ( nSupp > 3 )
00356         return -1;
00357     if ( Ivy_TruthWordCountOnes(uTruth) != 16 )
00358         return -1;
00359     // this is a majority gate; determine polarity
00360     Node.Type = IVY_DEC_MAJ;
00361     Count[0] = Count[1] = Count[2] = 0;
00362     for ( i = 0; i < 8; i++ )
00363     {
00364         Num = 0;
00365         for ( k = 0; k < 3; k++ )
00366             if ( i & (1 << k) )
00367                 Num |= (1 << pSupp[k]);
00368         assert( Num < 32 );
00369         if ( (uTruth & (1 << Num)) == 0 )
00370             continue;
00371         for ( k = 0; k < 3; k++ )
00372             if ( i & (1 << k) )
00373                 Count[k]++;
00374     }
00375     assert( Count[0] == 1 || Count[0] == 3 );
00376     assert( Count[1] == 1 || Count[1] == 3 );
00377     assert( Count[2] == 1 || Count[2] == 3 );
00378     Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) );
00379     Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) );
00380     Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) );
00381     Vec_IntPush( vTree, Ivy_DecToInt(Node) );
00382     return ((Vec_IntSize(vTree)-1) << 1) | 0;
00383 }

void Ivy_TruthTest (  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 729 of file ivyDsd.c.

00730 {
00731     FILE * pFile;
00732     char Buffer[100];
00733     unsigned uTruth;
00734     int i;
00735 
00736     pFile = fopen( "npn4.txt", "r" );
00737     for ( i = 0; i < 222; i++ )
00738 //    pFile = fopen( "npn5.txt", "r" );
00739 //    for ( i = 0; i < 616126; i++ )
00740     {
00741         fscanf( pFile, "%s", Buffer );
00742         Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
00743 //        Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
00744         uTruth |= (uTruth << 16);
00745 //        uTruth = ~uTruth;
00746         Ivy_TruthTestOne( uTruth );
00747     }
00748     fclose( pFile );
00749 }

void Ivy_TruthTest3 (  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 762 of file ivyDsd.c.

00763 {
00764     FILE * pFile;
00765     char Buffer[100];
00766     unsigned uTruth;
00767     int i;
00768 
00769     pFile = fopen( "npn3.txt", "r" );
00770     for ( i = 0; i < 14; i++ )
00771     {
00772         fscanf( pFile, "%s", Buffer );
00773         Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 );
00774         uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24);
00775         Ivy_TruthTestOne( uTruth );
00776     }
00777     fclose( pFile );
00778 }

void Ivy_TruthTest5 (  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 791 of file ivyDsd.c.

00792 {
00793     FILE * pFile;
00794     char Buffer[100];
00795     unsigned uTruth;
00796     int i;
00797 
00798 //    pFile = fopen( "npn4.txt", "r" );
00799 //    for ( i = 0; i < 222; i++ )
00800     pFile = fopen( "npn5.txt", "r" );
00801     for ( i = 0; i < 616126; i++ )
00802     {
00803         fscanf( pFile, "%s", Buffer );
00804 //        Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
00805         Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
00806 //        uTruth |= (uTruth << 16);
00807 //        uTruth = ~uTruth;
00808         Ivy_TruthTestOne( uTruth );
00809     }
00810     fclose( pFile );
00811 }

void Ivy_TruthTestOne ( unsigned  uTruth  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 693 of file ivyDsd.c.

00694 {
00695     static int Counter = 0;
00696     static Vec_Int_t * vTree = NULL;
00697     // decompose
00698     if ( vTree == NULL )
00699         vTree = Vec_IntAlloc( 12 );
00700 
00701     if ( !Ivy_TruthDsd( uTruth, vTree ) )
00702     {
00703 //        printf( "Undecomposable\n" );
00704     }
00705     else
00706     {
00707 //        nTruthDsd++;
00708         printf( "%5d : ", Counter++ );
00709         Extra_PrintBinary( stdout, &uTruth, 32 );
00710         printf( "  " );
00711         Ivy_TruthDsdPrint( stdout, vTree );
00712         if ( uTruth != Ivy_TruthDsdCompute(vTree) )
00713             printf( "Verification failed.\n" );
00714     }
00715 //    Vec_IntFree( vTree );
00716 }

static int Ivy_TruthWordCountOnes ( unsigned  uWord  )  [inline, static]

Definition at line 67 of file ivyDsd.c.

00068 {
00069     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00070     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00071     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00072     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00073     return  (uWord & 0x0000FFFF) + (uWord>>16);
00074 }

Variable Documentation

unsigned s_Masks[6][2] [static]
Initial value:
 {
    { 0x55555555, 0xAAAAAAAA },
    { 0x33333333, 0xCCCCCCCC },
    { 0x0F0F0F0F, 0xF0F0F0F0 },
    { 0x00FF00FF, 0xFF00FF00 },
    { 0x0000FFFF, 0xFFFF0000 },
    { 0x00000000, 0xFFFFFFFF }
}

Definition at line 58 of file ivyDsd.c.

Generated on Tue Jan 5 12:18:23 2010 for abc70930 by  doxygen 1.6.1