Skip to content

A
abc
Commit e917dda1 by Alan Mishchenko
Options

Version abc81013

parent a2535d49
Showing with 925 additions and 2376 deletions
abc.dsp
...@@ -3298,6 +3298,10 @@ SOURCE=.\src\aig\saig\saigHaig.c ...@@ -3298,6 +3298,10 @@ SOURCE=.\src\aig\saig\saigHaig.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\saig\saigInd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigIoa.c SOURCE=.\src\aig\saig\saigIoa.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -3494,6 +3498,10 @@ SOURCE=.\src\aig\ssw\sswSat.c ...@@ -3494,6 +3498,10 @@ SOURCE=.\src\aig\ssw\sswSat.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\ssw\sswSemi.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswSim.c SOURCE=.\src\aig\ssw\sswSim.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/aig/aig.h
...@@ -654,6 +654,8 @@ extern void Aig_ManCleanPioNumbers( Aig_Man_t * p ); ...@@ -654,6 +654,8 @@ extern void Aig_ManCleanPioNumbers( Aig_Man_t * p );
extern int Aig_ManCountChoices( Aig_Man_t * p ); extern int Aig_ManCountChoices( Aig_Man_t * p );
extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix ); extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
extern unsigned Aig_ManRandom( int fReset ); extern unsigned Aig_ManRandom( int fReset );
extern void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
extern void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
/*=== aigWin.c =========================================================*/ /*=== aigWin.c =========================================================*/
extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ); extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
......
src/aig/aig/aigUtil.c
...@@ -1122,6 +1122,86 @@ unsigned Aig_ManRandom( int fReset ) ...@@ -1122,6 +1122,86 @@ unsigned Aig_ManRandom( int fReset )
} }
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
*pBeg++ = *pBeg1++;
else
*pBeg++ = *pBeg2++;
}
while ( pBeg1 < pEnd1 )
*pBeg++ = *pBeg1++;
while ( pBeg2 < pEnd2 )
*pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize >= vArr1->nSize );
assert( vArr->nSize >= vArr2->nSize );
}
/**Function*************************************************************
Synopsis [Returns the result of intersecting the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
// *pBeg++ = *pBeg1++;
pBeg1++;
else
// *pBeg++ = *pBeg2++;
pBeg2++;
}
// while ( pBeg1 < pEnd1 )
// *pBeg++ = *pBeg1++;
// while ( pBeg2 < pEnd2 )
// *pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize <= vArr1->nSize );
assert( vArr->nSize <= vArr2->nSize );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/saig/module.make
...@@ -3,6 +3,7 @@ SRC += src/aig/saig/saigAbs.c \ ...@@ -3,6 +3,7 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigCone.c \ src/aig/saig/saigCone.c \
src/aig/saig/saigDup.c \ src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \ src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \ src/aig/saig/saigIoa.c \
src/aig/saig/saigLoc.c \ src/aig/saig/saigLoc.c \
src/aig/saig/saigMiter.c \ src/aig/saig/saigMiter.c \
......
src/aig/saig/saig.h
...@@ -87,6 +87,8 @@ extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p ); ...@@ -87,6 +87,8 @@ extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); extern Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/ /*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
/*=== saigInd.c ==========================================================*/
extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== saigIoa.c ==========================================================*/ /*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
......
src/aig/saig/saigAbs.c
...@@ -51,7 +51,7 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** ...@@ -51,7 +51,7 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
{ {
Aig_Man_t * pFrames; Aig_Man_t * pFrames;
Aig_Obj_t ** ppMap; Aig_Obj_t ** ppMap;
Aig_Obj_t * pObj, * pObjLi, * pObjLo; Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pResult;
int i, f; int i, f;
assert( Saig_ManRegNum(pAig) > 0 ); assert( Saig_ManRegNum(pAig) > 0 );
// start the mapping // start the mapping
...@@ -61,10 +61,12 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** ...@@ -61,10 +61,12 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
// create variables for register outputs // create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i ) Saig_ManForEachLo( pAig, pObj, i )
{ {
pObj->pData = Aig_ManConst0( pFrames ); // pObj->pData = Aig_ManConst0( pFrames );
pObj->pData = Aig_ObjCreatePi( pFrames );
Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData ); Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
} }
// add timeframes // add timeframes
pResult = Aig_ManConst0(pFrames);
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < nFrames; f++ )
{ {
// map the constant node // map the constant node
...@@ -82,14 +84,17 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** ...@@ -82,14 +84,17 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
} }
// OR the POs
Saig_ManForEachPo( pAig, pObj, i )
pResult = Aig_Or( pFrames, pResult, Aig_ObjChild0Copy(pObj) );
// create POs for this frame // create POs for this frame
if ( f == nFrames - 1 ) if ( f == nFrames - 1 )
{ {
Saig_ManForEachPo( pAig, pObj, i ) // Saig_ManForEachPo( pAig, pObj, i )
{ // {
pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); // pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData ); // Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
} // }
break; break;
} }
// save register inputs // save register inputs
...@@ -105,6 +110,7 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** ...@@ -105,6 +110,7 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData ); Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
} }
} }
Aig_ObjCreatePo( pFrames, pResult );
Aig_ManCleanup( pFrames ); Aig_ManCleanup( pFrames );
// remove mapping for the nodes that are no longer there // remove mapping for the nodes that are no longer there
for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ ) for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
...@@ -124,14 +130,15 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** ...@@ -124,14 +130,15 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose ) int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nRegs, int nConfMax, int fVerbose )
{ {
void * pSatCnf; void * pSatCnf;
Intp_Man_t * pManProof; Intp_Man_t * pManProof;
Aig_Obj_t * pObj;
sat_solver * pSat; sat_solver * pSat;
Vec_Int_t * vCore; Vec_Int_t * vCore;
int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars; int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
int i, RetValue; int i, Lit, RetValue;
// create the SAT solver // create the SAT solver
pSat = sat_solver_new(); pSat = sat_solver_new();
sat_solver_store_alloc( pSat ); sat_solver_store_alloc( pSat );
...@@ -145,6 +152,15 @@ int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose ) ...@@ -145,6 +152,15 @@ int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose )
return NULL; return NULL;
} }
} }
Aig_ManForEachPi( pCnf->pMan, pObj, i )
{
if ( i == nRegs )
break;
assert( pCnf->pVarNums[pObj->Id] >= 0 );
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
assert( 0 );
}
sat_solver_store_mark_roots( pSat ); sat_solver_store_mark_roots( pSat );
// solve the problem // solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 ); RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
...@@ -240,11 +256,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, ...@@ -240,11 +256,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
// create the timeframes // create the timeframes
pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames ); pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
printf( "AIG nodes = %d. Frames = %d.\n", Aig_ManNodeNum(p), Aig_ManNodeNum(pFrames) );
// convert them into CNF // convert them into CNF
// pCnf = Cnf_Derive( pFrames, 0 ); // pCnf = Cnf_Derive( pFrames, 0 );
pCnf = Cnf_DeriveSimple( pFrames, 0 ); pCnf = Cnf_DeriveSimple( pFrames, 0 );
// collect CNF variables involved in UNSAT core // collect CNF variables involved in UNSAT core
pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 ); pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, Saig_ManRegNum(p), nConfMax, 0 );
if ( pUnsatCoreVars == NULL ) if ( pUnsatCoreVars == NULL )
{ {
Aig_ManStop( pFrames ); Aig_ManStop( pFrames );
......
src/aig/saig/saigBmc.c
...@@ -249,8 +249,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim ...@@ -249,8 +249,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
{ {
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
if ( fVerbose ) if ( fVerbose )
{
printf( "Solving output %2d of frame %3d ... \r", printf( "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
clk = clock(); clk = clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 ); status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) ) if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
...@@ -258,12 +260,22 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim ...@@ -258,12 +260,22 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Solved %2d outputs of frame %3d. ", printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) ); Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations ); printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
PRT( "Time", clock() - clkPart ); PRT( "T", clock() - clkPart );
clkPart = clock(); clkPart = clock();
fflush( stdout ); fflush( stdout );
} }
if ( status == l_False ) if ( status == l_False )
{ {
/*
Lit = lit_neg( Lit );
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue );
if ( pSat->qtail != pSat->qhead )
{
RetValue = sat_solver_simplify(pSat);
assert( RetValue );
}
*/
} }
else if ( status == l_True ) else if ( status == l_True )
{ {
......
src/aig/saig/saigInd.c 0 → 100644
/**CFile****************************************************************
FileName [saigLoc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [K-step induction for one property only.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigLoc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "cnf.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs localization by unrolling timeframes backward.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose )
{
sat_solver * pSat;
Aig_Man_t * pAigPart;
Cnf_Dat_t * pCnfPart;
Vec_Int_t * vTopVarNums;
Vec_Ptr_t * vTop, * vBot;
Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetPioNumbers( p );
// start the top by including the PO
vBot = Vec_PtrAlloc( 100 );
vTop = Vec_PtrAlloc( 100 );
Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
// start the array of CNF variables
vTopVarNums = Vec_IntAlloc( 100 );
// start the solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, 1000 );
// iterate backward unrolling
RetValue = -1;
nSatVarNum = 0;
if ( fVerbose )
printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
for ( f = 0; ; f++ )
{
if ( f > 0 )
{
Aig_ManStop( pAigPart );
Cnf_DataFree( pCnfPart );
}
clk = clock();
// get the bottom
Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
// derive AIG for the part between top and bottom
pAigPart = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
// convert it into CNF
pCnfPart = Cnf_Derive( pAigPart, Aig_ManPoNum(pAigPart) );
Cnf_DataLift( pCnfPart, nSatVarNum );
nSatVarNum += pCnfPart->nVars;
// stitch variables of top and bot
assert( Aig_ManPoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) );
Aig_ManForEachPo( pAigPart, pObjPo, i )
{
if ( i == 0 )
{
// do not perform inductive strengthening
// if ( f > 0 )
// continue;
// add topmost literal
Lits[0] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], f>0 );
if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
assert( 0 );
continue;
}
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 0 );
Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i-1), 1 );
Lits[1] = toLitCond( pCnfPart->pVarNums[pObjPo->Id], 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
}
// add CNF to the SAT solver
for ( i = 0; i < pCnfPart->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnfPart->pClauses[i], pCnfPart->pClauses[i+1] ) )
break;
if ( i < pCnfPart->nClauses )
{
// printf( "SAT solver became UNSAT after adding clauses.\n" );
RetValue = 1;
break;
}
// run the SAT solver
nConfPrev = pSat->stats.conflicts;
status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
if ( fVerbose )
{
printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
f+1, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart),
nSatVarNum, pSat->stats.conflicts-nConfPrev );
PRT( "Time", clock() - clk );
}
if ( status == l_Undef )
break;
if ( status == l_False )
{
RetValue = 1;
break;
}
assert( status == l_True );
if ( f == nFramesMax - 1 )
break;
// the problem is SAT - add more clauses
// create new set of POs to derive new top
Vec_PtrClear( vTop );
Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
Vec_IntClear( vTopVarNums );
Vec_PtrForEachEntry( vBot, pObjPi, i )
{
assert( Aig_ObjIsPi(pObjPi) );
if ( Saig_ObjIsLo(p, pObjPi) )
{
pObjPiCopy = pObjPi->pData;
assert( pObjPiCopy != NULL );
Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) );
Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] );
}
}
}
// printf( "Completed %d interations.\n", f+1 );
// cleanup
sat_solver_delete( pSat );
Aig_ManStop( pAigPart );
Cnf_DataFree( pCnfPart );
Vec_IntFree( vTopVarNums );
Vec_PtrFree( vTop );
Vec_PtrFree( vBot );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigLoc.c
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
PackageName [Sequential AIG package.] PackageName [Sequential AIG package.]
Synopsis [Localization package.] Synopsis [Localization.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
...@@ -19,8 +19,6 @@ ...@@ -19,8 +19,6 @@
***********************************************************************/ ***********************************************************************/
#include "saig.h" #include "saig.h"
#include "cnf.h"
#include "satSolver.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -32,7 +30,7 @@ ...@@ -32,7 +30,7 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs localization by unrolling timeframes backward.] Synopsis []
Description [] Description []
...@@ -41,126 +39,7 @@ ...@@ -41,126 +39,7 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose )
{
sat_solver * pSat;
Vec_Int_t * vTopVarNums;
Vec_Ptr_t * vTop, * vBot;
Cnf_Dat_t * pCnfTop, * pCnfBot;
Aig_Man_t * pPartTop, * pPartBot;
Aig_Obj_t * pObj, * pObjBot;
int i, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
assert( Saig_ManPoNum(p) == 1 );
Aig_ManSetPioNumbers( p );
// start the top by including the PO
vBot = Vec_PtrAlloc( 100 );
vTop = Vec_PtrAlloc( 100 );
Vec_PtrPush( vTop, Aig_ManPo(p, 0) );
// create the manager composed of one PI/PO pair
pPartTop = Aig_ManStart( 10 );
Aig_ObjCreatePo( pPartTop, Aig_ObjCreatePi(pPartTop) );
pCnfTop = Cnf_Derive( pPartTop, 0 );
// start the array of CNF variables
vTopVarNums = Vec_IntAlloc( 100 );
Vec_IntPush( vTopVarNums, pCnfTop->pVarNums[Aig_ManPi(pPartTop,0)->Id] );
// start the solver
pSat = Cnf_DataWriteIntoSolver( pCnfTop, 1, 0 );
// iterate backward unrolling
RetValue = -1;
nSatVarNum = pCnfTop->nVars;
if ( fVerbose )
printf( "Localization parameters: FramesMax = %5d. ConflictMax = %6d.\n", nFramesMax, nConfMax );
for ( f = 0; ; f++ )
{
clk = clock();
// get the bottom
Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vTop), Vec_PtrSize(vTop), vBot );
// derive AIG for the part between top and bottom
pPartBot = Aig_ManDupSimpleDfsPart( p, vBot, vTop );
// convert it into CNF
pCnfBot = Cnf_Derive( pPartBot, Aig_ManPoNum(pPartBot) );
Cnf_DataLift( pCnfBot, nSatVarNum );
nSatVarNum += pCnfBot->nVars;
// stitch variables of top and bot
assert( Aig_ManPoNum(pPartBot) == Vec_IntSize(vTopVarNums) );
Aig_ManForEachPo( pPartBot, pObjBot, i )
{
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 0 );
Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
Lits[0] = toLitCond( Vec_IntEntry(vTopVarNums, i), 1 );
Lits[1] = toLitCond( pCnfBot->pVarNums[pObjBot->Id], 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
assert( 0 );
}
// add CNF to the SAT solver
for ( i = 0; i < pCnfBot->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnfBot->pClauses[i], pCnfBot->pClauses[i+1] ) )
break;
if ( i < pCnfBot->nClauses )
{
// printf( "SAT solver became UNSAT after adding clauses.\n" );
RetValue = 1;
break;
}
// run the SAT solver
nConfPrev = pSat->stats.conflicts;
status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, 0, 0, 0 );
if ( fVerbose )
{
printf( "%3d : PI = %5d. PO = %5d. AIG = %5d. Var = %6d. Conf = %6d. ",
f+1, Aig_ManPiNum(pPartBot), Aig_ManPoNum(pPartBot), Aig_ManNodeNum(pPartBot),
nSatVarNum, pSat->stats.conflicts-nConfPrev );
PRT( "Time", clock() - clk );
}
if ( status == l_Undef )
break;
if ( status == l_False )
{
RetValue = 1;
break;
}
assert( status == l_True );
if ( f == nFramesMax - 1 )
break;
// the problem is SAT - add more clauses
// create new set of POs to derive new top
Vec_PtrClear( vTop );
Vec_IntClear( vTopVarNums );
Vec_PtrForEachEntry( vBot, pObj, i )
{
assert( Aig_ObjIsPi(pObj) );
if ( Saig_ObjIsLo(p, pObj) )
{
pObjBot = pObj->pData;
assert( pObjBot != NULL );
Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObj) );
Vec_IntPush( vTopVarNums, pCnfBot->pVarNums[pObjBot->Id] );
}
}
// remove old top and replace it by bottom
Aig_ManStop( pPartTop );
pPartTop = pPartBot;
pPartBot = NULL;
Cnf_DataFree( pCnfTop );
pCnfTop = pCnfBot;
pCnfBot = NULL;
}
// printf( "Completed %d interations.\n", f+1 );
// cleanup
sat_solver_delete( pSat );
Aig_ManStop( pPartTop );
Cnf_DataFree( pCnfTop );
Aig_ManStop( pPartBot );
Cnf_DataFree( pCnfBot );
Vec_IntFree( vTopVarNums );
Vec_PtrFree( vTop );
Vec_PtrFree( vBot );
return RetValue;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/aig/ssw/module.make
...@@ -8,6 +8,7 @@ SRC += src/aig/ssw/sswAig.c \ ...@@ -8,6 +8,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswPart.c \ src/aig/ssw/sswPart.c \
src/aig/ssw/sswPairs.c \ src/aig/ssw/sswPairs.c \
src/aig/ssw/sswSat.c \ src/aig/ssw/sswSat.c \
src/aig/ssw/sswSemi.c \
src/aig/ssw/sswSim.c \ src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \ src/aig/ssw/sswSimSat.c \
src/aig/ssw/sswSweep.c \ src/aig/ssw/sswSweep.c \
......
src/aig/ssw/ssw.h
...@@ -50,8 +50,8 @@ struct Ssw_Pars_t_ ...@@ -50,8 +50,8 @@ struct Ssw_Pars_t_
int nBTLimit; // conflict limit at a node int nBTLimit; // conflict limit at a node
int nBTLimitGlobal;// conflict limit for multiple runs int nBTLimitGlobal;// conflict limit for multiple runs
int nMinDomSize; // min clock domain considered for optimization int nMinDomSize; // min clock domain considered for optimization
int nItersStop; // stop after the given number of iterations
int fPolarFlip; // uses polarity adjustment int fPolarFlip; // uses polarity adjustment
int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints int fUniqueness; // enable uniqueness constraints
...@@ -88,13 +88,13 @@ struct Ssw_Cex_t_ ...@@ -88,13 +88,13 @@ struct Ssw_Cex_t_
/*=== sswAbs.c ==========================================================*/ /*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose ); extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
/*=== sswBmc.c ==========================================================*/
extern int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose, int * piFrame );
/*=== sswCore.c ==========================================================*/ /*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ); 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_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswLoc.c ==========================================================*/
extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== sswMiter.c ===================================================*/ /*=== sswMiter.c ===================================================*/
extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose ); extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
/*=== sswPart.c ==========================================================*/ /*=== sswPart.c ==========================================================*/
......
src/aig/ssw/sswAig.c
...@@ -30,6 +30,50 @@ ...@@ -30,6 +30,50 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Starts the SAT manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
{
Ssw_Frm_t * p;
p = ALLOC( Ssw_Frm_t, 1 );
memset( p, 0, sizeof(Ssw_Frm_t) );
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax( pAig );
p->nFrames = 0;
p->pFrames = NULL;
p->vAig2Frm = Vec_PtrAlloc( 0 );
Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
return p;
}
/**Function*************************************************************
Synopsis [Starts the SAT manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_FrmStop( Ssw_Frm_t * p )
{
if ( p->pFrames )
Aig_ManStop( p->pFrames );
Vec_PtrFree( p->vAig2Frm );
free( p );
}
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.] Synopsis [Performs speculative reduction for one node.]
Description [] Description []
...@@ -164,7 +208,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) ...@@ -164,7 +208,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
assert( Aig_ManRegNum(p->pAig) > 0 ); assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0; p->nConstrTotal = p->nConstrReduced = 0;
// start the fraig package // start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// map constants and PIs // map constants and PIs
...@@ -190,8 +234,8 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) ...@@ -190,8 +234,8 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
// remove dangling nodes // remove dangling nodes
Aig_ManCleanup( pFrames ); Aig_ManCleanup( pFrames );
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) ); Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", // printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
p->nConstrTotal, p->nConstrReduced ); // p->nConstrTotal, p->nConstrReduced );
return pFrames; return pFrames;
} }
......
src/aig/ssw/sswCnf.c
...@@ -30,6 +30,63 @@ ...@@ -30,6 +30,63 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Starts the SAT manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
{
Ssw_Sat_t * p;
int Lit;
p = ALLOC( Ssw_Sat_t, 1 );
memset( p, 0, sizeof(Ssw_Sat_t) );
p->pAig = NULL;
p->fPolarFlip = fPolarFlip;
p->vSatVars = Vec_IntStart( 10000 );
p->vFanins = Vec_PtrAlloc( 100 );
p->vUsedPis = Vec_PtrAlloc( 100 );
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
p->nSatVars = 1;
Lit = toLit( p->nSatVars );
if ( fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
// Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
return p;
}
/**Function*************************************************************
Synopsis [Stop the SAT manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SatStop( Ssw_Sat_t * p )
{
if ( p->pSat )
sat_solver_delete( p->pSat );
Vec_IntFree( p->vSatVars );
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vUsedPis );
free( p );
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.] Synopsis [Addes clauses to the solver.]
Description [] Description []
...@@ -39,7 +96,7 @@ ...@@ -39,7 +96,7 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
{ {
Aig_Obj_t * pNodeI, * pNodeT, * pNodeE; Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
...@@ -68,7 +125,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -68,7 +125,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1); pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT); pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0); pLits[2] = toLitCond(VarF, 0);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -79,7 +136,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -79,7 +136,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 1); pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT); pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1); pLits[2] = toLitCond(VarF, 1);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -90,7 +147,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -90,7 +147,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0); pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE); pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0); pLits[2] = toLitCond(VarF, 0);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -101,7 +158,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -101,7 +158,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarI, 0); pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE); pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1); pLits[2] = toLitCond(VarF, 1);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -126,7 +183,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -126,7 +183,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 0^fCompT); pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE); pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1); pLits[2] = toLitCond(VarF, 1);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -137,7 +194,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -137,7 +194,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
pLits[0] = toLitCond(VarT, 1^fCompT); pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE); pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0); pLits[2] = toLitCond(VarF, 0);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -158,7 +215,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode ) ...@@ -158,7 +215,7 @@ void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{ {
Aig_Obj_t * pFanin; Aig_Obj_t * pFanin;
int * pLits, nLits, RetValue, i; int * pLits, nLits, RetValue, i;
...@@ -173,7 +230,7 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) ...@@ -173,7 +230,7 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
{ {
pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin)); pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1); pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
...@@ -185,13 +242,13 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) ...@@ -185,13 +242,13 @@ void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Vec_PtrForEachEntry( vSuper, pFanin, i ) Vec_PtrForEachEntry( vSuper, pFanin, i )
{ {
pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin)); pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
} }
} }
pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0); pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
if ( p->pPars->fPolarFlip ) if ( p->fPolarFlip )
{ {
if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
} }
...@@ -221,6 +278,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int ...@@ -221,6 +278,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
Vec_PtrPushUnique( vSuper, pObj ); Vec_PtrPushUnique( vSuper, pObj );
return; return;
} }
// pObj->fMarkA = 1;
// go through the branches // go through the branches
Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes ); Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes ); Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
...@@ -256,7 +314,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) ...@@ -256,7 +314,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier ) void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{ {
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
if ( Ssw_ObjSatNum(p,pObj) ) if ( Ssw_ObjSatNum(p,pObj) )
...@@ -264,12 +322,10 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie ...@@ -264,12 +322,10 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
assert( Ssw_ObjSatNum(p,pObj) == 0 ); assert( Ssw_ObjSatNum(p,pObj) == 0 );
if ( Aig_ObjIsConst1(pObj) ) if ( Aig_ObjIsConst1(pObj) )
return; return;
if ( p->pPars->fLatchCorrOpt ) // pObj->fMarkA = 1;
{ // save PIs (used by register correspondence)
Vec_PtrPush( p->vUsedNodes, pObj ); if ( Aig_ObjIsPi(pObj) )
if ( Aig_ObjIsPi(pObj) ) Vec_PtrPush( p->vUsedPis, pObj );
Vec_PtrPush( p->vUsedPis, pObj );
}
Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ ); Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) ); sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
if ( Aig_ObjIsNode(pObj) ) if ( Aig_ObjIsNode(pObj) )
...@@ -287,7 +343,7 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie ...@@ -287,7 +343,7 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ) void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
{ {
Vec_Ptr_t * vFrontier; Vec_Ptr_t * vFrontier;
Aig_Obj_t * pNode, * pFanin; Aig_Obj_t * pNode, * pFanin;
...@@ -327,6 +383,36 @@ void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ) ...@@ -327,6 +383,36 @@ void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
} }
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
{
int Value0, Value1, nVarNum;
assert( !Aig_IsComplement(pObj) );
nVarNum = Ssw_ObjSatNum( p, pObj );
if ( nVarNum > 0 )
return sat_solver_var_value( p->pSat, nVarNum );
// if ( pObj->fMarkA == 1 )
// return 0;
if ( Aig_ObjIsPi(pObj) )
return 0;
assert( Aig_ObjIsNode(pObj) );
Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
Value0 ^= Aig_ObjFaninC0(pObj);
Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
Value1 ^= Aig_ObjFaninC1(pObj);
return Value0 & Value1;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
src/aig/ssw/sswCore.c
...@@ -45,13 +45,13 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) ...@@ -45,13 +45,13 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nPartSize = 0; // size of the partition p->nPartSize = 0; // size of the partition
p->nOverSize = 0; // size of the overlap between partitions p->nOverSize = 0; // size of the overlap between partitions
p->nFramesK = 1; // the induction depth p->nFramesK = 1; // the induction depth
p->nFramesAddSim = 0; // additional frames to simulate p->nFramesAddSim = 2; // additional frames to simulate
p->nConstrs = 0; // treat the last nConstrs POs as seq constraints p->nConstrs = 0; // treat the last nConstrs POs as seq constraints
p->nBTLimit = 1000; // conflict limit at a node p->nBTLimit = 1000; // conflict limit at a node
p->nBTLimitGlobal = 5000000; // conflict limit for all runs p->nBTLimitGlobal = 5000000; // conflict limit for all runs
p->nMinDomSize = 100; // min clock domain considered for optimization p->nMinDomSize = 100; // min clock domain considered for optimization
p->nItersStop = 0; // stop after the given number of iterations
p->fPolarFlip = 0; // uses polarity adjustment p->fPolarFlip = 0; // uses polarity adjustment
p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering p->fSemiFormal = 0; // enable semiformal filtering
p->fUniqueness = 0; // enable uniqueness constraints p->fUniqueness = 0; // enable uniqueness constraints
...@@ -111,7 +111,12 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) ...@@ -111,7 +111,12 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
} }
if ( !p->pPars->fLatchCorr ) if ( !p->pPars->fLatchCorr )
{ {
p->pMSat = Ssw_SatStart( 0 );
Ssw_ManSweepBmc( p ); Ssw_ManSweepBmc( p );
if ( p->pPars->nFramesK > 1 && p->pPars->fUniqueness )
Ssw_UniqueRegisterPairInfo( p );
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p ); Ssw_ManCleanup( p );
} }
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
...@@ -120,20 +125,23 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) ...@@ -120,20 +125,23 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ClassesPrint( p->ppClasses, 0 );
} }
// apply semi-formal filtering // apply semi-formal filtering
/*
if ( p->pPars->fSemiFormal ) if ( p->pPars->fSemiFormal )
{ {
Aig_Man_t * pSRed; Aig_Man_t * pSRed;
Ssw_FilterUsingBmc( p, 0, 2000, p->pPars->fVerbose ); Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
// Ssw_FilterUsingBmc( p, 1, 100000, p->pPars->fVerbose ); // Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
pSRed = Ssw_SpeculativeReduction( p ); pSRed = Ssw_SpeculativeReduction( p );
Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
Aig_ManStop( pSRed ); Aig_ManStop( pSRed );
} }
*/
// refine classes using induction // refine classes using induction
nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0; nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
for ( nIter = 0; ; nIter++ ) for ( nIter = 0; ; nIter++ )
{ {
clk = clock(); clk = clock();
p->pMSat = Ssw_SatStart( 0 );
if ( p->pPars->fLatchCorrOpt ) if ( p->pPars->fLatchCorrOpt )
{ {
RetValue = Ssw_ManSweepLatch( p ); RetValue = Ssw_ManSweepLatch( p );
...@@ -153,34 +161,32 @@ clk = clock(); ...@@ -153,34 +161,32 @@ clk = clock();
else else
{ {
RetValue = Ssw_ManSweep( p ); RetValue = Ssw_ManSweep( p );
p->pPars->nConflicts += p->pSat->stats.conflicts; p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
{ {
printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ",
nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal ); p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
if ( p->pPars->fSkipCheck )
printf( "Use = %5d. Skip = %5d. ",
p->nRefUse, p->nRefSkip );
PRT( "T", clock() - clk ); PRT( "T", clock() - clk );
} }
} }
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p ); Ssw_ManCleanup( p );
if ( !RetValue ) if ( !RetValue )
break; break;
/*
if ( p->pPars->nItersStop && p->pPars->nItersStop == nIter )
{ {
static int Flag = 0; Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
if ( Flag++ == 4 && nIter == 4 ) Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
{ Aig_ManStop( pSRed );
Aig_Man_t * pSRed; printf( "Iterative refinement is stopped after iteration %d.\n", nIter );
pSRed = Ssw_SpeculativeReduction( p ); printf( "The network is reduced using candidate equivalences.\n" );
Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
Aig_ManStop( pSRed ); printf( "If the miter is SAT, the reduced result is incorrect.\n" );
} break;
} }
*/
} }
p->pPars->nIters = nIter + 1; p->pPars->nIters = nIter + 1;
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
...@@ -224,6 +230,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -224,6 +230,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return Aig_ManDupOrdered(pAig); return Aig_ManDupOrdered(pAig);
} }
// check and update parameters // check and update parameters
if ( pPars->fUniqueness )
{
pPars->nFramesAddSim = 0;
if ( pPars->nFramesK != 2 )
printf( "Setting K = 2 for uniqueness constaints to work.\n" );
pPars->nFramesK = 2;
}
if ( pPars->fLatchCorrOpt ) if ( pPars->fLatchCorrOpt )
{ {
pPars->fLatchCorr = 1; pPars->fLatchCorr = 1;
...@@ -232,8 +245,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -232,8 +245,6 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
else else
{ {
assert( pPars->nFramesK > 0 ); assert( pPars->nFramesK > 0 );
if ( pPars->nFramesK > 1 )
pPars->fSkipCheck = 0;
// perform partitioning // perform partitioning
if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
|| (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
...@@ -259,6 +270,9 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -259,6 +270,9 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
} }
// perform refinement of classes // perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p ); pAigNew = Ssw_SignalCorrespondenceRefine( p );
if ( pPars->fUniqueness )
printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n",
p->nUniquesAdded, p->nUniquesUseful );
// cleanup // cleanup
Ssw_ManStop( p ); Ssw_ManStop( p );
return pAigNew; return pAigNew;
......
src/aig/ssw/sswInt.h
...@@ -42,6 +42,8 @@ extern "C" { ...@@ -42,6 +42,8 @@ extern "C" {
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
...@@ -57,17 +59,10 @@ struct Ssw_Man_t_ ...@@ -57,17 +59,10 @@ struct Ssw_Man_t_
// equivalence classes // equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens int fRefined; // is set to 1 when refinement happens
int nRefUse; // the number of equivalences used // SAT solving
int nRefSkip; // the number of equivalences skipped Ssw_Sat_t * pMSatBmc; // SAT manager for base case
// SAT solving Ssw_Sat_t * pMSat; // SAT manager for inductive case
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
Vec_Int_t * vSatVars; // 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
// SAT solving (latch corr only) // SAT solving (latch corr only)
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 Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs
int nPatterns; // the number of patterns saved int nPatterns; // the number of patterns saved
int nSimRounds; // the number of simulation rounds performed int nSimRounds; // the number of simulation rounds performed
...@@ -81,7 +76,10 @@ struct Ssw_Man_t_ ...@@ -81,7 +76,10 @@ struct Ssw_Man_t_
// uniqueness // uniqueness
Vec_Ptr_t * vCommon; // the set of common variables in the logic cones Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
int iOutputLit; // the output literal of the uniqueness constaint int iOutputLit; // the output literal of the uniqueness constaint
Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff
int nUniques; // the number of uniqueness constaints used int nUniques; // the number of uniqueness constaints used
int nUniquesAdded; // useful uniqueness constraints
int nUniquesUseful; // useful uniqueness constraints
// sequential simulator // sequential simulator
Ssw_Sml_t * pSml; Ssw_Sml_t * pSml;
// counter example storage // counter example storage
...@@ -118,12 +116,35 @@ struct Ssw_Man_t_ ...@@ -118,12 +116,35 @@ struct Ssw_Man_t_
int timeTotal; // total runtime int timeTotal; // total runtime
}; };
// internal SAT manager
struct Ssw_Sat_t_
{
Aig_Man_t * pAig; // the AIG manager
int fPolarFlip; // flips polarity
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
Vec_Int_t * vSatVars; // 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 * vUsedPis; // the PIs with SAT variables
};
// internal frames manager
struct Ssw_Frm_t_
{
Aig_Man_t * pAig; // user-given AIG
int nObjs; // offset in terms of AIG nodes
int nFrames; // the number of frames in current unrolling
Aig_Man_t * pFrames; // unrolled AIG
Vec_Ptr_t * vAig2Frm; // mapping of AIG nodes into frame nodes
};
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, pObj->Id ); } static inline int Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vSatVars, pObj->Id ); }
static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntWriteEntryFill( p->vSatVars, pObj->Id, Num ); } static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num); }
static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{ {
...@@ -141,15 +162,22 @@ static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int ...@@ -141,15 +162,22 @@ static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int
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_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; } 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; }
static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); }
static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); }
static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_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_Frm_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 /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== sswAig.c ===================================================*/ /*=== sswAig.c ===================================================*/
extern Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig );
extern void Ssw_FrmStop( Ssw_Frm_t * p );
extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ); extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ); extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p );
/*=== sswBmc.c ===================================================*/ /*=== sswBmc.c ===================================================*/
extern int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswClass.c =================================================*/ /*=== sswClass.c =================================================*/
extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ); extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
...@@ -177,7 +205,10 @@ extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr ...@@ -177,7 +205,10 @@ extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, 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_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
/*=== sswCnf.c ===================================================*/ /*=== sswCnf.c ===================================================*/
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip );
extern void Ssw_SatStop( Ssw_Sat_t * p );
extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
/*=== sswCore.c ===================================================*/ /*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/ /*=== sswLcorr.c ==========================================================*/
...@@ -190,6 +221,8 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p ); ...@@ -190,6 +221,8 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p );
/*=== sswSat.c ===================================================*/ /*=== sswSat.c ===================================================*/
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); 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 ); extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSemi.c ===================================================*/
extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
/*=== sswSim.c ===================================================*/ /*=== sswSim.c ===================================================*/
extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ); 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_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
...@@ -214,6 +247,7 @@ extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, i ...@@ -214,6 +247,7 @@ extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, i
extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/ /*=== sswUnique.c ===================================================*/
extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ); extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
......
src/aig/ssw/sswLcorr.c
...@@ -31,48 +31,6 @@ ...@@ -31,48 +31,6 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Recycles the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
{
int Lit;
if ( p->pSat )
{
Aig_Obj_t * pObj;
int i;
Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
Ssw_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
Vec_PtrClear( p->vUsedPis );
// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
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 );
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
p->nRecycles++;
p->nRecycleCalls = 0;
}
/**Function*************************************************************
Synopsis [Tranfers simulation information from FRAIG to AIG.] Synopsis [Tranfers simulation information from FRAIG to AIG.]
Description [] Description []
...@@ -148,11 +106,11 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) ...@@ -148,11 +106,11 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
unsigned * pInfo; unsigned * pInfo;
int i, nVarNum, Value; int i, nVarNum, Value;
Vec_PtrForEachEntry( p->vUsedPis, pObj, i ) Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i )
{ {
nVarNum = Ssw_ObjSatNum( p, pObj ); nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
assert( nVarNum > 0 ); assert( nVarNum > 0 );
Value = sat_solver_var_value( p->pSat, nVarNum ); Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
if ( Value == 0 ) if ( Value == 0 )
continue; continue;
pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
...@@ -339,9 +297,14 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) ...@@ -339,9 +297,14 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
Ssw_ManSweepResimulate( p ); Ssw_ManSweepResimulate( p );
// attempt recycling the SAT solver // attempt recycling the SAT solver
if ( p->pPars->nSatVarMax && if ( p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax && p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls ) p->nRecycleCalls > p->pPars->nRecycleCalls )
Ssw_ManSatSolverRecycle( p ); {
Ssw_SatStop( p->pMSat );
p->pMSat = Ssw_SatStart( 0 );
p->nRecycles++;
p->nRecycleCalls = 0;
}
} }
// resimulate // resimulate
if ( p->nPatterns > 0 ) if ( p->nPatterns > 0 )
......
src/aig/ssw/sswMan.c
...@@ -53,12 +53,6 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) ...@@ -53,12 +53,6 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->pAig = pAig; p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1; p->nFrames = pPars->nFramesK + 1;
p->pNodeToFrames = 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->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
p->vFanins = Vec_PtrAlloc( 100 );
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
p->vCommon = Vec_PtrAlloc( 100 ); p->vCommon = Vec_PtrAlloc( 100 );
p->iOutputLit = -1; p->iOutputLit = -1;
// allocate storage for sim pattern // allocate storage for sim pattern
...@@ -106,11 +100,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) ...@@ -106,11 +100,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); 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", 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), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
p->nSatVarsTotal/p->pPars->nIters ); 0/p->pPars->nIters );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", 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 ); p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n", printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n",
p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds ); 0, p->nConeMax, p->nRecycles, p->nSimRounds );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 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->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) ); p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
...@@ -141,23 +135,14 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) ...@@ -141,23 +135,14 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p ) void Ssw_ManCleanup( Ssw_Man_t * p )
{ {
assert( p->pMSat == NULL );
if ( p->pFrames ) if ( p->pFrames )
{ {
Aig_ManCleanMarkA( p->pFrames );
Aig_ManStop( p->pFrames ); Aig_ManStop( p->pFrames );
p->pFrames = NULL; p->pFrames = NULL;
memset( p->pNodeToFrames, 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 )
{
int i;
// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
p->nSatVarsTotal += p->pSat->size;
sat_solver_delete( p->pSat );
p->pSat = NULL;
// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
for ( i = 0; i < Vec_IntSize(p->vSatVars); i++ )
p->vSatVars->pArray[i] = 0;
}
if ( p->vSimInfo ) if ( p->vSimInfo )
{ {
Vec_PtrFree( p->vSimInfo ); Vec_PtrFree( p->vSimInfo );
...@@ -188,46 +173,14 @@ void Ssw_ManStop( Ssw_Man_t * p ) ...@@ -188,46 +173,14 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_ClassesStop( p->ppClasses ); Ssw_ClassesStop( p->ppClasses );
if ( p->pSml ) if ( p->pSml )
Ssw_SmlStop( p->pSml ); Ssw_SmlStop( p->pSml );
Vec_PtrFree( p->vFanins ); if ( p->vDiffPairs )
Vec_PtrFree( p->vUsedNodes ); Vec_IntFree( p->vDiffPairs );
Vec_PtrFree( p->vUsedPis );
Vec_IntFree( p->vSatVars );
Vec_PtrFree( p->vCommon ); Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames ); FREE( p->pNodeToFrames );
FREE( p->pPatWords ); FREE( p->pPatWords );
free( p ); free( p );
} }
/**Function*************************************************************
Synopsis [Starts the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManStartSolver( Ssw_Man_t * p )
{
int Lit;
assert( p->pSat == NULL );
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
p->nSatVars = 1;
Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
Vec_PtrClear( p->vUsedNodes );
Vec_PtrClear( p->vUsedPis );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswSat.c
...@@ -50,18 +50,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -50,18 +50,19 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pNew) ); assert( !Aig_IsComplement(pNew) );
assert( pOld != pNew ); assert( pOld != pNew );
if ( p->pSat == NULL ) // if ( p->pSat == NULL )
Ssw_ManStartSolver( p ); // Ssw_ManStartSolver( p );
assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them // if the nodes do not have SAT variables, allocate them
Ssw_CnfNodeAddToSolver( p, pOld ); Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
Ssw_CnfNodeAddToSolver( p, pNew ); Ssw_CnfNodeAddToSolver( p->pMSat, pNew );
// solve under assumptions // solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1 // A = 1; B = 0 OR A = 1; B = 1
nLits = 2; nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase ); pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
if ( p->iOutputLit > -1 ) if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit; pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip ) if ( p->pPars->fPolarFlip )
...@@ -71,14 +72,14 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -71,14 +72,14 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
} }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
if ( p->pSat->qtail != p->pSat->qhead ) if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{ {
RetValue = sat_solver_simplify(p->pSat); RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 ); assert( RetValue != 0 );
} }
clk = clock(); clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk; p->timeSat += clock() - clk;
if ( RetValue1 == l_False ) if ( RetValue1 == l_False )
...@@ -88,8 +89,15 @@ p->timeSatUnsat += clock() - clk; ...@@ -88,8 +89,15 @@ p->timeSatUnsat += clock() - clk;
{ {
pLits[0] = lit_neg( pLits[0] ); pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] ); pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue ); assert( RetValue );
/*
if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 );
}
*/
} }
p->nSatCallsUnsat++; p->nSatCallsUnsat++;
} }
...@@ -116,8 +124,8 @@ p->timeSatUndec += clock() - clk; ...@@ -116,8 +124,8 @@ p->timeSatUndec += clock() - clk;
// solve under assumptions // solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0 // A = 0; B = 1 OR A = 0; B = 0
nLits = 2; nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase ); pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
if ( p->iOutputLit > -1 ) if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit; pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip ) if ( p->pPars->fPolarFlip )
...@@ -126,14 +134,14 @@ p->timeSatUndec += clock() - clk; ...@@ -126,14 +134,14 @@ p->timeSatUndec += clock() - clk;
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
} }
if ( p->pSat->qtail != p->pSat->qhead ) if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{ {
RetValue = sat_solver_simplify(p->pSat); RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 ); assert( RetValue != 0 );
} }
clk = clock(); clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits, RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 ); (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk; p->timeSat += clock() - clk;
if ( RetValue1 == l_False ) if ( RetValue1 == l_False )
...@@ -143,8 +151,15 @@ p->timeSatUnsat += clock() - clk; ...@@ -143,8 +151,15 @@ p->timeSatUnsat += clock() - clk;
{ {
pLits[0] = lit_neg( pLits[0] ); pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] ); pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue ); assert( RetValue );
/*
if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 );
}
*/
} }
p->nSatCallsUnsat++; p->nSatCallsUnsat++;
} }
...@@ -183,6 +198,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -183,6 +198,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// sanity checks // sanity checks
assert( Aig_Regular(pOld) != Aig_Regular(pNew) ); assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
assert( Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
// move constant to the old node // move constant to the old node
if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) ) if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
...@@ -200,13 +216,13 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -200,13 +216,13 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
pNew = Aig_Not(pNew); pNew = Aig_Not(pNew);
} }
// start the solver // if ( p->pSat == NULL )
if ( p->pSat == NULL ) // Ssw_ManStartSolver( p );
Ssw_ManStartSolver( p ); assert( p->pMSat != NULL );
// if the nodes do not have SAT variables, allocate them // if the nodes do not have SAT variables, allocate them
Ssw_CnfNodeAddToSolver( p, pOld ); Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );
// transform the new node // transform the new node
fComplNew = Aig_IsComplement( pNew ); fComplNew = Aig_IsComplement( pNew );
...@@ -216,12 +232,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -216,12 +232,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
if ( pOld == Aig_ManConst1(p->pFrames) ) if ( pOld == Aig_ManConst1(p->pFrames) )
{ {
// add constaint A = 1 ----> A // add constaint A = 1 ----> A
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
if ( p->pPars->fPolarFlip ) if ( p->pPars->fPolarFlip )
{ {
if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pNew->fPhase ) pLits[0] = lit_neg( pLits[0] );
} }
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
assert( RetValue ); assert( RetValue );
} }
else else
...@@ -229,8 +245,8 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -229,8 +245,8 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// add constaint A = B ----> (A v !B)(!A v B) // add constaint A = B ----> (A v !B)(!A v B)
// (A v !B) // (A v !B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew ); pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
if ( p->pPars->fPolarFlip ) if ( p->pPars->fPolarFlip )
{ {
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
...@@ -238,12 +254,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -238,12 +254,12 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
} }
pLits[0] = lit_neg( pLits[0] ); pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] ); pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue ); assert( RetValue );
// (!A v B) // (!A v B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew); pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
if ( p->pPars->fPolarFlip ) if ( p->pPars->fPolarFlip )
{ {
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] ); if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
...@@ -251,7 +267,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -251,7 +267,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
} }
pLits[0] = lit_neg( pLits[0] ); pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] ); pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
assert( RetValue ); assert( RetValue );
} }
return 1; return 1;
......
src/aig/ssw_old/sswBmc.c → src/aig/ssw/sswSemi.c
/**CFile**************************************************************** /**CFile****************************************************************
FileName [sswBmc.c] FileName [sswSemi.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.] PackageName [Inductive prover with constraints.]
Synopsis [Bounded model checker for equivalence clases.] Synopsis [Semiformal for equivalence clases.]
Author [Alan Mishchenko] Author [Alan Mishchenko]
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - September 1, 2008.] Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswBmc.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] Revision [$Id: sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
...@@ -24,9 +24,9 @@ ...@@ -24,9 +24,9 @@
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Ssw_Bmc_t_ Ssw_Bmc_t; // BMC manager typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager
struct Ssw_Bmc_t_ struct Ssw_Sem_t_
{ {
// parameters // parameters
int nConfMaxStart; // the starting conflict limit int nConfMaxStart; // the starting conflict limit
...@@ -58,14 +58,14 @@ struct Ssw_Bmc_t_ ...@@ -58,14 +58,14 @@ struct Ssw_Bmc_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
{ {
Ssw_Bmc_t * p; Ssw_Sem_t * p;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
// create interpolation manager // create interpolation manager
p = ALLOC( Ssw_Bmc_t, 1 ); p = ALLOC( Ssw_Sem_t, 1 );
memset( p, 0, sizeof(Ssw_Bmc_t) ); memset( p, 0, sizeof(Ssw_Sem_t) );
p->nConfMaxStart = nConfMax; p->nConfMaxStart = nConfMax;
p->nConfMax = nConfMax; p->nConfMax = nConfMax;
p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames ); p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
...@@ -83,10 +83,13 @@ Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) ...@@ -83,10 +83,13 @@ Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
p->vHistory = Vec_IntAlloc( 100 ); p->vHistory = Vec_IntAlloc( 100 );
Vec_IntPush( p->vHistory, 0 ); Vec_IntPush( p->vHistory, 0 );
// update arrays of the manager // update arrays of the manager
assert( 0 );
/*
free( p->pMan->pNodeToFrames ); free( p->pMan->pNodeToFrames );
Vec_IntFree( p->pMan->vSatVars ); Vec_IntFree( p->pMan->vSatVars );
p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep ); p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) ); p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
*/
return p; return p;
} }
...@@ -101,7 +104,7 @@ Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose ) ...@@ -101,7 +104,7 @@ Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_BmcManStop( Ssw_Bmc_t * p ) void Ssw_SemManStop( Ssw_Sem_t * p )
{ {
Vec_PtrFree( p->vTargets ); Vec_PtrFree( p->vTargets );
Vec_PtrFree( p->vPatterns ); Vec_PtrFree( p->vPatterns );
...@@ -120,7 +123,7 @@ void Ssw_BmcManStop( Ssw_Bmc_t * p ) ...@@ -120,7 +123,7 @@ void Ssw_BmcManStop( Ssw_Bmc_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_BmcCheckTargets( Ssw_Bmc_t * p ) int Ssw_SemCheckTargets( Ssw_Sem_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
...@@ -141,7 +144,7 @@ int Ssw_BmcCheckTargets( Ssw_Bmc_t * p ) ...@@ -141,7 +144,7 @@ int Ssw_BmcCheckTargets( Ssw_Bmc_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p ) void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
{ {
unsigned * pInfo; unsigned * pInfo;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
...@@ -168,7 +171,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p ) ...@@ -168,7 +171,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_ManFilterBmc( Ssw_Bmc_t * pBmc, int iPat, int fCheckTargets ) int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
{ {
Ssw_Man_t * p = pBmc->pMan; Ssw_Man_t * p = pBmc->pMan;
Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo; Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
...@@ -186,7 +189,6 @@ clk = clock(); ...@@ -186,7 +189,6 @@ clk = clock();
} }
// sweep internal nodes // sweep internal nodes
Ssw_ManStartSolver( p );
RetValue = pBmc->nFramesSweep; RetValue = pBmc->nFramesSweep;
for ( f = 0; f < pBmc->nFramesSweep; f++ ) for ( f = 0; f < pBmc->nFramesSweep; f++ )
{ {
...@@ -208,19 +210,19 @@ clk = clock(); ...@@ -208,19 +210,19 @@ clk = clock();
pBmc->nConfMax *= 10; pBmc->nConfMax *= 10;
} }
} }
if ( f > 0 && p->pSat->stats.conflicts >= pBmc->nConfMax ) if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
{ {
RetValue = -1; RetValue = -1;
break; break;
} }
} }
// quit if this is the last timeframe // quit if this is the last timeframe
if ( p->pSat->stats.conflicts >= pBmc->nConfMax ) if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
{ {
RetValue += f + 1; RetValue += f + 1;
break; break;
} }
if ( fCheckTargets && Ssw_BmcCheckTargets( pBmc ) ) if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
break; break;
// transfer latch input to the latch outputs // transfer latch input to the latch outputs
// build logic cones for register outputs // build logic cones for register outputs
...@@ -228,7 +230,7 @@ clk = clock(); ...@@ -228,7 +230,7 @@ clk = clock();
{ {
pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
} }
//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts ); //printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
} }
...@@ -252,15 +254,15 @@ p->timeBmc += clock() - clk; ...@@ -252,15 +254,15 @@ p->timeBmc += clock() - clk;
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ) int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
{ {
Ssw_Bmc_t * p; Ssw_Sem_t * p;
int RetValue, Frames, Iter, clk = clock(); int RetValue, Frames, Iter, clk = clock();
p = Ssw_BmcManStart( pMan, nConfMax, fVerbose ); p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
if ( fCheckTargets && Ssw_BmcCheckTargets( p ) ) if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
{ {
assert( 0 ); assert( 0 );
Ssw_BmcManStop( p ); Ssw_SemManStop( p );
return 1; return 1;
} }
if ( fVerbose ) if ( fVerbose )
...@@ -273,17 +275,18 @@ int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int f ...@@ -273,17 +275,18 @@ int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int f
for ( Iter = 0; Iter < p->nPatterns; Iter++ ) for ( Iter = 0; Iter < p->nPatterns; Iter++ )
{ {
clk = clock(); clk = clock();
pMan->pMSat = Ssw_SatStart( 0 );
Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets ); Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pSat->stats.conflicts, p->nPatterns, Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
p->pMan->nSatFailsReal? "f" : " " ); p->pMan->nSatFailsReal? "f" : " " );
PRT( "T", clock() - clk ); PRT( "T", clock() - clk );
} }
Ssw_ManCleanup( p->pMan ); Ssw_ManCleanup( p->pMan );
if ( fCheckTargets && Ssw_BmcCheckTargets( p ) ) if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
{ {
printf( "Target is hit!!!\n" ); printf( "Target is hit!!!\n" );
RetValue = 1; RetValue = 1;
...@@ -291,7 +294,7 @@ clk = clock(); ...@@ -291,7 +294,7 @@ clk = clock();
if ( p->nPatterns >= p->nPatternsAlloc ) if ( p->nPatterns >= p->nPatternsAlloc )
break; break;
} }
Ssw_BmcManStop( p ); Ssw_SemManStop( p );
pMan->nStrangers = 0; pMan->nStrangers = 0;
pMan->nSatCalls = 0; pMan->nSatCalls = 0;
......
src/aig/ssw/sswSim.c
...@@ -271,45 +271,6 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit ) ...@@ -271,45 +271,6 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ ); Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ );
} }
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SmlSavePattern( Ssw_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pFrames, pObj, i )
if ( p->pSat->model.ptr[Ssw_ObjSatNum(p, pObj)] == l_True )
Aig_InfoSetBit( p->pPatWords, i );
/*
if ( p->vCex )
{
Vec_IntClear( p->vCex );
for ( i = 0; i < Saig_ManPiNum(p->pAig); i++ )
Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
for ( i = Saig_ManPiNum(p->pFrames); i < Aig_ManPiNum(p->pFrames); i++ )
Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
}
*/
/*
printf( "Pattern: " );
Aig_ManForEachPi( p->pFrames, pObj, i )
printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
printf( "\n" );
*/
}
/**Function************************************************************* /**Function*************************************************************
......
src/aig/ssw/sswUnique.c
...@@ -30,83 +30,39 @@ ...@@ -30,83 +30,39 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.] Synopsis [Performs computation of signal correspondence with constraints.]
Description [Assumes that the vectors are sorted in the increasing order.] Description []
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr ) void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
{ {
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray; Aig_Obj_t * pObjLo, * pObj0, * pObj1;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray; int i;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray; if ( p->vDiffPairs == NULL )
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize; p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize; Vec_IntClear( p->vDiffPairs );
Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) ); Saig_ManForEachLo( p->pAig, pObjLo, i )
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{ {
if ( (*pBeg1)->Id == (*pBeg2)->Id ) pObj0 = Ssw_ObjFrame( p, pObjLo, 0 );
*pBeg++ = *pBeg1++, pBeg2++; pObj1 = Ssw_ObjFrame( p, pObjLo, 1 );
else if ( (*pBeg1)->Id < (*pBeg2)->Id ) if ( pObj0 == pObj1 )
*pBeg++ = *pBeg1++; Vec_IntPush( p->vDiffPairs, 0 );
else if ( pObj0 == Aig_Not(pObj1) )
Vec_IntPush( p->vDiffPairs, 1 );
else else
*pBeg++ = *pBeg2++; {
// assume that if the nodes are structurally different
// they can also be functionally different
Vec_IntPush( p->vDiffPairs, 1 );
}
} }
while ( pBeg1 < pEnd1 )
*pBeg++ = *pBeg1++;
while ( pBeg2 < pEnd2 )
*pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize >= vArr1->nSize );
assert( vArr->nSize >= vArr2->nSize );
} }
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
// *pBeg++ = *pBeg1++;
pBeg1++;
else
// *pBeg++ = *pBeg2++;
pBeg2++;
}
// while ( pBeg1 < pEnd1 )
// *pBeg++ = *pBeg1++;
// while ( pBeg2 < pEnd2 )
// *pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize <= vArr1->nSize );
assert( vArr->nSize <= vArr2->nSize );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -123,56 +79,32 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) ...@@ -123,56 +79,32 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{ {
int fVerbose = 0; int fVerbose = 0;
Aig_Obj_t * ppObjs[2], * pTemp; Aig_Obj_t * ppObjs[2], * pTemp;
Vec_Ptr_t * vSupp, * vSupp2; int i, k, Value0, Value1, RetValue, fFeasible;
int i, k, Value0, Value1, RetValue;
assert( p->pPars->nFramesK > 1 );
vSupp = Vec_PtrAlloc( 100 ); assert( p->pPars->nFramesK > 1 );
vSupp2 = Vec_PtrAlloc( 100 ); assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
Vec_PtrClear( p->vCommon );
// compute the first support in terms of LOs // compute the first support in terms of LOs
ppObjs[0] = pRepr; ppObjs[0] = pRepr;
ppObjs[1] = pObj; ppObjs[1] = pObj;
Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp ); Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
// modify support to be in terms of LIs // keep only LOs
RetValue = Vec_PtrSize( p->vCommon );
fFeasible = 0;
k = 0; k = 0;
Vec_PtrForEachEntry( vSupp, pTemp, i ) Vec_PtrForEachEntry( p->vCommon, pTemp, i )
if ( Saig_ObjIsLo(p->pAig, pTemp) ) if ( Saig_ObjIsLo(p->pAig, pTemp) )
Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) ); {
Vec_PtrShrink( vSupp, k ); Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
// compute the support of support if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 ); fFeasible = 1;
// return support to LO }
Vec_PtrForEachEntry( vSupp, pTemp, i ) Vec_PtrShrink( p->vCommon, k );
Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
// find the number of common vars
Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
/*
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
printf( "Not unique!\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
printf( "Not unique!\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
printf( "Not unique!\n" );
}
*/
if ( fVerbose ) if ( fVerbose )
printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ", printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) ); Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
fFeasible? "yes": "no " );
// check the current values // check the current values
RetValue = 1; RetValue = 1;
...@@ -185,14 +117,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) ...@@ -185,14 +117,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
if ( fVerbose ) if ( fVerbose )
printf( "%d", Value0 ^ Value1 ); printf( "%d", Value0 ^ Value1 );
} }
if ( Vec_PtrSize(p->vCommon) == 0 )
RetValue = 0;
if ( fVerbose ) if ( fVerbose )
printf( "\n" ); printf( "\n" );
Vec_PtrFree( vSupp ); return RetValue && fFeasible;
Vec_PtrFree( vSupp2 );
return RetValue;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -227,11 +155,10 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int ...@@ -227,11 +155,10 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
// printf( "Skipped\n" ); // printf( "Skipped\n" );
return 0; return 0;
} }
p->nUniques++;
// create CNF // create CNF
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) );
// add output constraint // add output constraint
pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) ); pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/* /*
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue ); assert( RetValue );
......
src/aig/ssw_old/module.make deleted 100644 → 0
SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswBmc.c \
src/aig/ssw/sswClass.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \
src/aig/ssw/sswPairs.c \
src/aig/ssw/sswSat.c \
src/aig/ssw/sswSim.c \
src/aig/ssw/sswSimSat.c \
src/aig/ssw/sswSweep.c \
src/aig/ssw/sswUnique.c
src/aig/ssw_old/ssw.h deleted 100644 → 0
/**CFile****************************************************************
FileName [ssw.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __SSW_H__
#define __SSW_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// choicing parameters
typedef struct Ssw_Pars_t_ Ssw_Pars_t;
struct Ssw_Pars_t_
{
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
int nConstrs; // treat the last nConstrs POs as seq constraints
int nMaxLevs; // the max number of levels of nodes to consider
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
int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints
int fVerbose; // verbose stats
// 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 nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
// internal parameters
int nIters; // the number of iterations performed
};
// sequential counter-example
typedef struct Ssw_Cex_t_ Ssw_Cex_t;
struct Ssw_Cex_t_
{
int iPo; // the zero-based number of PO, for which verification failed
int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
int nRegs; // the number of registers in the miter
int nPis; // the number of primary inputs in the miter
int nBits; // the number of words of bit data used
unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
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 );
/*=== sswLoc.c ==========================================================*/
extern int Saig_ManLocalization( Aig_Man_t * p, int nFramesMax, int nConfMax, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswSim.c ===================================================*/
extern Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
extern Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswAig.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswAig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [AIG manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame, int fTwoPos )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
// skip nodes without representative
pObjRepr = Aig_ObjRepr(pAig, pObj);
if ( pObjRepr == NULL )
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
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_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
// add the constraint
if ( fTwoPos )
{
Aig_ObjCreatePo( pFrames, pObjNew2 );
Aig_ObjCreatePo( pFrames, pObjNew );
}
else
{
pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
}
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
int i, f;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// set the constraints on the latch outputs
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
// add internal nodes of this frame
Aig_ManForEachNode( p->pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
}
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
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_ObjFrame( p, pObj, p->pPars->nFramesK ) );
for ( f = 0; f <= p->pPars->nFramesK; f++ )
Saig_ManForEachLo( p->pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, f ) );
// remove dangling nodes
Aig_ManCleanup( pFrames );
// make sure the satisfying assignment is node assigned
assert( pFrames->pData == NULL );
//Aig_ManShow( pFrames, 0, NULL );
return pFrames;
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// set the constraints on the latch outputs
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
// add internal nodes of this frame
Aig_ManForEachNode( p->pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
}
// add the POs for the latch outputs of the last frame
Saig_ManForEachLi( p->pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
// remove dangling nodes
Aig_ManCleanup( pFrames );
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
p->nConstrTotal, p->nConstrReduced );
return pFrames;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswMan.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Calls to the SAT solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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;
p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving
p->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
p->vFanins = Vec_PtrAlloc( 100 );
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
p->vCommon = Vec_PtrAlloc( 100 );
p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatWords2 = ALLOC( unsigned, p->nPatWords );
return p;
}
/**Function*************************************************************
Synopsis [Prints stats of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManCountEquivs( Ssw_Man_t * p )
{
Aig_Obj_t * pObj;
int i, nEquivs = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL );
return nEquivs;
}
/**Function*************************************************************
Synopsis [Prints stats of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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. 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) );
p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
PRTP( "BMC ", p->timeBmc, p->timeTotal );
PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
PRTP( "SAT solving", p->timeSat, 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 );
}
/**Function*************************************************************
Synopsis [Frees the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p )
{
if ( p->pFrames )
{
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->pSat )
{
int i;
// printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
p->nSatVarsTotal += p->pSat->size;
sat_solver_delete( p->pSat );
p->pSat = NULL;
// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
for ( i = 0; i < Vec_IntSize(p->vSatVars); i++ )
p->vSatVars->pArray[i] = 0;
}
if ( p->vSimInfo )
{
Vec_PtrFree( p->vSimInfo );
p->vSimInfo = NULL;
}
p->nConstrTotal = 0;
p->nConstrReduced = 0;
}
/**Function*************************************************************
Synopsis [Frees the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 )
Ssw_ClassesStop( p->ppClasses );
if ( p->pSml )
Ssw_SmlStop( p->pSml );
Vec_PtrFree( p->vFanins );
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
Vec_IntFree( p->vSatVars );
Vec_PtrFree( p->vCommon );
FREE( p->pNodeToFrames );
FREE( p->pPatWords );
FREE( p->pPatWords2 );
free( p );
}
/**Function*************************************************************
Synopsis [Starts the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManStartSolver( Ssw_Man_t * p )
{
int Lit;
assert( p->pSat == NULL );
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
// var 0 is not used
// var 1 is reserved for const1 node - add the clause
p->nSatVars = 1;
Lit = toLit( p->nSatVars );
if ( p->pPars->fPolarFlip )
Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
Vec_PtrClear( p->vUsedNodes );
Vec_PtrClear( p->vUsedPis );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswPart.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswPart.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Partitioned signal correspondence.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweepingG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 0;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
int clk = clock();
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
}
else
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
if ( fPrintParts )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
}
// perform SSW with partitions
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
Aig_ManSetRegNum( pTemp, pTemp->nRegs );
// create the projection of 1-hot registers
if ( pAig->vOnehots )
pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
// run SSW
pNew = Ssw_SignalCorrespondence( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
if ( fVerbose )
printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
Aig_ManStop( pTemp );
free( pMapBack );
}
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
PRT( "Total time", clock() - clk );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswSat.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Calls to the SAT solver.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description [Both nodes should be regular and different from each other.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int nBTLimit = p->pPars->nBTLimit;
int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
p->nSatCalls++;
// sanity checks
assert( !Aig_IsComplement(pOld) );
assert( !Aig_IsComplement(pNew) );
assert( pOld != pNew );
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 );
if ( p->pSat->qtail != p->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
}
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->nSatFailsReal++;
return -1;
}
// if the old node was constant 0, we already know the answer
if ( pOld == Aig_ManConst1(p->pFrames) )
{
p->nSatProof++;
return 1;
}
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
nLits = 2;
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
if ( p->iOutputLit > -1 )
pLits[nLits++] = p->iOutputLit;
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
/*
if ( p->pSat->qtail != p->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
}
*/
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + nLits,
(sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
if ( nLits == 2 )
{
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->nSatFailsReal++;
return -1;
}
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Constrains two nodes to be equivalent in the SAT solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{
int pLits[2], RetValue, fComplNew;
Aig_Obj_t * pTemp;
// sanity checks
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, 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) )
{
// 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] );
}
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
}
else
{
// 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), !fComplNew );
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// (!A v B)
pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
if ( p->pPars->fPolarFlip )
{
if ( pOld->fPhase ) pLits[0] = lit_neg( pLits[0] );
if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] );
}
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswSimSat.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswSimSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Performs resimulation using counter-examples.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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();
// set the PI simulation information
Aig_ManConst1(p->pAig)->fMarkB = 1;
Aig_ManForEachPi( p->pAig, pObj, i )
pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
// 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, 0 );
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
/**Function*************************************************************
Synopsis [Verifies the result of simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateWordVerify( Ssw_Man_t * p, int f )
{
Aig_Obj_t * pObj, * pObjFraig;
unsigned uWord;
int Value1, Value2;
int i, nVarNum, Counter = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
{
pObjFraig = Ssw_ObjFrame( p, pObj, f );
if ( pObjFraig == NULL )
continue;
nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
if ( nVarNum == 0 )
continue;
Value1 = Ssw_ManGetSatVarValue( p, pObj, f );
uWord = Ssw_SmlObjGetWord( p->pSml, pObj, 0, 0 );
Value2 = ((uWord != 0) ^ pObj->fPhase);
Counter += (Value1 != Value2);
if ( Value1 != Value2 )
{
/*
int Value1f = Ssw_ManGetSatVarValue( p, Aig_ObjFanin0(pObj), f );
int Value2f = Ssw_ManGetSatVarValue( p, Aig_ObjFanin1(pObj), f );
*/
int x = 0;
int Value3 = Ssw_ManGetSatVarValue( p, pObj, f );
}
}
if ( Counter )
printf( "Counter = %d.\n", Counter );
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
// simulate internal nodes
Ssw_SmlSimulateOne( p->pSml );
Ssw_ManResimulateWordVerify( p, f );
// check equivalence classes
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
/**Function*************************************************************
Synopsis [Handle the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManResimulateWord2( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
{
int RetValue1, RetValue2, clk = clock();
// set the PI simulation information
Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords2 );
// simulate internal nodes
Ssw_SmlSimulateOne( p->pSml );
Ssw_ManResimulateWordVerify( p, f );
// check equivalence classes
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ssw_old/sswUnique.c deleted 100644 → 0
/**CFile****************************************************************
FileName [sswSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [On-demand uniqueness constraints.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrTwoMerge( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
*pBeg++ = *pBeg1++;
else
*pBeg++ = *pBeg2++;
}
while ( pBeg1 < pEnd1 )
*pBeg++ = *pBeg1++;
while ( pBeg2 < pEnd2 )
*pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize >= vArr1->nSize );
assert( vArr->nSize >= vArr2->nSize );
}
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrTwoCommon( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr )
{
Aig_Obj_t ** pBeg = (Aig_Obj_t **)vArr->pArray;
Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, AIG_MIN( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( (*pBeg1)->Id == (*pBeg2)->Id )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( (*pBeg1)->Id < (*pBeg2)->Id )
// *pBeg++ = *pBeg1++;
pBeg1++;
else
// *pBeg++ = *pBeg2++;
pBeg2++;
}
// while ( pBeg1 < pEnd1 )
// *pBeg++ = *pBeg1++;
// while ( pBeg2 < pEnd2 )
// *pBeg++ = *pBeg2++;
vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize <= vArr1->nSize );
assert( vArr->nSize <= vArr2->nSize );
}
/**Function*************************************************************
Synopsis [Returns 1 if uniqueness constraints can be added.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
int fVerbose = 1;
Aig_Obj_t * ppObjs[2], * pTemp;
Vec_Ptr_t * vSupp, * vSupp2;
int i, k, Value0, Value1, RetValue;
assert( p->pPars->nFramesK > 1 );
vSupp = Vec_PtrAlloc( 100 );
vSupp2 = Vec_PtrAlloc( 100 );
Vec_PtrClear( p->vCommon );
// compute the first support in terms of LOs
ppObjs[0] = pRepr;
ppObjs[1] = pObj;
Aig_SupportNodes( p->pAig, ppObjs, 2, vSupp );
// modify support to be in terms of LIs
k = 0;
Vec_PtrForEachEntry( vSupp, pTemp, i )
if ( Saig_ObjIsLo(p->pAig, pTemp) )
Vec_PtrWriteEntry( vSupp, k++, Saig_ObjLoToLi(p->pAig, pTemp) );
Vec_PtrShrink( vSupp, k );
// compute the support of support
Aig_SupportNodes( p->pAig, (Aig_Obj_t **)Vec_PtrArray(vSupp), Vec_PtrSize(vSupp), vSupp2 );
// return support to LO
Vec_PtrForEachEntry( vSupp, pTemp, i )
Vec_PtrWriteEntry( vSupp, i, Saig_ObjLiToLo(p->pAig, pTemp) );
// find the number of common vars
Vec_PtrSort( vSupp, Aig_ObjCompareIdIncrease );
Vec_PtrSort( vSupp2, Aig_ObjCompareIdIncrease );
Vec_PtrTwoCommon( vSupp, vSupp2, p->vCommon );
// Vec_PtrTwoMerge( vSupp, vSupp2, p->vCommon );
/*
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp) )
printf( "Not unique!\n" );
Vec_PtrFree( vNew );
Vec_PtrForEachEntry( vSupp, pTemp, i )
printf( "%d ", pTemp->Id );
printf( "\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(vSupp2);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(vSupp2) )
printf( "Not unique!\n" );
Vec_PtrFree( vNew );
Vec_PtrForEachEntry( vSupp2, pTemp, i )
printf( "%d ", pTemp->Id );
printf( "\n" );
}
{
Vec_Ptr_t * vNew = Vec_PtrDup(p->vCommon);
Vec_PtrUniqify( vNew, Aig_ObjCompareIdIncrease );
if ( Vec_PtrSize(vNew) != Vec_PtrSize(p->vCommon) )
printf( "Not unique!\n" );
Vec_PtrFree( vNew );
Vec_PtrForEachEntry( p->vCommon, pTemp, i )
printf( "%d ", pTemp->Id );
printf( "\n" );
}
*/
if ( fVerbose )
printf( "Node = %5d : One = %3d. Two = %3d. Common = %3d. ",
Aig_ObjId(pObj), Vec_PtrSize(vSupp), Vec_PtrSize(vSupp2), Vec_PtrSize(p->vCommon) );
// Vec_PtrClear( vSupp );
// Vec_PtrForEachEntry( vSupp2, pTemp, i )
// Vec_PtrPush( vSupp, pTemp );
// check the current values
RetValue = 1;
// Vec_PtrForEachEntry( p->vCommon, pTemp, i )
Vec_PtrForEachEntry( vSupp, pTemp, i )
{
Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
if ( Value0 != Value1 )
RetValue = 0;
if ( fVerbose )
printf( "%d", Value0 ^ Value1 );
}
if ( Vec_PtrSize(p->vCommon) == 0 )
RetValue = 0;
Vec_PtrForEachEntry( vSupp, pTemp, i )
printf( " %d", pTemp->Id );
if ( fVerbose )
printf( "\n" );
Vec_PtrClear( p->vCommon );
Vec_PtrForEachEntry( vSupp, pTemp, i )
Vec_PtrPush( p->vCommon, pTemp );
Vec_PtrFree( vSupp );
Vec_PtrFree( vSupp2 );
return RetValue;
}
/**Function*************************************************************
Synopsis [Returns the output of the uniqueness constraint.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 )
{
Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
int i, pLits[2];
// int RetValue;
assert( Vec_PtrSize(vCommon) > 0 );
// generate the constraint
pTotal = Aig_ManConst0(p->pFrames);
Vec_PtrForEachEntry( vCommon, pObj, i )
{
assert( Saig_ObjIsLo(p->pAig, pObj) );
pObj1New = Ssw_ObjFrame( p, pObj, f1 );
pObj2New = Ssw_ObjFrame( p, pObj, f2 );
pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
}
/*
if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
{
// printf( "Skipped\n" );
return 0;
}
*/
p->nUniques++;
// create CNF
// {
// int Num1 = p->nSatVars;
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pTotal) );
// printf( "Created variable %d while vars are %d. (diff = %d)\n",
// Ssw_ObjSatNum( p, Aig_Regular(pTotal) ), p->nSatVars, p->nSatVars - Num1 );
// }
// add output constraint
pLits[0] = toLitCond( Ssw_ObjSatNum(p,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// simplify the solver
if ( p->pSat->qtail != p->pSat->qhead )
{
RetValue = sat_solver_simplify(p->pSat);
assert( RetValue != 0 );
}
*/
assert( p->iOutputLit == -1 );
p->iOutputLit = pLits[0];
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
...@@ -215,7 +215,7 @@ static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** arg ...@@ -215,7 +215,7 @@ static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmcInter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLocalize ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -483,7 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -483,7 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 ); Cmd_CommandAdd( pAbc, "Verification", "int", Abc_CommandBmcInter, 0 );
Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 ); Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 );
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 ); Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
Cmd_CommandAdd( pAbc, "Verification", "loc", Abc_CommandLocalize, 0 ); Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
...@@ -620,7 +620,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -620,7 +620,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fDumpResult = 0; fDumpResult = 0;
fUseLutLib = 0; fUseLutLib = 0;
fPrintTime = 0; fPrintTime = 0;
fPrintMuxes = 1; fPrintMuxes = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF )
{ {
...@@ -7936,7 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -7936,7 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/ */
/*
pNtkRes = Abc_NtkDarTestNtk( pNtk ); pNtkRes = Abc_NtkDarTestNtk( pNtk );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
...@@ -7945,9 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -7945,9 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// replace the current network // replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
Abc_NtkDarTest( pNtk );
// Abc_NtkDarTest( pNtk );
return 0; return 0;
usage: usage:
...@@ -13559,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13559,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Ssw_ManSetDefaultParams( pPars ); Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfuvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIplfuvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -13640,15 +13640,23 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13640,15 +13640,23 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesAddSim < 0 ) if ( pPars->nFramesAddSim < 0 )
goto usage; goto usage;
break; break;
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nItersStop = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nItersStop < 0 )
goto usage;
break;
case 'p': case 'p':
pPars->fPolarFlip ^= 1; pPars->fPolarFlip ^= 1;
break; break;
case 'l': case 'l':
pPars->fLatchCorr ^= 1; pPars->fLatchCorr ^= 1;
break; break;
case 's':
pPars->fSkipCheck ^= 1;
break;
case 'f': case 'f':
pPars->fSemiFormal ^= 1; pPars->fSemiFormal ^= 1;
break; break;
...@@ -13710,7 +13718,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -13710,7 +13718,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfuvwh]\n" ); fprintf( pErr, "usage: scorr [-PQFCLNSI <num>] [-plfuvwh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\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-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 ); fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
...@@ -13719,10 +13727,10 @@ usage: ...@@ -13719,10 +13727,10 @@ usage:
fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs ); fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
fprintf( pErr, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim ); fprintf( pErr, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
fprintf( pErr, "\t-I num : iteration number to stop and output SR-model (0=none) [default = %d]\n", pPars->nItersStop );
fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" ); // fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" ); fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" );
...@@ -16560,7 +16568,7 @@ usage: ...@@ -16560,7 +16568,7 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
...@@ -16575,8 +16583,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -16575,8 +16583,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// set defaults // set defaults
nFramesMax = 50; nFramesMax = 100;
nConfMax = 500; nConfMax = 1000;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
...@@ -16639,8 +16647,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -16639,8 +16647,8 @@ int Abc_CommandLocalize( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose ); Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose );
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: loc [-FC num] [-vh]\n" ); fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
fprintf( pErr, "\t performs localization for single-output miter\n" ); fprintf( pErr, "\t runs K-step induction for the property output\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
...@@ -19121,7 +19129,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19121,7 +19129,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
Ssw_ManSetDefaultParams( pPars ); Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDplsvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDplvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -19219,9 +19227,6 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19219,9 +19227,6 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l': case 'l':
pPars->fLatchCorr ^= 1; pPars->fLatchCorr ^= 1;
break; break;
case 's':
pPars->fSkipCheck ^= 1;
break;
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
...@@ -19268,7 +19273,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -19268,7 +19273,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plsvh]\n" ); fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" ); fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
...@@ -19280,7 +19285,6 @@ usage: ...@@ -19280,7 +19285,6 @@ usage:
fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize ); fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( stdout, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n"); fprintf( stdout, "\t-h : print the command usage\n");
return 1; return 1;
......
src/base/abci/abcDar.c
...@@ -1465,7 +1465,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in ...@@ -1465,7 +1465,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ) int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
{ {
Aig_Man_t * pMan; Aig_Man_t * pMan;
int RetValue = -1, clk = clock(); int status, RetValue = -1, clk = clock();
// derive the AIG manager // derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL ) if ( pMan == NULL )
...@@ -1494,6 +1494,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in ...@@ -1494,6 +1494,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
} }
else else
{ {
/*
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose ); Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
FREE( pNtk->pModel ); FREE( pNtk->pModel );
FREE( pNtk->pSeqModel ); FREE( pNtk->pSeqModel );
...@@ -1509,8 +1510,30 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in ...@@ -1509,8 +1510,30 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
printf( "No output was asserted in %d frames. ", nFrames ); printf( "No output was asserted in %d frames. ", nFrames );
RetValue = 1; RetValue = 1;
} }
*/
int iFrame;
RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
printf( "No output was asserted in %d frames. ", iFrame );
else if ( RetValue == -1 )
printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
} }
PRT( "Time", clock() - clk ); PRT( "Time", clock() - clk );
// verify counter-example
if ( pNtk->pSeqModel )
{
status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return RetValue; return RetValue;
} }
...@@ -2128,7 +2151,7 @@ void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVe ...@@ -2128,7 +2151,7 @@ void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVe
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL ) if ( pMan == NULL )
return; return;
RetValue = Saig_ManLocalization( pTemp = pMan, nFramesMax, nConfMax, fVerbose ); RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
if ( RetValue == 1 ) if ( RetValue == 1 )
{ {
......
src/base/abci/abcPrint.c
...@@ -114,7 +114,6 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) ...@@ -114,7 +114,6 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ) void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes )
{ {
int Num; int Num;
if ( fSaveBest ) if ( fSaveBest )
Abc_NtkCompareAndSaveBest( pNtk ); Abc_NtkCompareAndSaveBest( pNtk );
if ( fDumpResult ) if ( fDumpResult )
...@@ -147,15 +146,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave ...@@ -147,15 +146,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) );
if ( (Num = Abc_NtkGetChoiceNum(pNtk)) ) if ( (Num = Abc_NtkGetChoiceNum(pNtk)) )
fprintf( pFile, " (choice = %d)", Num ); fprintf( pFile, " (choice = %d)", Num );
if ( (Num = Abc_NtkGetExorNum(pNtk)) )
fprintf( pFile, " (exor = %d)", Num );
// if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
// fprintf( pFile, " (mux = %d)", Num2-Num );
// if ( Num2 )
// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
if ( fPrintMuxes ) if ( fPrintMuxes )
{ {
extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk ); extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk );
Num = Abc_NtkGetExorNum(pNtk);
fprintf( pFile, " (exor = %d)", Num );
fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num ); fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num );
fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) ); fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) );
} }
......
src/misc/vec/vecInt.h
...@@ -382,12 +382,12 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin ) ...@@ -382,12 +382,12 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry ) static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Fill )
{ {
int i; int i;
Vec_IntGrow( p, nSize ); Vec_IntGrow( p, nSize );
for ( i = 0; i < nSize; i++ ) for ( i = 0; i < nSize; i++ )
p->pArray[i] = Entry; p->pArray[i] = Fill;
p->nSize = nSize; p->nSize = nSize;
} }
...@@ -402,20 +402,40 @@ static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry ) ...@@ -402,20 +402,40 @@ static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry ) static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Fill )
{ {
int i; int i;
if ( p->nSize >= nSize ) if ( p->nSize >= nSize )
return; return;
Vec_IntGrow( p, nSize ); if ( 2 * p->nSize > nSize )
Vec_IntGrow( p, 2 * nSize );
else
Vec_IntGrow( p, nSize );
for ( i = p->nSize; i < nSize; i++ ) for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry; p->pArray[i] = Fill;
p->nSize = nSize; p->nSize = nSize;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Returns the entry even if the place not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntGetEntry( Vec_Int_t * p, int i )
{
Vec_IntFillExtra( p, i + 1, 0 );
return Vec_IntEntry( p, i );
}
/**Function*************************************************************
Synopsis [Inserts the entry even if the place does not exist.]
Description [] Description []
...@@ -424,11 +444,9 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry ) ...@@ -424,11 +444,9 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntWriteEntryFill( Vec_Int_t * p, int i, int Entry ) static inline void Vec_IntSetEntry( Vec_Int_t * p, int i, int Entry )
{ {
assert( i >= 0 ); Vec_IntFillExtra( p, i + 1, 0 );
if ( i >= p->nSize )
Vec_IntFillExtra( p, 2 * i, 0 );
Vec_IntWriteEntry( p, i, Entry ); Vec_IntWriteEntry( p, i, Entry );
} }
......
src/sat/bsat/satInter.c
...@@ -718,6 +718,27 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin ...@@ -718,6 +718,27 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
Int_ManPrintResolvent( p->pResLits, p->nResLits ); Int_ManPrintResolvent( p->pResLits, p->nResLits );
Int_ManPrintClause( p, pFinal ); Int_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; p->timeTrace += clock() - clk;
...@@ -727,6 +748,8 @@ p->timeTrace += clock() - clk; ...@@ -727,6 +748,8 @@ p->timeTrace += clock() - clk;
// Int_ManPrintInterOne( p, pFinal ); // Int_ManPrintInterOne( p, pFinal );
} }
Int_ManProofSet( p, pFinal, p->Counter ); Int_ManProofSet( p, pFinal, p->Counter );
// make sure the same proof ID is not asssigned to two consecutive clauses
assert( p->pProofNums[pFinal->Id-1] != p->Counter );
return p->Counter; return p->Counter;
} }
...@@ -754,6 +777,13 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause ) ...@@ -754,6 +777,13 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
// add assumptions to the trail // add assumptions to the trail
assert( !pClause->fRoot ); assert( !pClause->fRoot );
assert( p->nTrailSize == p->nRootSize ); 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;
for ( i = 0; i < (int)pClause->nLits; i++ ) for ( i = 0; i < (int)pClause->nLits; i++ )
if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{ {
...@@ -769,6 +799,27 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause ) ...@@ -769,6 +799,27 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
return 0; return 0;
} }
// skip the clause if it is weaker or the same as the conflict clause
if ( pClause->nLits >= pConflict->nLits )
{
// check if every literal of conflict clause can be found in the given clause
int j;
for ( i = 0; i < (int)pConflict->nLits; i++ )
{
for ( j = 0; j < (int)pClause->nLits; j++ )
if ( pConflict->pLits[i] == pClause->pLits[j] )
break;
if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
break;
}
if ( i == (int)pConflict->nLits ) // all lits are found
{
// undo to the root level
Int_ManCancelUntil( p, p->nRootSize );
return 1;
}
}
// construct the proof // construct the proof
Int_ManProofTraceOne( p, pConflict, pClause ); Int_ManProofTraceOne( p, pConflict, pClause );
...@@ -854,8 +905,12 @@ int Int_ManProcessRoots( Int_Man_t * p ) ...@@ -854,8 +905,12 @@ int Int_ManProcessRoots( Int_Man_t * p )
if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
{ {
// detected root level conflict // detected root level conflict
printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" ); // printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
assert( 0 ); // assert( 0 );
// detected root level conflict
Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
if ( p->fVerbose )
printf( "Found root level conflict!\n" );
return 0; return 0;
} }
} }
......
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