abc70930: src/base/abci/abcDar.c Source File

00001 
00021 #include "abc.h"
00022 #include "aig.h"
00023 #include "dar.h"
00024 #include "cnf.h"
00025 #include "fra.h"
00026 #include "fraig.h"
00027 
00031 
00035 
00047 Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
00048 {
00049     Aig_Man_t * pMan;
00050     Aig_Obj_t * pObjNew;
00051     Abc_Obj_t * pObj;
00052     int i, nNodes, nDontCares;
00053     // make sure the latches follow PIs/POs
00054     if ( fRegisters ) 
00055     { 
00056         assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
00057         Abc_NtkForEachCi( pNtk, pObj, i )
00058             if ( i < Abc_NtkPiNum(pNtk) )
00059                 assert( Abc_ObjIsPi(pObj) );
00060             else
00061                 assert( Abc_ObjIsBo(pObj) );
00062         Abc_NtkForEachCo( pNtk, pObj, i )
00063             if ( i < Abc_NtkPoNum(pNtk) )
00064                 assert( Abc_ObjIsPo(pObj) );
00065             else
00066                 assert( Abc_ObjIsBi(pObj) );
00067         // print warning about initial values
00068         nDontCares = 0;
00069         Abc_NtkForEachLatch( pNtk, pObj, i )
00070             if ( Abc_LatchIsInitDc(pObj) )
00071             {
00072                 Abc_LatchSetInit0(pObj);
00073                 nDontCares++;
00074             }
00075         if ( nDontCares )
00076         {
00077             printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
00078             printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
00079             printf( "Use command \"print_latch\" to see the init values of registers.\n" );
00080             printf( "Use command \"init\" to change the values.\n" );
00081         }
00082     }
00083     // create the manager
00084     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
00085     pMan->pName = Extra_UtilStrsav( pNtk->pName );
00086     // save the number of registers
00087     if ( fRegisters )
00088     {
00089         pMan->nRegs = Abc_NtkLatchNum(pNtk);
00090         pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
00091     }
00092     // transfer the pointers to the basic nodes
00093     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
00094     Abc_NtkForEachCi( pNtk, pObj, i )
00095         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
00096     // complement the 1-values registers
00097     if ( fRegisters )
00098         Abc_NtkForEachLatch( pNtk, pObj, i )
00099             if ( Abc_LatchIsInit1(pObj) )
00100                 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
00101     // perform the conversion of the internal nodes (assumes DFS ordering)
00102 //    pMan->fAddStrash = 1;
00103     Abc_NtkForEachNode( pNtk, pObj, i )
00104     {
00105         pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
00106 //        printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
00107     }
00108     pMan->fAddStrash = 0;
00109     // create the POs
00110     Abc_NtkForEachCo( pNtk, pObj, i )
00111         Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
00112     // complement the 1-valued registers
00113     if ( fRegisters )
00114         Aig_ManForEachLiSeq( pMan, pObjNew, i )
00115             if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
00116                 pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
00117     // remove dangling nodes
00118     if ( nNodes = Aig_ManCleanup( pMan ) )
00119         printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
00120 //Aig_ManDumpVerilog( pMan, "test.v" );
00121     if ( !Aig_ManCheck( pMan ) )
00122     {
00123         printf( "Abc_NtkToDar: AIG check has failed.\n" );
00124         Aig_ManStop( pMan );
00125         return NULL;
00126     }
00127     return pMan;
00128 }
00129 
00141 Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
00142 {
00143     Vec_Ptr_t * vNodes;
00144     Abc_Ntk_t * pNtkNew;
00145     Abc_Obj_t * pObjNew;
00146     Aig_Obj_t * pObj;
00147     int i;
00148 //    assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
00149     // perform strashing
00150     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00151     // transfer the pointers to the basic nodes
00152     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
00153     Aig_ManForEachPi( pMan, pObj, i )
00154         pObj->pData = Abc_NtkCi(pNtkNew, i);
00155     // rebuild the AIG
00156     vNodes = Aig_ManDfs( pMan );
00157     Vec_PtrForEachEntry( vNodes, pObj, i )
00158         if ( Aig_ObjIsBuf(pObj) )
00159             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
00160         else
00161             pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
00162     Vec_PtrFree( vNodes );
00163     // connect the PO nodes
00164     Aig_ManForEachPo( pMan, pObj, i )
00165     {
00166         if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
00167             break;
00168         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
00169     }
00170     // if there are assertions, add them
00171     if ( pMan->nAsserts > 0 )
00172         Aig_ManForEachAssert( pMan, pObj, i )
00173         {
00174             pObjNew = Abc_NtkCreateAssert(pNtkNew);
00175             Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
00176             Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
00177         }
00178     if ( !Abc_NtkCheck( pNtkNew ) )
00179         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
00180     return pNtkNew;
00181 }
00182 
00195 Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
00196 {
00197     Vec_Ptr_t * vNodes;
00198     Abc_Ntk_t * pNtkNew;
00199     Abc_Obj_t * pObjNew, * pLatch;
00200     Aig_Obj_t * pObj, * pObjLo, * pObjLi;
00201     int i;
00202 //    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
00203     // perform strashing
00204     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00205     // transfer the pointers to the basic nodes
00206     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
00207     Aig_ManForEachPiSeq( pMan, pObj, i )
00208         pObj->pData = Abc_NtkCi(pNtkNew, i);
00209     // create as many latches as there are registers in the manager
00210     Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
00211     {
00212         pObjNew = Abc_NtkCreateLatch( pNtkNew );
00213         pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
00214         pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
00215         Abc_ObjAddFanin( pObjNew, pObjLi->pData );
00216         Abc_ObjAddFanin( pObjLo->pData, pObjNew );
00217         Abc_LatchSetInit0( pObjNew );
00218     }
00219     if ( pMan->vFlopNums == NULL )
00220         Abc_NtkAddDummyBoxNames( pNtkNew );
00221     else
00222     {
00223         assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
00224         Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
00225         {
00226             pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
00227             Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
00228             Abc_ObjAssignName( Abc_ObjFanin0(pObjNew),  Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
00229             Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
00230         }
00231     }
00232     // rebuild the AIG
00233     vNodes = Aig_ManDfs( pMan );
00234     Vec_PtrForEachEntry( vNodes, pObj, i )
00235         if ( Aig_ObjIsBuf(pObj) )
00236             pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
00237         else
00238             pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
00239     Vec_PtrFree( vNodes );
00240     // connect the PO nodes
00241     Aig_ManForEachPo( pMan, pObj, i )
00242     {
00243         if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
00244             break;
00245         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
00246     }
00247     // if there are assertions, add them
00248     if ( pMan->nAsserts > 0 )
00249         Aig_ManForEachAssert( pMan, pObj, i )
00250         {
00251             pObjNew = Abc_NtkCreateAssert(pNtkNew);
00252             Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
00253             Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
00254         }
00255     if ( !Abc_NtkCheck( pNtkNew ) )
00256         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
00257     return pNtkNew;
00258 }
00259 
00271 Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
00272 {
00273     Vec_Ptr_t * vNodes;
00274     Abc_Ntk_t * pNtkNew;
00275     Aig_Obj_t * pObj, * pTemp;
00276     int i;
00277     assert( pMan->pEquivs != NULL );
00278     assert( Aig_ManBufNum(pMan) == 0 );
00279     // perform strashing
00280     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00281     // transfer the pointers to the basic nodes
00282     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
00283     Aig_ManForEachPi( pMan, pObj, i )
00284         pObj->pData = Abc_NtkCi(pNtkNew, i);
00285 
00286     // rebuild the AIG
00287     vNodes = Aig_ManDfsChoices( pMan );
00288     Vec_PtrForEachEntry( vNodes, pObj, i )
00289     {
00290         pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
00291         if ( pTemp = pMan->pEquivs[pObj->Id] )
00292         {
00293             Abc_Obj_t * pAbcRepr, * pAbcObj;
00294             assert( pTemp->pData != NULL );
00295             pAbcRepr = pObj->pData;
00296             pAbcObj  = pTemp->pData;
00297             pAbcObj->pData  = pAbcRepr->pData;
00298             pAbcRepr->pData = pAbcObj;
00299         }
00300     }
00301 //printf( "Total = %d.  Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
00302     Vec_PtrFree( vNodes );
00303     // connect the PO nodes
00304     Aig_ManForEachPo( pMan, pObj, i )
00305         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
00306     if ( !Abc_NtkCheck( pNtkNew ) )
00307         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
00308     return pNtkNew;
00309 }
00310 
00322 Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
00323 {
00324     Vec_Ptr_t * vNodes;
00325     Abc_Ntk_t * pNtkNew;
00326     Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
00327     Aig_Obj_t * pObj;
00328     int i;
00329 //    assert( Aig_ManLatchNum(pMan) > 0 );
00330     // perform strashing
00331     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
00332     // transfer the pointers to the basic nodes
00333     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
00334     Aig_ManForEachPi( pMan, pObj, i )
00335         pObj->pData = Abc_NtkPi(pNtkNew, i);
00336     // create latches of the new network
00337     Aig_ManForEachObj( pMan, pObj, i )
00338     {
00339         if ( !Aig_ObjIsLatch(pObj) )
00340             continue;
00341         pObjNew = Abc_NtkCreateLatch( pNtkNew );
00342         pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
00343         pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
00344         Abc_ObjAddFanin( pObjNew, pFaninNew0 );
00345         Abc_ObjAddFanin( pFaninNew1, pObjNew );
00346         Abc_LatchSetInit0( pObjNew );
00347         pObj->pData = Abc_ObjFanout0( pObjNew );
00348     }
00349     Abc_NtkAddDummyBoxNames( pNtkNew );
00350     // rebuild the AIG
00351     vNodes = Aig_ManDfs( pMan );
00352     Vec_PtrForEachEntry( vNodes, pObj, i )
00353     {
00354         // add the first fanin
00355         pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
00356         if ( Aig_ObjIsBuf(pObj) )
00357             continue;
00358         // add the second fanin
00359         pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
00360         // create the new node
00361         if ( Aig_ObjIsExor(pObj) )
00362             pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
00363         else
00364             pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
00365     }
00366     Vec_PtrFree( vNodes );
00367     // connect the PO nodes
00368     Aig_ManForEachPo( pMan, pObj, i )
00369     {
00370         pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
00371         Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
00372     }
00373     // connect the latches
00374     Aig_ManForEachObj( pMan, pObj, i )
00375     {
00376         if ( !Aig_ObjIsLatch(pObj) )
00377             continue;
00378         pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
00379         Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
00380     }
00381     if ( !Abc_NtkCheck( pNtkNew ) )
00382         fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
00383     return pNtkNew;
00384 }
00385 
00397 Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
00398 {
00399     Vec_Int_t * vInits;
00400     Abc_Obj_t * pLatch;
00401     int i;
00402     vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
00403     Abc_NtkForEachLatch( pNtk, pLatch, i )
00404     {
00405         assert( Abc_LatchIsInit1(pLatch) == 0 );
00406         Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
00407     }
00408     return vInits;
00409 }
00410 
00422 void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
00423 {
00424     int fRemove1, fRemove2;
00425     Aig_Man_t * pMan1, * pMan2;
00426     int * pArray;
00427 
00428     fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
00429     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
00430 
00431 
00432     pMan1 = Abc_NtkToDar( pNtk1, 0 );
00433     pMan2 = Abc_NtkToDar( pNtk2, 0 );
00434 
00435     Aig_ManPrintStats( pMan1 );
00436     Aig_ManPrintStats( pMan2 );
00437 
00438 //    pArray = Abc_NtkGetLatchValues(pNtk1);
00439     pArray = NULL;
00440     Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
00441     free( pArray );
00442 
00443 //    pArray = Abc_NtkGetLatchValues(pNtk2);
00444     pArray = NULL;
00445     Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
00446     free( pArray );
00447 
00448     Aig_ManPrintStats( pMan1 );
00449     Aig_ManPrintStats( pMan2 );
00450 
00451     Aig_ManStop( pMan1 );
00452     Aig_ManStop( pMan2 );
00453 
00454 
00455     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
00456     if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
00457 }
00458 
00470 Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
00471 {
00472     Abc_Ntk_t * pNtkAig = NULL;
00473     Aig_Man_t * pMan;
00474     extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
00475 
00476     assert( Abc_NtkIsStrash(pNtk) );
00477     // convert to the AIG manager
00478     pMan = Abc_NtkToDar( pNtk, 0 );
00479     if ( pMan == NULL )
00480         return NULL;
00481 
00482     // perform computation
00483 //    Fra_ManPartitionTest( pMan, 4 );
00484     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00485     Aig_ManStop( pMan );
00486 
00487     // make sure everything is okay
00488     if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
00489     {
00490         printf( "Abc_NtkDar: The network check has failed.\n" );
00491         Abc_NtkDelete( pNtkAig );
00492         return NULL;
00493     }
00494     return pNtkAig;
00495 }
00496 
00497 
00509 Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
00510 {
00511     Fra_Par_t Pars, * pPars = &Pars; 
00512     Abc_Ntk_t * pNtkAig;
00513     Aig_Man_t * pMan, * pTemp;
00514     pMan = Abc_NtkToDar( pNtk, 0 );
00515     if ( pMan == NULL )
00516         return NULL;
00517     Fra_ParamsDefault( pPars );
00518     pPars->nBTLimitNode = nConfLimit;
00519     pPars->fChoicing    = fChoicing;
00520     pPars->fDoSparse    = fDoSparse;
00521     pPars->fSpeculate   = fSpeculate;
00522     pPars->fProve       = fProve;
00523     pPars->fVerbose     = fVerbose;
00524     pMan = Fra_FraigPerform( pTemp = pMan, pPars );
00525     if ( fChoicing )
00526         pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
00527     else
00528         pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00529     Aig_ManStop( pTemp );
00530     Aig_ManStop( pMan );
00531     return pNtkAig;
00532 }
00533 
00545 Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
00546 {
00547     extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
00548     Abc_Ntk_t * pNtkAig;
00549     Aig_Man_t * pMan, * pTemp;
00550     pMan = Abc_NtkToDar( pNtk, 0 );
00551     if ( pMan == NULL )
00552         return NULL;
00553     pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
00554     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00555     Aig_ManStop( pTemp );
00556     Aig_ManStop( pMan );
00557     return pNtkAig;
00558 }
00559 
00571 Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
00572 {
00573     Aig_Man_t * pMan, * pTemp;
00574     Abc_Ntk_t * pNtkAig;
00575     int clk;
00576     assert( Abc_NtkIsStrash(pNtk) );
00577     pMan = Abc_NtkToDar( pNtk, 0 );
00578     if ( pMan == NULL )
00579         return NULL;
00580 //    Aig_ManPrintStats( pMan );
00581 /*
00582 //    Aig_ManSupports( pMan );
00583     {
00584         Vec_Vec_t * vParts;
00585         vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
00586         Vec_VecFree( vParts );
00587     }
00588 */
00589     Dar_ManRewrite( pMan, pPars );
00590 //    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
00591 //    Aig_ManStop( pTemp );
00592 
00593 clk = clock();
00594     pMan = Aig_ManDup( pTemp = pMan, 0 ); 
00595     Aig_ManStop( pTemp );
00596 //PRT( "time", clock() - clk );
00597 
00598 //    Aig_ManPrintStats( pMan );
00599     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00600     Aig_ManStop( pMan );
00601     return pNtkAig;
00602 }
00603 
00615 Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
00616 {
00617     Aig_Man_t * pMan, * pTemp;
00618     Abc_Ntk_t * pNtkAig;
00619     int clk;
00620     assert( Abc_NtkIsStrash(pNtk) );
00621     pMan = Abc_NtkToDar( pNtk, 0 );
00622     if ( pMan == NULL )
00623         return NULL;
00624 //    Aig_ManPrintStats( pMan );
00625 
00626     Dar_ManRefactor( pMan, pPars );
00627 //    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
00628 //    Aig_ManStop( pTemp );
00629 
00630 clk = clock();
00631     pMan = Aig_ManDup( pTemp = pMan, 0 ); 
00632     Aig_ManStop( pTemp );
00633 //PRT( "time", clock() - clk );
00634 
00635 //    Aig_ManPrintStats( pMan );
00636     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00637     Aig_ManStop( pMan );
00638     return pNtkAig;
00639 }
00640 
00652 Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
00653 {
00654     Aig_Man_t * pMan, * pTemp;
00655     Abc_Ntk_t * pNtkAig;
00656     int clk;
00657     assert( Abc_NtkIsStrash(pNtk) );
00658     pMan = Abc_NtkToDar( pNtk, 0 );
00659     if ( pMan == NULL )
00660         return NULL;
00661 //    Aig_ManPrintStats( pMan );
00662 
00663 clk = clock();
00664     pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); 
00665     Aig_ManStop( pTemp );
00666 //PRT( "time", clock() - clk );
00667 
00668 //    Aig_ManPrintStats( pMan );
00669     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00670     Aig_ManStop( pMan );
00671     return pNtkAig;
00672 }
00673 
00685 Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
00686 {
00687     Aig_Man_t * pMan, * pTemp;
00688     Abc_Ntk_t * pNtkAig;
00689     assert( Abc_NtkIsStrash(pNtk) );
00690     pMan = Abc_NtkToDar( pNtk, 0 );
00691     if ( pMan == NULL )
00692         return NULL;
00693     pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
00694     Aig_ManStop( pTemp );
00695     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
00696     Aig_ManStop( pMan );
00697     return pNtkAig;
00698 }
00699 
00711 Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
00712 {
00713     Aig_Man_t * pMan, * pTemp;
00714     Abc_Ntk_t * pNtkAig;
00715     int clk;
00716     assert( Abc_NtkIsStrash(pNtk) );
00717     pMan = Abc_NtkToDar( pNtk, 0 );
00718     if ( pMan == NULL )
00719         return NULL;
00720 //    Aig_ManPrintStats( pMan );
00721 
00722 clk = clock();
00723     pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); 
00724     Aig_ManStop( pTemp );
00725 //PRT( "time", clock() - clk );
00726 
00727 //    Aig_ManPrintStats( pMan );
00728     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00729     Aig_ManStop( pMan );
00730     return pNtkAig;
00731 }
00732 
00744 Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
00745 {
00746     Abc_Ntk_t * pNtkNew;
00747     Abc_Obj_t * pNode, * pNodeNew;
00748     Aig_Obj_t * pObj, * pLeaf;
00749     Cnf_Cut_t * pCut;
00750     Vec_Int_t * vCover;
00751     unsigned uTruth;
00752     int i, k, nDupGates;
00753     // create the new network
00754     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
00755     // make the mapper point to the new network
00756     Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
00757     Abc_NtkForEachCi( pNtk, pNode, i )
00758         Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
00759     // process the nodes in topological order
00760     vCover = Vec_IntAlloc( 1 << 16 );
00761     Vec_PtrForEachEntry( vMapped, pObj, i )
00762     {
00763         // create new node
00764         pNodeNew = Abc_NtkCreateNode( pNtkNew );
00765         // add fanins according to the cut
00766         pCut = pObj->pData;
00767         Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
00768             Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
00769         // add logic function
00770         if ( pCut->nFanins < 5 )
00771         {
00772             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
00773             Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
00774             pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
00775         }
00776         else
00777             pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
00778         // save the node
00779         pObj->pData = pNodeNew;
00780     }
00781     Vec_IntFree( vCover );
00782     // add the CO drivers
00783     Abc_NtkForEachCo( pNtk, pNode, i )
00784     {
00785         pObj = Aig_ManPo(p->pManAig, i);
00786         pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
00787         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
00788     }
00789 
00790     // remove the constant node if not used
00791     pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
00792     if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
00793         Abc_NtkDeleteObj( pNodeNew );
00794     // minimize the node
00795 //    Abc_NtkSweep( pNtkNew, 0 );
00796     // decouple the PO driver nodes to reduce the number of levels
00797     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
00798 //    if ( nDupGates && If_ManReadVerbose(pIfMan) )
00799 //        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
00800     if ( !Abc_NtkCheck( pNtkNew ) )
00801         fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
00802     return pNtkNew;
00803 }
00804 
00816 Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
00817 {
00818     Vec_Ptr_t * vMapped;
00819     Aig_Man_t * pMan;
00820     Cnf_Man_t * pManCnf;
00821     Cnf_Dat_t * pCnf;
00822     Abc_Ntk_t * pNtkNew = NULL;
00823     assert( Abc_NtkIsStrash(pNtk) );
00824 
00825     // convert to the AIG manager
00826     pMan = Abc_NtkToDar( pNtk, 0 );
00827     if ( pMan == NULL )
00828         return NULL;
00829     if ( !Aig_ManCheck( pMan ) )
00830     {
00831         printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
00832         Aig_ManStop( pMan );
00833         return NULL;
00834     }
00835     // perform balance
00836     Aig_ManPrintStats( pMan );
00837 
00838     // derive CNF
00839     pCnf = Cnf_Derive( pMan, 0 );
00840     pManCnf = Cnf_ManRead();
00841 
00842     // write the network for verification
00843     vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
00844     pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
00845     Vec_PtrFree( vMapped );
00846 
00847     // write CNF into a file
00848     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
00849     Cnf_DataFree( pCnf );
00850     Cnf_ClearMemory();
00851 
00852     Aig_ManStop( pMan );
00853     return pNtkNew;
00854 }
00855 
00856 
00868 int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
00869 {
00870     sat_solver * pSat;
00871     Aig_Man_t * pMan;
00872     Cnf_Dat_t * pCnf;
00873     int status, RetValue, clk = clock();
00874     Vec_Int_t * vCiIds;
00875 
00876     assert( Abc_NtkIsStrash(pNtk) );
00877     assert( Abc_NtkLatchNum(pNtk) == 0 );
00878     assert( Abc_NtkPoNum(pNtk) == 1 );
00879 
00880     // conver to the manager
00881     pMan = Abc_NtkToDar( pNtk, 0 );
00882     // derive CNF
00883     pCnf = Cnf_Derive( pMan, 0 );
00884 //    pCnf = Cnf_DeriveSimple( pMan, 0 );
00885     // convert into the SAT solver
00886     pSat = Cnf_DataWriteIntoSolver( pCnf );
00887     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
00888     Aig_ManStop( pMan );
00889     Cnf_DataFree( pCnf );
00890     // solve SAT
00891     if ( pSat == NULL )
00892     {
00893         Vec_IntFree( vCiIds );
00894 //        printf( "Trivially unsat\n" );
00895         return 1;
00896     }
00897 
00898 
00899 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
00900 //    PRT( "Time", clock() - clk );
00901 
00902     // simplify the problem
00903     clk = clock();
00904     status = sat_solver_simplify(pSat);
00905 //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
00906 //    PRT( "Time", clock() - clk );
00907     if ( status == 0 )
00908     {
00909         Vec_IntFree( vCiIds );
00910         sat_solver_delete( pSat );
00911 //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
00912         return 1;
00913     }
00914 
00915     // solve the miter
00916     clk = clock();
00917     if ( fVerbose )
00918         pSat->verbosity = 1;
00919     status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
00920     if ( status == l_Undef )
00921     {
00922 //        printf( "The problem timed out.\n" );
00923         RetValue = -1;
00924     }
00925     else if ( status == l_True )
00926     {
00927 //        printf( "The problem is SATISFIABLE.\n" );
00928         RetValue = 0;
00929     }
00930     else if ( status == l_False )
00931     {
00932 //        printf( "The problem is UNSATISFIABLE.\n" );
00933         RetValue = 1;
00934     }
00935     else
00936         assert( 0 );
00937 //    PRT( "SAT sat_solver time", clock() - clk );
00938 //    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
00939  
00940     // if the problem is SAT, get the counterexample
00941     if ( status == l_True )
00942     {
00943         pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
00944     }
00945     // free the sat_solver
00946     if ( fVerbose )
00947         Sat_SolverPrintStats( stdout, pSat );
00948 //sat_solver_store_write( pSat, "trace.cnf" );
00949 //sat_solver_store_free( pSat );
00950     sat_solver_delete( pSat );
00951     Vec_IntFree( vCiIds );
00952     return RetValue;
00953 }
00954 
00966 Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
00967 {
00968     Fraig_Params_t Params;
00969     Abc_Ntk_t * pNtkAig, * pNtkFraig;
00970     Aig_Man_t * pMan, * pTemp;
00971     int clk = clock();
00972 
00973     // preprocess the miter by fraiging it
00974     // (note that for each functional class, fraiging leaves one representative;
00975     // so fraiging does not reduce the number of functions represented by nodes
00976     Fraig_ParamsSetDefault( &Params );
00977     Params.nBTLimit = 100000;
00978 //    pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
00979     pNtkFraig = Abc_NtkDup( pNtk );
00980 if ( fVerbose ) 
00981 {
00982 PRT( "Initial fraiging time", clock() - clk );
00983 }
00984 
00985     pMan = Abc_NtkToDar( pNtkFraig, 1 );
00986     Abc_NtkDelete( pNtkFraig );
00987     if ( pMan == NULL )
00988         return NULL;
00989 
00990     pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
00991     Aig_ManStop( pTemp );
00992 
00993     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
00994         pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
00995     else
00996         pNtkAig = Abc_NtkFromDar( pNtk, pMan );
00997     Aig_ManStop( pMan );
00998     return pNtkAig;
00999 }
01000 
01012 Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
01013 {
01014     Aig_Man_t * pMan, * pTemp;
01015     Abc_Ntk_t * pNtkAig;
01016     pMan = Abc_NtkToDar( pNtk, 1 );
01017     if ( pMan == NULL )
01018         return NULL;
01019     pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
01020     Aig_ManStop( pTemp );
01021     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
01022         pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
01023     else
01024         pNtkAig = Abc_NtkFromDar( pNtk, pMan );
01025     Aig_ManStop( pMan );
01026     return pNtkAig;
01027 }
01028 
01040 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
01041 {
01042     Aig_Man_t * pMan;
01043     int RetValue;
01044     // derive the AIG manager
01045     pMan = Abc_NtkToDar( pNtk, 1 );
01046     if ( pMan == NULL )
01047     {
01048         printf( "Converting miter into AIG has failed.\n" );
01049         return -1;
01050     }
01051     assert( pMan->nRegs > 0 );
01052     // perform verification
01053     RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
01054     Aig_ManStop( pMan );
01055     return RetValue;
01056 }
01057 
01069 int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
01070 {
01071 //    Fraig_Params_t Params;
01072     Aig_Man_t * pMan;
01073     Abc_Ntk_t * pMiter;//, * pTemp;
01074     int RetValue;
01075 
01076     // get the miter of the two networks
01077     pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
01078     if ( pMiter == NULL )
01079     {
01080         printf( "Miter computation has failed.\n" );
01081         return 0;
01082     }
01083     RetValue = Abc_NtkMiterIsConstant( pMiter );
01084     if ( RetValue == 0 )
01085     {
01086         extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
01087         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
01088         // report the error
01089         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
01090         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
01091         FREE( pMiter->pModel );
01092         Abc_NtkDelete( pMiter );
01093         return 0;
01094     }
01095     if ( RetValue == 1 )
01096     {
01097         Abc_NtkDelete( pMiter );
01098         printf( "Networks are equivalent after structural hashing.\n" );
01099         return 1;
01100     }
01101 
01102     // commented out because something became non-inductive
01103 /*
01104     // preprocess the miter by fraiging it
01105     // (note that for each functional class, fraiging leaves one representative;
01106     // so fraiging does not reduce the number of functions represented by nodes
01107     Fraig_ParamsSetDefault( &Params );
01108     Params.nBTLimit = 100000;
01109     pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
01110     Abc_NtkDelete( pTemp );
01111     RetValue = Abc_NtkMiterIsConstant( pMiter );
01112     if ( RetValue == 0 )
01113     {
01114         extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
01115         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
01116         // report the error
01117         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
01118         Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
01119         FREE( pMiter->pModel );
01120         Abc_NtkDelete( pMiter );
01121         return 0;
01122     }
01123     if ( RetValue == 1 )
01124     {
01125         Abc_NtkDelete( pMiter );
01126         printf( "Networks are equivalent after structural hashing.\n" );
01127         return 1;
01128     }
01129 */
01130     // derive the AIG manager
01131     pMan = Abc_NtkToDar( pMiter, 1 );
01132     Abc_NtkDelete( pMiter );
01133     if ( pMan == NULL )
01134     {
01135         printf( "Converting miter into AIG has failed.\n" );
01136         return -1;
01137     }
01138     assert( pMan->nRegs > 0 );
01139 
01140     // perform verification
01141     RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
01142     Aig_ManStop( pMan );
01143     return RetValue;
01144 }
01145 
01157 Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
01158 {
01159     Abc_Ntk_t * pNtkAig;
01160     Aig_Man_t * pMan;
01161     pMan = Abc_NtkToDar( pNtk, 1 );
01162     if ( pMan == NULL )
01163         return NULL;
01164     Aig_ManSeqCleanup( pMan );
01165     if ( fLatchSweep )
01166     {
01167         if ( pMan->nRegs )
01168             pMan = Aig_ManReduceLaches( pMan, fVerbose );
01169         if ( pMan->nRegs )
01170             pMan = Aig_ManConstReduce( pMan, fVerbose );
01171     }
01172     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
01173     Aig_ManStop( pMan );
01174     return pNtkAig;
01175 }
01176 
01188 Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
01189 {
01190     Abc_Ntk_t * pNtkAig;
01191     Aig_Man_t * pMan, * pTemp;
01192     pMan = Abc_NtkToDar( pNtk, 1 );
01193     if ( pMan == NULL )
01194         return NULL;
01195 //    Aig_ManReduceLachesCount( pMan );
01196 
01197     pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
01198     Aig_ManStop( pTemp );
01199 
01200 //    pMan = Aig_ManReduceLaches( pMan, 1 );
01201 //    pMan = Aig_ManConstReduce( pMan, 1 );
01202 
01203     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
01204     Aig_ManStop( pMan );
01205     return pNtkAig;
01206 }
01207 
01211 
01212