#include "ivy.h"

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 }
	DECLARATIONS ///. More...

Functions
static int	Ivy_DecToInt (Ivy_Dec_t m)

static Ivy_Dec_t	Ivy_IntToDec (int m)

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)
	FUNCTION DEFINITIONS ///. More...

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)

Variables
static unsigned	s_Masks [6][2]

Typedef Documentation

typedef struct Ivy_Dec_t_ Ivy_Dec_t

Definition at line 42 of file ivyDsd.c.

Enumeration Type Documentation

enum Ivy_DecType_t

DECLARATIONS ///.

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

]

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 31 of file ivyDsd.c.

              { 
     IVY_DEC_PI,             // 0: var
     IVY_DEC_CONST1,         // 1: CONST1
     IVY_DEC_BUF,            // 2: BUF
     IVY_DEC_AND,            // 3: AND
     IVY_DEC_EXOR,           // 4: EXOR
     IVY_DEC_MUX,            // 5: MUX
     IVY_DEC_MAJ,            // 6: MAJ
     IVY_DEC_PRIME           // 7: undecomposable
 } Ivy_DecType_t;

Function Documentation

static void Ivy_DecClear ( Ivy_Dec_t * pNode )

inlinestatic

Definition at line 58 of file ivyDsd.c.

58 { *pNode = Ivy_IntToDec(0); }

Ivy_IntToDec

static Ivy_Dec_t Ivy_IntToDec(int m)

Definition: ivyDsd.c:57

static unsigned Ivy_DecGetVar	(	Ivy_Dec_t *	pNode,
		int	iNum
	)

inlinestatic

Definition at line 130 of file ivyDsd.c.

 {
     assert( iNum >= 0 && iNum <= 5 );
     switch( iNum )
     {
         case 0: return pNode->Fan0;
         case 1: return pNode->Fan1;
         case 2: return pNode->Fan2;
         case 3: return pNode->Fan3;
         case 4: return pNode->Fan4;
         case 5: return pNode->Fan5;
     }
     return ~0;
 }

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

inlinestatic

Definition at line 116 of file ivyDsd.c.

 {
     assert( iNum >= 0 && iNum <= 5 );
     switch( iNum )
     {
         case 0: pNode->Fan0 = Var; break;
         case 1: pNode->Fan1 = Var; break;
         case 2: pNode->Fan2 = Var; break;
         case 3: pNode->Fan3 = Var; break;
         case 4: pNode->Fan4 = Var; break;
         case 5: pNode->Fan5 = Var; break;
     }
 }

static int Ivy_DecToInt ( Ivy_Dec_t m )

inlinestatic

Definition at line 56 of file ivyDsd.c.

56 { union { Ivy_Dec_t x; int y; } v; v.x = m; return v.y; }

Ivy_Dec_t_

Definition: ivyDsd.c:43

static Ivy_Dec_t Ivy_IntToDec ( int m )

inlinestatic

Definition at line 57 of file ivyDsd.c.

57 { union { Ivy_Dec_t x; int y; } v; v.y = m; return v.x; }

Ivy_Dec_t_

Definition: ivyDsd.c:43

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 655 of file ivyDsd.c.

 {
     int Entry, i;
     // implement latches on the frontier (TEMPORARY!!!)
     Vec_IntForEachEntry( vFront, Entry, i )
         Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
     // recursively construct the tree
     return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
 }

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 586 of file ivyDsd.c.

 {
     Ivy_Obj_t * pResult, * pChild, * pNodes[16];
     int Var, i;
     // get the node
     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
     // compute the node function
     if ( Node.Type == IVY_DEC_CONST1 )
         return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl );
     if ( Node.Type == IVY_DEC_PI )
     {
         pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) );
         return Ivy_NotCond( pResult, Node.fCompl );
     }
     if ( Node.Type == IVY_DEC_BUF )
     {
         pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree );
         return Ivy_NotCond( pResult, Node.fCompl );
     }
     if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR )
     {
         for ( i = 0; i < (int)Node.nFans; i++ )
         {
             Var = Ivy_DecGetVar( &Node, i );
             assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 );
             pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree );
             pChild = Ivy_NotCond( pChild, (Var & 1) );
             pNodes[i] = pChild;
         }
 
 //        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
 
         pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
         return Ivy_NotCond( pResult, Node.fCompl );
     }
     assert( Node.fCompl == 0 );
     if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
     {
         int VarC, Var1, Var0;
         VarC = Ivy_DecGetVar( &Node, 0 );
         Var1 = Ivy_DecGetVar( &Node, 1 );
         Var0 = Ivy_DecGetVar( &Node, 2 );
         pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree );
         pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree );
         pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree );
         assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
         pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) );
         pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
         pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
         if ( Node.Type == IVY_DEC_MUX )
             return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
         else
             return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
     }
     assert( 0 );
     return 0;
 }

static unsigned Ivy_TruthCofactor	(	unsigned	uTruth,
		int	Var
	)

inlinestatic

Definition at line 96 of file ivyDsd.c.

 {
     unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0];
     int Shift = (1 << (Var >> 1));
     if ( Var & 1 )
         return uCofactor | (uCofactor << Shift);
     return uCofactor | (uCofactor >> Shift);
 }

static unsigned Ivy_TruthCofactor2	(	unsigned	uTruth,
		int	Var0,
		int	Var1
	)

inlinestatic

Definition at line 105 of file ivyDsd.c.

 {
     return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 );
 }

static int Ivy_TruthCofactorIsConst	(	unsigned	uTruth,
		int	Var,
		int	Cof,
		int	Const
	)

inlinestatic

Definition at line 83 of file ivyDsd.c.

 {
     if ( Const == 0 )
         return (uTruth & s_Masks[Var][Cof]) == 0;
     else
         return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof];
 }

static int Ivy_TruthCofactorIsOne	(	unsigned	uTruth,
		int	Var
	)

inlinestatic

Definition at line 91 of file ivyDsd.c.

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

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 219 of file ivyDsd.c.

 {
     Ivy_Dec_t Node;
     int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars;
     int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, i;
     unsigned uTruthCof, uCof0, uCof1;
 
     // get constant confactors
     Count0 = Count1 = Count2 = nSupp = 0;
     for ( i = 0; i < 5; i++ )
     {
         if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) )
             Vars0[Count0++] = (i << 1) | 0;
         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) )
             Vars0[Count0++] = (i << 1) | 1;
         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) )
             Vars1[Count1++] = (i << 1) | 0;
         else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) )
             Vars1[Count1++] = (i << 1) | 1;
         else
         {
             uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 );
             uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 );
             if ( uCof0 == ~uCof1 )
                 Vars2[Count2++] = (i << 1) | 0;
             else if ( uCof0 != uCof1 )
                 Supp[nSupp++] = i;
         }
     }
     assert( Count0 == 0 || Count1 == 0 );
     assert( Count0 == 0 || Count2 == 0 );
     assert( Count1 == 0 || Count2 == 0 );
 
     // consider the case of a single variable
     if ( Count0 == 1 && nSupp == 0 )
         return Vars0[0];
 
     // consider more complex decompositions
     if ( Count0 == 0 && Count1 == 0 && Count2 == 0 )
         return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree );
 
     // extract the nodes
     Ivy_DecClear( &Node );
     if ( Count0 > 0 )
         nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND,  fCompl = 0;
     else if ( Count1 > 0 )
         nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND,  fCompl = 1, uTruth = ~uTruth;
     else if ( Count2 > 0 )
         nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0;
     else 
         assert( 0 );
     Node.nFans = nVars+(nSupp>0);
 
     // compute cofactor
     uTruthCof = uTruth;
     for ( i = 0; i < nVars; i++ )
     {
         uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] );
         Ivy_DecSetVar( &Node, i, pVars[i] );
     }
 
     if ( Node.Type == IVY_DEC_EXOR )
         fCompl ^= ((Node.nFans & 1) == 0);
 
     if ( nSupp > 0 )
     {
         assert( uTruthCof != 0 && ~uTruthCof != 0 );
         // call recursively
         RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree );
         // quit if non-decomposable
         if ( RetValue == -1 )
             return -1;
         // remove the complement from the child if the node is EXOR
         if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) )
         {
             fCompl ^= 1;
             RetValue ^= 1;
         }
         // set the new decomposition
         Ivy_DecSetVar( &Node, nVars, RetValue );
     }
     else if ( Node.Type == IVY_DEC_EXOR )
         fCompl ^= (uTruthCof == 0);
 
     Vec_IntPush( vTree, Ivy_DecToInt(Node) );
     return ((Vec_IntSize(vTree)-1) << 1) | fCompl;
 }

static int Ivy_TruthDepends	(	unsigned	uTruth,
		int	Var
	)

inlinestatic

Definition at line 111 of file ivyDsd.c.

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

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 166 of file ivyDsd.c.

 {
     Ivy_Dec_t Node;
     int i, RetValue;
     // set the PI variables
     Vec_IntClear( vTree );
     for ( i = 0; i < 5; i++ )
         Vec_IntPush( vTree, 0 );
     // check if it is a constant
     if ( uTruth == 0 || ~uTruth == 0 )
     {
         Ivy_DecClear( &Node );
         Node.Type = IVY_DEC_CONST1;
         Node.fCompl = (uTruth == 0);
         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
         return 1;
     }
     // perform the decomposition
     RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
     if ( RetValue == -1 )
         return 0;
     // get the topmost node
     if ( (RetValue >> 1) < 5 )
     { // add buffer
         Ivy_DecClear( &Node );
         Node.Type = IVY_DEC_BUF;
         Node.fCompl = (RetValue & 1);
         Node.Fan0 = ((RetValue >> 1) << 1);
         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
     }
     else if ( RetValue & 1 )
     { // check if the topmost node has to be complemented
         Node = Ivy_IntToDec( Vec_IntPop(vTree) );
         assert( Node.fCompl == 0 );
         Node.fCompl = (RetValue & 1);
         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
     }
     if ( uTruth != Ivy_TruthDsdCompute(vTree) )
         printf( "Verification failed.\n" );
     return 1;
 }

unsigned Ivy_TruthDsdCompute ( Vec_Int_t * vTree )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 478 of file ivyDsd.c.

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

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 404 of file ivyDsd.c.

 {
     unsigned uTruthChild, uTruthTotal;
     int Var, i;
     // get the node
     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
     // compute the node function
     if ( Node.Type == IVY_DEC_CONST1 )
         return s_Masks[5][ !Node.fCompl ];
     if ( Node.Type == IVY_DEC_PI )
         return s_Masks[iNode][ !Node.fCompl ];
     if ( Node.Type == IVY_DEC_BUF )
     {
         uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree );
         return Node.fCompl? ~uTruthTotal : uTruthTotal;
     }
     if ( Node.Type == IVY_DEC_AND )
     {
         uTruthTotal = s_Masks[5][1];
         for ( i = 0; i < (int)Node.nFans; i++ )
         {
             Var = Ivy_DecGetVar( &Node, i );
             uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
             uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild;
         }
         return Node.fCompl? ~uTruthTotal : uTruthTotal;
     }
     if ( Node.Type == IVY_DEC_EXOR )
     {
         uTruthTotal = 0;
         for ( i = 0; i < (int)Node.nFans; i++ )
         {
             Var = Ivy_DecGetVar( &Node, i );
             uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
             assert( (Var & 1) == 0 );
         }
         return Node.fCompl? ~uTruthTotal : uTruthTotal;
     }
     assert( Node.fCompl == 0 );
     if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
     {
         unsigned uTruthChildC, uTruthChild1, uTruthChild0;
         int VarC, Var1, Var0;
         VarC = Ivy_DecGetVar( &Node, 0 );
         Var1 = Ivy_DecGetVar( &Node, 1 );
         Var0 = Ivy_DecGetVar( &Node, 2 );
         uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree );
         uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree );
         uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree );
         assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
         uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC;
         uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1;
         uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0;
         if ( Node.Type == IVY_DEC_MUX )
             return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0);
         else
             return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0);
     }
     assert( 0 );
     return 0;
 }

void Ivy_TruthDsdComputePrint ( unsigned uTruth )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 678 of file ivyDsd.c.

 {
     static Vec_Int_t * vTree = NULL;
     if ( vTree == NULL )
         vTree = Vec_IntAlloc( 12 );
     if ( Ivy_TruthDsd( uTruth, vTree ) )
         Ivy_TruthDsdPrint( stdout, vTree );
     else
         printf( "Undecomposable\n" );
 }

void Ivy_TruthDsdPrint	(	FILE *	pFile,
		Vec_Int_t *	vTree
	)

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file ivyDsd.c.

 {
     fprintf( pFile, "F = " );
     Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
     fprintf( pFile, "\n" );
 }

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

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file ivyDsd.c.

 {
     int Var, i;
     // get the node
     Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
     // compute the node function
     if ( Node.Type == IVY_DEC_CONST1 )
         fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") );
     else if ( Node.Type == IVY_DEC_PI )
         fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") );
     else if ( Node.Type == IVY_DEC_BUF )
     {
         Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree );
         fprintf( pFile, "%s", (Node.fCompl? "\'" : "") );
     }
     else if ( Node.Type == IVY_DEC_AND )
     {
         fprintf( pFile, "AND(" );
         for ( i = 0; i < (int)Node.nFans; i++ )
         {
             Var = Ivy_DecGetVar( &Node, i );
             Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
             fprintf( pFile, "%s", (Var & 1)? "\'" : "" );
             if ( i != (int)Node.nFans-1 )
                 fprintf( pFile, "," );
         }
         fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
     }
     else if ( Node.Type == IVY_DEC_EXOR )
     {
         fprintf( pFile, "EXOR(" );
         for ( i = 0; i < (int)Node.nFans; i++ )
         {
             Var = Ivy_DecGetVar( &Node, i );
             Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
             if ( i != (int)Node.nFans-1 )
                 fprintf( pFile, "," );
             assert( (Var & 1) == 0 );
         }
         fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
     }
     else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
     {
         int VarC, Var1, Var0;
         assert( Node.fCompl == 0 );
         VarC = Ivy_DecGetVar( &Node, 0 );
         Var1 = Ivy_DecGetVar( &Node, 1 );
         Var0 = Ivy_DecGetVar( &Node, 2 );
         fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" );
         Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree );
         fprintf( pFile, "%s", (VarC & 1)? "\'" : "" );
         fprintf( pFile, "," );
         Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree );
         fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" );
         fprintf( pFile, "," );
         Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree );
         fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" );
         fprintf( pFile, ")" );
     }
     else assert( 0 );
 }

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 319 of file ivyDsd.c.

 {
     Ivy_Dec_t Node;
     int i, k, RetValue0, RetValue1;
     unsigned uCof0, uCof1, Num;
     char Count[3];
     assert( nSupp >= 3 );
     // start the node
     Ivy_DecClear( &Node );
     Node.Type = IVY_DEC_MUX;
     Node.nFans = 3;
     // try each of the variables
     for ( i = 0; i < nSupp; i++ )
     {
         // get the cofactors with respect to these variables
         uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 );
         uCof1 = Ivy_TruthCofactor( uTruth,  pSupp[i] << 1 );
         // go through all other variables and make sure 
         // each of them belongs to the support of one cofactor
         for ( k = 0; k < nSupp; k++ )
         {
             if ( k == i )
                 continue;
             if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) )
                 break;
         }
         if ( k < nSupp )
             continue;
         // MUX decomposition exists
         RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree );
         if ( RetValue0 == -1 )
             break;
         RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree );
         if ( RetValue1 == -1 )
             break;
         // both of them exist; create the node
         Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 );
         Ivy_DecSetVar( &Node, 1, RetValue1 );
         Ivy_DecSetVar( &Node, 2, RetValue0 );
         Vec_IntPush( vTree, Ivy_DecToInt(Node) );
         return ((Vec_IntSize(vTree)-1) << 1) | 0;
     }
     // check majority gate
     if ( nSupp > 3 )
         return -1;
     if ( Ivy_TruthWordCountOnes(uTruth) != 16 )
         return -1;
     // this is a majority gate; determine polarity
     Node.Type = IVY_DEC_MAJ;
     Count[0] = Count[1] = Count[2] = 0;
     for ( i = 0; i < 8; i++ )
     {
         Num = 0;
         for ( k = 0; k < 3; k++ )
             if ( i & (1 << k) )
                 Num |= (1 << pSupp[k]);
         assert( Num < 32 );
         if ( (uTruth & (1 << Num)) == 0 )
             continue;
         for ( k = 0; k < 3; k++ )
             if ( i & (1 << k) )
                 Count[k]++;
     }
     assert( Count[0] == 1 || Count[0] == 3 );
     assert( Count[1] == 1 || Count[1] == 3 );
     assert( Count[2] == 1 || Count[2] == 3 );
     Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) );
     Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) );
     Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) );
     Vec_IntPush( vTree, Ivy_DecToInt(Node) );
     return ((Vec_IntSize(vTree)-1) << 1) | 0;
 }

void Ivy_TruthTestOne ( unsigned uTruth )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 700 of file ivyDsd.c.

 {
     static int Counter = 0;
     static Vec_Int_t * vTree = NULL;
     // decompose
     if ( vTree == NULL )
         vTree = Vec_IntAlloc( 12 );
 
     if ( !Ivy_TruthDsd( uTruth, vTree ) )
     {
 //        printf( "Undecomposable\n" );
     }
     else
     {
 //        nTruthDsd++;
         printf( "%5d : ", Counter++ );
         Extra_PrintBinary( stdout, &uTruth, 32 );
         printf( "  " );
         Ivy_TruthDsdPrint( stdout, vTree );
         if ( uTruth != Ivy_TruthDsdCompute(vTree) )
             printf( "Verification failed.\n" );
     }
 //    Vec_IntFree( vTree );
 }

static int Ivy_TruthWordCountOnes ( unsigned uWord )

inlinestatic

Definition at line 74 of file ivyDsd.c.

 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
     return  (uWord & 0x0000FFFF) + (uWord>>16);
 }

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 65 of file ivyDsd.c.

Data Structures

Typedefs

Enumerations

Functions

Variables

Typedef Documentation

Enumeration Type Documentation

Function Documentation

Variable Documentation