Skip to content

A
abc
Commit 092c7be0 by Alan Mishchenko
Options

Version abc80905

parent 73c8aa7c
Showing with 307 additions and 121 deletions
src/aig/dch/dchMan.c
......@@ -170,16 +170,21 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
Lit = toLit( 1 );
p->nSatVars = 1;
// p->nSatVars = 0;
Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
p->nSatVars = 2;
Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );
p->nRecycles++;
p->nCallsSince = 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/dch/dchSimSat.c
......@@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
if ( Aig_ObjIsPi(pObj) )
{
Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj );
int nVarNum = Dch_ObjSatNum( p, pObjFraig );
Aig_Obj_t * pObjFraig;
int nVarNum;
pObjFraig = Dch_ObjFraig( pObj );
assert( !Aig_IsComplement(pObjFraig) );
nVarNum = Dch_ObjSatNum( p, pObjFraig );
// get the value from the SAT solver
// (account for the fact that some vars may be minimized away)
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
......
src/aig/fra/fraClass.c
......@@ -296,7 +296,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// skip the node with more that the given number of levels
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
// hash the node by its simulation info
......
src/aig/fra/fraInd.c
......@@ -505,6 +505,7 @@ PRT( "Time", clock() - clk );
int nLitsOld = Fra_ClassesCountLits(p->pCla);
int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
int clk3 = clock();
if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
{
......@@ -571,7 +572,7 @@ p->timeTrav += clock() - clk2;
// report the intermediate results
if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
......@@ -579,7 +580,8 @@ p->timeTrav += clock() - clk2;
if ( p->pPars->fUse1Hot )
printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
printf( "\n" );
PRT( "T", clock() - clk3 );
// printf( "\n" );
}
// perform sweeping
......
src/aig/ivy/ivyFraig.c
......@@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk;
int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
{
int pLits[2], RetValue1, clk;
// int RetValue;
int RetValue;
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
......@@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk;
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
// RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
// assert( RetValue );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
......@@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t *
Ivy_ObjSetFaninVec( pNode, vFanins );
}
Vec_PtrFree( vFrontier );
sat_solver_simplify( p->pSat );
}
/**Function*************************************************************
......
src/aig/ssw/sswAig.c
......@@ -44,7 +44,8 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
// skip nodes without representative
if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
pObjRepr = Aig_ObjRepr(pAig, pObj);
if ( pObjRepr == NULL )
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
......@@ -53,16 +54,26 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// get the new node of the representative
pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
if ( pObj->fPhase == pObjRepr->fPhase )
{
assert( pObjNew != Aig_Not(pObjReprNew) );
if ( pObjNew == pObjReprNew )
return;
}
else
{
assert( pObjNew != pObjReprNew );
if ( pObjNew == Aig_Not(pObjReprNew) )
return;
}
p->nConstrReduced++;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
// add the constraint
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) );
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) );
Aig_ObjCreatePo( pFrames, pObjNew2 );
Aig_ObjCreatePo( pFrames, pObjNew );
}
/**Function*************************************************************
......@@ -80,7 +91,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
int i, k, f;
int i, f;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
......@@ -90,18 +101,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < p->pPars->nFramesK; f++ )
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// map constant nodes
for ( f = 0; f < p->pPars->nFramesK; f++ )
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
// add timeframes
p->nConstrTotal = p->nConstrReduced = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
......@@ -113,7 +120,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
}
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
}
// add the POs for the latch outputs of the last frame
......@@ -124,6 +131,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Aig_ManCleanup( pFrames );
// make sure the satisfying assignment is node assigned
assert( pFrames->pData == NULL );
//Aig_ManShow( pFrames, 0, NULL );
return pFrames;
}
......
src/aig/ssw/sswClass.c
......@@ -425,15 +425,15 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
if ( fLatchCorr )
{
if ( !Aig_ObjIsPi(pObj) )
if ( !Saig_ObjIsPi(p->pAig, pObj) )
continue;
}
else
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsPi(p->pAig, pObj) )
continue;
// skip the node with more that the given number of levels
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
// check if the node belongs to the class of constant 1
......@@ -556,7 +556,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
p = Ssw_ClassesStart( pAig );
// go through the nodes
p->nCands1 = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
Aig_ManForEachObj( pAig, pObj, i )
{
if ( fLatchCorr )
{
......@@ -568,10 +568,10 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
continue;
// skip the node with more that the given number of levels
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
continue;
}
Ssw_ObjSetConst1Cand( p->pAig, pObj );
Ssw_ObjSetConst1Cand( pAig, pObj );
p->nCands1++;
}
// allocate room for classes
......@@ -708,6 +708,53 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
return 1;
}
/**Function*************************************************************
Synopsis [Refine the group of constant 1 nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
{
Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
int i;
// collect the nodes to be refined
Vec_PtrClear( p->vClassNew );
for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
{
pObj = Aig_ManObj( p->pAig, i );
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
Vec_PtrPush( p->vClassNew, pObj );
}
// check if there is a new class
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
p->nCands1 -= Vec_PtrSize(p->vClassNew);
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
if ( Vec_PtrSize(p->vClassNew) == 1 )
return 1;
// create a new class composed of these nodes
ppClassNew = p->pMemClassesFree;
p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
Vec_PtrForEachEntry( p->vClassNew, pObj, i )
{
ppClassNew[i] = pObj;
Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
}
Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
// refine them recursively
if ( fRecursive )
return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/ssw/sswCore.c
......@@ -48,7 +48,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
p->fLatchCorr = 1; // performs register correspondence
p->fVerbose = 1; // verbose stats
p->nIters = 0; // the number of iterations performed
}
......@@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
Aig_Man_t * pAigNew;
Ssw_Man_t * p;
int RetValue, nIter, clk, clkTotal = clock();
// reset random numbers
......@@ -75,27 +76,33 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// compute candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
// refine classes using BMC
Ssw_ClassesPrint( p->ppClasses, 0 );
if ( pPars->fVerbose )
Ssw_ClassesPrint( p->ppClasses, 0 );
Ssw_ManSweepBmc( p );
Ssw_ClassesPrint( p->ppClasses, 0 );
Ssw_ManCleanup( p );
if ( pPars->fVerbose )
Ssw_ClassesPrint( p->ppClasses, 0 );
// refine classes using induction
for ( nIter = 0; ; nIter++ )
{
clk = clock();
RetValue = Ssw_ManSweep(p);
RetValue = Ssw_ManSweep( p );
if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. NR = %6d. ",
printf( "%3d : Const = %6d. Cl = %6d. L = %6d. LR = %6d. NR = %6d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrTotal, p->nConstrReduced, p->nFrameNodes );
p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
PRT( "T", clock() - clk );
}
Ssw_ManCleanup( p );
if ( !RetValue )
break;
}
}
p->timeTotal = clock() - clkTotal;
Ssw_ManStop( p );
return Aig_ManDupRepr( pAig, 0 );
pAigNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswInt.h
......@@ -55,7 +55,6 @@ struct Ssw_Man_t_
Aig_Man_t * pAig; // user-given AIG
Aig_Man_t * pFrames; // final AIG
Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
int nFrameNodes; // the number of nodes in the timeframes
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
// Aig_Obj_t ** pReprsProved; // equivalences proved
......@@ -70,6 +69,7 @@ struct Ssw_Man_t_
// constraints
int nConstrTotal; // the number of total constraints
int nConstrReduced; // the number of reduced constraints
int nStragers;
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
......@@ -136,6 +136,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr,
extern int Ssw_ClassesRefine( Ssw_Cla_t * p );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
/*=== sswCnf.c ===================================================*/
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswMan.c ===================================================*/
......@@ -148,6 +149,7 @@ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSimSat.c ===================================================*/
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
......
src/aig/ssw/sswMan.c
......@@ -42,22 +42,25 @@
Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
// prepare the sequential AIG
assert( Saig_ManRegNum(pAig) > 0 );
Aig_ManFanoutStart( pAig );
Aig_ManSetPioNumbers( pAig );
// create interpolation manager
p = ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) );
p->pPars = pPars;
p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1;
Aig_ManFanoutStart( pAig );
p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving
p->nSatVars = 1;
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) );
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames );
p->vFanins = Vec_PtrAlloc( 100 );
p->vSimRoots = Vec_PtrAlloc( 1000 );
p->vSimClasses = Vec_PtrAlloc( 1000 );
// equivalences proved
// p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
return p;
}
......@@ -97,21 +100,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n",
p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs );
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) );
printf( "SAT solver: Vars = %d.\n", p->nSatVars );
printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n",
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. SAT vars = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVars );
printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d. Equivs = %d. Str = %d.\n",
p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal,
p->nSatCallsSat, p->nSatFailsReal );
printf( "Equivs : All = %6d.\n", Ssw_ManCountEquivs(p) );
p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStragers );
printf( "Runtime statistics:\n" );
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
PRTP( "BMC ", p->timeBmc, p->timeTotal );
PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
PRTP( "SAT solving", p->timeSat, p->timeTotal );
PRTP( " sat ", p->timeSatSat, p->timeTotal );
PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
PRTP( " sat ", p->timeSatSat, p->timeTotal );
PRTP( " undecided", p->timeSatUndec, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
......@@ -135,14 +136,15 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
{
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->pSat )
{
sat_solver_delete( p->pSat );
p->pSat = NULL;
p->nSatVars = 0;
// p->nSatVars = 0;
memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
p->nConstrTotal = 0;
p->nConstrReduced = 0;
}
......@@ -192,11 +194,12 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
sat_solver_setnvars( p->pSat, 10000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
Lit = toLit( 1 );
p->nSatVars = 1;
Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
p->nSatVars = 2;
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswSat.c
......@@ -32,7 +32,7 @@
Synopsis [Runs equivalence test for the two nodes.]
Description []
Description [Both nodes should be regular and different from each other.]
SideEffects []
......@@ -42,13 +42,13 @@
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
int pLits[2], RetValue, RetValue1, status, clk;
int pLits[2], RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
// sanity checks
assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
assert( !Aig_IsComplement(pNew) );
assert( pOld != pNew );
if ( p->pSat == NULL )
Ssw_ManStartSolver( p );
......@@ -57,14 +57,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
Ssw_CnfNodeAddToSolver( p, pOld );
Ssw_CnfNodeAddToSolver( p, pNew );
// propagate unit clauses
if ( p->pSat->qtail != p->pSat->qhead )
{
status = sat_solver_simplify(p->pSat);
assert( status != 0 );
assert( p->pSat->qtail == p->pSat->qhead );
}
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
......@@ -75,6 +67,10 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
......@@ -117,6 +113,10 @@ p->timeSatUndec += clock() - clk;
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
......@@ -160,23 +160,45 @@ p->timeSatUndec += clock() - clk;
***********************************************************************/
int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int pLits[2], RetValue;
int pLits[2], RetValue, fComplNew;
Aig_Obj_t * pTemp;
// sanity checks
assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
// move constant to the old node
if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
{
assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
pTemp = pOld;
pOld = pNew;
pNew = pTemp;
}
// move complement to the new node
if ( Aig_IsComplement(pOld) )
{
pOld = Aig_Regular(pOld);
pNew = Aig_Not(pNew);
}
// start the solver
if ( p->pSat == NULL )
Ssw_ManStartSolver( p );
// if the nodes do not have SAT variables, allocate them
Ssw_CnfNodeAddToSolver( p, pOld );
Ssw_CnfNodeAddToSolver( p, pNew );
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) );
// transform the new node
fComplNew = Aig_IsComplement( pNew );
pNew = Aig_Regular( pNew );
// consider the constant 1 case
if ( pOld == Aig_ManConst1(p->pFrames) )
{
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
// add constaint A = 1 ----> A
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
......@@ -186,10 +208,11 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
}
else
{
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
// add constaint A = B ----> (A v !B)(!A v B)
// (A v !B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
......@@ -200,10 +223,9 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
// (!A v B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
......@@ -214,16 +236,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
/*
// propagate unit clauses
if ( p->pSat->qtail != p->pSat->qhead )
{
int status;
status = sat_solver_simplify(p->pSat);
assert( status != 0 );
assert( p->pSat->qtail == p->pSat->qhead );
}
*/
return 1;
}
......
src/aig/ssw/sswSimSat.c
......@@ -92,6 +92,32 @@ void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
/**Function*************************************************************
Synopsis [Retrives value of the PI in the original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
Aig_Obj_t * pObjFraig;
int nVarNum, Value;
assert( Aig_ObjIsPi(pObj) );
pObjFraig = Ssw_ObjFraig( p, pObj, f );
nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
if ( p->pPars->fPolarFlip )
{
if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1;
}
return Value;
}
/**Function*************************************************************
Synopsis [Resimulates the cone of influence of the solved nodes.]
Description []
......@@ -108,11 +134,7 @@ void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
if ( Aig_ObjIsPi(pObj) )
{
Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f );
int nVarNum = Ssw_ObjSatNum( p, pObjFraig );
// get the value from the SAT solver
// (account for the fact that some vars may be minimized away)
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
return;
}
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
......@@ -194,6 +216,40 @@ void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, i
p->timeSimSat += clock() - clk;
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
{
Aig_Obj_t * pObj;
int i, RetValue1, RetValue2, clk = clock();
// set the PI simulation information
Aig_ManConst1(p->pAig)->fMarkB = 1;
Aig_ManForEachPi( p->pAig, pObj, i )
pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
// simulate internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
// check equivalence classes
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
RetValue2 = Ssw_ClassesRefine( p->ppClasses );
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
assert( RetValue1 );
else
assert( RetValue2 );
p->timeSimSat += clock() - clk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/ssw/sswSweep.c
......@@ -50,12 +50,33 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
// get the fraiged node
pObjFraig = Ssw_ObjFraig( p, pObj, f );
if ( pObjFraig == NULL )
return;
assert( pObjFraig != NULL );
// get the fraiged representative
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
if ( pObjReprFraig == NULL )
assert( pObjReprFraig != NULL );
// check if constant 0 pattern distinquishes these nodes
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
{
Aig_Obj_t * pObj;
int i;
if ( p->pSat->model.cap < p->pSat->size )
{
veci_resize(&p->pSat->model, 0);
for ( i = 0; i < p->pSat->size; i++ )
veci_push( &p->pSat->model, (int)l_False );
}
// set the values of SAT vars to be equal to the phase of the nodes
Aig_ManForEachObj( p->pFrames, pObj, i )
if ( Ssw_ObjSatNum( p, pObj ) )
{
int iVar = Ssw_ObjSatNum( p, pObj );
assert( iVar < p->pSat->size );
p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
p->pSat->model.size = p->pSat->size;
}
p->nStragers++;
return;
}
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
{
......@@ -63,10 +84,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
// p->pReprsProved[ pObj->Id ] = pObjRepr;
return;
}
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
// assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
else
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
if ( RetValue == -1 ) // timed out
{
assert( 0 );
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
p->fRefined = 1;
return;
......@@ -80,7 +106,8 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
return;
}
// disproved the equivalence
Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
......@@ -110,7 +137,8 @@ clk = clock();
// sweep internal nodes
p->fRefined = 0;
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
......@@ -120,17 +148,18 @@ clk = clock();
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
}
}
Bar_ProgressStop( pProgress );
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
// cleanup
Ssw_ClassesCheck( p->ppClasses );
Ssw_ManCleanup( p );
// Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += clock() - clk;
return p->fRefined;
}
......@@ -150,21 +179,21 @@ int Ssw_ManSweep( Ssw_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f = p->pPars->nFramesK;
int nConstrPairs, clk, i, f;
// perform speculative reduction
clk = clock();
// create timeframes
p->pFrames = Ssw_FramesWithClasses( p );
p->nFrameNodes = Aig_ManNodeNum( p->pFrames );
// add constraints
Ssw_ManStartSolver( p );
nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
assert( (nConstrPairs & 1) == 0 );
for ( i = 0; i < nConstrPairs; i += 2 )
{
pObj = Aig_ManPo( p->pFrames, i );
pObj2 = Aig_ManPo( p->pFrames, i+1 );
Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) );
Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
}
// build logic cones for register inputs
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
......@@ -175,25 +204,36 @@ clk = clock();
sat_solver_simplify( p->pSat );
p->timeReduce += clock() - clk;
// map constants and PIs
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
// make sure LOs are assigned
Saig_ManForEachLo( p->pAig, pObj, i )
assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachNode( p->pAig, pObj, i )
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
Bar_ProgressUpdate( pProgress, i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
Ssw_ManSweepNode( p, pObj, f );
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f );
}
}
Bar_ProgressStop( pProgress );
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
// cleanup
Ssw_ClassesCheck( p->ppClasses );
Ssw_ManCleanup( p );
// Ssw_ClassesCheck( p->ppClasses );
return p->fRefined;
}
......
src/base/abci/abc.c
......@@ -453,8 +453,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "fretime", Abc_CommandFlowRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssw", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssw2", Abc_CommandSeqSweep2, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scorr", Abc_CommandSeqSweep2, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "testssw", Abc_CommandSeqSweepTest, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
......@@ -13482,7 +13482,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssw [-PQNFL num] [-lrfetvh]\n" );
fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
......@@ -13655,7 +13655,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssw2 [-PQFCLN num] [-plvh]\n" );
fprintf( pErr, "usage: scorr [-PQFCLN num] [-plvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment