diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.h | 2 | ||||
-rw-r--r-- | src/base/abc/abcFunc.c | 15 | ||||
-rw-r--r-- | src/base/abc/abcSop.c | 6 | ||||
-rw-r--r-- | src/base/abci/abc.c | 96 | ||||
-rw-r--r-- | src/base/abci/abcHaig.c | 385 | ||||
-rw-r--r-- | src/base/abci/abcIf.c | 1 | ||||
-rw-r--r-- | src/base/abci/abcRenode.c | 14 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c | 29 | ||||
-rw-r--r-- | src/base/io/io.c | 63 | ||||
-rw-r--r-- | src/base/io/ioReadDsd.c | 308 | ||||
-rw-r--r-- | src/base/io/ioWriteBench.c | 2 | ||||
-rw-r--r-- | src/base/io/io_.c | 12 | ||||
-rw-r--r-- | src/base/io/module.make | 1 |
13 files changed, 822 insertions, 112 deletions
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 \ |