src/base/abci/abcQuant.c File Reference

#include "abc.h"
Include dependency graph for abcQuant.c:

Go to the source code of this file.

Functions

void Abc_NtkSynthesize (Abc_Ntk_t **ppNtk, int fMoreEffort)
int Abc_NtkQuantify (Abc_Ntk_t *pNtk, int fUniv, int iVar, int fVerbose)
Abc_Ntk_t * Abc_NtkTransRel (Abc_Ntk_t *pNtk, int fInputs, int fVerbose)
Abc_Ntk_t * Abc_NtkInitialState (Abc_Ntk_t *pNtk)
Abc_Ntk_t * Abc_NtkSwapVariables (Abc_Ntk_t *pNtk)
Abc_Ntk_t * Abc_NtkReachability (Abc_Ntk_t *pNtkRel, int nIters, int fVerbose)

Function Documentation

Abc_Ntk_t* Abc_NtkInitialState ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Performs one image computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file abcQuant.c.

00248 {
00249     Abc_Ntk_t * pNtkNew;
00250     Abc_Obj_t * pMiter;
00251     int i, nVars = Abc_NtkPiNum(pNtk)/2;
00252     assert( Abc_NtkIsStrash(pNtk) );
00253     // start the new network 
00254     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00255     // compute the all-zero state in terms of the CS variables
00256     pMiter = Abc_AigConst1(pNtkNew);
00257     for ( i = 0; i < nVars; i++ )
00258         pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) );
00259     // add the PO
00260     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
00261     return pNtkNew;
00262 }

int Abc_NtkQuantify ( Abc_Ntk_t *  pNtk,
int  fUniv,
int  iVar,
int  fVerbose 
)

Function*************************************************************

Synopsis [Existentially quantifies one variable.]

Description []

SideEffects [This procedure creates dangling nodes in the AIG.]

SeeAlso []

Definition at line 75 of file abcQuant.c.

00076 {
00077     Vec_Ptr_t * vNodes;
00078     Abc_Obj_t * pObj, * pNext, * pFanin;
00079     int i;
00080     assert( Abc_NtkIsStrash(pNtk) );
00081     assert( iVar < Abc_NtkCiNum(pNtk) );
00082 
00083     // collect the internal nodes
00084     pObj = Abc_NtkCi( pNtk, iVar );
00085     vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 );
00086 
00087     // assign the cofactors of the CI node to be constants
00088     pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) ); 
00089     pObj->pData = Abc_AigConst1(pNtk); 
00090 
00091     // quantify the nodes
00092     Vec_PtrForEachEntry( vNodes, pObj, i )
00093     {
00094         for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj )
00095         {
00096             pFanin = Abc_ObjFanin0(pObj);
00097             if ( !Abc_NodeIsTravIdCurrent(pFanin) )
00098                 pFanin->pCopy = pFanin->pData = pFanin;
00099             pFanin = Abc_ObjFanin1(pObj);
00100             if ( !Abc_NodeIsTravIdCurrent(pFanin) )
00101                 pFanin->pCopy = pFanin->pData = pFanin;
00102             pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00103             pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) );
00104         }
00105     }
00106     Vec_PtrFree( vNodes );
00107 
00108     // update the affected COs
00109     Abc_NtkForEachCo( pNtk, pObj, i )
00110     {
00111         if ( !Abc_NodeIsTravIdCurrent(pObj) )
00112             continue;
00113         pFanin = Abc_ObjFanin0(pObj);
00114         // get the result of quantification
00115         if ( fUniv )
00116             pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
00117         else
00118             pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
00119         pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
00120         if ( Abc_ObjRegular(pNext) == pFanin )
00121             continue;
00122         // update the fanins of the CO
00123         Abc_ObjPatchFanin( pObj, pFanin, pNext );
00124 //        if ( Abc_ObjFanoutNum(pFanin) == 0 )
00125 //            Abc_AigDeleteNode( pNtk->pManFunc, pFanin );
00126     }
00127 
00128     // make sure the node has no fanouts
00129 //    pObj = Abc_NtkCi( pNtk, iVar );
00130 //    assert( Abc_ObjFanoutNum(pObj) == 0 );
00131     return 1;
00132 }

Abc_Ntk_t* Abc_NtkReachability ( Abc_Ntk_t *  pNtkRel,
int  nIters,
int  fVerbose 
)

Function*************************************************************

Synopsis [Performs reachability analisys.]

Description [Assumes that the input is the transition relation.]

SideEffects []

SeeAlso []

Definition at line 312 of file abcQuant.c.

00313 {
00314     Abc_Obj_t * pObj;
00315     Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
00316     int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
00317     int fFixedPoint = 0;
00318     int fSynthesis  = 1;
00319     int fMoreEffort = 1;
00320 
00321     assert( Abc_NtkIsStrash(pNtkRel) );
00322     assert( Abc_NtkLatchNum(pNtkRel) == 0 );
00323     assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 );
00324 
00325     // compute the network composed of the initial states
00326     pNtkFront = Abc_NtkInitialState( pNtkRel );
00327     pNtkReached = Abc_NtkDup( pNtkFront );
00328 //Abc_NtkShow( pNtkReached, 0, 0, 0 );
00329 
00330 //    if ( fVerbose )
00331 //        printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
00332 
00333     // perform iterations of reachability analysis
00334     nNodesPrev = Abc_NtkNodeNum(pNtkFront);
00335     nVars = Abc_NtkPiNum(pNtkRel)/2;
00336     for ( i = 0; i < nIters; i++ )
00337     {
00338         clk = clock();
00339         // get the set of next states
00340         pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 );
00341         Abc_NtkDelete( pNtkFront );
00342         // quantify the current state variables
00343         for ( v = 0; v < nVars; v++ )
00344         {
00345             Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
00346             if ( fSynthesis && (v % 3 == 2) )
00347             {
00348                 Abc_NtkCleanData( pNtkNext );
00349                 Abc_AigCleanup( pNtkNext->pManFunc );
00350                 Abc_NtkSynthesize( &pNtkNext, fMoreEffort );
00351             }
00352         }
00353         Abc_NtkCleanData( pNtkNext );
00354         Abc_AigCleanup( pNtkNext->pManFunc );
00355         if ( fSynthesis )
00356             Abc_NtkSynthesize( &pNtkNext, 1 );
00357         // map the next states into the current states
00358         pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
00359         Abc_NtkDelete( pNtkTemp );
00360         // check the termination condition
00361         if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) )
00362         {
00363             fFixedPoint = 1;
00364             printf( "Fixed point is reached!\n" );
00365             Abc_NtkDelete( pNtkNext );
00366             break;
00367         }
00368         // compute new front
00369         pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 );
00370         Abc_NtkDelete( pNtkNext );
00371         // add the reached states
00372         pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 );
00373         Abc_NtkDelete( pNtkTemp );
00374         // compress the size of Front
00375         nNodesOld = Abc_NtkNodeNum(pNtkFront);
00376         if ( fSynthesis )
00377         {
00378             Abc_NtkSynthesize( &pNtkFront, fMoreEffort );
00379             Abc_NtkSynthesize( &pNtkReached, fMoreEffort );
00380         }
00381         nNodesNew = Abc_NtkNodeNum(pNtkFront);
00382         // print statistics
00383         if ( fVerbose )
00384         {
00385             printf( "I = %3d : Reach = %6d  Fr = %6d  FrM = %6d  %7.2f %%   ", 
00386                 i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesPrev );
00387             PRT( "T", clock() - clk );
00388         }
00389         nNodesPrev = Abc_NtkNodeNum(pNtkFront);
00390     }
00391     if ( !fFixedPoint )
00392         fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
00393 
00394     // complement the output to represent the set of unreachable states
00395     Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
00396 
00397     // remove next state variables
00398     for ( i = 2*nVars - 1; i >= nVars; i-- )
00399     {
00400         pObj = Abc_NtkPi( pNtkReached, i );
00401         assert( Abc_ObjFanoutNum(pObj) == 0 );
00402         Abc_NtkDeleteObj( pObj );
00403     }
00404 
00405     // check consistency of the network
00406     if ( !Abc_NtkCheck( pNtkReached ) )
00407     {
00408         printf( "Abc_NtkReachability: The network check has failed.\n" );
00409         Abc_NtkDelete( pNtkReached );
00410         return NULL;
00411     }
00412     return pNtkReached;
00413 }

Abc_Ntk_t* Abc_NtkSwapVariables ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Swaps current state and next state variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file abcQuant.c.

00276 {
00277     Abc_Ntk_t * pNtkNew;
00278     Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1;
00279     int i, nVars = Abc_NtkPiNum(pNtk)/2;
00280     assert( Abc_NtkIsStrash(pNtk) );
00281     // start the new network 
00282     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
00283     // update the PIs
00284     for ( i = 0; i < nVars; i++ )
00285     {
00286         pObj0 = Abc_NtkPi( pNtk, i );
00287         pObj1 = Abc_NtkPi( pNtk, i+nVars );
00288         pMiter = pObj0->pCopy;
00289         pObj0->pCopy = pObj1->pCopy;
00290         pObj1->pCopy = pMiter;
00291     }
00292     // restrash
00293     Abc_NtkForEachNode( pNtk, pObj, i )
00294         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00295     // add the PO
00296     pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) );
00297     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
00298     return pNtkNew;
00299 }

void Abc_NtkSynthesize ( Abc_Ntk_t **  ppNtk,
int  fMoreEffort 
)

CFile****************************************************************

FileName [abcQuant.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [AIG-based variable quantification.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Performs fast synthesis.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file abcQuant.c.

00043 {
00044     Abc_Ntk_t * pNtk, * pNtkTemp;
00045 
00046     pNtk = *ppNtk;
00047 
00048     Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00049     Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00050     pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00051     Abc_NtkDelete( pNtkTemp );
00052 
00053     if ( fMoreEffort )
00054     {
00055         Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
00056         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
00057         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
00058         Abc_NtkDelete( pNtkTemp );
00059     }
00060 
00061     *ppNtk = pNtk;
00062 }

Abc_Ntk_t* Abc_NtkTransRel ( Abc_Ntk_t *  pNtk,
int  fInputs,
int  fVerbose 
)

Function*************************************************************

Synopsis [Constructs the transition relation.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file abcQuant.c.

00146 {
00147     char Buffer[1000];
00148     Vec_Ptr_t * vPairs;
00149     Abc_Ntk_t * pNtkNew;
00150     Abc_Obj_t * pObj, * pMiter;
00151     int i, nLatches;
00152     int fSynthesis = 1;
00153 
00154     assert( Abc_NtkIsStrash(pNtk) );
00155     assert( Abc_NtkLatchNum(pNtk) );
00156     nLatches = Abc_NtkLatchNum(pNtk);
00157     // start the network
00158     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
00159     // duplicate the name and the spec
00160     sprintf( Buffer, "%s_TR", pNtk->pName );
00161     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
00162 //    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
00163     Abc_NtkCleanCopy( pNtk );
00164     // create current state variables
00165     Abc_NtkForEachLatchOutput( pNtk, pObj, i )
00166     {
00167         pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
00168         Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
00169     }
00170     // create next state variables
00171     Abc_NtkForEachLatchInput( pNtk, pObj, i )
00172         Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
00173     // create PI variables
00174     Abc_NtkForEachPi( pNtk, pObj, i )
00175         Abc_NtkDupObj( pNtkNew, pObj, 1 );
00176     // create the PO
00177     Abc_NtkCreatePo( pNtkNew );
00178     // restrash the nodes (assuming a topological order of the old network)
00179     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
00180     Abc_NtkForEachNode( pNtk, pObj, i )
00181         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00182     // create the function of the primary output
00183     assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
00184     vPairs = Vec_PtrAlloc( 2*nLatches );
00185     Abc_NtkForEachLatchInput( pNtk, pObj, i )
00186     {
00187         Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
00188         Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
00189     }
00190     pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
00191     Vec_PtrFree( vPairs );
00192     // add the primary output
00193     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
00194     Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
00195 
00196     // quantify inputs
00197     if ( fInputs )
00198     {
00199         assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
00200         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
00201 //        for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
00202         {
00203             Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
00204 //            if ( fSynthesis && (i % 3 == 2) )
00205             if ( fSynthesis  )
00206             {
00207                 Abc_NtkCleanData( pNtkNew );
00208                 Abc_AigCleanup( pNtkNew->pManFunc );
00209                 Abc_NtkSynthesize( &pNtkNew, 1 );
00210             }
00211 //            printf( "Var = %3d. Nodes = %6d. ", Abc_NtkPiNum(pNtkNew) - 1 - i, Abc_NtkNodeNum(pNtkNew) );
00212 //            printf( "Var = %3d. Nodes = %6d. ", i - 2*nLatches, Abc_NtkNodeNum(pNtkNew) );
00213         }
00214 //        printf( "\n" );
00215         Abc_NtkCleanData( pNtkNew );
00216         Abc_AigCleanup( pNtkNew->pManFunc );
00217         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
00218         {
00219             pObj = Abc_NtkPi( pNtkNew, i );
00220             assert( Abc_ObjFanoutNum(pObj) == 0 );
00221             Abc_NtkDeleteObj( pObj );
00222         }
00223     }
00224 
00225     // check consistency of the network
00226     if ( !Abc_NtkCheck( pNtkNew ) )
00227     {
00228         printf( "Abc_NtkTransRel: The network check has failed.\n" );
00229         Abc_NtkDelete( pNtkNew );
00230         return NULL;
00231     }
00232     return pNtkNew;
00233 }

Generated on Tue Jan 5 12:18:40 2010 for abc70930 by  doxygen 1.6.1