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

616 lines
20 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [bbrReach.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD-based reachability analysis.]
Synopsis [Procedures to perform reachability analysis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bbr.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
int iOutput, int fVerbose, int fSilent );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default resynthesis parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p )
{
memset( p, 0, sizeof(Saig_ParBbr_t) );
p->TimeLimit = 0;
p->nBddMax = 50000;
p->nIterMax = 1000;
p->fPartition = 1;
p->fReorder = 1;
p->fReorderImage = 1;
p->fVerbose = 0;
p->fSilent = 0;
p->iFrame = -1;
}
/**Function********************************************************************
Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
{
DdNode * bTemp, * bProd;
int i;
assert( iStart <= iStop );
assert( iStart >= 0 && iStart <= dd->size );
assert( iStop >= 0 && iStop <= dd->size );
bProd = (dd)->one; Cudd_Ref( bProd );
for ( i = iStart; i < iStop; i++ )
{
bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bProd );
return bProd;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bbr_StopManager( DdManager * dd )
{
int RetValue;
// check for remaining references in the package
RetValue = Cudd_CheckZeroRef( dd );
if ( RetValue > 0 )
printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
// Cudd_PrintInfo( dd, stdout );
Cudd_Quit( dd );
}
/**Function*************************************************************
Synopsis [Computes the initial state and sets up the variable map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
{
DdNode ** pbVarsX, ** pbVarsY;
DdNode * bTemp, * bProd;
Aig_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 = (dd)->one; Cudd_Ref( bProd );
Saig_ManForEachLo( p, pLatch, i )
{
pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ];
pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
// get the initial value of the latch
bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
ABC_FREE( pbVarsX );
ABC_FREE( pbVarsY );
Cudd_Deref( bProd );
return bProd;
}
/**Function*************************************************************
Synopsis [Collects the array of output BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p )
{
DdNode ** pbOutputs;
Aig_Obj_t * pNode;
int i;
// compute the transition relation
pbOutputs = ABC_ALLOC( DdNode *, Saig_ManPoNum(p) );
Saig_ManForEachPo( p, pNode, i )
{
pbOutputs[i] = Aig_ObjGlobalBdd(pNode); Cudd_Ref( pbOutputs[i] );
}
return pbOutputs;
}
/**Function*************************************************************
Synopsis [Collects the array of partition BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose )
{
DdNode ** pbParts;
DdNode * bVar;
Aig_Obj_t * pNode;
int i;
// extand the BDD manager to represent NS variables
assert( dd->size == Saig_ManCiNum(p) );
Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 );
// enable reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
else
Cudd_AutodynDisable( dd );
// compute the transition relation
pbParts = ABC_ALLOC( DdNode *, Saig_ManRegNum(p) );
Saig_ManForEachLi( p, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] );
}
// free global BDDs
Aig_ManFreeGlobalBdds( p, dd );
// reorder and disable reordering
if ( fReorder )
{
if ( fVerbose )
fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
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,Saig_ManRegNum(p)) );
}
return pbParts;
}
/**Function*************************************************************
Synopsis [Computes the set of unreachable states.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs )
{
int fInternalReorder = 0;
Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
Bbr_ImageTree2_t * pTree2 = NULL; // Supprses "might be used uninitialized"
DdNode * bReached, * bCubeCs;
DdNode * bCurrent;
DdNode * bNext = NULL; // Suppress "might be used uninitialized"
DdNode * bTemp;
Cudd_ReorderingType method;
int i, nIters, nBddSize = 0, status;
int nThreshold = 10000;
abctime clk = Abc_Clock();
Vec_Ptr_t * vOnionRings;
int fixedPoint = 0;
status = Cudd_ReorderingStatus( dd, &method );
if ( status )
Cudd_AutodynDisable( dd );
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
if ( pPars->fPartition )
pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose );
else
pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose );
Cudd_RecursiveDeref( dd, bCubeCs );
if ( pTree == NULL )
{
if ( !pPars->fSilent )
printf( "BDDs blew up during qualitification scheduling. " );
return -1;
}
if ( status )
Cudd_AutodynEnable( dd, method );
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// perform reachability analysis
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent );
for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
{
// check the runtime limit
if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
{
printf( "Reached timeout after image computation (%d seconds).\n", pPars->TimeLimit );
Vec_PtrFree( vOnionRings );
// undo the image tree
if ( pPars->fPartition )
Bbr_bddImageTreeDelete( pTree );
else
Bbr_bddImageTreeDelete2( pTree2 );
pPars->iFrame = nIters - 1;
return -1;
}
// compute the next states
if ( pPars->fPartition )
bNext = Bbr_bddImageCompute( pTree, bCurrent );
else
bNext = Bbr_bddImageCompute2( pTree2, bCurrent );
if ( bNext == NULL )
{
if ( !pPars->fSilent )
printf( "BDDs blew up during image computation. " );
if ( pPars->fPartition )
Bbr_bddImageTreeDelete( pTree );
else
Bbr_bddImageTreeDelete2( pTree2 );
Vec_PtrFree( vOnionRings );
pPars->iFrame = nIters - 1;
return -1;
}
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 ) ) {
fixedPoint = 1;
break;
}
// check the BDD size
nBddSize = Cudd_DagSize(bNext);
if ( nBddSize > pPars->nBddMax )
break;
// check the result
for ( i = 0; i < Saig_ManPoNum(p); i++ )
{
if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
{
DdNode * bIntersect;
bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] ); Cudd_Ref( bIntersect );
assert( p->pSeqModel == NULL );
p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent );
Cudd_RecursiveDeref( dd, bIntersect );
if ( !pPars->fSilent )
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, Vec_PtrSize(vOnionRings) );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
pPars->iFrame = nIters;
break;
}
}
if ( i < Saig_ManPoNum(p) )
break;
// get the new states
bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
Vec_PtrPush( vOnionRings, bCurrent ); 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 ( pPars->fVerbose )
fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold )
{
if ( pPars->fVerbose )
fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
Cudd_AutodynDisable( dd );
if ( pPars->fVerbose )
fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
nThreshold *= 2;
}
if ( pPars->fVerbose )
// fprintf( stdout, "\r" );
fprintf( stdout, "\n" );
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
// Extra_bddPrint( dd, bReached );printf( "\n" );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
fflush( stdout );
}
}
Cudd_RecursiveDeref( dd, bNext );
// free the onion rings
Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
// undo the image tree
if ( pPars->fPartition )
Bbr_bddImageTreeDelete( pTree );
else
Bbr_bddImageTreeDelete2( pTree2 );
if ( bReached == NULL )
return 0; // proved reachable
// report the stats
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
else
fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
fflush( stdout );
}
//ABC_PRB( dd, bReached );
Cudd_RecursiveDeref( dd, bReached );
// SPG
//
if ( fixedPoint ) {
if ( !pPars->fSilent ) {
printf( "The miter is proved unreachable after %d iterations. ", nIters );
}
pPars->iFrame = nIters - 1;
return 1;
}
assert(nIters >= pPars->nIterMax || nBddSize >= pPars->nBddMax);
if ( !pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
pPars->iFrame = nIters - 1;
return -1; // undecided
}
/**Function*************************************************************
Synopsis [Performs reachability to see if any PO can be asserted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
{
int fCheckOutputs = !pPars->fSkipOutCheck;
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
DdNode * bInitial, * bTemp;
int RetValue, i;
abctime clk = Abc_Clock();
Vec_Ptr_t * vOnionRings;
assert( Saig_ManRegNum(p) > 0 );
// compute the global BDDs of the latches
dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose );
if ( dd == NULL )
{
if ( !pPars->fSilent )
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax );
return -1;
}
if ( pPars->fVerbose )
printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// check the runtime limit
if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
{
printf( "Reached timeout after constructing global BDDs (%d seconds).\n", pPars->TimeLimit );
Cudd_Quit( dd );
return -1;
}
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// save outputs
pbOutputs = Aig_ManCreateOutputs( dd, p );
// create partitions
pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose );
// create the initial state and the variable map
bInitial = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose ); Cudd_Ref( bInitial );
// set reordering
if ( pPars->fReorderImage )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
// check the result
RetValue = -1;
for ( i = 0; i < Saig_ManPoNum(p); i++ )
{
if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
{
DdNode * bIntersect;
bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] ); Cudd_Ref( bIntersect );
assert( p->pSeqModel == NULL );
p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent );
Cudd_RecursiveDeref( dd, bIntersect );
if ( !pPars->fSilent )
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, -1 );
RetValue = 0;
break;
}
}
// free the onion rings
Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
// explore reachable states
if ( RetValue == -1 )
RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs );
// cleanup
Cudd_RecursiveDeref( dd, bInitial );
for ( i = 0; i < Saig_ManRegNum(p); i++ )
Cudd_RecursiveDeref( dd, pbParts[i] );
ABC_FREE( pbParts );
for ( i = 0; i < Saig_ManPoNum(p); i++ )
Cudd_RecursiveDeref( dd, pbOutputs[i] );
ABC_FREE( pbOutputs );
// if ( RetValue == -1 )
Cudd_Quit( dd );
// else
// Bbr_StopManager( dd );
// report the runtime
if ( !pPars->fSilent )
{
ABC_PRT( "Time", Abc_Clock() - clk );
fflush( stdout );
}
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs reachability to see if any PO can be asserted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
{
Abc_Cex_t * pCexOld, * pCexNew;
Aig_Man_t * p;
Aig_Obj_t * pObj;
Vec_Int_t * vInputMap;
int i, k, Entry, iBitOld, iBitNew, RetValue;
// pPars->fVerbose = 1;
// check if there are PIs without fanout
Saig_ManForEachPi( pInit, pObj, i )
if ( Aig_ObjRefs(pObj) == 0 )
break;
if ( i == Saig_ManPiNum(pInit) )
return Aig_ManVerifyUsingBdds_int( pInit, pPars );
// create new AIG
p = Aig_ManDupTrim( pInit );
assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
if ( RetValue != 0 )
{
Aig_ManStop( p );
return RetValue;
}
// the problem is satisfiable - remap the pattern
pCexOld = p->pSeqModel;
assert( pCexOld != NULL );
// create input map
vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
Saig_ManForEachPi( pInit, pObj, i )
if ( pObj->pData != NULL )
Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
else
Vec_IntPush( vInputMap, -1 );
// create new pattern
pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
pCexNew->iFrame = pCexOld->iFrame;
pCexNew->iPo = pCexOld->iPo;
// copy the bit-data
for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
if ( Abc_InfoHasBit( pCexOld->pData, iBitOld ) )
Abc_InfoSetBit( pCexNew->pData, iBitOld );
// copy the primary input data
iBitNew = iBitOld;
for ( i = 0; i <= pCexNew->iFrame; i++ )
{
Vec_IntForEachEntry( vInputMap, Entry, k )
{
if ( Entry == -1 )
continue;
if ( Abc_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
Abc_InfoSetBit( pCexNew->pData, iBitNew + k );
}
iBitOld += Saig_ManPiNum(p);
iBitNew += Saig_ManPiNum(pInit);
}
assert( iBitOld < iBitNew );
assert( iBitOld == pCexOld->nBits );
assert( iBitNew == pCexNew->nBits );
Vec_IntFree( vInputMap );
pInit->pSeqModel = pCexNew;
Aig_ManStop( p );
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink