summaryrefslogtreecommitdiffstats
path: root/src/aig/ivy/ivyDsd.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ivy/ivyDsd.c')
-rw-r--r--src/aig/ivy/ivyDsd.c819
1 files changed, 0 insertions, 819 deletions
diff --git a/src/aig/ivy/ivyDsd.c b/src/aig/ivy/ivyDsd.c
deleted file mode 100644
index 3b8a2e68..00000000
--- a/src/aig/ivy/ivyDsd.c
+++ /dev/null
@@ -1,819 +0,0 @@
-/**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"
-
-////////////////////////////////////////////////////////////////////////
-/// 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 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;
- 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;
-}
-
-/**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 );
-}
-
-/**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 );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 15:58:05 +0000