diff options
Diffstat (limited to 'src')
39 files changed, 3935 insertions, 72 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e43ee31b..e0a27f9a 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -209,8 +209,9 @@ struct Abc_Ntk_t_ #define ABC_INFINITY (10000000) // transforming floats into ints and back -static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); } -static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); } +static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); } +static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); } +static inline int Abc_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } // checking the network type static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; } @@ -570,7 +571,7 @@ extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode ); extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames ); extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ); -extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ); +extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); /*=== abcReconv.c ==========================================================*/ extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop ); @@ -600,12 +601,13 @@ extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int n extern char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan ); extern char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan ); extern char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 ); -extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars ); +extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl ); extern char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars ); extern char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl ); extern char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl ); extern char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars ); extern char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars ); +extern char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars ); extern char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars ); extern char * Abc_SopCreateInv( Extra_MmFlex_t * pMan ); extern char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 742c8c8d..2ab3842f 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -93,27 +93,41 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop ) DdNode * bSum, * bCube, * bTemp, * bVar; char * pCube; int nVars, Value, v; + extern int Abc_SopIsExorType( char * pSop ); + // start the cover nVars = Abc_SopGetVarNum(pSop); - // check the logic function of the node bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum ); - Abc_SopForEachCube( pSop, nVars, pCube ) + if ( Abc_SopIsExorType(pSop) ) + { + for ( v = 0; v < nVars; v++ ) + { + bSum = Cudd_bddXor( dd, bTemp = bSum, Cudd_bddIthVar(dd, v) ); Cudd_Ref( bSum ); + Cudd_RecursiveDeref( dd, bTemp ); + } + } + else { - bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); - Abc_CubeForEachVar( pCube, Value, v ) + // check the logic function of the node + Abc_SopForEachCube( pSop, nVars, pCube ) { - if ( Value == '0' ) - bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); - else if ( Value == '1' ) - bVar = Cudd_bddIthVar( dd, v ); - else - continue; - bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); + bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); + else if ( Value == '1' ) + bVar = Cudd_bddIthVar( dd, v ); + else + continue; + bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( dd, bTemp ); + } + bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); + Cudd_Ref( bSum ); Cudd_RecursiveDeref( dd, bTemp ); + Cudd_RecursiveDeref( dd, bCube ); } - bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); Cudd_Ref( bSum ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); } // complement the result if necessary bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) ); @@ -246,16 +260,18 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) ); if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) ) { + if ( fMode == -1 ) // if the phase is not known, write constant 1 + fMode = 1; Vec_StrFill( vCube, nFanins, '-' ); Vec_StrPush( vCube, '\0' ); if ( pMan ) pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 ); else pSop = ALLOC( char, nFanins + 4 ); - if ( bFuncOn == Cudd_ReadLogicZero(dd) ) - sprintf( pSop, "%s 0\n", vCube->pArray ); + if ( bFuncOn == Cudd_ReadOne(dd) ) + sprintf( pSop, "%s %d\n", vCube->pArray, fMode ); else - sprintf( pSop, "%s 1\n", vCube->pArray ); + sprintf( pSop, "%s %d\n", vCube->pArray, !fMode ); return pSop; } diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 53f8c1e9..65cc6e2e 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -342,7 +342,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk ) if ( !Abc_NodeIsConst(pObj) ) { Abc_NtkDupObj( pNtkNew, pObj ); - pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 ); + pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL ); } if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) ) pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy ); diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index dc69f651..4152dd0a 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -156,13 +156,14 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 ) SeeAlso [] ***********************************************************************/ -char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars ) +char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl ) { char * pSop; int i; pSop = Abc_SopStart( pMan, 1, nVars ); for ( i = 0; i < nVars; i++ ) - pSop[i] = '1'; + pSop[i] = '1' - (pfCompl? pfCompl[i] : 0); + pSop[nVars + 1] = '1'; return pSop; } @@ -275,6 +276,26 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars ) /**Function************************************************************* + Synopsis [Starts the multi-input XOR cover (special case).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars ) +{ + char * pSop; + pSop = Abc_SopCreateAnd( pMan, nVars, NULL ); + pSop[nVars+1] = 'x'; + assert( pSop[nVars+2] == '\n' ); + return pSop; +} + +/**Function************************************************************* + Synopsis [Starts the multi-input XNOR cover.] Description [] @@ -402,9 +423,9 @@ int Abc_SopGetVarNum( char * pSop ) int Abc_SopGetPhase( char * pSop ) { int nVars = Abc_SopGetVarNum( pSop ); - if ( pSop[nVars+1] == '0' ) + if ( pSop[nVars+1] == '0' || pSop[nVars+1] == 'n' ) return 0; - if ( pSop[nVars+1] == '1' ) + if ( pSop[nVars+1] == '1' || pSop[nVars+1] == 'x' ) return 1; assert( 0 ); return -1; @@ -453,6 +474,10 @@ void Abc_SopComplement( char * pSop ) *(pCur - 1) = '1'; else if ( *(pCur - 1) == '1' ) *(pCur - 1) = '0'; + else if ( *(pCur - 1) == 'x' ) + *(pCur - 1) = 'n'; + else if ( *(pCur - 1) == 'n' ) + *(pCur - 1) = 'x'; else assert( 0 ); } @@ -474,7 +499,7 @@ bool Abc_SopIsComplement( char * pSop ) char * pCur; for ( pCur = pSop; *pCur; pCur++ ) if ( *pCur == '\n' ) - return (int)(*(pCur - 1) == '0'); + return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n'); assert( 0 ); return 0; } @@ -616,6 +641,27 @@ bool Abc_SopIsOrType( char * pSop ) SeeAlso [] ***********************************************************************/ +int Abc_SopIsExorType( char * pSop ) +{ + char * pCur; + for ( pCur = pSop; *pCur; pCur++ ) + if ( *pCur == '\n' ) + return (int)(*(pCur - 1) == 'x' || *(pCur - 1) == 'n'); + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ bool Abc_SopCheck( char * pSop, int nFanins ) { char * pCubes, * pCubesOld; @@ -638,7 +684,7 @@ bool Abc_SopCheck( char * pSop, int nFanins ) fFound0 = 1; else if ( *pCubes == '1' ) fFound1 = 1; - else + else if ( *pCubes != 'x' && *pCubes != 'n' ) { fprintf( stdout, "Abc_SopCheck: SOP has a strange character in the output part of its cube.\n" ); return 0; diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 8e1615d7..9d95fade 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -76,6 +76,8 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk ) assert( Abc_NtkHasSop(pNtk) ); Abc_NtkForEachNode( pNtk, pNode, i ) { + if ( Abc_NodeIsConst(pNode) ) + continue; assert( pNode->pData ); nCubes += Abc_SopGetCubeNum( pNode->pData ); } @@ -153,6 +155,8 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk ) assert( Abc_NtkIsBddLogic(pNtk) ); Abc_NtkForEachNode( pNtk, pNode, i ) { + if ( Abc_NodeIsConst(pNode) ) + continue; assert( pNode->pData ); nNodes += pNode->pData? Cudd_DagSize( pNode->pData ) : 0; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b6de6cbf..71b76cf6 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -77,6 +77,7 @@ static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -173,6 +174,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 ); Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); + Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); @@ -648,6 +650,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; Abc_Obj_t * pNode; int c; + int fListNodes; int fProfile; pNtk = Abc_FrameReadNet(pAbc); @@ -655,12 +658,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fProfile = 1; + fListNodes = 0; + fProfile = 1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF ) { switch ( c ) { + case 'n': + fListNodes ^= 1; + break; case 'p': fProfile ^= 1; break; @@ -701,12 +708,13 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // process all COs - Abc_NtkPrintLevel( pOut, pNtk, fProfile ); + Abc_NtkPrintLevel( pOut, pNtk, fProfile, fListNodes ); return 0; usage: - fprintf( pErr, "usage: print_level [-ph] <node>\n" ); + fprintf( pErr, "usage: print_level [-nph] <node>\n" ); fprintf( pErr, "\t prints information about node level and cone size\n" ); + fprintf( pErr, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" ); fprintf( pErr, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\tnode : (optional) one node to consider\n"); @@ -732,6 +740,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fVerbose; extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose ); + extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -759,6 +768,11 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + + // print support information + Abc_NtkPrintStrSupports( pNtk ); + return 0; + if ( !Abc_NtkIsComb(pNtk) ) { fprintf( pErr, "This command works only for combinational networks.\n" ); @@ -3649,11 +3663,102 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; + int fVerbose; + int fUseInvs; + 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); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + fUseInvs = 1; + nFaninMax = 128; + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nFaninMax = atoi(argv[util_optind]); + util_optind++; + if ( nFaninMax < 0 ) + goto usage; + break; + case 'i': + fUseInvs ^= 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, "Only works for strashed networks.\n" ); + return 1; + } + + // run the command + pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" ); + fprintf( pErr, "\t specilized AND/OR/EXOR decomposition\n" ); + fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax ); + fprintf( pErr, "\t-i : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk;//, * pNtkRes; + int c; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3676,6 +3781,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Only works for strashed networks.\n" ); + return 1; + } + +// Abc_NtkDeriveEsops( pNtk ); +// Abc_NtkXyz( pNtk, 128, 0, 0, 0 ); + printf( "This command is currently not used.\n" ); + +/* // run the command pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); if ( pNtkRes == NULL ) @@ -3685,6 +3802,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ return 0; usage: @@ -3696,7 +3814,6 @@ usage: - /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 1adbfef7..fed89dbb 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -102,6 +102,42 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica /**Function************************************************************* + Synopsis [Randomizes the node positions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper ) +{ + Abc_Obj_t * pNode1, * pNode2; + int i, Signature; + if ( Vec_PtrSize(vSuper) < 3 ) + return; + pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 ); + pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 ); + if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level ) + return; + // some reordering will be performed + Signature = rand(); + for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- ) + { + pNode1 = Vec_PtrEntry( vSuper, i ); + pNode2 = Vec_PtrEntry( vSuper, i-1 ); + if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level ) + return; + if ( Signature & (1 << (i % 10)) ) + continue; + Vec_PtrWriteEntry( vSuper, i, pNode2 ); + Vec_PtrWriteEntry( vSuper, i-1, pNode1 ); + } +} + +/**Function************************************************************* + Synopsis [Rebalances the multi-input node rooted at pNodeOld.] Description [] @@ -143,6 +179,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ assert( vSuper->nSize > 1 ); while ( vSuper->nSize > 1 ) { + // randomize the node positions +// Abc_NodeBalanceRandomize( vSuper ); + // pull out the last two nodes pNode1 = Vec_PtrPop(vSuper); pNode2 = Vec_PtrPop(vSuper); Abc_VecObjPushUniqueOrderByLevel( vSuper, Abc_AigAnd(pMan, pNode1, pNode2) ); diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index bfc992ef..d59f21a0 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f { Fraig_Params_t * pPars = pParams; Abc_Ntk_t * pNtkNew; - Fraig_Man_t * pMan; + Fraig_Man_t * pMan; // check if EXDC is present if ( fExdc && pNtk->pExdc == NULL ) fExdc = 0, printf( "Warning: Networks has no EXDC.\n" ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 82325619..6791f08c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -79,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) ); } else if ( Abc_NtkHasBdd(pNtk) ) - fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) ); + fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) ); else if ( Abc_NtkHasMapping(pNtk) ) { fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) ); @@ -423,10 +423,26 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile ) +void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes ) { Abc_Obj_t * pNode; - int i, Length; + int i, k, Length; + + if ( fListNodes ) + { + int nLevels; + nLevels = Abc_NtkGetLevelNum(pNtk); + printf( "Nodes by level:\n" ); + for ( i = 0; i <= nLevels; i++ ) + { + printf( "%2d : ", i ); + Abc_NtkForEachNode( pNtk, pNode, k ) + if ( (int)pNode->Level == i ) + printf( " %s", Abc_ObjName(pNode) ); + printf( "\n" ); + } + return; + } // print the delay profile if ( fProfile && Abc_NtkHasMapping(pNtk) ) @@ -716,6 +732,34 @@ void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk ) printf( "\n" ); } +/**Function************************************************************* + + Synopsis [Prints info for each output cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vSupp, * vNodes; + Abc_Obj_t * pObj; + int i; + printf( "Structural support info:\n" ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); + vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); + printf( "%20s : Cone = %5d. Supp = %5d.\n", + Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSupp ); + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index ab594667..b3b30d9a 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -109,6 +109,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); // print stats if ( fVerbose ) Rwr_ManPrintStats( pManRwr ); +// Rwr_ManPrintStatsFile( pManRwr ); // delete the managers Rwr_ManStop( pManRwr ); Cut_ManStop( pManCut ); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 1a35d143..4a65659c 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,8 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ); -static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); +static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ); +static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -57,6 +57,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) // load clauses into the solver clk = clock(); pSat = Abc_NtkMiterSatCreate( pNtk ); + if ( pSat == NULL ) + return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); @@ -69,7 +71,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) { solver_delete( pSat ); // printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return -1; + return 1; } // solve the miter @@ -143,13 +145,19 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) // derive SOPs for both phases of the node Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 ); // add the clauses to the solver - Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ); + if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) ) + { + solver_delete( pSat ); + return NULL; + } } - // add clauses for each PO -// Abc_NtkForEachPo( pNtk, pNode, i ) -// Abc_NodeAddClausesTop( pSat, pNode, vVars ); - - Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ); + // add clauses for the POs + if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) ) + { + solver_delete( pSat ); + return NULL; + } +// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 ); // delete Vec_StrFree( vCube ); @@ -169,7 +177,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) { Abc_Obj_t * pFanin; int i, c, nFanins; @@ -177,6 +185,16 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * nFanins = Abc_ObjFaninNum( pNode ); assert( nFanins == Abc_SopGetVarNum( pSop0 ) ); + + if ( nFanins == 0 ) + { + vVars->nSize = 0; + if ( Abc_SopIsConst1(pSop1) ) + Vec_IntPush( vVars, toLit(pNode->Id) ); + else + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + } // add clauses for the negative phase for ( c = 0; ; c++ ) @@ -195,7 +213,8 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); } Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; } // add clauses for the positive phase @@ -215,8 +234,10 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); } Vec_IntPush( vVars, toLit(pNode->Id) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; } + return 1; } /**Function************************************************************* @@ -230,7 +251,7 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * SeeAlso [] ***********************************************************************/ -void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) { Abc_Obj_t * pFanin; @@ -240,29 +261,33 @@ void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars vVars->nSize = 0; Vec_IntPush( vVars, toLit(pFanin->Id) ); Vec_IntPush( vVars, toLit(pNode->Id) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; vVars->nSize = 0; Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; } else { vVars->nSize = 0; Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); Vec_IntPush( vVars, toLit(pNode->Id) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; vVars->nSize = 0; Vec_IntPush( vVars, toLit(pFanin->Id) ); Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; } vVars->nSize = 0; Vec_IntPush( vVars, toLit(pNode->Id) ); - solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); } diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index d1734d88..72f4215b 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -29,6 +29,7 @@ // static functions static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes ); static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); +static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); extern char * Mio_GateReadSop( void * pGate ); @@ -182,6 +183,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) { int fUseFactor = 1; char * pSop; + extern int Abc_SopIsExorType( char * pSop ); assert( Abc_ObjIsNode(pNode) ); @@ -203,6 +205,10 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) if ( Abc_NodeIsConst(pNode) ) return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) ); + // consider the special case of EXOR function + if ( Abc_SopIsExorType(pSop) ) + return Abc_NodeStrashExor( pNtkNew, pNode, pSop ); + // decide when to use factoring if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) return Abc_NodeStrashFactor( pNtkNew, pNode, pSop ); @@ -254,6 +260,37 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pS /**Function************************************************************* + Synopsis [Strashed n-input XOR function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ) +{ + Abc_Aig_t * pMan = pNtkNew->pManFunc; + Abc_Obj_t * pFanin, * pSum; + int i, nFanins; + // get the number of node's fanins + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum(pSop) ); + // go through the cubes of the node's SOP + pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); + for ( i = 0; i < nFanins; i++ ) + { + pFanin = Abc_ObjFanin( pNode, i ); + pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy ); + } + if ( Abc_SopIsComplement(pSop) ) + pSum = Abc_ObjNot(pSum); + return pSum; +} + +/**Function************************************************************* + Synopsis [Strashes one logic node using its SOP.] Description [] diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index bbaca5a9..f20855ab 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -1245,6 +1245,12 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) } fclose( pFile ); + if ( Abc_NtkIsMappedLogic(pNtk) ) + { + Abc_NtkUnmap(pNtk); + printf( "The current network is unmapped before calling SIS.\n" ); + } + // write out the current network pNetlist = Abc_NtkLogicToNetlist(pNtk); Io_WriteBlif( pNetlist, "_sis_in.blif", 1 ); @@ -1375,6 +1381,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) } fclose( pFile ); + if ( Abc_NtkIsMappedLogic(pNtk) ) + { + Abc_NtkUnmap(pNtk); + printf( "The current network is unmapped before calling MVSIS.\n" ); + } // write out the current network pNetlist = Abc_NtkLogicToNetlist(pNtk); diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index 2f74c2a5..9b7fb49f 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -245,7 +245,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) argc = *argcp; argv = *argvp; stopit = 0; - for ( ; *loop < 20; ( *loop )++ ) + for ( ; *loop < 200; ( *loop )++ ) { if ( argc == 0 ) return 0; diff --git a/src/base/io/io.c b/src/base/io/io.c index 1330d114..69b60000 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -44,6 +44,7 @@ static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -81,6 +82,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 ); } /**Function************************************************************* @@ -1383,6 +1385,69 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + Abc_Ntk_t * pNtk, * pNtkTemp; + char * FileName; + int c; + + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( argc != util_optind + 1 ) + { + goto usage; + } + // get the input file name + FileName = argv[util_optind]; + + // derive the netlist + pNtkTemp = Abc_NtkLogicToNetlist(pNtk); + if ( pNtkTemp == NULL ) + { + fprintf( pAbc->Out, "Writing PLA has failed.\n" ); + return 0; + } + Io_WriteVerilog( pNtkTemp, FileName ); + Abc_NtkDelete( pNtkTemp ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" ); + fprintf( pAbc->Err, "\t write a very special subset of Verilog\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.h b/src/base/io/io.h index cb8678b3..286b570c 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -90,6 +90,8 @@ extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName ); extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost ); /*=== abcWritePla.c ==========================================================*/ extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteVerilog.c ==========================================================*/ +extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 510167a8..d8ad8f71 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -127,7 +127,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], ppNames, nNames ); // assign the cover if ( strcmp(pType, "AND") == 0 ) - Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames) ); + Abc_ObjSetData( pNode, Abc_SopCreateAnd(pNtk->pManFunc, nNames, NULL) ); else if ( strcmp(pType, "OR") == 0 ) Abc_ObjSetData( pNode, Abc_SopCreateOr(pNtk->pManFunc, nNames, NULL) ); else if ( strcmp(pType, "NAND") == 0 ) diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index e23bfdb7..b8a2ed01 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -504,7 +504,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens ) Vec_StrAppend( p->vCubes, vTokens->pArray[0] ); // check the char Char = ((char *)vTokens->pArray[1])[0]; - if ( Char != '0' && Char != '1' ) + if ( Char != '0' && Char != '1' && Char != 'x' && Char != 'n' ) { p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0); sprintf( p->sError, "The output character in the constant cube is wrong." ); diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index 63345fd7..a2a2f527 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -191,7 +191,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p ) Abc_NtkForEachNode( pNtk, pObj, i ) { if ( strncmp( pObj->pData, "And", 3 ) == 0 ) - Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) ); + Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) ); else if ( strncmp( pObj->pData, "Or", 2 ) == 0 ) Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) ); else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 ) diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c new file mode 100644 index 00000000..f56da052 --- /dev/null +++ b/src/base/io/ioWriteVerilog.c @@ -0,0 +1,445 @@ +/**CFile**************************************************************** + + FileName [ioWriteVerilog.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to output a special subset of Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "io.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); +static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); +static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ); +static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros ); +static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk ); +static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Write verilog.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName ) +{ + FILE * pFile; + + if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogCheckNtk(pNtk) ) + { + printf( "Io_WriteVerilog(): Can write Verilog for a very special subset of logic networks.\n" ); + printf( "The current network is not in the subset; writing Verilog is not performed.\n" ); + return; + } + + if ( Abc_NtkLatchNum(pNtk) > 0 ) + printf( "Io_WriteVerilog(): Warning: only combinational portion is being written.\n" ); + + // start the output stream + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName ); + return; + } + + // write the equations for the network + Io_WriteVerilogInt( pFile, pNtk ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Writes verilog.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + // write inputs and outputs + fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n ", Abc_NtkName(pNtk) ); + Io_WriteVerilogPis( pFile, pNtk, 3 ); + fprintf( pFile, ",\n " ); + Io_WriteVerilogPos( pFile, pNtk, 3 ); + fprintf( pFile, " );\n" ); + // write inputs, outputs and wires + fprintf( pFile, " input" ); + Io_WriteVerilogPis( pFile, pNtk, 5 ); + fprintf( pFile, ";\n" ); + fprintf( pFile, " output" ); + Io_WriteVerilogPos( pFile, pNtk, 5 ); + fprintf( pFile, ";\n" ); + fprintf( pFile, " wire" ); + Io_WriteVerilogWires( pFile, pNtk, 4 ); + fprintf( pFile, ";\n" ); + // write the nodes + Io_WriteVerilogNodes( pFile, pNtk ); + // finalize the file + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Writes the primary inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) +{ + Abc_Obj_t * pTerm, * pNet; + int LineLength; + int AddedLength; + int NameCounter; + int i; + + LineLength = Start; + NameCounter = 0; + Abc_NtkForEachCi( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanout0(pTerm); + // get the line length after this name is written + AddedLength = strlen(Abc_ObjName(pNet)) + 2; + if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, "\n " ); + // reset the line length + LineLength = 3; + NameCounter = 0; + } + fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCiNum(pNtk)-1)? "" : "," ); + LineLength += AddedLength; + NameCounter++; + } +} + +/**Function************************************************************* + + Synopsis [Writes the primary outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) +{ + Abc_Obj_t * pTerm, * pNet; + int LineLength; + int AddedLength; + int NameCounter; + int i; + + LineLength = Start; + NameCounter = 0; + Abc_NtkForEachCo( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanin0(pTerm); + // get the line length after this name is written + AddedLength = strlen(Abc_ObjName(pNet)) + 2; + if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, "\n " ); + // reset the line length + LineLength = 3; + NameCounter = 0; + } + fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkCoNum(pNtk)-1)? "" : "," ); + LineLength += AddedLength; + NameCounter++; + } +} + +/**Function************************************************************* + + Synopsis [Writes the wires.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start ) +{ + Abc_Obj_t * pTerm, * pNet; + int LineLength; + int AddedLength; + int NameCounter; + int i, Counter, nNodes; + + // count the number of wires + nNodes = 0; + Abc_NtkForEachNode( pNtk, pTerm, i ) + { + if ( i == 0 ) + continue; + pNet = Abc_ObjFanout0(pTerm); + if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) ) + continue; + nNodes++; + } + + // write the wires + Counter = 0; + LineLength = Start; + NameCounter = 0; + Abc_NtkForEachNode( pNtk, pTerm, i ) + { + if ( i == 0 ) + continue; + pNet = Abc_ObjFanout0(pTerm); + if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) ) + continue; + Counter++; + // get the line length after this name is written + AddedLength = strlen(Abc_ObjName(pNet)) + 2; + if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH ) + { // write the line extender + fprintf( pFile, "\n " ); + // reset the line length + LineLength = 3; + NameCounter = 0; + } + fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," ); + LineLength += AddedLength; + NameCounter++; + } +} + +/**Function************************************************************* + + Synopsis [Writes the wires.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i, nCubes, nFanins, Counter, nDigits, fPadZeros; + char * pName; + extern int Abc_SopIsExorType( char * pSop ); + + nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) ); + Counter = 1; + Abc_NtkForEachNode( pNtk, pObj, i ) + { + nFanins = Abc_ObjFaninNum(pObj); + nCubes = Abc_SopGetCubeNum(pObj->pData); + if ( Abc_SopIsAndType(pObj->pData) ) + pName = "ts_and", fPadZeros = 1; + else if ( Abc_SopIsExorType(pObj->pData) ) + pName = "ts_xor", fPadZeros = 1; + else // if ( Abc_SopIsOrType(pObj->pData) ) + pName = "ts_or", fPadZeros = 0; + + assert( nCubes < 2 ); + if ( nCubes == 0 ) + { + fprintf( pFile, " ts_gnd g%0*d ", nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros ); + } + else if ( nCubes == 1 && nFanins == 0 ) + { + fprintf( pFile, " ts_vdd g%0*d ", nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros ); + } + else if ( nFanins == 1 && Abc_SopIsInv(pObj->pData) ) + { + fprintf( pFile, " ts_inv g%0*d ", nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros ); + } + else if ( nFanins == 1 ) + { + fprintf( pFile, " ts_buf g%0*d ", nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros ); + } + else if ( nFanins <= 4 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 4, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 4, fPadZeros ); + } + else if ( nFanins <= 6 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 6, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 6, fPadZeros ); + } + else if ( nFanins == 7 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 7, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 7, fPadZeros ); + } + else if ( nFanins == 8 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 8, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 8, fPadZeros ); + } + else if ( nFanins <= 16 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 16, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 16, fPadZeros ); + } + else if ( nFanins <= 32 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 32, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 32, fPadZeros ); + } + else if ( nFanins <= 64 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 64, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 64, fPadZeros ); + } + else if ( nFanins <= 128 ) + { + fprintf( pFile, " %s%d g%0*d ", pName, 128, nDigits, Counter++ ); + Io_WriteVerilogArgs( pFile, pObj, 128, fPadZeros ); + } + } +} + +/**Function************************************************************* + + Synopsis [Writes the inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros ) +{ + Abc_Obj_t * pFanin; + int i, Counter = 2; + fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) ); + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + if ( Counter++ % 4 == 0 ) + fprintf( pFile, "\n " ); + fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) ); + } + for ( ; i < nInMax; i++ ) + { + if ( Counter++ % 4 == 0 ) + fprintf( pFile, "\n " ); + fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" ); + } + fprintf( pFile, ");\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + char * pSop; + int i, k, nFanins; + Abc_NtkForEachNode( pNtk, pObj, i ) + { + if ( Abc_SopGetCubeNum(pObj->pData) > 1 ) + { + printf( "Node %s contains a cover with more than one cube.\n", Abc_ObjName(pObj) ); + return 0; + } + nFanins = Abc_ObjFaninNum(pObj); + if ( nFanins < 2 ) + continue; + pSop = pObj->pData; + for ( k = 0; k < nFanins; k++ ) + if ( pSop[k] != '1' ) + { + printf( "Node %s contains a cover with non-positive literals.\n", Abc_ObjName(pObj) ); + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Prepares the name for writing the Verilog file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Io_WriteVerilogGetName( Abc_Obj_t * pObj ) +{ + static char Buffer[20]; + char * pName; + pName = Abc_ObjName(pObj); + if ( pName[0] != '[' ) + return pName; + // replace opening bracket by the escape sign and closing bracket by space + // as a result of this transformation, the length of the name does not change + strcpy( Buffer, pName ); + Buffer[0] = '\\'; + Buffer[strlen(Buffer)-1] = ' '; + return Buffer; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/fpga/fpgaUtils.c b/src/map/fpga/fpgaUtils.c index f4eefa8c..b951fd8f 100644 --- a/src/map/fpga/fpgaUtils.c +++ b/src/map/fpga/fpgaUtils.c @@ -51,11 +51,11 @@ static Fpga_Man_t * s_pMan = NULL; ***********************************************************************/ Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv ) { - Fpga_NodeVec_t * vNodes, * vNodesCo; + Fpga_NodeVec_t * vNodes;//, * vNodesCo; Fpga_Node_t * pNode; int i; // collect the CO nodes by level - vNodesCo = Fpga_MappingOrderCosByLevel( pMan ); +// vNodesCo = Fpga_MappingOrderCosByLevel( pMan ); // start the array vNodes = Fpga_NodeVecAlloc( 100 ); // collect the PIs @@ -66,17 +66,17 @@ Fpga_NodeVec_t * Fpga_MappingDfs( Fpga_Man_t * pMan, int fCollectEquiv ) pNode->fMark0 = 1; } // perform the traversal -// for ( i = 0; i < pMan->nOutputs; i++ ) -// Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv ); - for ( i = 0; i < vNodesCo->nSize; i++ ) - for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 ) - Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv ); + for ( i = 0; i < pMan->nOutputs; i++ ) + Fpga_MappingDfs_rec( Fpga_Regular(pMan->pOutputs[i]), vNodes, fCollectEquiv ); +// for ( i = vNodesCo->nSize - 1; i >= 0 ; i-- ) +// for ( pNode = vNodesCo->pArray[i]; pNode; pNode = (Fpga_Node_t *)pNode->pData0 ) +// Fpga_MappingDfs_rec( pNode, vNodes, fCollectEquiv ); // clean the node marks for ( i = 0; i < vNodes->nSize; i++ ) vNodes->pArray[i]->fMark0 = 0; // for ( i = 0; i < pMan->nOutputs; i++ ) // Fpga_MappingUnmark_rec( Fpga_Regular(pMan->pOutputs[i]) ); - Fpga_NodeVecFree( vNodesCo ); +// Fpga_NodeVecFree( vNodesCo ); return vNodes; } @@ -954,7 +954,7 @@ Fpga_NodeVec_t * Fpga_MappingOrderCosByLevel( Fpga_Man_t * pMan ) Fpga_Node_t * pNode; Fpga_NodeVec_t * vNodes; int i, nLevels; - // get the largest node + // get the largest level of a CO nLevels = Fpga_MappingMaxLevel( pMan ); // allocate the array of nodes vNodes = Fpga_NodeVecAlloc( nLevels + 1 ); diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index 3856c04e..70e1070b 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -129,6 +129,7 @@ extern void Rwr_ManIncTravId( Rwr_Man_t * p ); extern Rwr_Man_t * Rwr_ManStart( bool fPrecompute ); extern void Rwr_ManStop( Rwr_Man_t * p ); extern void Rwr_ManPrintStats( Rwr_Man_t * p ); +extern void Rwr_ManPrintStatsFile( Rwr_Man_t * p ); extern void * Rwr_ManReadDecs( Rwr_Man_t * p ); extern int Rwr_ManReadCompl( Rwr_Man_t * p ); extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time ); diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c index 1d306e7e..115065f5 100644 --- a/src/opt/rwr/rwrMan.c +++ b/src/opt/rwr/rwrMan.c @@ -179,6 +179,29 @@ void Rwr_ManPrintStats( Rwr_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Rwr_ManPrintStatsFile( Rwr_Man_t * p ) +{ + FILE * pTable; + pTable = fopen( "stats.txt", "a+" ); + fprintf( pTable, "%d ", p->nCutsGood ); + fprintf( pTable, "%d ", p->nSubgraphs ); + fprintf( pTable, "%d ", p->nNodesRewritten ); + fprintf( pTable, "%d", p->nNodesGained ); + fprintf( pTable, "\n" ); + fclose( pTable ); +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void * Rwr_ManReadDecs( Rwr_Man_t * p ) { return p->pGraph; diff --git a/src/opt/xyz/module.make b/src/opt/xyz/module.make new file mode 100644 index 00000000..ae7dab0f --- /dev/null +++ b/src/opt/xyz/module.make @@ -0,0 +1,8 @@ +SRC += src/opt/xyz/xyzBuild.c \ + src/opt/xyz/xyzCore.c \ + src/opt/xyz/xyzMan.c \ + src/opt/xyz/xyzMinEsop.c \ + src/opt/xyz/xyzMinMan.c \ + src/opt/xyz/xyzMinSop.c \ + src/opt/xyz/xyzMinUtil.c \ + src/opt/xyz/xyzTest.c diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h new file mode 100644 index 00000000..f18686ff --- /dev/null +++ b/src/opt/xyz/xyz.h @@ -0,0 +1,94 @@ +/**CFile**************************************************************** + + FileName [xyz.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Xyz_Man_t_ Xyz_Man_t; +typedef struct Xyz_Obj_t_ Xyz_Obj_t; + +// storage for node information +struct Xyz_Obj_t_ +{ + Min_Cube_t * pCover[3]; // pos/neg/esop + Vec_Int_t * vSupp; // computed support (all nodes except CIs) +}; + +// storage for additional information +struct Xyz_Man_t_ +{ + // general characteristics + int nFaninMax; // the number of vars + int nCubesMax; // the limit on the number of cubes in the intermediate covers + int nWords; // the number of words + Vec_Int_t * vFanCounts; // fanout counts + Vec_Ptr_t * vObjStrs; // object structures + void * pMemory; // memory for the internal data strctures + Min_Man_t * pManMin; // the cub manager + // arrays to map local variables + Vec_Int_t * vComTo0; // mapping of common variables into first fanin + Vec_Int_t * vComTo1; // mapping of common variables into second fanin + Vec_Int_t * vPairs0; // the first var in each pair of common vars + Vec_Int_t * vPairs1; // the second var in each pair of common vars + Vec_Int_t * vTriv0; // trival support of the first node + Vec_Int_t * vTriv1; // trival support of the second node + // statistics + int nSupps; // supports created + int nSuppsMax; // the maximum number of supports + int nBoundary; // the boundary size + int nNodes; // the number of nodes processed +}; + +static inline Xyz_Obj_t * Abc_ObjGetStr( Abc_Obj_t * pObj ) { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); } + +static inline void Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec ) { Abc_ObjGetStr(pObj)->vSupp = vVec; } +static inline Vec_Int_t * Abc_ObjGetSupp( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->vSupp; } + +static inline void Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; } +static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->pCover[2]; } + +static inline void Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; } +static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol ) { return Abc_ObjGetStr(pObj)->pCover[Pol]; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== xyzBuild.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ); +/*=== xyzCore.c ===========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ); +/*=== xyzMan.c ============================================================*/ +extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ); +extern void Xyz_ManFree( Xyz_Man_t * p ); +extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ); +/*=== xyzTest.c ===========================================================*/ +extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzBuild.c b/src/opt/xyz/xyzBuild.c new file mode 100644 index 00000000..e32721e7 --- /dev/null +++ b/src/opt/xyz/xyzBuild.c @@ -0,0 +1,379 @@ +/**CFile**************************************************************** + + FileName [xyzBuild.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Network construction procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + Vec_Int_t * vLits; + Abc_Obj_t * pNodeNew, * pFanin; + int i, iFanin, Lit; + // create empty cube + if ( pCube->nLits == 0 ) + return Abc_NodeCreateConst1(pNtkNew); + // get the literals of this cube + vLits = Vec_IntAlloc( 10 ); + Min_CubeGetLits( pCube, vLits ); + assert( pCube->nLits == (unsigned)vLits->nSize ); + // create special case when there is only one literal + if ( pCube->nLits == 1 ) + { + iFanin = Vec_IntEntry(vLits,0); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntFree( vLits ); + if ( Lit == 1 )// negative + return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); + return pFanin->pCopy; + } + assert( pCube->nLits > 1 ); + // create the AND cube + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + for ( i = 0; i < vLits->nSize; i++ ) + { + iFanin = Vec_IntEntry(vLits,i); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntWriteEntry( vLits, i, Lit==1 ); + Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); + } + pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); + Vec_IntFree( vLits ); + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; + Vec_Int_t * vSupp; + int Entry, nCubes, i; + + if ( Abc_ObjIsCi(pObj) ) + return pObj->pCopy; + assert( Abc_ObjIsNode(pObj) ); + // skip if already computed + if ( pObj->pCopy ) + return pObj->pCopy; + + // get the support and the cover + vSupp = Abc_ObjGetSupp( pObj ); + pCover = Abc_ObjGetCover2( pObj ); + assert( vSupp ); +/* + if ( pCover && pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 ) + { + printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) ); + Min_CoverWrite( stdout, pCover ); + } +*/ +/* + // print the support of this node + printf( "{ " ); + Vec_IntForEachEntry( vSupp, Entry, i ) + printf( "%d ", Entry ); + printf( "} cubes = %d\n", Min_CoverCountCubes( pCover ) ); +*/ + // process the fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 ); + } + + // for each cube, construct the node + nCubes = Min_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pNodeNew = Abc_NodeCreateConst0(pNtkNew); + else if ( nCubes == 1 ) + pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp ); + else + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Min_CoverForEachCube( pCover, pCube ) + { + pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp ); + Abc_ObjAddFanin( pNodeNew, pFaninNew ); + } + pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); + } +/* + printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level ); + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id ); + } + printf( "\n" ); + Min_CoverWrite( stdout, pCover ); +*/ + pObj->pCopy = pNodeNew; + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // reconstruct the network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 ); +// printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id ); + } + // add the COs + Abc_NtkFinalize( pNtk, pNtkNew ); + Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyzDerive: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + + + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) +{ + assert( pObj->pCopy ); + if ( !fCompl ) + return pObj->pCopy; + if ( pObj->pCopy->pCopy == NULL ) + pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy ); + return pObj->pCopy->pCopy; + } + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp ) +{ + Vec_Int_t * vLits; + Abc_Obj_t * pNodeNew, * pFanin; + int i, iFanin, Lit; + // create empty cube + if ( pCube->nLits == 0 ) + return Abc_NodeCreateConst1(pNtkNew); + // get the literals of this cube + vLits = Vec_IntAlloc( 10 ); + Min_CubeGetLits( pCube, vLits ); + assert( pCube->nLits == (unsigned)vLits->nSize ); + // create special case when there is only one literal + if ( pCube->nLits == 1 ) + { + iFanin = Vec_IntEntry(vLits,0); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntFree( vLits ); +// if ( Lit == 1 )// negative +// return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy ); +// return pFanin->pCopy; + return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ); + } + assert( pCube->nLits > 1 ); + // create the AND cube + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + for ( i = 0; i < vLits->nSize; i++ ) + { + iFanin = Vec_IntEntry(vLits,i); + pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) ); + Lit = Min_CubeGetVar(pCube, iFanin); + assert( Lit == 1 || Lit == 2 ); + Vec_IntWriteEntry( vLits, i, Lit==1 ); +// Abc_ObjAddFanin( pNodeNew, pFanin->pCopy ); + Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) ); + } +// pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray ); + pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL ); + Vec_IntFree( vLits ); + return pNodeNew; +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin; + Vec_Int_t * vSupp; + int Entry, nCubes, i; + + // skip if already computed + if ( pObj->pCopy ) + return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); + assert( Abc_ObjIsNode(pObj) ); + + // get the support and the cover + vSupp = Abc_ObjGetSupp( pObj ); + pCover = Abc_ObjGetCover2( pObj ); + assert( vSupp ); + + // process the fanins + Vec_IntForEachEntry( vSupp, Entry, i ) + { + pFanin = Abc_NtkObj(pObj->pNtk, Entry); + Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 ); + } + + // for each cube, construct the node + nCubes = Min_CoverCountCubes( pCover ); + if ( nCubes == 0 ) + pNodeNew = Abc_NodeCreateConst0(pNtkNew); + else if ( nCubes == 1 ) + pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp ); + else + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Min_CoverForEachCube( pCover, pCube ) + { + pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp ); + Abc_ObjAddFanin( pNodeNew, pFaninNew ); + } + pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes ); + } + + pObj->pCopy = pNodeNew; + return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl ); +} + +/**Function************************************************************* + + Synopsis [Derives the decomposed network.] + + Description [The resulting network contains only pure AND/OR/EXOR gates + and inverters. This procedure is usedful to generate Verilog.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pNodeNew; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // reconstruct the network + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pNodeNew ); + } + // add the COs + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c new file mode 100644 index 00000000..a48f749e --- /dev/null +++ b/src/opt/xyz/xyzCore.c @@ -0,0 +1,697 @@ +/**CFile**************************************************************** + + FileName [xyzCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); +static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); +static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); + +static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); +static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); +static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + Xyz_Man_t * p; + + assert( Abc_NtkIsStrash(pNtk) ); + + // create the manager + p = Xyz_ManAlloc( pNtk, nFaninMax ); + pNtk->pManCut = p; + + // perform mapping + Abc_NtkXyzCovers( p, pNtk, fVerbose ); + + // derive the final network + if ( fUseInvs ) + pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk ); + else + pNtkNew = Abc_NtkXyzDerive( p, pNtk ); + + Xyz_ManFree( p ); + pNtk->pManCut = NULL; + + // make sure that everything is okay + if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkXyz: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Compute the supports.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) +{ + Abc_Obj_t * pObj; + int i, clk = clock(); + + // start the manager + p->vFanCounts = Abc_NtkFanoutCounts(pNtk); + + // set trivial cuts for the constant and the CIs + pObj = Abc_NtkConst1(pNtk); + pObj->fMarkA = 1; + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->fMarkA = 1; + + // perform iterative decomposition + for ( i = 0; ; i++ ) + { + if ( fVerbose ) + printf( "Iter %d : ", i+1 ); + if ( Abc_NtkXyzCoversOne(p, pNtk, fVerbose) ) + break; + } + + // clean the cut-point markers + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkA = 0; + +if ( fVerbose ) +{ +PRT( "Total", clock() - clk ); +} +} + +/**Function************************************************************* + + Synopsis [Compute the supports.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pObj; + Vec_Ptr_t * vBoundary; + int i, clk = clock(); + int Counter = 0; + int fStop = 1; + + // array to collect the nodes in the new boundary + vBoundary = Vec_PtrAlloc( 100 ); + + // start from the COs and mark visited nodes using pObj->fMarkB + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the solved nodes (including the CIs) + pObj = Abc_ObjFanin0(pObj); + if ( pObj->fMarkA ) + { + Counter++; + continue; + } + + // traverse the cone starting from this node + Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + fStop = 0; + else + Counter++; + +/* + printf( "%-15s : ", Abc_ObjName(pObj) ); + printf( "lev = %5d ", pObj->Level ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + { + printf( "\n" ); + continue; + } + printf( "supp = %3d ", Abc_ObjGetSupp(pObj)->nSize ); + printf( "esop = %3d ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); + printf( "\n" ); +*/ + } + Extra_ProgressBarStop( pProgress ); + + // clean visited nodes + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkB = 0; + + // create the new boundary + p->nBoundary = 0; + Vec_PtrForEachEntry( vBoundary, pObj, i ) + { + if ( !pObj->fMarkA ) + { + pObj->fMarkA = 1; + p->nBoundary++; + } + } + Vec_PtrFree( vBoundary ); + +if ( fVerbose ) +{ + printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ", + Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary ); +PRT( "T", clock() - clk ); +} + return fStop; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ) +{ + Abc_Obj_t * pObj0, * pObj1; + // return if the support is already computed + if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) ) + return; + // mark as visited + pObj->fMarkB = 1; + // get the fanins + pObj0 = Abc_ObjFanin0(pObj); + pObj1 = Abc_ObjFanin1(pObj); + // solve for the fanins + Abc_NtkXyzCovers_rec( p, pObj0, vBoundary ); + Abc_NtkXyzCovers_rec( p, pObj1, vBoundary ); + // skip the node that spaced out + if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready + !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready + !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // node's support or covers cannot be computed + { + // save the nodes of the future boundary + if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) ) + Vec_PtrPush( vBoundary, pObj0 ); + if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) ) + Vec_PtrPush( vBoundary, pObj1 ); + return; + } + // consider dropping the fanin supports +// Abc_NodeXyzDropData( p, pObj0 ); +// Abc_NodeXyzDropData( p, pObj1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 ) +{ + Vec_Int_t * vSupp; + int k0, k1; + + assert( vSupp0 && vSupp1 ); + Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 ); + Vec_IntClear( p->vPairs0 ); + Vec_IntClear( p->vPairs1 ); + + vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize ); + for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; ) + { + if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( p->vPairs0, k0 ); + Vec_IntPush( p->vPairs1, k1 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; k1++; + } + else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + k0++; + } + else + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + k1++; + } + } + for ( ; k0 < vSupp0->nSize; k0++ ) + { + Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); + Vec_IntPush( vSupp, vSupp0->pArray[k0] ); + } + for ( ; k1 < vSupp1->nSize; k1++ ) + { + Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); + Vec_IntPush( vSupp, vSupp1->pArray[k1] ); + } +/* + printf( "Zero : " ); + for ( k0 = 0; k0 < vSupp0->nSize; k0++ ) + printf( "%d ", vSupp0->pArray[k0] ); + printf( "\n" ); + + printf( "One : " ); + for ( k1 = 0; k1 < vSupp1->nSize; k1++ ) + printf( "%d ", vSupp1->pArray[k1] ); + printf( "\n" ); + + printf( "Sum : " ); + for ( k0 = 0; k0 < vSupp->nSize; k0++ ) + printf( "%d ", vSupp->pArray[k0] ); + printf( "\n" ); + printf( "\n" ); +*/ + return vSupp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +{ + Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the covers + pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); + pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); + + // complement the first if needed + if ( !Abc_ObjFaninC0(pObj) ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !Abc_ObjFaninC1(pObj) ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; + + // derive and minimize the cover (quit if too large) + if ( !Abc_NodeXyzProductEsop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCover ); + Vec_IntFree( vSupp ); + return 0; + } + + // minimize the cover + Min_EsopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, vSupp->nSize ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCover ); + Vec_IntFree( vSupp ); + return 0; + } + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover2( pObj, pCover ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ) +{ + Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + int fCompl0, fCompl1; + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the complemented attributes + fCompl0 = Abc_ObjFaninC0(pObj); + fCompl1 = Abc_ObjFaninC1(pObj); + + // prepare the positive cover + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); + + // derive and minimize the cover (quit if too large) + if ( !pCover0 || !pCover1 ) + pCoverP = NULL; + else if ( !Abc_NodeXyzProductSop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCoverP ); + pCoverP = NULL; + } + else + { + Min_SopMinimize( p->pManMin ); + pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize ); + // quit if the cover is too large + if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCoverP ); + pCoverP = NULL; + } + } + + // prepare the negative cover + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); + + // derive and minimize the cover (quit if too large) + if ( !pCover0 || !pCover1 ) + pCoverN = NULL; + else if ( !Abc_NodeXyzUnionSop( p, pCover0, pCover1, vSupp->nSize ) ) + { + pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); + Min_CoverRecycle( p->pManMin, pCoverN ); + pCoverN = NULL; + } + else + { + Min_SopMinimize( p->pManMin ); + pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize ); + // quit if the cover is too large + if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCoverN ); + pCoverN = NULL; + } + } + + if ( pCoverP == NULL && pCoverN == NULL ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover( pObj, pCoverP, 0 ); + Abc_ObjSetCover( pObj, pCoverN, 1 ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + int i, Val0, Val1; + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + if ( pCover0 == NULL || pCover1 == NULL ) + return 1; + + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + // go through the support variables of the cubes + for ( i = 0; i < p->vPairs0->nSize; i++ ) + { + Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); + Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); + if ( (Val0 & Val1) == 0 ) + break; + } + // check disjointness + if ( i < p->vPairs0->nSize ) + continue; + + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + + // create the product cube + pCube = Min_CubeAlloc( p->pManMin ); + + // add the literals + pCube->nLits = 0; + for ( i = 0; i < nSupp; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + Val0 = 3; + else + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + + if ( p->vComTo1->pArray[i] == -1 ) + Val1 = 3; + else + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + + if ( (Val0 & Val1) == 3 ) + continue; + + Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); + pCube->nLits++; + } + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + return 1; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + int i, Val0, Val1; + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + if ( pCover0 ) + { + Min_CoverForEachCube( pCover0, pCube0 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo0->nSize; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + continue; + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + if ( Val0 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val0 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + } + if ( pCover1 ) + { + Min_CoverForEachCube( pCover1, pCube1 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo1->nSize; i++ ) + { + if ( p->vComTo1->pArray[i] == -1 ) + continue; + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + if ( Val1 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val1 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes >= p->nCubesMax ) + return 0; + // add the cube to storage + while ( Min_EsopAddCube( p->pManMin, pCube ) ); + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ) +{ + return 1; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h new file mode 100644 index 00000000..22950bfd --- /dev/null +++ b/src/opt/xyz/xyzInt.h @@ -0,0 +1,631 @@ +/**CFile**************************************************************** + + FileName [xyzInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Min_Man_t_ Min_Man_t; +typedef struct Min_Cube_t_ Min_Cube_t; + +struct Min_Man_t_ +{ + int nVars; // the number of vars + int nWords; // the number of words + Extra_MmFixed_t * pMemMan; // memory manager for cubes + // temporary cubes + Min_Cube_t * pOne0; // tautology cube + Min_Cube_t * pOne1; // tautology cube + Min_Cube_t * pTriv0[2]; // trivial cube + Min_Cube_t * pTriv1[2]; // trivial cube + Min_Cube_t * pTemp; // cube for computing the distance + Min_Cube_t * pBubble; // cube used as a separator + // temporary storage for the new cover + int nCubes; // the number of cubes + Min_Cube_t ** ppStore; // storage for cubes by number of literals +}; + +struct Min_Cube_t_ +{ + Min_Cube_t * pNext; // the pointer to the next cube in the cover + unsigned nVars : 10; // the number of variables + unsigned nWords : 12; // the number of machine words + unsigned nLits : 10; // the number of literals in the cube + unsigned uData[1]; // the bit-data for the cube +}; + + +// iterators through the entries in the linked lists of cubes +#define Min_CoverForEachCube( pCover, pCube ) \ + for ( pCube = pCover; \ + pCube; \ + pCube = pCube->pNext ) +#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ + for ( pCube = pCover, \ + pCube2 = pCube? pCube->pNext: NULL; \ + pCube; \ + pCube = pCube2, \ + pCube2 = pCube? pCube->pNext: NULL ) +#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ + for ( pCube = pCover, \ + ppPrev = &(pCover); \ + pCube; \ + ppPrev = &pCube->pNext, \ + pCube = pCube->pNext ) + +// macros to get hold of bits and values in the cubes +static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); } +static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); } +static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); } +static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); } + +/*=== xyzMinEsop.c ==========================================================*/ +extern void Min_EsopMinimize( Min_Man_t * p ); +extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +/*=== xyzMinSop.c ==========================================================*/ +extern void Min_SopMinimize( Min_Man_t * p ); +extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +/*=== xyzMinMan.c ==========================================================*/ +extern Min_Man_t * Min_ManAlloc( int nVars ); +extern void Min_ManClean( Min_Man_t * p, int nSupp ); +extern void Min_ManFree( Min_Man_t * p ); +/*=== xyzMinUtil.c ==========================================================*/ +extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); +extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); +extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); +extern void Min_CoverCheck( Min_Man_t * p ); +extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); +extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); +extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p ) +{ + Min_Cube_t * pCube; + pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan ); + pCube->pNext = NULL; + pCube->nVars = p->nVars; + pCube->nWords = p->nWords; + pCube->nLits = 0; + memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube representing elementary var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl ) +{ + Min_Cube_t * pCube; + pCube = Min_CubeAlloc( p ); + Min_CubeXorBit( pCube, iVar*2+fCompl ); + pCube->nLits = 1; + return pCube; +} + +/**Function************************************************************* + + Synopsis [Creates the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) +{ + Min_Cube_t * pCube; + pCube = Min_CubeAlloc( p ); + memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Recycles the cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube ) +{ + Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); +} + +/**Function************************************************************* + + Synopsis [Recycles the cube cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2; + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube ); +} + + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeCountLits( Min_Cube_t * pCube ) +{ + unsigned uData; + int Count = 0, i, w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Count++; + } + return Count; +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vLits ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vLits, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Counts the number of cubes in the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CoverCountCubes( Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + int Count = 0; + Min_CoverForEachCube( pCover, pCube ) + Count++; + return Count; +} + + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + unsigned uData; + int i; + assert( pCube0->nVars == pCube1->nVars ); + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] & pCube1->uData[i]; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( uData != 0x55555555 ) + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Collects the disjoint variables of the two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars ) +{ + unsigned uData; + int i, w; + Vec_IntClear( vVars ); + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; + uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); + if ( uData == 0 ) + continue; + for ( i = 0; i < 32; i += 2 ) + if ( uData & (1 << i) ) + Vec_IntPush( vVars, w*16 + i/2 ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp ) +{ + unsigned uData; + int i, fFound = 0; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + { + if ( pTemp ) pTemp->uData[i] = 0; + continue; + } + if ( fFound ) + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (uData & (uData-1)) > 0 ) // more than one 1 + return 0; + if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); + fFound = 1; + } + if ( fFound == 0 ) + { + printf( "\n" ); + Min_CubeWrite( stdout, pCube0 ); + Min_CubeWrite( stdout, pCube1 ); + printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are disjoint.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 ) +{ + unsigned uData;//, uData2; + int i, k, Var0 = -1, Var1 = -1; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + { + uData = pCube0->uData[i] ^ pCube1->uData[i]; + if ( uData == 0 ) + continue; + if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s + return 0; + uData = (uData | (uData >> 1)) & 0x55555555; + if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) + return 0; + for ( k = 0; k < 32; k += 2 ) + if ( uData & (1 << k) ) + { + if ( Var0 == -1 ) + Var0 = 16 * i + k/2; + else if ( Var1 == -1 ) + Var1 = 16 * i + k/2; + else + return 0; + } + /* + if ( Var0 >= 0 ) + { + uData &= 0xFFFF; + uData2 = (uData >> 16); + if ( uData && uData2 ) + return 0; + if ( uData ) + { + } + uData }= uData2; + uData &= 0x + } + */ + } + if ( Var0 >= 0 && Var1 >= 0 ) + { + *pVar0 = Var0; + *pVar1 = Var1; + return 1; + } + if ( Var0 == -1 || Var1 == -1 ) + { + printf( "\n" ); + Min_CubeWrite( stdout, pCube0 ); + Min_CubeWrite( stdout, pCube1 ); + printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + Min_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Min_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; + pCube->nLits = Min_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + Min_Cube_t * pCube; + int i; + assert( pCube0->nVars == pCube1->nVars ); + pCube = Min_CubeAlloc( p ); + for ( i = 0; i < p->nWords; i++ ) + pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; + pCube->nLits = Min_CubeCountLits( pCube ); + return pCube; +} + +/**Function************************************************************* + + Synopsis [Makes the produce of two cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( pCube0->uData[i] != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 ) +{ + int i; + for ( i = 0; i < (int)pCube0->nWords; i++ ) + if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + { + pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; + pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); + } +} + + + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2, * pThis; + if ( pCover == NULL ) + { + Min_ManClean( p, p->nVars ); + return; + } + Min_ManClean( p, pCover->nVars ); + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + // go through the linked list + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeRecycle( p, pCube ); + break; + } + if ( pThis != NULL ) + continue; + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + int i; + // check identity + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesAreEqual( pCube, pNew ) ) + return 1; + // check containment + for ( i = 0; i < (int)pNew->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pCube ) + if ( Min_CubeIsContained( pCube, pNew ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Check if the cube is equal or dist1 or contained.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew ) +{ + Min_Cube_t * pCube; + Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) + if ( Min_CubesDistOne( pCube, pNew, NULL ) ) + return pCube; + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMan.c b/src/opt/xyz/xyzMan.c new file mode 100644 index 00000000..844e8c13 --- /dev/null +++ b/src/opt/xyz/xyzMan.c @@ -0,0 +1,144 @@ +/**CFile**************************************************************** + + FileName [xyzMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Decomposition manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax ) +{ + Xyz_Man_t * pMan; + Xyz_Obj_t * pMem; + Abc_Obj_t * pObj; + int i; + assert( pNtk->pManCut == NULL ); + + // start the manager + pMan = ALLOC( Xyz_Man_t, 1 ); + memset( pMan, 0, sizeof(Xyz_Man_t) ); + pMan->nFaninMax = nFaninMax; + pMan->nCubesMax = 2 * pMan->nFaninMax; + pMan->nWords = Abc_BitWordNum( nFaninMax * 2 ); + + // get the cubes + pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax ); + pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax ); + pMan->vPairs0 = Vec_IntAlloc( nFaninMax ); + pMan->vPairs1 = Vec_IntAlloc( nFaninMax ); + pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); + pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); + + // allocate memory for object structures + pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); + memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) ); + // allocate storage for the pointers to the memory + pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) ); + Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL ); + Abc_NtkForEachObj( pNtk, pObj, i ) + Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i ); + // create the cube manager + pMan->pManMin = Min_ManAlloc( nFaninMax ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Xyz_ManFree( Xyz_Man_t * p ) +{ + Vec_Int_t * vSupp; + int i; + for ( i = 0; i < p->vObjStrs->nSize; i++ ) + { + vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp; + if ( vSupp ) Vec_IntFree( vSupp ); + } + + Min_ManFree( p->pManMin ); + Vec_PtrFree( p->vObjStrs ); + Vec_IntFree( p->vFanCounts ); + Vec_IntFree( p->vTriv0 ); + Vec_IntFree( p->vTriv1 ); + Vec_IntFree( p->vComTo0 ); + Vec_IntFree( p->vComTo1 ); + Vec_IntFree( p->vPairs0 ); + Vec_IntFree( p->vPairs1 ); + free( p->pMemory ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Drop the covers at the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj ) +{ + int nFanouts; + assert( p->vFanCounts ); + nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id ); + assert( nFanouts > 0 ); + if ( --nFanouts == 0 ) + { + Vec_IntFree( Abc_ObjGetSupp(pObj) ); + Abc_ObjSetSupp( pObj, NULL ); + Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) ); + Abc_ObjSetCover2( pObj, NULL ); + p->nSupps--; + } + Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c new file mode 100644 index 00000000..114e28a6 --- /dev/null +++ b/src/opt/xyz/xyzMinEsop.c @@ -0,0 +1,277 @@ +/**CFile**************************************************************** + + FileName [xyzMinEsop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [ESOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Min_EsopRewrite( Min_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopMinimize( Min_Man_t * p ) +{ + int nCubesInit, nCubesOld, nIter; + if ( p->nCubes < 3 ) + return; + nIter = 0; + nCubesInit = p->nCubes; + do { + nCubesOld = p->nCubes; + Min_EsopRewrite( p ); + nIter++; + } + while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); + +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of rewriting using distance 2 cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopRewrite( Min_Man_t * p ) +{ + Min_Cube_t * pCube, ** ppPrev; + Min_Cube_t * pThis, ** ppPrevT; + int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld; + int nPairs = 0; + + // insert the bubble before the first cube + p->pBubble->pNext = p->ppStore[0]; + p->ppStore[0] = p->pBubble; + p->pBubble->nLits = 0; + + // go through the cubes + while ( 1 ) + { + // get the index of the bubble + Index = p->pBubble->nLits; + + // find the bubble + Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) + if ( pCube == p->pBubble ) + break; + assert( pCube == p->pBubble ); + + // remove the bubble, get the next cube after the bubble + *ppPrev = p->pBubble->pNext; + pCube = p->pBubble->pNext; + if ( pCube == NULL ) + for ( Index++; Index <= p->nVars; Index++ ) + if ( p->ppStore[Index] ) + { + ppPrev = &(p->ppStore[Index]); + pCube = p->ppStore[Index]; + break; + } + // stop if there is no more cubes + if ( pCube == NULL ) + break; + + // find the first dist2 cube + Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars ) + Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars - 1 ) + Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + // continue if there is no dist2 cube + if ( pThis == NULL ) + { + // insert the bubble after the cube + p->pBubble->pNext = pCube->pNext; + pCube->pNext = p->pBubble; + p->pBubble->nLits = pCube->nLits; + continue; + } + nPairs++; + + // remove the cubes, insert the bubble instead of pCube + *ppPrevT = pThis->pNext; + *ppPrev = p->pBubble; + p->pBubble->pNext = pCube->pNext; + p->pBubble->nLits = pCube->nLits; + p->nCubes -= 2; + + // Exorlink-2: + // A{v00} B{v01} + A{v10} B{v11} = + // A{v00+v10} B{v01} + A{v10} B{v01+v11} = + // A{v00} B{v01+v11} + A{v00+v10} B{v11} + + // save the dist2 parameters + v00 = Min_CubeGetVar( pCube, Var0 ); + v01 = Min_CubeGetVar( pCube, Var1 ); + v10 = Min_CubeGetVar( pThis, Var0 ); + v11 = Min_CubeGetVar( pThis, Var1 ); +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // derive the first pair of resulting cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= (v00 != 3); + pCube->nLits += ((v00 ^ v10) != 3); + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= (v11 != 3); + pThis->nLits += ((v01 ^ v11) != 3); + + // add the cubes + nCubesOld = p->nCubes; + while ( Min_EsopAddCube( p, pCube ) ); + while ( Min_EsopAddCube( p, pThis ) ); + // check if the cubes were absorbed + if ( p->nCubes < nCubesOld + 2 ) + continue; + + // pull out both cubes + assert( pThis == p->ppStore[pThis->nLits] ); + p->ppStore[pThis->nLits] = pThis->pNext; + assert( pCube == p->ppStore[pCube->nLits] ); + p->ppStore[pCube->nLits] = pCube->pNext; + p->nCubes -= 2; + + // derive the second pair of resulting cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits -= ((v00 ^ v10) != 3); + pCube->nLits += (v00 != 3); + Min_CubeXorVar( pCube, Var1, v11 ); + pCube->nLits -= (v01 != 3); + pCube->nLits += ((v01 ^ v11) != 3); + + Min_CubeXorVar( pThis, Var0, v00 ); + pThis->nLits -= (v10 != 3); + pThis->nLits += ((v00 ^ v10) != 3); + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits -= ((v01 ^ v11) != 3); + pThis->nLits += (v11 != 3); + + // add them anyhow + while ( Min_EsopAddCube( p, pCube ) ); + while ( Min_EsopAddCube( p, pThis ) ); + } +// printf( "Pairs = %d ", nPairs ); +} + +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [If the distance one cube is found, returns the transformed + cube. If there is no distance one, adds the given cube to storage. + Do not forget to clean the storage!] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + Min_Cube_t * pThis, ** ppPrev; + // try to find the identical cube + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + *ppPrev = pThis->pNext; + Min_CubeRecycle( p, pCube ); + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 0; + } + } + // find a distance-1 cube if it exists + if ( pCube->nLits < pCube->nVars ) + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits++; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + pCube->nLits--; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + if ( pCube->nLits > 0 ) + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransform( pCube, pThis, p->pTemp ); + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + // add the cube + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c new file mode 100644 index 00000000..423564c1 --- /dev/null +++ b/src/opt/xyz/xyzMinMan.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [xyzMinMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [SOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Man_t * Min_ManAlloc( int nVars ) +{ + Min_Man_t * pMan; + // start the manager + pMan = ALLOC( Min_Man_t, 1 ); + memset( pMan, 0, sizeof(Min_Man_t) ); + pMan->nVars = nVars; + pMan->nWords = Abc_BitWordNum( nVars * 2 ); + pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) ); + // allocate storage for the temporary cover + pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 ); + // create tautology cubes + Min_ManClean( pMan, nVars ); + pMan->pOne0 = Min_CubeAlloc( pMan ); + pMan->pOne1 = Min_CubeAlloc( pMan ); + pMan->pTemp = Min_CubeAlloc( pMan ); + pMan->pBubble = Min_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0; + // create trivial cubes + Min_ManClean( pMan, 1 ); + pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 ); + pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 ); + pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 ); + pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Cleans the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_ManClean( Min_Man_t * p, int nSupp ) +{ + // set the size of the cube manager + p->nVars = nSupp; + p->nWords = Abc_BitWordNum(2*nSupp); + // clean the storage + memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) ); + p->nCubes = 0; +} + +/**Function************************************************************* + + Synopsis [Stops the minimization manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_ManFree( Min_Man_t * p ) +{ + Extra_MmFixedStop ( p->pMemMan, 0 ); + free( p->ppStore ); + free( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c new file mode 100644 index 00000000..1c5951fe --- /dev/null +++ b/src/opt/xyz/xyzMinSop.c @@ -0,0 +1,341 @@ +/**CFile**************************************************************** + + FileName [xyzMinSop.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [SOP manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Min_SopRewrite( Min_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopMinimize( Min_Man_t * p ) +{ + int nCubesInit, nCubesOld, nIter; + if ( p->nCubes < 3 ) + return; + nIter = 0; + nCubesInit = p->nCubes; + do { + nCubesOld = p->nCubes; + Min_SopRewrite( p ); + nIter++; + } + while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); + +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopRewrite( Min_Man_t * p ) +{ + Min_Cube_t * pCube, ** ppPrev; + Min_Cube_t * pThis, ** ppPrevT; + Min_Cube_t * pTemp; + int v00, v01, v10, v11, Var0, Var1, Index; + int nPairs = 0; + + // insert the bubble before the first cube + p->pBubble->pNext = p->ppStore[0]; + p->ppStore[0] = p->pBubble; + p->pBubble->nLits = 0; + + // go through the cubes + while ( 1 ) + { + // get the index of the bubble + Index = p->pBubble->nLits; + + // find the bubble + Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) + if ( pCube == p->pBubble ) + break; + assert( pCube == p->pBubble ); + + // remove the bubble, get the next cube after the bubble + *ppPrev = p->pBubble->pNext; + pCube = p->pBubble->pNext; + if ( pCube == NULL ) + for ( Index++; Index <= p->nVars; Index++ ) + if ( p->ppStore[Index] ) + { + ppPrev = &(p->ppStore[Index]); + pCube = p->ppStore[Index]; + break; + } + // stop if there is no more cubes + if ( pCube == NULL ) + break; + + // find the first dist2 cube + Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + if ( pThis == NULL && Index < p->nVars ) + Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) + if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) + break; + // continue if there is no dist2 cube + if ( pThis == NULL ) + { + // insert the bubble after the cube + p->pBubble->pNext = pCube->pNext; + pCube->pNext = p->pBubble; + p->pBubble->nLits = pCube->nLits; + continue; + } + nPairs++; + + // remove the cubes, insert the bubble instead of pCube + *ppPrevT = pThis->pNext; + *ppPrev = p->pBubble; + p->pBubble->pNext = pCube->pNext; + p->pBubble->nLits = pCube->nLits; + p->nCubes -= 2; + + + // save the dist2 parameters + v00 = Min_CubeGetVar( pCube, Var0 ); + v01 = Min_CubeGetVar( pCube, Var1 ); + v10 = Min_CubeGetVar( pThis, Var0 ); + v11 = Min_CubeGetVar( pThis, Var1 ); + assert( v00 != v10 && v01 != v11 ); + assert( v00 != 3 || v01 != 3 ); + assert( v10 != 3 || v11 != 3 ); + + // skip the case when rewriting is impossible + if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) + continue; + + // if one of them does not have DC lit, move it + if ( v00 != 3 && v01 != 3 ) + { + pTemp = pCube; pCube = pThis; pThis = pTemp; + Index = v00; v00 = v10; v10 = Index; + Index = v01; v01 = v11; v11 = Index; + } + +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // make sure the first cube has first var DC + if ( v00 != 3 ) + { + assert( v01 == 3 ); + Index = Var0; Var0 = Var1; Var1 = Index; + Index = v00; v00 = v01; v01 = Index; + Index = v10; v10 = v11; v11 = Index; + } + + // consider both cases: both have DC lit + if ( v00 == 3 && v11 == 3 ) + { + assert( v01 != 3 && v10 != 3 ); + // try two reduced cubes + + } + else // the first cube has DC lit + { + assert( v01 != 3 && v10 != 3 && v11 != 3 ); + // try reduced and expanded cube + } + } +// printf( "Pairs = %d ", nPairs ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + return 1; +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopDist1Merge( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, * pCubeNew; + int i; + for ( i = p->nVars; i >= 0; i-- ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCube( pCube->pNext, pCube2 ) + { + assert( pCube->nLits == pCube2->nLits ); + if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) + continue; + pCubeNew = Min_CubesXor( p, pCube, pCube2 ); + assert( pCubeNew->nLits == pCube->nLits - 1 ); + pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; + p->ppStore[pCubeNew->nLits] = pCubeNew; + p->nCubes++; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_SopContain( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, ** ppPrev; + int i, k; + for ( i = 0; i <= p->nVars; i++ ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev ) + { + if ( !Min_CubesAreEqual( pCube, pCube2 ) ) + continue; + *ppPrev = pCube2->pNext; + Min_CubeRecycle( p, pCube2 ); + p->nCubes--; + } + for ( k = i + 1; k <= p->nVars; k++ ) + Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev ) + { + if ( !Min_CubeIsContained( pCube, pCube2 ) ) + continue; + *ppPrev = pCube2->pNext; + Min_CubeRecycle( p, pCube2 ); + p->nCubes--; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) +{ + Vec_Int_t * vVars; + Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev; + int Num, Value, i; + + // get the variables + vVars = Vec_IntAlloc( 100 ); + // create the tautology cube + pCover = Min_CubeAlloc( p ); + // sharp it with all cubes + Min_CoverForEachCube( pSharp, pCube ) + Min_CoverForEachCubePrev( pCover, pThis, ppPrev ) + { + if ( Min_CubesDisjoint( pThis, pCube ) ) + continue; + // remember the next pointer + pNext = pThis->pNext; + // get the variables, in which pThis is '-' while pCube is fixed + Min_CoverGetDisjVars( pThis, pCube, vVars ); + // generate the disjoint cubes + pReady = pThis; + Vec_IntForEachEntryReverse( vVars, Num, i ) + { + // correct the literal + Min_CubeXorVar( pReady, vVars->pArray[i], 3 ); + if ( i == 0 ) + break; + // create the new cube and clean this value + Value = Min_CubeGetVar( pReady, vVars->pArray[i] ); + pReady = Min_CubeDup( p, pReady ); + Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value ); + // add to the cover + *ppPrev = pReady; + ppPrev = &pReady->pNext; + } + pThis = pReady; + pThis->pNext = pNext; + } + Vec_IntFree( vVars ); + + // perform dist-1 merge and contain + Min_CoverExpandRemoveEqual( p, pCover ); + Min_SopDist1Merge( p ); + Min_SopContain( p ); + return Min_CoverCollect( p, p->nVars ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c new file mode 100644 index 00000000..0aebb815 --- /dev/null +++ b/src/opt/xyz/xyzMinUtil.c @@ -0,0 +1,225 @@ +/**CFile**************************************************************** + + FileName [xyzMinUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyzInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ) +{ + int i; + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Min_CubeHasBit(pCube, i*2) ) + { + if ( Min_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "-" ); + else + fprintf( pFile, "0" ); + } + else + { + if ( Min_CubeHasBit(pCube, i*2+1) ) + fprintf( pFile, "1" ); + else + fprintf( pFile, "?" ); + } + fprintf( pFile, " 1\n" ); +// fprintf( pFile, " %d\n", pCube->nLits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + Min_CoverForEachCube( pCover, pCube ) + Min_CubeWrite( pFile, pCube ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) +{ + char Buffer[1000]; + Min_Cube_t * pCube; + FILE * pFile; + int i; + sprintf( Buffer, "%s.esop", pName ); + for ( i = strlen(Buffer) - 1; i >= 0; i-- ) + if ( Buffer[i] == '<' || Buffer[i] == '>' ) + Buffer[i] = '_'; + pFile = fopen( Buffer, "w" ); + fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() ); + fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); + fprintf( pFile, ".o %d\n", 1 ); + fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) ); + if ( fEsop ) fprintf( pFile, ".type esop\n" ); + Min_CoverForEachCube( pCover, pCube ) + Min_CubeWrite( pFile, pCube ); + fprintf( pFile, ".e\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Performs one round of rewriting using distance 2 cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverCheck( Min_Man_t * p ) +{ + Min_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + Min_CoverForEachCube( p->ppStore[i], pCube ) + assert( i == (int)pCube->nLits ); +} + + +/**Function************************************************************* + + Synopsis [Converts the cover from the sorted structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ) +{ + Min_Cube_t * pCov = NULL, ** ppTail = &pCov; + Min_Cube_t * pCube, * pCube2; + int i; + for ( i = 0; i <= nSuppSize; i++ ) + { + Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 ) + { + assert( i == (int)pCube->nLits ); + *ppTail = pCube; + ppTail = &pCube->pNext; + } + } + *ppTail = NULL; + return pCov; +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube, * pCube2; + Min_ManClean( p, p->nVars ); + Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) + { + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + } +} + +/**Function************************************************************* + + Synopsis [Sorts the cover in the increasing number of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ) +{ + Min_Cube_t * pCube; + int i, Counter; + if ( pCover == NULL ) + return 0; + // clean the cube + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] = ~((unsigned)0); + // add the bit data + Min_CoverForEachCube( pCover, pCube ) + for ( i = 0; i < (int)pCover->nWords; i++ ) + p->pTemp->uData[i] &= pCube->uData[i]; + // count the vars + Counter = 0; + for ( i = 0; i < (int)pCover->nVars; i++ ) + Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 ); + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c new file mode 100644 index 00000000..6c0a63f3 --- /dev/null +++ b/src/opt/xyz/xyzTest.c @@ -0,0 +1,51 @@ +/**CFile**************************************************************** + + FileName [xyzTest.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Cover manipulation package.] + + Synopsis [Testing procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "xyz.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ) +{ + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 99f1fafe..497087fb 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -71,6 +71,11 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin // start the file pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); + return; + } fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index efc183a3..74503a2b 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -188,7 +188,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c case CSAT_BAND: if ( nofi < 1 ) { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } - pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi ); + pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); break; case CSAT_BNAND: if ( nofi < 1 ) diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 4801e340..673fcad7 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -104,7 +104,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) Fraig_Man_t * p; // set the random seed for simulation - srand( 0xFEEDDEAF ); +// srand( 0xFEEDDEAF ); + srand( 0xDEADCAFE ); // set parameters for equivalence checking if ( pParams == NULL ) diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index e585e8ab..bc60e4e9 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -1049,6 +1049,26 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); + Msat_IntVecClear( p->vProj ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) ); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 92311e48..ed228b33 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra if ( nBackTrackLimit > 0 ) break; // if the runtime limit is exceeded, quit the restart loop - if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) + if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) break; } Msat_SolverCancelUntil( p, 0 ); |