diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-11 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-11 08:01:00 -0800 |
| commit | 77d7377442c28fd5c65144d7ea23938600967b2b (patch) | |
| tree | dad44cc2d4bad07bf91c47c889c8c8c46ef13006 /src | |
| parent | c0ef1f469a3204adbd26edec0b9d3af56532d794 (diff) | |
| download | abc-77d7377442c28fd5c65144d7ea23938600967b2b.tar.gz abc-77d7377442c28fd5c65144d7ea23938600967b2b.tar.bz2 abc-77d7377442c28fd5c65144d7ea23938600967b2b.zip | |
Version abc60211
Diffstat (limited to 'src')
59 files changed, 4328 insertions, 222 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index cbdf87c7..7ace4880 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -425,7 +425,7 @@ extern void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); /*=== abcBalance.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); +extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ); /*=== abcCheck.c ==========================================================*/ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ); @@ -587,6 +587,7 @@ extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, Dd extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax ); /*=== abcRefs.c ==========================================================*/ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); +extern int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); @@ -673,6 +674,7 @@ 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 void Abc_NtkCleanMarkA( 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/abcRefs.c b/src/base/abc/abcRefs.c index 04647d0b..5d0c68d1 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -25,6 +25,7 @@ //////////////////////////////////////////////////////////////////////// static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes ); +static int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes ); static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ); static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); @@ -46,6 +47,7 @@ static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); int Abc_NodeMffcSize( Abc_Obj_t * pNode ) { int nConeSize1, nConeSize2; + assert( Abc_NtkIsStrash(pNode->pNtk) ); assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); if ( Abc_ObjFaninNum(pNode) == 0 ) @@ -59,6 +61,36 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Returns the MFFC size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vNodes; + int nSuppSize, nConeSize1, nConeSize2; + assert( Abc_NtkIsStrash(pNode->pNtk) ); + assert( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_ObjIsNode( pNode ) ); + if ( Abc_ObjFaninNum(pNode) == 0 ) + return 0; + vNodes = Vec_PtrAlloc( 10 ); + nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0, vNodes ); // dereference + nSuppSize = Abc_NodeMffcCountSupp(vNodes); + nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference + assert( nConeSize1 == nConeSize2 ); + assert( nConeSize1 > 0 ); + Vec_PtrFree(vNodes); + return nSuppSize; +} + +/**Function************************************************************* + Synopsis [Returns the MFFC size while stopping at the complemented edges.] Description [] @@ -71,6 +103,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ) { int nConeSize1, nConeSize2; + assert( Abc_NtkIsStrash(pNode->pNtk) ); assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); if ( Abc_ObjFaninNum(pNode) == 0 ) @@ -219,6 +252,61 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t /**Function************************************************************* + Synopsis [References/references the node and returns MFFC supp size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pNode, * pNode0, * pNode1; + int i, Counter = 0; + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_ObjIsCi(pNode) ) + { + if ( pNode->fMarkB == 0 ) + { + pNode->fMarkB = 1; + Counter++; + } + continue; + } + pNode0 = Abc_ObjFanin0(pNode); + if ( pNode0->vFanouts.nSize > 0 && pNode0->fMarkB == 0 ) + { + pNode0->fMarkB = 1; + Counter++; + } + pNode1 = Abc_ObjFanin1(pNode); + if ( pNode1->vFanouts.nSize > 0 && pNode1->fMarkB == 0 ) + { + pNode1->fMarkB = 1; + Counter++; + } + } + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_ObjIsCi(pNode) ) + { + pNode->fMarkB = 0; + continue; + } + pNode0 = Abc_ObjFanin0(pNode); + pNode0->fMarkB = 0; + pNode1 = Abc_ObjFanin1(pNode); + pNode1->fMarkB = 0; + } + return Counter; + +} + +/**Function************************************************************* + Synopsis [References/references the node and returns MFFC size.] Description [] diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index 4152dd0a..1e59b17b 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -308,7 +308,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars ) char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars ) { assert( nVars == 2 ); - return Abc_SopRegister(pMan, "11 1\n11 1\n"); + return Abc_SopRegister(pMan, "11 1\n00 1\n"); } /**Function************************************************************* diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 9d95fade..1e52e4a6 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -335,6 +335,25 @@ void Abc_NtkCleanNext( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Cleans the copy field of all objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkA = 0; +} + +/**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 5f5c4b49..119f8cdf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40,6 +40,8 @@ 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_CommandPrintUnate ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -137,6 +139,8 @@ 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_unate", Abc_CommandPrintUnate, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_auto", Abc_CommandPrintAuto, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_kmap", Abc_CommandPrintKMap, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 ); @@ -247,7 +251,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fFactor; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -310,7 +314,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -398,7 +402,7 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Obj_t * pNode; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -467,7 +471,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -517,7 +521,7 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -570,7 +574,7 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fUseRealNames; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -653,7 +657,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) int fListNodes; int fProfile; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -742,7 +746,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -817,7 +821,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -884,6 +888,160 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandPrintUnate( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fUseBdds; + int fUseNaive; + int fVerbose; + extern void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fUseBdds = 1; + fUseNaive = 0; + fVerbose = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fUseBdds ^= 1; + break; + case 'n': + fUseNaive ^= 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_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" ); + return 1; + } + Abc_NtkPrintUnate( pNtk, fUseBdds, fUseNaive, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: print_unate [-bnvh]\n" ); + fprintf( pErr, "\t computes unate variables of the PO functions\n" ); + fprintf( pErr, "\t-b : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "BDD": "SAT" ); + fprintf( pErr, "\t-n : toggle naive BDD-based computation [default = %s].\n", fUseNaive? "yes": "no" ); + fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int Output; + int fNaive; + int fVerbose; + extern void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Output = -1; + fNaive = 0; + fVerbose = 0; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "Onvh" ) ) != EOF ) + { + switch ( c ) + { + case 'O': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + Output = atoi(argv[util_optind]); + util_optind++; + if ( Output < 0 ) + goto usage; + break; + case 'n': + fNaive ^= 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_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs (run \"strash\").\n" ); + return 1; + } + + + Abc_NtkAutoPrint( pNtk, Output, fNaive, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: print_auto [-O num] [-nvh]\n" ); + fprintf( pErr, "\t computes autosymmetries of the PO functions\n" ); + fprintf( pErr, "\t-O num : (optional) the 0-based number of the output [default = all]\n"); + fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" ); + fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -894,7 +1052,7 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -981,7 +1139,7 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1044,7 +1202,7 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1106,7 +1264,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern void Abc_NodeShowBdd( Abc_Obj_t * pNode ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1194,7 +1352,7 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConeSizeMax; extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1295,7 +1453,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk ); extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1369,7 +1527,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv ) int fGateNames; extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1432,7 +1590,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1506,7 +1664,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAllNodes; int fCleanup; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1573,22 +1731,27 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp; int c; - int fDuplicate; + bool fDuplicate; + bool fSelective; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults fDuplicate = 0; + fSelective = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "dsh" ) ) != EOF ) { switch ( c ) { case 'd': fDuplicate ^= 1; break; + case 's': + fSelective ^= 1; + break; case 'h': goto usage; default: @@ -1610,7 +1773,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) { - pNtkRes = Abc_NtkBalance( pNtk, fDuplicate ); + pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective ); } else { @@ -1620,7 +1783,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before balancing has failed.\n" ); return 1; } - pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate ); + pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective ); Abc_NtkDelete( pNtkTemp ); } @@ -1635,9 +1798,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: balance [-dh]\n" ); + fprintf( pErr, "usage: balance [-dsh]\n" ); fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" ); fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" ); + fprintf( pErr, "\t-s : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -1662,7 +1826,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) int fMulti; int fSimple; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1769,7 +1933,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1824,7 +1988,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1883,7 +2047,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) extern bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ); extern void Abc_NtkFxuFreeInfo( Fxu_Data_t * p ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2010,7 +2174,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ); extern int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2136,7 +2300,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Rwr_Precompute(); extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2233,7 +2397,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) bool fVerbose; extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2351,7 +2515,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2420,7 +2584,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCheck; int fComb; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2491,7 +2655,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFrames; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2575,7 +2739,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2635,7 +2799,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2696,7 +2860,7 @@ int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2757,7 +2921,7 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2825,7 +2989,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; int nSeconds; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -2887,7 +3051,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) */ if ( Abc_NtkIsStrash(pNtk) ) { - RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose ); + RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); if ( RetValue == -1 ) printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -2899,7 +3063,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pTemp; pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose ); + RetValue = Abc_NtkMiterSat( pTemp, nSeconds, fVerbose ); if ( RetValue == -1 ) printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -2939,7 +3103,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3010,7 +3174,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) int fUseAllCis; int Output; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3122,7 +3286,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Obj_t * pNode; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3202,7 +3366,7 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3251,7 +3415,7 @@ int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3311,7 +3475,7 @@ int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3369,7 +3533,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv ) char * FileName; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3461,7 +3625,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); extern void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * pCutOracle ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3591,7 +3755,7 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3696,7 +3860,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFaninMax; extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3784,9 +3948,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); +// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -3819,7 +3983,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // printf( "This command is currently not used.\n" ); // run the command // pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); - pNtkRes = Abc_NtkNewAig( pNtk ); + +// pNtkRes = Abc_NtkNewAig( pNtk ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -3859,7 +4025,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fExdc; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4017,7 +4183,7 @@ int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fDuplicate; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4081,7 +4247,7 @@ int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fDuplicate; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4142,7 +4308,7 @@ int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fDuplicate; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4206,7 +4372,7 @@ int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fDuplicate; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4258,7 +4424,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4345,7 +4511,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) 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); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4410,7 +4576,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -4481,7 +4647,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4542,7 +4708,7 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4605,7 +4771,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4678,7 +4844,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4740,7 +4906,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -4806,7 +4972,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -4863,7 +5029,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -4931,7 +5097,7 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) int fRandom; int fDontCare; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5039,7 +5205,7 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv ) int nLatches; extern void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5115,7 +5281,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5192,7 +5358,7 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fShare; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5269,7 +5435,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) int fInitial; int fVerbose; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5395,7 +5561,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nMaxIters; int fVerbose; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5459,7 +5625,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 ); + pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 ); Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -5519,7 +5685,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nMaxIters; int fVerbose; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5583,7 +5749,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0 ); + pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 ); Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -5649,7 +5815,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5756,7 +5922,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5822,7 +5988,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -5914,7 +6080,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c new file mode 100644 index 00000000..752943c3 --- /dev/null +++ b/src/base/abci/abcAuto.c @@ -0,0 +1,229 @@ +/**CFile**************************************************************** + + FileName [abcAuto.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Computation of autosymmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcAuto.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive ); +static void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) +{ + DdManager * dd; // the BDD manager used to hold shared BDDs + DdNode ** pbGlobal; // temporary storage for global BDDs + char ** pInputNames; // pointers to the CI names + char ** pOutputNames; // pointers to the CO names + int nOutputs, nInputs, i; + + // compute the global BDDs + if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + return; + + // get information about the network + nInputs = Abc_NtkCiNum(pNtk); + nOutputs = Abc_NtkCoNum(pNtk); + dd = pNtk->pManGlob; + pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob ); + + // get the network names + pInputNames = Abc_NtkCollectCioNames( pNtk, 0 ); + pOutputNames = Abc_NtkCollectCioNames( pNtk, 1 ); + + // print the size of the BDDs + if ( fVerbose ) + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // allocate additional variables + for ( i = 0; i < nInputs; i++ ) + Cudd_bddNewVar( dd ); + assert( Cudd_ReadSize(dd) == 2 * nInputs ); + + // create ZDD variables in the manager + Cudd_zddVarsFromBddVars( dd, 2 ); + + // perform the analysis of the primary output functions for auto-symmetry + if ( Output == -1 ) + Abc_NtkAutoPrintAll( dd, nInputs, pbGlobal, nOutputs, pInputNames, pOutputNames, fNaive ); + else + Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive ); + + // deref the PO functions + Abc_NtkFreeGlobalBdds( pNtk ); + // stop the global BDD manager + Extra_StopManager( pNtk->pManGlob ); + pNtk->pManGlob = NULL; + free( pInputNames ); + free( pOutputNames ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAutoPrintAll( DdManager * dd, int nInputs, DdNode * pbOutputs[], int nOutputs, char * pInputNames[], char * pOutputNames[], int fNaive ) +{ + DdNode * bSpace1, * bSpace2, * bCanVars, * bReduced, * zEquations; + double nMints; + int nSupp, SigCounter, o; + + int nAutos; + int nAutoSyms; + int nAutoSymsMax; + int nAutoSymsMaxSupp; + int nAutoSymOuts; + int nSuppSizeMax; + int clk; + + nAutoSymOuts = 0; + nAutoSyms = 0; + nAutoSymsMax = 0; + nAutoSymsMaxSupp = 0; + nSuppSizeMax = 0; + clk = clock(); + + SigCounter = 0; + for ( o = 0; o < nOutputs; o++ ) + { + bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[o] ); Cudd_Ref( bSpace1 ); +// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[o], pbOutputs[o] ); Cudd_Ref( bSpace1 ); + bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars ); + bReduced = Extra_bddSpaceReduce( dd, pbOutputs[o], bCanVars ); Cudd_Ref( bReduced ); + zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations ); + + nSupp = Cudd_SupportSize( dd, bSpace1 ); + nMints = Cudd_CountMinterm( dd, bSpace1, nSupp ); + nAutos = Extra_Base2LogDouble(nMints); + printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", o, nSupp, nAutos ); + + if ( nAutos > 0 ) + { + nAutoSymOuts++; + nAutoSyms += nAutos; + if ( nAutoSymsMax < nAutos ) + { + nAutoSymsMax = nAutos; + nAutoSymsMaxSupp = nSupp; + } + } + if ( nSuppSizeMax < nSupp ) + nSuppSizeMax = nSupp; + + +//PRB( dd, bCanVars ); +//PRB( dd, bReduced ); +//Cudd_PrintMinterm( dd, bReduced ); +//printf( "The equations are:\n" ); +//Cudd_zddPrintCover( dd, zEquations ); +//printf( "\n" ); +//fflush( stdout ); + + bSpace2 = Extra_bddSpaceFromMatrixPos( dd, zEquations ); Cudd_Ref( bSpace2 ); +//PRB( dd, bSpace1 ); +//PRB( dd, bSpace2 ); + if ( bSpace1 != bSpace2 ) + printf( "Spaces are NOT EQUAL!\n" ); +// else +// printf( "Spaces are equal.\n" ); + + Cudd_RecursiveDeref( dd, bSpace1 ); + Cudd_RecursiveDeref( dd, bSpace2 ); + Cudd_RecursiveDeref( dd, bCanVars ); + Cudd_RecursiveDeref( dd, bReduced ); + Cudd_RecursiveDerefZdd( dd, zEquations ); + } + + printf( "The cumulative statistics for all outputs:\n" ); + printf( "Ins=%3d ", nInputs ); + printf( "InMax=%3d ", nSuppSizeMax ); + printf( "Outs=%3d ", nOutputs ); + printf( "Auto=%3d ", nAutoSymOuts ); + printf( "SumK=%3d ", nAutoSyms ); + printf( "KMax=%2d ", nAutoSymsMax ); + printf( "Supp=%3d ", nAutoSymsMaxSupp ); + printf( "Time=%4.2f ", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAutoPrintOne( DdManager * dd, int nInputs, DdNode * pbOutputs[], int Output, char * pInputNames[], char * pOutputNames[], int fNaive ) +{ + DdNode * bSpace1, * bCanVars, * bReduced, * zEquations; + double nMints; + int nSupp, SigCounter; + int nAutos; + + SigCounter = 0; + bSpace1 = Extra_bddSpaceFromFunctionFast( dd, pbOutputs[Output] ); Cudd_Ref( bSpace1 ); +// bSpace1 = Extra_bddSpaceFromFunction( dd, pbOutputs[Output], pbOutputs[Output] ); Cudd_Ref( bSpace1 ); + bCanVars = Extra_bddSpaceCanonVars( dd, bSpace1 ); Cudd_Ref( bCanVars ); + bReduced = Extra_bddSpaceReduce( dd, pbOutputs[Output], bCanVars ); Cudd_Ref( bReduced ); + zEquations = Extra_bddSpaceEquations( dd, bSpace1 ); Cudd_Ref( zEquations ); + + nSupp = Cudd_SupportSize( dd, bSpace1 ); + nMints = Cudd_CountMinterm( dd, bSpace1, nSupp ); + nAutos = Extra_Base2LogDouble(nMints); + printf( "Output #%3d: Inputs = %2d. AutoK = %2d.\n", Output, nSupp, nAutos ); + + Cudd_RecursiveDeref( dd, bSpace1 ); + Cudd_RecursiveDeref( dd, bCanVars ); + Cudd_RecursiveDeref( dd, bReduced ); + Cudd_RecursiveDerefZdd( dd, zEquations ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index fed89dbb..effae853 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -24,10 +24,11 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate ); -static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate ); -static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate ); -static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate ); +static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective ); +static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective ); +static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective ); +static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective ); +static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -44,14 +45,26 @@ static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSupe SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ) +Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ) { Abc_Ntk_t * pNtkAig; assert( Abc_NtkIsStrash(pNtk) ); + // compute the required times + if ( fSelective ) + { + Abc_NtkStartReverseLevels( pNtk ); + Abc_NtkMarkCriticalNodes( pNtk ); + } // perform balancing pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); - Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate ); + Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective ); Abc_NtkFinalize( pNtk, pNtkAig ); + // undo the required times + if ( fSelective ) + { + Abc_NtkStopReverseLevels( pNtk ); + Abc_NtkCleanMarkA( pNtk ); + } if ( pNtk->pExdc ) pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); // make sure everything is okay @@ -75,7 +88,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ) SeeAlso [] ***********************************************************************/ -void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate ) +void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective ) { int fCheck = 1; ProgressBar * pProgress; @@ -94,7 +107,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica Extra_ProgressBarUpdate( pProgress, i, NULL ); // strash the driver node pDriver = Abc_ObjFanin0(pNode); - Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate ); + Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective ); } Extra_ProgressBarStop( pProgress ); Vec_VecFree( vStorage ); @@ -147,7 +160,7 @@ void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate ) +Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective ) { Abc_Aig_t * pMan = pNtkNew->pManFunc; Abc_Obj_t * pNodeNew, * pNode1, * pNode2; @@ -159,7 +172,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ return pNodeOld->pCopy; assert( Abc_ObjIsNode(pNodeOld) ); // get the implication supergate - vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate ); + vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective ); if ( vSuper->nSize == 0 ) { // it means that the supergate contains two nodes in the opposite polarity pNodeOld->pCopy = Abc_ObjNot(Abc_NtkConst1(pNtkNew)); @@ -168,7 +181,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ // for each old node, derive the new well-balanced node for ( i = 0; i < vSuper->nSize; i++ ) { - pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate ); + pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective ); vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) ); } if ( vSuper->nSize < 2 ) @@ -207,7 +220,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate ) +Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate, bool fSelective ) { Vec_Ptr_t * vNodes; int RetValue, i; @@ -219,7 +232,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le vNodes = Vec_VecEntry( vStorage, Level ); Vec_PtrClear( vNodes ); // collect the nodes in the implication supergate - RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate ); + RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate, fSelective ); assert( vNodes->nSize > 1 ); // unmark the visited nodes for ( i = 0; i < vNodes->nSize; i++ ) @@ -245,7 +258,7 @@ Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Le SeeAlso [] ***********************************************************************/ -int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate ) +int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective ) { int RetValue1, RetValue2, i; // check if the node is visited @@ -263,7 +276,7 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, return 0; } // if the new node is complemented or a PI, another gate begins - if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && (Abc_ObjFanoutNum(pNode) > 1)) ) + if ( !fFirst && (Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || !fDuplicate && !fSelective && (Abc_ObjFanoutNum(pNode) > 1)) ) { Vec_PtrPush( vSuper, pNode ); Abc_ObjRegular(pNode)->fMarkB = 1; @@ -272,8 +285,8 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, assert( !Abc_ObjIsComplement(pNode) ); assert( Abc_ObjIsNode(pNode) ); // go through the branches - RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate ); - RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate ); + RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate, fSelective ); + RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate, fSelective ); if ( RetValue1 == -1 || RetValue2 == -1 ) return -1; // return 1 if at least one branch has a duplicate @@ -315,7 +328,7 @@ Vec_Ptr_t * Abc_NodeFindCone_rec( Abc_Obj_t * pNode ) else { // collect the nodes in the implication supergate - RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1 ); + RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, 1, 0 ); assert( vNodes->nSize > 1 ); // unmark the visited nodes Vec_PtrForEachEntry( vNodes, pNode, i ) @@ -442,6 +455,28 @@ void Abc_NtkBalanceLevel( Abc_Ntk_t * pNtk ) } +/**Function************************************************************* + + Synopsis [Marks the nodes on the critical and near critical paths.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( Abc_NodeReadRequiredLevel(pNode) - pNode->Level <= 1 ) + pNode->fMarkA = 1, Counter++; + printf( "The number of nodes on the critical paths = %6d (%5.2f %%)\n", Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk) ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 5c7f0d48..a73ab2b5 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -172,6 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * int i, nNodesDsd; // save the CI nodes in the DSD nodes + Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkConst1(pNtk)->pCopy ); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 39bf15aa..128e054a 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -105,7 +105,7 @@ clk = clock(); Map_ManFree( pMan ); return NULL; } -// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); + Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); // reconstruct the network after mapping pNtkNew = Abc_NtkFromMap( pMan, pNtk ); diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index c1f83e1f..ea2f808c 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -173,6 +173,8 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld ) assert( !Abc_NodeIsConst(pNodeOld) ); assert( pNodeOld->fMarkA ); +//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) ); + // collect the renoding cone vCone = Vec_PtrAlloc( 10 ); Abc_NtkRenodeCone( pNodeOld, vCone ); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index f7b9892e..9c650aa9 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -29,6 +29,8 @@ static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ); +static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); + static nMuxes; //////////////////////////////////////////////////////////////////////// @@ -46,7 +48,7 @@ static nMuxes; SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) +int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) { solver * pSat; lbool status; @@ -317,7 +319,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) +int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) { solver * pSat; lbool status; @@ -376,7 +378,8 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) // if the problem is SAT, get the counterexample if ( status == l_True ) { - Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); +// Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); + Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk ); pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); Vec_IntFree( vCiIds ); } @@ -385,6 +388,28 @@ int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) return RetValue; } +/**Function************************************************************* + + Synopsis [Returns the array of CI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vCiIds; + Abc_Obj_t * pObj; + int i; + vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + Vec_IntPush( vCiIds, (int)pObj->pCopy ); + return vCiIds; +} + diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c new file mode 100644 index 00000000..08a42623 --- /dev/null +++ b/src/base/abci/abcUnate.c @@ -0,0 +1,150 @@ +/**CFile**************************************************************** + + FileName [abcUnate.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcUnate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose ); +static void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detects unate variables of the multi-output function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintUnate( Abc_Ntk_t * pNtk, int fUseBdds, int fUseNaive, int fVerbose ) +{ + if ( fUseBdds || fUseNaive ) + Abc_NtkPrintUnateBdd( pNtk, fUseNaive, fVerbose ); + else + Abc_NtkPrintUnateSat( pNtk, fVerbose ); +} + +/**Function************************************************************* + + Synopsis [Detects unate variables using BDDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose ) +{ + Abc_Obj_t * pNode; + Extra_UnateInfo_t * p; + DdManager * dd; // the BDD manager used to hold shared BDDs + DdNode ** pbGlobal; // temporary storage for global BDDs + int TotalSupps = 0; + int TotalUnate = 0; + int i, clk = clock(); + int clkBdd, clkUnate; + + // compute the global BDDs + if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL ) + return; +clkBdd = clock() - clk; + + // get information about the network + dd = pNtk->pManGlob; + pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob ); + + // print the size of the BDDs + printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + + // perform naive BDD-based computation + if ( fUseNaive ) + { + Abc_NtkForEachCo( pNtk, pNode, i ) + { + p = Extra_UnateComputeSlow( dd, pbGlobal[i] ); + if ( fVerbose ) + Extra_UnateInfoPrint( p ); + TotalSupps += p->nVars; + TotalUnate += p->nUnate; + Extra_UnateInfoDissolve( p ); + } + } + // perform smart BDD-based computation + else + { + // create ZDD variables in the manager + Cudd_zddVarsFromBddVars( dd, 2 ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + p = Extra_UnateComputeFast( dd, pbGlobal[i] ); + if ( fVerbose ) + Extra_UnateInfoPrint( p ); + TotalSupps += p->nVars; + TotalUnate += p->nUnate; + Extra_UnateInfoDissolve( p ); + } + } +clkUnate = clock() - clk - clkBdd; + + // print stats + printf( "Ins/Outs = %4d/%4d. Total supp = %5d. Total unate = %5d.\n", + Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), TotalSupps, TotalUnate ); + PRT( "Glob BDDs", clkBdd ); + PRT( "Unateness", clkUnate ); + PRT( "Total ", clock() - clk ); + + // deref the PO functions + Abc_NtkFreeGlobalBdds( pNtk ); + // stop the global BDD manager + Extra_StopManager( pNtk->pManGlob ); + pNtk->pManGlob = NULL; +} + +/**Function************************************************************* + + Synopsis [Detects unate variables using SAT.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintUnateSat( Abc_Ntk_t * pNtk, int fVerbose ) +{ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index b30a6452..99392e48 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -148,9 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; - Params.fFuncRed = 0; - Params.nPatsRand = 0; - Params.nPatsDyna = 0; +// Params.fFuncRed = 0; +// Params.nPatsRand = 0; +// Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); @@ -328,9 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; - Params.fFuncRed = 0; - Params.nPatsRand = 0; - Params.nPatsDyna = 0; +// Params.fFuncRed = 0; +// Params.nPatsRand = 0; +// Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 660aee63..5b15641b 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -1,5 +1,6 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcAttach.c \ + src/base/abci/abcAuto.c \ src/base/abci/abcBalance.c \ src/base/abci/abcCollapse.c \ src/base/abci/abcCut.c \ @@ -21,6 +22,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcSweep.c \ src/base/abci/abcSymm.c \ src/base/abci/abcTiming.c \ + src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ src/base/abci/abcVanEijk.c \ src/base/abci/abcVanImp.c \ diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index f20855ab..b2a90806 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1204,7 +1204,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) char * pSisName; int i; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -1340,7 +1340,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) char * pMvsisName; int i; - pNtk = Abc_FrameReadNet(pAbc); + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); diff --git a/src/base/io/io.h b/src/base/io/io.h index 286b570c..fe5c237f 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -69,6 +69,7 @@ extern Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 ); extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut ); +extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose ); /*=== abcWriteBaf.c ==========================================================*/ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); /*=== abcWriteBlif.c ==========================================================*/ diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index d8ad8f71..1cb0ae5d 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ) Abc_Ntk_t * pNtk; // start the file - p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r,()=" ); + p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t,()=" ); if ( p == NULL ) return NULL; diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index b8a2ed01..c05f444e 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -135,7 +135,8 @@ Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName ) Io_ReadBlif_t * p; // start the reader - pReader = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r" ); + pReader = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t" ); + if ( pReader == NULL ) return NULL; diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index a2a2f527..f100a45f 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck ) Abc_Ntk_t * pNtk; // start the file - p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r()" ); + p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t()" ); if ( p == NULL ) return NULL; diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c index 387f8730..0413dc8f 100644 --- a/src/base/io/ioReadPla.c +++ b/src/base/io/ioReadPla.c @@ -47,7 +47,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck ) Abc_Ntk_t * pNtk; // start the file - p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r|" ); + p = Extra_FileReaderAlloc( pFileName, "#", "\n\r", " \t|" ); if ( p == NULL ) return NULL; diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 342dfbaf..e817bee8 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -194,6 +194,61 @@ Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut return pNet; } + +/**Function************************************************************* + + Synopsis [Provide an fopen replacement with path lookup] + + Description [Provide an fopen replacement where the path stored + in pathvar MVSIS variable is used to look up the path + for name. Returns NULL if file cannot be opened.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose ) +{ + char * t = 0, * c = 0, * i; + extern char * Abc_FrameReadFlag( char * pFlag ); + + if ( PathVar == 0 ) + { + return fopen( FileName, Mode ); + } + else + { + if ( c = Abc_FrameReadFlag( (char*)PathVar ) ) + { + char ActualFileName[4096]; + FILE * fp = 0; + t = util_strsav( c ); + for (i = strtok( t, ":" ); i != 0; i = strtok( 0, ":") ) + { +#ifdef WIN32 + _snprintf ( ActualFileName, 4096, "%s/%s", i, FileName ); +#else + snprintf ( ActualFileName, 4096, "%s/%s", i, FileName ); +#endif + if ( ( fp = fopen ( ActualFileName, Mode ) ) ) + { + if ( fVerbose ) + fprintf ( stdout, "Using file %s\n", ActualFileName ); + free( t ); + return fp; + } + } + free( t ); + return 0; + } + else + { + return fopen( FileName, Mode ); + } + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/module.make b/src/base/io/module.make index 21579266..8693c8eb 100644 --- a/src/base/io/module.make +++ b/src/base/io/module.make @@ -16,4 +16,5 @@ SRC += src/base/io/io.c \ src/base/io/ioWriteEqn.c \ src/base/io/ioWriteGml.c \ src/base/io/ioWriteList.c \ - src/base/io/ioWritePla.c + src/base/io/ioWritePla.c \ + src/base/io/ioWriteVerilog.c diff --git a/src/base/main/main.c b/src/base/main/main.c index 4c572a07..a9f27bf8 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -217,7 +217,7 @@ int main( int argc, char * argv[] ) break; } } - + // if the memory should be freed, quit packages if ( fStatus < 0 ) { diff --git a/src/base/main/main.h b/src/base/main/main.h index 4280808d..c5f311aa 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -78,7 +78,7 @@ extern void Abc_Start(); extern void Abc_Stop(); /*=== mainFrame.c ===========================================================*/ -extern Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p ); +extern Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p ); extern FILE * Abc_FrameReadOut( Abc_Frame_t * p ); extern FILE * Abc_FrameReadErr( Abc_Frame_t * p ); extern bool Abc_FrameReadMode( Abc_Frame_t * p ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index f75df49e..e9e243af 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -164,7 +164,7 @@ void Abc_FrameRestart( Abc_Frame_t * p ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p ) +Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p ) { return p->pNtkCur; } diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c index b1f66721..ed2a33fc 100644 --- a/src/base/seq/seqAigCore.c +++ b/src/base/seq/seqAigCore.c @@ -351,11 +351,13 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); // transform the miter into a logic network for efficient CNF construction - pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); - Abc_NtkDelete( pNtkMiter ); +// pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); +// Abc_NtkDelete( pNtkMiter ); + pNtkCnf = pNtkMiter; // solve the miter clk = clock(); +// RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 ); RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 ); if ( fVerbose ) if ( clock() - clk > 100 ) diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h index 6e180fac..3fd365d7 100644 --- a/src/bdd/dsd/dsd.h +++ b/src/bdd/dsd/dsd.h @@ -91,6 +91,7 @@ extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); +extern Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ); /*=== dsdMan.c =======================================================*/ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ); extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c index c7675f8e..d1c90e23 100644 --- a/src/bdd/dsd/dsdApi.c +++ b/src/bdd/dsd/dsdApi.c @@ -89,6 +89,7 @@ void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } ***********************************************************************/ Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ) { return pMan->pRoots[i]; } Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } +Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ) { return pMan->pConst1; } DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } //////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 8eaa0969..5569c443 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -42,6 +42,7 @@ struct Dsd_Manager_t_ int nRootsAlloc;// the number of primary outputs Dsd_Node_t ** pInputs; // the primary input nodes Dsd_Node_t ** pRoots; // the primary output nodes + Dsd_Node_t * pConst1; // the constant node int fVerbose; // the verbosity level }; diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c index 4529e75a..6e43f0f4 100644 --- a/src/bdd/dsd/dsdMan.c +++ b/src/bdd/dsd/dsdMan.c @@ -73,6 +73,7 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ) pNode->G = b1; Cudd_Ref( pNode->G ); pNode->S = b1; Cudd_Ref( pNode->S ); st_insert( dMan->Table, (char*)b1, (char*)pNode ); + dMan->pConst1 = pNode; Dsd_CheckCacheAllocate( 5000 ); return dMan; diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c index d9629ecc..31894590 100644 --- a/src/map/fpga/fpga.c +++ b/src/map/fpga/fpga.c @@ -105,7 +105,7 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) int fVerbose; int c; - pNet = Abc_FrameReadNet(pAbc); + pNet = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -195,7 +195,7 @@ int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) int fVerbose; int c; - pNet = Abc_FrameReadNet(pAbc); + pNet = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); diff --git a/src/map/mapper/mapper.c b/src/map/mapper/mapper.c index f6cceda1..4d77df8f 100644 --- a/src/map/mapper/mapper.c +++ b/src/map/mapper/mapper.c @@ -87,7 +87,7 @@ int Map_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) int fAlgorithm; int c; - pNet = Abc_FrameReadNet(pAbc); + pNet = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -128,8 +128,8 @@ int Map_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) // get the input file name FileName = argv[util_optind]; -// if ( (pFile = Io_FileOpen( FileName, "open_path", "r" )) == NULL ) - if ( (pFile = fopen( FileName, "r" )) == NULL ) + if ( (pFile = Io_FileOpen( FileName, "open_path", "r", 0 )) == NULL ) +// if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); if ( FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL ) ) diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c index bc7346b5..ec1c095e 100644 --- a/src/map/mapper/mapperCreate.c +++ b/src/map/mapper/mapperCreate.c @@ -314,7 +314,7 @@ void Map_ManPrintTimeStats( Map_Man_t * p ) void Map_ManPrintStatsToFile( char * pName, float Area, float Delay, int Time ) { FILE * pTable; - pTable = fopen( "stats.txt", "a+" ); + pTable = fopen( "map_stats.txt", "a+" ); fprintf( pTable, "%s ", pName ); fprintf( pTable, "%4.2f ", Area ); fprintf( pTable, "%4.2f ", Delay ); diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c index 9656b0f5..ef66082d 100644 --- a/src/map/mapper/mapperTree.c +++ b/src/map/mapper/mapperTree.c @@ -60,8 +60,8 @@ int Map_LibraryReadTree( Map_SuperLib_t * pLib, char * pFileName, char * pExclud // read the beginning of the file assert( pLib->pGenlib == NULL ); -// pFile = Io_FileOpen( pFileName, "open_path", "r" ); - pFile = fopen( pFileName, "r" ); + pFile = Io_FileOpen( pFileName, "open_path", "r", 1 ); +// pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) { printf( "Cannot open input file \"%s\".\n", pFileName ); @@ -149,8 +149,8 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam } #endif -// pFileGen = Io_FileOpen( pLibFile, "open_path", "r" ); - pFileGen = fopen( pLibFile, "r" ); + pFileGen = Io_FileOpen( pLibFile, "open_path", "r", 1 ); +// pFileGen = fopen( pLibFile, "r" ); if ( pFileGen == NULL ) { printf( "Cannot open the GENLIB file \"%s\".\n", pLibFile ); diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c index ba05f7ec..a5dd8f95 100644 --- a/src/map/mio/mio.c +++ b/src/map/mio/mio.c @@ -133,7 +133,7 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) int fVerbose; int c; - pNet = Abc_FrameReadNet(pAbc); + pNet = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); @@ -163,7 +163,7 @@ int Mio_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) // get the input file name FileName = argv[util_optind]; - if ( (pFile = fopen( FileName, "r" )) == NULL ) + if ( (pFile = Io_FileOpen( FileName, "open_path", "r", 0 )) == NULL ) { fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); if ( (FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL )) ) @@ -223,7 +223,7 @@ int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv ) int fVerbose; int c; - pNet = Abc_FrameReadNet(pAbc); + pNet = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c index 93b214b5..0c2000a3 100644 --- a/src/map/mio/mioRead.c +++ b/src/map/mio/mioRead.c @@ -114,8 +114,8 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, bool fE int nFileSize; // open the BLIF file for binary reading -// pFile = Io_FileOpen( FileName, "open_path", "rb" ); - pFile = fopen( FileName, "rb" ); + pFile = Io_FileOpen( FileName, "open_path", "rb", 1 ); +// pFile = fopen( FileName, "rb" ); // if we got this far, file should be okay otherwise would // have been detected by caller assert ( pFile != NULL ); diff --git a/src/map/super/super.c b/src/map/super/super.c index a3fbc98c..4b4968dd 100644 --- a/src/map/super/super.c +++ b/src/map/super/super.c @@ -245,8 +245,8 @@ int Super_CommandSupergates( Abc_Frame_t * pAbc, int argc, char **argv ) // get the input file name FileName = argv[util_optind]; -// if ( (pFile = Io_FileOpen( FileName, "open_path", "r" )) == NULL ) - if ( (pFile = fopen( FileName, "r" )) == NULL ) + if ( (pFile = Io_FileOpen( FileName, "open_path", "r", 0 )) == NULL ) +// if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pErr, "Cannot open input file \"%s\". ", FileName ); if (( FileName = Extra_FileGetSimilarName( FileName, ".genlib", ".lib", ".gen", ".g", NULL ) )) diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index bb776ab7..0d0c93a8 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -106,7 +106,35 @@ typedef unsigned long long uint64; /* Various Utilities */ /*===========================================================================*/ +/*=== extraBddAuto.c ========================================================*/ + +extern DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ); +extern DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ); +extern DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); +extern DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ); + +extern DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ); +extern DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); +extern DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ); + +extern DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ); +extern DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); +extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ); + +extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ); +extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ); + /*=== 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 ); @@ -126,6 +154,7 @@ 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 ); +extern DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ); /*=== extraBddKmap.c ================================================================*/ @@ -185,6 +214,46 @@ extern DdNode * extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNo extern DdNode * Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS ); extern DdNode * extraZddSelectOneSubset( DdManager * dd, DdNode * zS ); +/*=== extraBddUnate.c =================================================================*/ + +typedef struct Extra_UnateVar_t_ Extra_UnateVar_t; +struct Extra_UnateVar_t_ { + unsigned iVar : 30; // index of the variable + unsigned Pos : 1; // 1 if positive unate + unsigned Neg : 1; // 1 if negative unate +}; + +typedef struct Extra_UnateInfo_t_ Extra_UnateInfo_t; +struct Extra_UnateInfo_t_ { + int nVars; // the number of variables in the support + int nVarsMax; // the number of variables in the DD manager + int nUnate; // the number of unate variables + Extra_UnateVar_t * pVars; // the array of variables present in the support +}; + +/* allocates the data structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ); +/* deallocates the data structure */ +extern void Extra_UnateInfoDissolve( Extra_UnateInfo_t * ); +/* print the contents the data structure */ +extern void Extra_UnateInfoPrint( Extra_UnateInfo_t * ); +/* converts the ZDD into the Extra_SymmInfo_t structure */ +extern Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zUnate, DdNode * bVars ); +/* naive check of unateness of one variable */ +extern int Extra_bddCheckUnateNaive( DdManager * dd, DdNode * bF, int iVar ); + +/* computes the unateness information for the function */ +extern Extra_UnateInfo_t * Extra_UnateComputeFast( DdManager * dd, DdNode * bFunc ); +extern Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ); + +/* computes the classical symmetry information as a ZDD */ +extern DdNode * Extra_zddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); +extern DdNode * extraZddUnateInfoCompute( DdManager * dd, DdNode * bF, DdNode * bVars ); + +/* converts a set of variables into a set of singleton subsets */ +extern DdNode * Extra_zddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); +extern DdNode * extraZddGetSingletonsBoth( DdManager * dd, DdNode * bVars ); + /*=== extraUtilBitMatrix.c ================================================================*/ typedef struct Extra_BitMat_t_ Extra_BitMat_t; diff --git a/src/misc/extra/extraBddAuto.c b/src/misc/extra/extraBddAuto.c new file mode 100644 index 00000000..21a969ba --- /dev/null +++ b/src/misc/extra/extraBddAuto.c @@ -0,0 +1,1558 @@ +/**CFile**************************************************************** + + FileName [extraBddAuto.c] + + PackageName [extra] + + Synopsis [Computation of autosymmetries.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $] + +***********************************************************************/ + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + + +/* + LinearSpace(f) = Space(f,f) + + Space(f,g) + { + if ( f = const ) + { + if ( f = g ) return 1; + else return 0; + } + if ( g = const ) return 0; + return x' * Space(fx',gx') * Space(fx,gx) + x * Space(fx',gx) * Space(fx,gx'); + } + + Equations(s) = Pos(s) + Neg(s); + + Pos(s) + { + if ( s = 0 ) return 1; + if ( s = 1 ) return 0; + if ( sx'= 0 ) return Pos(sx) + x; + if ( sx = 0 ) return Pos(sx'); + return 1 * [Pos(sx') & Pos(sx)] + x * [Pos(sx') & Neg(sx)]; + } + + Neg(s) + { + if ( s = 0 ) return 1; + if ( s = 1 ) return 0; + if ( sx'= 0 ) return Neg(sx); + if ( sx = 0 ) return Neg(sx') + x; + return 1 * [Neg(sx') & Neg(sx)] + x * [Neg(sx') & Pos(sx)]; + } + + + SpaceP(A) + { + if ( A = 0 ) return 1; + if ( A = 1 ) return 1; + return x' * SpaceP(Ax') * SpaceP(Ax) + x * SpaceP(Ax') * SpaceN(Ax); + } + + SpaceN(A) + { + if ( A = 0 ) return 1; + if ( A = 1 ) return 0; + return x' * SpaceN(Ax') * SpaceN(Ax) + x * SpaceN(Ax') * SpaceP(Ax); + } + + + LinInd(A) + { + if ( A = const ) return 1; + if ( !LinInd(Ax') ) return 0; + if ( !LinInd(Ax) ) return 0; + if ( LinSumOdd(Ax') & LinSumEven(Ax) != 0 ) return 0; + if ( LinSumEven(Ax') & LinSumEven(Ax) != 0 ) return 0; + return 1; + } + + LinSumOdd(A) + { + if ( A = 0 ) return 0; // Odd0 ---e-- Odd1 + if ( A = 1 ) return 1; // \ o + Odd0 = LinSumOdd(Ax'); // x is absent // \ + Even0 = LinSumEven(Ax'); // x is absent // / o + Odd1 = LinSumOdd(Ax); // x is present // Even0 ---e-- Even1 + Even1 = LinSumEven(Ax); // x is absent + return 1 * [Odd0 + ExorP(Odd0, Even1)] + x * [Odd1 + ExorP(Odd1, Even0)]; + } + + LinSumEven(A) + { + if ( A = 0 ) return 0; + if ( A = 1 ) return 0; + Odd0 = LinSumOdd(Ax'); // x is absent + Even0 = LinSumEven(Ax'); // x is absent + Odd1 = LinSumOdd(Ax); // x is present + Even1 = LinSumEven(Ax); // x is absent + return 1 * [Even0 + Even1 + ExorP(Even0, Even1)] + x * [ExorP(Odd0, Odd1)]; + } + +*/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionFast( DdManager * dd, DdNode * bFunc ) +{ + int * pSupport; + int * pPermute; + int * pPermuteBack; + DdNode ** pCompose; + DdNode * bCube, * bTemp; + DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift; + int nSupp, Counter; + int i, lev; + + // get the support + pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); + Extra_SupportArray( dd, bFunc, pSupport ); + nSupp = 0; + for ( i = 0; i < dd->size; i++ ) + if ( pSupport[i] ) + nSupp++; + + // make sure the manager has enough variables + if ( 2*nSupp > dd->size ) + { + printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" ); + fflush( stdout ); + free( pSupport ); + return NULL; + } + + // create the permutation arrays + pPermute = ALLOC( int, dd->size ); + pPermuteBack = ALLOC( int, dd->size ); + pCompose = ALLOC( DdNode *, dd->size ); + for ( i = 0; i < dd->size; i++ ) + { + pPermute[i] = i; + pPermuteBack[i] = i; + pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] ); + } + + // remap the function in such a way that the variables are interleaved + Counter = 0; + bCube = b1; Cudd_Ref( bCube ); + for ( lev = 0; lev < dd->size; lev++ ) + if ( pSupport[ dd->invperm[lev] ] ) + { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter; + pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter]; + // var from level 2*Counter+1 should go back to the place of this var + pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev]; + // the permutation should be defined in such a way that variable + // on level 2*Counter is replaced by an EXOR of itself and var on the next level + Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] ); + pCompose[ dd->invperm[2*Counter] ] = + Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] ); + Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] ); + // add this variable to the cube + bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + // increment the counter + Counter ++; + } + + // permute the functions + bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 ); + // compose to gate the function depending on both vars + bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 ); + // gate the vector space + // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] ) + bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift ); + bSpaceShift = Cudd_Not( bSpaceShift ); + // permute the space back into the original mapping + bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace ); + Cudd_RecursiveDeref( dd, bFunc1 ); + Cudd_RecursiveDeref( dd, bFunc2 ); + Cudd_RecursiveDeref( dd, bSpaceShift ); + Cudd_RecursiveDeref( dd, bCube ); + + for ( i = 0; i < dd->size; i++ ) + Cudd_RecursiveDeref( dd, pCompose[i] ); + free( pPermute ); + free( pPermuteBack ); + free( pCompose ); + free( pSupport ); + + Cudd_Deref( bSpace ); + return bSpace; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunction( dd, bF, bG ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionPos( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunctionPos( dd, bFunc ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromFunctionNeg( DdManager * dd, DdNode * bFunc ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromFunctionNeg( dd, bFunc ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceCanonVars( DdManager * dd, DdNode * bSpace ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceCanonVars( dd, bSpace ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars ) +{ + DdNode * bNegCube; + DdNode * bResult; + bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube ); + bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bNegCube ); + Cudd_Deref( bResult ); + return bResult; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquations( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + DdNode * zEquPos; + DdNode * zEquNeg; + zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos ); + zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg ); + zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes ); + Cudd_RecursiveDerefZdd( dd, zEquPos ); + Cudd_RecursiveDerefZdd( dd, zEquNeg ); + Cudd_Deref( zRes ); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquationsPos( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + do { + dd->reordered = 0; + zRes = extraBddSpaceEquationsPos( dd, bSpace ); + } while (dd->reordered == 1); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceEquationsNeg( DdManager * dd, DdNode * bSpace ) +{ + DdNode * zRes; + do { + dd->reordered = 0; + zRes = extraBddSpaceEquationsNeg( dd, bSpace ); + } while (dd->reordered == 1); + return zRes; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromMatrixPos( dd, zA ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Extra_bddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + do { + dd->reordered = 0; + bRes = extraBddSpaceFromMatrixNeg( dd, zA ); + } while (dd->reordered == 1); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Counts the number of literals in one combination.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_zddLitCountComb( DdManager * dd, DdNode * zComb ) +{ + int Counter; + if ( zComb == z0 ) + return 0; + Counter = 0; + for ( ; zComb != z1; zComb = cuddT(zComb) ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [Returns the array of ZDDs with the number equal to the number of + vars in the DD manager. If the given var is non-canonical, this array contains + the referenced ZDD representing literals in the corresponding EXOR equation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations ) +{ + DdNode ** pzRes; + int * pVarsNonCan; + DdNode * zEquRem; + int iVarNonCan; + DdNode * zExor, * zTemp; + + // get the set of non-canonical variables + pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); + Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); + + // allocate storage for the EXOR sets + pzRes = ALLOC( DdNode *, dd->size ); + memset( pzRes, 0, sizeof(DdNode *) * dd->size ); + + // go through all the equations + zEquRem = zEquations; Cudd_Ref( zEquRem ); + while ( zEquRem != z0 ) + { + // extract one product + zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor ); + // remove it from the set + zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + + // locate the non-canonical variable + iVarNonCan = -1; + for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) ) + { + if ( pVarsNonCan[zTemp->index/2] == 1 ) + { + assert( iVarNonCan == -1 ); + iVarNonCan = zTemp->index/2; + } + } + assert( iVarNonCan != -1 ); + + if ( Extra_zddLitCountComb( dd, zExor ) > 1 ) + pzRes[ iVarNonCan ] = zExor; // takes ref + else + Cudd_RecursiveDerefZdd( dd, zExor ); + } + Cudd_RecursiveDerefZdd( dd, zEquRem ); + + free( pVarsNonCan ); + return pzRes; +} + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraBddSpaceFromFunction( DdManager * dd, DdNode * bF, DdNode * bG ) +{ + DdNode * bRes; + DdNode * bFR, * bGR; + + bFR = Cudd_Regular( bF ); + bGR = Cudd_Regular( bG ); + if ( cuddIsConstant(bFR) ) + { + if ( bF == bG ) + return b1; + else + return b0; + } + if ( cuddIsConstant(bGR) ) + return b0; + // both bFunc and bCore are not constants + + // the operation is commutative - normalize the problem + if ( (unsigned)bF > (unsigned)bG ) + return extraBddSpaceFromFunction(dd, bG, bF); + + + if ( bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bG0, * bG1; + DdNode * bTemp1, * bTemp2; + DdNode * bRes0, * bRes1; + int LevelF, LevelG; + int index; + + LevelF = dd->perm[bFR->index]; + LevelG = dd->perm[bGR->index]; + if ( LevelF <= LevelG ) + { + index = dd->invperm[LevelF]; + if ( bFR != bF ) + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + } + else + { + index = dd->invperm[LevelG]; + bF0 = bF1 = bF; + } + + if ( LevelG <= LevelF ) + { + if ( bGR != bG ) + { + bG0 = Cudd_Not( cuddE(bGR) ); + bG1 = Cudd_Not( cuddT(bGR) ); + } + else + { + bG0 = cuddE(bGR); + bG1 = cuddT(bGR); + } + } + else + bG0 = bG1 = bG; + + bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 ); + if ( bTemp1 == NULL ) + return NULL; + cuddRef( bTemp1 ); + + bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 ); + if ( bTemp2 == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp1 ); + return NULL; + } + cuddRef( bTemp2 ); + + + bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + + + bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 ); + if ( bTemp1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bTemp1 ); + + bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 ); + if ( bTemp2 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + return NULL; + } + cuddRef( bTemp2 ); + + bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bTemp1 ); + Cudd_RecursiveDeref( dd, bTemp2 ); + + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0)); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + // insert the result into cache + cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes); + return bRes; + } +} /* end of extraBddSpaceFromFunction */ + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromFunctionPos( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return b1; + + if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bPos0, * bPos1; + DdNode * bNeg0, * bNeg1; + DdNode * bRes0, * bRes1; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + + bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 ); + if ( bPos0 == NULL ) + return NULL; + cuddRef( bPos0 ); + + bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 ); + if ( bPos1 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + return NULL; + } + cuddRef( bPos1 ); + + bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + + + bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); + if ( bNeg0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bNeg0 ); + + bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); + if ( bNeg1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + return NULL; + } + cuddRef( bNeg1 ); + + bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes ); + return bRes; + } +} + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromFunctionNeg( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return b0; + + if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bPos0, * bPos1; + DdNode * bNeg0, * bNeg1; + DdNode * bRes0, * bRes1; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + + bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); + if ( bPos0 == NULL ) + return NULL; + cuddRef( bPos0 ); + + bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); + if ( bPos1 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + return NULL; + } + cuddRef( bPos1 ); + + bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bPos0 ); + Cudd_RecursiveDeref( dd, bPos1 ); + + + bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 ); + if ( bNeg0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bNeg0 ); + + bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 ); + if ( bNeg1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + return NULL; + } + cuddRef( bNeg1 ); + + bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bNeg0 ); + Cudd_RecursiveDeref( dd, bNeg1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes ); + return bRes; + } +} + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF ) +{ + DdNode * bRes, * bFR; + statLine( dd ); + + bFR = Cudd_Regular(bF); + if ( cuddIsConstant(bFR) ) + return bF; + + if ( bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF) ) + return bRes; + else + { + DdNode * bF0, * bF1; + DdNode * bRes, * bRes0; + + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + bRes = extraBddSpaceCanonVars( dd, bF1 ); + if ( bRes == NULL ) + return NULL; + } + else if ( bF1 == b0 ) + { + bRes = extraBddSpaceCanonVars( dd, bF0 ); + if ( bRes == NULL ) + return NULL; + } + else + { + bRes0 = extraBddSpaceCanonVars( dd, bF0 ); + if ( bRes0 == NULL ) + return NULL; + cuddRef( bRes0 ); + + bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref( dd,bRes0 ); + return NULL; + } + cuddDeref( bRes0 ); + } + + cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes ); + return bRes; + } +} + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceEquationsPos( DdManager * dd, DdNode * bF ) +{ + DdNode * zRes; + statLine( dd ); + + if ( bF == b0 ) + return z1; + if ( bF == b1 ) + return z0; + + if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF) ) + return zRes; + else + { + DdNode * bFR, * bF0, * bF1; + DdNode * zPos0, * zPos1, * zNeg1; + DdNode * zRes, * zRes0, * zRes1; + + bFR = Cudd_Regular(bF); + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + zRes1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zRes1 == NULL ) + return NULL; + cuddRef( zRes1 ); + + // add the current element to the set + zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes1 ); + } + else if ( bF1 == b0 ) + { + zRes = extraBddSpaceEquationsPos( dd, bF0 ); + if ( zRes == NULL ) + return NULL; + } + else + { + zPos0 = extraBddSpaceEquationsPos( dd, bF0 ); + if ( zPos0 == NULL ) + return NULL; + cuddRef( zPos0 ); + + zPos1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zPos1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + return NULL; + } + cuddRef( zPos1 ); + + zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zNeg1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zNeg1 ); + + + zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes0 ); + + zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + // only zRes0 and zRes1 are refed at this point + + zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + + cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes ); + return zRes; + } +} + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceEquationsNeg( DdManager * dd, DdNode * bF ) +{ + DdNode * zRes; + statLine( dd ); + + if ( bF == b0 ) + return z1; + if ( bF == b1 ) + return z0; + + if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF) ) + return zRes; + else + { + DdNode * bFR, * bF0, * bF1; + DdNode * zPos0, * zPos1, * zNeg1; + DdNode * zRes, * zRes0, * zRes1; + + bFR = Cudd_Regular(bF); + if ( bFR != bF ) // bF is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + if ( bF0 == b0 ) + { + zRes = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zRes == NULL ) + return NULL; + } + else if ( bF1 == b0 ) + { + zRes0 = extraBddSpaceEquationsNeg( dd, bF0 ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // add the current element to the set + zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + return NULL; + } + cuddDeref( zRes0 ); + } + else + { + zPos0 = extraBddSpaceEquationsNeg( dd, bF0 ); + if ( zPos0 == NULL ) + return NULL; + cuddRef( zPos0 ); + + zPos1 = extraBddSpaceEquationsNeg( dd, bF1 ); + if ( zPos1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + return NULL; + } + cuddRef( zPos1 ); + + zNeg1 = extraBddSpaceEquationsPos( dd, bF1 ); + if ( zNeg1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zNeg1 ); + + + zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); + if ( zRes0 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes0 ); + + zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + return NULL; + } + cuddRef( zRes1 ); + Cudd_RecursiveDerefZdd(dd, zNeg1); + Cudd_RecursiveDerefZdd(dd, zPos0); + Cudd_RecursiveDerefZdd(dd, zPos1); + // only zRes0 and zRes1 are refed at this point + + zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zRes0); + Cudd_RecursiveDerefZdd(dd, zRes1); + return NULL; + } + cuddDeref( zRes0 ); + cuddDeref( zRes1 ); + } + + cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes ); + return zRes; + } +} + + + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromMatrixPos( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + statLine( dd ); + + if ( zA == z0 ) + return b1; + if ( zA == z1 ) + return b1; + + if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA) ) + return bRes; + else + { + DdNode * bP0, * bP1; + DdNode * bN0, * bN1; + DdNode * bRes0, * bRes1; + + bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); + if ( bP0 == NULL ) + return NULL; + cuddRef( bP0 ); + + bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); + if ( bP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + return NULL; + } + cuddRef( bP1 ); + + bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + + + bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); + if ( bN0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bN0 ); + + bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); + if ( bN1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + return NULL; + } + cuddRef( bN1 ); + + bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes ); + return bRes; + } +} + + +/**Function************************************************************* + + Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA ) +{ + DdNode * bRes; + statLine( dd ); + + if ( zA == z0 ) + return b1; + if ( zA == z1 ) + return b0; + + if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA) ) + return bRes; + else + { + DdNode * bP0, * bP1; + DdNode * bN0, * bN1; + DdNode * bRes0, * bRes1; + + bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); + if ( bP0 == NULL ) + return NULL; + cuddRef( bP0 ); + + bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); + if ( bP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + return NULL; + } + cuddRef( bP1 ); + + bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); + if ( bRes0 == NULL ) + { + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + return NULL; + } + cuddRef( bRes0 ); + Cudd_RecursiveDeref( dd, bP0 ); + Cudd_RecursiveDeref( dd, bP1 ); + + + bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); + if ( bN0 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + return NULL; + } + cuddRef( bN0 ); + + bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); + if ( bN1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + return NULL; + } + cuddRef( bN1 ); + + bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); + if ( bRes1 == NULL ) + { + Cudd_RecursiveDeref( dd, bRes0 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + return NULL; + } + cuddRef( bRes1 ); + Cudd_RecursiveDeref( dd, bN0 ); + Cudd_RecursiveDeref( dd, bN1 ); + + + // consider the case when Res0 and Res1 are the same node + if ( bRes0 == bRes1 ) + bRes = bRes1; + // consider the case when Res1 is complemented + else if ( Cudd_IsComplement(bRes1) ) + { + bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + bRes = Cudd_Not(bRes); + } + else + { + bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); + if ( bRes == NULL ) + { + Cudd_RecursiveDeref(dd,bRes0); + Cudd_RecursiveDeref(dd,bRes1); + return NULL; + } + } + cuddDeref( bRes0 ); + cuddDeref( bRes1 ); + + cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes ); + return bRes; + } +} + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 932ed525..7d806ec7 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -719,6 +719,83 @@ DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** return bResult; } /* end of Extra_bddBitsToCube */ +/**Function******************************************************************** + + Synopsis [Finds the support as a negative polarity cube.] + + Description [Finds the variables on which a DD depends. Returns a BDD + consisting of the product of the variables in the negative polarity + if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_VectorSupport Cudd_Support] + +******************************************************************************/ +DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ) +{ + int *support; + DdNode *res, *tmp, *var; + int i, j; + int size; + + /* Allocate and initialize support array for ddSupportStep. */ + size = ddMax( dd->size, dd->sizeZ ); + support = ALLOC( int, size ); + if ( support == NULL ) + { + dd->errorCode = CUDD_MEMORY_OUT; + return ( NULL ); + } + for ( i = 0; i < size; i++ ) + { + support[i] = 0; + } + + /* Compute support and clean up markers. */ + ddSupportStep( Cudd_Regular( f ), support ); + ddClearFlag( Cudd_Regular( f ) ); + + /* Transform support from array to cube. */ + do + { + dd->reordered = 0; + res = DD_ONE( dd ); + cuddRef( res ); + for ( j = size - 1; j >= 0; j-- ) + { /* for each level bottom-up */ + i = ( j >= dd->size ) ? j : dd->invperm[j]; + if ( support[i] == 1 ) + { + var = cuddUniqueInter( dd, i, dd->one, Cudd_Not( dd->one ) ); + ////////////////////////////////////////////////////////////////// + var = Cudd_Not(var); + ////////////////////////////////////////////////////////////////// + cuddRef( var ); + tmp = cuddBddAndRecur( dd, res, var ); + if ( tmp == NULL ) + { + Cudd_RecursiveDeref( dd, res ); + Cudd_RecursiveDeref( dd, var ); + res = NULL; + break; + } + cuddRef( tmp ); + Cudd_RecursiveDeref( dd, res ); + Cudd_RecursiveDeref( dd, var ); + res = tmp; + } + } + } + while ( dd->reordered == 1 ); + + FREE( support ); + if ( res != NULL ) + cuddDeref( res ); + return ( res ); + +} /* end of Extra_SupportNeg */ + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ diff --git a/src/misc/extra/extraBddUnate.c b/src/misc/extra/extraBddUnate.c new file mode 100644 index 00000000..b0297c77 --- /dev/null +++ b/src/misc/extra/extraBddUnate.c @@ -0,0 +1,641 @@ +/**CFile**************************************************************** + + FileName [extraBddUnate.c] + + PackageName [extra] + + Synopsis [Efficient methods to compute the information about + unate variables using an algorithm that is conceptually similar to + the algorithm for two-variable symmetry computation presented in: + A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. + Transactions on CAD, Nov. 2003.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 2.0. Started - September 1, 2003.] + + Revision [$Id: extraBddUnate.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information for the function.] + + Description [Returns the symmetry information in the form of Extra_UnateInfo_t structure.] + + SideEffects [If the ZDD variables are not derived from BDD variables with + multiplicity 2, this function may derive them in a wrong way.] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateComputeFast( + DdManager * dd, /* the manager */ + DdNode * bFunc) /* the function whose symmetries are computed */ +{ + DdNode * bSupp; + DdNode * zRes; + Extra_UnateInfo_t * p; + + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + zRes = Extra_zddUnateInfoCompute( dd, bFunc, bSupp ); Cudd_Ref( zRes ); + + p = Extra_UnateInfoCreateFromZdd( dd, zRes, bSupp ); + + Cudd_RecursiveDeref( dd, bSupp ); + Cudd_RecursiveDerefZdd( dd, zRes ); + + return p; + +} /* end of Extra_UnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Computes the classical symmetry information as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddUnateInfoCompute( + DdManager * dd, /* the DD manager */ + DdNode * bF, + DdNode * bVars) +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddUnateInfoCompute( dd, bF, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddUnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Converts a set of variables into a set of singleton subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddGetSingletonsBoth( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * res; + do { + dd->reordered = 0; + res = extraZddGetSingletonsBoth( dd, bVars ); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddGetSingletonsBoth */ + +/**Function******************************************************************** + + Synopsis [Allocates unateness information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateInfoAllocate( int nVars ) +{ + Extra_UnateInfo_t * p; + // allocate and clean the storage for unateness info + p = ALLOC( Extra_UnateInfo_t, 1 ); + memset( p, 0, sizeof(Extra_UnateInfo_t) ); + p->nVars = nVars; + p->pVars = ALLOC( Extra_UnateVar_t, nVars ); + memset( p->pVars, 0, nVars * sizeof(Extra_UnateVar_t) ); + return p; +} /* end of Extra_UnateInfoAllocate */ + +/**Function******************************************************************** + + Synopsis [Deallocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_UnateInfoDissolve( Extra_UnateInfo_t * p ) +{ + free( p->pVars ); + free( p ); +} /* end of Extra_UnateInfoDissolve */ + +/**Function******************************************************************** + + Synopsis [Allocates symmetry information structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Extra_UnateInfoPrint( Extra_UnateInfo_t * p ) +{ + char * pBuffer; + int i; + pBuffer = ALLOC( char, p->nVarsMax+1 ); + memset( pBuffer, ' ', p->nVarsMax ); + pBuffer[p->nVarsMax] = 0; + for ( i = 0; i < p->nVars; i++ ) + if ( p->pVars[i].Neg ) + pBuffer[ p->pVars[i].iVar ] = 'n'; + else if ( p->pVars[i].Pos ) + pBuffer[ p->pVars[i].iVar ] = 'p'; + else + pBuffer[ p->pVars[i].iVar ] = '.'; + printf( "%s\n", pBuffer ); + free( pBuffer ); +} /* end of Extra_UnateInfoPrint */ + + +/**Function******************************************************************** + + Synopsis [Creates the symmetry information structure from ZDD.] + + Description [ZDD representation of symmetries is the set of cubes, each + of which has two variables in the positive polarity. These variables correspond + to the symmetric variable pair.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateInfoCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp ) +{ + Extra_UnateInfo_t * p; + DdNode * bTemp, * zSet, * zCube, * zTemp; + int * pMapVars2Nums; + int i, nSuppSize; + + nSuppSize = Extra_bddSuppSize( dd, bSupp ); + + // allocate and clean the storage for symmetry info + p = Extra_UnateInfoAllocate( nSuppSize ); + + // allocate the storage for the temporary map + pMapVars2Nums = ALLOC( int, dd->size ); + memset( pMapVars2Nums, 0, dd->size * sizeof(int) ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + p->pVars[i].iVar = bTemp->index; + pMapVars2Nums[bTemp->index] = i; + } + + // write the symmetry info into the structure + zSet = zPairs; Cudd_Ref( zSet ); +// Cudd_zddPrintCover( dd, zPairs ); printf( "\n" ); + while ( zSet != z0 ) + { + // get the next cube + zCube = Extra_zddSelectOneSubset( dd, zSet ); Cudd_Ref( zCube ); + + // add this var to the data structure + assert( cuddT(zCube) == z1 && cuddE(zCube) == z0 ); + if ( zCube->index & 1 ) // neg + p->pVars[ pMapVars2Nums[zCube->index/2] ].Neg = 1; + else + p->pVars[ pMapVars2Nums[zCube->index/2] ].Pos = 1; + // count the unate vars + p->nUnate++; + + // update the cuver and deref the cube + zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube ); Cudd_Ref( zSet ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zCube ); + + } // for each cube + Cudd_RecursiveDerefZdd( dd, zSet ); + FREE( pMapVars2Nums ); + return p; + +} /* end of Extra_UnateInfoCreateFromZdd */ + + + +/**Function******************************************************************** + + Synopsis [Computes the classical unateness information for the function.] + + Description [Uses the naive way of comparing cofactors.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +Extra_UnateInfo_t * Extra_UnateComputeSlow( DdManager * dd, DdNode * bFunc ) +{ + int nSuppSize; + DdNode * bSupp, * bTemp; + Extra_UnateInfo_t * p; + int i, Res; + + // compute the support + bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp ); + nSuppSize = Extra_bddSuppSize( dd, bSupp ); +//printf( "Support = %d. ", nSuppSize ); +//Extra_bddPrint( dd, bSupp ); +//printf( "%d ", nSuppSize ); + + // allocate the storage for symmetry info + p = Extra_UnateInfoAllocate( nSuppSize ); + + // assign the variables + p->nVarsMax = dd->size; + for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ ) + { + Res = Extra_bddCheckUnateNaive( dd, bFunc, bTemp->index ); + p->pVars[i].iVar = bTemp->index; + if ( Res == -1 ) + p->pVars[i].Neg = 1; + else if ( Res == 1 ) + p->pVars[i].Pos = 1; + p->nUnate += (Res != 0); + } + Cudd_RecursiveDeref( dd, bSupp ); + return p; + +} /* end of Extra_UnateComputeSlow */ + +/**Function******************************************************************** + + Synopsis [Checks if the two variables are symmetric.] + + Description [Returns 0 if vars are not unate. Return -1/+1 if the var is neg/pos unate.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_bddCheckUnateNaive( + DdManager * dd, /* the DD manager */ + DdNode * bF, + int iVar) +{ + DdNode * bCof0, * bCof1; + int Res; + + assert( iVar < dd->size ); + + bCof0 = Cudd_Cofactor( dd, bF, Cudd_Not(Cudd_bddIthVar(dd,iVar)) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, bF, Cudd_bddIthVar(dd,iVar) ); Cudd_Ref( bCof1 ); + + if ( Cudd_bddLeq( dd, bCof0, bCof1 ) ) + Res = 1; + else if ( Cudd_bddLeq( dd, bCof1, bCof0 ) ) + Res =-1; + else + Res = 0; + + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + return Res; +} /* end of Extra_bddCheckUnateNaive */ + + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_UnateInfoCompute.] + + Description [Returns the set of symmetric variable pairs represented as a set + of two-literal ZDD cubes. Both variables always appear in the positive polarity + in the cubes. This function works without building new BDD nodes. Some relatively + small number of ZDD nodes may be built to ensure proper bookkeeping of the + symmetry information.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraZddUnateInfoCompute( + DdManager * dd, /* the manager */ + DdNode * bFunc, /* the function whose symmetries are computed */ + DdNode * bVars ) /* the set of variables on which this function depends */ +{ + DdNode * zRes; + DdNode * bFR = Cudd_Regular(bFunc); + + if ( cuddIsConstant(bFR) ) + { + if ( cuddIsConstant(bVars) ) + return z0; + return extraZddGetSingletonsBoth( dd, bVars ); + } + assert( bVars != b1 ); + + if ( zRes = cuddCacheLookup2Zdd(dd, extraZddUnateInfoCompute, bFunc, bVars) ) + return zRes; + else + { + DdNode * zRes0, * zRes1; + DdNode * zTemp, * zPlus; + DdNode * bF0, * bF1; + DdNode * bVarsNew; + int nVarsExtra; + int LevelF; + int AddVar; + + // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV + // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F + // count how many extra vars are there in bVars + nVarsExtra = 0; + LevelF = dd->perm[bFR->index]; + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + nVarsExtra++; + // the indexes (level) of variables should be synchronized now + assert( bFR->index == bVarsNew->index ); + + // cofactor the function + if ( bFR != bFunc ) // bFunc is complemented + { + bF0 = Cudd_Not( cuddE(bFR) ); + bF1 = Cudd_Not( cuddT(bFR) ); + } + else + { + bF0 = cuddE(bFR); + bF1 = cuddT(bFR); + } + + // solve subproblems + zRes0 = extraZddUnateInfoCompute( dd, bF0, cuddT(bVarsNew) ); + if ( zRes0 == NULL ) + return NULL; + cuddRef( zRes0 ); + + // if there is no symmetries in the negative cofactor + // there is no need to test the positive cofactor + if ( zRes0 == z0 ) + zRes = zRes0; // zRes takes reference + else + { + zRes1 = extraZddUnateInfoCompute( dd, bF1, cuddT(bVarsNew) ); + if ( zRes1 == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + return NULL; + } + cuddRef( zRes1 ); + + // only those variables are pair-wise symmetric + // that are pair-wise symmetric in both cofactors + // therefore, intersect the solutions + zRes = cuddZddIntersect( dd, zRes0, zRes1 ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zRes0 ); + Cudd_RecursiveDerefZdd( dd, zRes1 ); + } + + // consider the current top-most variable + AddVar = -1; + if ( Cudd_bddLeq( dd, bF0, bF1 ) ) // pos + AddVar = 0; + else if ( Cudd_bddLeq( dd, bF1, bF0 ) ) // neg + AddVar = 1; + if ( AddVar >= 0 ) + { + // create the singleton + zPlus = cuddZddGetNode( dd, 2*bFR->index + AddVar, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + // only zRes is referenced at this point + + // if we skipped some variables, these variables cannot be symmetric with + // any variables that are currently in the support of bF, but they can be + // symmetric with the variables that are in bVars but not in the support of bF + for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) ) + { + // create the negative singleton + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index+1, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + + // create the positive singleton + zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + } + cuddDeref( zRes ); + + /* insert the result into cache */ + cuddCacheInsert2(dd, extraZddUnateInfoCompute, bFunc, bVars, zRes); + return zRes; + } +} /* end of extraZddUnateInfoCompute */ + + +/**Function******************************************************************** + + Synopsis [Performs a recursive step of Extra_zddGetSingletons.] + + Description [Returns the set of ZDD singletons, containing those pos/neg + polarity ZDD variables that correspond to the BDD variables in bVars.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * extraZddGetSingletonsBoth( + DdManager * dd, /* the DD manager */ + DdNode * bVars) /* the set of variables */ +{ + DdNode * zRes; + + if ( bVars == b1 ) + return z1; + + if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletonsBoth, bVars) ) + return zRes; + else + { + DdNode * zTemp, * zPlus; + + // solve subproblem + zRes = extraZddGetSingletonsBoth( dd, cuddT(bVars) ); + if ( zRes == NULL ) + return NULL; + cuddRef( zRes ); + + + // create the negative singleton + zPlus = cuddZddGetNode( dd, 2*bVars->index+1, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + + // create the positive singleton + zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 ); + if ( zPlus == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zRes ); + return NULL; + } + cuddRef( zPlus ); + + // add these to the result + zRes = cuddZddUnion( dd, zTemp = zRes, zPlus ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + return NULL; + } + cuddRef( zRes ); + Cudd_RecursiveDerefZdd( dd, zTemp ); + Cudd_RecursiveDerefZdd( dd, zPlus ); + + cuddDeref( zRes ); + cuddCacheInsert1( dd, extraZddGetSingletonsBoth, bVars, zRes ); + return zRes; + } +} /* end of extraZddGetSingletonsBoth */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c index 9d4e5b5d..fcc7d84d 100644 --- a/src/misc/extra/extraUtilCanon.c +++ b/src/misc/extra/extraUtilCanon.c @@ -99,7 +99,8 @@ int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned Description [] - SideEffects [] + SideEffects [This procedure has a bug, which shows on Solaris. + Most likely has something to do with the casts, i.g *((unsigned *)pt0)] SeeAlso [] @@ -129,21 +130,22 @@ int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, ch pt0 = pt; pt1 = pt + (1 << nVarsN) / 8; // 5-var truth tables for this call - uInit0 = *((unsigned *)pt0); - uInit1 = *((unsigned *)pt1); +// uInit0 = *((unsigned *)pt0); +// uInit1 = *((unsigned *)pt1); if ( nVarsN == 3 ) { - uInit0 &= 0xFF; - uInit1 &= 0xFF; - uInit0 = (uInit0 << 24) | (uInit0 << 16) | (uInit0 << 8) | uInit0; - uInit1 = (uInit1 << 24) | (uInit1 << 16) | (uInit1 << 8) | uInit1; + uInit0 = (pt0[0] << 24) | (pt0[0] << 16) | (pt0[0] << 8) | pt0[0]; + uInit1 = (pt1[0] << 24) | (pt1[0] << 16) | (pt1[0] << 8) | pt1[0]; } else if ( nVarsN == 4 ) { - uInit0 &= 0xFFFF; - uInit1 &= 0xFFFF; - uInit0 = (uInit0 << 16) | uInit0; - uInit1 = (uInit1 << 16) | uInit1; + uInit0 = (pt0[1] << 24) | (pt0[0] << 16) | (pt0[1] << 8) | pt0[0]; + uInit1 = (pt1[1] << 24) | (pt1[0] << 16) | (pt1[1] << 8) | pt1[0]; + } + else + { + uInit0 = (pt0[3] << 24) | (pt0[2] << 16) | (pt0[1] << 8) | pt0[0]; + uInit1 = (pt1[3] << 24) | (pt1[2] << 16) | (pt1[1] << 8) | pt1[0]; } // storage for truth tables and phases diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c index 016f01e3..6e16b399 100644 --- a/src/misc/extra/extraUtilReader.c +++ b/src/misc/extra/extraUtilReader.c @@ -262,6 +262,9 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) // check if the new data should to be loaded if ( p->pBufferCur > p->pBufferStop ) Extra_FileReaderReload( p ); + +// printf( "%d\n", p->pBufferEnd - p->pBufferCur ); + // process the string starting from the current position for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ ) { @@ -270,6 +273,10 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) p->nLineCounter++; // switch depending on the character MapValue = p->pCharMap[*pChar]; + +// printf( "Char value = %d. Map value = %d.\n", *pChar, MapValue ); + + switch ( MapValue ) { case EXTRA_CHAR_COMMENT: @@ -326,6 +333,14 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p ) return p->vTokens; } printf( "Extra_FileReader failed to parse the file \"%s\".\n", p->pFileName ); +/* + { + int i; + for ( i = 0; i < p->vTokens->nSize; i++ ) + printf( "%s ", p->vTokens->pArray[i] ); + printf( "\n" ); + } +*/ return NULL; } diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 42a0d84f..8e7b1772 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,4 +1,5 @@ -SRC += src/misc/extra/extraBddKmap.c \ +SRC += src/misc/extra/extraBddAuto.c \ + src/misc/extra/extraBddKmap.c \ src/misc/extra/extraBddMisc.c \ src/misc/extra/extraBddSymm.c \ src/misc/extra/extraUtilBitMatrix.c \ diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 2d36addd..7a96b0d7 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -345,6 +345,7 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) if ( p->nCap >= nCapMin ) return; p->pArray = REALLOC( int, p->pArray, nCapMin ); + assert( p->pArray ); p->nCap = nCapMin; } diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c index b24773be..af76cd84 100644 --- a/src/opt/dec/decAbc.c +++ b/src/opt/dec/decAbc.c @@ -18,7 +18,7 @@ #include "abc.h" #include "dec.h" -#include "aig.h" +//#include "aig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -214,6 +214,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda SeeAlso [] ***********************************************************************/ +/* Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) { Dec_Node_t * pNode; @@ -235,6 +236,7 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ) // complement the result if necessary return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); } +*/ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index 55a75cf5..ee029789 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -160,6 +160,7 @@ struct Aig_Man_t_ Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes + Aig_Pattern_t * pPatMask; // the mask which shows what patterns are used // simulation patterns int nPiWords; // the number of words in the PI info int nPatsMax; // the max number of patterns @@ -169,6 +170,7 @@ struct Aig_Man_t_ // temporary data Vec_Ptr_t * vFanouts; // temporary storage for fanouts of a node Vec_Ptr_t * vToReplace; // the nodes to replace + Vec_Int_t * vClassTemp; // temporary class representatives }; // the simulation patter @@ -254,6 +256,7 @@ static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * p static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; } +static inline unsigned * Aig_SimInfoForNodeId( Aig_SimInfo_t * p, int NodeId ) { assert( p->Type ); return p->pData + p->nWords * NodeId; } static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; } static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; } @@ -332,15 +335,16 @@ extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ); /*=== fraigClasses.c ==========================================================*/ extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll ); -extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ); +extern int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask ); +extern void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats ); /*=== fraigCnf.c ==========================================================*/ extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan ); /*=== fraigEngine.c ==========================================================*/ +extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ); extern void Aig_EngineSimulateFirst( Aig_Man_t * p ); extern int Aig_EngineSimulate( Aig_Man_t * p ); -extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ); /*=== fraigSim.c ==========================================================*/ -extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ); +extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, int Type ); extern void Aig_SimInfoClean( Aig_SimInfo_t * p ); extern void Aig_SimInfoRandom( Aig_SimInfo_t * p ); extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ); @@ -349,6 +353,8 @@ extern void Aig_SimInfoFree( Aig_SimInfo_t * p ); extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll ); extern Aig_Pattern_t * Aig_PatternAlloc( int nBits ); extern void Aig_PatternClean( Aig_Pattern_t * pPat ); +extern void Aig_PatternFill( Aig_Pattern_t * pPat ); +extern int Aig_PatternCount( Aig_Pattern_t * pPat ); extern void Aig_PatternRandom( Aig_Pattern_t * pPat ); extern void Aig_PatternFree( Aig_Pattern_t * pPat ); diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c index 3807d28a..4c64c897 100644 --- a/src/sat/aig/aigMan.c +++ b/src/sat/aig/aigMan.c @@ -42,7 +42,7 @@ void Aig_ManSetDefaultParams( Aig_Param_t * pParam ) { memset( pParam, 0, sizeof(Aig_Param_t) ); - pParam->nPatsRand = 1024; // the number of random patterns + pParam->nPatsRand = 4096; // the number of random patterns pParam->nBTLimit = 99; // backtrack limit at the intermediate nodes pParam->nSeconds = 1; // the timeout for the final miter in seconds } @@ -67,8 +67,8 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ) p = ALLOC( Aig_Man_t, 1 ); memset( p, 0, sizeof(Aig_Man_t) ); p->pParam = &p->Param; - p->nTravIds = 1; - p->nPatsMax = 20; + p->nTravIds = 1; + p->nPatsMax = 25; // set the defaults *p->pParam = *pParam; // start memory managers @@ -84,6 +84,8 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ) // initialize other variables p->vFanouts = Vec_PtrAlloc( 10 ); p->vToReplace = Vec_PtrAlloc( 10 ); + p->vClassTemp = Vec_IntAlloc( 10 ); + p->vPats = Vec_PtrAlloc( p->nPatsMax ); return p; } @@ -132,6 +134,9 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 ); if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 ); if ( p->vClasses ) Vec_VecFree( p->vClasses ); + // patterns + if ( p->vPats ) Vec_PtrFree( p->vPats ); + if ( p->pPatMask ) Aig_PatternFree( p->pPatMask ); // nodes Aig_MemFixedStop( p->mmNodes, 0 ); Vec_PtrFree( p->vNodes ); @@ -140,6 +145,7 @@ void Aig_ManStop( Aig_Man_t * p ) // temporary Vec_PtrFree( p->vFanouts ); Vec_PtrFree( p->vToReplace ); + Vec_IntFree( p->vClassTemp ); Aig_TableFree( p->pTable ); free( p ); } diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c index 2f2d3e0c..a8df9a72 100644 --- a/src/sat/aig/fraigClass.c +++ b/src/sat/aig/fraigClass.c @@ -80,7 +80,7 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) } } stmm_free_table( tSim2Node ); - +/* // print the classes { Vec_Ptr_t * vVec; @@ -93,6 +93,8 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) printf( "%d ", Vec_PtrSize(vVec) ); printf( "\n" ); } +*/ + printf( "Classes = %6d. Pairs = %6d.\n", Vec_VecSize(vClasses), Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses) ); return vClasses; } @@ -115,14 +117,86 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) uKey = 0; if ( fPhase ) for ( i = 0; i < nWords; i++ ) - uKey ^= Primes[i%10] * pData[i]; + uKey ^= i * Primes[i%10] * pData[i]; else for ( i = 0; i < nWords; i++ ) - uKey ^= Primes[i%10] * ~pData[i]; + uKey ^= i * Primes[i%10] * ~pData[i]; return uKey; } + +/**Function************************************************************* + + Synopsis [Splits the equivalence class.] + + Description [Given an equivalence class (vClass) and the simulation info, + split the class into two based on the info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManSplitClass( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Int_t * vClass, Vec_Int_t * vClass2, Aig_Pattern_t * pPat ) +{ + int NodeId, i, k, w; + Aig_Node_t * pRoot, * pTemp; + unsigned * pRootData, * pTempData; + assert( Vec_IntSize(vClass) > 1 ); + assert( pInfo->nPatsCur == pPat->nBits ); +// printf( "Class = %5d. --> ", Vec_IntSize(vClass) ); + // clear storage for the new classes + Vec_IntClear( vClass2 ); + // get the root member of the class + pRoot = Aig_ManNode( p, Vec_IntEntry(vClass, 0) ); + pRootData = Aig_SimInfoForNode( pInfo, pRoot ); + // sort the class members: + // (1) with the same siminfo as pRoot remain in vClass + // (2) nodes with other siminfo go to vClass2 + k = 1; + Vec_IntForEachEntryStart( vClass, NodeId, i, 1 ) + { + NodeId = Vec_IntEntry(vClass, i); + pTemp = Aig_ManNode( p, NodeId ); + pTempData = Aig_SimInfoForNode( pInfo, pTemp ); + if ( pRoot->fPhase == pTemp->fPhase ) + { + for ( w = 0; w < pInfo->nWords; w++ ) + if ( pRootData[w] != pTempData[w] ) + break; + if ( w == pInfo->nWords ) // the same info + Vec_IntWriteEntry( vClass, k++, NodeId ); + else + { + Vec_IntPush( vClass2, NodeId ); + // record the diffs if they are not distinguished by the first pattern + if ( ((pRootData[0] ^ pTempData[0]) & 1) == 0 ) + for ( w = 0; w < pInfo->nWords; w++ ) + pPat->pData[w] |= (pRootData[w] ^ pTempData[w]); + } + } + else + { + for ( w = 0; w < pInfo->nWords; w++ ) + if ( pRootData[w] != ~pTempData[w] ) + break; + if ( w == pInfo->nWords ) // the same info + Vec_IntWriteEntry( vClass, k++, NodeId ); + else + { + Vec_IntPush( vClass2, NodeId ); + // record the diffs if they are not distinguished by the first pattern + if ( ((pRootData[0] ^ ~pTempData[0]) & 1) == 0 ) + for ( w = 0; w < pInfo->nWords; w++ ) + pPat->pData[w] |= (pRootData[w] ^ ~pTempData[w]); + } + } + } + Vec_IntShrink( vClass, k ); +// printf( "Class1 = %5d. Class2 = %5d.\n", Vec_IntSize(vClass), Vec_IntSize(vClass2) ); +} + /**Function************************************************************* Synopsis [Updates the equivalence classes using the simulation info.] @@ -135,8 +209,108 @@ unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) SeeAlso [] ***********************************************************************/ -void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ) +int Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses, Aig_Pattern_t * pPatMask ) +{ + Vec_Ptr_t * vClass; + int i, k, fSplit = 0; + assert( Vec_VecSize(vClasses) > 0 ); + // collect patterns that lead to changes + Aig_PatternClean( pPatMask ); + // split the classes using the new symmetry info + Vec_VecForEachLevel( vClasses, vClass, i ) + { + if ( i == 0 ) + continue; + // split vClass into two parts (vClass and vClassTemp) + Aig_ManSplitClass( p, pInfo, (Vec_Int_t *)vClass, p->vClassTemp, pPatMask ); + // check if there is any splitting + if ( Vec_IntSize(p->vClassTemp) > 0 ) + fSplit = 1; + // skip the new class if it is empty or trivial + if ( Vec_IntSize(p->vClassTemp) < 2 ) + continue; + // consider replacing the current class with the new one + if ( Vec_PtrSize(vClass) == 1 ) + { + assert( vClasses->pArray[i] == vClass ); + vClasses->pArray[i] = p->vClassTemp; + p->vClassTemp = (Vec_Int_t *)vClass; + i--; + continue; + } + // add the new non-trival class in the end + Vec_PtrPush( (Vec_Ptr_t *)vClasses, p->vClassTemp ); + p->vClassTemp = Vec_IntAlloc( 10 ); + } + // free trivial classes + k = 0; + Vec_VecForEachLevel( vClasses, vClass, i ) + { + assert( Vec_PtrSize(vClass) > 0 ); + if ( Vec_PtrSize(vClass) == 1 ) + Vec_PtrFree(vClass); + else + vClasses->pArray[k++] = vClass; + } + Vec_PtrShrink( (Vec_Ptr_t *)vClasses, k ); + // catch the patterns which led to splitting + printf( "Classes = %6d. Pairs = %6d. Patterns = %3d.\n", + Vec_VecSize(vClasses), + Vec_VecSizeSize(vClasses) - Vec_VecSize(vClasses), + Vec_PtrSize(p->vPats) ); + return fSplit; +} + +/**Function************************************************************* + + Synopsis [Collects useful patterns.] + + Description [If the flag fAddToVector is 1, creates and adds new patterns + to the internal storage of patterns.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCollectPatterns( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Aig_Pattern_t * pMask, Vec_Ptr_t * vPats ) { + Aig_SimInfo_t * pInfoRes = p->pInfo; + Aig_Pattern_t * pPatNew; + Aig_Node_t * pNode; + int i, k; + + assert( Aig_InfoHasBit(pMask->pData, 0) == 0 ); + for ( i = 0; i < pMask->nBits; i++ ) + { + if ( vPats && Vec_PtrSize(vPats) >= p->nPatsMax ) + break; + if ( i == 0 || Aig_InfoHasBit(pMask->pData, i) ) + { + // expand storage if needed + if ( pInfoRes->nPatsCur == pInfoRes->nPatsMax ) + Aig_SimInfoResize( pInfoRes ); + // create a new pattern + if ( vPats ) + { + pPatNew = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternClean( pPatNew ); + } + // go through the PIs + Aig_ManForEachPi( p, pNode, k ) + { + if ( Aig_InfoHasBit( Aig_SimInfoForNode(pInfo, pNode), i ) ) + { + Aig_InfoSetBit( Aig_SimInfoForPi(pInfoRes, k), pInfoRes->nPatsCur ); + if ( vPats ) Aig_InfoSetBit( pPatNew->pData, k ); + } + } + // store the new pattern + if ( vPats ) Vec_PtrPush( vPats, pPatNew ); + // increment the number of patterns stored + pInfoRes->nPatsCur++; + } + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c index e7df1335..decf05ee 100644 --- a/src/sat/aig/fraigCore.c +++ b/src/sat/aig/fraigCore.c @@ -68,6 +68,8 @@ Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ) // create equivalence classes Aig_EngineSimulateRandomFirst( pMan ); + // reduce equivalence classes using simulation + Aig_EngineSimulateFirst( pMan ); return RetValue; } diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c index 6214bf3b..17468e8f 100644 --- a/src/sat/aig/fraigEngine.c +++ b/src/sat/aig/fraigEngine.c @@ -30,6 +30,39 @@ /**Function************************************************************* + Synopsis [Simulates all nodes using random simulation for the first time.] + + Description [Assigns the original simulation info and the storage for the + future simulation info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ) +{ + Aig_SimInfo_t * pInfoPi, * pInfoAll; + assert( !p->pInfo && !p->pInfoTemp ); + // create random PI info + pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 ); + Aig_SimInfoRandom( pInfoPi ); + // allocate sim info for all nodes + pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 1 ); + // simulate though the circuit + Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); + // detect classes + p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); + Aig_SimInfoFree( pInfoAll ); + // save simulation info + p->pInfo = pInfoPi; + p->pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), Aig_ManPiNum(p)+1, 0 ); + p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1, 1 ); + p->pPatMask = Aig_PatternAlloc( Aig_ManPiNum(p)+1 ); +} + +/**Function************************************************************* + Synopsis [Starts the simulation engine for the first time.] Description [Tries several random patterns and their distance-1 @@ -43,15 +76,55 @@ void Aig_EngineSimulateFirst( Aig_Man_t * p ) { Aig_Pattern_t * pPat; - int i; - assert( Vec_PtrSize(p->vPats) == 0 ); - for ( i = 0; i < p->nPatsMax; i++ ) + int i, Counter; + + // simulate the pattern of all zeros + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternClean( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + + // simulate the pattern of all ones + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternFill( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + + // simulate random until the number of new patterns is reasonable + do { + // generate random PI siminfo + Aig_SimInfoRandom( p->pInfoPi ); + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL ); + if ( Vec_VecSize(p->vClasses) == 0 ) + return; + // count the number of useful patterns + Counter = Aig_PatternCount(p->pPatMask); + } + while ( Counter > p->nPatsMax/2 ); + + // perform targetted simulation + for ( i = 0; i < 3; i++ ) { - pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); - Aig_PatternRandom( pPat ); - Vec_PtrPush( p->vPats, pPat ); - if ( !Aig_EngineSimulate( p ) ) + assert( Vec_PtrSize(p->vPats) == 0 ); + // generate random PI siminfo + Aig_SimInfoRandom( p->pInfoPi ); + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats ); + if ( Vec_VecSize(p->vClasses) == 0 ) return; + // simulate the remaining patters + if ( Vec_PtrSize(p->vPats) > 0 ) + if ( !Aig_EngineSimulate( p ) ) + return; } } @@ -79,51 +152,21 @@ int Aig_EngineSimulate( Aig_Man_t * p ) { // get the pattern and create new siminfo pPat = Vec_PtrPop(p->vPats); + assert( pPat->nBits == Aig_ManPiNum(p) ); // create the new siminfo Aig_SimInfoFromPattern( p->pInfoPi, pPat ); - // free the patter + // free the pattern Aig_PatternFree( pPat ); // simulate this info Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); // split the classes and collect the new patterns - Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses ); + if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) ) + Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats ); } return Vec_VecSize(p->vClasses) > 0; } -/**Function************************************************************* - - Synopsis [Simulates all nodes using random simulation for the first time.] - - Description [Assigns the original simulation info and the storage for the - future simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ) -{ - Aig_SimInfo_t * pInfoPi, * pInfoAll; - assert( !p->pInfo && !p->pInfoTemp ); - // create random PI info - pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 ); - Aig_SimInfoRandom( pInfoPi ); - // allocate sim info for all nodes - pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); - // simulate though the circuit - Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); - // detect classes - p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); - Aig_SimInfoFree( pInfoAll ); - // save simulation info - p->pInfo = pInfoPi; - p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 ); - p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c index 415b6918..6d4f214c 100644 --- a/src/sat/aig/fraigSim.c +++ b/src/sat/aig/fraigSim.c @@ -80,7 +80,7 @@ void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t pDataAnd[k] = pData0[k] & pData1[k]; } // derive the PO siminfo - Aig_ManForEachPi( p, pNode, i ) + Aig_ManForEachPo( p, pNode, i ) { pDataPo = Aig_SimInfoForNode( pInfoAll, pNode ); pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) ); @@ -106,16 +106,17 @@ void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t SeeAlso [] ***********************************************************************/ -Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ) +Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nBits, int Type ) { Aig_SimInfo_t * p; p = ALLOC( Aig_SimInfo_t, 1 ); memset( p, 0, sizeof(Aig_SimInfo_t) ); p->Type = Type; p->nNodes = nNodes; - p->nWords = nWords; - p->nPatsMax = nWords * sizeof(unsigned) * 8; - p->pData = ALLOC( unsigned, nNodes * nWords ); + p->nWords = Aig_BitWordNum(nBits); + p->nPatsCur = nBits; + p->nPatsMax = p->nWords * sizeof(unsigned) * 8; + p->pData = ALLOC( unsigned, nNodes * p->nWords ); return p; } @@ -161,7 +162,6 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p ) pData = p->pData + p->nWords * i; *pData <<= 1; } - p->nPatsCur = p->nPatsMax; } /**Function************************************************************* @@ -180,8 +180,8 @@ void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ) unsigned * pData; int i, k; assert( p->Type == 0 ); - assert( p->nNodes == pPat->nBits ); - for ( i = 0; i < p->nNodes; i++ ) + assert( p->nPatsCur == pPat->nBits+1 ); + for ( i = 0; i < p->nPatsCur; i++ ) { // get the pointer to the bitdata for node i pData = p->pData + p->nWords * i; @@ -192,8 +192,8 @@ void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ) else for ( k = 0; k < p->nWords; k++ ) pData[k] = 0; - // flip one bit - Aig_InfoXorBit( pData, i ); + // flip one bit, starting from the first pattern + if ( i ) Aig_InfoXorBit( pData, i-1 ); } } @@ -285,6 +285,22 @@ void Aig_PatternClean( Aig_Pattern_t * pPat ) /**Function************************************************************* + Synopsis [Cleans the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternFill( Aig_Pattern_t * pPat ) +{ + memset( pPat->pData, 0xff, sizeof(unsigned) * pPat->nWords ); +} + +/**Function************************************************************* + Synopsis [Sets the random pattern.] Description [] @@ -303,6 +319,25 @@ void Aig_PatternRandom( Aig_Pattern_t * pPat ) /**Function************************************************************* + Synopsis [Counts the number of 1s in the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_PatternCount( Aig_Pattern_t * pPat ) +{ + int i, Counter = 0; + for ( i = 0; i < pPat->nBits; i++ ) + Counter += Aig_InfoHasBit( pPat->pData, i ); + return Counter; +} + +/**Function************************************************************* + Synopsis [Deallocates the pattern.] Description [] diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c new file mode 100644 index 00000000..2c402184 --- /dev/null +++ b/src/sat/aig/rwrTruth.c @@ -0,0 +1,454 @@ +/**CFile**************************************************************** + + FileName [rwrTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +/* The code in this file was written with portability to 64-bits in mind. + The type "unsigned" is assumed to be 32-bit on any platform. +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ABCTMAX 8 // the max number of vars + +typedef struct Aig_Truth_t_ Aig_Truth_t; +struct Aig_Truth_t_ +{ + short nVars; // the number of variables + short nWords; // the number of 32-bit words + unsigned Truth[1<<(ABCTMAX-5)]; // the truth table + unsigned Cofs[2][1<<(ABCTMAX-6)]; // the truth table of cofactors + unsigned Data[4][1<<(ABCTMAX-7)]; // the truth table of cofactors + short Counts[ABCTMAX][2]; // the minterm counters + Aig_Node_t * pLeaves[ABCTMAX]; // the pointers to leaves + Aig_Man_t * pMan; // the AIG manager +}; + +static void Aig_TruthCount( Aig_Truth_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the function given the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Truth_t * Aig_TruthCreate( int nVars, unsigned * pTruth, Aig_Node_t ** pLeaves ) +{ + Aig_Truth_t * p; + int i; + p = ALLOC( Aig_Truth_t, 1 ); + memset( p, 0, sizeof(Aig_Truth_t) ); + p->nVars = nVars; + p->nWords = (nVars < 5)? 1 : (1 << (nVars-5)); + for ( i = 0; i < p->nWords; i++ ) + p->Truth[i] = pTruth[i]; + if ( nVars < 5 ) + p->Truth[0] &= (~0u >> (32-(1<<nVars))); + for ( i = 0; i < p->nVars; i++ ) + p->pLeaves[i] = pLeaves[i]; + Aig_TruthCount( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Counts the number of miterms in the cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_WordCountOnes( unsigned val ) +{ + val = (val & 0x55555555) + ((val>>1) & 0x55555555); + val = (val & 0x33333333) + ((val>>2) & 0x33333333); + val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F); + val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF); + return (val & 0x0000FFFF) + (val>>8); +} + +/**Function************************************************************* + + Synopsis [Counts the number of miterms in the cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TruthCount( Aig_Truth_t * p ) +{ + static unsigned Masks[5][2] = { + { 0x33333333, 0xAAAAAAAA }, + { 0x55555555, 0xCCCCCCCC }, + { 0x0F0F0F0F, 0xF0F0F0F0 }, + { 0x00FF00FF, 0xFF00FF00 }, + { 0x0000FFFF, 0xFFFF0000 } + }; + + int i, k; + assert( p->Counts[0][0] == 0 && p->Counts[0][1] == 0 ); + for ( i = 0; i < p->nVars; i++ ) + { + p->Counts[i][0] = p->Counts[i][1] = 0; + if ( i < 5 ) + { + for ( k = 0; k < p->nWords; k++ ) + { + p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] & Masks[i][0] ); + p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] & Masks[i][1] ); + } + } + else + { + for ( k = 0; k < p->nWords; k++ ) + if ( i & (1 << (k-5)) ) + p->Counts[i][1] += Aig_WordCountOnes( p->Truth[k] ); + else + p->Counts[i][0] += Aig_WordCountOnes( p->Truth[k] ); + } + } +/* + // normalize the variables + for ( i = 0; i < p->nVars; i++ ) + if ( p->Counts[i][0] > p->Counts[i][1] ) + { + k = p->Counts[i][0]; + p->Counts[i][0] = p->Counts[i][1]; + p->Counts[i][1] = k; + p->pLeaves[i] = Aig_Not( p->pLeaves[i] ); + } +*/ +} + +/**Function************************************************************* + + Synopsis [Extracts one part of the bitstring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size ) +{ + return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size)); +} + +/**Function************************************************************* + + Synopsis [Inserts one part of the bitstring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part ) +{ + p[Start/5] |= (Part << (Start%32)); +} + +/**Function************************************************************* + + Synopsis [Computes the cofactor with respect to one variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TruthCofactor( int Var, int Pol, int nVars, unsigned * pTruth, unsigned * pResult ) +{ + if ( Var < 5 ) + { + int nPartSize = ( 1 << Var ); + int nParts = ( 1 << (nVars-Var-1) ); + unsigned uPart; + int i; + for ( i = 0; i < nParts; i++ ) + { + uPart = Aig_WordGetPart( pTruth, (2*i+Pol)*nPartSize, nPartSize ); + Aig_WordSetPart( pResult, i*nPartSize, uPart ); + } + if ( nVars <= 5 ) + pResult[0] &= (~0u >> (32-(1<<(nVars-1)))); + } + else + { + int nWords = (1 << (nVars-5)); + int i, k = 0; + for ( i = 0; i < nWords; i++ ) + if ( (i & (1 << (Var-5))) == Pol ) + pResult[k++] = pTruth[i]; + assert( k == nWords/2 ); + } +} + + + + +/**Function************************************************************* + + Synopsis [Computes the BDD of the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int nVars, int iVar ) +{ + DdNode * bCof0, * bCof1, * bRes; + if ( nVars == 1 ) + return Cudd_NotCond( Cudd_ReadOne(dd), !Aig_WordGetPart(pTruth, Shift, 1) ); + if ( nVars == 3 ) + { + unsigned char * pChar = ((char *)pTruth) + Shift/8; + assert( Shift % 8 == 0 ); + if ( *pChar == 0 ) + return Cudd_ReadLogicZero(dd); + if ( *pChar == 0xFF ) + return Cudd_ReadOne(dd); + } + if ( nVars == 5 ) + { + unsigned * pWord = pTruth + Shift/32; + assert( Shift % 32 == 0 ); + if ( *pWord == 0 ) + return Cudd_ReadLogicZero(dd); + if ( *pWord == 0xFFFFFFFF ) + return Cudd_ReadOne(dd); + } + bCof0 = Aig_TruthToBdd_rec( dd, pTruth, Shift, nVars-1, iVar+1 ); Cudd_Ref( bCof0 ); + bCof1 = Aig_TruthToBdd_rec( dd, pTruth, Shift + (1 << (nVars-1)), nVars-1, iVar+1 ); Cudd_Ref( bCof1 ); + bRes = Cudd_bddIte( dd, Cudd_bddIthVar(dd, iVar), bCof1, bCof0 ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + Cudd_Deref( bRes ); + return bRes; +} + +/**Function************************************************************* + + Synopsis [Computes the BDD of the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Aig_TruthToBdd( DdManager * dd, Aig_Truth_t * p ) +{ + return Aig_TruthToBdd_rec( dd, p->Truth, 0, p->nVars, 0 ); +} + + + + +/**Function************************************************************* + + Synopsis [Compare bistrings.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_WordCompare( unsigned * p0, unsigned * p1, int nWords ) +{ + int i; + for ( i = 0; i < nWords; i++ ) + if ( p0[i] != p1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Compare bistrings.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_WordCompareCompl( unsigned * p0, unsigned * p1, int nWords ) +{ + int i; + for ( i = 0; i < nWords; i++ ) + if ( p0[i] != ~p1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the cofactor with respect to one variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TruthReplaceByCofactor( Aig_Truth_t * p, int iVar, unsigned * pTruth ) +{ +} + + +/**Function************************************************************* + + Synopsis [Computes the cofactor with respect to one variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p ) +{ + Aig_Node_t * pVar; + int nOnesCof = ( 1 << (p->nVars-1) ); + int nWordsCof = (p->nWords == 1 ? 1 : p->nWords/2); + int i; + + // check for constant function + if ( p->nVars == 0 ) + return Aig_NotCond( Aig_ManConst1(p->pMan), (p->Truth[0]&1)==0 ); + + // count the number of minterms in the cofactors + Aig_TruthCount( p ); + + // remove redundant variables and EXORs + for ( i = p->nVars - 1; i >= 0; i-- ) + { + if ( p->Counts[i][0] == p->Counts[i][1] ) + { + // compute cofactors + Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] ); + Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] ); + if ( Aig_WordCompare( p->Cofs[0], p->Cofs[1], nWordsCof ) ) + { // equal + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] ); + return Aig_TruthDecompose( p ); + } + } + // check the case of EXOR + if ( p->Counts[i][0] == nOnesCof - p->Counts[i][1] ) + { + // compute cofactors + Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] ); + Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] ); + if ( Aig_WordCompareCompl( p->Cofs[0], p->Cofs[1], nWordsCof ) ) + { // equal + pVar = p->pLeaves[i]; + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] ); + // F = x' * F0 + x * F1 = x <+> F0 assuming that F0 == ~F1 + return Aig_Xor( p->pMan, pVar, Aig_TruthDecompose( p ) ); + } + } + } + + // process variables with constant cofactors + for ( i = p->nVars - 1; i >= 0; i-- ) + { + if ( p->Counts[i][0] != 0 && p->Counts[i][1] != 0 && + p->Counts[i][0] != nOnesCof && p->Counts[i][1] != nOnesCof ) + continue; + pVar = p->pLeaves[i]; + if ( p->Counts[i][0] == 0 ) + { + Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] ); + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] ); + // F = x' * 0 + x * F1 = x * F1 + return Aig_And( p->pMan, pVar, Aig_TruthDecompose( p ) ); + } + if ( p->Counts[i][1] == 0 ) + { + Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] ); + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] ); + // F = x' * F0 + x * 0 = x' * F0 + return Aig_And( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) ); + } + if ( p->Counts[i][0] == nOnesCof ) + { + Aig_TruthCofactor( i, 1, p->nVars, p->Truth, p->Cofs[1] ); + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[1] ); + // F = x' * 1 + x * F1 = x' + F1 + return Aig_Or( p->pMan, Aig_Not(pVar), Aig_TruthDecompose( p ) ); + } + if ( p->Counts[i][1] == nOnesCof ) + { + Aig_TruthCofactor( i, 0, p->nVars, p->Truth, p->Cofs[0] ); + // remove redundant variable + Aig_TruthReplaceByCofactor( p, i, p->Cofs[0] ); + // F = x' * F0 + x * 1 = x + F0 + return Aig_Or( p->pMan, pVar, Aig_TruthDecompose( p ) ); + } + assert( 0 ); + } + +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 3fadd457..d25e42db 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -34,6 +34,7 @@ struct ABC_ManagerStruct_t Abc_Ntk_t * pNtk; // the starting ABC network Abc_Ntk_t * pTarget; // the AIG representing the target char * pDumpFileName; // the name of the file to dump the target network + Extra_MmFlex_t * pMmNames; // memory manager for signal names // solving parameters int mode; // 0 = brute-force SAT; 1 = resource-aware FRAIG int nSeconds; // time limit for pure SAT solving @@ -76,6 +77,7 @@ ABC_Manager ABC_InitManager() mng->pNtk->pName = util_strsav("csat_network"); mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); + mng->pMmNames = Extra_MmFlexStart(); mng->vNodes = Vec_PtrAlloc( 100 ); mng->vValues = Vec_IntAlloc( 100 ); mng->nSeconds = ABC_DEFAULT_TIMEOUT; @@ -97,6 +99,7 @@ void ABC_QuitManager( ABC_Manager mng ) { if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); + if ( mng->pMmNames ) Extra_MmFlexStop( mng->pMmNames, 0 ); if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk ); if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); if ( mng->vNodes ) Vec_PtrFree( mng->vNodes ); @@ -146,9 +149,15 @@ void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option ) int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) { Abc_Obj_t * pObj, * pFanin; - char * pSop; + char * pSop, * pNewName; int i; + // save the name in the local memory manager + pNewName = Extra_MmFlexEntryFetch( mng->pMmNames, strlen(name) + 1 ); + strcpy( pNewName, name ); + name = pNewName; + + // consider different cases, create the node, and map the node into the name switch( type ) { case ABC_BPI: @@ -250,6 +259,8 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha printf( "ABC_AddGate: Unknown gate type.\n" ); break; } + + // map the name into the node if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) ) { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } return 1; @@ -690,6 +701,101 @@ char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ) return pName; } + + +/**Function************************************************************* + + Synopsis [This procedure applies a rewriting script to the network.] + + Description [Rewriting is performed without regard for the number of + logic levels. This corresponds to "circuit compression for formal + verification" (Per Bjesse et al, ICCAD 2004) but implemented in a more + exhaustive way than in the above paper.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void ABC_PerformRewriting( ABC_Manager mng ) +{ + void * pAbc; + char Command[1000]; + int clkBalan, clkResyn, clk; + int fPrintStats = 1; + int fUseResyn = 1; + + // procedures to get the ABC framework and execute commands in it + extern void * Abc_FrameGetGlobalFrame(); + extern void Abc_FrameReplaceCurrentNetwork( void * p, Abc_Ntk_t * pNtk ); + extern int Cmd_CommandExecute( void * p, char * sCommand ); + extern Abc_Ntk_t * Abc_FrameReadNtk( void * p ); + + + // get the pointer to the ABC framework + pAbc = Abc_FrameGetGlobalFrame(); + assert( pAbc != NULL ); + + // replace the current network by the target network + Abc_FrameReplaceCurrentNetwork( pAbc, mng->pTarget ); + +clk = clock(); + ////////////////////////////////////////////////////////////////////////// + // balance + sprintf( Command, "balance" ); + if ( Cmd_CommandExecute( pAbc, Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } +clkBalan = clock() - clk; + + ////////////////////////////////////////////////////////////////////////// + // print stats + if ( fPrintStats ) + { + sprintf( Command, "print_stats" ); + if ( Cmd_CommandExecute( pAbc, Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } + +clk = clock(); + ////////////////////////////////////////////////////////////////////////// + // synthesize + if ( fUseResyn ) + { + sprintf( Command, "balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance" ); + if ( Cmd_CommandExecute( pAbc, Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } +clkResyn = clock() - clk; + + ////////////////////////////////////////////////////////////////////////// + // print stats + if ( fPrintStats ) + { + sprintf( Command, "print_stats" ); + if ( Cmd_CommandExecute( pAbc, Command ) ) + { + fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); + return; + } + } + printf( "Balancing = %6.2f sec ", (float)(clkBalan)/(float)(CLOCKS_PER_SEC) ); + printf( "Rewriting = %6.2f sec ", (float)(clkResyn)/(float)(CLOCKS_PER_SEC) ); + printf( "\n" ); + + // read the target network from the current network + mng->pTarget = Abc_NtkDup( Abc_FrameReadNtk(pAbc) ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index 3e04c7df..a6179710 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -171,6 +171,8 @@ extern void ABC_Dump_Bench_File(ABC_Manager mng); extern void ABC_QuitManager( ABC_Manager mng ); extern void ABC_TargetResFree( ABC_Target_ResultT * p ); +extern void ABC_PerformRewriting( ABC_Manager mng ); + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 673fcad7..ff6faa33 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -185,7 +185,7 @@ void Fraig_ManFree( Fraig_Man_t * p ) // Fraig_TablePrintStatsF( p ); // Fraig_TablePrintStatsF0( p ); } - + for ( i = 0; i < p->vNodes->nSize; i++ ) if ( p->vNodes->pArray[i]->vFanins ) { diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index a9e09f61..d4358772 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -156,6 +156,132 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p ) /**Function************************************************************* + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 1; + // check the children + return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) + + Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi2_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 0; + // skip the boundary node + if ( pNode->TravId == pMan->nTravIds-1 ) + { + pNode->TravId = pMan->nTravIds; + return 1; + } + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 1; + // check the children + return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) + + Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pOld is in the TFI of pNew.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_MarkTfi3_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode ) +{ + // skip the visited node + if ( pNode->TravId == pMan->nTravIds ) + return 1; + // skip the boundary node + if ( pNode->TravId == pMan->nTravIds-1 ) + { + pNode->TravId = pMan->nTravIds; + return 1; + } + pNode->TravId = pMan->nTravIds; + // skip the PI node + if ( pNode->NumPi >= 0 ) + return 0; + // check the children + return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) * + Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + int NumPis, NumCut, fContain; + + // mark the TFI of pNew + p->nTravIds++; + NumPis = Fraig_MarkTfi_rec( p, pNew ); + printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level ); + + // check if the old is in the TFI + if ( pOld->TravId == p->nTravIds ) + { + printf( "* " ); + return; + } + + // count the boundary of nodes in pOld + p->nTravIds++; + NumCut = Fraig_MarkTfi2_rec( p, pOld ); + printf( "%d", NumCut ); + + // check if the new is contained in the old's support + p->nTravIds++; + fContain = Fraig_MarkTfi3_rec( p, pNew ); + printf( "%c ", fContain? '+':'-' ); +} + + +/**Function************************************************************* + Synopsis [Checks whether two nodes are functinally equivalent.] Description [The flag (fComp) tells whether the nodes to be checked @@ -202,6 +328,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * // get the logic cone clk = clock(); +// Fraig_VarsStudy( p, pOld, pNew ); Fraig_OrderVariables( p, pOld, pNew ); // Fraig_PrepareCones( p, pOld, pNew ); p->timeTrav += clock() - clk; @@ -223,18 +350,20 @@ if ( fVerbose ) Msat_SolverPrepare( p->pSat, p->vVarsInt ); //p->time3 += clock() - clk; + // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 Msat_IntVecClear( p->vProj ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); + +//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); + // run the solver clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; -//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); - if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index 62b9ecad..2ba8cd32 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -194,7 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, { Msat_SolverVarBumpActivity( p, pLits[i] ); // Msat_SolverVarBumpActivity( p, pLits[i] ); - p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; +// p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; } } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 5f13694b..091a0c55 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -140,8 +140,8 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra int64 nConflictsOld = p->Stats.nConflicts; int64 nDecisionsOld = p->Stats.nDecisions; - p->pFreq = ALLOC( int, p->nVarsAlloc ); - memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); +// p->pFreq = ALLOC( int, p->nVarsAlloc ); +// memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); if ( vAssumps ) { |