diff options
Diffstat (limited to 'src')
42 files changed, 3328 insertions, 106 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 64df9fc5..968dc596 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -419,12 +419,13 @@ extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_ extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ); extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel ); extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld ); +extern void Abc_AigRehash( Abc_Aig_t * pMan ); extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ); extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ); extern void Abc_AigPrintNode( Abc_Obj_t * pNode ); extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot ); extern void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan ); -extern void Abc_AigRehash( Abc_Aig_t * pMan ); +extern void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); /*=== abcBalance.c ==========================================================*/ @@ -462,8 +463,8 @@ extern void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFani extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); /*=== abcFraig.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ); -extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ); +extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); +extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); extern Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ); extern int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkFraigRestore(); @@ -557,9 +558,10 @@ extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkStartRead( char * pName ); extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); +extern Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); -extern Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); +extern Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); +extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ); extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); /*=== abcPrint.c ==========================================================*/ @@ -625,12 +627,13 @@ extern bool Abc_SopIsOrType( char * pSop ); extern bool Abc_SopCheck( char * pSop, int nFanins ); extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars ); extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ); +extern char * Abc_SopFromTruthBin( char * pTruth ); +extern char * Abc_SopFromTruthHex( char * pTruth ); /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ); extern Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); /*=== abcSweep.c ==========================================================*/ -extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ); extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ); extern int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ); /*=== abcTiming.c ==========================================================*/ @@ -666,6 +669,7 @@ extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk ); extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ); extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk ); +extern void Abc_NtkCleanNext( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode ); extern bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk ); extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 3f7f8d7c..45d7a6e9 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -1236,6 +1236,35 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan ) } } +/**Function************************************************************* + + Synopsis [Sets the correct phase of the nodes.] + + Description [The AIG nodes should be in the DFS order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkIsDfsOrdered(pNtk) ); + Abc_AigConst1(pNtk->pManFunc)->fPhase = 1; +// Abc_NtkForEachCi( pNtk, pObj, i ) +// pObj->fPhase = 0; + Abc_NtkForEachPi( pNtk, pObj, i ) + pObj->fPhase = 0; + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->fPhase = Abc_LatchIsInit1(pObj); + Abc_AigForEachAnd( pNtk, pObj, i ) + pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)) & (Abc_ObjFanin1(pObj)->fPhase ^ Abc_ObjFaninC1(pObj)); + Abc_NtkForEachPo( pNtk, pObj, i ) + pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 097ee92d..ba1443ab 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -229,6 +229,8 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk ) // go through the nodes Abc_NtkForEachNode( pNtk, pNode, i ) { + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) ) return 0; if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) ) diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 0cdee0b3..57219eea 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -162,13 +162,16 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, ABC_FUNC_SOP ); else pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, ABC_FUNC_BDD ); + // create the CI nets and remember them in the new CI nodes Abc_NtkForEachCi( pNtk, pObj, i ) { pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); Abc_ObjAddFanin( pNet, pObj->pCopy ); pObj->pCopy->pCopy = pNet; +//printf( "%s ", Abc_ObjName(pObj) ); } +//printf( "\n" ); // duplicate all nodes Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkDupObj(pNtkNew, pObj); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 2720f169..ba9ab231 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -318,7 +318,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ) +Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; @@ -373,13 +373,13 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkCreateOutput(): Network check has failed.\n" ); return pNtkNew; } /**Function************************************************************* - Synopsis [Creates the network composed of one output.] + Synopsis [Creates the miter composed of one multi-output cone.] Description [] @@ -439,7 +439,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * /**Function************************************************************* - Synopsis [Deletes the Ntk.] + Synopsis [Creates the network composed of one node.] Description [] @@ -448,7 +448,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) +Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pFanin, * pNodePo; @@ -471,7 +471,48 @@ Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) Abc_ObjAddFanin( pNodePo, pNode->pCopy ); Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkCreateFromNode(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Creates the network composed of one node with the given SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pFanin, * pNode, * pNodePo; + Vec_Ptr_t * vNames; + int i, nVars; + // start the network + pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); + pNtkNew->pName = util_strsav("ex"); + // create PIs + Vec_PtrPush( pNtkNew->vObjs, NULL ); + nVars = Abc_SopGetVarNum( pSop ); + vNames = Abc_NodeGetFakeNames( nVars ); + for ( i = 0; i < nVars; i++ ) + Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtkNew), Vec_PtrEntry(vNames, i) ); + Abc_NodeFreeNames( vNames ); + // create the node, add PIs as fanins, set the function + pNode = Abc_NtkCreateNode( pNtkNew ); + Abc_NtkForEachPi( pNtkNew, pFanin, i ) + Abc_ObjAddFanin( pNode, pFanin ); + pNode->pData = Abc_SopRegister( pNtkNew->pManFunc, pSop ); + // create the only PO + pNodePo = Abc_NtkCreatePo(pNtkNew); + Abc_ObjAddFanin( pNodePo, pNode ); + Abc_NtkLogicStoreName( pNodePo, "F" ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkCreateWithNode(): Network check has failed.\n" ); return pNtkNew; } diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index cc8b90f6..2e2d758d 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -105,6 +105,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk ) fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); return; } + fclose( pFile ); // collect all nodes in the network vNodes = Vec_PtrAlloc( 100 ); @@ -149,6 +150,7 @@ void Abc_NtkShowMulti( Abc_Ntk_t * pNtk ) fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); return; } + fclose( pFile ); // get the implication supergates Abc_NtkBalanceAttach( pNtk ); diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index 28e92889..03a73787 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -731,6 +731,132 @@ void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, V } +/**Function************************************************************* + + Synopsis [Derives SOP from the truth table representation.] + + Description [Truth table is expected to be in the hexadecimal notation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopFromTruthBin( char * pTruth ) +{ + char * pSopCover, * pCube; + int nTruthSize, nVars, Digit, Length, Mint, i, b; + Vec_Int_t * vMints; + + // get the number of variables + nTruthSize = strlen(pTruth); + nVars = Extra_Base2Log( nTruthSize ); + if ( nTruthSize != (1 << (nVars)) ) + { + printf( "String %s does not look like a truth table of a %d-variable function.\n", pTruth, nVars ); + return NULL; + } + + // collect the on-set minterms + vMints = Vec_IntAlloc( 100 ); + for ( i = 0; i < nTruthSize; i++ ) + { + if ( pTruth[i] >= '0' && pTruth[i] <= '1' ) + Digit = pTruth[i] - '0'; + else + { + printf( "String %s does not look like a binary representation of the truth table.\n", pTruth ); + return NULL; + } + if ( Digit == 1 ) + Vec_IntPush( vMints, nTruthSize - 1 - i ); + } + + // create the SOP representation of the minterms + Length = Vec_IntSize(vMints) * (nVars + 3); + pSopCover = ALLOC( char, Length + 1 ); + pSopCover[Length] = 0; + Vec_IntForEachEntry( vMints, Mint, i ) + { + pCube = pSopCover + i * (nVars + 3); + for ( b = 0; b < nVars; b++ ) + if ( Mint & (1 << b) ) + pCube[b] = '1'; + else + pCube[b] = '0'; + pCube[nVars + 0] = ' '; + pCube[nVars + 1] = '1'; + pCube[nVars + 2] = '\n'; + } + Vec_IntFree( vMints ); + return pSopCover; +} + +/**Function************************************************************* + + Synopsis [Derives SOP from the truth table representation.] + + Description [Truth table is expected to be in the hexadecimal notation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopFromTruthHex( char * pTruth ) +{ + char * pSopCover, * pCube; + int nTruthSize, nVars, Digit, Length, Mint, i, b; + Vec_Int_t * vMints; + + // get the number of variables + nTruthSize = strlen(pTruth); + nVars = Extra_Base2Log( nTruthSize ) + 2; + if ( nTruthSize != (1 << (nVars-2)) ) + { + printf( "String %s does not look like a truth table of a %d-variable function.\n", pTruth, nVars ); + return NULL; + } + + // collect the on-set minterms + vMints = Vec_IntAlloc( 100 ); + for ( i = 0; i < nTruthSize; i++ ) + { + if ( pTruth[i] >= '0' && pTruth[i] <= '9' ) + Digit = pTruth[i] - '0'; + else if ( pTruth[i] >= 'a' && pTruth[i] <= 'f' ) + Digit = 10 + pTruth[i] - 'a'; + else if ( pTruth[i] >= 'A' && pTruth[i] <= 'F' ) + Digit = 10 + pTruth[i] - 'A'; + else + { + printf( "String %s does not look like a hexadecimal representation of the truth table.\n", pTruth ); + return NULL; + } + for ( b = 0; b < 4; b++ ) + if ( Digit & (1 << b) ) + Vec_IntPush( vMints, 4*(nTruthSize-1-i)+b ); + } + + // create the SOP representation of the minterms + Length = Vec_IntSize(vMints) * (nVars + 3); + pSopCover = ALLOC( char, Length + 1 ); + pSopCover[Length] = 0; + Vec_IntForEachEntry( vMints, Mint, i ) + { + pCube = pSopCover + i * (nVars + 3); + for ( b = 0; b < nVars; b++ ) + if ( Mint & (1 << b) ) + pCube[b] = '1'; + else + pCube[b] = '0'; + pCube[nVars + 0] = ' '; + pCube[nVars + 1] = '1'; + pCube[nVars + 2] = '\n'; + } + Vec_IntFree( vMints ); + return pSopCover; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index a5605d4e..13720aeb 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -305,15 +305,32 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk ) void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; - int i; - i = 0; - // set the data filed to NULL + int i = 0; Abc_NtkForEachObj( pNtk, pObj, i ) pObj->pCopy = NULL; } /**Function************************************************************* + Synopsis [Cleans the copy field of all objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCleanNext( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->pNext = NULL; +} + +/**Function************************************************************* + Synopsis [Checks if the internal node has a unique CO.] Description [Checks if the internal node can borrow a name from a CO diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ca9f1dfa..cde9c16b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32,6 +32,7 @@ //////////////////////////////////////////////////////////////////////// static int Abc_CommandPrintStats ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -39,6 +40,7 @@ static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -61,12 +63,16 @@ static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOneNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -93,6 +99,7 @@ static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -114,7 +121,10 @@ static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ***********************************************************************/ void Abc_Init( Abc_Frame_t * pAbc ) { +// Abc_NtkBddImplicationTest(); + Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_exdc", Abc_CommandPrintExdc, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_io", Abc_CommandPrintIo, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_latch", Abc_CommandPrintLatch, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Abc_CommandPrintFanio, 0 ); @@ -122,6 +132,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_kmap", Abc_CommandPrintKMap, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 ); @@ -139,17 +150,21 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); - Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); +// Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 ); Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); + Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "one_output", Abc_CommandOneOutput, 1 ); Cmd_CommandAdd( pAbc, "Various", "one_node", Abc_CommandOneNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); + Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); + Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); + Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 ); Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); @@ -176,6 +191,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "seq_sweep", Abc_CommandSeqSweep, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); @@ -248,7 +264,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtk == NULL ) { - fprintf( Abc_FrameReadErr(pAbc), "Empty network\n" ); + fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); return 1; } Abc_NtkPrintStats( pOut, pNtk, fFactor ); @@ -256,7 +272,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: print_stats [-fh]\n" ); - fprintf( pErr, "\t prints the network statistics and\n" ); + fprintf( pErr, "\t prints the network statistics\n" ); fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -273,6 +289,98 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkTemp; + double Percentage; + bool fShort; + int c; + int fPrintDc; + + extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set the defaults + fShort = 1; + fPrintDc = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "sdh" ) ) != EOF ) + { + switch ( c ) + { + case 's': + fShort ^= 1; + break; + case 'd': + fPrintDc ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); + return 1; + } + if ( pNtk->pExdc == NULL ) + { + fprintf( Abc_FrameReadErr(pAbc), "Network has no EXDC.\n" ); + return 1; + } + + if ( fPrintDc ) + { + if ( !Abc_NtkIsStrash(pNtk->pExdc) ) + { + pNtkTemp = Abc_NtkStrash(pNtk->pExdc, 0, 0); + Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtkTemp, 0) ) ); + Abc_NtkDelete( pNtkTemp ); + } + else + Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtk->pExdc, 0) ) ); + + printf( "EXDC network statistics: " ); + printf( "(" ); + if ( Percentage > 0.05 && Percentage < 99.95 ) + printf( "%.2f", Percentage ); + else if ( Percentage > 0.000005 && Percentage < 99.999995 ) + printf( "%.6f", Percentage ); + else + printf( "%f", Percentage ); + printf( " %% don't-cares)\n" ); + } + else + printf( "EXDC network statistics: \n" ); + Abc_NtkPrintStats( pOut, pNtk->pExdc, 0 ); + return 0; + +usage: + fprintf( pErr, "usage: print_exdc [-dh]\n" ); + fprintf( pErr, "\t prints the EXDC network statistics\n" ); + fprintf( pErr, "\t-d : toggles printing don't-care percentage [default = %s]\n", fPrintDc? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -754,6 +862,94 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pNode; + int c; + int fUseRealNames; + + extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fUseRealNames = 1; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF ) + { + switch ( c ) + { + case 'n': + fUseRealNames ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsBddLogic(pNtk) ) + { + fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" ); + return 1; + } + if ( argc > util_optind + 1 ) + { + fprintf( pErr, "Wrong number of auguments.\n" ); + goto usage; + } + if ( argc == util_optind ) + { + pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); + if ( !Abc_ObjIsNode(pNode) ) + { + fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) ); + return 1; + } + } + else + { + pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + if ( pNode == NULL ) + { + fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + return 1; + } + } + Abc_NodePrintKMap( pNode, fUseRealNames ); + return 0; + +usage: + fprintf( pErr, "usage: print_kmap [-nh] <node>\n" ); + fprintf( pErr, " shows the truth table of the node\n" ); + fprintf( pErr, "\t-n : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tnode : the node to consider (default = the driver of the first PO)\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -787,21 +983,32 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkIsBddLogic(pNtk) ) { - fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" ); + fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" ); return 1; } - if ( argc != util_optind + 1 ) + if ( argc > util_optind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); - if ( pNode == NULL ) + if ( argc == util_optind ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); - return 1; + pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); + if ( !Abc_ObjIsNode(pNode) ) + { + fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) ); + return 1; + } + } + else + { + pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + if ( pNode == NULL ) + { + fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + return 1; + } } Abc_NodeShowBdd( pNode ); return 0; @@ -813,7 +1020,7 @@ usage: fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); #endif - fprintf( pErr, "\tnode : the node to consider\n"); + fprintf( pErr, "\tnode : the node to consider [default = the driver of the first PO]\n"); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -1423,7 +1630,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) ) { - fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (unmap it first).\n" ); + fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (run \"unmap\").\n" ); return 1; } // modify the current network @@ -1666,7 +1873,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_NtkIsBddLogic( pNtk ) ) { - fprintf( pErr, "This command is only applicable to logic BDD networks.\n" ); + fprintf( pErr, "This command is only applicable to logic BDD networks (run \"bdd\").\n" ); return 1; } fprintf( stdout, "Performing simple non-recursive DSD of local functions.\n" ); @@ -2233,7 +2440,6 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - // get the new network if ( !Abc_NtkIsSopLogic(pNtk) ) { fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" ); @@ -2264,6 +2470,69 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fVerbose; + extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + // get the new network + if ( !Abc_NtkIsBddLogic(pNtk) ) + { + fprintf( pErr, "Variable reordering is possible when node functions are BDDs (run \"bdd\").\n" ); + return 1; + } + Abc_NtkBddReorder( pNtk, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: reorder [-vh]\n" ); + fprintf( pErr, "\t reorders local functions of the nodes using sifting\n" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -2559,7 +2828,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Cannot find CO node \"%s\".\n", argv[util_optind] ); return 1; } - pNtkRes = Abc_NtkSplitOutput( pNtk, pNode, fUseAllCis ); + pNtkRes = Abc_NtkCreateOutput( pNtk, pNode, fUseAllCis ); } else { @@ -2573,7 +2842,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) ); return 1; } - pNtkRes = Abc_NtkSplitOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis ); + pNtkRes = Abc_NtkCreateOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis ); } if ( pNtkRes == NULL ) { @@ -2654,7 +2923,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkSplitNode( pNtk, pNode ); + pNtkRes = Abc_NtkCreateFromNode( pNtk, pNode ); // pNtkRes = Abc_NtkDeriveFromBdd( pNtk->pManFunc, pNode->pData, NULL, NULL ); if ( pNtkRes == NULL ) { @@ -2735,6 +3004,210 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( pNtk->pExdc == NULL ) + { + fprintf( pErr, "The network has no EXDC.\n" ); + return 1; + } + + Abc_NtkDelete( pNtk->pExdc ); + pNtk->pExdc = NULL; + + // replace the current network + pNtkRes = Abc_NtkDup( pNtk ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: exdc_free [-h]\n" ); + fprintf( pErr, "\t frees the EXDC network of the current network\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( pNtk->pExdc == NULL ) + { + fprintf( pErr, "The network has no EXDC.\n" ); + return 1; + } + + // replace the current network + pNtkRes = Abc_NtkDup( pNtk->pExdc ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: exdc_get [-h]\n" ); + fprintf( pErr, "\t replaces the current network by the EXDC of the current network\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr, * pFile; + Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes; + char * FileName; + int c; + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[util_optind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) + fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); + fprintf( pAbc->Err, "\n" ); + return 1; + } + fclose( pFile ); + + // set the new network + pNtkNew = Io_Read( FileName, 1 ); + if ( pNtkNew == NULL ) + { + fprintf( pAbc->Err, "Reading network from file has failed.\n" ); + return 1; + } + + // replace the EXDC + if ( pNtk->pExdc ) + { + Abc_NtkDelete( pNtk->pExdc ); + pNtk->pExdc = NULL; + } + pNtkRes = Abc_NtkDup( pNtk ); + pNtkRes->pExdc = pNtkNew; + + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: exdc_set [-h] <file>\n" ); + fprintf( pErr, "\t sets the network from file as EXDC for the current network\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t<file> : file with the new EXDC network\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) { Cut_Params_t Params, * pParams = &Params; @@ -3038,6 +3511,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int fAllNodes; + int fExdc; int c; pNtk = Abc_FrameReadNet(pAbc); @@ -3045,6 +3519,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fExdc = 0; fAllNodes = 0; memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = 2048; // the number of words of random simulation info @@ -3059,7 +3534,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbosiness flag util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "RDBrscpvaeh" ) ) != EOF ) { switch ( c ) { @@ -3115,6 +3590,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fAllNodes ^= 1; break; + case 'e': + fExdc ^= 1; + break; case 'h': goto usage; default: @@ -3138,11 +3616,11 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); else { pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes ); - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes ); + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -3170,6 +3648,7 @@ usage: fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", pParams->fChoicing? "yes": "no" ); fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", pParams->fTryProve? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3430,7 +3909,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int fUseInv; + int fExdc; int fVerbose; + extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3438,15 +3919,19 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseInv = 1; + fExdc = 0; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ivh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "ievh" ) ) != EOF ) { switch ( c ) { case 'i': fUseInv ^= 1; break; + case 'e': + fExdc ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -3473,7 +3958,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // modify the current network - if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fVerbose ) ) + if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) ) { fprintf( pErr, "Sweeping has failed.\n" ); return 1; @@ -3481,9 +3966,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: fraig_sweep [-vh]\n" ); + fprintf( pErr, "usage: fraig_sweep [-evh]\n" ); fprintf( pErr, "\t performs technology-dependent sweep\n" ); -// fprintf( pErr, "\t-i : toggle using inverter for complemented nodes [default = %s]\n", fUseInv? "yes": "no" ); + fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3513,6 +3998,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; int c; extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose ); + extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3603,7 +4089,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fSweep ) - Abc_NtkFraigSweep( pNtkRes, 0, 0 ); + Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 ); // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -4517,6 +5003,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" ); return 1; } +return 0; // get the new network pNtkRes = Abc_NtkFpgaSeq( pNtk, fVerbose ); @@ -4588,6 +5075,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" ); return 1; } +return 0; // get the new network pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose ); @@ -4608,6 +5096,109 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int nFrames; + int fExdc; + int fVerbose; + extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 1; + fExdc = 1; + fVerbose = 1; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[util_optind]); + util_optind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'e': + fExdc ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Works only for combinational networks (run \"unseq\").\n" ); + return 1; + } + + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Works only for structurally hashed networks (run \"strash\").\n" ); + return 1; + } + + // get the new network + pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" ); + fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); + fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames ); + fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index c612a1ce..9b5f7d5b 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -52,6 +52,8 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ) pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate ); Abc_NtkFinalize( pNtk, pNtkAig ); + if ( pNtk->pExdc ) + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkAig ) ) { diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 8c2f5bd3..9de61389 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -69,6 +69,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ) // make the network minimum base Abc_NtkMinimumBase( pNtkNew ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 5b317994..7e81c579 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -76,6 +76,9 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool Extra_StopManager( pNtk->pManGlob ); pNtk->pManGlob = NULL; + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index ea97826a..161607b5 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -88,6 +88,9 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV // make the network minimum base Abc_NtkMinimumBase( pNtkNew ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 5657fe38..421cdfed 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -26,12 +26,16 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); -static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ); - -static int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk ); -static void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); +static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); +static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ); +static void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs ); +extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc ); +static void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); + +static int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk ); +static void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); +static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -48,19 +52,27 @@ static Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) +Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ) { Fraig_Params_t * pPars = pParams; Abc_Ntk_t * pNtkNew; Fraig_Man_t * pMan; + // check if EXDC is present + if ( fExdc && pNtk->pExdc == NULL ) + fExdc = 0, printf( "Warning: Networks has no EXDC.\n" ); // perform fraiging - pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); + pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); // prove the miter if asked to if ( pPars->fTryProve ) Fraig_ManProveMiter( pMan ); // reconstruct FRAIG in the new network - pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + if ( fExdc ) + pNtkNew = Abc_NtkFromFraig2( pMan, pNtk ); + else + pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); Fraig_ManFree( pMan ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { @@ -82,14 +94,13 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) SeeAlso [] ***********************************************************************/ -void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) +void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ) { + int fInternal = ((Fraig_Params_t *)pParams)->fInternal; Fraig_Man_t * pMan; ProgressBar * pProgress; - Fraig_Node_t * pNodeFraig; Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode, * pConst1; - int fInternal = ((Fraig_Params_t *)pParams)->fInternal; + Abc_Obj_t * pNode; int i; assert( Abc_NtkIsStrash(pNtk) ); @@ -97,11 +108,12 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) // create the FRAIG manager pMan = Fraig_ManCreate( pParams ); - // create PIs and remember them in the old nodes + // map the constant node Abc_NtkCleanCopy( pNtk ); + Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + // create PIs and remember them in the old nodes Abc_NtkForEachCi( pNtk, pNode, i ) pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); - pConst1 = Abc_AigConst1( pNtk->pManFunc ); // perform strashing vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 ); @@ -109,21 +121,22 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; if ( !fInternal ) Extra_ProgressBarUpdate( pProgress, i, NULL ); - if ( pNode == pConst1 ) - pNodeFraig = Fraig_ManReadConst1(pMan); - else - pNodeFraig = Fraig_NodeAnd( pMan, + pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); - assert( pNode->pCopy == NULL ); - pNode->pCopy = (Abc_Obj_t *)pNodeFraig; } if ( !fInternal ) Extra_ProgressBarStop( pProgress ); Vec_PtrFree( vNodes ); + // use EXDC to change the mapping of nodes into FRAIG nodes + if ( fExdc ) + Abc_NtkFraigRemapUsingExdc( pMan, pNtk ); + // set the primary outputs Abc_NtkForEachCo( pNtk, pNode, i ) Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) ); @@ -132,7 +145,123 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) /**Function************************************************************* - Synopsis [Transforms FRAIG into what looks like a strashed network.] + Synopsis [Derives EXDC node for the given network.] + + Description [Assumes that EXDCs of all POs are the same. + Returns the EXDC of the first PO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc ) +{ + Abc_Ntk_t * pNtkStrash; + Abc_Obj_t * pObj; + Fraig_Node_t * gResult; + char ** ppNames; + int i, k; + // strash the EXDC network + pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0 ); + Abc_NtkCleanCopy( pNtkStrash ); + Abc_AigConst1(pNtkStrash->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + // set the mapping of the PI nodes + ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 ); + Abc_NtkForEachCi( pNtkStrash, pObj, i ) + { + for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ ) + if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 ) + { + pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k); + break; + } + assert( pObj->pCopy != NULL ); + } + free( ppNames ); + // build FRAIG for each node + Abc_AigForEachAnd( pNtkStrash, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, + Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ), + Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ) ); + // get the EXDC to be returned + pObj = Abc_NtkPo( pNtkStrash, 0 ); + gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + Abc_NtkDelete( pNtkStrash ); + return gResult; +} + + +/**Function************************************************************* + + Synopsis [Changes mapping of the old nodes into FRAIG nodes using EXDC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) +{ + Fraig_Node_t * gNodeNew, * gNodeExdc; + stmm_table * tTable; + stmm_generator * gen; + Abc_Obj_t * pNode, * pNodeBest; + Abc_Obj_t * pClass, ** ppSlot; + Vec_Ptr_t * vNexts; + int i; + + // get the global don't-cares + assert( pNtk->pExdc ); + gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc ); + + // save the next pointers + vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext ); + + // find the classes of AIG nodes which have FRAIG nodes assigned + Abc_NtkCleanNext( pNtk ); + tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash); + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( pNode->pCopy ) + { + gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) ); + if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) ) + *ppSlot = NULL; + pNode->pNext = *ppSlot; + *ppSlot = pNode; + } + + // for reach non-trival class, find the node with minimum level, and replace other nodes by it + Abc_AigSetNodePhases( pNtk ); + stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass ) + { + if ( pClass->pNext == NULL ) + continue; + // find the node with minimum level + pNodeBest = pClass; + for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) + if ( pNodeBest->Level > pNode->Level ) + pNodeBest = pNode; + // remap the class nodes + for ( pNode = pClass; pNode; pNode = pNode->pNext ) + pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase ); + } + stmm_free_table( tTable ); + + // restore the next pointers + Abc_NtkCleanNext( pNtk ); + Abc_NtkForEachNode( pNtk, pNode, i ) + pNode->pNext = Vec_PtrEntry( vNexts, pNode->Id ); + Vec_PtrFree( vNexts ); +} + +/**Function************************************************************* + + Synopsis [Transforms FRAIG into strashed network with choices.] Description [] @@ -229,6 +358,110 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) ); } +/**Function************************************************************* + + Synopsis [Transforms FRAIG into strashed network without choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + stmm_table * tTable; + Vec_Ptr_t * vNodeReprs; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pRepr, ** ppSlot; + int i; + + // map the nodes into their lowest level representives + tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash); + pNode = Abc_AigConst1(pNtk->pManFunc); + if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) ) + *ppSlot = pNode; + Abc_NtkForEachCi( pNtk, pNode, i ) + if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) ) + *ppSlot = pNode; + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( pNode->pCopy ) + { + if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) ) + *ppSlot = pNode; + else if ( (*ppSlot)->Level > pNode->Level ) + *ppSlot = pNode; + } + // save representatives for each node + vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( pNode->pCopy ) + { + if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) ) + assert( 0 ); + if ( pNode != pRepr ) + Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr ); + } + stmm_free_table( tTable ); + + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); + + // perform strashing + Abc_AigSetNodePhases( pNtk ); + Abc_NtkIncrementTravId( pNtk ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs ); + } + Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodeReprs ); + + // finalize the network + Abc_NtkFinalize( pNtk, pNtkNew ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Transforms into AIG one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs ) +{ + Abc_Obj_t * pRepr; + // skip the PIs and constants + if ( Abc_ObjFaninNum(pNode) < 2 ) + return; + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + assert( Abc_ObjIsNode( pNode ) ); + // get the node's representative + if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) ) + { + Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs ); + pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase ); + return; + } + Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs ); + Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs ); + pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); +} @@ -507,7 +740,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore() // Fraig_ManReportChoices( p ); // transform it into FRAIG - pFraig = Abc_NtkFraig( pStore, &Params, 1 ); + pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 ); if ( pFraig == NULL ) return NULL; Abc_NtkDelete( pStore ); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 7e83b4f0..0f727006 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -113,6 +113,9 @@ clk = clock(); return NULL; Map_ManFree( pMan ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index c5a9f5f3..0017a9de 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -31,6 +31,10 @@ static void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb ); static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes ); +// to be exported +typedef void (*AddFrameMapping)( Abc_Obj_t*, Abc_Obj_t*, int, void*); +extern Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg ); +static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -598,6 +602,178 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_ } + +/**Function************************************************************* + + Synopsis [Derives the timeframes of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg ) +{ + char Buffer[100]; + ProgressBar * pProgress; + Abc_Ntk_t * pNtkFrames; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pLatch, * pLatchNew; + int i, Counter; + assert( nFrames > 0 ); + assert( Abc_NtkIsStrash(pNtk) ); + // start the new network + pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); + sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames ); + pNtkFrames->pName = util_strsav(Buffer); + // create new latches (or their initial values) and remember them in the new latches + if ( !fInitial ) + { + Abc_NtkForEachLatch( pNtk, pLatch, i ) { + Abc_NtkDupObj( pNtkFrames, pLatch ); + if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg); + } + } + else + { + Counter = 0; + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI + { + pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames); + Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) ); + Counter++; + } + else { + pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) ); + } + + if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg); + } + if ( Counter ) + printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); + } + + // create the timeframes + vNodes = Abc_NtkDfs( pNtk, 0 ); + pProgress = Extra_ProgressBarStart( stdout, nFrames ); + for ( i = 0; i < nFrames; i++ ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Abc_NtkAddFrame2( pNtkFrames, pNtk, i, vNodes, addFrameMapping, arg ); + } + Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodes ); + + // connect the new latches to the outputs of the last frame + if ( !fInitial ) + { + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + pLatchNew = Abc_NtkLatch(pNtkFrames, i); + Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); + + Vec_PtrPush( pNtkFrames->vCis, pLatchNew ); + Vec_PtrPush( pNtkFrames->vCos, pLatchNew ); + Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); + } + } + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pNext = NULL; + + // remove dangling nodes + Abc_AigCleanup( pNtkFrames->pManFunc ); + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkFrames ) ) + { + printf( "Abc_NtkFrames: The network check has failed.\n" ); + Abc_NtkDelete( pNtkFrames ); + return NULL; + } + return pNtkFrames; +} + +/**Function************************************************************* + + Synopsis [Adds one time frame to the new network.] + + Description [Assumes that the latches of the old network point + to the outputs of the previous frame of the new network (pLatch->pCopy). + In the end, updates the latches of the old network to point to the + outputs of the current frame of the new network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg ) +{ + char Buffer[10]; + Abc_Obj_t * pNode, * pNodeNew, * pLatch; + Abc_Obj_t * pConst1, * pConst1New; + int i; + // get the constant nodes + pConst1 = Abc_AigConst1( pNtk->pManFunc ); + pConst1New = Abc_AigConst1( pNtkFrames->pManFunc ); + // create the prefix to be added to the node names + sprintf( Buffer, "_%02d", iFrame ); + // add the new PI nodes + Abc_NtkForEachPi( pNtk, pNode, i ) + { + pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); + Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); + } + // add the internal nodes + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( pNode == pConst1 ) + pNodeNew = pConst1New; + else + pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); + pNode->pCopy = pNodeNew; + if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); + } + // add the new POs + Abc_NtkForEachPo( pNtk, pNode, i ) + { + pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); + Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) ); + Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); + } + // transfer the implementation of the latch drivers to the latches + + // it is important that these two steps are performed it two loops + // and not in the same loop + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pNext = Abc_ObjChild0Copy(pLatch); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pCopy = pLatch->pNext; + + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + if (addFrameMapping) { + // don't give Mike complemented pointers because he doesn't like it + if (Abc_ObjIsComplement(pLatch->pCopy)) { + pNodeNew = Abc_NtkCreateNode( pNtkFrames ); + Abc_ObjAddFanin( pNodeNew, pLatch->pCopy ); + assert(Abc_ObjFaninNum(pNodeNew) == 1); + pNodeNew->Level = 1 + Abc_ObjRegular(pLatch->pCopy)->Level; + + pLatch->pNext = pNodeNew; + pLatch->pCopy = pNodeNew; + } + addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg); + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 8aee5014..d88e5370 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -394,6 +394,159 @@ void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ) pNtk->vFuncsGlob = NULL; } +/**Function************************************************************* + + Synopsis [Computes the BDD of the logic cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pNodeR; + DdManager * dd; + DdNode * bFunc; + double Result; + int i; + pNodeR = Abc_ObjRegular(pNode); + assert( Abc_NtkIsStrash(pNodeR->pNtk) ); + Abc_NtkCleanCopy( pNodeR->pNtk ); + // get the CIs in the support of the node + vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 ); + // start the manager + dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + // assign elementary BDDs for the CIs + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; + // build the BDD of the cone + bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, pNode != pNodeR ); + // count minterms + Result = Cudd_CountMinterm( dd, bFunc, dd->size ); + // get the percentagle + Result *= 100.0; + for ( i = 0; i < dd->size; i++ ) + Result /= 2; + // clean up + Cudd_Quit( dd ); + Vec_PtrFree( vNodes ); + return Result; +} + + + +#include "reo.h" + +/**Function************************************************************* + + Synopsis [Reorders BDD of the local function of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pFanin; + DdNode * bFunc; + int * pOrder, i; + // create the temporary array for the variable order + pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) ); + for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ ) + pOrder[i] = -1; + // reorder the BDD + bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData ); + pNode->pData = bFunc; + // update the fanin order + Abc_ObjForEachFanin( pNode, pFanin, i ) + pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ].iFan; + Abc_ObjForEachFanin( pNode, pFanin, i ) + pNode->vFanins.pArray[i].iFan = pOrder[i]; + free( pOrder ); +} + +/**Function************************************************************* + + Synopsis [Reorders BDDs of the local functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ) +{ + reo_man * p; + Abc_Obj_t * pNode; + int i; + p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_ObjFaninNum(pNode) < 3 ) + continue; + if ( fVerbose ) + fprintf( stdout, "%10s: ", Abc_ObjName(pNode) ); + if ( fVerbose ) + fprintf( stdout, "Before = %5d BDD nodes. ", Cudd_DagSize(pNode->pData) ); + Abc_NodeBddReorder( p, pNode ); + if ( fVerbose ) + fprintf( stdout, "After = %5d BDD nodes.\n", Cudd_DagSize(pNode->pData) ); + } + Extra_ReorderQuit( p ); +} + + + +/**Function************************************************************* + + Synopsis [Experiment with BDD-based representation of implications.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBddImplicationTest() +{ + DdManager * dd; + DdNode * bImp, * bSum, * bTemp; + int nVars = 200; + int nImps = 200; + int i, clk; +clk = clock(); + dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT ); + bSum = b0; Cudd_Ref( bSum ); + for ( i = 0; i < nImps; i++ ) + { + printf( "." ); + bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] ); Cudd_Ref( bImp ); + bSum = Cudd_bddOr( dd, bTemp = bSum, bImp ); Cudd_Ref( bSum ); + Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bImp ); + } + printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 ); + printf( "The BDD after = %d.\n", Cudd_DagSize(bSum) ); +PRT( "Time", clock() - clk ); + Cudd_RecursiveDeref( dd, bSum ); + Cudd_Quit( dd ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c index 5142d66b..5a115410 100644 --- a/src/base/abci/abcPga.c +++ b/src/base/abci/abcPga.c @@ -75,6 +75,9 @@ Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams ) // make the network minimum base Abc_NtkMinimumBase( pNtkNew ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 2e9c3cc8..aff31f4c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -499,6 +499,33 @@ void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ) fprintf( pFile, "\n" ); } +/**Function************************************************************* + + Synopsis [Prints the factored form of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames ) +{ + Vec_Ptr_t * vNamesIn; + if ( fUseRealNames ) + { + vNamesIn = Abc_NodeGetFaninNames(pNode); + Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), + Abc_ObjFaninNum(pNode), NULL, 0, (char **)vNamesIn->pArray ); + Abc_NodeFreeNames( vNamesIn ); + } + else + Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), + Abc_ObjFaninNum(pNode), NULL, 0, NULL ); + +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 3871b52c..672fd376 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -91,6 +91,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn } //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) ); + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 8059f222..93f534ce 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -71,7 +71,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) printf( "Cleanup has removed %d nodes.\n", nNodes ); // duplicate EXDC if ( pNtk->pExdc ) - pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 ); + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkAig ) ) { diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index fa840937..62cd5b55 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -25,10 +25,11 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ); +static void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); +static stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ); static void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose ); -static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv ); -static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv ); +static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose ); +static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose ); static int Abc_NodeDroppingCost( Abc_Obj_t * pNode ); static void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose ); @@ -52,7 +53,7 @@ static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF SeeAlso [] ***********************************************************************/ -bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) +bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig; @@ -63,11 +64,24 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) // derive the AIG pNtkAig = Abc_NtkStrash( pNtk, 0, 1 ); + // perform fraiging of the AIG Fraig_ParamsSetDefault( &Params ); - pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 ); + pMan = Abc_NtkToFraig( pNtkAig, &Params, 0, 0 ); + // cannot use EXDC with FRAIG because it can create classes of equivalent FRAIG nodes + // with representative nodes that do not correspond to the nodes with the current network + + // update FRAIG using EXDC + if ( fExdc ) + { + if ( pNtk->pExdc == NULL ) + printf( "Warning: Networks has no EXDC.\n" ); + else + Abc_NtkFraigSweepUsingExdc( pMan, pNtk ); + } + // collect the classes of equivalent nets - tEquiv = Abc_NtkFraigEquiv( pMan, pNtk, fUseInv, fVerbose ); + tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose ); // transform the network into the equivalent one Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose ); @@ -90,6 +104,47 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) /**Function************************************************************* + Synopsis [Sweep the network using EXDC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) +{ + Fraig_Node_t * gNodeExdc, * gNode, * gNodeRes; + Abc_Obj_t * pNode, * pNodeAig; + int i; + extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkExdc ); + + assert( pNtk->pExdc ); + // derive FRAIG node representing don't-cares in the EXDC network + gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc ); + // update the node pointers + Abc_NtkForEachNode( pNtk, pNode, i ) + { + // skip the constant input nodes + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; + // get the strashed node + pNodeAig = pNode->pCopy; + // skip the dangling nodes + if ( pNodeAig == NULL ) + continue; + // get the FRAIG node + gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) ); + // perform ANDing with EXDC + gNodeRes = Fraig_NodeAnd( pMan, gNode, Fraig_Not(gNodeExdc) ); + // write the node back + Abc_ObjRegular(pNodeAig)->pCopy = (Abc_Obj_t *)Fraig_NotCond( gNodeRes, Abc_ObjIsComplement(pNodeAig) ); + } +} + +/**Function************************************************************* + Synopsis [Collects equivalence classses of node in the network.] Description [] @@ -99,7 +154,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose ) SeeAlso [] ***********************************************************************/ -stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ) +stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ) { Abc_Obj_t * pList, * pNode, * pNodeAig; Fraig_Node_t * gNode; @@ -113,14 +168,14 @@ stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, tStrash2Net = stmm_init_table(stmm_ptrcmp,stmm_ptrhash); Abc_NtkForEachNode( pNtk, pNode, c ) { + // skip the constant input nodes + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; // get the strashed node pNodeAig = pNode->pCopy; // skip the dangling nodes if ( pNodeAig == NULL ) continue; - // skip the constant input nodes - if ( Abc_ObjFaninNum(pNode) == 0 ) - continue; // skip the nodes that fanout into POs if ( Abc_NodeHasUniqueCoFanout(pNode) ) continue; diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 182d688d..e932d076 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -87,6 +87,8 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) // allocate ZDD variables Cudd_zddVarsFromBddVars( dd, 2 ); // create the EXDC network representing the unreachable states + if ( pNtk->pExdc ) + Abc_NtkDelete( pNtk->pExdc ); pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach ); Cudd_RecursiveDeref( dd, bUnreach ); Extra_StopManager( dd ); @@ -283,9 +285,13 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // start the new network pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD ); + pNtkNew->pName = util_strsav("exdc"); + pNtkNew->pSpec = NULL; + // create PIs corresponding to LOs Abc_NtkForEachLatch( pNtk, pNode, i ) - pNode->pCopy = Abc_NtkCreatePi(pNtkNew); + Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) ); + // cannot ADD POs here because pLatch->pCopy point to the PIs // create a new node pNodeNew = Abc_NtkCreateNode(pNtkNew); @@ -304,21 +310,22 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn free( pPermute ); Abc_NodeMinimumBase( pNodeNew ); - // make the new node drive all the COs - Abc_NtkForEachCo( pNtk, pNode, i ) - Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); - - // store the PI names of the EXDC network + // for each CO, create PO (skip POs equal to CIs because of name conflict) + Abc_NtkForEachPo( pNtk, pNode, i ) + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) ) + Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) ); Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) ); - // store the PO names of the EXDC network + Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") ); + + // link to the POs of the network Abc_NtkForEachPo( pNtk, pNode, i ) - Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) ); + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) ) + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - // make the network minimum base - Abc_NtkMinimumBase( pNtkNew ); + // remove the extra nodes + Abc_AigCleanup( pNtkNew->pManFunc ); // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c new file mode 100644 index 00000000..d0179514 --- /dev/null +++ b/src/base/abci/abcVanEijk.c @@ -0,0 +1,789 @@ +/**CFile**************************************************************** + + FileName [abcVanEijk.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Implementation of van Eijk's method for finding + signal correspondence: C. A. J. van Eijk. "Sequential equivalence + checking based on structural similarities", IEEE Trans. CAD, + vol. 19(7), July 2000, pp. 814-819.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 2, 2005.] + + Revision [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); +static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames ); +static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ); +static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ); +static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); +static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); +static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); +static Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); +static void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); +static Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); +static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); + +//////////////////////////////////////////////////////////////////////// +/// INLINED FUNCTIONS /// +//////////////////////////////////////////////////////////////////////// + +// sets the correspondence of the node in the frame +static inline void Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) +{ + Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); +} +// returns the correspondence of the node in the frame +static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) +{ + return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); +} +// returns the hash value of the node in the frame +static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) +{ + return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy ); +} +// returns the representative node of the class to which the node belongs +static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) +{ + if ( pNode->pNext == NULL ) + return NULL; + while ( pNode->pNext ) + pNode = pNode->pNext; + return pNode; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives classes of sequentially equivalent nodes.] + + Description [Performs sequential sweep by combining the equivalent + nodes. Adds EXDC network to the current network to record the subset + of unreachable states computed by identifying the equivalent nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) +{ + Fraig_Params_t Params; + Abc_Ntk_t * pNtkSingle; + Vec_Ptr_t * vClasses; + Abc_Ntk_t * pNtkNew; + + assert( Abc_NtkIsStrash(pNtk) ); + + // FRAIG the network to get rid of combinational equivalences + Fraig_ParamsSetDefaultFull( &Params ); + pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + Abc_AigSetNodePhases( pNtkSingle ); + + // get the equivalence classes + vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); + if ( Vec_PtrSize(vClasses) > 0 ) + { + // transform the network by merging nodes in the equivalence classes + pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 ); +// pNtkNew = Abc_NtkDup( pNtkSingle ); + // derive the EXDC network if asked + if ( fExdc ) + pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses ); + } + else + pNtkNew = Abc_NtkDup( pNtkSingle ); + Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses ); + Vec_PtrFree( vClasses ); + + Abc_NtkDelete( pNtkSingle ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Derives the classes of sequentially equivalent nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose ) +{ + Fraig_Man_t * pFraig; + Abc_Ntk_t * pNtkMulti; + Vec_Ptr_t * vCorresp, * vClasses; + int nIter, RetValue; + + if ( fVerbose ) + printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); + + // get the AIG of the base case + vCorresp = Vec_PtrAlloc( 100 ); + Abc_NtkCleanNext(pNtkSingle); + pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 ); + if ( fVerbose ) + printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) ); + + // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) + pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); + Fraig_ManFree( pFraig ); + + // find initial equivalence classes + vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames ); + if ( fVerbose ) + printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); + Abc_NtkDelete( pNtkMulti ); + + // refine the classes using iterative FRAIGing + for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ ) + { + // derive the network with equivalence classes + Abc_NtkVanEijkClassesOrder( vClasses ); + pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 ); + // simulate with classes (TO DO) + + // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) + pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 ); + Fraig_ManFree( pFraig ); + + // refine the classes + RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses ); + Abc_NtkDelete( pNtkMulti ); + if ( fVerbose ) + printf( "The number of classes after %2d iterations = %5d. Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); + // quit if there is no change + if ( RetValue == 0 ) + break; + } + Vec_PtrFree( vCorresp ); + + if ( fVerbose ) + { + Abc_Obj_t * pObj, * pClass; + int i, Counter; + printf( "The classes are: " ); + Vec_PtrForEachEntry( vClasses, pClass, i ) + { + Counter = 0; + for ( pObj = pClass; pObj; pObj = pObj->pNext ) + Counter++; + printf( " %d", Counter ); + } + printf( "\n" ); + } + return vClasses; +} + +/**Function************************************************************* + + Synopsis [Computes the equivalence classes of nodes using the base case.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames ) +{ + Vec_Ptr_t * vClasses; + int i, RetValue; + // derive the classes for the last frame + vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 ); + // refine the classes using other timeframes + for ( i = 0; i < nFrames - 1; i++ ) + { + if ( Vec_PtrSize(vClasses) == 0 ) + break; + RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses ); +// if ( RetValue ) +// printf( " yes%s", (i==nFrames-2 ? "\n":"") ); +// else +// printf( " no%s", (i==nFrames-2 ? "\n":"") ); + } + return vClasses; +} + + +/**Function************************************************************* + + Synopsis [Computes the equivalence classes of nodes.] + + Description [Original network (pNtk) is mapped into the unfolded frames + using given array of nodes (vCorresp). Each node in the unfolded frames + is mapped into a FRAIG node (pNode->pCopy). This procedure uses next + pointers (pNode->pNext) to combine the nodes into equivalence classes. + Each class is represented by its representative node with the minimum level. + Only the last frame is considered.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ) +{ + Abc_Obj_t * pNode, * pKey, ** ppSlot; + stmm_table * tTable; + stmm_generator * gen; + Vec_Ptr_t * vClasses; + int i; + // start the table hashing FRAIG nodes into classes of original network nodes + tTable = stmm_init_table( st_ptrcmp, st_ptrhash ); + // create the table + Abc_NtkCleanNext( pNtk ); + Abc_NtkForEachObj( pNtk, pNode, i ) + { + if ( Abc_ObjIsPo(pNode) ) + continue; + pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame ); + if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) ) + *ppSlot = NULL; + pNode->pNext = *ppSlot; + *ppSlot = pNode; + } + // collect only non-trivial classes + vClasses = Vec_PtrAlloc( 100 ); + stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode ) + if ( pNode->pNext ) + Vec_PtrPush( vClasses, pNode ); + stmm_free_table( tTable ); + return vClasses; +} + +/**Function************************************************************* + + Synopsis [Refines the classes using one frame.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ) +{ + Abc_Obj_t * pHeadSame, ** ppTailSame; + Abc_Obj_t * pHeadDiff, ** ppTailDiff; + Abc_Obj_t * pNode, * pClass, * pKey; + int i, k, fChange = 0; + Vec_PtrForEachEntry( vClasses, pClass, i ) + { +// assert( pClass->pNext ); + pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame ); + for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) + if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) + break; + if ( pNode == NULL ) + continue; + fChange = 1; + // create two classes + pHeadSame = NULL; ppTailSame = &pHeadSame; + pHeadDiff = NULL; ppTailDiff = &pHeadDiff; + for ( pNode = pClass; pNode; pNode = pNode->pNext ) + if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) + *ppTailDiff = pNode, ppTailDiff = &pNode->pNext; + else + *ppTailSame = pNode, ppTailSame = &pNode->pNext; + *ppTailSame = NULL; + *ppTailDiff = NULL; + assert( pHeadSame && pHeadDiff ); + // put the updated class back + Vec_PtrWriteEntry( vClasses, i, pHeadSame ); + // append the new class to be processed later + Vec_PtrPush( vClasses, pHeadDiff ); + } + // remove trivial classes + k = 0; + Vec_PtrForEachEntry( vClasses, pClass, i ) + if ( pClass->pNext ) + Vec_PtrWriteEntry( vClasses, k++, pClass ); + Vec_PtrShrink( vClasses, k ); + return fChange; +} + +/**Function************************************************************* + + Synopsis [Orders nodes in the equivalence classes.] + + Description [Finds a min-level representative of each class and puts it last.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ) +{ + Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin; + int i; + // go through the classes + Vec_PtrForEachEntry( vClasses, pClass, i ) + { + assert( pClass->pNext ); + pPrevMin = NULL; + pNodeMin = pClass; + for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext ) + if ( pNodeMin->Level >= pNode->Level ) + { + pPrevMin = pPrev; + pNodeMin = pNode; + } + if ( pNodeMin->pNext == NULL ) // already last + continue; + // update the class + if ( pNodeMin == pClass ) + Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext ); + else + pPrevMin->pNext = pNodeMin->pNext; + // attach the min node + assert( pPrev->pNext == NULL ); + pPrev->pNext = pNodeMin; + pNodeMin->pNext = NULL; + } + Vec_PtrForEachEntry( vClasses, pClass, i ) + assert( pClass->pNext ); +} + +/**Function************************************************************* + + Synopsis [Counts pairs of equivalent nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) +{ + Abc_Obj_t * pClass, * pNode; + int i, nPairs = 0; + Vec_PtrForEachEntry( vClasses, pClass, i ) + { + assert( pClass->pNext ); + for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) + nPairs++; + } + return nPairs; +} + +/**Function************************************************************* + + Synopsis [Sanity check for the class representation.] + + Description [Checks that pNode->pNext is only used in the classes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ) +{ + Abc_Obj_t * pClass, * pObj; + int i; + Abc_NtkCleanCopy( pNtkSingle ); + Vec_PtrForEachEntry( vClasses, pClass, i ) + for ( pObj = pClass; pObj; pObj = pObj->pNext ) + if ( pObj->pNext ) + pObj->pCopy = (Abc_Obj_t *)1; + Abc_NtkForEachObj( pNtkSingle, pObj, i ) + assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) ); + Abc_NtkCleanCopy( pNtkSingle ); +} + + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pRepr; + // skip CI and const + if ( Abc_ObjFaninNum(pNode) < 2 ) + return; + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + assert( Abc_ObjIsNode( pNode ) ); + // check if the node belongs to the class + if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) + Abc_NtkVanEijkDfs_rec( pRepr, vNodes ); + else + { + Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes ); + Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes ); + } + // add the node after the fanins have been added + Vec_PtrPush( vNodes, pNode ); +} + +/**Function************************************************************* + + Synopsis [Finds DFS ordering of nodes using equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes ); + return vNodes; +} + + +/**Function************************************************************* + + Synopsis [Derives the timeframes of the network.] + + Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ) +{ + char Buffer[100]; + Abc_Ntk_t * pNtkFrames; + Abc_Obj_t * pLatch, * pLatchNew; + Vec_Ptr_t * vOrder; + int i; + assert( nFrames > 0 ); + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkIsDfsOrdered(pNtk) ); + // clean the array of connections + if ( vCorresp ) + Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL ); + // start the new network + pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); + if ( fShortNames ) + { + pNtkFrames->pName = util_strsav(pNtk->pName); + pNtkFrames->pSpec = util_strsav(pNtk->pSpec); + } + else + { + sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); + pNtkFrames->pName = util_strsav(Buffer); + } + // map the constant nodes + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkFrames->pManFunc); + // create new latches and remember them in the new latches + Abc_NtkForEachLatch( pNtk, pLatch, i ) + Abc_NtkDupObj( pNtkFrames, pLatch ); + // collect nodes in such a way each class representative goes first + vOrder = Abc_NtkVanEijkDfs( pNtk ); + // create the timeframes + for ( i = 0; i < nFrames; i++ ) + Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames ); + Vec_PtrFree( vOrder ); + // add one more timeframe without class info + if ( fAddLast ) + Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames ); + // connect the new latches to the outputs of the last frame + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + pLatchNew = Abc_NtkLatch(pNtkFrames, i); + Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); + Vec_PtrPush( pNtkFrames->vCis, pLatchNew ); + Vec_PtrPush( pNtkFrames->vCos, pLatchNew ); + Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); + pLatch->pNext = NULL; + } + // remove dangling nodes + Abc_AigCleanup( pNtkFrames->pManFunc ); + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkFrames ) ) + printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); + return pNtkFrames; +} + +/**Function************************************************************* + + Synopsis [Adds one time frame to the new network.] + + Description [If the ordering of nodes is given, uses it. Otherwise, + uses the DSF order of the nodes in the network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ) +{ + char Buffer[10]; + Abc_Obj_t * pNode, * pLatch, * pRepr; + Vec_Ptr_t * vTemp; + int i; + // create the prefix to be added to the node names + sprintf( Buffer, "_%02d", iFrame ); + // add the new PI nodes + Abc_NtkForEachPi( pNtk, pNode, i ) + { + pNode->pCopy = Abc_NtkCreatePi(pNtkFrames); + if ( fShortNames ) + Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); + else + Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); + } + // remember the CI mapping + if ( vCorresp ) + { + pNode = Abc_AigConst1(pNtk->pManFunc); + Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); + Abc_NtkForEachCi( pNtk, pNode, i ) + Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); + } + // go through the nodes in the given order or in the natural order + if ( vOrder ) + { + // add the internal nodes + Vec_PtrForEachEntry( vOrder, pNode, i ) + { + if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) + pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase ); + else + pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); + assert( Abc_ObjRegular(pNode->pCopy) != NULL ); + if ( vCorresp ) + Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); + } + } + else + { + // add the internal nodes + Abc_AigForEachAnd( pNtk, pNode, i ) + { + pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); + assert( Abc_ObjRegular(pNode->pCopy) != NULL ); + if ( vCorresp ) + Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); + } + } + // add the new POs + Abc_NtkForEachPo( pNtk, pNode, i ) + { + pNode->pCopy = Abc_NtkCreatePo(pNtkFrames); + Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); + if ( fShortNames ) + Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); + else + Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); + } + // transfer the implementation of the latch drivers to the latches + vTemp = Vec_PtrAlloc( 100 ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pLatch->pCopy = Vec_PtrEntry( vTemp, i ); + Vec_PtrFree( vTemp ); + + Abc_AigForEachAnd( pNtk, pNode, i ) + pNode->pCopy = NULL; +} + +/**Function************************************************************* + + Synopsis [Fraigs the network with or without initialization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) +{ + Fraig_Man_t * pMan; + Fraig_Params_t Params; + ProgressBar * pProgress; + Abc_Obj_t * pNode; + int i; + assert( Abc_NtkIsStrash(pMulti) ); + // create the FRAIG manager + Fraig_ParamsSetDefaultFull( &Params ); + pMan = Fraig_ManCreate( &Params ); + // clean the copy fields in the old network + Abc_NtkCleanCopy( pMulti ); + // map the constant nodes + Abc_AigConst1(pMulti->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + if ( fInit ) + { + // map the PI nodes + Abc_NtkForEachPi( pMulti, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); + // map the latches + Abc_NtkForEachLatch( pMulti, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) ); + } + else + { + // map the CI nodes + Abc_NtkForEachCi( pMulti, pNode, i ) + pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); + } + // perform fraiging + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) ); + Abc_AigForEachAnd( pMulti, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, + Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), + Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); + } + Extra_ProgressBarStop( pProgress ); + return pMan; +} + + +/**Function************************************************************* + + Synopsis [Create EXDC from the equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pClass, * pNode, * pRepr, * pObj; + Abc_Obj_t * pMiter, * pTotal; + Vec_Ptr_t * vCone; + int i, k; + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + pNtkNew->pName = util_strsav("exdc"); + pNtkNew->pSpec = NULL; + + // map the constant nodes + Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc); + // for each CI, create PI + Abc_NtkForEachCi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) ); + // cannot add latches here because pLatch->pCopy pointers are used + + // create the cones for each pair of nodes in an equivalence class + pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) ); + Vec_PtrForEachEntry( vClasses, pClass, i ) + { + assert( pClass->pNext ); + // get the cone for the representative node + pRepr = Abc_NodeVanEijkRepr( pClass ); + if ( Abc_ObjFaninNum(pRepr) == 2 ) + { + vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 ); + Vec_PtrForEachEntry( vCone, pObj, k ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vCone ); + assert( pObj == pRepr ); + } + // go through the node pairs (representative is last in the list) + for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext ) + { + // get the cone for the node + assert( Abc_ObjFaninNum(pNode) == 2 ); + vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); + Vec_PtrForEachEntry( vCone, pObj, k ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Vec_PtrFree( vCone ); + assert( pObj == pNode ); + // complement if there is phase difference + pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase ); + // add the miter + pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy ); + } + // add the miter to the final + pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); + } + + // for each CO, create PO (skip POs equal to CIs because of name conflict) + Abc_NtkForEachPo( pNtk, pObj, i ) + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") ); + + // link to the POs of the network + Abc_NtkForEachPo( pNtk, pObj, i ) + if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) + Abc_ObjAddFanin( pObj->pCopy, pTotal ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjAddFanin( pObj->pCopy, pTotal ); + + // remove the extra nodes + Abc_AigCleanup( pNtkNew->pManFunc ); + + // check the result + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 2d5493ea..08a54e80 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -60,12 +60,12 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { - Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); // report the error pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); return; } if ( RetValue == 1 ) @@ -127,18 +127,18 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { - Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); // report the error pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); return; } if ( RetValue == 1 ) { - Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); + Abc_NtkDelete( pMiter ); return; } @@ -146,7 +146,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; - pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); // analyze the result @@ -315,7 +315,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; - pMan = Abc_NtkToFraig( pFrames, &Params, 0 ); + pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); // analyze the result diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 0123e213..4466cf99 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -22,4 +22,5 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcSymm.c \ src/base/abci/abcTiming.c \ src/base/abci/abcUnreach.c \ + src/base/abci/abcVanEijk.c \ src/base/abci/abcVerify.c diff --git a/src/base/abcs/module.make b/src/base/abcs/module.make index 309a8871..e8d5a8db 100644 --- a/src/base/abcs/module.make +++ b/src/base/abcs/module.make @@ -1,4 +1,6 @@ -SRC += src/base/abcs/abcRetCore.c \ +SRC += src/base/abcs/abcFpgaDelay.c \ + src/base/abcs/abcFpgaSeq.c \ + src/base/abcs/abcRetCore.c \ src/base/abcs/abcRetDelay.c \ src/base/abcs/abcRetImpl.c \ src/base/abcs/abcRetUtil.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index 2f7bd229..bffdfc10 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -32,6 +32,7 @@ static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -65,6 +66,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); @@ -643,6 +645,76 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk; + char * pSopCover; + int fHex; + int c; + + fHex = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "xh" ) ) != EOF ) + { + switch ( c ) + { + case 'x': + fHex ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + + // convert truth table to SOP + if ( fHex ) + pSopCover = Abc_SopFromTruthHex(argv[util_optind]); + else + pSopCover = Abc_SopFromTruthBin(argv[util_optind]); + if ( pSopCover == NULL ) + { + fprintf( pAbc->Err, "Reading truth table has failed.\n" ); + return 1; + } + + pNtk = Abc_NtkCreateWithNode( pSopCover ); + free( pSopCover ); + if ( pNtk == NULL ) + { + fprintf( pAbc->Err, "Deriving the network has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_truth [-xh] <truth>\n" ); + fprintf( pAbc->Err, "\t creates network with node having given truth table\n" ); + fprintf( pAbc->Err, "\t-x : toggles between bin and hex representation [default = %s]\n", fHex? "hex":"bin" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\ttruth : truth table with most signficant bit first (e.g. 1000 for AND(a,b))\n" ); + return 1; +} + /**Function************************************************************* diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 09824f38..5235d9a1 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -60,7 +60,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) // create solver with clauses pSat = Abc_NtkMiterSatCreate( pNtk ); // write the clauses - Asat_SolverWriteDimacs( pSat, pFileName ); + Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); // free the solver solver_delete( pSat ); return 1; diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 839aa0b4..bb776ab7 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -106,7 +106,7 @@ typedef unsigned long long uint64; /* Various Utilities */ /*===========================================================================*/ -/*=== extraUtilBdd.c ========================================================*/ +/*=== extraBddMisc.c ========================================================*/ extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute ); extern DdNode * Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f ); extern DdNode * Extra_bddRemapUp( DdManager * dd, DdNode * bF ); @@ -125,6 +125,14 @@ extern int * Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n extern DdNode * Extra_bddFindOneCube( DdManager * dd, DdNode * bF ); extern DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc ); extern DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ); +extern DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ); + +/*=== extraBddKmap.c ================================================================*/ + +/* displays the Karnaugh Map of a function */ +extern void Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames ); +/* displays the Karnaugh Map of a relation */ +extern void Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars ); /*=== extraBddSymm.c =================================================================*/ diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c new file mode 100644 index 00000000..bb43db68 --- /dev/null +++ b/src/misc/extra/extraBddKmap.c @@ -0,0 +1,783 @@ +/**CFile**************************************************************** + + FileName [extraBddKmap.c] + + PackageName [extra] + + Synopsis [Visualizing the K-map.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +/// K-map visualization using pseudo graphics /// +/// Version 1.0. Started - August 20, 2000 /// +/// Version 2.0. Added to EXTRA - July 17, 2001 /// + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +// the maximum number of variables in the Karnaugh Map +#define MAXVARS 20 + +/* +// single line +#define SINGLE_VERTICAL (char)179 +#define SINGLE_HORIZONTAL (char)196 +#define SINGLE_TOP_LEFT (char)218 +#define SINGLE_TOP_RIGHT (char)191 +#define SINGLE_BOT_LEFT (char)192 +#define SINGLE_BOT_RIGHT (char)217 + +// double line +#define DOUBLE_VERTICAL (char)186 +#define DOUBLE_HORIZONTAL (char)205 +#define DOUBLE_TOP_LEFT (char)201 +#define DOUBLE_TOP_RIGHT (char)187 +#define DOUBLE_BOT_LEFT (char)200 +#define DOUBLE_BOT_RIGHT (char)188 + +// line intersections +#define SINGLES_CROSS (char)197 +#define DOUBLES_CROSS (char)206 +#define S_HOR_CROSS_D_VER (char)215 +#define S_VER_CROSS_D_HOR (char)216 + +// single line joining +#define S_JOINS_S_VER_LEFT (char)180 +#define S_JOINS_S_VER_RIGHT (char)195 +#define S_JOINS_S_HOR_TOP (char)193 +#define S_JOINS_S_HOR_BOT (char)194 + +// double line joining +#define D_JOINS_D_VER_LEFT (char)185 +#define D_JOINS_D_VER_RIGHT (char)204 +#define D_JOINS_D_HOR_TOP (char)202 +#define D_JOINS_D_HOR_BOT (char)203 + +// single line joining double line +#define S_JOINS_D_VER_LEFT (char)182 +#define S_JOINS_D_VER_RIGHT (char)199 +#define S_JOINS_D_HOR_TOP (char)207 +#define S_JOINS_D_HOR_BOT (char)209 +*/ + +// single line +#define SINGLE_VERTICAL (char)'|' +#define SINGLE_HORIZONTAL (char)'-' +#define SINGLE_TOP_LEFT (char)'+' +#define SINGLE_TOP_RIGHT (char)'+' +#define SINGLE_BOT_LEFT (char)'+' +#define SINGLE_BOT_RIGHT (char)'+' + +// double line +#define DOUBLE_VERTICAL (char)'|' +#define DOUBLE_HORIZONTAL (char)'-' +#define DOUBLE_TOP_LEFT (char)'+' +#define DOUBLE_TOP_RIGHT (char)'+' +#define DOUBLE_BOT_LEFT (char)'+' +#define DOUBLE_BOT_RIGHT (char)'+' + +// line intersections +#define SINGLES_CROSS (char)'+' +#define DOUBLES_CROSS (char)'+' +#define S_HOR_CROSS_D_VER (char)'+' +#define S_VER_CROSS_D_HOR (char)'+' + +// single line joining +#define S_JOINS_S_VER_LEFT (char)'+' +#define S_JOINS_S_VER_RIGHT (char)'+' +#define S_JOINS_S_HOR_TOP (char)'+' +#define S_JOINS_S_HOR_BOT (char)'+' + +// double line joining +#define D_JOINS_D_VER_LEFT (char)'+' +#define D_JOINS_D_VER_RIGHT (char)'+' +#define D_JOINS_D_HOR_TOP (char)'+' +#define D_JOINS_D_HOR_BOT (char)'+' + +// single line joining double line +#define S_JOINS_D_VER_LEFT (char)'+' +#define S_JOINS_D_VER_RIGHT (char)'+' +#define S_JOINS_D_HOR_TOP (char)'+' +#define S_JOINS_D_HOR_BOT (char)'+' + + +// other symbols +#define UNDERSCORE (char)95 +//#define SYMBOL_ZERO (char)248 // degree sign +//#define SYMBOL_ZERO (char)'o' +#define SYMBOL_ZERO (char)' ' +#define SYMBOL_ONE (char)'1' +#define SYMBOL_DC (char)'-' +#define SYMBOL_OVERLAP (char)'?' + +// full cells and half cells +#define CELL_FREE (char)32 +#define CELL_FULL (char)219 +#define HALF_UPPER (char)223 +#define HALF_LOWER (char)220 +#define HALF_LEFT (char)221 +#define HALF_RIGHT (char)222 + + +/*---------------------------------------------------------------------------*/ +/* Structure declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +// the array of BDD variables used internally +static DdNode * s_XVars[MAXVARS]; + +// flag which determines where the horizontal variable names are printed +static int fHorizontalVarNamesPrintedAbove = 1; + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +// Oleg's way of generating the gray code +static int GrayCode( int BinCode ); +static int BinCode ( int GrayCode ); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Prints the K-map of the function.] + + Description [If the pointer to the array of variables XVars is NULL, + fSuppType determines how the support will be determined. + fSuppType == 0 -- takes the first nVars of the manager + fSuppType == 1 -- takes the topmost nVars of the manager + fSuppType == 2 -- determines support from the on-set and the offset + ] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_PrintKMap( + FILE * Output, /* the output stream */ + DdManager * dd, + DdNode * OnSet, + DdNode * OffSet, + int nVars, + DdNode ** XVars, + int fSuppType, /* the flag which determines how support is computed */ + char ** pVarNames ) +{ + int d, p, n, s, v, h, w; + int nVarsVer; + int nVarsHor; + int nCellsVer; + int nCellsHor; + int nSkipSpaces; + + // make sure that on-set and off-set do not overlap + if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) ) + { + fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" ); + return; + } +/* + if ( OnSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 1\n" ); + return; + } + if ( OffSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 0\n" ); + return; + } +*/ + if ( nVars < 0 || nVars > MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); + return; + } + + // determine the support if it is not given + if ( XVars == NULL ) + { + if ( fSuppType == 0 ) + { // assume that the support includes the first nVars of the manager + assert( nVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = Cudd_bddIthVar( dd, v ); + } + else if ( fSuppType == 1 ) + { // assume that the support includes the topmost nVars of the manager + assert( nVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] ); + } + else // determine the support + { + DdNode * SuppOn, * SuppOff, * Supp; + int cVars = 0; + DdNode * TempSupp; + + // determine support + SuppOn = Cudd_Support( dd, OnSet ); Cudd_Ref( SuppOn ); + SuppOff = Cudd_Support( dd, OffSet ); Cudd_Ref( SuppOff ); + Supp = Cudd_bddAnd( dd, SuppOn, SuppOff ); Cudd_Ref( Supp ); + Cudd_RecursiveDeref( dd, SuppOn ); + Cudd_RecursiveDeref( dd, SuppOff ); + + nVars = Cudd_SupportSize( dd, Supp ); + if ( nVars > MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS ); + Cudd_RecursiveDeref( dd, Supp ); + return; + } + + // assign variables + for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ ) + s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index ); + + Cudd_RecursiveDeref( dd, TempSupp ); + } + } + else + { + // copy variables + assert( XVars ); + for ( v = 0; v < nVars; v++ ) + s_XVars[v] = XVars[v]; + } + + //////////////////////////////////////////////////////////////////// + // determine the Karnaugh map parameters + nVarsVer = nVars/2; + nVarsHor = nVars - nVarsVer; + nCellsVer = (1<<nVarsVer); + nCellsHor = (1<<nVarsHor); + nSkipSpaces = nVarsVer + 1; + + //////////////////////////////////////////////////////////////////// + // print variable names + fprintf( Output, "\n" ); + for ( w = 0; w < nVarsVer; w++ ) + if ( pVarNames == NULL ) + fprintf( Output, "%c", 'a'+nVarsHor+w ); + else + fprintf( Output, " %s", pVarNames[nVarsHor+w] ); + + if ( fHorizontalVarNamesPrintedAbove ) + { + fprintf( Output, " \\ " ); + for ( w = 0; w < nVarsHor; w++ ) + if ( pVarNames == NULL ) + fprintf( Output, "%c", 'a'+w ); + else + fprintf( Output, "%s ", pVarNames[w] ); + } + fprintf( Output, "\n" ); + + if ( fHorizontalVarNamesPrintedAbove ) + { + //////////////////////////////////////////////////////////////////// + // print horizontal digits + for ( d = 0; d < nVarsHor; d++ ) + { + for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nCellsHor; n++ ) + if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) + fprintf( Output, "1 " ); + else + fprintf( Output, "0 " ); + fprintf( Output, "\n" ); + } + } + + //////////////////////////////////////////////////////////////////// + // print the upper line + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + fprintf( Output, "%c", DOUBLE_TOP_LEFT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", D_JOINS_D_HOR_BOT ); + else + fprintf( Output, "%c", S_JOINS_D_HOR_BOT ); + } + fprintf( Output, "%c", DOUBLE_TOP_RIGHT ); + fprintf( Output, "\n" ); + + //////////////////////////////////////////////////////////////////// + // print the map + for ( v = 0; v < nCellsVer; v++ ) + { + DdNode * CubeVerBDD; + + // print horizontal digits +// for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nVarsVer; n++ ) + if ( GrayCode(v) & (1<<(nVarsVer-1-n)) ) + fprintf( Output, "1" ); + else + fprintf( Output, "0" ); + fprintf( Output, " " ); + + // find vertical cube + CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 ); Cudd_Ref( CubeVerBDD ); + + // print text line + fprintf( Output, "%c", DOUBLE_VERTICAL ); + for ( h = 0; h < nCellsHor; h++ ) + { + DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet; + + fprintf( Output, " " ); +// fprintf( Output, "x" ); + /////////////////////////////////////////////////////////////// + // determine what should be printed + CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 ); Cudd_Ref( CubeHorBDD ); + Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod ); + Cudd_RecursiveDeref( dd, CubeHorBDD ); + + ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet ); + ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet ); + Cudd_RecursiveDeref( dd, Prod ); + + if ( ValueOnSet == b1 && ValueOffSet == b0 ) + fprintf( Output, "%c", SYMBOL_ONE ); + else if ( ValueOnSet == b0 && ValueOffSet == b1 ) + fprintf( Output, "%c", SYMBOL_ZERO ); + else if ( ValueOnSet == b0 && ValueOffSet == b0 ) + fprintf( Output, "%c", SYMBOL_DC ); + else if ( ValueOnSet == b1 && ValueOffSet == b1 ) + fprintf( Output, "%c", SYMBOL_OVERLAP ); + else + assert(0); + + Cudd_RecursiveDeref( dd, ValueOnSet ); + Cudd_RecursiveDeref( dd, ValueOffSet ); + /////////////////////////////////////////////////////////////// + fprintf( Output, " " ); + + if ( h != nCellsHor-1 ) + if ( h&1 ) + fprintf( Output, "%c", DOUBLE_VERTICAL ); + else + fprintf( Output, "%c", SINGLE_VERTICAL ); + } + fprintf( Output, "%c", DOUBLE_VERTICAL ); + fprintf( Output, "\n" ); + + Cudd_RecursiveDeref( dd, CubeVerBDD ); + + if ( v != nCellsVer-1 ) + // print separator line + { + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + if ( v&1 ) + { + fprintf( Output, "%c", D_JOINS_D_VER_RIGHT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", DOUBLES_CROSS ); + else + fprintf( Output, "%c", S_VER_CROSS_D_HOR ); + } + fprintf( Output, "%c", D_JOINS_D_VER_LEFT ); + } + else + { + fprintf( Output, "%c", S_JOINS_D_VER_RIGHT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", S_HOR_CROSS_D_VER ); + else + fprintf( Output, "%c", SINGLES_CROSS ); + } + fprintf( Output, "%c", S_JOINS_D_VER_LEFT ); + } + fprintf( Output, "\n" ); + } + } + + //////////////////////////////////////////////////////////////////// + // print the lower line + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + fprintf( Output, "%c", DOUBLE_BOT_LEFT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", D_JOINS_D_HOR_TOP ); + else + fprintf( Output, "%c", S_JOINS_D_HOR_TOP ); + } + fprintf( Output, "%c", DOUBLE_BOT_RIGHT ); + fprintf( Output, "\n" ); + + if ( !fHorizontalVarNamesPrintedAbove ) + { + //////////////////////////////////////////////////////////////////// + // print horizontal digits + for ( d = 0; d < nVarsHor; d++ ) + { + for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nCellsHor; n++ ) + if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) + fprintf( Output, "1 " ); + else + fprintf( Output, "0 " ); + + ///////////////////////////////// + fprintf( Output, "%c", (char)('a'+d) ); + ///////////////////////////////// + fprintf( Output, "\n" ); + } + } +} + + + +/**Function******************************************************************** + + Synopsis [Prints the K-map of the relation.] + + Description [Assumes that the relation depends the first nXVars of XVars and + the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_PrintKMapRelation( + FILE * Output, /* the output stream */ + DdManager * dd, + DdNode * OnSet, + DdNode * OffSet, + int nXVars, + int nYVars, + DdNode ** XVars, + DdNode ** YVars ) /* the flag which determines how support is computed */ +{ + int d, p, n, s, v, h, w; + int nVars; + int nVarsVer; + int nVarsHor; + int nCellsVer; + int nCellsHor; + int nSkipSpaces; + + // make sure that on-set and off-set do not overlap + if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) ) + { + fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" ); + return; + } + + if ( OnSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 1\n" ); + return; + } + if ( OffSet == b1 ) + { + fprintf( Output, "PrintKMap(): Constant 0\n" ); + return; + } + + nVars = nXVars + nYVars; + if ( nVars < 0 || nVars > MAXVARS ) + { + fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS ); + return; + } + + + //////////////////////////////////////////////////////////////////// + // determine the Karnaugh map parameters + nVarsVer = nXVars; + nVarsHor = nYVars; + nCellsVer = (1<<nVarsVer); + nCellsHor = (1<<nVarsHor); + nSkipSpaces = nVarsVer + 1; + + //////////////////////////////////////////////////////////////////// + // print variable names + fprintf( Output, "\n" ); + for ( w = 0; w < nVarsVer; w++ ) + fprintf( Output, "%c", 'a'+nVarsHor+w ); + if ( fHorizontalVarNamesPrintedAbove ) + { + fprintf( Output, " \\ " ); + for ( w = 0; w < nVarsHor; w++ ) + fprintf( Output, "%c", 'a'+w ); + } + fprintf( Output, "\n" ); + + if ( fHorizontalVarNamesPrintedAbove ) + { + //////////////////////////////////////////////////////////////////// + // print horizontal digits + for ( d = 0; d < nVarsHor; d++ ) + { + for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nCellsHor; n++ ) + if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) + fprintf( Output, "1 " ); + else + fprintf( Output, "0 " ); + fprintf( Output, "\n" ); + } + } + + //////////////////////////////////////////////////////////////////// + // print the upper line + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + fprintf( Output, "%c", DOUBLE_TOP_LEFT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", D_JOINS_D_HOR_BOT ); + else + fprintf( Output, "%c", S_JOINS_D_HOR_BOT ); + } + fprintf( Output, "%c", DOUBLE_TOP_RIGHT ); + fprintf( Output, "\n" ); + + //////////////////////////////////////////////////////////////////// + // print the map + for ( v = 0; v < nCellsVer; v++ ) + { + DdNode * CubeVerBDD; + + // print horizontal digits +// for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nVarsVer; n++ ) + if ( GrayCode(v) & (1<<(nVarsVer-1-n)) ) + fprintf( Output, "1" ); + else + fprintf( Output, "0" ); + fprintf( Output, " " ); + + // find vertical cube +// CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor ); Cudd_Ref( CubeVerBDD ); + CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 ); Cudd_Ref( CubeVerBDD ); + + // print text line + fprintf( Output, "%c", DOUBLE_VERTICAL ); + for ( h = 0; h < nCellsHor; h++ ) + { + DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet; + + fprintf( Output, " " ); +// fprintf( Output, "x" ); + /////////////////////////////////////////////////////////////// + // determine what should be printed +// CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars ); Cudd_Ref( CubeHorBDD ); + CubeHorBDD = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 ); Cudd_Ref( CubeHorBDD ); + Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD ); Cudd_Ref( Prod ); + Cudd_RecursiveDeref( dd, CubeHorBDD ); + + ValueOnSet = Cudd_Cofactor( dd, OnSet, Prod ); Cudd_Ref( ValueOnSet ); + ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod ); Cudd_Ref( ValueOffSet ); + Cudd_RecursiveDeref( dd, Prod ); + + if ( ValueOnSet == b1 && ValueOffSet == b0 ) + fprintf( Output, "%c", SYMBOL_ONE ); + else if ( ValueOnSet == b0 && ValueOffSet == b1 ) + fprintf( Output, "%c", SYMBOL_ZERO ); + else if ( ValueOnSet == b0 && ValueOffSet == b0 ) + fprintf( Output, "%c", SYMBOL_DC ); + else if ( ValueOnSet == b1 && ValueOffSet == b1 ) + fprintf( Output, "%c", SYMBOL_OVERLAP ); + else + assert(0); + + Cudd_RecursiveDeref( dd, ValueOnSet ); + Cudd_RecursiveDeref( dd, ValueOffSet ); + /////////////////////////////////////////////////////////////// + fprintf( Output, " " ); + + if ( h != nCellsHor-1 ) + if ( h&1 ) + fprintf( Output, "%c", DOUBLE_VERTICAL ); + else + fprintf( Output, "%c", SINGLE_VERTICAL ); + } + fprintf( Output, "%c", DOUBLE_VERTICAL ); + fprintf( Output, "\n" ); + + Cudd_RecursiveDeref( dd, CubeVerBDD ); + + if ( v != nCellsVer-1 ) + // print separator line + { + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + if ( v&1 ) + { + fprintf( Output, "%c", D_JOINS_D_VER_RIGHT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", DOUBLES_CROSS ); + else + fprintf( Output, "%c", S_VER_CROSS_D_HOR ); + } + fprintf( Output, "%c", D_JOINS_D_VER_LEFT ); + } + else + { + fprintf( Output, "%c", S_JOINS_D_VER_RIGHT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + fprintf( Output, "%c", SINGLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", S_HOR_CROSS_D_VER ); + else + fprintf( Output, "%c", SINGLES_CROSS ); + } + fprintf( Output, "%c", S_JOINS_D_VER_LEFT ); + } + fprintf( Output, "\n" ); + } + } + + //////////////////////////////////////////////////////////////////// + // print the lower line + for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) ); + fprintf( Output, "%c", DOUBLE_BOT_LEFT ); + for ( s = 0; s < nCellsHor; s++ ) + { + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + fprintf( Output, "%c", DOUBLE_HORIZONTAL ); + if ( s != nCellsHor-1 ) + if ( s&1 ) + fprintf( Output, "%c", D_JOINS_D_HOR_TOP ); + else + fprintf( Output, "%c", S_JOINS_D_HOR_TOP ); + } + fprintf( Output, "%c", DOUBLE_BOT_RIGHT ); + fprintf( Output, "\n" ); + + if ( !fHorizontalVarNamesPrintedAbove ) + { + //////////////////////////////////////////////////////////////////// + // print horizontal digits + for ( d = 0; d < nVarsHor; d++ ) + { + for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) ); + for ( n = 0; n < nCellsHor; n++ ) + if ( GrayCode(n) & (1<<(nVarsHor-1-d)) ) + fprintf( Output, "1 " ); + else + fprintf( Output, "0 " ); + + ///////////////////////////////// + fprintf( Output, "%c", (char)('a'+d) ); + ///////////////////////////////// + fprintf( Output, "\n" ); + } + } +} + + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int GrayCode ( int BinCode ) +{ + return BinCode ^ ( BinCode >> 1 ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int BinCode ( int GrayCode ) +{ + int bc = GrayCode; + while( GrayCode >>= 1 ) bc ^= GrayCode; + return bc; +} + + diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 373ce5c5..932ed525 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + Revision [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $] ***********************************************************************/ @@ -684,6 +684,41 @@ DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop ) return bProd; } +/**Function******************************************************************** + + Synopsis [Computes the cube of BDD variables corresponding to bits it the bit-code] + + Description [Returns a bdd composed of elementary bdds found in array BddVars[] such + that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, + the most significant bit is encoded with the first bdd variable). If the variables + BddVars are not specified, takes the first CodeWidth variables of the manager] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst ) +{ + int z; + DdNode * bTemp, * bVar, * bVarBdd, * bResult; + + bResult = b1; Cudd_Ref( bResult ); + for ( z = 0; z < CodeWidth; z++ ) + { + bVarBdd = (pbVars)? pbVars[z]: dd->vars[z]; + if ( fMsbFirst ) + bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 ); + else + bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 ); + bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bResult ); + + return bResult; +} /* end of Extra_bddBitsToCube */ + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 6cbf5d2c..42a0d84f 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,4 +1,5 @@ -SRC += src/misc/extra/extraBddMisc.c \ +SRC += src/misc/extra/extraBddKmap.c \ + src/misc/extra/extraBddMisc.c \ src/misc/extra/extraBddSymm.c \ src/misc/extra/extraUtilBitMatrix.c \ src/misc/extra/extraUtilCanon.c \ diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make index 2e7519d1..af2d8fc1 100644 --- a/src/opt/cut/module.make +++ b/src/opt/cut/module.make @@ -3,5 +3,6 @@ SRC += src/opt/cut/cutApi.c \ src/opt/cut/cutMan.c \ src/opt/cut/cutMerge.c \ src/opt/cut/cutNode.c \ + src/opt/cut/cutOracle.c \ src/opt/cut/cutSeq.c \ src/opt/cut/cutTruth.c diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c index 786b7583..a9f0dd88 100644 --- a/src/opt/sim/simSupp.c +++ b/src/opt/sim/simSupp.c @@ -470,7 +470,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) Params.nSeconds = ABC_INFINITY; Params.fInternal = 1; clk = clock(); - pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); p->timeFraig += clock() - clk; clk = clock(); Fraig_ManProveMiter( pMan ); diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c index a98d4b5e..d9821088 100644 --- a/src/opt/sim/simSymSat.c +++ b/src/opt/sim/simSymSat.c @@ -147,7 +147,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * Params.nSeconds = ABC_INFINITY; clk = clock(); - pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); p->timeFraig += clock() - clk; clk = clock(); Fraig_ManProveMiter( pMan ); diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index d7358749..662fe1ff 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $] ***********************************************************************/ @@ -57,7 +57,7 @@ static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) SeeAlso [] ***********************************************************************/ -void Asat_SolverWriteDimacs( solver * p, char * pFileName ) +void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) { FILE * pFile; void ** pClauses; @@ -78,18 +78,31 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName ) nClauses = p->clauses.size; pClauses = p->clauses.ptr; for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); + Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); // write the learned clauses nClauses = p->learnts.size; pClauses = p->learnts.ptr; for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 ); + Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); // write zero-level assertions for ( i = 0; i < p->size; i++ ) if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) - fprintf( pFile, "%s%d 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 ); + fprintf( pFile, "%s%d%s\n", + (p->assigns[i] == l_False)? "-": "", + i + (int)(incrementVars>0), + (incrementVars) ? " 0" : ""); + + // write the assumptions + if (assumptionsBegin) { + for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) { + fprintf( pFile, "%s%d%s\n", + lit_sign(*assumptionsBegin)? "-": "", + lit_var(*assumptionsBegin) + (int)(incrementVars>0), + (incrementVars) ? " 0" : ""); + } + } fprintf( pFile, "\n" ); fclose( pFile ); diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index d248b115..3927fac3 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -1099,7 +1099,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds) nof_conflicts *= 1.5; nof_learnts *= 1.1; // if the runtime limit is exceeded, quit the restart loop - if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC ) + if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) ) break; } if (s->verbosity >= 1) diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 9f80bc7e..b82601c4 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -73,7 +73,9 @@ extern int solver_nvars(solver* s); extern int solver_nclauses(solver* s); // additional procedures -extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName ); +extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, + lit* assumptionsBegin, lit* assumptionsEnd, + int incrementVars); struct stats_t { diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 1f324c4b..a34f3b9a 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -542,7 +542,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) else if ( mng->mode == 1 ) // resource-aware fraiging { // transform the target into a fraig - pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); + pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0, 0 ); Fraig_ManProveMiter( pMan ); RetValue = Fraig_ManCheckMiter( pMan ); diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 75dfb812..dc679907 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -149,6 +149,7 @@ extern void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t /*=== fraigMan.c =============================================================*/ extern void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ); +extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ); extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ); extern void Fraig_ManFree( Fraig_Man_t * pMan ); extern void Fraig_ManPrintStats( Fraig_Man_t * p ); diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index aa7e5999..1a34af86 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -60,6 +60,35 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) /**Function************************************************************* + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for complete FRAIGing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ) +{ + memset( pParams, 0, sizeof(Fraig_Params_t) ); + pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info + pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info + pParams->nBTLimit = -1; // the max number of backtracks to perform + pParams->nSeconds = 20; // the max number of seconds to solve the miter + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 1; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 0; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run +} + +/**Function************************************************************* + Synopsis [Creates the new FRAIG manager.] Description [] |