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

1092 lines
36 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [llb2Nonlin.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD based reachability.]
Synopsis [Non-linear quantification scheduling.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: llb2Nonlin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "llbInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Mnx_t_ Llb_Mnx_t;
struct Llb_Mnx_t_
{
// user info
Aig_Man_t * pAig; // AIG manager
Gia_ParLlb_t * pPars; // parameters
// intermediate BDDs
DdManager * dd; // BDD manager
DdNode * bBad; // bad states in terms of CIs
DdNode * bReached; // reached states
DdNode * bCurrent; // from states
DdNode * bNext; // to states
Vec_Ptr_t * vRings; // onion rings in ddR
Vec_Ptr_t * vRoots; // BDDs for partitions
// structural info
Vec_Int_t * vOrder; // for each object ID, its BDD variable number or -1
Vec_Int_t * vVars2Q; // 1 if variable is quantifiable; 0 othervise
int timeImage;
int timeRemap;
int timeReo;
int timeOther;
int timeTotal;
};
//extern int timeBuild, timeAndEx, timeOther;
//extern int nSuppMax;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes bad in working manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
Vec_Ptr_t * vNodes;
DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult, * bCube;
Aig_Obj_t * pObj;
int i;
Aig_ManCleanData( pAig );
// assign elementary variables
Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
Aig_ManForEachCi( pAig, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
// compute internal nodes
vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), Saig_ManPoNum(pAig) );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) )
continue;
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
if ( bBdd == NULL )
{
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
return NULL;
}
Cudd_Ref( bBdd );
pObj->pData = bBdd;
}
// quantify PIs of each PO
bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult );
Saig_ManForEachPo( pAig, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 );
if ( bResult == NULL )
{
Cudd_RecursiveDeref( dd, bTemp );
break;
}
Cudd_Ref( bResult );
Cudd_RecursiveDeref( dd, bTemp );
}
// deref
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrFree( vNodes );
if ( bResult )
{
bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
Saig_ManForEachPi( pAig, pObj, i )
{
bCube = Cudd_bddAnd( dd, bTemp = bCube, (DdNode *)pObj->pData );
if ( bCube == NULL )
{
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bResult );
bResult = NULL;
break;
}
Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
if ( bResult != NULL )
{
bResult = Cudd_bddExistAbstract( dd, bTemp = bResult, bCube ); Cudd_Ref( bResult );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCube );
Cudd_Deref( bResult );
}
}
//if ( bResult )
//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) );
return bResult;
}
/**Function*************************************************************
Synopsis [Derives BDDs for the partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
Vec_Ptr_t * vRoots;
Aig_Obj_t * pObj;
DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
int i;
Aig_ManCleanData( pAig );
// assign elementary variables
Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd);
Aig_ManForEachCi( pAig, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
Aig_ManForEachNode( pAig, pObj, i )
if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
{
pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
Cudd_Ref( (DdNode *)pObj->pData );
}
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
// compute intermediate BDDs
vRoots = Vec_PtrAlloc( 100 );
Aig_ManForEachNode( pAig, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 );
if ( bBdd == NULL )
goto finish;
Cudd_Ref( bBdd );
if ( pObj->pData == NULL )
{
pObj->pData = bBdd;
continue;
}
// create new partition
bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );
if ( bPart == NULL )
goto finish;
Cudd_Ref( bPart );
Cudd_RecursiveDeref( dd, bBdd );
Vec_PtrPush( vRoots, bPart );
//printf( "%d ", Cudd_DagSize(bPart) );
}
// compute register output BDDs
Saig_ManForEachLi( pAig, pObj, i )
{
bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );
if ( bPart == NULL )
goto finish;
Cudd_Ref( bPart );
Vec_PtrPush( vRoots, bPart );
//printf( "%d ", Cudd_DagSize(bPart) );
}
//printf( "\n" );
Aig_ManForEachNode( pAig, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
return vRoots;
// early termination
finish:
Aig_ManForEachNode( pAig, pObj, i )
if ( pObj->pData )
Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
Cudd_RecursiveDeref( dd, bPart );
Vec_PtrFree( vRoots );
return NULL;
}
/**Function*************************************************************
Synopsis [Find simple variable ordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
{
Vec_Int_t * vOrder;
Aig_Obj_t * pObj;
int i, Counter = 0;
vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
Aig_ManForEachCi( pAig, pObj, i )
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
Saig_ManForEachLi( pAig, pObj, i )
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
return vOrder;
}
/**Function*************************************************************
Synopsis [Find good static variable ordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
{
Aig_Obj_t * pFanin0, * pFanin1;
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent( pAig, pObj );
assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
if ( Aig_ObjIsCi(pObj) )
{
// if ( Saig_ObjIsLo(pAig, pObj) )
// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
return;
}
// try fanins with higher level first
pFanin0 = Aig_ObjFanin0(pObj);
pFanin1 = Aig_ObjFanin1(pObj);
// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
if ( pFanin0->Level > pFanin1->Level )
{
Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
}
else
{
Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
}
if ( pObj->fMarkA )
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
}
/**Function*************************************************************
Synopsis [Collect nodes with the given fanout count.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
{
Vec_Int_t * vNodes;
Aig_Obj_t * pObj;
int i;
Aig_ManCleanMarkA( pAig );
Aig_ManForEachNode( pAig, pObj, i )
if ( Aig_ObjRefs(pObj) >= nFans )
pObj->fMarkA = 1;
// unmark flop drivers
Saig_ManForEachLi( pAig, pObj, i )
Aig_ObjFanin0(pObj)->fMarkA = 0;
// collect mapping
vNodes = Vec_IntAlloc( 100 );
Aig_ManForEachNode( pAig, pObj, i )
if ( pObj->fMarkA )
Vec_IntPush( vNodes, Aig_ObjId(pObj) );
Aig_ManCleanMarkA( pAig );
return vNodes;
}
/**Function*************************************************************
Synopsis [Find good static variable ordering.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
{
Vec_Int_t * vNodes = NULL;
Vec_Int_t * vOrder;
Aig_Obj_t * pObj;
int i, Counter = 0;
/*
// mark internal nodes to be used
Aig_ManCleanMarkA( pAig );
vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
pObj->fMarkA = 1;
printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
*/
// collect nodes in the order
vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
Aig_ManIncrementTravId( pAig );
Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
{
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
}
Aig_ManForEachCi( pAig, pObj, i )
if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
{
// if ( Saig_ObjIsLo(pAig, pObj) )
// Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
}
assert( Counter <= Aig_ManCiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
Aig_ManCleanMarkA( pAig );
Vec_IntFreeP( &vNodes );
return vOrder;
}
/**Function*************************************************************
Synopsis [Creates quantifiable varaibles for both types of traversal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fBackward )
{
Vec_Int_t * vVars2Q;
Aig_Obj_t * pObjLi, * pObjLo;
int i;
vVars2Q = Vec_IntAlloc( 0 );
Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, fBackward ? pObjLo : pObjLi), 0 );
return vVars2Q;
}
/**Function*************************************************************
Synopsis [Compute initial state in terms of current state variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
{
DdNode ** pVarsX, ** pVarsY;
Aig_Obj_t * pObjLo, * pObjLi;
int i;
pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
{
assert( Llb_ObjBddVar(vOrder, pObjLo) >= 0 );
assert( Llb_ObjBddVar(vOrder, pObjLi) >= 0 );
pVarsX[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLo) );
pVarsY[i] = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) );
}
Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) );
ABC_FREE( pVarsX );
ABC_FREE( pVarsY );
}
/**Function*************************************************************
Synopsis [Compute initial state in terms of current state variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fBackward )
{
Aig_Obj_t * pObjLi, * pObjLo;
DdNode * bRes, * bVar, * bTemp;
int i, TimeStop;
TimeStop = dd->TimeStop; dd->TimeStop = 0;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
{
bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo) );
bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
dd->TimeStop = TimeStop;
return bRes;
}
/**Function*************************************************************
Synopsis [Compute initial state in terms of current state variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues, int Flag )
{
Aig_Obj_t * pObjLo, * pObjLi, * pObjTemp;
DdNode * bRes, * bVar, * bTemp;
int i, TimeStop;
TimeStop = dd->TimeStop; dd->TimeStop = 0;
bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
{
if ( Flag )
pObjTemp = pObjLo, pObjLo = pObjLi, pObjLi = pObjTemp;
// get the correspoding flop input variable
bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObjLi) );
if ( pValues[Llb_ObjBddVar(vOrder, pObjLo)] != 1 )
bVar = Cudd_Not(bVar);
// create cube
bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
dd->TimeStop = TimeStop;
return bRes;
}
/**Function*************************************************************
Synopsis [Compute initial state in terms of current state variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4RecordState( Aig_Man_t * pAig, Vec_Int_t * vOrder, unsigned * pState, char * pValues, int fBackward )
{
Aig_Obj_t * pObjLo, * pObjLi;
int i;
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
if ( pValues[Llb_ObjBddVar(vOrder, fBackward? pObjLi : pObjLo)] == 1 )
Abc_InfoSetBit( pState, i );
}
/**Function*************************************************************
Synopsis [Multiply every partition by the cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4Multiply( DdManager * dd, DdNode * bCube, Vec_Ptr_t * vParts )
{
Vec_Ptr_t * vNew;
DdNode * bTemp, * bFunc;
int i;
vNew = Vec_PtrAlloc( Vec_PtrSize(vParts) );
Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
{
bTemp = Cudd_bddAnd( dd, bFunc, bCube ); Cudd_Ref( bTemp );
Vec_PtrPush( vNew, bTemp );
}
return vNew;
}
/**Function*************************************************************
Synopsis [Multiply every partition by the cube.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4Deref( DdManager * dd, Vec_Ptr_t * vParts )
{
DdNode * bFunc;
int i;
Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrFree( vParts );
}
/**Function*************************************************************
Synopsis [Derives counter-example by backward reachability.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose )
{
Vec_Int_t * vVars2Q;
Vec_Ptr_t * vStates, * vRootsNew;
Aig_Obj_t * pObj;
DdNode * bState = NULL, * bImage, * bOneCube, * bRing;
int i, v, RetValue;//, clk = clock();
char * pValues;
assert( Vec_PtrSize(p->vRings) > 0 );
// disable the timeout
p->dd->TimeStop = 0;
// start the state set
vStates = Vec_PtrAllocSimInfo( Vec_PtrSize(p->vRings), Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
Vec_PtrCleanSimInfo( vStates, 0, Abc_BitWordNum(Aig_ManRegNum(p->pAig)) );
if ( fBackward )
Vec_PtrReverseOrder( vStates );
// get the last cube
pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
bOneCube = Cudd_bddIntersect( p->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad ); Cudd_Ref( bOneCube );
RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
Cudd_RecursiveDeref( p->dd, bOneCube );
assert( RetValue );
// record the cube
Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntryLast(vStates), pValues, fBackward );
// write state in terms of NS variables
if ( Vec_PtrSize(p->vRings) > 1 )
{
bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState );
}
// perform backward analysis
vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, !fBackward );
Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
{
if ( v == Vec_PtrSize(p->vRings) - 1 )
continue;
// preprocess partitions
vRootsNew = Llb_Nonlin4Multiply( p->dd, bState, p->vRoots );
Cudd_RecursiveDeref( p->dd, bState );
// compute the next states
bImage = Llb_Nonlin4Image( p->dd, vRootsNew, NULL, vVars2Q ); Cudd_Ref( bImage );
Llb_Nonlin4Deref( p->dd, vRootsNew );
// intersect with the previous set
bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube );
Cudd_RecursiveDeref( p->dd, bImage );
// find any assignment of the BDD
RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
Cudd_RecursiveDeref( p->dd, bOneCube );
assert( RetValue );
// record the cube
Llb_Nonlin4RecordState( p->pAig, p->vOrder, (unsigned *)Vec_PtrEntry(vStates, v), pValues, fBackward );
// check that we get the init state
if ( v == 0 )
{
Saig_ManForEachLo( p->pAig, pObj, i )
assert( fBackward || pValues[Llb_ObjBddVar(p->vOrder, pObj)] == 0 );
break;
}
// write state in terms of NS variables
bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues, fBackward ); Cudd_Ref( bState );
}
Vec_IntFree( vVars2Q );
ABC_FREE( pValues );
if ( fBackward )
Vec_PtrReverseOrder( vStates );
// if ( fVerbose )
// Abc_PrintTime( 1, "BDD-based cex generation time", clock() - clk );
return vStates;
}
/**Function*************************************************************
Synopsis [Perform reachability with hints.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
{
DdNode * bAux;
int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0;
int clkTemp, clkIter, clk = clock();
assert( Aig_ManRegNum(p->pAig) > 0 );
if ( p->pPars->fBackward )
{
// create bad state in the ring manager
if ( !p->pPars->fSkipOutCheck )
{
p->bBad = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bBad );
}
// create init state
if ( p->pPars->fCluster )
p->bCurrent = p->dd->bFunc, p->dd->bFunc = NULL;
else
{
p->bCurrent = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );
if ( p->bCurrent == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1;
}
Cudd_Ref( p->bCurrent );
}
// remap into the next states
p->bCurrent = Cudd_bddVarMap( p->dd, bAux = p->bCurrent );
if ( p->bCurrent == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during remapping bad states.\n", p->pPars->TimeLimit );
Cudd_RecursiveDeref( p->dd, bAux );
p->pPars->iFrame = -1;
return -1;
}
Cudd_Ref( p->bCurrent );
Cudd_RecursiveDeref( p->dd, bAux );
}
else
{
// create bad state in the ring manager
if ( !p->pPars->fSkipOutCheck )
{
if ( p->pPars->fCluster )
p->bBad = p->dd->bFunc, p->dd->bFunc = NULL;
else
{
p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );
if ( p->bBad == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
p->pPars->iFrame = -1;
return -1;
}
Cudd_Ref( p->bBad );
}
}
else if ( p->dd->bFunc )
Cudd_RecursiveDeref( p->dd, p->dd->bFunc ), p->dd->bFunc = NULL;
// compute the starting set of states
p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder, p->pPars->fBackward ); Cudd_Ref( p->bCurrent );
}
// perform iterations
p->bReached = p->bCurrent; Cudd_Ref( p->bReached );
for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
{
clkIter = clock();
// check the runtime limit
if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
return -1;
}
// save the onion ring
Vec_PtrPush( p->vRings, p->bCurrent ); Cudd_Ref( p->bCurrent );
// check it for bad states
if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) )
{
Vec_Ptr_t * vStates;
assert( p->pAig->pSeqModel == NULL );
vStates = Llb_Nonlin4DeriveCex( p, p->pPars->fBackward, p->pPars->fVerbose );
p->pAig->pSeqModel = Llb4_Nonlin4TransformCex( p->pAig, vStates, -1, p->pPars->fVerbose );
Vec_PtrFreeP( &vStates );
if ( !p->pPars->fSilent )
{
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, nIters );
Abc_PrintTime( 1, "Time", clock() - clk );
}
p->pPars->iFrame = nIters - 1;
return 0;
}
// compute the next states
clkTemp = clock();
p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q );
if ( p->bNext == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
return -1;
}
Cudd_Ref( p->bNext );
p->timeImage += clock() - clkTemp;
// remap into current states
clkTemp = clock();
p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext );
if ( p->bNext == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during remapping next states.\n", p->pPars->TimeLimit );
Cudd_RecursiveDeref( p->dd, bAux );
p->pPars->iFrame = nIters - 1;
return -1;
}
Cudd_Ref( p->bNext );
Cudd_RecursiveDeref( p->dd, bAux );
p->timeRemap += clock() - clkTemp;
// collect statistics
if ( p->pPars->fVerbose )
{
nBddSizeFr = Cudd_DagSize( p->bCurrent );
nBddSizeTo = Cudd_DagSize( bAux );
nBddSizeTo2 = Cudd_DagSize( p->bNext );
}
Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL;
// derive new states
p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) );
if ( p->bCurrent == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
return -1;
}
Cudd_Ref( p->bCurrent );
Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
if ( Cudd_IsConstant(p->bCurrent) )
break;
/*
// reduce BDD size using constrain // Cudd_bddRestrict
p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );
Cudd_Ref( p->bCurrent );
printf( "Before = %d. After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
Cudd_RecursiveDeref( p->dd, bAux );
*/
// add to the reached set
p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );
if ( p->bReached == NULL )
{
if ( !p->pPars->fSilent )
printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
p->pPars->iFrame = nIters - 1;
Cudd_RecursiveDeref( p->dd, bAux );
return -1;
}
Cudd_Ref( p->bReached );
Cudd_RecursiveDeref( p->dd, bAux );
// report the results
if ( p->pPars->fVerbose )
{
printf( "I =%5d : ", nIters );
printf( "Fr =%7d ", nBddSizeFr );
printf( "ImNs =%7d ", nBddSizeTo );
printf( "ImCs =%7d ", nBddSizeTo2 );
printf( "Rea =%7d ", Cudd_DagSize(p->bReached) );
printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
Abc_PrintTime( 1, "T", clock() - clkIter );
}
/*
if ( pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) );
// Extra_bddPrint( p->dd, bReached );printf( "\n" );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
*/
if ( nIters == p->pPars->nIterMax - 1 )
{
if ( !p->pPars->fSilent )
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
p->pPars->iFrame = nIters;
return -1;
}
}
// report the stats
if ( p->pPars->fVerbose )
{
double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) );
if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) )
printf( "Reachability analysis completed after %d frames.\n", nIters );
else
printf( "Reachability analysis is stopped after %d frames.\n", nIters );
printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
fflush( stdout );
}
if ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) )
{
if ( !p->pPars->fSilent )
printf( "Verified only for states reachable in %d frames. ", nIters );
p->pPars->iFrame = p->pPars->nIterMax;
return -1; // undecided
}
// report
if ( !p->pPars->fSilent )
printf( "The miter is proved unreachable after %d iterations. ", nIters );
p->pPars->iFrame = nIters - 1;
Abc_PrintTime( 1, "Time", clock() - clk );
return 1; // unreachable
}
/**Function*************************************************************
Synopsis [Reorders BDDs in the working manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose )
{
int clk = clock();
if ( fVerbose )
Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
if ( fTwice )
{
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
if ( fVerbose )
Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
}
if ( fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnx_t * p;
p = ABC_CALLOC( Llb_Mnx_t, 1 );
p->pAig = pAig;
p->pPars = pPars;
// compute time to stop
p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
if ( pPars->fCluster )
{
// Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Llb4_Nonlin4Sweep( p->pAig, pPars->nBddMax, pPars->nClusterMax, &p->dd, &p->vOrder, &p->vRoots, pPars->fVerbose );
// set the stop time parameter
p->dd->TimeStop = p->pPars->TimeTarget;
}
else
{
// p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig );
p->vOrder = Llb_Nonlin4CreateOrder( pAig );
p->dd = Cudd_Init( Vec_IntCountPositive(p->vOrder) + 1, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Cudd_SetMaxGrowth( p->dd, 1.05 );
// set the stop time parameter
p->dd->TimeStop = p->pPars->TimeTarget;
p->vRoots = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
}
Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, p->pPars->fBackward );
p->vRings = Vec_PtrAlloc( 100 );
if ( pPars->fReorder )
Llb_Nonlin4Reorder( p->dd, 0, 1 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_MnxStop( Llb_Mnx_t * p )
{
DdNode * bTemp;
int i;
if ( p->pPars->fVerbose )
{
p->timeReo = Cudd_ReadReorderingTime(p->dd);
p->timeOther = p->timeTotal - p->timeImage - p->timeRemap;
ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
ABC_PRTP( "Remap ", p->timeRemap, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
}
// remove BDDs
if ( p->bBad )
Cudd_RecursiveDeref( p->dd, p->bBad );
if ( p->bReached )
Cudd_RecursiveDeref( p->dd, p->bReached );
if ( p->bCurrent )
Cudd_RecursiveDeref( p->dd, p->bCurrent );
if ( p->bNext )
Cudd_RecursiveDeref( p->dd, p->bNext );
if ( p->vRings )
Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
Cudd_RecursiveDeref( p->dd, bTemp );
if ( p->vRoots )
Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
Cudd_RecursiveDeref( p->dd, bTemp );
// remove arrays
Vec_PtrFreeP( &p->vRings );
Vec_PtrFreeP( &p->vRoots );
//Cudd_PrintInfo( p->dd, stdout );
Extra_StopManager( p->dd );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vVars2Q );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Llb_MnxCheckNextStateVars( Llb_Mnx_t * p )
{
Aig_Obj_t * pObj;
int i, Counter0 = 0, Counter1 = 0;
Saig_ManForEachLi( p->pAig, pObj, i )
if ( Saig_ObjIsLo(p->pAig, Aig_ObjFanin0(pObj)) )
{
if ( Aig_ObjFaninC0(pObj) )
Counter0++;
else
Counter1++;
}
printf( "Total = %d. Direct LO = %d. Compl LO = %d.\n", Aig_ManRegNum(p->pAig), Counter1, Counter0 );
}
/**Function*************************************************************
Synopsis [Finds balanced cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
{
Llb_Mnx_t * pMnn;
int RetValue = -1;
if ( pPars->fVerbose )
Aig_ManPrintStats( pAig );
if ( pPars->fCluster && Aig_ManObjNum(pAig) >= (1 << 15) )
{
printf( "The number of objects is more than 2^15. Clustering cannot be used.\n" );
return RetValue;
}
{
int clk = clock();
pMnn = Llb_MnxStart( pAig, pPars );
//Llb_MnxCheckNextStateVars( pMnn );
if ( !pPars->fSkipReach )
RetValue = Llb_Nonlin4Reachability( pMnn );
pMnn->timeTotal = clock() - clk;
Llb_MnxStop( pMnn );
}
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink