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

1171 lines
39 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [giaSweeper.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Incremental SAT sweeper.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaSweeper.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "base/main/main.h"
#include "sat/bsat/satSolver.h"
#include "proof/ssc/ssc.h"
ABC_NAMESPACE_IMPL_START
/*
SAT sweeping/equivalence checking requires the following steps:
- Creating probes
These APIs should be called for all internal points in the logic, which may be used as
- nodes representing conditions to be used as constraints
- nodes representing functions to be equivalence checked
- nodes representing functions needed by the user at the end of SAT sweeping
Creating new probe using Gia_SweeperProbeCreate(): int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit );
Delete existing probe using Gia_SweeperProbeDelete(): int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId );
Update existing probe using Gia_SweeperProbeUpdate(): int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLit );
Comments:
- a probe is identified by its 0-based ID, which is returned by above procedures
- GIA literal of the probe is returned by int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
- Adding/removing conditions on the current path by calling Gia_SweeperCondPush() and Gia_SweeperCondPop()
extern void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId );
extern void Gia_SweeperCondPop( Gia_Man_t * p );
- Performing equivalence checking by calling int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
(resource limits, such as the number of conflicts, will be controllable by dedicated GIA APIs)
- The resulting AIG to be returned to the user by calling Gia_SweeperExtractUserLogic()
Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames )
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Swp_Man_t_ Swp_Man_t;
struct Swp_Man_t_
{
Gia_Man_t * pGia; // GIA manager under construction
int nConfMax; // conflict limit in seconds
int nTimeOut; // runtime limit in seconds
Vec_Int_t * vProbes; // probes
Vec_Int_t * vCondProbes; // conditions as probes
Vec_Int_t * vCondAssump; // conditions as SAT solver literals
// equivalence checking
sat_solver * pSat; // SAT solver
Vec_Int_t * vId2Lit; // mapping of Obj IDs into SAT literal
Vec_Int_t * vFront; // temporary frontier
Vec_Int_t * vFanins; // temporary fanins
Vec_Int_t * vCexSwp; // sweeper counter-example
Vec_Int_t * vCexUser; // user-visible counter-example
int nSatVars; // counter of SAT variables
// statistics
int nSatCalls;
int nSatCallsSat;
int nSatCallsUnsat;
int nSatCallsUndec;
int nSatProofs;
abctime timeStart;
abctime timeTotal;
abctime timeCnf;
abctime timeSat;
abctime timeSatSat;
abctime timeSatUnsat;
abctime timeSatUndec;
};
static inline int Swp_ManObj2Lit( Swp_Man_t * p, int Id ) { return Vec_IntGetEntry( p->vId2Lit, Id ); }
static inline int Swp_ManLit2Lit( Swp_Man_t * p, int Lit ) { assert( Vec_IntEntry(p->vId2Lit, Abc_Lit2Var(Lit)) ); return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit ); }
static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit ) { assert( Lit > 0 ); Vec_IntSetEntry( p->vId2Lit, Id, Lit ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creating/deleting the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
{
Swp_Man_t * p;
int Lit;
assert( pGia->pHTable != NULL );
pGia->pData = p = ABC_CALLOC( Swp_Man_t, 1 );
p->pGia = pGia;
p->nConfMax = 1000;
p->vProbes = Vec_IntAlloc( 100 );
p->vCondProbes = Vec_IntAlloc( 100 );
p->vCondAssump = Vec_IntAlloc( 100 );
p->vId2Lit = Vec_IntAlloc( 10000 );
p->vFront = Vec_IntAlloc( 100 );
p->vFanins = Vec_IntAlloc( 100 );
p->vCexSwp = Vec_IntAlloc( 100 );
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 0)) );
Lit = Abc_LitNot(Lit);
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
p->timeStart = Abc_Clock();
return p;
}
static inline void Swp_ManStop( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
sat_solver_delete( p->pSat );
Vec_IntFree( p->vFanins );
Vec_IntFree( p->vCexSwp );
Vec_IntFree( p->vId2Lit );
Vec_IntFree( p->vFront );
Vec_IntFree( p->vProbes );
Vec_IntFree( p->vCondProbes );
Vec_IntFree( p->vCondAssump );
ABC_FREE( p );
pGia->pData = NULL;
}
Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia )
{
if ( pGia == NULL )
pGia = Gia_ManStart( 10000 );
if ( pGia->pHTable == NULL )
Gia_ManHashStart( pGia );
// recompute fPhase and fMark1 to mark multiple fanout nodes if AIG is already defined!!!
Swp_ManStart( pGia );
pGia->fSweeper = 1;
return pGia;
}
void Gia_SweeperStop( Gia_Man_t * pGia )
{
pGia->fSweeper = 0;
Swp_ManStop( pGia );
Gia_ManHashStop( pGia );
// Gia_ManStop( pGia );
}
int Gia_SweeperIsRunning( Gia_Man_t * pGia )
{
return (pGia->pData != NULL);
}
double Gia_SweeperMemUsage( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
double nMem = sizeof(Swp_Man_t);
nMem += Vec_IntCap(p->vProbes);
nMem += Vec_IntCap(p->vCondProbes);
nMem += Vec_IntCap(p->vCondAssump);
nMem += Vec_IntCap(p->vId2Lit);
nMem += Vec_IntCap(p->vFront);
nMem += Vec_IntCap(p->vFanins);
nMem += Vec_IntCap(p->vCexSwp);
return 4.0 * nMem;
}
void Gia_SweeperPrintStats( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
double nMemSwp = Gia_SweeperMemUsage(pGia);
double nMemGia = (double)Gia_ManObjNum(pGia)*(sizeof(Gia_Obj_t) + sizeof(int));
double nMemSat = sat_solver_memory(p->pSat);
double nMemTot = nMemSwp + nMemGia + nMemSat;
printf( "SAT sweeper statistics:\n" );
printf( "Memory usage:\n" );
ABC_PRMP( "Sweeper ", nMemSwp, nMemTot );
ABC_PRMP( "AIG manager ", nMemGia, nMemTot );
ABC_PRMP( "SAT solver ", nMemSat, nMemTot );
ABC_PRMP( "TOTAL ", nMemTot, nMemTot );
printf( "Runtime usage:\n" );
p->timeTotal = Abc_Clock() - p->timeStart;
ABC_PRTP( "CNF construction", p->timeCnf, p->timeTotal );
ABC_PRTP( "SAT solving ", p->timeSat, p->timeTotal );
ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal );
ABC_PRTP( " Unsat ", p->timeSatUnsat, p->timeTotal );
ABC_PRTP( " Undecided ", p->timeSatUndec, p->timeTotal );
ABC_PRTP( "TOTAL RUNTIME ", p->timeTotal, p->timeTotal );
printf( "GIA: " );
Gia_ManPrintStats( pGia, NULL );
printf( "SAT calls = %d. Sat = %d. Unsat = %d. Undecided = %d. Proofs = %d.\n",
p->nSatCalls, p->nSatCallsSat, p->nSatCallsUnsat, p->nSatCallsUndec, p->nSatProofs );
Sat_SolverPrintStats( stdout, p->pSat );
}
/**Function*************************************************************
Synopsis [Setting resource limits.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_SweeperSetConflictLimit( Gia_Man_t * p, int nConfMax )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
pSwp->nConfMax = nConfMax;
}
void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
pSwp->nTimeOut = nSeconds;
}
Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
assert( pSwp->vCexUser == NULL || Vec_IntSize(pSwp->vCexUser) == Gia_ManPiNum(p) );
return pSwp->vCexUser;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
// create new probe
int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
int ProbeId = Vec_IntSize(pSwp->vProbes);
assert( iLit >= 0 );
Vec_IntPush( pSwp->vProbes, iLit );
return ProbeId;
}
// delete existing probe
int Gia_SweeperProbeDelete( Gia_Man_t * p, int ProbeId )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
assert( iLit >= 0 );
Vec_IntWriteEntry(pSwp->vProbes, ProbeId, -1);
return iLit;
}
// update existing probe
int Gia_SweeperProbeUpdate( Gia_Man_t * p, int ProbeId, int iLitNew )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
assert( iLit >= 0 );
Vec_IntWriteEntry(pSwp->vProbes, ProbeId, iLitNew);
return iLit;
}
// returns literal associated with the probe
int Gia_SweeperProbeLit( Gia_Man_t * p, int ProbeId )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
int iLit = Vec_IntEntry(pSwp->vProbes, ProbeId);
assert( iLit >= 0 );
return iLit;
}
/**Function*************************************************************
Synopsis [This procedure returns indexes of all currently defined valid probes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_SweeperCollectValidProbeIds( Gia_Man_t * p )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
Vec_Int_t * vProbeIds = Vec_IntAlloc( 1000 );
int iLit, ProbeId;
Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
{
if ( iLit < 0 ) continue;
Vec_IntPush( vProbeIds, ProbeId );
}
return vProbeIds;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_SweeperCondPush( Gia_Man_t * p, int ProbeId )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
Vec_IntPush( pSwp->vCondProbes, ProbeId );
}
int Gia_SweeperCondPop( Gia_Man_t * p )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
return Vec_IntPop( pSwp->vCondProbes );
}
Vec_Int_t * Gia_SweeperCondVector( Gia_Man_t * p )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
return pSwp->vCondProbes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjIds )
{
if ( !Gia_ObjIsAnd(pObj) )
return;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
Gia_ManExtract_rec( p, Gia_ObjFanin0(pObj), vObjIds );
Gia_ManExtract_rec( p, Gia_ObjFanin1(pObj), vObjIds );
Vec_IntPush( vObjIds, Gia_ObjId(p, pObj) );
}
Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vInNames, Vec_Ptr_t * vOutNames )
{
Vec_Int_t * vObjIds, * vValues;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, ProbeId;
assert( vInNames == NULL || Gia_ManPiNum(p) == Vec_PtrSize(vInNames) );
assert( vOutNames == NULL || Vec_IntSize(vProbeIds) == Vec_PtrSize(vOutNames) );
// create new
Gia_ManIncrementTravId( p );
vObjIds = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vProbeIds, ProbeId, i )
{
pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
}
// create new manager
pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + Vec_IntSize(vProbeIds) + 100 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create internal nodes
Gia_ManHashStart( pNew );
vValues = Vec_IntAlloc( Vec_IntSize(vObjIds) );
Gia_ManForEachObjVec( vObjIds, p, pObj, i )
{
Vec_IntPush( vValues, pObj->Value );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_ManHashStop( pNew );
// create outputs
Vec_IntForEachEntry( vProbeIds, ProbeId, i )
{
pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
Gia_ManAppendCo( pNew, Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj) );
}
// return the values back
Gia_ManForEachPi( p, pObj, i )
pObj->Value = 0;
Gia_ManForEachObjVec( vObjIds, p, pObj, i )
pObj->Value = Vec_IntEntry( vValues, i );
Vec_IntFree( vObjIds );
Vec_IntFree( vValues );
// duplicate if needed
if ( Gia_ManHasDangling(pNew) )
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
}
// copy names if present
if ( vInNames )
pNew->vNamesIn = Vec_PtrDupStr( vInNames );
if ( vOutNames )
pNew->vNamesOut = Vec_PtrDupStr( vOutNames );
return pNew;
}
/**Function*************************************************************
Synopsis [Sweeper cleanup.]
Description [Returns new GIA with sweeper defined, which is the same
as the original sweeper, with all the dangling logic removed and SAT
solver restarted. The probe IDs are guaranteed to have the same logic
functions as in the original manager.]
SideEffects [The input manager is deleted inside this procedure.]
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_SweeperCleanup( Gia_Man_t * p, char * pCommLime )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
Vec_Int_t * vObjIds;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit, ProbeId;
// collect all internal nodes pointed to by currently-used probes
Gia_ManIncrementTravId( p );
vObjIds = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
{
if ( iLit < 0 ) continue;
pObj = Gia_Lit2Obj( p, iLit );
Gia_ManExtract_rec( p, Gia_Regular(pObj), vObjIds );
}
// create new manager
pNew = Gia_ManStart( 1 + Gia_ManPiNum(p) + Vec_IntSize(vObjIds) + 100 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
// create internal nodes
Gia_ManHashStart( pNew );
Gia_ManForEachObjVec( vObjIds, p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManHashStop( pNew );
// create outputs
Vec_IntForEachEntry( pSwp->vProbes, iLit, ProbeId )
{
if ( iLit < 0 ) continue;
pObj = Gia_Lit2Obj( p, iLit );
iLit = Gia_Regular(pObj)->Value ^ Gia_IsComplement(pObj);
Vec_IntWriteEntry( pSwp->vProbes, ProbeId, iLit );
}
Vec_IntFree( vObjIds );
// duplicate if needed
if ( Gia_ManHasDangling(pNew) )
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
}
// execute command line
if ( pCommLime )
{
// set pNew to be current GIA in ABC
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
// execute command line pCommLine using Abc_CmdCommandExecute()
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
// get pNew to be current GIA in ABC
pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
}
// restart the SAT solver
Vec_IntClear( pSwp->vId2Lit );
sat_solver_delete( pSwp->pSat );
pSwp->pSat = sat_solver_new();
pSwp->nSatVars = 1;
sat_solver_setnvars( pSwp->pSat, 1000 );
Swp_ManSetObj2Lit( pSwp, 0, (iLit = Abc_Var2Lit(pSwp->nSatVars++, 0)) );
iLit = Abc_LitNot(iLit);
sat_solver_addclause( pSwp->pSat, &iLit, &iLit + 1 );
pSwp->timeStart = Abc_Clock();
// return the result
pNew->pData = p->pData; p->pData = NULL;
Gia_ManStop( p );
return pNew;
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Gia_ManAddClausesMux( Swp_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], LitF, LitI, LitT, LitE, RetValue;
assert( !Gia_IsComplement( pNode ) );
assert( Gia_ObjIsMuxType( pNode ) );
// get nodes (I = if, T = then, E = else)
pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the Litiable numbers
LitF = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
LitI = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeI) );
LitT = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeT) );
LitE = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeE) );
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
pLits[0] = Abc_LitNotCond(LitI, 1);
pLits[1] = Abc_LitNotCond(LitT, 1);
pLits[2] = Abc_LitNotCond(LitF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = Abc_LitNotCond(LitI, 1);
pLits[1] = Abc_LitNotCond(LitT, 0);
pLits[2] = Abc_LitNotCond(LitF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = Abc_LitNotCond(LitI, 0);
pLits[1] = Abc_LitNotCond(LitE, 1);
pLits[2] = Abc_LitNotCond(LitF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = Abc_LitNotCond(LitI, 0);
pLits[1] = Abc_LitNotCond(LitE, 0);
pLits[2] = Abc_LitNotCond(LitF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
if ( LitT == LitE )
{
// assert( fCompT == !fCompE );
return;
}
pLits[0] = Abc_LitNotCond(LitT, 0);
pLits[1] = Abc_LitNotCond(LitE, 0);
pLits[2] = Abc_LitNotCond(LitF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = Abc_LitNotCond(LitT, 1);
pLits[1] = Abc_LitNotCond(LitE, 1);
pLits[2] = Abc_LitNotCond(LitF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Gia_ManAddClausesSuper( Swp_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
{
int i, RetValue, Lit, LitNode, pLits[2];
assert( !Gia_IsComplement(pNode) );
assert( Gia_ObjIsAnd( pNode ) );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
// add !B => !C or B + !C
LitNode = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
Vec_IntForEachEntry( vSuper, Lit, i )
{
pLits[0] = Swp_ManLit2Lit( p, Lit );
pLits[1] = Abc_LitNot( LitNode );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// update literals
Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
}
// add A & B => C or !A + !B + C
Vec_IntPush( vSuper, LitNode );
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) );
assert( RetValue );
(void) RetValue;
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
{
// stop at complements, shared, PIs, and MUXes
if ( Gia_IsComplement(pObj) || pObj->fMark1 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
{
Vec_IntPushUnique( vSuper, Gia_Obj2Lit(p, pObj) );
return;
}
Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
}
static void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
{
assert( !Gia_IsComplement(pObj) );
assert( Gia_ObjIsAnd(pObj) );
Vec_IntClear( vSuper );
Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper );
Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper );
}
/**Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Gia_ManObjAddToFrontier( Swp_Man_t * p, int Id, Vec_Int_t * vFront )
{
Gia_Obj_t * pObj;
if ( Id == 0 || Swp_ManObj2Lit(p, Id) )
return;
pObj = Gia_ManObj( p->pGia, Id );
Swp_ManSetObj2Lit( p, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) );
sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vFront, Id );
}
static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
{
Gia_Obj_t * pNode;
int i, k, Id, Lit;
abctime clk;
// quit if CNF is ready
if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
return;
clk = Abc_Clock();
// start the frontier
Vec_IntClear( p->vFront );
Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
// explore nodes in the frontier
Gia_ManForEachObjVec( p->vFront, p->pGia, pNode, i )
{
// create the supergate
assert( Swp_ManObj2Lit(p, Gia_ObjId(p->pGia, pNode)) );
if ( Gia_ObjIsMuxType(pNode) )
{
Vec_IntClear( p->vFanins );
Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin0(pNode) ) );
Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin1(pNode) ) );
Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin0(pNode) ) );
Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin1(pNode) ) );
Vec_IntForEachEntry( p->vFanins, Id, k )
Gia_ManObjAddToFrontier( p, Id, p->vFront );
Gia_ManAddClausesMux( p, pNode );
}
else
{
Gia_ManCollectSuper( p->pGia, pNode, p->vFanins );
Vec_IntForEachEntry( p->vFanins, Lit, k )
Gia_ManObjAddToFrontier( p, Abc_Lit2Var(Lit), p->vFront );
Gia_ManAddClausesSuper( p, pNode, p->vFanins );
}
assert( Vec_IntSize(p->vFanins) > 1 );
}
p->timeCnf += Abc_Clock() - clk;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_solver * pSat, Vec_Int_t * vCex )
{
Gia_Obj_t * pObj;
int i, LitSat, Value;
Vec_IntClear( vCex );
Gia_ManForEachPi( pGia, pObj, i )
{
LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) );
if ( LitSat == 0 )
{
Vec_IntPush( vCex, 2 );
continue;
}
assert( LitSat > 0 );
Value = sat_solver_var_value(pSat, Abc_Lit2Var(LitSat)) ^ Abc_LitIsCompl(LitSat);
Vec_IntPush( vCex, Value );
}
return vCex;
}
/**Function*************************************************************
Synopsis [Runs equivalence test for probes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int iLitOld, iLitNew, iLitAig, pLitsSat[2], RetValue, RetValue1, ProbeId, i;
abctime clk;
p->nSatCalls++;
assert( p->pSat != NULL );
p->vCexUser = NULL;
// get the literals
iLitOld = Gia_SweeperProbeLit( pGia, Probe1 );
iLitNew = Gia_SweeperProbeLit( pGia, Probe2 );
// if the literals are identical, the probes are equivalent
if ( iLitOld == iLitNew )
return 1;
// if the literals are opposites, the probes are not equivalent
if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) )
{
Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 2 );
p->vCexUser = p->vCexSwp;
return 0;
}
// order the literals
if ( iLitOld < iLitNew )
ABC_SWAP( int, iLitOld, iLitNew );
assert( iLitOld > iLitNew );
// create logic cones and the array of assumptions
Vec_IntClear( p->vCondAssump );
Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
{
iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
}
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
sat_solver_compress( p->pSat );
// set the SAT literals
pLitsSat[0] = Swp_ManLit2Lit( p, iLitOld );
pLitsSat[1] = Swp_ManLit2Lit( p, iLitNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
Vec_IntPush( p->vCondAssump, pLitsSat[0] );
Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[1]) );
// set runtime limit for this call
if ( p->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
pLitsSat[0] = Abc_LitNot( pLitsSat[0] );
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}
// if the old node was constant 0, we already know the answer
if ( Gia_ManIsConstLit(iLitNew) )
{
p->nSatProofs++;
return 1;
}
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[0]) );
Vec_IntPush( p->vCondAssump, pLitsSat[1] );
clk = Abc_Clock();
RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Vec_IntShrink( p->vCondAssump, Vec_IntSize(p->vCondAssump) - 2 );
p->timeSat += Abc_Clock() - clk;
if ( RetValue1 == l_False )
{
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
assert( RetValue );
pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}
// return SAT proof
p->nSatProofs++;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int RetValue, ProbeId, iLitAig, i;
abctime clk;
assert( p->pSat != NULL );
p->nSatCalls++;
p->vCexUser = NULL;
// create logic cones and the array of assumptions
Vec_IntClear( p->vCondAssump );
Vec_IntForEachEntry( p->vCondProbes, ProbeId, i )
{
iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
}
sat_solver_compress( p->pSat );
// set runtime limit for this call
if ( p->nTimeOut )
sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
clk = Abc_Clock();
RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
if ( RetValue == l_False )
{
assert( Vec_IntSize(p->vCondProbes) > 0 );
p->timeSatUnsat += Abc_Clock() - clk;
p->nSatCallsUnsat++;
p->nSatProofs++;
return 1;
}
else if ( RetValue == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += Abc_Clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += Abc_Clock() - clk;
p->nSatCallsUndec++;
return -1;
}
}
/**Function*************************************************************
Synopsis [Performs grafting from another manager.]
Description [Returns the array of resulting literals in the destination manager.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc )
{
Vec_Int_t * vOutLits;
Gia_Obj_t * pObj;
int i;
assert( Gia_SweeperIsRunning(pDst) );
if ( vProbes )
assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) );
else
assert( Gia_ManPiNum(pDst) == Gia_ManPiNum(pSrc) );
Gia_ManForEachPi( pSrc, pObj, i )
pObj->Value = vProbes ? Gia_SweeperProbeLit(pDst, Vec_IntEntry(vProbes, i)) : Gia_Obj2Lit(pDst,Gia_ManPi(pDst, i));
Gia_ManForEachAnd( pSrc, pObj, i )
pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) );
Gia_ManForEachPo( pSrc, pObj, i )
Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) );
return vOutLits;
}
/**Function*************************************************************
Synopsis [Verification of the sweeper.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
{
Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 );
Gia_ManStop( pConstr );
Gia_ManStop( pMiter );
return 1;
}
/**Function*************************************************************
Synopsis [Performs conditional sweeping of the cone.]
Description [Returns the result as a new GIA manager with as many inputs
as the original manager and as many outputs as there are logic cones.]
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords, int nConfs, int fVerbose )
{
Vec_Int_t * vProbeConds;
Gia_Man_t * pGiaCond, * pGiaOuts, * pGiaRes;
Ssc_Pars_t Pars, * pPars = &Pars;
Ssc_ManSetDefaultParams( pPars );
pPars->nWords = nWords;
pPars->nBTLimit = nConfs;
pPars->fVerbose = fVerbose;
// sweeper is running
assert( Gia_SweeperIsRunning(p) );
// extract conditions and logic cones
vProbeConds = Gia_SweeperCondVector( p );
pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
Gia_ManSetPhase( pGiaOuts );
// if there is no conditions, define constant true constraint (constant 0 output)
if ( Gia_ManPoNum(pGiaCond) == 0 )
Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
// perform sweeping under constraints
pGiaRes = Ssc_PerformSweeping( pGiaOuts, pGiaCond, pPars );
Gia_ManStop( pGiaCond );
Gia_ManStop( pGiaOuts );
return pGiaRes;
}
/**Function*************************************************************
Synopsis [Procedure to perform conditional fraig sweeping on separate logic cones.]
Description [The procedure takes GIA with the sweeper defined. The sweeper
is assumed to have some conditions currently pushed, which will be used
as constraints for fraig sweeping. The second argument (vProbes) contains
the array of probe IDs pointing to the user's logic cones to be SAT swept.
Finally, the optional command line (pCommLine) is an ABC command line
to be applied to the resulting GIA after SAT sweeping before it is
grafted back into the original GIA manager. The return value is the status
(success/failure) and the array of original probes possibly pointing to the
new literals in the original GIA manager, corresponding to the user's
logic cones after sweeping, synthesis and grafting.]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperFraig( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int nWords, int nConfs, int fVerbose )
{
Gia_Man_t * pNew;
Vec_Int_t * vLits;
int ProbeId, i;
// sweeper is running
assert( Gia_SweeperIsRunning(p) );
// sweep the logic
pNew = Gia_SweeperSweep( p, vProbeIds, nWords, nConfs, fVerbose );
if ( pNew == NULL )
return 0;
// execute command line
if ( pCommLime )
{
// set pNew to be current GIA in ABC
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
// execute command line pCommLine using Abc_CmdCommandExecute()
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
// get pNew to be current GIA in ABC
pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
}
// return logic back into the main manager
vLits = Gia_SweeperGraft( p, NULL, pNew );
Gia_ManStop( pNew );
// update the array of probes
Vec_IntForEachEntry( vProbeIds, ProbeId, i )
Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
Vec_IntFree( vLits );
return 1;
}
/**Function*************************************************************
Synopsis [Executes given command line for the logic defined by the probes.]
Description [ ]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperRun( Gia_Man_t * p, Vec_Int_t * vProbeIds, char * pCommLime, int fVerbose )
{
Gia_Man_t * pNew;
Vec_Int_t * vLits;
int ProbeId, i;
// sweeper is running
assert( Gia_SweeperIsRunning(p) );
// sweep the logic
pNew = Gia_SweeperExtractUserLogic( p, vProbeIds, NULL, NULL );
// execute command line
if ( pCommLime )
{
if ( fVerbose )
printf( "GIA manager statistics before and after applying \"%s\":\n", pCommLime );
if ( fVerbose )
Gia_ManPrintStats( pNew, NULL );
// set pNew to be current GIA in ABC
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
// execute command line pCommLine using Abc_CmdCommandExecute()
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), pCommLime );
// get pNew to be current GIA in ABC
pNew = Abc_FrameGetGia( Abc_FrameGetGlobalFrame() );
if ( fVerbose )
Gia_ManPrintStats( pNew, NULL );
}
// return logic back into the main manager
vLits = Gia_SweeperGraft( p, NULL, pNew );
Gia_ManStop( pNew );
// update the array of probes
Vec_IntForEachEntry( vProbeIds, ProbeId, i )
Gia_SweeperProbeUpdate( p, ProbeId, Vec_IntEntry(vLits, i) );
Vec_IntFree( vLits );
return 1;
}
/**Function*************************************************************
Synopsis [Sweeper sweeper test.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * pInit, int nWords, int nConfs, int fVerbose )
{
Gia_Man_t * p, * pGia;
Gia_Obj_t * pObj;
Vec_Int_t * vOuts;
int i;
// add one-hotness constraints
p = Gia_ManDupOneHot( pInit );
// create sweeper
Gia_SweeperStart( p );
// collect outputs and create conditions
vOuts = Vec_IntAlloc( Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
if ( i < Gia_ManPoNum(p) - p->nConstrs ) // this is the user's output
Vec_IntPush( vOuts, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
else // this is a constraint
Gia_SweeperCondPush( p, Gia_SweeperProbeCreate( p, Gia_ObjFaninLit0p(p, pObj) ) );
// perform the sweeping
pGia = Gia_SweeperSweep( p, vOuts, nWords, nConfs, fVerbose );
// pGia = Gia_ManDup( p );
Vec_IntFree( vOuts );
// sop the sweeper
Gia_SweeperStop( p );
Gia_ManStop( p );
return pGia;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink