/**CFile****************************************************************
FileName [cecChoice.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Computation of structural choices.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cecInt.h"
#include "aig/gia/giaAig.h"
#include "proof/dch/dch.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the real value of the literal w/o spec reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
assert( Gia_ObjIsAnd(pObj) );
Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Recursively performs speculative reduction for the object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
Gia_Obj_t * pRepr;
if ( ~pObj->Value )
return;
if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
{
Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
return;
}
pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int i, iPrev, iObj, iPrevNew, iObjNew;
assert( p->pReprs != NULL );
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
if ( fRings )
{
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsConst( p, i ) )
{
iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
if ( iObjNew != 0 )
{
Vec_IntPush( *pvOutputs, 0 );
Vec_IntPush( *pvOutputs, i );
Vec_IntPush( vXorLits, iObjNew );
}
}
else if ( Gia_ObjIsHead( p, i ) )
{
iPrev = i;
Gia_ClassForEachObj1( p, i, iObj )
{
iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
}
iPrev = iObj;
}
iObj = i;
iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
iObjNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
{
Vec_IntPush( *pvOutputs, iPrev );
Vec_IntPush( *pvOutputs, iObj );
Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
}
}
}
}
else
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
{
int nItersMax = 1000;
Vec_Str_t * vStatus;
Vec_Int_t * vOutputs;
Vec_Int_t * vCexStore;
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
Cec_ManSim_t * pSim;
Gia_Man_t * pSrm;
int r, RetValue;
clock_t clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
clock_t clk2, clk = clock();
ABC_FREE( pAig->pReprs );
ABC_FREE( pAig->pNexts );
Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
pParsSim->nFrames = pPars->nRounds;
pParsSim->fVerbose = pPars->fVerbose;
pParsSim->fLatchCorr = 0;
pParsSim->fSeqSimulate = 0;
// create equivalence classes of registers
pSim = Cec_ManSimStart( pAig, pParsSim );
Cec_ManSimClassesPrepare( pSim, -1 );
Cec_ManSimClassesRefine( pSim );
// prepare SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose;
if ( pPars->fVerbose )
{
Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
}
// perform refinement of equivalence classes
for ( r = 0; r < nItersMax; r++ )
{
clk = clock();
// perform speculative reduction
clk2 = clock();
pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
clkSrm += clock() - clk2;
if ( Gia_ManCoNum(pSrm) == 0 )
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
Vec_IntFree( vOutputs );
Gia_ManStop( pSrm );
break;
}
//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
// found counter-examples to speculation
clk2 = clock();
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
clkSat += clock() - clk2;
if ( Vec_IntSize(vCexStore) == 0 )
{
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
break;
}
// refine classes with these counter-examples
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
Vec_IntFree( vCexStore );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
if ( pPars->fVerbose )
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
Vec_StrFree( vStatus );
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
// check the overflow
if ( r == nItersMax )
Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
// report the results
if ( pPars->fVerbose )
{
Abc_PrintTimeP( 1, "Srm ", clkSrm, clkTotal );
Abc_PrintTimeP( 1, "Sat ", clkSat, clkTotal );
Abc_PrintTimeP( 1, "Sim ", clkSim, clkTotal );
Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
Abc_PrintTime( 1, "TOTAL", clkTotal );
}
return 0;
}
/**Function*************************************************************
Synopsis [Computes choices for the vector of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
{
Gia_Man_t * pNew;
int RetValue;
// compute equivalences of the miter
// pMiter = Gia_ManChoiceMiter( vGias );
// Gia_ManSetRegNum( pMiter, 0 );
RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
// derive AIG with choices
pNew = Gia_ManEquivToChoices( pGia, nGias );
Gia_ManHasChoices( pNew );
// Gia_ManStop( pMiter );
// report the results
if ( pPars->fVerbose )
{
// Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
// Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
// 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
// Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
// 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Computes choices for one AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
{
// extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
Dch_Pars_t Pars, * pPars = &Pars;
Aig_Man_t * pMan, * pManNew;
Gia_Man_t * pGia;
if ( 0 )
{
pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
}
else
{
pMan = Gia_ManToAig( pAig, 0 );
Dch_ManSetDefaultParams( pPars );
pPars->fUseGia = 1;
pPars->nBTLimit = pParsChc->nBTLimit;
pPars->fUseCSat = pParsChc->fUseCSat;
pPars->fVerbose = pParsChc->fVerbose;
pManNew = Dar_ManChoiceNew( pMan, pPars );
pGia = Gia_ManFromAig( pManNew );
Aig_ManStop( pManNew );
// Aig_ManStop( pMan );
}
return pGia;
}
/**Function*************************************************************
Synopsis [Performs computation of AIGs with choices.]
Description [Takes several AIGs and performs choicing.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
{
Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
Aig_Man_t * pAig;
if ( pPars->fVerbose )
Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );
Cec_ManChcSetDefaultParams( pParsChc );
pParsChc->nBTLimit = pPars->nBTLimit;
pParsChc->fUseCSat = pPars->fUseCSat;
if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
pParsChc->nBTLimit = 100;
pParsChc->fVerbose = pPars->fVerbose;
pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END