/**CFile****************************************************************
FileName [bmcMulti.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Proving multi-output properties.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcMulti.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extra.h"
#include "aig/gia/giaAig.h"
#include "aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Divides outputs into solved and unsolved.]
Description [Return array of unsolved outputs to extract into a new AIG.
Updates the resulting CEXes (vCexesOut) and current output map (vOutMap).]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, Vec_Int_t * vOutMap )
{
Abc_Cex_t * pCex;
Vec_Int_t * vLeftOver;
int i, iOut;
assert( Vec_PtrSize(vCexesIn) == Vec_IntSize(vOutMap) );
vLeftOver = Vec_IntAlloc( Vec_PtrSize(vCexesIn) );
Vec_IntForEachEntry( vOutMap, iOut, i )
{
assert( Vec_PtrEntry(vCexesOut, iOut) == NULL );
pCex = (Abc_Cex_t *)Vec_PtrEntry( vCexesIn, i );
if ( pCex ) // found a CEX for output iOut
{
Vec_PtrWriteEntry( vCexesIn, i, NULL );
Vec_PtrWriteEntry( vCexesOut, iOut, pCex );
}
else // still unsolved
{
Vec_IntWriteEntry( vOutMap, Vec_IntSize(vLeftOver), iOut );
Vec_IntPush( vLeftOver, i );
}
}
Vec_IntShrink( vOutMap, Vec_IntSize(vLeftOver) );
return vLeftOver;
}
/**Function*************************************************************
Synopsis [Counts the number of constant 0 POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCountConst0PosGia( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, Counter = 0;
Gia_ManForEachPo( p, pObj, i )
Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
return Counter;
}
int Gia_ManCountConst0Pos( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
Saig_ManForEachPo( p, pObj, i )
Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSize, abctime clkStart )
{
printf( "%3s : ", pStr );
printf( "PI =%6d ", Saig_ManPiNum(p) );
printf( "PO =%6d ", Saig_ManPoNum(p) );
printf( "FF =%7d ", Saig_ManRegNum(p) );
printf( "ND =%7d ", Aig_ManNodeNum(p) );
printf( "Solved =%7d (%5.1f %%) ", nTotalPo-Saig_ManPoNum(p), 100.0*(nTotalPo-Saig_ManPoNum(p))/Abc_MaxInt(1, nTotalPo) );
printf( "Size =%7d (%5.1f %%) ", Aig_ManObjNum(p), 100.0*Aig_ManObjNum(p)/Abc_MaxInt(1, nTotalSize) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pTemp;
pGia = Gia_ManFromAig( p );
pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0, 0 );
Gia_ManStop( pTemp );
pAig = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );
return pAig;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
{
Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
Vec_Int_t * vOutMap, * vLeftOver;
Vec_Ptr_t * vCexes;
Aig_Man_t * pTemp;
abctime clkStart = Abc_Clock();
abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p);
int TimeOutLoc = pPars->TimeOutLoc;
int i, RetValue = -1;
if ( pPars->fVerbose )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n",
pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
if ( pPars->fVerbose )
printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n",
pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
// create output map
vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers)
for ( i = 0; i < 1000; i++ )
{
int nSolved = Vec_PtrCountZero(vCexes);
// perform SIM3
Ssw_RarSetDefaultParams( pParsSim );
pParsSim->fSolveAll = 1;
pParsSim->fNotVerbose = 1;
pParsSim->fSilent = !pPars->fVeryVerbose;
pParsSim->TimeOut = TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500;
pParsSim->nWords = 5;
RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs
if ( p->vSeqModelVec )
{
vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
if ( Vec_IntSize(vLeftOver) == 0 )
break;
// remove solved
p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
// perform BMC
Saig_ParBmcSetDefaultParams( pParsBmc );
pParsBmc->fSolveAll = 1;
pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = !pPars->fVeryVerbose;
pParsBmc->nTimeOut = TimeOutLoc;
pParsBmc->nTimeOutOne = pPars->TimePerOut;
RetValue *= Saig_ManBmcScalable( p, pParsBmc );
if ( pPars->fVeryVerbose )
Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
// sort outputs
if ( p->vSeqModelVec )
{
vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
if ( Vec_IntSize(vLeftOver) == 0 )
break;
// remove solved
p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout
if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
// check gap timeout
if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
{
printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
break;
}
// synthesize
if ( pPars->fUseSyn )
{
p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
Aig_ManStop( pTemp );
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
}
// increase timeout
TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
}
Vec_IntFree( vOutMap );
if ( pPars->fVerbose )
printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
if ( pPars->fDumpFinal )
{
char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
Ioa_WriteAiger( p, pFileName, 0, 0 );
printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
}
Aig_ManStop( p );
return vCexes;
}
int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars )
{
Aig_Man_t * pAig;
if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
pAig = Gia_ManToAig( p, 0 );
p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END