src/base/abci/abcUnreach.c File Reference

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

Go to the source code of this file.

Functions

static DdNode * Abc_NtkTransitionRelation (DdManager *dd, Abc_Ntk_t *pNtk, int fVerbose)
static DdNode * Abc_NtkInitStateAndVarMap (DdManager *dd, Abc_Ntk_t *pNtk, int fVerbose)
static DdNode * Abc_NtkComputeUnreachable (DdManager *dd, Abc_Ntk_t *pNtk, DdNode *bRelation, DdNode *bInitial, bool fVerbose)
static Abc_Ntk_t * Abc_NtkConstructExdc (DdManager *dd, Abc_Ntk_t *pNtk, DdNode *bUnreach)
int Abc_NtkExtractSequentialDcs (Abc_Ntk_t *pNtk, bool fVerbose)

Function Documentation

DdNode * Abc_NtkComputeUnreachable ( DdManager *  dd,
Abc_Ntk_t *  pNtk,
DdNode *  bTrans,
DdNode *  bInitial,
bool  fVerbose 
) [static]

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

Synopsis [Computes the set of unreachable states.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file abcUnreach.c.

00221 {
00222     DdNode * bRelation, * bReached, * bCubeCs;
00223     DdNode * bCurrent, * bNext, * bTemp;
00224     int nIters, nMints;
00225 
00226     // perform reachability analisys
00227     bCurrent  = bInitial;   Cudd_Ref( bCurrent );
00228     bReached  = bInitial;   Cudd_Ref( bReached );
00229     bRelation = bTrans;     Cudd_Ref( bRelation );
00230     bCubeCs   = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
00231     for ( nIters = 1; ; nIters++ )
00232     {
00233         // compute the next states
00234         bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs );  Cudd_Ref( bNext );
00235         Cudd_RecursiveDeref( dd, bCurrent );
00236         // remap these states into the current state vars
00237         bNext = Cudd_bddVarMap( dd, bTemp = bNext );                      Cudd_Ref( bNext );
00238         Cudd_RecursiveDeref( dd, bTemp );
00239         // check if there are any new states
00240         if ( Cudd_bddLeq( dd, bNext, bReached ) )
00241             break;
00242         // get the new states
00243         bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );          Cudd_Ref( bCurrent );
00244         // minimize the new states with the reached states
00245 //        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
00246 //        Cudd_RecursiveDeref( dd, bTemp );
00247         // add to the reached states
00248         bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );             Cudd_Ref( bReached );
00249         Cudd_RecursiveDeref( dd, bTemp );
00250         Cudd_RecursiveDeref( dd, bNext );
00251         // minimize the transition relation
00252 //        bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation );
00253 //        Cudd_RecursiveDeref( dd, bTemp );
00254     }
00255     Cudd_RecursiveDeref( dd, bRelation );
00256     Cudd_RecursiveDeref( dd, bCubeCs );
00257     Cudd_RecursiveDeref( dd, bNext );
00258     // report the stats
00259     if ( fVerbose )
00260     {
00261         nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
00262         fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
00263         fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
00264     }
00265 //PRB( dd, bReached );
00266     Cudd_Deref( bReached );
00267     return Cudd_Not( bReached );
00268 }

Abc_Ntk_t * Abc_NtkConstructExdc ( DdManager *  dd,
Abc_Ntk_t *  pNtk,
DdNode *  bUnreach 
) [static]

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

Synopsis [Creates the EXDC network.]

Description [The set of unreachable states depends on CS variables.]

SideEffects []

SeeAlso []

Definition at line 281 of file abcUnreach.c.

00282 {
00283     Abc_Ntk_t * pNtkNew;
00284     Abc_Obj_t * pNode, * pNodeNew;
00285     int * pPermute;
00286     int i;
00287 
00288     // start the new network
00289     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
00290     pNtkNew->pName = Extra_UtilStrsav( "exdc" );
00291     pNtkNew->pSpec = NULL;
00292 
00293     // create PIs corresponding to LOs
00294     Abc_NtkForEachLatchOutput( pNtk, pNode, i )
00295         Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL );
00296     // cannot ADD POs here because pLatch->pCopy point to the PIs
00297 
00298     // create a new node
00299     pNodeNew = Abc_NtkCreateNode(pNtkNew);
00300     // add the fanins corresponding to latch outputs
00301     Abc_NtkForEachLatchOutput( pNtk, pNode, i )
00302         Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
00303 
00304     // create the logic function
00305     pPermute = ALLOC( int, dd->size );
00306     for ( i = 0; i < dd->size; i++ )
00307         pPermute[i] = -1;
00308     Abc_NtkForEachLatch( pNtk, pNode, i )
00309         pPermute[Abc_NtkPiNum(pNtk) + i] = i;
00310     // remap the functions
00311     pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute );   Cudd_Ref( pNodeNew->pData );
00312     free( pPermute );
00313     Abc_NodeMinimumBase( pNodeNew );
00314 
00315     // for each CO, create PO (skip POs equal to CIs because of name conflict)
00316     Abc_NtkForEachPo( pNtk, pNode, i )
00317         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
00318             Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
00319     Abc_NtkForEachLatchInput( pNtk, pNode, i )
00320         Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
00321 
00322     // link to the POs of the network 
00323     Abc_NtkForEachPo( pNtk, pNode, i )
00324         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
00325             Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
00326     Abc_NtkForEachLatchInput( pNtk, pNode, i )
00327         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
00328 
00329     // remove the extra nodes
00330     Abc_AigCleanup( pNtkNew->pManFunc );
00331 
00332     // fix the problem with complemented and duplicated CO edges
00333     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
00334 
00335     // transform the network to the SOP representation
00336     if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
00337     {
00338         printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
00339         return NULL;
00340     }
00341     return pNtkNew;
00342 //    return NULL;
00343 }

int Abc_NtkExtractSequentialDcs ( Abc_Ntk_t *  pNtk,
bool  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Extracts sequential DCs of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file abcUnreach.c.

00048 {
00049     int fReorder = 1;
00050     DdManager * dd;
00051     DdNode * bRelation, * bInitial, * bUnreach;
00052 
00053     // remove EXDC network if present
00054     if ( pNtk->pExdc )
00055     {
00056         Abc_NtkDelete( pNtk->pExdc );
00057         pNtk->pExdc = NULL; 
00058     }
00059 
00060     // compute the global BDDs of the latches
00061     dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
00062     if ( dd == NULL )
00063         return 0;
00064     if ( fVerbose )
00065         printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
00066 
00067     // create the transition relation (dereferenced global BDDs)
00068     bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose );              Cudd_Ref( bRelation );
00069     // create the initial state and the variable map
00070     bInitial  = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose );              Cudd_Ref( bInitial );
00071     // compute the unreachable states
00072     bUnreach  = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose );   Cudd_Ref( bUnreach );
00073     Cudd_RecursiveDeref( dd, bRelation );
00074     Cudd_RecursiveDeref( dd, bInitial );
00075 
00076     // reorder and disable reordering
00077     if ( fReorder )
00078     {
00079         if ( fVerbose )
00080             fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) );
00081         Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
00082         Cudd_AutodynDisable( dd );
00083         if ( fVerbose )
00084             fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) );
00085     }
00086 
00087     // allocate ZDD variables
00088     Cudd_zddVarsFromBddVars( dd, 2 );
00089     // create the EXDC network representing the unreachable states
00090     if ( pNtk->pExdc )
00091         Abc_NtkDelete( pNtk->pExdc );
00092     pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
00093     Cudd_RecursiveDeref( dd, bUnreach );
00094     Extra_StopManager( dd );
00095 //    pNtk->pManGlob = NULL;
00096 
00097     // make sure that everything is okay
00098     if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) )
00099     {
00100         printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
00101         Abc_NtkDelete( pNtk->pExdc );
00102         return 0;
00103     }
00104     return 1;
00105 }

DdNode * Abc_NtkInitStateAndVarMap ( DdManager *  dd,
Abc_Ntk_t *  pNtk,
int  fVerbose 
) [static]

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

Synopsis [Computes the initial state and sets up the variable map.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file abcUnreach.c.

00182 {
00183     DdNode ** pbVarsX, ** pbVarsY;
00184     DdNode * bTemp, * bProd, * bVar;
00185     Abc_Obj_t * pLatch;
00186     int i;
00187 
00188     // set the variable mapping for Cudd_bddVarMap()
00189     pbVarsX = ALLOC( DdNode *, dd->size );
00190     pbVarsY = ALLOC( DdNode *, dd->size );
00191     bProd = b1;         Cudd_Ref( bProd );
00192     Abc_NtkForEachLatch( pNtk, pLatch, i )
00193     {
00194         pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
00195         pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
00196         // get the initial value of the latch
00197         bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
00198         bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
00199         Cudd_RecursiveDeref( dd, bTemp ); 
00200     }
00201     Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
00202     FREE( pbVarsX );
00203     FREE( pbVarsY );
00204 
00205     Cudd_Deref( bProd );
00206     return bProd;
00207 }

DdNode * Abc_NtkTransitionRelation ( DdManager *  dd,
Abc_Ntk_t *  pNtk,
int  fVerbose 
) [static]

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

FileName [abcUnreach.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Computes unreachable states for small benchmarks.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] DECLARATIONS ///

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

Synopsis [Computes the transition relation of the network.]

Description [Assumes that the global BDDs are computed.]

SideEffects []

SeeAlso []

Definition at line 118 of file abcUnreach.c.

00119 {
00120     DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs;
00121     Abc_Obj_t * pNode;
00122     int fReorder = 1;
00123     int i;
00124 
00125     // extand the BDD manager to represent NS variables
00126     assert( dd->size == Abc_NtkCiNum(pNtk) );
00127     Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
00128 
00129     // enable reordering
00130     if ( fReorder )
00131         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
00132     else
00133         Cudd_AutodynDisable( dd );
00134 
00135     // compute the transition relation
00136     bRel = b1;   Cudd_Ref( bRel );
00137     Abc_NtkForEachLatch( pNtk, pNode, i )
00138     {
00139         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
00140 //        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
00141         bProd = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( bProd );
00142         bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );                 Cudd_Ref( bRel );
00143         Cudd_RecursiveDeref( dd, bTemp ); 
00144         Cudd_RecursiveDeref( dd, bProd ); 
00145     }
00146     // free the global BDDs
00147 //    Abc_NtkFreeGlobalBdds( pNtk );
00148     Abc_NtkFreeGlobalBdds( pNtk, 0 );
00149 
00150     // quantify the PI variables
00151     bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
00152     bRel    = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs );    Cudd_Ref( bRel );
00153     Cudd_RecursiveDeref( dd, bTemp ); 
00154     Cudd_RecursiveDeref( dd, bInputs ); 
00155 
00156     // reorder and disable reordering
00157     if ( fReorder )
00158     {
00159         if ( fVerbose )
00160             fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) );
00161         Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
00162         Cudd_AutodynDisable( dd );
00163         if ( fVerbose )
00164             fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) );
00165     }
00166     Cudd_Deref( bRel );
00167     return bRel;
00168 }

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