luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcReach.c

328 lines
11 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [abcReach.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Performs reachability analysis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef ABC_USE_CUDD
/**Function*************************************************************
Synopsis [Computes the initial state and sets up the variable map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
{
DdNode ** pbVarsX, ** pbVarsY;
DdNode * bTemp, * bProd, * bVar;
Abc_Obj_t * pLatch;
int i;
// set the variable mapping for Cudd_bddVarMap()
pbVarsX = ABC_ALLOC( DdNode *, dd->size );
pbVarsY = ABC_ALLOC( DdNode *, dd->size );
bProd = b1; Cudd_Ref( bProd );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
// get the initial value of the latch
bVar = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
ABC_FREE( pbVarsX );
ABC_FREE( pbVarsY );
Cudd_Deref( bProd );
return bProd;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
{
DdNode ** pbParts;
DdNode * bVar;
Abc_Obj_t * pNode;
int i;
// extand the BDD manager to represent NS variables
assert( dd->size == Abc_NtkCiNum(pNtk) );
Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
// enable reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
else
Cudd_AutodynDisable( dd );
// compute the transition relation
pbParts = ABC_ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, (DdNode *)Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] );
}
// free the global BDDs
Abc_NtkFreeGlobalBdds( pNtk, 0 );
// reorder and disable reordering
if ( fReorder )
{
if ( fVerbose )
fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
Cudd_AutodynDisable( dd );
if ( fVerbose )
fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
}
return pbParts;
}
/**Function*************************************************************
Synopsis [Computes the set of unreachable states.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
int fInternalReorder = 0;
Extra_ImageTree_t * pTree = NULL;
Extra_ImageTree2_t * pTree2 = NULL;
DdNode * bReached, * bCubeCs;
DdNode * bCurrent, * bNext = NULL, * bTemp;
DdNode ** pbVarsY;
Abc_Obj_t * pLatch;
int i, nIters, nBddSize;
int nThreshold = 10000;
// collect the NS variables
// set the variable mapping for Cudd_bddVarMap()
pbVarsY = ABC_ALLOC( DdNode *, dd->size );
Abc_NtkForEachLatch( pNtk, pLatch, i )
pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
// start the image computation
bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs );
if ( fPartition )
pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
else
pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
ABC_FREE( pbVarsY );
Cudd_RecursiveDeref( dd, bCubeCs );
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
assert( nIterMax > 1 ); // required to not deref uninitialized bNext
for ( nIters = 1; nIters <= nIterMax; nIters++ )
{
// compute the next states
if ( fPartition )
bNext = Extra_bddImageCompute( pTree, bCurrent );
else
bNext = Extra_bddImageCompute2( pTree2, bCurrent );
Cudd_Ref( bNext );
Cudd_RecursiveDeref( dd, bCurrent );
// remap these states into the current state vars
bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext );
Cudd_RecursiveDeref( dd, bTemp );
// check if there are any new states
if ( Cudd_bddLeq( dd, bNext, bReached ) )
break;
// check the BDD size
nBddSize = Cudd_DagSize(bNext);
if ( nBddSize > nBddMax )
break;
// check the result
if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
{
printf( "The miter is proved REACHABLE in %d iterations. ", nIters );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
break;
}
// get the new states
bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// minimize the new states with the reached states
// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// Cudd_RecursiveDeref( dd, bTemp );
// add to the reached states
bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bNext );
if ( fVerbose )
fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
if ( fInternalReorder && fReorder && nBddSize > nThreshold )
{
if ( fVerbose )
fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
Cudd_AutodynDisable( dd );
if ( fVerbose )
fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
nThreshold *= 2;
}
if ( fVerbose )
fprintf( stdout, "\r" );
}
Cudd_RecursiveDeref( dd, bNext );
// undo the image tree
if ( fPartition )
Extra_bddImageTreeDelete( pTree );
else
Extra_bddImageTreeDelete2( pTree2 );
if ( bReached == NULL )
return NULL;
// report the stats
if ( fVerbose )
{
double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
else
fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
fflush( stdout );
}
//ABC_PRB( dd, bReached );
Cudd_Deref( bReached );
if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
printf( "The miter is proved unreachable in %d iteration. ", nIters );
return bReached;
}
/**Function*************************************************************
Synopsis [Performs reachability to see if any .]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
DdManager * dd;
DdNode ** pbParts;
DdNode * bOutput, * bReached, * bInitial;
int i;
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkPoNum(pNtk) == 1 );
assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
// compute the global BDDs of the latches
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, 0, fVerbose );
if ( dd == NULL )
{
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
return;
}
if ( fVerbose )
printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// save the output BDD
bOutput = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
// create partitions
pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
// create the initial state and the variable map
bInitial = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial );
// check the result
if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
printf( "The miter is proved REACHABLE in the initial state. " );
else
{
// compute the reachable states
bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
if ( bReached != NULL )
{
Cudd_Ref( bReached );
Cudd_RecursiveDeref( dd, bReached );
}
}
// cleanup
Cudd_RecursiveDeref( dd, bOutput );
Cudd_RecursiveDeref( dd, bInitial );
for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
Cudd_RecursiveDeref( dd, pbParts[i] );
ABC_FREE( pbParts );
Extra_StopManager( dd );
// report the runtime
ABC_PRT( "Time", Abc_Clock() - clk );
fflush( stdout );
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink