| /**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 $] |
| |
| ***********************************************************************/ |
| |
| #include "ivy.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // decomposition types |
| typedef enum { |
| 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; |
| |
| typedef struct Ivy_Dec_t_ Ivy_Dec_t; |
| struct Ivy_Dec_t_ |
| { |
| unsigned Type : 4; // the node type (PI, CONST1, AND, EXOR, MUX, PRIME) |
| unsigned fCompl : 1; // shows if node is complemented (root node only) |
| unsigned nFans : 3; // the number of fanins |
| unsigned Fan0 : 4; // fanin 0 |
| unsigned Fan1 : 4; // fanin 1 |
| unsigned Fan2 : 4; // fanin 2 |
| unsigned Fan3 : 4; // fanin 3 |
| unsigned Fan4 : 4; // fanin 4 |
| unsigned Fan5 : 4; // fanin 5 |
| }; |
| |
| static inline int Ivy_DecToInt( Ivy_Dec_t m ) { union { Ivy_Dec_t x; int y; } v; v.x = m; return v.y; } |
| static inline Ivy_Dec_t Ivy_IntToDec( int m ) { union { Ivy_Dec_t x; int y; } v; v.y = m; return v.x; } |
| static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *pNode = Ivy_IntToDec(0); } |
| |
| //static inline int Ivy_DecToInt( Ivy_Dec_t Node ) { return *((int *)&Node); } |
| //static inline Ivy_Dec_t Ivy_IntToDec( int Node ) { return *((Ivy_Dec_t *)&Node); } |
| //static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *((int *)pNode) = 0; } |
| |
| |
| static unsigned s_Masks[6][2] = { |
| { 0x55555555, 0xAAAAAAAA }, |
| { 0x33333333, 0xCCCCCCCC }, |
| { 0x0F0F0F0F, 0xF0F0F0F0 }, |
| { 0x00FF00FF, 0xFF00FF00 }, |
| { 0x0000FFFF, 0xFFFF0000 }, |
| { 0x00000000, 0xFFFFFFFF } |
| }; |
| |
| static inline int Ivy_TruthWordCountOnes( unsigned uWord ) |
| { |
| 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); |
| } |
| |
| static inline int Ivy_TruthCofactorIsConst( unsigned uTruth, int Var, int Cof, int Const ) |
| { |
| if ( Const == 0 ) |
| return (uTruth & s_Masks[Var][Cof]) == 0; |
| else |
| return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof]; |
| } |
| |
| static inline int Ivy_TruthCofactorIsOne( unsigned uTruth, int Var ) |
| { |
| return (uTruth & s_Masks[Var][0]) == 0; |
| } |
| |
| static inline unsigned Ivy_TruthCofactor( unsigned uTruth, int Var ) |
| { |
| 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 inline unsigned Ivy_TruthCofactor2( unsigned uTruth, int Var0, int Var1 ) |
| { |
| return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 ); |
| } |
| |
| // returns 1 if the truth table depends on this var (var is regular interger var) |
| static inline int Ivy_TruthDepends( unsigned uTruth, int Var ) |
| { |
| return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1); |
| } |
| |
| static inline void Ivy_DecSetVar( Ivy_Dec_t * pNode, int iNum, unsigned Var ) |
| { |
| 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 inline unsigned Ivy_DecGetVar( Ivy_Dec_t * pNode, int iNum ) |
| { |
| 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 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 nTruthDsd; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// 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 [] |
| |
| ***********************************************************************/ |
| int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ) |
| { |
| 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; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes DSD of truth table.] |
| |
| Description [Returns the number of topmost decomposition node.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree ) |
| { |
| Ivy_Dec_t Node; |
| int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars = NULL; |
| int nSupp, Count0, Count1, Count2, nVars = 0, RetValue, fCompl = 0, 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; |
| } |
| |
| /**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 [] |
| |
| ***********************************************************************/ |
| int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree ) |
| { |
| 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; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of decomposition tree for verification.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Ivy_TruthDsdCompute_rec( int iNode, Vec_Int_t * vTree ) |
| { |
| 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; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes truth table of decomposition tree for verification.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ) |
| { |
| return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prints the decomposition tree.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthDsdPrint_rec( FILE * pFile, int iNode, Vec_Int_t * vTree ) |
| { |
| 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 ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prints the decomposition tree.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ) |
| { |
| fprintf( pFile, "F = " ); |
| Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree ); |
| fprintf( pFile, "\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Implement DSD in the AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNode, Vec_Int_t * vTree ) |
| { |
| 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; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Implement DSD in the AIG.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ) |
| { |
| 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 ); |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthDsdComputePrint( unsigned uTruth ) |
| { |
| 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" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthTestOne( unsigned uTruth ) |
| { |
| 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 ); |
| } |
| |
| #if 0 |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthTest() |
| { |
| FILE * pFile; |
| char Buffer[100]; |
| unsigned uTruth; |
| int i; |
| |
| pFile = fopen( "npn4.txt", "r" ); |
| for ( i = 0; i < 222; i++ ) |
| // pFile = fopen( "npn5.txt", "r" ); |
| // for ( i = 0; i < 616126; i++ ) |
| { |
| fscanf( pFile, "%s", Buffer ); |
| Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); |
| // Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); |
| uTruth |= (uTruth << 16); |
| // uTruth = ~uTruth; |
| Ivy_TruthTestOne( uTruth ); |
| } |
| fclose( pFile ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthTest3() |
| { |
| FILE * pFile; |
| char Buffer[100]; |
| unsigned uTruth; |
| int i; |
| |
| pFile = fopen( "npn3.txt", "r" ); |
| for ( i = 0; i < 14; i++ ) |
| { |
| fscanf( pFile, "%s", Buffer ); |
| Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 ); |
| uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); |
| Ivy_TruthTestOne( uTruth ); |
| } |
| fclose( pFile ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ivy_TruthTest5() |
| { |
| FILE * pFile; |
| char Buffer[100]; |
| unsigned uTruth; |
| int i; |
| |
| // pFile = fopen( "npn4.txt", "r" ); |
| // for ( i = 0; i < 222; i++ ) |
| pFile = fopen( "npn5.txt", "r" ); |
| for ( i = 0; i < 616126; i++ ) |
| { |
| fscanf( pFile, "%s", Buffer ); |
| // Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); |
| Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); |
| // uTruth |= (uTruth << 16); |
| // uTruth = ~uTruth; |
| Ivy_TruthTestOne( uTruth ); |
| } |
| fclose( pFile ); |
| } |
| |
| #endif |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
