mirror of https://github.com/YosysHQ/abc.git
Initial new interpolation code.
This commit is contained in:
Alan Mishchenko
parent
d9bbcb5dc9
commit
b910cba3e2
|
|
@ -0,0 +1,90 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__aig__int2__int_h
|
||||
#define ABC__aig__int2__int_h
|
||||
|
||||
|
||||
/*
|
||||
The interpolation algorithm implemented here was introduced in the papers:
|
||||
K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
|
||||
C.-Y. Wu et al. A CEX-Guided Interpolant Generation Algorithm for
|
||||
SAT-based Model Checking. DAC'13.
|
||||
*/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// simulation manager
|
||||
typedef struct Int2_ManPars_t_ Int2_ManPars_t;
|
||||
struct Int2_ManPars_t_
|
||||
{
|
||||
int nBTLimit; // limit on the number of conflicts
|
||||
int nFramesS; // the starting number timeframes
|
||||
int nFramesMax; // the max number timeframes to unroll
|
||||
int nSecLimit; // time limit in seconds
|
||||
int nFramesK; // the number of timeframes to use in induction
|
||||
int fRewrite; // use additional rewriting to simplify timeframes
|
||||
int fTransLoop; // add transition into the init state under new PI var
|
||||
int fDropInvar; // dump inductive invariant into file
|
||||
int fVerbose; // print verbose statistics
|
||||
int iFrameMax; // the time frame reached
|
||||
char * pFileName; // file name to dump interpolant
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== intCore.c ==========================================================*/
|
||||
extern void Int2_ManSetDefaultParams( Int2_ManPars_t * p );
|
||||
extern int Int2_ManPerformInterpolation( Gia_Man_t * p, Int2_ManPars_t * pPars );
|
||||
|
||||
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,355 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2Bmc.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [BMC used inside IMC.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "int2Int.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Trasnforms AIG to transition into the init state.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose )
|
||||
{
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
||||
int i, iCtrl;
|
||||
assert( Gia_ManRegNum(p) > 0 );
|
||||
pNew = Gia_ManStart( 10000 );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
{
|
||||
if ( i == Gia_ManPiNum(p) )
|
||||
iCtrl = Gia_ManAppendCi( pNew );
|
||||
pObj->Value = Gia_ManAppendCi( pNew );
|
||||
}
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Gia_ManForEachPo( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
|
||||
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
|
||||
Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
|
||||
Gia_ManHashStop( pNew );
|
||||
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
|
||||
// remove dangling
|
||||
pNew = Gia_ManCleanup( pTemp = pNew );
|
||||
if ( fVerbose )
|
||||
printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
|
||||
Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
|
||||
Gia_ManStop( pTemp );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if AIG has transition into init state.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Int2_ManCheckInit( Gia_Man_t * p )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Cnf_Dat_t * pCnf;
|
||||
Gia_Man_t * pNew;
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vLits;
|
||||
int i, Lit, RetValue = 0;
|
||||
assert( Gia_ManRegNum(p) > 0 );
|
||||
pNew = Jf_ManDeriveCnf( p, 0 );
|
||||
pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||
if ( pSat != NULL )
|
||||
{
|
||||
vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
|
||||
Gia_ManForEachRi( pNew, pObj, i )
|
||||
{
|
||||
Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
|
||||
Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
|
||||
Vec_IntPush( vLits, Abc_LitNot(Lit) );
|
||||
}
|
||||
if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
|
||||
RetValue = 1;
|
||||
Vec_IntFree( vLits );
|
||||
sat_solver_delete( pSat );
|
||||
}
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pNew );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates the BMC instance in the SAT solver.]
|
||||
|
||||
Description [The PIs are mapped in the natural order. The flop inputs
|
||||
are the last Gia_ManRegNum(p) variables of resulting SAT solver.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Int2_ManFrameInit( Gia_Man_t * p, int nFrames, int fVerbose )
|
||||
{
|
||||
Gia_Man_t * pFrames, * pTemp;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, f;
|
||||
pFrames = Gia_ManStart( 10000 );
|
||||
pFrames->pName = Abc_UtilStrsav( p->pName );
|
||||
pFrames->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
// perform structural hashing
|
||||
Gia_ManHashAlloc( pFrames );
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
Gia_ManForEachPi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pFrames );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0;
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ObjFanin0Copy(pObj);
|
||||
}
|
||||
Gia_ManHashStop( pFrames );
|
||||
// create flop inputs
|
||||
Gia_ManForEachRi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
|
||||
// remove dangling
|
||||
pFrames = Gia_ManCleanup( pTemp = pFrames );
|
||||
if ( fVerbose )
|
||||
printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
|
||||
Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
|
||||
Gia_ManStop( pTemp );
|
||||
return pFrames;
|
||||
}
|
||||
sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames )
|
||||
{
|
||||
Gia_Man_t * pFrames, * pTemp;
|
||||
Cnf_Dat_t * pCnf;
|
||||
sat_solver * pSat;
|
||||
// unfold for the given number of timeframes
|
||||
pFrames = Int2_ManFrameInit( p, nFrames, 1 );
|
||||
assert( Gia_ManRegNum(pFrames) == 0 );
|
||||
// derive CNF for the timeframes
|
||||
pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp );
|
||||
pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
|
||||
// create SAT solver
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||
if ( pSat != NULL )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, nVars = sat_solver_nvars( pSat );
|
||||
sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
|
||||
// add clauses for the POs
|
||||
Gia_ManForEachCo( pFrames, pObj, i )
|
||||
sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
|
||||
}
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pFrames );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Int2_ManCheckFrames( Int2_Man_t * p, int iFrame, int iObj )
|
||||
{
|
||||
Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
|
||||
return Vec_IntEntry(vMapFrame, iObj);
|
||||
}
|
||||
static inline void Int2_ManWriteFrames( Int2_Man_t * p, int iFrame, int iObj, int iRes )
|
||||
{
|
||||
Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
|
||||
assert( Vec_IntEntry(vMapFrame, iObj) == -1 );
|
||||
Vec_IntWriteEntry( vMapFrame, iObj, iRes );
|
||||
}
|
||||
void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, Entry, iLit;
|
||||
// create storage room for unfolded IDs
|
||||
for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
|
||||
Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
|
||||
assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
|
||||
// create constant 0 node
|
||||
if ( f == 0 )
|
||||
{
|
||||
iLit = 1;
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, 0 );
|
||||
sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
|
||||
}
|
||||
// start the stack
|
||||
Vec_IntClear( p->vStack );
|
||||
Vec_IntForEachEntry( vPrefCos, Entry, i )
|
||||
{
|
||||
pObj = Gia_ManCo( p->pGia, Entry );
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
|
||||
}
|
||||
// construct unfolded AIG
|
||||
while ( Vec_IntSize(p->vStack) > 0 )
|
||||
{
|
||||
int iObj = Vec_IntPop(p->vStack);
|
||||
int iFrame = Vec_IntPop(p->vStack);
|
||||
if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
|
||||
continue;
|
||||
pObj = Gia_ManObj( p->pGia, iObj );
|
||||
if ( Gia_ObjIsPi(p->pGia, pObj) )
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
|
||||
else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, 0 );
|
||||
else if ( Gia_ObjIsRo(p->pGia, iObj) )
|
||||
{
|
||||
int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
|
||||
int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
|
||||
if ( iLit >= 0 )
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, iLit );
|
||||
else
|
||||
{
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObj );
|
||||
Vec_IntPush( p->vStack, iFrame-1 );
|
||||
Vec_IntPush( p->vStack, iObjF );
|
||||
}
|
||||
}
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
|
||||
int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
|
||||
if ( iLit >= 0 )
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
|
||||
else
|
||||
{
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObj );
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObjF );
|
||||
}
|
||||
}
|
||||
else if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
|
||||
int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
|
||||
int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
|
||||
int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
|
||||
if ( iLit0 >= 0 && iLit1 >= 0 )
|
||||
{
|
||||
Entry = Gia_ManObjNum(pFrames);
|
||||
iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
|
||||
Int2_ManWriteFrames( p, iFrame, iObj, iLit );
|
||||
if ( Entry < Gia_ManObjNum(pFrames) )
|
||||
{
|
||||
assert( !Abc_LitIsCompl(iLit) );
|
||||
sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObj );
|
||||
if ( iLit0 < 0 )
|
||||
{
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObjF0 );
|
||||
}
|
||||
if ( iLit1 < 0 )
|
||||
{
|
||||
Vec_IntPush( p->vStack, iFrame );
|
||||
Vec_IntPush( p->vStack, iObjF1 );
|
||||
}
|
||||
}
|
||||
}
|
||||
else assert( 0 );
|
||||
}
|
||||
}
|
||||
int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube )
|
||||
{
|
||||
int status;
|
||||
if ( vCube == NULL )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, iLit;
|
||||
Gia_ManForEachPo( p->pGia, pObj, i )
|
||||
{
|
||||
iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
|
||||
if ( iLit == 0 )
|
||||
continue;
|
||||
if ( iLit == 1 )
|
||||
return 0;
|
||||
status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
|
||||
if ( status == l_False )
|
||||
continue;
|
||||
if ( status == l_True )
|
||||
return 0;
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
|
||||
if ( status == l_False )
|
||||
return 1;
|
||||
if ( status == l_True )
|
||||
return 0;
|
||||
return -1;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,335 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2Core.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [Core procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "int2Int.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This procedure sets default values of interpolation parameters.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Int2_ManSetDefaultParams( Int2_ManPars_t * p )
|
||||
{
|
||||
memset( p, 0, sizeof(Int2_ManPars_t) );
|
||||
p->nBTLimit = 0; // limit on the number of conflicts
|
||||
p->nFramesS = 1; // the starting number timeframes
|
||||
p->nFramesMax = 0; // the max number timeframes to unroll
|
||||
p->nSecLimit = 0; // time limit in seconds
|
||||
p->nFramesK = 1; // the number of timeframes to use in induction
|
||||
p->fRewrite = 0; // use additional rewriting to simplify timeframes
|
||||
p->fTransLoop = 0; // add transition into the init state under new PI var
|
||||
p->fDropInvar = 0; // dump inductive invariant into file
|
||||
p->fVerbose = 0; // print verbose statistics
|
||||
p->iFrameMax = -1;
|
||||
}
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames )
|
||||
{
|
||||
Gia_Man_t * pFrames, * pTemp;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, f;
|
||||
assert( Gia_ManRegNum(pAig) > 0 );
|
||||
pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
|
||||
pFrames->pName = Abc_UtilStrsav( pAig->pName );
|
||||
pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
|
||||
Gia_ManHashAlloc( pFrames );
|
||||
Gia_ManConst0(pAig)->Value = 0;
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
Gia_ManForEachRo( pAig, pObj, i )
|
||||
pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
|
||||
Gia_ManForEachPi( pAig, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi( pFrames );
|
||||
Gia_ManForEachAnd( pAig, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Gia_ManForEachRi( pAig, pObj, i )
|
||||
pObj->Value = Gia_ObjFanin0Copy(pObj);
|
||||
}
|
||||
Gia_ManForEachRi( pAig, pObj, i )
|
||||
Gia_ManAppendCo( pFrames, pObj->Value );
|
||||
Gia_ManHashStop( pFrames );
|
||||
pFrames = Gia_ManCleanup( pTemp = pFrames );
|
||||
Gia_ManStop( pTemp );
|
||||
return pFrames;
|
||||
}
|
||||
sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap )
|
||||
{
|
||||
Gia_Man_t * pPref, * pNew;
|
||||
sat_solver * pSat;
|
||||
// create subset of the timeframe
|
||||
pPref = Int2_ManUnroll( p, f );
|
||||
// create SAT solver
|
||||
pNew = Jf_ManDeriveCnf( pPref, 0 );
|
||||
pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL;
|
||||
Gia_ManStop( pPref );
|
||||
// derive the SAT solver
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||
// collect indexes of CO variables
|
||||
*pvCiMap = Vec_IntAlloc( 100 );
|
||||
Gia_ManForEachPo( pNew, pObj, i )
|
||||
Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
|
||||
// cleanup
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pNew );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff )
|
||||
{
|
||||
Gia_Man_t * pSuff, * pNew;
|
||||
Gia_Obj_t * pObj;
|
||||
Cnf_Dat_t * pCnf;
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
int i, Lit, Limit;
|
||||
// create subset of the timeframe
|
||||
pSuff = Int2_ManProbToGia( p, vImageOne );
|
||||
assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) );
|
||||
// create SAT solver
|
||||
pNew = Jf_ManDeriveCnf( pSuff, 0 );
|
||||
pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL;
|
||||
Gia_ManStop( pSuff );
|
||||
// derive the SAT solver
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
|
||||
// create new constraints
|
||||
vLits = Vec_IntAlloc( 1000 );
|
||||
Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 )
|
||||
{
|
||||
Vec_IntClear( vLits );
|
||||
for ( k = 0; k < Limit; k++ )
|
||||
{
|
||||
i++;
|
||||
Lit = Vec_IntEntry( vSop, i + k );
|
||||
Vec_IntPush( vLits, Abc_LitNot(Lit) );
|
||||
}
|
||||
if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) // UNSAT
|
||||
{
|
||||
Vec_IntFree( vLits );
|
||||
Cnf_DataFree( pCnf );
|
||||
Gia_ManStop( pNew );
|
||||
*pvCoMap = NULL;
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
Vec_IntFree( vLits );
|
||||
// collect indexes of CO variables
|
||||
*pvCoMap = Vec_IntAlloc( 100 );
|
||||
Gia_ManForEachRo( p, pObj, i )
|
||||
{
|
||||
pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) );
|
||||
Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
|
||||
}
|
||||
// cleanup
|
||||
Cnf_DataFree( pCnf );
|
||||
if ( ppSuff )
|
||||
*ppSuff = pNew;
|
||||
else
|
||||
Gia_ManStop( pNew );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the cube cover and status.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio )
|
||||
{
|
||||
int i, iVar, status;
|
||||
Vec_IntClear( p->vImage );
|
||||
while ( 1 )
|
||||
{
|
||||
// run suffix solver
|
||||
status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 );
|
||||
if ( status == l_Undef )
|
||||
return NULL; // timeout
|
||||
if ( status == l_False )
|
||||
return INT2_COMPUTED;
|
||||
assert( status == l_True );
|
||||
// collect assignment
|
||||
Vec_IntClear( p->vAssign );
|
||||
Vec_IntForEachEntry( p->vCiMap, iVar, i )
|
||||
Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) );
|
||||
// derive initial cube
|
||||
vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio );
|
||||
// expend the cube using prefix
|
||||
status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
|
||||
if ( status == l_False )
|
||||
{
|
||||
int k, nCoreLits, * pCoreLits;
|
||||
nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits );
|
||||
// create cube
|
||||
Vec_IntClear( vCube );
|
||||
Vec_IntPush( vImage, nCoreLits );
|
||||
for ( k = 0; k < nCoreLits; k++ )
|
||||
{
|
||||
Vec_IntPush( vCube, pCoreLits[k] );
|
||||
Vec_IntPush( vImage, pCoreLits[k] );
|
||||
}
|
||||
// add cube to the solver
|
||||
if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) )
|
||||
{
|
||||
Vec_IntFree( vCube );
|
||||
return INT2_COMPUTED;
|
||||
}
|
||||
}
|
||||
Vec_IntFree( vCube );
|
||||
if ( status == l_Undef )
|
||||
return INT2_TIME_OUT;
|
||||
if ( status == l_True )
|
||||
return INT2_FALSE_NEG;
|
||||
assert( status == l_False );
|
||||
continue;
|
||||
}
|
||||
return p->vImage;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Interpolates while the number of conflicts is not exceeded.]
|
||||
|
||||
Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
|
||||
|
||||
SideEffects [Does not check the property in 0-th frame.]
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Int2_ManPerformInterpolation( Gia_Man_t * pInit, Int2_ManPars_t * pPars )
|
||||
{
|
||||
Int2_Man_t * p;
|
||||
int f, i, RetValue = -1;
|
||||
abctime clk, clkTotal = Abc_Clock(), timeTemp = 0;
|
||||
abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
|
||||
|
||||
// sanity checks
|
||||
assert( Gia_ManPiNum(pInit) > 0 );
|
||||
assert( Gia_ManPoNum(pInit) > 0 );
|
||||
assert( Gia_ManRegNum(pInit) > 0 );
|
||||
|
||||
// create manager
|
||||
p = Int2_ManCreate( pInit, pPars );
|
||||
|
||||
// create SAT solver
|
||||
p->pSatPref = sat_solver_new();
|
||||
sat_solver_setnvars( p->pSatPref, 1000 );
|
||||
sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop );
|
||||
|
||||
// check outputs in the first frame
|
||||
for ( i = 0; i < Gia_ManPoNum(pInit); i++ )
|
||||
Vec_IntPush( p->vPrefCos, i );
|
||||
Int2_ManCreateFrames( p, 0, p->vPrefCos );
|
||||
RetValue = Int2_ManCheckBmc( p, NULL );
|
||||
if ( RetValue != 1 )
|
||||
return RetValue;
|
||||
|
||||
// create original image
|
||||
for ( f = pPars->nFramesS; f < p->nFramesMax; f++ )
|
||||
{
|
||||
for ( i = 0; i < p->nFramesMax; i++ )
|
||||
{
|
||||
p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff );
|
||||
sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop );
|
||||
Vec_IntFreeP( &vImageOne );
|
||||
vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap );
|
||||
Vec_IntFree( vCoMap );
|
||||
Gia_ManStop( pGiaSuff );
|
||||
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
|
||||
return -1;
|
||||
if ( vImageOne == NULL )
|
||||
{
|
||||
if ( i == 0 )
|
||||
{
|
||||
printf( "Satisfiable in frame %d.\n", f );
|
||||
Vec_IntFree( vCiMap );
|
||||
sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
|
||||
return 0;
|
||||
}
|
||||
f += i;
|
||||
break;
|
||||
}
|
||||
Vec_IntAppend( vImagesAll, vImageOne );
|
||||
sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL;
|
||||
}
|
||||
Vec_IntFree( vCiMap );
|
||||
sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
|
||||
}
|
||||
Abc_PrintTime( "Time", Abc_Clock() - clk );
|
||||
|
||||
|
||||
p->timeSatPref += Abc_Clock() - clk;
|
||||
|
||||
Int2_ManStop( p );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,164 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2Int.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [Internal declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef ABC__Gia__int2__intInt_h
|
||||
#define ABC__Gia__int2__intInt_h
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "aig/gia/gia.h"
|
||||
#include "sat/bsat/satSolver.h"
|
||||
#include "sat/cnf/cnf.h"
|
||||
#include "int2.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// interpolation manager
|
||||
typedef struct Int2_Man_t_ Int2_Man_t;
|
||||
struct Int2_Man_t_
|
||||
{
|
||||
// parameters
|
||||
Int2_ManPars_t * pPars; // parameters
|
||||
// GIA managers
|
||||
Gia_Man_t * pGia; // original manager
|
||||
Gia_Man_t * pGiaPref; // prefix manager
|
||||
Gia_Man_t * pGiaSuff; // suffix manager
|
||||
// subset of the manager
|
||||
Vec_Int_t * vSuffCis; // suffix CIs
|
||||
Vec_Int_t * vSuffCos; // suffix COs
|
||||
Vec_Int_t * vPrefCos; // suffix POs
|
||||
Vec_Int_t * vStack; // temporary stack
|
||||
// preimages
|
||||
Vec_Int_t * vImageOne; // latest preimage
|
||||
Vec_Int_t * vImagesAll; // cumulative preimage
|
||||
// variable maps
|
||||
Vec_Ptr_t * vMapFrames; // mapping of GIA IDs into frame IDs
|
||||
Vec_Int_t * vMapPref; // mapping of flop inputs into SAT variables
|
||||
Vec_Int_t * vMapSuff; // mapping of flop outputs into SAT variables
|
||||
// initial minimization
|
||||
Vec_Int_t * vAssign; // assignment of PIs in pGiaSuff
|
||||
Vec_Int_t * vPrio; // priority of PIs in pGiaSuff
|
||||
// SAT solving
|
||||
sat_solver * pSatPref; // prefix solver
|
||||
sat_solver * pSatSuff; // suffix solver
|
||||
// runtime
|
||||
abctime timeSatPref;
|
||||
abctime timeSatSuff;
|
||||
abctime timeOther;
|
||||
abctime timeTotal;
|
||||
};
|
||||
|
||||
static inline Int2_Man_t * Int2_ManCreate( Gia_Man_t * pGia, Int2_ManPars_t * pPars )
|
||||
{
|
||||
Int2_Man_t * p;
|
||||
p = ABC_CALLOC( Int2_Man_t, 1 );
|
||||
p->pPars = pPars;
|
||||
p->pGia = pGia;
|
||||
p->pGiaPref = Gia_ManStart( 10000 );
|
||||
// perform structural hashing
|
||||
Gia_ManHashAlloc( pFrames );
|
||||
// subset of the manager
|
||||
p->vSuffCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
||||
p->vSuffCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
|
||||
p->vPrefCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
|
||||
p->vStack = Vec_IntAlloc( 10000 );
|
||||
// preimages
|
||||
p->vImageOne = Vec_IntAlloc( 1000 );
|
||||
p->vImagesAll = Vec_IntAlloc( 1000 );
|
||||
// variable maps
|
||||
p->vMapFrames = Vec_PtrAlloc( 100 );
|
||||
p->vMapPref = Vec_IntAlloc( Gia_ManRegNum(pGia) );
|
||||
p->vMapSuff = Vec_IntAlloc( Gia_ManRegNum(pGia) );
|
||||
// initial minimization
|
||||
p->vAssign = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
||||
p->vPrio = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
||||
return p;
|
||||
}
|
||||
static inline void Int2_ManStop( Int2_Man_t * p )
|
||||
{
|
||||
// GIA managers
|
||||
Gia_ManStopP( &p->pGiaPref );
|
||||
Gia_ManStopP( &p->pGiaSuff );
|
||||
// subset of the manager
|
||||
Vec_IntFreeP( &p->vSuffCis );
|
||||
Vec_IntFreeP( &p->vSuffCos );
|
||||
Vec_IntFreeP( &p->vPrefCos );
|
||||
Vec_IntFreeP( &p->vStack );
|
||||
// preimages
|
||||
Vec_IntFreeP( &p->vImageOne );
|
||||
Vec_IntFreeP( &p->vImagesAll );
|
||||
// variable maps
|
||||
Vec_VecFree( (Vec_Vec_t *)p->vMapFrames );
|
||||
Vec_IntFreeP( &p->vMapPref );
|
||||
Vec_IntFreeP( &p->vMapSuff );
|
||||
// initial minimization
|
||||
Vec_IntFreeP( &p->vAssign );
|
||||
Vec_IntFreeP( &p->vPrio );
|
||||
// SAT solving
|
||||
if ( p->pSatPref )
|
||||
sat_solver_delete( p->pSatPref );
|
||||
if ( p->timeSatSuff )
|
||||
sat_solver_delete( p->pSatSuff );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== int2Bmc.c =============================================================*/
|
||||
extern int Int2_ManCheckInit( Gia_Man_t * p );
|
||||
extern Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose );
|
||||
extern sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames );
|
||||
extern void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos );
|
||||
extern int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube );
|
||||
|
||||
/*=== int2Refine.c =============================================================*/
|
||||
extern Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio );
|
||||
|
||||
/*=== int2Util.c ============================================================*/
|
||||
extern Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop );
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,154 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2Refine.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [Various utilities.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2Refine.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "int2Int.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Int2_ManJustify_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSelect )
|
||||
{
|
||||
if ( pObj->fMark1 )
|
||||
return;
|
||||
pObj->fMark1 = 1;
|
||||
if ( Gia_ObjIsPi(p, pObj) )
|
||||
return;
|
||||
if ( Gia_ObjIsCo(pObj) )
|
||||
{
|
||||
Vec_IntPush( vSelect, Gia_ObjCioId(pObj) );
|
||||
return;
|
||||
}
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
if ( pObj->Value == 1 )
|
||||
{
|
||||
if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
|
||||
if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
|
||||
return;
|
||||
}
|
||||
if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
|
||||
{
|
||||
if ( Gia_ObjFanin0(pObj)->fMark0 <= Gia_ObjFanin1(pObj)->fMark0 ) // choice
|
||||
{
|
||||
if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
|
||||
}
|
||||
}
|
||||
else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
|
||||
{
|
||||
if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
|
||||
}
|
||||
else if ( (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
|
||||
{
|
||||
if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
|
||||
}
|
||||
else assert( 0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes the reduced set of flop variables.]
|
||||
|
||||
Description [Given is a single-output seq AIG manager and an assignment
|
||||
of its CIs. Returned is a subset of flops that justifies the output.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio )
|
||||
{
|
||||
Vec_Int_t * vSubset;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
// set values and prios
|
||||
assert( Gia_ManRegNum(p) > 0 );
|
||||
assert( Vec_IntSize(vAssign) == Vec_IntSize(vPrio) );
|
||||
Gia_ManConst0(p)->fMark0 = 0;
|
||||
Gia_ManConst0(p)->fMark1 = 0;
|
||||
Gia_ManConst0(p)->Value = ABC_INFINITY;
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
{
|
||||
pObj->fMark0 = Vec_IntEntry(vAssign, i);
|
||||
pObj->fMark1 = 0;
|
||||
pObj->Value = Vec_IntEntry(vPrio, i);
|
||||
}
|
||||
Gia_ManForEachAnd( p, pObj, i )
|
||||
{
|
||||
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
||||
pObj->fMark1 = 0;
|
||||
if ( pObj->fMark0 == 1 )
|
||||
pObj->Value = Abc_MaxInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
|
||||
else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
|
||||
pObj->Value = Abc_MinInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); // choice
|
||||
else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
|
||||
pObj->Value = Gia_ObjFanin0(pObj)->Value;
|
||||
else
|
||||
pObj->Value = Gia_ObjFanin1(pObj)->Value;
|
||||
}
|
||||
pObj = Gia_ManPo( p, 0 );
|
||||
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
|
||||
pObj->fMark1 = 0;
|
||||
pObj->Value = Gia_ObjFanin0(pObj)->Value;
|
||||
assert( pObj->fMark0 == 1 );
|
||||
assert( pObj->Value < ABC_INFINITY );
|
||||
// select subset
|
||||
vSubset = Vec_IntAlloc( 100 );
|
||||
Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSubset );
|
||||
return vSubset;
|
||||
}
|
||||
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,152 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [int2Util.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Interpolation engine.]
|
||||
|
||||
Synopsis [Various utilities.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
||||
|
||||
Revision [$Id: int2Util.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "int2Int.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Int2_ManComputeCoPres( Vec_Int_t * vSop, int nRegs )
|
||||
{
|
||||
Vec_Int_t * vCoPres, * vMap;
|
||||
vCoPres = Vec_IntAlloc( 100 );
|
||||
if ( vSop == NULL )
|
||||
Vec_IntPush( vCoPres, 0 );
|
||||
else
|
||||
{
|
||||
int i, k, Limit;
|
||||
vMap = Vec_IntStart( nRegs );
|
||||
Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
|
||||
{
|
||||
for ( k = 0; k < Limit; k++ )
|
||||
{
|
||||
i++;
|
||||
assert( Vec_IntEntry(vSop, i + k) < 2 * nRegs );
|
||||
Vec_IntWriteEntry( vMap, Abc_Lit2Var(Vec_IntEntry(vSop, i + k)), 1 );
|
||||
}
|
||||
}
|
||||
Vec_IntForEachEntry( vMap, Limit, i )
|
||||
if ( Limit )
|
||||
Vec_IntPush( vCoPres, i+1 );
|
||||
Vec_IntFree( vMap );
|
||||
}
|
||||
return vCoPres;
|
||||
}
|
||||
|
||||
void Int2_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
|
||||
{
|
||||
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
||||
return;
|
||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
return;
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(pObj), vNodes );
|
||||
Int2_ManCollectInternal_rec( p, Gia_ObjFanin1(pObj), vNodes );
|
||||
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
|
||||
}
|
||||
Vec_Int_t * Int2_ManCollectInternal( Gia_Man_t * p, Vec_Int_t * vCoPres )
|
||||
{
|
||||
Vec_Int_t * vNodes;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, Entry;
|
||||
Gia_ManIncrementTravId( p );
|
||||
Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||
vNodes = Vec_IntAlloc( 1000 );
|
||||
Vec_IntForEachEntry( vCoPres, Entry, i )
|
||||
Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(Gia_ManCo(p, Entry)), vNodes );
|
||||
return vNodes;
|
||||
}
|
||||
Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop )
|
||||
{
|
||||
Vec_Int_t * vCoPres, * vNodes;
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, k, Entry, Limit;
|
||||
int Lit, Cube, Sop;
|
||||
assert( Gia_ManPoNum(p) == 1 );
|
||||
// collect COs and ANDs
|
||||
vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) );
|
||||
vNodes = Int2_ManCollectInternal( p, vCoPres );
|
||||
// create new manager
|
||||
pNew = Gia_ManStart( Gia_ManObjNum(p) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCi(pNew);
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManForEachObjVec( vNodes, p, pObj, i )
|
||||
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
Vec_IntForEachEntry( vCoPres, Entry, i )
|
||||
{
|
||||
pObj = Gia_ManCo(p, Entry);
|
||||
pObj->Value = Gia_ObjFanin0Copy( pObj );
|
||||
}
|
||||
// create additional cubes
|
||||
Sop = 0;
|
||||
Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
|
||||
{
|
||||
Cube = 1;
|
||||
for ( k = 0; k < Limit; k++ )
|
||||
{
|
||||
i++;
|
||||
Lit = Vec_IntEntry( vSop, i + k );
|
||||
pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) );
|
||||
Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) );
|
||||
}
|
||||
Sop = Gia_ManHashOr( pNew, Sop, Cube );
|
||||
}
|
||||
Gia_ManAppendCo( pNew, Sop );
|
||||
Gia_ManHashStop( pNew );
|
||||
// cleanup
|
||||
pNew = Gia_ManCleanup( pTemp = pNew );
|
||||
Gia_ManStop( pTemp );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
SRC += src/proof/int2/int2Bmc.c \
|
||||
src/proof/int2/int2Core.c \
|
||||
src/proof/int2/int2Refine.c \
|
||||
src/proof/int2/int2Util.c
|
||||
Loading…
Reference in New Issue