Skip to content

A
abc
Commit 4d71c114 by Alan Mishchenko
Options

Version abc80921

parent 3429e630
Showing with 285 additions and 365 deletions
src/aig/aig/aig.h
......@@ -471,6 +471,7 @@ extern int Aig_ManChoiceLevel( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
......
src/aig/aig/aigDfs.c
......@@ -734,6 +734,33 @@ Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
Synopsis [Counts the support size of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp )
{
int i;
Vec_PtrClear( vSupp );
Aig_ManIncrementTravId( p );
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
for ( i = 0; i < nObjs; i++ )
{
assert( !Aig_IsComplement(ppObjs[i]) );
if ( Aig_ObjIsPo(ppObjs[i]) )
Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp );
else
Aig_Support_rec( p, ppObjs[i], vSupp );
}
}
/**Function*************************************************************
Synopsis [Transfers the AIG from one manager into another.]
Description []
......
src/aig/dch/dchSat.c
......@@ -50,13 +50,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
// p->nCallsSince++; // experiment with this!!!
p->nCallsSince++; // experiment with this!!!
// check if SAT solver needs recycling
if ( p->pSat == NULL ||
(p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax &&
++p->nCallsSince > p->pPars->nCallsRecycle) )
p->nCallsSince > p->pPars->nCallsRecycle) )
Dch_ManSatSolverRecycle( p );
// if the nodes do not have SAT variables, allocate them
......
src/aig/dch/dchSimSat.c
......@@ -60,10 +60,10 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vSimRoots, pObj );
return;
}
// pRepr is the representative of the equivalence class
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
// pRepr is the representative of an equivalence class
if ( pRepr->fMarkA )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
pRepr->fMarkA = 1;
Vec_PtrPush( p->vSimClasses, pRepr );
}
......@@ -80,6 +80,8 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
***********************************************************************/
void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
Aig_Obj_t * pObj;
int i;
Vec_PtrClear( p->vSimRoots );
Vec_PtrClear( p->vSimClasses );
Aig_ManIncrementTravId( p->pAigTotal );
......@@ -88,6 +90,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
Dch_ManCollectTfoCands_rec( p, pObj2 );
Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
Vec_PtrForEachEntry( p->vSimClasses, pObj, i )
pObj->fMarkA = 0;
}
/**Function*************************************************************
......@@ -116,6 +120,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
// 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 = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
return;
}
Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
......
src/aig/fra/fraSec.c
......@@ -93,8 +93,6 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
goto finish;
// prepare parameters
Ssw_ManSetDefaultParams( pPars2 );
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = pParSec->fVeryVerbose;
......@@ -142,7 +140,8 @@ PRT( "Time", clock() - clk );
if ( pParSec->fRetimeFirst && pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
......@@ -172,11 +171,21 @@ clk = clock();
goto finish;
}
}
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
// pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
Ssw_ManSetDefaultParamsLcorr( pPars2 );
pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
nIter = pPars2->nIters;
// prepare parameters for scorr
Ssw_ManSetDefaultParams( pPars2 );
if ( pTemp->pSeqModel )
{
if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" );
printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
......
src/aig/int/intCtrex.c
......@@ -66,7 +66,10 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
break;
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
// create POs for the output of the last frame
pObj = Aig_ManPo( pAig, 0 );
......
src/aig/ntl/ntlFraig.c
......@@ -435,6 +435,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
***********************************************************************/
Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
{
Ssw_Pars_t Pars, * pPars = &Pars;
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
......@@ -444,7 +445,12 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
// perform SCL for the given design
pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
// pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
Ssw_ManSetDefaultParamsLcorr( pPars );
pPars->nBTLimit = nConfMax;
pPars->fVerbose = fVerbose;
pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
Aig_ManStop( pTemp );
if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
......
src/aig/ssw/ssw.h
......@@ -50,11 +50,12 @@ struct Ssw_Pars_t_
int nBTLimit; // conflict limit at a node
int nMinDomSize; // min clock domain considered for optimization
int fPolarFlip; // uses polarity adjustment
int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
int nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
int fSkipCheck; // does not run equivalence check for unaffected cones
int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
int fVerbose; // verbose stats
// internal parameters
int nIters; // the number of iterations performed
......@@ -82,7 +83,9 @@ struct Ssw_Cex_t_
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
......
src/aig/ssw/sswAig.c
......@@ -49,9 +49,9 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( pObj->fPhase == pObjRepr->fPhase )
{
......@@ -69,7 +69,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// 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 );
Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
// add the constraint
Aig_ObjCreatePo( pFrames, pObjNew2 );
Aig_ObjCreatePo( pFrames, pObjNew );
......@@ -99,15 +99,15 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(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) );
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
Ssw_ObjSetFrame( 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 );
......@@ -115,16 +115,16 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Aig_ManForEachNode( p->pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
}
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
}
// add the POs for the latch outputs of the last frame
Saig_ManForEachLo( p->pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
// remove dangling nodes
Aig_ManCleanup( pFrames );
......
src/aig/ssw/sswClass.c
......@@ -286,6 +286,8 @@ int Ssw_ClassesLitNum( Ssw_Cla_t * p )
***********************************************************************/
Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
{
if ( p->pId2Class[pRepr->Id] == NULL )
return NULL;
assert( p->pId2Class[pRepr->Id] != NULL );
assert( p->pClassSizes[pRepr->Id] > 1 );
*pnSize = p->pClassSizes[pRepr->Id];
......@@ -333,6 +335,7 @@ void Ssw_ClassesCheck( Ssw_Cla_t * p )
Ssw_ManForEachClass( p, ppClass, k )
{
pPrev = NULL;
assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
{
if ( i == 0 )
......@@ -423,12 +426,15 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pRepr, * pTemp;
assert( p->pClassSizes[pObj->Id] == 0 );
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
assert( p->pClassSizes[pRepr->Id] == 0 );
assert( p->pId2Class[pRepr->Id] == NULL );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
p->nCands1--;
return;
......@@ -439,7 +445,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pClassSizes[pRepr->Id] >= 2 );
if ( p->pClassSizes[pRepr->Id] == 2 )
{
p->pId2Class[pObj->Id] = NULL;
p->pId2Class[pRepr->Id] = NULL;
p->nClasses--;
p->pClassSizes[pRepr->Id] = 0;
p->nLits--;
......@@ -491,7 +497,7 @@ PRT( "Simulation of 32 frames with 4 words", clock() - clk );
// set comparison procedures
clk = clock();
Ssw_ClassesSetData( p, pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// allocate the hash table hashing simulation info into nodes
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
......@@ -593,38 +599,6 @@ PRT( "Collecting candidate equival classes", clock() - clk );
/**Function*************************************************************
Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
{
return pObj->fPhase == pObj->fMarkB;
}
/**Function*************************************************************
Synopsis [Returns 1 if the nodes appear equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
}
/**Function*************************************************************
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
......
src/aig/ssw/sswCore.c
......@@ -50,18 +50,37 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nBTLimit = 1000; // conflict limit at a node
p->nMinDomSize = 100; // min clock domain considered for optimization
p->fPolarFlip = 0; // uses polarity adjustment
p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 5000; // the max number of SAT variables
p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
p->nSatVarMax = 1000; // the max number of SAT variables
p->nRecycleCalls = 50; // calls to perform before recycling SAT solver
// return values
p->nIters = 0; // the number of iterations performed
}
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
{
Ssw_ManSetDefaultParams( p );
p->fLatchCorrOpt = 1;
p->nBTLimit = 10000;
}
/**Function*************************************************************
Synopsis [Performs computation of signal correspondence with constraints.]
Description []
......@@ -73,6 +92,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal;
Aig_Man_t * pAigNew;
int RetValue, nIter;
int clk, clkTotal = clock();
......@@ -97,23 +117,40 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using induction
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
for ( nIter = 0; ; nIter++ )
{
clk = clock();
if ( p->pPars->fLatchCorrOpt )
{
RetValue = Ssw_ManSweepLatch( p );
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
PRT( "T", clock() - clk );
nSatProof = p->nSatProof;
nSatCallsSat = p->nSatCallsSat;
nRecycles = p->nRecycles;
nSatFailsReal = p->nSatFailsReal;
}
}
else
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
if ( p->pPars->fSkipCheck )
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk );
}
RetValue = Ssw_ManSweep( p );
if ( p->pPars->fVerbose )
{
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
if ( p->pPars->fSkipCheck )
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk );
}
}
Ssw_ManCleanup( p );
if ( !RetValue )
break;
......@@ -161,7 +198,10 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
}
// check and update parameters
if ( pPars->fLatchCorrOpt )
{
pPars->fLatchCorr = 1;
pPars->nFramesAddSim = 0;
}
else
{
assert( pPars->nFramesK > 0 );
......@@ -181,13 +221,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// perform one round of seq simulation and generate candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
}
else
{
// create trivial equivalence classes with all nodes being candidates for constant 1
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
}
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
......@@ -196,6 +236,24 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return pAigNew;
}
/**Function*************************************************************
Synopsis [Performs computation of latch correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
Ssw_Pars_t Pars;
if ( pPars == NULL )
Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
return Ssw_SignalCorrespondence( pAig, pPars );
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswInt.h
......@@ -53,25 +53,31 @@ struct Ssw_Man_t_
// AIGs used in the package
Aig_Man_t * pAig; // user-given AIG
Aig_Man_t * pFrames; // final AIG
Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
Aig_Obj_t ** pNodeToFrames; // mapping of AIG nodes into FRAIG nodes
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
int nRefUse;
int nRefSkip;
int nRefUse; // the number of equivalences used
int nRefSkip; // the number of equivalences skipped
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
int * pSatVars; // mapping of each node into its SAT var
int nSatVarsTotal; // the total number of SAT vars created
Vec_Ptr_t * vFanins; // fanins of the CNF node
Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
// SAT solving (latch corr only)
int nCallsSince; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables
Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs
int nPatterns; // the number of patterns saved
int nSimRounds; // the number of simulation rounds performed
int nCallsCount; // the number of calls in this round
int nCallsDelta; // the number of calls to skip
int nCallsSat; // the number of SAT calls in this round
int nCallsUnsat; // the number of UNSAT calls in this round
int nRecycleCalls; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
int nConeMax; // the maximum cone size
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
......@@ -125,11 +131,11 @@ static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}
static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; }
static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFrames[p->nFrames*pObj->Id + i]; }
static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }
static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
......@@ -161,8 +167,6 @@ extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
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 );
extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj );
extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
/*=== sswCnf.c ===================================================*/
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswCore.c ===================================================*/
......@@ -178,19 +182,23 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p );
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSim.c ===================================================*/
extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
extern int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Ssw_SmlClean( Ssw_Sml_t * p );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
extern void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
extern void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
/*=== sswSimSat.c ===================================================*/
extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
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 );
extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, 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
......@@ -52,12 +52,10 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->pPars = pPars;
p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1;
p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
p->vFanins = Vec_PtrAlloc( 100 );
p->vSimRoots = Vec_PtrAlloc( 1000 );
p->vSimClasses = Vec_PtrAlloc( 1000 );
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
......@@ -102,13 +100,15 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
p->nSatVarsTotal/p->pPars->nIters );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n",
p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
......@@ -139,12 +139,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p )
{
Aig_ManCleanMarkB( p->pAig );
if ( p->pFrames )
{
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->pSat )
{
......@@ -154,6 +153,11 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
p->pSat = NULL;
memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
}
if ( p->vSimInfo )
{
Vec_PtrFree( p->vSimInfo );
p->vSimInfo = NULL;
}
p->nConstrTotal = 0;
p->nConstrReduced = 0;
}
......@@ -172,6 +176,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
void Ssw_ManStop( Ssw_Man_t * p )
{
Aig_ManCleanMarkA( p->pAig );
Aig_ManCleanMarkB( p->pAig );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
......@@ -179,11 +184,9 @@ void Ssw_ManStop( Ssw_Man_t * p )
if ( p->pSml )
Ssw_SmlStop( p->pSml );
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vSimRoots );
Vec_PtrFree( p->vSimClasses );
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
FREE( p->pNodeToFraig );
FREE( p->pNodeToFrames );
FREE( p->pSatVars );
FREE( p->pPatWords );
free( p );
......
src/aig/ssw/sswPairs.c
......@@ -289,7 +289,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
// create equivalence classes using these IDs
p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
// cleanup
......
src/aig/ssw/sswSimSat.c
......@@ -30,157 +30,6 @@
/**Function*************************************************************
Synopsis [Collects internal nodes in the reverse DFS order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanout, * pRepr;
int iFanout = -1, i;
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
// traverse the fanouts
Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i )
Ssw_ManCollectTfoCands_rec( p, pFanout );
// check if the given node has a representative
pRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pRepr == NULL )
return;
// pRepr is the constant 1 node
if ( pRepr == Aig_ManConst1(p->pAig) )
{
Vec_PtrPush( p->vSimRoots, pObj );
return;
}
// pRepr is the representative of the equivalence class
if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
return;
Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
Vec_PtrPush( p->vSimClasses, pRepr );
}
/**Function*************************************************************
Synopsis [Collect equivalence classes and const1 cands in the TFO.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
Vec_PtrClear( p->vSimRoots );
Vec_PtrClear( p->vSimClasses );
Aig_ManIncrementTravId( p->pAig );
Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
Ssw_ManCollectTfoCands_rec( p, pObj1 );
Ssw_ManCollectTfoCands_rec( p, pObj2 );
Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
}
/**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;
}
/*
if ( nVarNum==0 )
printf( "x" );
else if ( Value == 0 )
printf( "0" );
else
printf( "1" );
*/
return Value;
}
/**Function*************************************************************
Synopsis [Resimulates the cone of influence of the solved nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
if ( Aig_ObjIsPi(pObj) )
{
pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
return;
}
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f );
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
}
/**Function*************************************************************
Synopsis [Resimulates the cone of influence of the other nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
{
if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAig, pObj);
if ( Aig_ObjIsPi(pObj) )
{
// set random value
pObj->fMarkB = Aig_ManRandom(0) & 1;
return;
}
Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
......@@ -190,52 +39,7 @@ void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f )
{
Aig_Obj_t * pRoot, ** ppClass;
int i, k, nSize, RetValue1, RetValue2, clk = clock();
// get the equivalence classes
Ssw_ManCollectTfoCands( p, pObj, pRepr );
// resimulate the cone of influence of the solved nodes
Aig_ManIncrementTravId( p->pAig );
Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
Ssw_ManResimulateSolved_rec( p, pObj, f );
Ssw_ManResimulateSolved_rec( p, pRepr, f );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
Ssw_ManResimulateOther_rec( p, pRoot );
// refine these nodes
RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
// resimulate the cone of influence of the cand classes
RetValue2 = 0;
Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
{
ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize );
for ( k = 0; k < nSize; k++ )
Ssw_ManResimulateOther_rec( p, ppClass[k] );
// refine this class
RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
}
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
assert( RetValue1 );
else
assert( RetValue2 );
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 )
void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pObj;
int i, RetValue1, RetValue2, clk = clock();
......@@ -255,18 +59,17 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" );
printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" );
printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
......@@ -278,7 +81,7 @@ p->timeSimSat += clock() - clk;
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
{
int RetValue1, RetValue2, clk = clock();
// set the PI simulation information
......@@ -293,18 +96,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" );
printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" );
printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswSweep.c
......@@ -78,6 +78,33 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
/**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_ObjFrame( p, pObj, f );
nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (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 [Copy pattern from the solver into the internal storage.]
Description []
......@@ -114,7 +141,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
Aig_InfoSetBit( p->pPatWords, i );
}
......@@ -138,9 +165,9 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( pObjRepr == NULL )
return;
// get the fraiged node
pObjFraig = Ssw_ObjFraig( p, pObj, f );
pObjFraig = Ssw_ObjFrame( p, pObj, f );
// get the fraiged representative
pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
// check if constant 0 pattern distinquishes these nodes
assert( pObjFraig != NULL && pObjReprFraig != NULL );
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
......@@ -168,7 +195,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( RetValue == 1 ) // proved equivalent
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return;
}
if ( RetValue == -1 ) // timed out
......@@ -181,16 +208,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
{
assert( 0 );
printf( "\nMistake!!!\n" );
printf( "\nSsw_ManSweepNode(): Error!\n" );
}
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
if ( p->pPars->nConstrs == 0 )
Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
Ssw_ManResimulateBit( p, pObj, pObjRepr );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
......@@ -216,7 +242,7 @@ clk = clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) );
Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
// sweep internal nodes
p->fRefined = 0;
......@@ -226,16 +252,16 @@ clk = clock();
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Ssw_ObjSetFrame( 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) );
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
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_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f, 1 );
}
// quit if this is the last timeframe
......@@ -246,7 +272,7 @@ clk = clock();
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew );
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
}
}
......@@ -307,12 +333,12 @@ p->timeMarkCones += clock() - clk;
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Ssw_ObjSetFrame( 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) );
Ssw_ObjSetFrame( 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 );
assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
......@@ -330,7 +356,7 @@ p->timeMarkCones += clock() - clk;
{
pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f, 0 );
}
}
......
src/base/abci/abc.c
......@@ -13888,10 +13888,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFramesP = 0;
nConfMax = 10000;
nVarsMax = 5000;
nConfMax = 1000;
nVarsMax = 1000;
fNewAlgor = 0;
fVerbose = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
{
......
src/base/abci/abcDar.c
......@@ -1335,7 +1335,6 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
return NULL;
Ssw_ManSetDefaultParams( pPars );
pPars->fLatchCorrOpt = 1;
// pPars->nFramesAddSim = 0;
pPars->nBTLimit = nConfMax;
pPars->nSatVarMax = nVarsMax;
pPars->fVerbose = fVerbose;
......
src/sat/bsat/satInterA.c
......@@ -544,13 +544,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int i, v, Var, PrevId;
int fPrint = 0;
int clk = clock();
/*
if ( pFinal->Id == 5187 )
{
int x = 0;
Inta_ManPrintClause( p, pConflict );
}
*/
// collect resolvent literals
if ( p->fProofVerif )
{
......@@ -579,28 +573,17 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
if ( !p->pSeens[Var] )
continue;
p->pSeens[Var] = 0;
/*
if ( pFinal->Id == 5187 )
{
printf( "pivot = %d ", p->pTrail[i] );
}
*/
// skip literals of the resulting clause
pReason = p->pReasons[Var];
if ( pReason == NULL )
continue;
assert( p->pTrail[i] == pReason->pLits[0] );
/*
if ( pFinal->Id == 5187 )
{
Inta_ManPrintClause( p, pReason );
}
*/
// add the variables to seen
for ( v = 1; v < (int)pReason->nLits; v++ )
p->pSeens[lit_var(pReason->pLits[v])] = 1;
// record the reason clause
assert( Inta_ManProofGet(p, pReason) > 0 );
p->Counter++;
......@@ -656,7 +639,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
}
}
// Vec_PtrPush( pFinal->pAntis, pReason );
}
......@@ -673,20 +655,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int v1, v2;
if ( fPrint )
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
/*
if ( pFinal->Id == 5187 )
{
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
*/
/*
if ( p->nResLits != pFinal->nLits )
{
printf( "Recording clause %d: The resolvent is wrong (nRetLits = %d, pFinal->nLits = %d).\n",
pFinal->Id, p->nResLits, pFinal->nLits );
}
*/
for ( v1 = 0; v1 < p->nResLits; v1++ )
{
for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
......@@ -703,6 +671,27 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
// if there are literals in the clause that are not in the resolvent
// it means that the derived resolvent is stronger than the clause
// we can replace the clause with the resolvent by removing these literals
if ( p->nResLits != (int)pFinal->nLits )
{
for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
{
for ( v2 = 0; v2 < p->nResLits; v2++ )
if ( pFinal->pLits[v1] == p->pResLits[v2] )
break;
if ( v2 < p->nResLits )
continue;
// remove literal v1 from the final clause
pFinal->nLits--;
for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
pFinal->pLits[v2] = pFinal->pLits[v2+1];
v1--;
}
assert( p->nResLits == (int)pFinal->nLits );
}
}
p->timeTrace += clock() - clk;
......@@ -736,9 +725,16 @@ int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
if ( pClause->nLits == 0 )
printf( "Error: Empty clause is attempted.\n" );
// add assumptions to the trail
assert( !pClause->fRoot );
assert( p->nTrailSize == p->nRootSize );
// if any of the clause literals are already assumed
// it means that the clause is redundant and can be skipped
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
return 1;
// add assumptions to the trail
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{
......
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