summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/hop/hop.h10
-rw-r--r--src/aig/hop/hopMan.c18
-rw-r--r--src/aig/hop/hopObj.c11
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abc/abcFunc.c15
-rw-r--r--src/base/abc/abcSop.c6
-rw-r--r--src/base/abci/abc.c96
-rw-r--r--src/base/abci/abcHaig.c385
-rw-r--r--src/base/abci/abcIf.c1
-rw-r--r--src/base/abci/abcRenode.c14
-rw-r--r--src/base/abci/abcVerify.c29
-rw-r--r--src/base/io/io.c63
-rw-r--r--src/base/io/ioReadDsd.c308
-rw-r--r--src/base/io/ioWriteBench.c2
-rw-r--r--src/base/io/io_.c12
-rw-r--r--src/base/io/module.make1
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/map/if/ifMan.c3
-rw-r--r--src/opt/kit/kit.h25
-rw-r--r--src/opt/kit/kitDsd.c689
-rw-r--r--src/opt/kit/kitTruth.c126
-rw-r--r--src/opt/kit/module.make1
22 files changed, 1674 insertions, 144 deletions
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 34124599..44f5ac8e 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -81,7 +81,7 @@ struct Hop_Man_t_
// AIG nodes
Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs
- Vec_Ptr_t * vNodes; // the array of all nodes (optional)
+ Vec_Ptr_t * vObjs; // the array of all nodes (optional)
Hop_Obj_t * pConst1; // the constant 1 node
Hop_Obj_t Ghost; // the ghost node
// AIG node counters
@@ -131,6 +131,8 @@ static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_N
static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; }
static inline Hop_Obj_t * Hop_ManGhost( Hop_Man_t * p ) { return &p->Ghost; }
static inline Hop_Obj_t * Hop_ManPi( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i); }
+static inline Hop_Obj_t * Hop_ManPo( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i); }
+static inline Hop_Obj_t * Hop_ManObj( Hop_Man_t * p, int i ) { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline Hop_Edge_t Hop_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
static inline int Hop_EdgeId( Hop_Edge_t Edge ) { return Edge >> 1; }
@@ -223,10 +225,10 @@ static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p )
pTemp = p->pListFree;
p->pListFree = *((Hop_Obj_t **)pTemp);
memset( pTemp, 0, sizeof(Hop_Obj_t) );
- if ( p->vNodes )
+ if ( p->vObjs )
{
- assert( p->nCreated == Vec_PtrSize(p->vNodes) );
- Vec_PtrPush( p->vNodes, pTemp );
+ assert( p->nCreated == Vec_PtrSize(p->vObjs) );
+ Vec_PtrPush( p->vObjs, pTemp );
}
pTemp->Id = p->nCreated++;
return pTemp;
diff --git a/src/aig/hop/hopMan.c b/src/aig/hop/hopMan.c
index 4fa52fbd..b7858564 100644
--- a/src/aig/hop/hopMan.c
+++ b/src/aig/hop/hopMan.c
@@ -94,10 +94,10 @@ void Hop_ManStop( Hop_Man_t * p )
if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); }
// Hop_TableProfile( p );
- if ( p->vChunks ) Hop_ManStopMemory( p );
- if ( p->vPis ) Vec_PtrFree( p->vPis );
- if ( p->vPos ) Vec_PtrFree( p->vPos );
- if ( p->vNodes ) Vec_PtrFree( p->vNodes );
+ if ( p->vChunks ) Hop_ManStopMemory( p );
+ if ( p->vPis ) Vec_PtrFree( p->vPis );
+ if ( p->vPos ) Vec_PtrFree( p->vPos );
+ if ( p->vObjs ) Vec_PtrFree( p->vObjs );
free( p->pTable );
free( p );
}
@@ -115,20 +115,20 @@ void Hop_ManStop( Hop_Man_t * p )
***********************************************************************/
int Hop_ManCleanup( Hop_Man_t * p )
{
- Vec_Ptr_t * vNodes;
+ Vec_Ptr_t * vObjs;
Hop_Obj_t * pNode;
int i, nNodesOld;
assert( p->fRefCount );
nNodesOld = Hop_ManNodeNum(p);
// collect roots of dangling nodes
- vNodes = Vec_PtrAlloc( 100 );
+ vObjs = Vec_PtrAlloc( 100 );
Hop_ManForEachNode( p, pNode, i )
if ( Hop_ObjRefs(pNode) == 0 )
- Vec_PtrPush( vNodes, pNode );
+ Vec_PtrPush( vObjs, pNode );
// recursively remove dangling nodes
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( vObjs, pNode, i )
Hop_ObjDelete_rec( p, pNode );
- Vec_PtrFree( vNodes );
+ Vec_PtrFree( vObjs );
return nNodesOld - Hop_ManNodeNum(p);
}
diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c
index c4430abd..c8e70dd3 100644
--- a/src/aig/hop/hopObj.c
+++ b/src/aig/hop/hopObj.c
@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
else
pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
// set the phase
-// pObj->fPhase = Hop_ObjFaninPhase(pDriver);
+ pObj->fPhase = Hop_ObjFaninPhase(pDriver);
// update node counters of the manager
p->nObjs[AIG_PO]++;
return pObj;
@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj
else
pObj->nRefs = Hop_ObjLevelNew( pObj );
// set the phase
-// pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
+ pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
// add the node to the structural hash table
Hop_TableInsert( p, pObj );
}
@@ -236,9 +236,10 @@ void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
***********************************************************************/
Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj )
{
- if ( Hop_Regular(pObj)->pData == NULL )
- return Hop_Regular(pObj);
- return Hop_ObjRepr( Hop_Regular(pObj)->pData );
+ assert( !Hop_IsComplement(pObj) );
+ if ( pObj->pData == NULL || pObj->pData == pObj )
+ return pObj;
+ return Hop_ObjRepr( pObj->pData );
}
/**Function*************************************************************
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 3a278927..ececd26f 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -616,7 +616,7 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth );
+extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 03f41f3b..2bfad15b 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -866,7 +866,7 @@ unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int
SeeAlso []
***********************************************************************/
-unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
+unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
{
static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
@@ -899,9 +899,18 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
return pTruth;
}
// set elementary truth tables at the leaves
+ assert( nVars <= Hop_ManPiNum(p) );
assert( Hop_ManPiNum(p) <= 8 );
- Hop_ManForEachPi( p, pObj, i )
- pObj->pData = (void *)uTruths[i];
+ if ( fMsbFirst )
+ {
+ Hop_ManForEachPi( p, pObj, i )
+ pObj->pData = (void *)uTruths[nVars-1-i];
+ }
+ else
+ {
+ Hop_ManForEachPi( p, pObj, i )
+ pObj->pData = (void *)uTruths[i];
+ }
// clear the marks and compute the truth table
pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index a39bd7bf..01fa8e13 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -855,7 +855,8 @@ char * Abc_SopFromTruthBin( char * pTruth )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
- if ( Mint & (1 << b) )
+ if ( Mint & (1 << (nVars-1-b)) )
+// if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
@@ -921,7 +922,8 @@ char * Abc_SopFromTruthHex( char * pTruth )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
- if ( Mint & (1 << b) )
+ if ( Mint & (1 << (nVars-1-b)) )
+// if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4aa13733..9138d897 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -47,6 +47,7 @@ static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintXCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintDsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -61,7 +62,7 @@ static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandIfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -194,6 +195,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_xcut", Abc_CommandPrintXCut, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "print_dsd", Abc_CommandPrintDsd, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show", Abc_CommandShow, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 );
@@ -208,7 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "sweep", Abc_CommandSweep, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
- Cmd_CommandAdd( pAbc, "Synthesis", "ifs", Abc_CommandIfs, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
@@ -1463,6 +1465,92 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fUseLibrary;
+
+ extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fUseLibrary = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'l':
+ fUseLibrary ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ // get the truth table of the first output
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "Currently works only for logic networks.\n" );
+ return 1;
+ }
+ Abc_NtkToAig( pNtk );
+ // convert it to truth table
+ {
+ Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+ Vec_Int_t * vMemory = Vec_IntAlloc( 100 );
+ unsigned * pTruth;
+ if ( !Abc_ObjIsNode(pObj) )
+ {
+ fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" );
+ return 1;
+ }
+ if ( Abc_ObjFaninNum(pObj) > 8 )
+ {
+ fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
+ return 1;
+ }
+ pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 1 );
+ if ( Hop_IsComplement(pObj->pData) )
+ Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
+ Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
+ printf( "\n" );
+ Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
+ Vec_IntFree( vMemory );
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: print_dsd [-h]\n" );
+ fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" );
+// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -2649,7 +2737,7 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
@@ -2756,7 +2844,7 @@ int Abc_CommandIfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: ifs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
+ fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" );
fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index 87fada22..a0ed5906 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -57,8 +57,8 @@ int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
assert( pObj->pEquiv == NULL );
// start the HOP package
p = Hop_ManStart();
- p->vNodes = Vec_PtrAlloc( 4096 );
- Vec_PtrPush( p->vNodes, Hop_ManConst1(p) );
+ p->vObjs = Vec_PtrAlloc( 4096 );
+ Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
// map the constant node
Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
// map the CIs
@@ -149,7 +149,6 @@ void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
-
/**Function*************************************************************
Synopsis [Collects the nodes in the classes.]
@@ -163,18 +162,18 @@ void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
***********************************************************************/
Vec_Ptr_t * Abc_NtkHaigCollectMembers( Hop_Man_t * p )
{
- Vec_Ptr_t * vNodes;
+ Vec_Ptr_t * vObjs;
Hop_Obj_t * pObj;
int i;
- vNodes = Vec_PtrAlloc( 4098 );
- Vec_PtrForEachEntry( p->vNodes, pObj, i )
+ vObjs = Vec_PtrAlloc( 4098 );
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
{
if ( pObj->pData == NULL )
continue;
pObj->pData = Hop_ObjRepr( pObj );
- Vec_PtrPush( vNodes, pObj );
+ Vec_PtrPush( vObjs, pObj );
}
- return vNodes;
+ return vObjs;
}
/**Function*************************************************************
@@ -235,10 +234,15 @@ Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers )
{
pRepr = pObj->pData;
assert( pRepr->pData == pRepr );
- pRepr->pData = NULL;
+// pRepr->pData = NULL;
Vec_PtrWriteEntry( vClasses, i, pRepr );
Vec_PtrPush( vMembers, pObj );
}
+
+ Vec_PtrForEachEntry( vMembers, pObj, i )
+ if ( pObj->pData == pObj )
+ pObj->pData = NULL;
+
/*
Vec_PtrForEachEntry( vMembers, pObj, i )
{
@@ -258,6 +262,122 @@ Vec_Ptr_t * Abc_NtkHaigCreateClasses( Vec_Ptr_t * vMembers )
return vClasses;
}
+/**Function*************************************************************
+
+ Synopsis [Counts how many data members have non-trivial fanout.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkHaigCountFans( Hop_Man_t * p )
+{
+ Hop_Obj_t * pObj;
+ int i, Counter = 0;
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( pObj->pData == NULL )
+ continue;
+ if ( Hop_ObjRefs(pObj) > 0 )
+ Counter++;
+ }
+ printf( "The number of class members with fanouts = %5d.\n", Counter );
+ return Counter;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjReprHop( Hop_Obj_t * pObj )
+{
+ Hop_Obj_t * pRepr;
+ assert( pObj->pNext != NULL );
+ if ( pObj->pData == NULL )
+ return pObj->pNext;
+ pRepr = pObj->pData;
+ assert( pRepr->pData == pRepr );
+ return Hop_NotCond( pRepr->pNext, pObj->fPhase ^ pRepr->fPhase );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Hop_Obj_t * Hop_ObjChild0Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); }
+static inline Hop_Obj_t * Hop_ObjChild1Hop( Hop_Obj_t * pObj ) { return Hop_NotCond( Hop_ObjReprHop(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); }
+
+/**Function*************************************************************
+
+ Synopsis [Stops history AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Man_t * Abc_NtkHaigReconstruct( Hop_Man_t * p )
+{
+ Hop_Man_t * pNew;
+ Hop_Obj_t * pObj;
+ int i, Counter = 0;
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ pObj->pNext = NULL;
+ // start the HOP package
+ pNew = Hop_ManStart();
+ pNew->vObjs = Vec_PtrAlloc( p->nCreated );
+ Vec_PtrPush( pNew->vObjs, Hop_ManConst1(pNew) );
+ // map the constant node
+ Hop_ManConst1(p)->pNext = Hop_ManConst1(pNew);
+ // map the CIs
+ Hop_ManForEachPi( p, pObj, i )
+ pObj->pNext = Hop_ObjCreatePi(pNew);
+ // map the internal nodes
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( !Hop_ObjIsNode(pObj) )
+ continue;
+ pObj->pNext = Hop_And( pNew, Hop_ObjChild0Hop(pObj), Hop_ObjChild1Hop(pObj) );
+// assert( !Hop_IsComplement(pObj->pNext) );
+ if ( Hop_ManConst1(pNew) == Hop_Regular(pObj->pNext) )
+ Counter++;
+ if ( pObj->pData ) // member of the class
+ Hop_Regular(pObj->pNext)->pData = Hop_Regular(((Hop_Obj_t *)pObj->pData)->pNext);
+ }
+ printf( " Counter = %d.\n", Counter );
+ // transfer the POs
+ Hop_ManForEachPo( p, pObj, i )
+ Hop_ObjCreatePo( pNew, Hop_ObjChild0Hop(pObj) );
+ // check the new manager
+ if ( !Hop_ManCheck(pNew) )
+ {
+ printf( "Abc_NtkHaigReconstruct: Check for History AIG has failed.\n" );
+ Hop_ManStop(pNew);
+ return NULL;
+ }
+ return pNew;
+}
+
/**Function*************************************************************
@@ -277,7 +397,7 @@ int Abc_NtkHaigCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld )
if ( pNode == pOld )
return 1;
// check the trivial cases
- if ( Abc_ObjIsPi(pNode) )
+ if ( Abc_ObjIsCi(pNode) )
return 0;
assert( Abc_ObjIsNode(pNode) );
// if this node is already visited, skip
@@ -324,36 +444,8 @@ int Abc_NtkHaigCheckTfi( Abc_Ntk_t * pNtk, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
SeeAlso []
***********************************************************************/
-static inline Abc_Obj_t * Hop_ObjReprAbc( Hop_Obj_t * pObj )
-{
- Hop_Obj_t * pRepr;
- Abc_Obj_t * pObjAbcThis, * pObjAbcRepr;
- assert( pObj->pNext != NULL );
- if ( pObj->pData == NULL )
- return (Abc_Obj_t *)pObj->pNext;
- pRepr = pObj->pData;
- assert( pRepr->pData == NULL );
- pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
- pObjAbcRepr = (Abc_Obj_t *)pRepr->pNext;
- assert( !Abc_ObjIsComplement(pObjAbcThis) );
- assert( !Abc_ObjIsComplement(pObjAbcRepr) );
- return Abc_ObjNotCond( pObjAbcRepr, pObjAbcRepr->fPhase ^ pObjAbcThis->fPhase );
-// return (Abc_Obj_t *)pObj->pNext;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Abc_Obj_t * Hop_ObjChild0Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin0(pObj)), Hop_ObjFaninC0(pObj) ); }
-static inline Abc_Obj_t * Hop_ObjChild1Abc( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( Hop_ObjReprAbc(Hop_ObjFanin1(pObj)), Hop_ObjFaninC1(pObj) ); }
+static inline Abc_Obj_t * Hop_ObjChild0Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin0(pObj)->pNext, Hop_ObjFaninC0(pObj) ); }
+static inline Abc_Obj_t * Hop_ObjChild1Next( Hop_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Hop_ObjFanin1(pObj)->pNext, Hop_ObjFaninC1(pObj) ); }
/**Function*************************************************************
@@ -369,13 +461,10 @@ static inline Abc_Obj_t * Hop_ObjChild1Abc( Hop_Obj_t * pObj ) { return Abc_ObjN
Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
{
Abc_Ntk_t * pNtkAig;
- Abc_Obj_t * pObjAbcThis, * pObjAbcRepr;
- Abc_Obj_t * pObjOld, * pObjNew;
+ Abc_Obj_t * pObjOld, * pObjAbcThis, * pObjAbcRepr;
Hop_Obj_t * pObj;
int i;
-
- assert( p->nCreated == Vec_PtrSize(p->vNodes) );
- assert( Hop_ManPoNum(p) == 0 );
+ assert( p->nCreated == Vec_PtrSize(p->vObjs) );
// start the new network
pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -383,51 +472,42 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
// transfer new nodes to the PIs of HOP
Hop_ManConst1(p)->pNext = (Hop_Obj_t *)Abc_AigConst1( pNtkAig );
Hop_ManForEachPi( p, pObj, i )
- pObj->pNext = (Hop_Obj_t *)Abc_NtkPi( pNtkAig, i );
+ pObj->pNext = (Hop_Obj_t *)Abc_NtkCi( pNtkAig, i );
// construct new nodes
- Vec_PtrForEachEntry( p->vNodes, pObj, i )
- if ( Hop_ObjIsNode(pObj) )
- pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Abc(pObj), Hop_ObjChild1Abc(pObj) );
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( !Hop_ObjIsNode(pObj) )
+ continue;
+ pObj->pNext = (Hop_Obj_t *)Abc_AigAnd( pNtkAig->pManFunc, Hop_ObjChild0Next(pObj), Hop_ObjChild1Next(pObj) );
+ assert( !Hop_IsComplement(pObj->pNext) );
+ }
// set the COs
Abc_NtkForEachCo( pNtk, pObjOld, i )
- {
- pObjNew = Hop_ObjReprAbc( Abc_ObjFanin0(pObjOld)->pEquiv );
- pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(pObjOld) );
- Abc_ObjAddFanin( pObjOld->pCopy, pObjNew );
- }
+ Abc_ObjAddFanin( pObjOld->pCopy, Hop_ObjChild0Next(Hop_ManPo(p,i)) );
- // create choice nodes
- Vec_PtrForEachEntry( p->vNodes, pObj, i )
+ // construct choice nodes
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
{
- Abc_Obj_t * pTemp;
+ // skip the node without choices
if ( pObj->pData == NULL )
continue;
-
- pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
- pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext;
- assert( !Abc_ObjIsComplement(pObjAbcThis) );
- assert( !Abc_ObjIsComplement(pObjAbcRepr) );
-
- // skip the case when the class is constant 1
- if ( pObjAbcRepr == Abc_AigConst1(pNtkAig) )
- continue;
-
- // skip the case when pObjAbcThis is part of the class already
- for ( pTemp = pObjAbcRepr; pTemp; pTemp = pTemp->pData )
- if ( pTemp == pObjAbcThis )
- break;
- if ( pTemp )
- continue;
-
-// assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 );
- if ( Abc_ObjFanoutNum(pObjAbcThis) > 0 )
+ // skip the representative of the class
+ if ( pObj->pData == pObj )
continue;
-// assert( pObjAbcThis->pData == NULL );
- if ( pObjAbcThis->pData )
+ // do not create choices for constant 1 and PIs
+ if ( !Hop_ObjIsNode(pObj->pData) )
continue;
-
+ // get the corresponding new nodes
+ pObjAbcThis = (Abc_Obj_t *)pObj->pNext;
+ pObjAbcRepr = (Abc_Obj_t *)((Hop_Obj_t *)pObj->pData)->pNext;
+ // the new node cannot be already in the class
+ assert( pObjAbcThis->pData == NULL );
+ // the new node cannot have fanouts
+ assert( Abc_ObjFanoutNum(pObjAbcThis) == 0 );
+ // these should be different nodes
+ assert( pObjAbcRepr != pObjAbcThis );
// do not create choices if there is a path from pObjAbcThis to pObjAbcRepr
if ( !Abc_NtkHaigCheckTfi( pNtkAig, pObjAbcRepr, pObjAbcThis ) )
{
@@ -454,6 +534,110 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
/**Function*************************************************************
+ Synopsis [Resets representatives.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkHaigResetReprsOld( Hop_Man_t * pMan )
+{
+ Vec_Ptr_t * vMembers, * vClasses;
+
+ // collect members of the classes and make them point to reprs
+ vMembers = Abc_NtkHaigCollectMembers( pMan );
+ printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) );
+
+ // create classes
+ vClasses = Abc_NtkHaigCreateClasses( vMembers );
+ printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses),
+ (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) );
+
+ Vec_PtrFree( vMembers );
+ Vec_PtrFree( vClasses );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resets representatives.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkHaigResetReprs( Hop_Man_t * p )
+{
+ Hop_Obj_t * pObj, * pRepr;
+ int i, nClasses, nMembers, nFanouts, nNormals;
+ // clear self-classes
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ // fix the strange situation of double-loop
+ pRepr = pObj->pData;
+ if ( pRepr && pRepr->pData == pObj )
+ pRepr->pData = pRepr;
+ // remove self-loops
+ if ( pObj->pData == pObj )
+ pObj->pData = NULL;
+ }
+ // set representatives
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( pObj->pData == NULL )
+ continue;
+ // get representative of the node
+ pRepr = Hop_ObjRepr( pObj );
+ pRepr->pData = pRepr;
+ // set the representative
+ pObj->pData = pRepr;
+ }
+ // make each class point to the smallest topological order
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( pObj->pData == NULL )
+ continue;
+ pRepr = Hop_ObjRepr( pObj );
+ if ( pRepr->Id > pObj->Id )
+ {
+ pRepr->pData = pObj;
+ pObj->pData = pObj;
+ }
+ else
+ pObj->pData = pRepr;
+ }
+ // count classes, members, and fanouts - and verify
+ nMembers = nClasses = nFanouts = nNormals = 0;
+ Vec_PtrForEachEntry( p->vObjs, pObj, i )
+ {
+ if ( pObj->pData == NULL )
+ continue;
+ // count members
+ nMembers++;
+ // count the classes and fanouts
+ if ( pObj->pData == pObj )
+ nClasses++;
+ else if ( Hop_ObjRefs(pObj) > 0 )
+ nFanouts++;
+ else
+ nNormals++;
+ // compare representatives
+ pRepr = Hop_ObjRepr( pObj );
+ assert( pObj->pData == pRepr );
+ assert( pRepr->Id <= pObj->Id );
+ }
+// printf( "Nodes = %7d. Member = %7d. Classes = %6d. Fanouts = %6d. Normals = %6d.\n",
+// Hop_ManNodeNum(p), nMembers, nClasses, nFanouts, nNormals );
+ return nFanouts;
+}
+
+/**Function*************************************************************
+
Synopsis [Stops history AIG.]
Description []
@@ -465,8 +649,10 @@ Abc_Ntk_t * Abc_NtkHaigRecreateAig( Abc_Ntk_t * pNtk, Hop_Man_t * p )
***********************************************************************/
Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
{
+ Hop_Man_t * pMan, * pManTemp;
Abc_Ntk_t * pNtkAig;
- Vec_Ptr_t * vMembers, * vClasses;
+ Abc_Obj_t * pObj;
+ int i;
// check if HAIG is available
assert( Abc_NtkIsStrash(pNtk) );
@@ -476,26 +662,39 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
return NULL;
}
// convert HOP package into AIG with choices
-
// print HAIG stats
-// Hop_ManPrintStats( pNtk->pHaig ); // USES DATA!!!
+// Hop_ManPrintStats( pMan ); // USES DATA!!!
- // collect members of the classes and make them point to reprs
- vMembers = Abc_NtkHaigCollectMembers( pNtk->pHaig );
- printf( "Collected %6d class members.\n", Vec_PtrSize(vMembers) );
+ // add the POs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
- // create classes
- vClasses = Abc_NtkHaigCreateClasses( vMembers );
- printf( "Collected %6d classes. (Ave = %5.2f)\n", Vec_PtrSize(vClasses),
- (float)(Vec_PtrSize(vMembers))/Vec_PtrSize(vClasses) );
- Vec_PtrFree( vMembers );
- Vec_PtrFree( vClasses );
+ // clean the old network
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pObj->pEquiv = NULL;
+ pMan = pNtk->pHaig;
+ pNtk->pHaig = 0;
+ // iteratively reconstruct the HOP manager to create choice nodes
+ while ( Abc_NtkHaigResetReprs( pMan ) )
+ {
+ pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+ Hop_ManStop( pManTemp );
+ }
+/*
+ pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+ Hop_ManStop( pManTemp );
+ Abc_NtkHaigResetReprs( pMan );
+
+ pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
+ Hop_ManStop( pManTemp );
+ Abc_NtkHaigResetReprs( pMan );
+*/
// traverse in the topological order and create new AIG
- pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pNtk->pHaig );
+ pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
+ Hop_ManStop( pMan );
// free HAIG
- Abc_NtkHaigStop( pNtk );
return pNtkAig;
}
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 00861e1b..46f7dd13 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -150,6 +150,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
// set up the choice node
if ( Abc_AigNodeIsChoice( pNode ) )
{
+ pIfMan->nChoices++;
for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 17db7ed9..6423d10c 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -38,6 +38,8 @@ static DdManager * s_pDd = NULL;
static Vec_Int_t * s_vMemory = NULL;
static Vec_Int_t * s_vMemory2 = NULL;
+static int nDsdCounter = 0;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -62,6 +64,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
if ( Abc_NtkGetChoiceNum( pNtk ) )
printf( "Performing renoding with choices.\n" );
+ nDsdCounter = 0;
+
// set defaults
memset( pPars, 0, sizeof(If_Par_t) );
// user-controlable paramters
@@ -136,6 +140,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
s_vMemory2 = NULL;
}
+ printf( "Decomposed %d functions.\n", nDsdCounter );
+
return pNtkNew;
}
@@ -154,6 +160,14 @@ int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
{
Kit_Graph_t * pGraph;
int i, nNodes;
+
+extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+if ( If_CutLeaveNum(pCut) == 8 )
+{
+ nDsdCounter++;
+ Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+}
+
pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
if ( pGraph == NULL )
{
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index b7a7d4b9..1054e071 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -256,13 +256,25 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
nOutputs = 0;
Abc_NtkForEachPo( pMiter, pObj, i )
{
- // get the cone of this output
- pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
- if ( Abc_ObjFaninC0(pObj) )
- Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
- // solve the cone
- // RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
- RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+ if ( Abc_ObjFanin0(pObj) == Abc_AigConst1(pMiter) )
+ {
+ if ( Abc_ObjFaninC0(pObj) ) // complemented -> const 0
+ RetValue = 1;
+ else
+ RetValue = 0;
+ pMiterPart = NULL;
+ }
+ else
+ {
+ // get the cone of this output
+ pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
+ if ( Abc_ObjFaninC0(pObj) )
+ Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
+ // solve the cone
+ // RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
+ RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+ }
+
if ( RetValue == -1 )
{
printf( "Networks are undecided (resource limits is reached).\r" );
@@ -286,7 +298,8 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
}
// if ( pMiter->pModel )
// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
- Abc_NtkDelete( pMiterPart );
+ if ( pMiterPart )
+ Abc_NtkDelete( pMiterPart );
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index cc907eb2..a7801f71 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -31,6 +31,7 @@ static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -82,6 +83,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
@@ -483,6 +485,67 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * pString;
+ int fCheck;
+ int c;
+ extern Abc_Ntk_t * Io_ReadDsd( char * pFormula );
+
+ fCheck = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 1 )
+ goto usage;
+ // get the input file name
+ pString = argv[globalUtilOptind];
+ // read the file using the corresponding file reader
+ pNtk = Io_ReadDsd( pString );
+ if ( pNtk == NULL )
+ return 1;
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
+ fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
+ fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
+ fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
+ fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(c,!d,e*f))*79B3(g,h,i,k))\n" );
+ fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
+ fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );
+ fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Ctrl,Data1,Data0))\n" );
+ fprintf( pAbc->Err, "\t The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
+ fprintf( pAbc->Err, "\t The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
+ fprintf( pAbc->Err, "\t No spaces are allowed in the formula.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c
new file mode 100644
index 00000000..1ab726e5
--- /dev/null
+++ b/src/base/io/ioReadDsd.c
@@ -0,0 +1,308 @@
+/**CFile****************************************************************
+
+ FileName [ioReadDsd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedure to read network from file.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Finds the end of the part.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Io_ReadDsdFindEnd( char * pCur )
+{
+ char * pEnd;
+ int nParts = 0;
+ assert( *pCur == '(' );
+ for ( pEnd = pCur; *pEnd; pEnd++ )
+ {
+ if ( *pEnd == '(' )
+ nParts++;
+ else if ( *pEnd == ')' )
+ nParts--;
+ if ( nParts == 0 )
+ return pEnd;
+ }
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Splits the formula into parts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadDsdStrSplit( char * pCur, char * pParts[], int * pTypeXor )
+{
+ int fAnd = 0, fXor = 0, fPri = 0, nParts = 0;
+ assert( *pCur );
+ // process the parts
+ while ( 1 )
+ {
+ // save the current part
+ pParts[nParts++] = pCur;
+ // skip the complement
+ if ( *pCur == '!' )
+ pCur++;
+ // skip var
+ if ( *pCur >= 'a' && *pCur <= 'z' )
+ pCur++;
+ else
+ {
+ // skip hex truth table
+ while ( (*pCur >= '0' && *pCur <= '9') || (*pCur >= 'A' && *pCur <= 'F') )
+ pCur++;
+ // process parantheses
+ if ( *pCur != '(' )
+ {
+ printf( "Cannot find the opening paranthesis.\n" );
+ break;
+ }
+ // find the corresponding closing paranthesis
+ pCur = Io_ReadDsdFindEnd( pCur );
+ if ( pCur == NULL )
+ {
+ printf( "Cannot find the closing paranthesis.\n" );
+ break;
+ }
+ pCur++;
+ }
+ // check the end
+ if ( *pCur == 0 )
+ break;
+ // check symbol
+ if ( *pCur != '*' && *pCur != '+' && *pCur != ',' )
+ {
+ printf( "Wrong separating symbol.\n" );
+ break;
+ }
+ // remember the symbol
+ fAnd |= (*pCur == '*');
+ fXor |= (*pCur == '+');
+ fPri |= (*pCur == ',');
+ *pCur++ = 0;
+ }
+ // check separating symbols
+ if ( fAnd + fXor + fPri > 1 )
+ {
+ printf( "Different types of separating symbol ennPartsed.\n" );
+ return 0;
+ }
+ *pTypeXor = fXor;
+ return nParts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively parses the formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
+{
+ Abc_Obj_t * pObj, * pFanin;
+ char * pEnd, * pParts[32];
+ int i, nParts, TypeExor;
+
+ // consider complemented formula
+ if ( *pCur == '!' )
+ {
+ pObj = Io_ReadDsd_rec( pNtk, pCur + 1, NULL );
+ return Abc_NtkCreateNodeInv( pNtk, pObj );
+ }
+ if ( *pCur == '(' )
+ {
+ assert( pCur[strlen(pCur)-1] == ')' );
+ pCur[strlen(pCur)-1] = 0;
+ nParts = Io_ReadDsdStrSplit( pCur+1, pParts, &TypeExor );
+ if ( nParts == 0 )
+ {
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ pObj = Abc_NtkCreateNode( pNtk );
+ if ( pSop )
+ {
+// for ( i = nParts - 1; i >= 0; i-- )
+ for ( i = 0; i < nParts; i++ )
+ {
+ pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
+ if ( pFanin == NULL )
+ return NULL;
+ Abc_ObjAddFanin( pObj, pFanin );
+ }
+ }
+ else
+ {
+ for ( i = 0; i < nParts; i++ )
+ {
+ pFanin = Io_ReadDsd_rec( pNtk, pParts[i], NULL );
+ if ( pFanin == NULL )
+ return NULL;
+ Abc_ObjAddFanin( pObj, pFanin );
+ }
+ }
+ if ( pSop )
+ pObj->pData = Abc_SopRegister( pNtk->pManFunc, pSop );
+ else if ( TypeExor )
+ pObj->pData = Abc_SopCreateXorSpecial( pNtk->pManFunc, nParts );
+ else
+ pObj->pData = Abc_SopCreateAnd( pNtk->pManFunc, nParts, NULL );
+ return pObj;
+ }
+ if ( *pCur >= 'a' && *pCur <= 'z' )
+ {
+ assert( *(pCur+1) == 0 );
+ return Abc_NtkPi( pNtk, *pCur - 'a' );
+ }
+
+ // skip hex truth table
+ pEnd = pCur;
+ while ( (*pEnd >= '0' && *pEnd <= '9') || (*pEnd >= 'A' && *pEnd <= 'F') )
+ pEnd++;
+ if ( *pEnd != '(' )
+ {
+ printf( "Cannot find the end of hexidecimal truth table.\n" );
+ return NULL;
+ }
+
+ // parse the truth table
+ *pEnd = 0;
+ pSop = Abc_SopFromTruthHex( pCur );
+ *pEnd = '(';
+ pObj = Io_ReadDsd_rec( pNtk, pEnd, pSop );
+ free( pSop );
+ return pObj;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the DSD network of the formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadDsd( char * pForm )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObj, * pTop;
+ Vec_Ptr_t * vNames;
+ char * pCur, * pFormCopy;
+ int i, nInputs;
+
+ // count the number of elementary variables
+ nInputs = 0;
+ for ( pCur = pForm; *pCur; pCur++ )
+ if ( *pCur >= 'a' && *pCur <= 'z' )
+ nInputs = ABC_MAX( nInputs, *pCur - 'a' );
+ nInputs++;
+
+ // create the network
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+ pNtk->pName = Extra_UtilStrsav( "dsd" );
+
+ // create PIs
+ vNames = Abc_NodeGetFakeNames( nInputs );
+ for ( i = 0; i < nInputs; i++ )
+ Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), Vec_PtrEntry(vNames, i), NULL );
+ Abc_NodeFreeNames( vNames );
+
+ // transform the formula by inserting parantheses
+ // this transforms strings like PRIME(a,b,cd) into (PRIME((a),(b),(cd)))
+ pCur = pFormCopy = ALLOC( char, 3 * strlen(pForm) + 10 );
+ *pCur++ = '(';
+ for ( ; *pForm; pForm++ )
+ if ( *pForm == '(' )
+ {
+ *pCur++ = '(';
+ *pCur++ = '(';
+ }
+ else if ( *pForm == ')' )
+ {
+ *pCur++ = ')';
+ *pCur++ = ')';
+ }
+ else if ( *pForm == ',' )
+ {
+ *pCur++ = ')';
+ *pCur++ = ',';
+ *pCur++ = '(';
+ }
+ else
+ *pCur++ = *pForm;
+ *pCur++ = ')';
+ *pCur = 0;
+
+ // parse the formula
+ pObj = Io_ReadDsd_rec( pNtk, pFormCopy, NULL );
+ free( pFormCopy );
+ if ( pObj == NULL )
+ return NULL;
+
+ // create output
+ pTop = Abc_NtkCreatePo(pNtk);
+ Abc_ObjAssignName( pTop, "F", NULL );
+ Abc_ObjAddFanin( pTop, pObj );
+
+ // create the only PO
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ fprintf( stdout, "Io_ReadDsd(): Network check has failed.\n" );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ return pNtk;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index e63489f4..b8b3b83b 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
nFanins = Abc_ObjFaninNum(pNode);
assert( nFanins <= 8 );
// compute the truth table
- pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth );
+ pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
if ( Hop_IsComplement(pNode->pData) )
Extra_TruthNot( pTruth, pTruth, nFanins );
// consider simple cases
diff --git a/src/base/io/io_.c b/src/base/io/io_.c
index 7721545a..62dd60e5 100644
--- a/src/base/io/io_.c
+++ b/src/base/io/io_.c
@@ -28,6 +28,18 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 4b6f762c..bb35a7fc 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -5,6 +5,7 @@ SRC += src/base/io/io.c \
src/base/io/ioReadBlif.c \
src/base/io/ioReadBlifAig.c \
src/base/io/ioReadBlifMv.c \
+ src/base/io/ioReadDsd.c \
src/base/io/ioReadEdif.c \
src/base/io/ioReadEqn.c \
src/base/io/ioReadPla.c \
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 7e22707f..759a9801 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -139,6 +139,7 @@ struct If_Man_t_
unsigned * puTemp[4]; // used for the truth table computation
int SortMode; // one of the three sorting modes
int fNextRound; // set to 1 after the first round
+ int nChoices; // the number of choice nodes
// sequential mapping
Vec_Ptr_t * vLatchOrder; // topological ordering of latches
Vec_Int_t * vLags; // sequentail lags of all nodes
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 20b2657f..77f4930a 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -480,7 +480,8 @@ void If_ManSetupSetAll( If_Man_t * p )
if ( p->pPars->fVerbose )
{
- printf( "Total memory = %7.2f Mb. Peak cut memory = %7.2f Mb. \n",
+ printf( "Node = %7d. Ch = %5d. Total mem = %7.2f Mb. Peak cut mem = %7.2f Mb.\n",
+ If_ManAndNum(p), p->nChoices,
1.0 * (p->nObjBytes + 2*sizeof(void *)) * If_ManObjNum(p) / (1<<20),
1.0 * p->nSetBytes * nCrossCut / (1<<20) );
}
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index ed2745e3..5d37a9e9 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -153,13 +153,22 @@ static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t
static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
-static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
-static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
+static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
static inline void Kit_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); }
static inline void Kit_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); }
static inline int Kit_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; }
+static inline int Kit_WordFindFirstBit( unsigned uWord )
+{
+ int i;
+ for ( i = 0; i < 32; i++ )
+ if ( uWord & (1 << i) )
+ return i;
+ return -1;
+}
static inline int Kit_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -183,6 +192,14 @@ static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars
return 0;
return 1;
}
+static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+ int w;
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( pIn0[w] != ~pIn1[w] )
+ return 0;
+ return 1;
+}
static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
{
int w;
@@ -332,9 +349,11 @@ extern void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nV
extern void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
extern int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars );
-extern int Kit_TruthSupport( unsigned * pTruth, int nVars );
+extern unsigned Kit_TruthSupport( unsigned * pTruth, int nVars );
extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
+extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
+extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
new file mode 100644
index 00000000..0068a29a
--- /dev/null
+++ b/src/opt/kit/kitDsd.c
@@ -0,0 +1,689 @@
+/**CFile****************************************************************
+
+ FileName [kitDsd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Computation kit.]
+
+ Synopsis [Performs disjoint-support decomposition based on truth tables.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Dec 6, 2006.]
+
+ Revision [$Id: kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Dsd_Ntk_t_ Dsd_Ntk_t;
+typedef struct Dsd_Obj_t_ Dsd_Obj_t;
+
+// network types
+typedef enum {
+ KIT_DSD_NONE = 0, // 0: unknown
+ KIT_DSD_CONST1, // 1: constant 1
+ KIT_DSD_VAR, // 2: elementary variable
+ KIT_DSD_AND, // 3: multi-input AND
+ KIT_DSD_XOR, // 4: multi-input XOR
+ KIT_DSD_MUX, // 5: multiplexer
+ KIT_DSD_PRIME // 6: arbitrary function of 3+ variables
+} Kit_Dsd_t;
+
+struct Dsd_Obj_t_
+{
+ unsigned uSupp; // the support of this node
+ unsigned Id : 6; // the number of this node
+ unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
+ unsigned fMark : 1; // finished checking output
+ unsigned Offset : 16; // offset to the truth table
+ unsigned nFans : 6; // the number of fanins of this node
+ unsigned char pFans[0]; // the fanin literals
+};
+
+struct Dsd_Ntk_t_
+{
+ unsigned char nVars; // at most 16 (perhaps 18?)
+ unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars)
+ unsigned char nNodes; // the number of nodes
+ unsigned char Root; // the root of the tree
+ unsigned * pMem; // memory for the truth tables (memory manager?)
+ Dsd_Obj_t * pNodes[0]; // the nodes
+};
+
+static inline unsigned Dsd_ObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
+static inline unsigned * Dsd_ObjTruth( Dsd_Obj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
+static inline Dsd_Obj_t * Dsd_NtkRoot( Dsd_Ntk_t * pNtk ) { return pNtk->pNodes[(pNtk->Root >> 1) - pNtk->nVars]; }
+
+#define Dsd_NtkForEachObj( pNtk, pObj, i ) \
+ for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
+#define Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i ) \
+ for ( i = 0; (i < (pObj)->nFans) && (((pFanin) = ((pObj)->pFans[i] < 2*pNtk->nVars)? NULL: (pNtk)->pNodes[((pObj)->pFans[i]>>1) - pNtk->nVars]), 1) && ((iVar) = (pObj)->pFans[i], 1); i++ )
+
+extern void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk );
+extern Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
+extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates the DSD node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dsd_Obj_t * Dsd_ObjAlloc( Dsd_Ntk_t * pNtk, Kit_Dsd_t Type, int nFans )
+{
+ Dsd_Obj_t * pObj;
+ int nSize = sizeof(Dsd_Obj_t) + sizeof(unsigned) * (Dsd_ObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans));
+ pObj = (Dsd_Obj_t *)ALLOC( char, nSize );
+ memset( pObj, 0, nSize );
+ pObj->Type = Type;
+ pObj->Id = pNtk->nVars + pNtk->nNodes;
+ pObj->nFans = nFans;
+ pObj->Offset = Dsd_ObjOffset( nFans );
+ // add the object
+ assert( pNtk->nNodes < pNtk->nNodesAlloc );
+ pNtk->pNodes[pNtk->nNodes++] = pObj;
+ return pObj;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the DSD node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
+{
+ free( pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocates the DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dsd_Ntk_t * Kit_DsdNtkAlloc( unsigned * pTruth, int nVars )
+{
+ Dsd_Ntk_t * pNtk;
+ int nSize = sizeof(Dsd_Ntk_t) + sizeof(void *) * nVars;
+ // allocate the network
+ pNtk = (Dsd_Ntk_t *)ALLOC( char, nSize );
+ memset( pNtk, 0, nSize );
+ pNtk->nVars = nVars;
+ pNtk->nNodesAlloc = nVars;
+ pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocate the DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk )
+{
+ Dsd_Obj_t * pObj;
+ unsigned i;
+ Dsd_NtkForEachObj( pNtk, pObj, i )
+ free( pObj );
+ free( pNtk->pMem );
+ free( pNtk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints the hex unsigned into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
+{
+ int nDigits, Digit, k;
+ nDigits = (1 << nFans) / 4;
+ for ( k = nDigits - 1; k >= 0; k-- )
+ {
+ Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15);
+ if ( Digit < 10 )
+ fprintf( pFile, "%d", Digit );
+ else
+ fprintf( pFile, "%c", 'A' + Digit-10 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively print the DSD formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+{
+ Dsd_Obj_t * pFanin;
+ unsigned iVar, i;
+ char Symbol;
+
+ if ( pObj->Type == KIT_DSD_CONST1 )
+ {
+ assert( pObj->nFans == 0 );
+ fprintf( pFile, "Const1" );
+ return;
+ }
+
+ if ( pObj->Type == KIT_DSD_VAR )
+ assert( pObj->nFans == 1 );
+
+ if ( pObj->Type == KIT_DSD_AND )
+ Symbol = '*';
+ else if ( pObj->Type == KIT_DSD_XOR )
+ Symbol = '+';
+ else
+ Symbol = ',';
+
+ if ( pObj->Type == KIT_DSD_MUX )
+ fprintf( pFile, "CA" );
+ else if ( pObj->Type == KIT_DSD_PRIME )
+ Kit_DsdPrintHex( stdout, Dsd_ObjTruth(pObj), pObj->nFans );
+
+ fprintf( pFile, "(" );
+ Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
+ {
+ if ( iVar & 1 )
+ fprintf( pFile, "!" );
+ if ( pFanin )
+ Kit_DsdPrint_rec( pFile, pNtk, pFanin );
+ else
+ fprintf( pFile, "%c", 'a' + (pNtk->nVars - 1 - (iVar >> 1)) );
+ if ( i < pObj->nFans - 1 )
+ fprintf( pFile, "%c", Symbol );
+ }
+ fprintf( pFile, ")" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the DSD formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
+{
+ fprintf( pFile, "F = " );
+ if ( pNtk->Root & 1 )
+ fprintf( pFile, "!" );
+ Kit_DsdPrint_rec( pFile, pNtk, Dsd_NtkRoot(pNtk) );
+ fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if there is a component with more than 3 inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+{
+ Dsd_Obj_t * pFanin;
+ unsigned iVar, i, RetValue;
+ if ( pObj->nFans > 3 )
+ return 1;
+ RetValue = 0;
+ Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
+ if ( pFanin )
+ RetValue |= Kit_DsdFindLargeBox( pNtk, pFanin );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned char * pPar )
+{
+ Dsd_Obj_t * pRes, * pRes0, * pRes1;
+ int nWords = Kit_TruthWordNum(pObj->nFans);
+ unsigned * pTruth = Dsd_ObjTruth(pObj);
+ unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
+ unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
+ int nFans0, nFans1, iVar0, iVar1, nPairs;
+ int fEquals[2][2], fOppos, fPairs[4][4];
+ unsigned j, k, nFansNew, uSupp0, uSupp1;
+ int i;
+
+ assert( pObj->nFans > 0 );
+ assert( pObj->Type == KIT_DSD_PRIME );
+ assert( pObj->uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) );
+
+ // compress the truth table
+ if ( pObj->uSupp != Kit_BitMask(pObj->nFans) )
+ {
+ nFansNew = Kit_WordCountOnes(pObj->uSupp);
+ Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, pObj->uSupp );
+ Kit_TruthCopy( pTruth, pNtk->pMem, pObj->nFans );
+ for ( j = k = 0; j < pObj->nFans; j++ )
+ if ( pObj->uSupp & (1 << j) )
+ pObj->pFans[k++] = pObj->pFans[j];
+ assert( k == nFansNew );
+ pObj->nFans = k;
+ pObj->uSupp = Kit_BitMask(pObj->nFans);
+ }
+
+ // consider the single variable case
+ if ( pObj->nFans == 1 )
+ {
+ pObj->Type = KIT_DSD_NONE;
+ if ( pTruth[0] == 0x55555555 )
+ pObj->pFans[0] ^= 1;
+ else
+ assert( pTruth[0] == 0xAAAAAAAA );
+ // update the parent pointer
+// assert( !((*pPar) & 1) );
+ *pPar = pObj->pFans[0] ^ ((*pPar) & 1);
+ return;
+ }
+
+ // decompose the output
+ if ( !pObj->fMark )
+ for ( i = pObj->nFans - 1; i >= 0; i-- )
+ {
+ // get the two-variable cofactors
+ Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
+ Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
+// assert( !Kit_TruthVarInSupport( pCofs2[0], pObj->nFans, i) );
+// assert( !Kit_TruthVarInSupport( pCofs2[1], pObj->nFans, i) );
+ // get the constant cofs
+ fEquals[0][0] = Kit_TruthIsConst0( pCofs2[0], pObj->nFans );
+ fEquals[0][1] = Kit_TruthIsConst0( pCofs2[1], pObj->nFans );
+ fEquals[1][0] = Kit_TruthIsConst1( pCofs2[0], pObj->nFans );
+ fEquals[1][1] = Kit_TruthIsConst1( pCofs2[1], pObj->nFans );
+ fOppos = Kit_TruthIsOpposite( pCofs2[0], pCofs2[1], pObj->nFans );
+ assert( !Kit_TruthIsEqual(pCofs2[0], pCofs2[1], pObj->nFans) );
+ if ( fEquals[0][0] + fEquals[0][1] + fEquals[1][0] + fEquals[1][1] + fOppos == 0 )
+ {
+ // check the MUX decomposition
+ uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+ uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+ assert( pObj->uSupp == (uSupp0 | uSupp1 | (1<<i)) );
+ if ( uSupp0 & uSupp1 )
+ continue;
+ // perform MUX decomposition
+ pRes0 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+ pRes1 = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+ for ( k = 0; k < pObj->nFans; k++ )
+ {
+ pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127;
+ pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127;
+ }
+ Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans );
+ Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans );
+ pRes0->uSupp = uSupp0;
+ pRes1->uSupp = uSupp1;
+ // update the current one
+ pObj->Type = KIT_DSD_MUX;
+ pObj->nFans = 3;
+ pObj->pFans[0] = pObj->pFans[i];
+ pObj->pFans[1] = 2*pRes1->Id;
+ pObj->pFans[2] = 2*pRes0->Id;
+ // call recursively
+ Kit_DsdDecompose_rec( pNtk, pRes0, pObj->pFans + 2 );
+ Kit_DsdDecompose_rec( pNtk, pRes1, pObj->pFans + 1 );
+ return;
+ }
+//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
+
+ // create the new node
+ pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+ pRes->nFans = 2;
+ pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; pObj->uSupp &= ~(1 << i);
+ pRes->pFans[1] = 2*pObj->Id;
+ // update the parent pointer
+ *pPar = 2 * pRes->Id;
+ // consider different decompositions
+ if ( fEquals[0][0] )
+ {
+ Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
+ }
+ else if ( fEquals[0][1] )
+ {
+ pRes->pFans[0] ^= 1;
+ Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+ }
+ else if ( fEquals[1][0] )
+ {
+ *pPar ^= 1;
+ pRes->pFans[1] ^= 1;
+ Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
+ }
+ else if ( fEquals[1][1] )
+ {
+ *pPar ^= 1;
+ pRes->pFans[0] ^= 1;
+ pRes->pFans[1] ^= 1;
+ Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+ }
+ else if ( fOppos )
+ {
+ pRes->Type = KIT_DSD_XOR;
+ Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
+ }
+ else
+ assert( 0 );
+ // decompose the remainder
+ assert( Dsd_ObjTruth(pObj) == pTruth );
+ Kit_DsdDecompose_rec( pNtk, pObj, pRes->pFans + 1 );
+ return;
+ }
+ pObj->fMark = 1;
+
+ // decompose the input
+ for ( i = pObj->nFans - 1; i >= 0; i-- )
+ {
+ assert( Kit_TruthVarInSupport( pTruth, pObj->nFans, i ) );
+ // get the single variale cofactors
+ Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i );
+ Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i );
+ // check the existence of MUX decomposition
+ uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+ uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+ // if one of the cofs is a constant, it is time to check it again
+ if ( uSupp0 == 0 || uSupp1 == 0 )
+ {
+ pObj->fMark = 0;
+ Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+ return;
+ }
+ assert( uSupp0 && uSupp1 );
+ // get the number of unique variables
+ nFans0 = Kit_WordCountOnes( uSupp0 & ~uSupp1 );
+ nFans1 = Kit_WordCountOnes( uSupp1 & ~uSupp0 );
+ if ( nFans0 == 1 && nFans1 == 1 )
+ {
+ // get the cofactors w.r.t. the unique variables
+ iVar0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
+ iVar1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
+ // get four cofactors
+ Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iVar0 );
+ Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iVar0 );
+ Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iVar1 );
+ Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iVar1 );
+ // check existence conditions
+ fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
+ fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
+ fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans );
+ fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans );
+ if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
+ {
+ // construct the MUX
+ pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_MUX, 3 );
+ pRes->nFans = 3;
+ pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
+ pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127; pObj->uSupp &= ~(1 << iVar1);
+ pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127; pObj->uSupp &= ~(1 << iVar0);
+ // update the node
+ if ( fEquals[0][0] && fEquals[0][1] )
+ Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
+ else
+ Kit_TruthMux( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i );
+ // decompose the remainder
+ Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+ return;
+ }
+ }
+
+ // try other inputs
+ for ( k = i+1; k < pObj->nFans; k++ )
+ {
+ // get four cofactors ik
+ Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, k ); // 00
+ Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, k ); // 01
+ Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10
+ Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11
+ // compare equal pairs
+ fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[0][1], pObj->nFans);
+ fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][0], pObj->nFans);
+ fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual(pCofs4[0][0], pCofs4[1][1], pObj->nFans);
+ fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][0], pObj->nFans);
+ fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual(pCofs4[0][1], pCofs4[1][1], pObj->nFans);
+ fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual(pCofs4[1][0], pCofs4[1][1], pObj->nFans);
+ nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3];
+ if ( nPairs != 3 && nPairs != 2 )
+ continue;
+
+ // decomposition exists
+ pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_AND, 2 );
+ pRes->nFans = 2;
+ pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains the support
+ pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; pObj->uSupp &= ~(1 << i);
+ if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
+ {
+ pRes->pFans[0] ^= 1;
+ pRes->pFans[1] ^= 1;
+ Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
+ }
+ else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
+ {
+ pRes->pFans[0] ^= 1;
+ Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
+ }
+ else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
+ {
+ pRes->pFans[1] ^= 1;
+ Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
+ }
+ else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
+ {
+// unsigned uSupp0 = Kit_TruthSupport(pCofs4[0][0], pObj->nFans);
+// unsigned uSupp1 = Kit_TruthSupport(pCofs4[1][1], pObj->nFans);
+// unsigned uSupp;
+// Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" );
+// Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" );
+ Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k );
+// uSupp = Kit_TruthSupport(pTruth, pObj->nFans);
+// Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" );
+ }
+ else
+ {
+ assert( fPairs[0][3] && fPairs[1][2] );
+ pRes->Type = KIT_DSD_XOR;;
+ Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
+ }
+ // decompose the remainder
+ Kit_DsdDecompose_rec( pNtk, pObj, pPar );
+ return;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+{
+ Dsd_Ntk_t * pNtk;
+ Dsd_Obj_t * pObj;
+ int i, nVarsReal;
+ assert( nVars <= 16 );
+ pNtk = Kit_DsdNtkAlloc( pTruth, nVars );
+ pNtk->Root = 2*pNtk->nVars;
+ // create the first node
+ pObj = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
+ pNtk->pNodes[0] = pObj;
+ for ( i = 0; i < nVars; i++ )
+ pObj->pFans[i] = 2*i;
+ Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
+ pObj->uSupp = Kit_TruthSupport( pTruth, nVars );
+ // consider special cases
+ nVarsReal = Kit_WordCountOnes( pObj->uSupp );
+ if ( nVarsReal == 0 )
+ {
+ pObj->Type = KIT_DSD_CONST1;
+ pObj->nFans = 0;
+ pNtk->Root ^= (pTruth[0] == 0);
+ return pNtk;
+ }
+ if ( nVarsReal == 1 )
+ {
+ pObj->Type = KIT_DSD_VAR;
+ pObj->nFans = 1;
+ pObj->pFans[0] = 2 * Kit_WordFindFirstBit( pObj->uSupp );
+ pObj->pFans[0] ^= (pTruth[0] & 1);
+ return pNtk;
+ }
+ Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], &pNtk->Root );
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdTestCofs( Dsd_Ntk_t * pNtk, unsigned * pTruthInit )
+{
+ Dsd_Ntk_t * pNtk0, * pNtk1;
+ Dsd_Obj_t * pRoot;
+ unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
+ unsigned i, * pTruth;
+ int fVerbose = 1;
+
+// pTruth = pTruthInit;
+
+ pRoot = Dsd_NtkRoot(pNtk);
+ pTruth = Dsd_ObjTruth(pRoot);
+ assert( pRoot->nFans == pNtk->nVars );
+
+ if ( fVerbose )
+ {
+ printf( "Function: " );
+// Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) );
+ Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars );
+ printf( "\n" );
+ }
+ for ( i = 0; i < pNtk->nVars; i++ )
+ {
+ Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i );
+ pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars );
+ if ( fVerbose )
+ {
+ printf( "Cof%d0: ", i );
+ Kit_DsdPrint( stdout, pNtk0 );
+ }
+ Kit_DsdNtkFree( pNtk0 );
+
+ Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
+ pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars );
+ if ( fVerbose )
+ {
+ printf( "Cof%d1: ", i );
+ Kit_DsdPrint( stdout, pNtk1 );
+ }
+ Kit_DsdNtkFree( pNtk0 );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdTest( unsigned * pTruth, int nVars )
+{
+ Dsd_Ntk_t * pNtk;
+ pNtk = Kit_DsdDecompose( pTruth, nVars );
+
+// if ( Kit_DsdFindLargeBox(pNtk, Dsd_NtkRoot(pNtk)) )
+// Kit_DsdPrint( stdout, pNtk );
+
+ if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 8 )
+ Kit_DsdTestCofs( pNtk, pTruth );
+
+ Kit_DsdNtkFree( pNtk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index 429875bc..5ac85524 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -311,7 +311,7 @@ int Kit_TruthSupportSize( unsigned * pTruth, int nVars )
SeeAlso []
***********************************************************************/
-int Kit_TruthSupport( unsigned * pTruth, int nVars )
+unsigned Kit_TruthSupport( unsigned * pTruth, int nVars )
{
int i, Support = 0;
for ( i = 0; i < nVars; i++ )
@@ -324,6 +324,57 @@ int Kit_TruthSupport( unsigned * pTruth, int nVars )
/**Function*************************************************************
+ Synopsis [Computes negative cofactor of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
+ return;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
+ return;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+ return;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
+ return;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
+ return;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ pTruth[Step+i] = pTruth[i];
+ pTruth += 2*Step;
+ }
+ return;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Computes positive cofactor of the function.]
Description []
@@ -375,7 +426,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
/**Function*************************************************************
- Synopsis [Computes negative cofactor of the function.]
+ Synopsis [Computes positive cofactor of the function.]
Description []
@@ -384,7 +435,7 @@ void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar )
SeeAlso []
***********************************************************************/
-void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
+void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
@@ -394,31 +445,84 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
- pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
+ pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
- pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
+ pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
- pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+ pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
- pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
+ pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
- pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
+ pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
- pTruth[Step+i] = pTruth[i];
- pTruth += 2*Step;
+ pOut[i] = pOut[Step+i] = pIn[i];
+ pIn += 2*Step;
+ pOut += 2*Step;
+ }
+ return;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes positive cofactor of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
+ return;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
+ return;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
+ return;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
+ return;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
+ return;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ pOut[i] = pOut[Step+i] = pIn[Step+i];
+ pIn += 2*Step;
+ pOut += 2*Step;
}
return;
}
@@ -733,6 +837,8 @@ void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVar
pOut[Step+i] = pCof1[Step+i];
}
pOut += 2*Step;
+ pCof0 += 2*Step;
+ pCof1 += 2*Step;
}
return;
}
diff --git a/src/opt/kit/module.make b/src/opt/kit/module.make
index 36beda7a..d1363ee2 100644
--- a/src/opt/kit/module.make
+++ b/src/opt/kit/module.make
@@ -1,4 +1,5 @@
SRC += src/opt/kit/kitBdd.c \
+ src/opt/kit/kitDsd.c \
src/opt/kit/kitFactor.c \
src/opt/kit/kitGraph.c \
src/opt/kit/kitHop.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 03:40:39 +0000