/**CFile****************************************************************
FileName [pdrMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Property driven reachability.]
Synopsis [Manager procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 20, 2010.]
Revision [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "pdrInt.h"
#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Structural analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Pdr_ManDeriveFlopPriorities3( Gia_Man_t * p, int fMuxCtrls )
{
int fDiscount = 0;
Vec_Wec_t * vLevels;
Vec_Int_t * vRes, * vLevel, * vCosts;
Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
int i, k, Entry, MaxEntry = 0;
Gia_ManCreateRefs(p);
// discount references
if ( fDiscount )
{
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjIsMuxType(pObj) )
continue;
pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
pData0 = Gia_Regular(pData0);
pData1 = Gia_Regular(pData1);
p->pRefs[Gia_ObjId(p, pCtrl)]--;
if ( pData0 == pData1 )
p->pRefs[Gia_ObjId(p, pData0)]--;
}
}
// create flop costs
vCosts = Vec_IntAlloc( Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
{
Vec_IntPush( vCosts, Gia_ObjRefNum(p, pObj) );
MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
//printf( "%d(%d) ", i, Gia_ObjRefNum(p, pObj) );
}
//printf( "\n" );
MaxEntry++;
// add costs due to MUX inputs
if ( fMuxCtrls )
{
int fVerbose = 0;
Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
Gia_Obj_t * pCtrl, * pData1, * pData0;
int nCtrls = 0, nDatas = 0, nBoth = 0;
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjIsMuxType(pObj) )
continue;
pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
pCtrl = Gia_Regular(pCtrl);
pData1 = Gia_Regular(pData1);
pData0 = Gia_Regular(pData0);
Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
}
Gia_ManForEachRo( p, pObj, i )
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
Vec_IntAddToEntry( vCosts, i, MaxEntry );
//else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
// Vec_IntAddToEntry( vCosts, i, MaxEntry );
MaxEntry = 2*MaxEntry + 1;
// print out
if ( fVerbose )
{
Gia_ManForEachRo( p, pObj, i )
{
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
nCtrls++;
if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
nDatas++;
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
nBoth++;
}
printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
}
Vec_BitFree( vCtrls );
Vec_BitFree( vDatas );
}
// create levelized structure
vLevels = Vec_WecStart( MaxEntry );
Vec_IntForEachEntry( vCosts, Entry, i )
Vec_WecPush( vLevels, Entry, i );
// collect in this order
MaxEntry = 0;
vRes = Vec_IntStart( Gia_ManRegNum(p) );
Vec_WecForEachLevel( vLevels, vLevel, i )
Vec_IntForEachEntry( vLevel, Entry, k )
Vec_IntWriteEntry( vRes, Entry, MaxEntry++ );
//printf( "%d ", Gia_ObjRefNum(p, Gia_ManCi(p, Gia_ManPiNum(p)+Entry)) );
//printf( "\n" );
assert( MaxEntry == Gia_ManRegNum(p) );
Vec_WecFree( vLevels );
Vec_IntFree( vCosts );
ABC_FREE( p->pRefs );
//Vec_IntPrint( vRes );
return vRes;
}
/**Function*************************************************************
Synopsis [Structural analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls )
{
int fDiscount = 0;
Vec_Int_t * vRes = NULL;
Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
int MaxEntry = 0;
int i, * pPerm;
// create flop costs
Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) );
Gia_ManCreateRefs(p);
// discount references
if ( fDiscount )
{
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjIsMuxType(pObj) )
continue;
pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
pData0 = Gia_Regular(pData0);
pData1 = Gia_Regular(pData1);
p->pRefs[Gia_ObjId(p, pCtrl)]--;
if ( pData0 == pData1 )
p->pRefs[Gia_ObjId(p, pData0)]--;
}
}
Gia_ManForEachRo( p, pObj, i )
{
Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) );
MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
}
MaxEntry++;
ABC_FREE( p->pRefs );
// add costs due to MUX inputs
if ( fMuxCtrls )
{
int fVerbose = 0;
Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
Gia_Obj_t * pCtrl, * pData1, * pData0;
int nCtrls = 0, nDatas = 0, nBoth = 0;
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Gia_ObjIsMuxType(pObj) )
continue;
pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
pCtrl = Gia_Regular(pCtrl);
pData1 = Gia_Regular(pData1);
pData0 = Gia_Regular(pData0);
Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
}
Gia_ManForEachRo( p, pObj, i )
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
Vec_IntAddToEntry( vCosts, i, MaxEntry );
//else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
// Vec_IntAddToEntry( vCosts, i, MaxEntry );
// print out
if ( fVerbose )
{
Gia_ManForEachRo( p, pObj, i )
{
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
nCtrls++;
if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
nDatas++;
if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
nBoth++;
}
printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
}
Vec_BitFree( vCtrls );
Vec_BitFree( vDatas );
}
// create ordering based on costs
pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) );
Vec_IntFree( vCosts );
vCosts = Vec_IntInvert( vRes, -1 );
Vec_IntFree( vRes );
//Vec_IntPrint( vCosts );
return vCosts;
}
/**Function*************************************************************
Synopsis [Creates manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
{
Pdr_Man_t * p;
p = ABC_CALLOC( Pdr_Man_t, 1 );
p->pPars = pPars;
p->pAig = pAig;
p->pGia = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
p->vSolvers = Vec_PtrAlloc( 0 );
p->vClauses = Vec_VecAlloc( 0 );
p->pQueue = NULL;
p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
p->vActVars = Vec_IntAlloc( 256 );
if ( !p->pPars->fMonoCnf )
p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
// internal use
p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig));
if ( vPrioInit )
p->vPrio = vPrioInit;
else if ( pPars->fFlopPrio )
p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
// else if ( p->pPars->fNewXSim )
// p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
else
p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
p->vLits = Vec_IntAlloc( 100 ); // array of literals
p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves
p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots
p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values
p->vCoVals = Vec_IntAlloc( 100 ); // cone root values
p->vNodes = Vec_IntAlloc( 100 ); // cone nodes
p->vUndo = Vec_IntAlloc( 100 ); // cone undos
p->vVisits = Vec_IntAlloc( 100 ); // intermediate
p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed
p->vRes = Vec_IntAlloc( 100 ); // final result
p->pCnfMan = Cnf_ManStart();
// ternary simulation
p->pTxs3 = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
// additional AIG data-members
if ( pAig->pFanData == NULL )
Aig_ManFanoutStart( pAig );
if ( pAig->pTerSimData == NULL )
pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
// time spent on each outputs
if ( pPars->nTimeOutOne )
{
int i;
p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
}
if ( pPars->fSolveAll )
{
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
}
return p;
}
/**Function*************************************************************
Synopsis [Frees manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Pdr_ManStop( Pdr_Man_t * p )
{
Pdr_Set_t * pCla;
sat_solver * pSat;
int i, k;
Gia_ManStopP( &p->pGia );
Aig_ManCleanMarkAB( p->pAig );
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Cex =%4d Start =%4d\n",
p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
ABC_PRTP( " sat ", p->tSatSat, p->tTotal );
ABC_PRTP( "Generalize ", p->tGeneral, p->tTotal );
ABC_PRTP( "Push clause", p->tPush, p->tTotal );
ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal );
ABC_PRTP( "Containment", p->tContain, p->tTotal );
ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
ABC_PRTP( "Refinement ", p->tAbs, p->tTotal );
ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
fflush( stdout );
}
// Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
sat_solver_delete( pSat );
Vec_PtrFree( p->vSolvers );
Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
Pdr_SetDeref( pCla );
Vec_VecFree( p->vClauses );
Pdr_QueueStop( p );
ABC_FREE( p->pOrder );
Vec_IntFree( p->vActVars );
// static CNF
Cnf_DataFree( p->pCnf1 );
Vec_IntFreeP( &p->vVar2Reg );
// dynamic CNF
Cnf_DataFree( p->pCnf2 );
if ( p->pvId2Vars )
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
ABC_FREE( p->pvId2Vars[i].pArray );
ABC_FREE( p->pvId2Vars );
// Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
ABC_FREE( p->vVar2Ids.pArray );
Vec_WecFreeP( &p->vVLits );
// CNF manager
Cnf_ManStop( p->pCnfMan );
Vec_IntFreeP( &p->vAbsFlops );
Vec_IntFreeP( &p->vMapFf2Ppi );
Vec_IntFreeP( &p->vMapPpi2Ff );
// terminary simulation
if ( p->pPars->fNewXSim )
Txs3_ManStop( p->pTxs3 );
// internal use
Vec_IntFreeP( &p->vPrio ); // priority flops
Vec_IntFree( p->vLits ); // array of literals
Vec_IntFree( p->vCiObjs ); // cone leaves
Vec_IntFree( p->vCoObjs ); // cone roots
Vec_IntFree( p->vCiVals ); // cone leaf values
Vec_IntFree( p->vCoVals ); // cone root values
Vec_IntFree( p->vNodes ); // cone nodes
Vec_IntFree( p->vUndo ); // cone undos
Vec_IntFree( p->vVisits ); // intermediate
Vec_IntFree( p->vCi2Rem ); // CIs to be removed
Vec_IntFree( p->vRes ); // final result
Vec_PtrFreeP( &p->vInfCubes );
ABC_FREE( p->pTime4Outs );
if ( p->vCexes )
Vec_PtrFreeFree( p->vCexes );
// additional AIG data-members
if ( p->pAig->pFanData != NULL )
Aig_ManFanoutStop( p->pAig );
if ( p->pAig->pTerSimData != NULL )
ABC_FREE( p->pAig->pTerSimData );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Derives counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
{
Abc_Cex_t * pCex;
Pdr_Obl_t * pObl;
int i, f, Lit, nFrames = 0;
// count the number of frames
for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
nFrames++;
// create the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
pCex->iPo = p->iOutCur;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
if ( Abc_LitIsCompl(Lit) )
continue;
if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
continue;
assert( Abc_Lit2Var(Lit) < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
}
assert( f == nFrames );
if ( !Saig_ManVerifyCex(p->pAig, pCex) )
printf( "CEX for output %d is not valid.\n", p->iOutCur );
return pCex;
}
/**Function*************************************************************
Synopsis [Derives counter-example when abstraction is used.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
{
extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
Gia_Man_t * pAbs;
Abc_Cex_t * pCex, * pCexCare;
Pdr_Obl_t * pObl;
int i, f, Lit, Flop, nFrames = 0;
int nPis = Saig_ManPiNum(p->pAig);
int nFfRefined = 0;
if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
return Pdr_ManDeriveCex(p);
// restore previous map
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
{
assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
}
Vec_IntClear( p->vMapPpi2Ff );
// count the number of frames
for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
{
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
continue;
Flop = Abc_Lit2Var(Lit) - nPis;
if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
continue;
Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
Vec_IntPush( p->vMapPpi2Ff, Flop );
}
nFrames++;
}
if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
return Pdr_ManDeriveCex(p);
if ( p->pPars->fUseSimpleRef )
{
// rely on ternary simulation to perform refinement
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
{
assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
nFfRefined++;
}
}
else
{
// create the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
pCex->iPo = p->iOutCur;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
if ( Abc_LitIsCompl(Lit) )
continue;
if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
else
{
int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
assert( iPPI < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
}
}
assert( f == nFrames );
// perform CEX minimization
pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
Gia_ManStop( pAbs );
assert( pCexCare->nPis == pCex->nPis );
Abc_CexFree( pCex );
// detect care PPIs
for ( f = 0; f < nFrames; f++ )
{
for ( i = nPis; i < pCexCare->nPis; i++ )
if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
{
if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
}
}
Abc_CexFree( pCexCare );
if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
return Pdr_ManDeriveCex(p);
}
//printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
p->nCexesTotal++;
p->nCexes++;
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END