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

Replaced printfs with Abc_Print

This commit is contained in:
Niklas Een 2012-10-29 15:35:02 -07:00
parent 1e8565eee3
commit c3168ba661
20 changed files with 465 additions and 451 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -86,7 +86,7 @@ clean:
@rm -rvf $(PROG) lib$(PROG).a $(OBJ) $(GARBAGE) $(OBJ:.o=.d)
tags:
ctags -R .
etags `find . -type f -regex '.*\.\(c\|h\)'`
$(PROG): $(OBJ)
@echo "\`\` Building binary:" $(notdir $@)

46
src/proof/pdr/pdrTsim.c
View File

@ -152,14 +152,14 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Synopsis [Performs ternary simulation for one design.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Pdr_ManSimDataInit( Aig_Man_t * pAig,
Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
int Pdr_ManSimDataInit( Aig_Man_t * pAig,
Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
{
Aig_Obj_t * pObj;
@ -190,7 +190,7 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig,
Synopsis [Tries to assign ternary value to one of the CIs.]
Description []
SideEffects []
SeeAlso []
@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
// collect CO objects
Vec_IntClear( vCoObjs );
if ( pCube == NULL ) // the target is the property output
Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
else // the target is the cube
{
for ( i = 0; i < pCube->nLits; i++ )
@ -400,6 +400,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
assert( RetValue );
#if 1
// try removing high-priority flops
Vec_IntClear( vCi2Rem );
Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
@ -429,10 +430,42 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
else
Pdr_ManExtendUndo( p->pAig, vUndo );
}
#else
// try removing low-priority flops
Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
{
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue;
Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
continue;
Vec_IntClear( vUndo );
if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
else
Pdr_ManExtendUndo( p->pAig, vUndo );
}
// try removing high-priority flops
Vec_IntClear( vCi2Rem );
Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
{
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue;
Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
continue;
Vec_IntClear( vUndo );
if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
else
Pdr_ManExtendUndo( p->pAig, vUndo );
}
#endif
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
assert( RetValue );
assert( RetValue );
// derive the set of resulting registers
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
@ -447,4 +480,3 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
ABC_NAMESPACE_IMPL_END

17
src/proof/ssw/sswAig.c
View File

@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
{
Ssw_Frm_t * p;
p = ABC_ALLOC( Ssw_Frm_t, 1 );
p = ABC_ALLOC( Ssw_Frm_t, 1 );
memset( p, 0, sizeof(Ssw_Frm_t) );
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax( pAig );
@ -80,7 +80,7 @@ void Ssw_FrmStop( Ssw_Frm_t * p )
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
@ -95,7 +95,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
// get the new node
// get the new node
pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
@ -135,7 +135,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
@ -181,7 +181,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
// transfer to the primary outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
// transfer latch input to the latch outputs
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
}
@ -203,7 +203,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
@ -218,7 +218,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
p->nConstrTotal = p->nConstrReduced = 0;
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
@ -245,7 +245,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
// remove dangling nodes
Aig_ManCleanup( pFrames );
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
// printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
// Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n",
// p->nConstrTotal, p->nConstrReduced );
return pFrames;
}
@ -256,4 +256,3 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END

17
src/proof/ssw/sswBmc.c
View File

@ -60,10 +60,10 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
{
if ( f == 0 )
pRes = Aig_ManConst0( pFrm->pFrames );
else
else
pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
}
else
else
{
assert( Aig_ObjIsNode(pObj) );
Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
@ -81,7 +81,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
Synopsis [Derives counter-example.]
Description []
SideEffects []
SeeAlso []
@ -140,7 +140,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
// report statistics
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
Abc_Print( 1, "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
fflush( stdout );
@ -162,7 +162,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
if ( fVerbose )
{
printf( "Solving output %2d of frame %3d ... \r",
Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@ -199,9 +199,9 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
}
if ( fVerbose )
{
printf( "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
printf( "Conf =%8.0f. Var =%8d. AIG=%9d. ",
(double)pSat->pSat->stats.conflicts,
Abc_Print( 1, "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
(double)pSat->pSat->stats.conflicts,
pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
ABC_PRT( "T", clock() - clkPart );
clkPart = clock();
@ -222,4 +222,3 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
ABC_NAMESPACE_IMPL_END

27
src/proof/ssw/sswCnf.c
View File

@ -46,7 +46,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
{
Ssw_Sat_t * p;
int Lit;
p = ABC_ALLOC( Ssw_Sat_t, 1 );
p = ABC_ALLOC( Ssw_Sat_t, 1 );
memset( p, 0, sizeof(Ssw_Sat_t) );
p->pAig = NULL;
p->fPolarFlip = fPolarFlip;
@ -80,7 +80,7 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
***********************************************************************/
void Ssw_SatStop( Ssw_Sat_t * p )
{
// printf( "Recycling SAT solver with %d vars and %d restarts.\n",
// Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n",
// p->pSat->size, p->pSat->stats.starts );
if ( p->pSat )
sat_solver_delete( p->pSat );
@ -174,10 +174,10 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t & e -> f
// t + e + f'
// t' + e' + f
// t' + e' + f
if ( VarT == VarE )
{
@ -214,7 +214,7 @@ void Ssw_AddClausesMux( Ssw_Sat_t * p, Aig_Obj_t * pNode )
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
@ -267,7 +267,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
@ -276,8 +276,8 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
(!fFirst && Aig_ObjRefs(pObj) > 1) ||
if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
(!fFirst && Aig_ObjRefs(pObj) > 1) ||
(fUseMuxes && Aig_ObjIsMuxType(pObj)) )
{
Vec_PtrPushUnique( vSuper, pObj );
@ -294,7 +294,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
@ -313,7 +313,7 @@ void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
@ -342,14 +342,14 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
{
{
Vec_Ptr_t * vFrontier;
Aig_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
@ -393,7 +393,7 @@ void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj )
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
@ -425,4 +425,3 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
ABC_NAMESPACE_IMPL_END

69
src/proof/ssw/sswConstr.c
View File

@ -77,32 +77,32 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
continue;
Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
}
// transfer latch inputs to the latch outputs
// transfer latch inputs to the latch outputs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
Aig_ObjSetCopy( pObjLo, Aig_ObjCopy(pObjLi) );
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
return pFrames;
}
return pFrames;
}
/**Function*************************************************************
Synopsis [Finds one satisfiable assignment of the timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
{
{
Aig_Man_t * pFrames;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
Aig_Obj_t * pObj;
int i, RetValue;
if ( pvInits )
*pvInits = NULL;
@ -110,7 +110,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
// derive the timeframes
pFrames = Ssw_FramesWithConstraints( p, nFrames );
// create CNF
pCnf = Cnf_Derive( pFrames, 0 );
pCnf = Cnf_Derive( pFrames, 0 );
// create SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
@ -120,7 +120,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
return 1;
}
// solve
RetValue = sat_solver_solve( pSat, NULL, NULL,
RetValue = sat_solver_solve( pSat, NULL, NULL,
(ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_True && pvInits )
{
@ -129,8 +129,8 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );
// Aig_ManForEachCi( pFrames, pObj, i )
// printf( "%d", Vec_IntEntry(*pvInits, i) );
// printf( "\n" );
// Abc_Print( 1, "%d", Vec_IntEntry(*pvInits, i) );
// Abc_Print( 1, "\n" );
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
@ -154,19 +154,19 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
***********************************************************************/
int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
{
{
Vec_Int_t * vLits;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj;
Aig_Obj_t * pObj;
int i, f, iVar, RetValue, nRegs;
if ( pvInits )
*pvInits = NULL;
assert( p->nConstrs > 0 );
// create CNF
nRegs = p->nRegs; p->nRegs = 0;
pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );
p->nRegs = nRegs;
pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );
p->nRegs = nRegs;
// create SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
assert( pSat->size == nFrames * pCnf->nVars );
@ -188,8 +188,8 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
Vec_IntPush( vLits, toLitCond(iVar, 1) );
}
}
RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits),
(int *)Vec_IntArray(vLits) + Vec_IntSize(vLits),
RetValue = sat_solver_solve( pSat, (int *)Vec_IntArray(vLits),
(int *)Vec_IntArray(vLits) + Vec_IntSize(vLits),
(ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_True && pvInits )
{
@ -225,12 +225,12 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
***********************************************************************/
void Ssw_ManPrintPolarity( Aig_Man_t * p )
{
{
Aig_Obj_t * pObj;
int i;
Aig_ManForEachObj( p, pObj, i )
printf( "%d", pObj->fPhase );
printf( "\n" );
Abc_Print( 1, "%d", pObj->fPhase );
Abc_Print( 1, "\n" );
}
/**Function*************************************************************
@ -245,7 +245,7 @@ void Ssw_ManPrintPolarity( Aig_Man_t * p )
***********************************************************************/
void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
{
{
Aig_Obj_t * pObj, * pObjLi;
int f, i, iLits, RetValue1, RetValue2;
int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig);
@ -276,12 +276,12 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
{
if ( pObj->fMarkB )
printf( "output %d failed in frame %d.\n", i, f );
Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
}
else
{
if ( pObj->fMarkB )
printf( "constraint %d failed in frame %d.\n", i, f );
Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
}
}
// transfer
@ -312,7 +312,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
***********************************************************************/
int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
{
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
// get representative of this class
@ -328,7 +328,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return 0;
return 0;
// call equivalence checking
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@ -351,7 +351,7 @@ int Ssw_ManSweepNodeConstr( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
printf( "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" );
Abc_Print( 1, "Ssw_ManSweepNodeConstr(): Failed to refine representative.\n" );
}
return 1;
}
@ -398,7 +398,7 @@ Aig_Obj_t * Ssw_ManSweepBmcConstr_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
@ -464,7 +464,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
// transfer latch input to the latch outputs
// transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@ -489,7 +489,7 @@ p->timeBmc += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
@ -545,7 +545,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
// transfer latch input to the latch outputs
// transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@ -572,7 +572,7 @@ p->timeBmc += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
@ -610,14 +610,14 @@ Aig_Obj_t * Ssw_FramesWithClasses_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepConstr( Ssw_Man_t * p )
{
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, i, f, iLits;
@ -672,7 +672,7 @@ p->timeReduce += clock() - clk;
assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) );
if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) )
{
printf( "Polarity violation.\n" );
Abc_Print( 1, "Polarity violation.\n" );
continue;
}
Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) );
@ -695,7 +695,7 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
else if ( Aig_ObjIsNode(pObj) )
{
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
@ -714,4 +714,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END

33
src/proof/ssw/sswDyn.c
View File

@ -94,7 +94,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
Synopsis [Collects new POs in p->vNewPos.]
Description []
SideEffects []
SeeAlso []
@ -129,11 +129,11 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
Synopsis [Loads logic cones and relevant constraints.]
Description [Both pRepr and pObj are objects of the AIG.
Description [Both pRepr and pObj are objects of the AIG.
The result is the current SAT solver loaded with the logic cones
for pRepr and pObj corresponding to them in the frames,
for pRepr and pObj corresponding to them in the frames,
as well as all the relevant constraints.]
SideEffects []
SeeAlso []
@ -151,7 +151,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
assert( pReprFrames != pObjFrames );
/*
// compute the AIG support
// compute the AIG support
Vec_PtrClear( p->vNewLos );
Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
Ssw_ManCollectPis_rec( pObj, p->vNewLos );
@ -166,7 +166,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
// compute the frames support
// compute the frames support
Vec_PtrClear( p->vNewLos );
Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos );
@ -202,7 +202,7 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
Synopsis [Tranfers simulation information from FRAIG to AIG.]
Description []
SideEffects []
SeeAlso []
@ -254,7 +254,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
Synopsis [Performs one round of simulation with counter-examples.]
Description []
SideEffects []
SeeAlso []
@ -286,7 +286,7 @@ p->timeSimSat += clock() - clk;
Synopsis [Performs one round of simulation with counter-examples.]
Description []
SideEffects []
SeeAlso []
@ -364,14 +364,14 @@ p->timeSimSat += clock() - clk;
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepDyn( Ssw_Man_t * p )
{
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i, f;
@ -414,15 +414,15 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
else if ( Aig_ObjIsNode(pObj) )
{
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
}
// check if it is time to recycle the solver
if ( p->pMSat->pSat == NULL ||
(p->pPars->nSatVarMax2 &&
p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
if ( p->pMSat->pSat == NULL ||
(p->pPars->nSatVarMax2 &&
p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
p->nRecycleCalls > p->pPars->nRecycleCalls2) )
{
// resimulate
@ -435,7 +435,7 @@ p->timeReduce += clock() - clk;
Ssw_ManSweepResimulateDyn( p, f );
p->iNodeStart = i+1;
}
// printf( "Recycling SAT solver with %d vars and %d calls.\n",
// Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n",
// p->pMSat->nSatVars, p->nRecycleCalls );
// Aig_ManCleanMarkAB( p->pAig );
Aig_ManCleanMarkAB( p->pFrames );
@ -489,4 +489,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END

47
src/proof/ssw/sswFilter.c
View File

@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
{
{
Aig_Obj_t * pObj, * pObjLi;
int f, i, RetValue1, RetValue2;
assert( nFrames > 0 );
@ -87,14 +87,14 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
{
{
Aig_Obj_t * pObj, * pObjLi;
int f, i;
assert( nFrames > 0 );
@ -129,14 +129,14 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
{
{
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
// assign register outputs
@ -164,7 +164,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( p->pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
// printf( "The counter-example does not refine the output.\n" );
// Abc_Print( 1, "The counter-example does not refine the output.\n" );
// record the new pattern
Saig_ManForEachLo( p->pAig, pObj, i )
if ( pObj->fMarkB ^ Abc_InfoHasBit(p->pPatWords, Saig_ManPiNum(p->pAig) + i) )
@ -183,7 +183,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
***********************************************************************/
int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
{
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
// get representative of this class
@ -199,7 +199,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return 0;
return 0;
// call equivalence checking
if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@ -222,7 +222,7 @@ int Ssw_ManSweepNodeFilter( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
printf( "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" );
Abc_Print( 1, "Ssw_ManSweepNodeFilter(): Failed to refine representative.\n" );
}
return 0;
}
@ -287,15 +287,15 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
if ( Abc_InfoHasBit( p->pPatWords, Saig_ManPiNum(p->pAig) + i ) )
{
Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst1(p->pFrames) );
//printf( "1" );
//Abc_Print( 1, "1" );
}
else
{
Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
//printf( "0" );
//Abc_Print( 1, "0" );
}
}
//printf( "\n" );
//Abc_Print( 1, "\n" );
// sweep internal nodes
for ( f = 0; f < p->pPars->nFramesK; f++ )
@ -332,20 +332,20 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
// printout
if ( p->pPars->fVerbose )
{
printf( "Frame %4d : ", f );
Abc_Print( 1, "Frame %4d : ", f );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
if ( i < Vec_PtrSize(p->pAig->vObjs) )
{
if ( p->pPars->fVerbose )
printf( "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit );
Abc_Print( 1, "Exceeded the resource limits (%d conflicts). Quitting...\n", p->pPars->nBTLimit );
break;
}
}
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
{
if ( p->pPars->fVerbose )
printf( "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK );
Abc_Print( 1, "Exceeded the time frame limit (%d time frames). Quitting...\n", p->pPars->nFramesK );
break;
}
// check timeout
@ -371,9 +371,9 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
Synopsis [Filter equivalence classes of nodes.]
Description [Unrolls at most nFramesMax frames. Works with nConfMax
Description [Unrolls at most nFramesMax frames. Works with nConfMax
conflicts until the first undefined SAT call. Verbose prints the message.]
SideEffects []
SeeAlso []
@ -415,18 +415,18 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
for ( r = 0; r < nRounds; r++ )
{
if ( p->pPars->fVerbose )
printf( "Round %3d:\n", r );
Abc_Print( 1, "Round %3d:\n", r );
// start filtering equivalence classes
Ssw_ManRefineByFilterSim( p, p->pPars->nFramesK );
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
printf( "All equivalences are refined away.\n" );
Abc_Print( 1, "All equivalences are refined away.\n" );
break;
}
// printout
if ( p->pPars->fVerbose )
{
printf( "Initial : " );
Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
p->pMSat = Ssw_SatStart( 0 );
@ -447,7 +447,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
// check timeout
if ( TimeLimit && clock() > nTimeToStop )
{
printf( "Reached timeout (%d seconds).\n", TimeLimit );
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeLimit );
break;
}
}
@ -471,7 +471,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
***********************************************************************/
void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRounds, int TimeLimit, int TimeLimit2, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
{
Aig_Man_t * pAig;
pAig = Gia_ManToAigSimple( p );
if ( p->pReprs != NULL )
@ -491,4 +491,3 @@ void Ssw_SignalFilterGia( Gia_Man_t * p, int nFramesMax, int nConfMax, int nRoun
ABC_NAMESPACE_IMPL_END

43
src/proof/ssw/sswIslands.c
View File

@ -104,7 +104,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
continue;
pObj1 = (Aig_Obj_t *)pObj0->pData;
if ( !Saig_ObjIsLo(p1, pObj1) )
printf( "Mismatch between LO pairs.\n" );
Abc_Print( 1, "Mismatch between LO pairs.\n" );
}
Saig_ManForEachLo( p1, pObj1, i )
{
@ -112,7 +112,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
continue;
pObj0 = (Aig_Obj_t *)pObj1->pData;
if ( !Saig_ObjIsLo(p0, pObj0) )
printf( "Mismatch between LO pairs.\n" );
Abc_Print( 1, "Mismatch between LO pairs.\n" );
}
}
@ -164,7 +164,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
Vec_PtrPush( vNodes, pNext );
}
}
Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
{
if ( Saig_ObjIsPo(p, pNext) )
continue;
@ -184,7 +184,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
Synopsis [Establishes relationship between nodes using pairing.]
Description []
SideEffects []
SeeAlso []
@ -228,9 +228,9 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
if ( fVerbose )
{
int nUnmached = Ssw_MatchingCountUnmached(p0);
printf( "Extending islands by %d steps:\n", nDist );
printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
for ( d = 0; d < nDist; d++ )
@ -262,8 +262,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
if ( fVerbose )
{
int nUnmached = Ssw_MatchingCountUnmached(p0);
printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
}
}
@ -323,7 +323,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Derives matching for all pairs.]
Description [Modifies both AIGs.]
SideEffects []
SeeAlso []
@ -361,7 +361,7 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
Synopsis [Transfers the result of matching to miter.]
Description [The array of pairs should be complete.]
SideEffects []
SeeAlso []
@ -410,7 +410,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
Synopsis [Solves SEC using structural similarity.]
Description [Modifies both p0 and p1 by adding extra logic.]
SideEffects []
SeeAlso []
@ -418,7 +418,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
***********************************************************************/
Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
Ssw_Man_t * p;
Vec_Int_t * vPairsAll, * vPairsMiter;
Aig_Man_t * pMiter, * pAigNew;
// derive full matching
@ -446,10 +446,10 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
Aig_ManStop( pSRed );
printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
}
else
printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
}
p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
@ -489,11 +489,11 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
// report the result of verification
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with a counter-example. " );
Abc_Print( 1, "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pAigRes );
@ -545,7 +545,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
Aig_Man_t * pPart0, * pPart1;
int RetValue;
if ( pPars->fVerbose )
printf( "Performing sequential verification using structural similarity.\n" );
Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
// consider the case when a miter is given
if ( p1 == NULL )
{
@ -556,7 +556,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
// demiter the miter
if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
{
printf( "Demitering has failed.\n" );
Abc_Print( 1, "Demitering has failed.\n" );
return -1;
}
}
@ -573,7 +573,7 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
{
// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
// Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
}
}
assert( Aig_ManRegNum(pPart0) > 0 );
@ -596,4 +596,3 @@ int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END

25
src/proof/ssw/sswLcorr.c
View File

@ -69,7 +69,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
Synopsis [Performs one round of simulation with counter-examples.]
Description []
SideEffects []
SeeAlso []
@ -99,7 +99,7 @@ p->timeSimSat += clock() - clk;
Synopsis [Saves one counter-example into internal storage.]
Description []
SideEffects []
SeeAlso []
@ -127,7 +127,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Synopsis [Builds fraiged logic cone of the node.]
Description []
SideEffects []
SeeAlso []
@ -151,7 +151,7 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
Synopsis [Recycles the SAT solver.]
Description []
SideEffects []
SeeAlso []
@ -173,17 +173,17 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
p->nCallsDelta = 0;
clk = clock();
// get the fraiged node
pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
// get the fraiged representative
if ( Aig_ObjIsCi(pObjRepr) )
{
pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
}
else
else
pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
p->timeReduce += clock() - clk;
// if the fraiged nodes are the same, return
@ -200,7 +200,7 @@ p->timeReduce += clock() - clk;
p->fRefined = 1;
}
else
{
{
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalence
{
@ -215,7 +215,7 @@ p->timeReduce += clock() - clk;
return;
}
else // disproved equivalence
{
{
Ssw_SmlAddPattern( p, pObjRepr, pObj );
p->nPatterns++;
p->nCallsSat++;
@ -229,7 +229,7 @@ p->timeReduce += clock() - clk;
Synopsis [Performs one iteration of sweeping latches.]
Description []
SideEffects []
SeeAlso []
@ -301,7 +301,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
if ( p->nPatterns == 32 )
Ssw_ManSweepResimulate( p );
// attempt recycling the SAT solver
if ( p->pPars->nSatVarMax &&
if ( p->pPars->nSatVarMax &&
p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
{
@ -315,7 +315,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
}
// ABC_PRT( "reduce", p->timeReduce );
// Aig_TableProfile( p->pFrames );
// printf( "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
// Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
// resimulate
if ( p->nPatterns > 0 )
Ssw_ManSweepResimulate( p );
@ -335,4 +335,3 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END

37
src/proof/ssw/sswMan.c
View File

@ -50,7 +50,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Aig_ManFanoutStart( pAig );
Aig_ManSetCioIds( pAig );
// create interpolation manager
p = ABC_ALLOC( Ssw_Man_t, 1 );
p = ABC_ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) );
p->pPars = pPars;
p->pAig = pAig;
@ -60,7 +60,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->iOutputLit = -1;
// allocate storage for sim pattern
p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
// other
p->vNewLos = Vec_PtrAlloc( 100 );
p->vNewPos = Vec_IntAlloc( 100 );
@ -75,7 +75,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
Synopsis [Prints stats of the manager.]
Description []
SideEffects []
SeeAlso []
@ -105,17 +105,17 @@ 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",
Abc_Print( 1, "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, Saig_ManConstrNum(p->pAig), 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),
Abc_Print( 1, "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),
0/(p->pPars->nIters+1) );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
Abc_Print( 1, "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
Abc_Print( 1, "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, 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),
Abc_Print( 1, "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;
@ -133,13 +133,13 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
// report the reductions
if ( p->pAig->nConstrs )
{
printf( "Statistics reflecting the use of constraints:\n" );
printf( "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
Abc_Print( 1, "Statistics reflecting the use of constraints:\n" );
Abc_Print( 1, "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal );
printf( "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
Abc_Print( 1, "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) );
}
}
@ -166,7 +166,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
p->pFrames = NULL;
memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->vSimInfo )
if ( p->vSimInfo )
{
Vec_PtrFree( p->vSimInfo );
p->vSimInfo = NULL;
@ -180,7 +180,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
Synopsis [Frees the manager.]
Description []
SideEffects []
SeeAlso []
@ -193,7 +193,7 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
Ssw_ClassesStop( p->ppClasses );
if ( p->pSml )
if ( p->pSml )
Ssw_SmlStop( p->pSml );
if ( p->vDiffPairs )
Vec_IntFree( p->vDiffPairs );
@ -215,4 +215,3 @@ void Ssw_ManStop( Ssw_Man_t * p )
ABC_NAMESPACE_IMPL_END

65
src/proof/ssw/sswPairs.c
View File

@ -80,11 +80,11 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
if ( fVerbose )
{
printf( "Miter has %d outputs. ", Saig_ManPoNum(p) );
printf( "Const0 = %d. ", CountConst0 );
printf( "NonConst0 = %d. ", CountNonConst0 );
printf( "Undecided = %d. ", CountUndecided );
printf( "\n" );
Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) );
Abc_Print( 1, "Const0 = %d. ", CountConst0 );
Abc_Print( 1, "NonConst0 = %d. ", CountNonConst0 );
Abc_Print( 1, "Undecided = %d. ", CountUndecided );
Abc_Print( 1, "\n" );
}
if ( CountNonConst0 )
@ -140,7 +140,7 @@ Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_
Synopsis [Transform pairs into class representation.]
Description []
SideEffects []
SeeAlso []
@ -187,12 +187,12 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
else if ( idReprRepr == -1 && idReprObj >= 0 )
{ // object has a class
assert( idReprObj != idRepr );
if ( idReprObj < idRepr )
if ( idReprObj < idRepr )
{ // add idRepr to the same class
Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr );
pReprs[ idRepr ] = idReprObj;
}
else // if ( idReprObj > idRepr )
else // if ( idReprObj > idRepr )
{ // make idRepr new representative
Vec_IntPushFirst( pvClasses[idReprObj], idRepr );
pvClasses[idRepr] = pvClasses[idReprObj];
@ -243,7 +243,7 @@ Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumM
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -253,7 +253,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
{
int i;
for ( i = 0; i < nObjNumMax; i++ )
if ( pvClasses[i] )
if ( pvClasses[i] )
Vec_IntFree( pvClasses[i] );
ABC_FREE( pvClasses );
}
@ -263,7 +263,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.]
Description []
SideEffects []
SeeAlso []
@ -271,7 +271,7 @@ void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
Ssw_Man_t * p;
Aig_Man_t * pAigNew, * pMiter;
Ssw_Pars_t Pars;
Vec_Int_t * vPairs;
@ -308,7 +308,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.]
Description []
SideEffects []
SeeAlso []
@ -337,16 +337,16 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
continue;
/*
if ( Aig_ObjIsNode(pObj) )
printf( "n " );
Abc_Print( 1, "n " );
else if ( Saig_ObjIsPi(pAig, pObj) )
printf( "pi " );
Abc_Print( 1, "pi " );
else if ( Saig_ObjIsLo(pAig, pObj) )
printf( "lo " );
Abc_Print( 1, "lo " );
*/
Vec_IntPush( vIds1, Aig_ObjId(pObj) );
Vec_IntPush( vIds2, Aig_ObjId(pRepr) );
}
printf( "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
Abc_Print( 1, "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) );
// try the new AIGs
pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars );
Vec_IntFree( vIds1 );
@ -354,11 +354,11 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with the counter-example. " );
Abc_Print( 1, "Verification failed with the counter-example. " );
else
printf( "Verification UNDECIDED. Remaining registers %d (total %d). ",
Abc_Print( 1, "Verification UNDECIDED. Remaining registers %d (total %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@ -384,16 +384,16 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
clock_t clk = clock();
assert( vIds1 != NULL && vIds2 != NULL );
// try the new AIGs
printf( "Performing specialized verification with node pairs.\n" );
Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with a counter-example. " );
Abc_Print( 1, "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@ -418,7 +418,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
int RetValue;
clock_t clk = clock();
// try the new AIGs
printf( "Performing general verification without node pairs.\n" );
Abc_Print( 1, "Performing general verification without node pairs.\n" );
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
Aig_ManCleanup( pMiter );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
@ -426,11 +426,11 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with a counter-example. " );
Abc_Print( 1, "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@ -455,16 +455,16 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
int RetValue;
clock_t clk = clock();
// try the new AIGs
// printf( "Performing general verification without node pairs.\n" );
// Abc_Print( 1, "Performing general verification without node pairs.\n" );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
Abc_Print( 1, "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with a counter-example. " );
Abc_Print( 1, "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
ABC_PRT( "Time", clock() - clk );
// cleanup
@ -478,4 +478,3 @@ int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END

9
src/proof/ssw/sswPart.c
View File

@ -56,7 +56,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
clock_t clk = clock();
if ( pPars->fConstrs )
{
printf( "Cannot use partitioned computation with constraints.\n" );
Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
return NULL;
}
// save parameters
@ -82,14 +82,14 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
if ( fPrintParts )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( Vec_Int_t *, 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",
Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
@ -109,7 +109,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
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",
Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
}
@ -138,4 +138,3 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
ABC_NAMESPACE_IMPL_END

183
src/proof/ssw/sswRarity.c
View File

@ -17,7 +17,7 @@
Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
#include "aig/gia/giaAig.h"
#include "base/main/main.h"
@ -59,19 +59,19 @@ struct Ssw_RarMan_t_
};
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
}
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
}
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
@ -93,7 +93,7 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6
Synopsis [Prepares random number generator.]
Description []
SideEffects []
SeeAlso []
@ -112,7 +112,7 @@ void Ssw_RarManPrepareRandom( int nRandSeed )
Synopsis [Initializes random primary inputs.]
Description []
SideEffects []
SeeAlso []
@ -139,7 +139,7 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
Synopsis [Derives the counter-example.]
Description []
SideEffects []
SeeAlso []
@ -184,13 +184,13 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
// Abc_CexFree( pCex );
// pCex = NULL;
}
else
{
// printf( "Counter-example verification is successful.\n" );
// Abc_Print( 1, "Counter-example verification is successful.\n" );
}
return pCex;
}
@ -209,9 +209,9 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
***********************************************************************/
void transpose32( unsigned A[32] )
{
int j, k;
unsigned t, m = 0x0000FFFF;
for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
int j, k;
unsigned t, m = 0x0000FFFF;
for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 32; k = (k + j + 1) & ~j )
{
@ -220,7 +220,7 @@ void transpose32( unsigned A[32] )
A[k+j] = A[k+j] ^ (t << j);
}
}
}
}
/**Function*************************************************************
@ -235,9 +235,9 @@ void transpose32( unsigned A[32] )
***********************************************************************/
void transpose64( word A[64] )
{
int j, k;
word t, m = 0x00000000FFFFFFFF;
for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
int j, k;
word t, m = 0x00000000FFFFFFFF;
for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 64; k = (k + j + 1) & ~j )
{
@ -246,14 +246,14 @@ void transpose64( word A[64] )
A[k+j] = A[k+j] ^ (t << j);
}
}
}
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
SideEffects []
SeeAlso []
@ -261,10 +261,10 @@ void transpose64( word A[64] )
***********************************************************************/
void transpose64Simple( word A[64], word B[64] )
{
int i, k;
int i, k;
for ( i = 0; i < 64; i++ )
B[i] = 0;
for ( i = 0; i < 64; i++ )
for ( i = 0; i < 64; i++ )
for ( k = 0; k < 64; k++ )
if ( (A[i] >> k) & 1 )
B[k] |= ((word)1 << (63-i));
@ -292,7 +292,7 @@ void TransposeTest()
for ( i = 0; i < 64; i++ )
M[i] = i? (word)0 : ~(word)0;
// for ( i = 0; i < 64; i++ )
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
clk = clock();
for ( i = 0; i < 100001; i++ )
@ -306,14 +306,14 @@ void TransposeTest()
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
printf( "Mismatch\n" );
Abc_Print( 1, "Mismatch\n" );
/*
printf( "\n" );
Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" );
*/
}
@ -357,15 +357,15 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p )
Saig_ManForEachLi( p->pAig, pObj, i )
{
word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); Abc_Print( 1, "\n" );
}
printf( "\n" );
Abc_Print( 1, "\n" );
for ( i = 0; i < p->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
}
printf( "\n" );
Abc_Print( 1, "\n" );
*/
}
@ -423,7 +423,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
@ -446,7 +446,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
@ -470,7 +470,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
@ -479,19 +479,19 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@ -509,7 +509,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
@ -537,7 +537,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
@ -568,7 +568,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
Synopsis [Performs one round of simulation.]
Description []
SideEffects []
SeeAlso []
@ -580,7 +580,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
word * pSim, * pSim0, * pSim1;
word Flip, Flip0, Flip1;
int w, i;
// initialize
// initialize
Ssw_RarManInitialize( p, vInit );
Vec_PtrClear( p->vUpdConst );
Vec_PtrClear( p->vUpdClass );
@ -603,7 +603,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// simulate
// simulate
Aig_ManForEachNode( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
@ -657,7 +657,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
}
}
}
}
@ -666,7 +666,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -700,7 +700,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -725,7 +725,7 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
Synopsis [Select best patterns.]
Description []
SideEffects []
SeeAlso []
@ -762,7 +762,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
p->pPatCosts[k] += 1.0/(Value*Value);
}
// print the result
//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
//Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
@ -785,7 +785,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) );
//printf( "Best pattern %5d\n", iPatBest );
//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
@ -804,7 +804,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
***********************************************************************/
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
@ -833,15 +833,15 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
// printf( "The counter-example does not refine the output.\n" );
// Abc_Print( 1, "The counter-example does not refine the output.\n" );
// record the new pattern
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
//printf( "%d", pObj->fMarkB );
//Abc_Print( 1, "%d", pObj->fMarkB );
Vec_IntPush( vInit, pObj->fMarkB );
}
//printf( "\n" );
//Abc_Print( 1, "\n" );
Aig_ManCleanMarkB( pAig );
return vInit;
}
@ -872,7 +872,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 );
pAig->pSeqModel->iPo = i;
if ( fVerbose )
printf( "Output %d is trivally SAT in frame 0. \n", i );
Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i );
return 1;
}
}
@ -911,7 +911,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
return 0;
if ( fVerbose )
printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
@ -929,7 +929,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
// if ( pNewAig->pSeqModel != NULL )
// printf( "BMC has found a counter-example in frame %d.\n", iFrameFail );
// Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
Aig_ManStop( pNewAig );
}
// simulate
@ -938,12 +938,12 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( fVerbose ) printf( "\n" );
// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( fVerbose ) Abc_Print( 1, "\n" );
// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nSavedSeed );
ABC_FREE( pAig->pSeqModel );
if ( fVerbose )
printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
@ -954,9 +954,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
printf( "Reached timeout (%d sec).\n", TimeOut );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish;
}
}
@ -977,16 +977,16 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// printout
if ( fVerbose )
{
// printf( "Round %3d: ", r );
// Abc_Print( 1, "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." );
Abc_Print( 1, "." );
}
}
finish:
if ( r == nRounds && f == nFrames )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@ -1048,7 +1048,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
return 0;
if ( fVerbose )
printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
@ -1060,7 +1060,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( pCex )
{
p->vInits = Ssw_RarFindStartingState( pAig, pCex );
printf( "Beginning simulation from the state derived using the counter-example.\n" );
Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
}
else
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
@ -1079,7 +1079,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// print the stats
if ( fVerbose )
{
printf( "Initial : " );
Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
@ -1088,7 +1088,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// start filtering equivalence classes
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
printf( "All equivalences are refined away.\n" );
Abc_Print( 1, "All equivalences are refined away.\n" );
break;
}
// simulate
@ -1097,11 +1097,11 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( !fVerbose )
printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
// printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( !fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( fVerbose )
printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
Ssw_RarManPrepareRandom( nSavedSeed );
Abc_CexFree( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 );
@ -1114,9 +1114,9 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
printf( "Reached timeout (%d sec).\n", TimeOut );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish;
}
}
@ -1137,21 +1137,21 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
// printout
if ( fVerbose )
{
printf( "Round %3d: ", r );
Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
else
{
printf( "." );
Abc_Print( 1, "." );
}
}
finish:
// report
if ( r == nRounds && f == nFrames )
{
if ( !fVerbose )
printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
printf( "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
if ( !fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@ -1171,7 +1171,7 @@ finish:
***********************************************************************/
int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
@ -1197,4 +1197,3 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
ABC_NAMESPACE_IMPL_END

63
src/proof/ssw/sswRarity2.c
View File

@ -50,19 +50,19 @@ struct Ssw_RarMan_t_
};
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
}
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
}
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
@ -78,7 +78,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -109,7 +109,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -148,7 +148,7 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
Saig_ManForEachLi( p->pAig, pObj, i )
{
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" );
Extra_PrintBinary( stdout, pData, 32 ); Abc_Print( 1, "\n" );
}
*/
for ( k = 0; k < p->nWords * 32; k++ )
@ -168,8 +168,8 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
for ( i = 0; i < p->nGroups; i++ )
{
for ( k = 0; k < (1 << p->nBinSize); k++ )
printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
printf( "\n" );
Abc_Print( 1, "%d ", Ssw_RarGetBinPat(p, i, k) );
Abc_Print( 1, "\n" );
}
*/
}
@ -212,7 +212,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
p->pPatCosts[k] += 1.0/(Value*Value);
}
// print the result
// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
// Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
@ -237,7 +237,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Vec_IntPush( vInits, Abc_InfoHasBit(pData, iPatBest) );
}
//printf( "Best pattern %5d\n", iPatBest );
//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
}
@ -255,7 +255,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
***********************************************************************/
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
@ -284,7 +284,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
// printf( "The counter-example does not refine the output.\n" );
// Abc_Print( 1, "The counter-example does not refine the output.\n" );
// record the new pattern
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
@ -318,7 +318,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
if ( fVerbose )
printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
Abc_Print( 1, "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
@ -336,8 +336,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
@ -348,22 +348,22 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// printout
if ( fVerbose )
{
// printf( "Round %3d: ", r );
// Abc_Print( 1, "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." );
Abc_Print( 1, "." );
}
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@ -397,7 +397,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
if ( fVerbose )
printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
Abc_Print( 1, "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
@ -427,7 +427,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// print the stats
if ( fVerbose )
{
printf( "Initial : " );
Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
@ -436,15 +436,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// start filtering equivalence classes
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
printf( "All equivalences are refined away.\n" );
Abc_Print( 1, "All equivalences are refined away.\n" );
break;
}
// simulate
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
@ -454,7 +454,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// printout
if ( fVerbose )
{
printf( "Round %3d: ", r );
Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// get initialization patterns
@ -464,14 +464,14 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// check timeout
if ( TimeOut && clock() > nTimeToStop )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
if ( fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_Print( 1, "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
@ -491,7 +491,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
***********************************************************************/
int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
@ -516,4 +516,3 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
ABC_NAMESPACE_IMPL_END

45
src/proof/ssw/sswSemi.c
View File

@ -67,7 +67,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
Aig_Obj_t * pObj;
int i;
// create interpolation manager
p = ABC_ALLOC( Ssw_Sem_t, 1 );
p = ABC_ALLOC( Ssw_Sem_t, 1 );
memset( p, 0, sizeof(Ssw_Sem_t) );
p->nConfMaxStart = nConfMax;
p->nConfMax = nConfMax;
@ -101,7 +101,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -120,7 +120,7 @@ void Ssw_SemManStop( Ssw_Sem_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -141,7 +141,7 @@ int Ssw_SemCheckTargets( Ssw_Sem_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
@ -168,7 +168,7 @@ void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
@ -212,7 +212,7 @@ clk = clock();
{
fFirst = 1;
pBmc->nConfMax *= 10;
}
}
}
if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
{
@ -236,7 +236,7 @@ clk = clock();
Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
}
//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
//Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
}
if ( fFirst )
pBmc->nConfMax /= 10;
@ -272,10 +272,10 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
}
if ( fVerbose )
{
printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
}
}
RetValue = 0;
for ( Iter = 0; Iter < p->nPatterns; Iter++ )
{
@ -284,16 +284,16 @@ clk = clock();
Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
if ( fVerbose )
{
printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
p->pMan->nSatFailsReal? "f" : " " );
ABC_PRT( "T", clock() - clk );
}
}
Ssw_ManCleanup( p->pMan );
if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
{
printf( "Target is hit!!!\n" );
Abc_Print( 1, "Target is hit!!!\n" );
RetValue = 1;
}
if ( p->nPatterns >= p->nPatternsAlloc )
@ -304,14 +304,14 @@ clk = clock();
pMan->nStrangers = 0;
pMan->nSatCalls = 0;
pMan->nSatProof = 0;
pMan->nSatFailsReal = 0;
pMan->nSatFailsReal = 0;
pMan->nSatCallsUnsat = 0;
pMan->nSatCallsSat = 0;
pMan->timeSimSat = 0;
pMan->timeSat = 0;
pMan->timeSatSat = 0;
pMan->timeSatUnsat = 0;
pMan->timeSatUndec = 0;
pMan->nSatCallsSat = 0;
pMan->timeSimSat = 0;
pMan->timeSat = 0;
pMan->timeSatSat = 0;
pMan->timeSatUnsat = 0;
pMan->timeSatUndec = 0;
return RetValue;
}
@ -321,4 +321,3 @@ clk = clock();
ABC_NAMESPACE_IMPL_END

139
src/proof/ssw/sswSim.c
View File

@ -62,19 +62,19 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa
***********************************************************************/
unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@ -93,7 +93,7 @@ unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
@ -115,7 +115,7 @@ int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
@ -138,7 +138,7 @@ int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1
Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
Description []
SideEffects []
SeeAlso []
@ -154,7 +154,7 @@ int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if the nodes appear equal.]
Description []
SideEffects []
SeeAlso []
@ -171,7 +171,7 @@ int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Counts the number of 1s in the XOR of simulation data.]
Description []
SideEffects []
SeeAlso []
@ -193,7 +193,7 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
Synopsis [Checks implication.]
Description []
SideEffects []
SeeAlso []
@ -228,7 +228,7 @@ int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
SideEffects []
SeeAlso []
@ -261,7 +261,7 @@ int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
SideEffects []
SeeAlso []
@ -285,7 +285,7 @@ int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
@ -307,7 +307,7 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
@ -324,7 +324,7 @@ int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Counts the number of one's in the patten the object.]
Description []
SideEffects []
SeeAlso []
@ -353,7 +353,7 @@ int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Counts the number of one's in the patten the object.]
Description []
SideEffects []
SeeAlso []
@ -389,7 +389,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
Synopsis [Generated const 0 pattern.]
Description []
SideEffects []
SeeAlso []
@ -405,7 +405,7 @@ void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit )
Synopsis [[Generated const 1 pattern.]
Description []
SideEffects []
SeeAlso []
@ -431,14 +431,14 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
Synopsis [Creates the counter-example from the successful pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
{
{
Aig_Obj_t * pFanin, * pObjPi;
unsigned * pSims;
int i, k, BestPat, * pModel;
@ -461,10 +461,10 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
Aig_ManForEachCi( p->pAig, pObjPi, i )
{
pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
// printf( "%d", pModel[i] );
// Abc_Print( 1, "%d", pModel[i] );
}
pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
// printf( "\n" );
// Abc_Print( 1, "\n" );
return pModel;
}
@ -485,7 +485,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Aig_ManCo( p->pAig, 0 );
assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
Aig_ManForEachCo( p->pAig, pObj, i )
{
if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
@ -504,7 +504,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
@ -529,7 +529,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
@ -551,7 +551,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
@ -566,14 +566,14 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
}
}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
@ -587,14 +587,14 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = fConst1? ~(unsigned)0 : 0;
}
}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
@ -607,14 +607,14 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = Word;
}
}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
@ -627,7 +627,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
assert( p->nFrames > 0 );
if ( p->nFrames == 1 )
{
// copy the PI info
// copy the PI info
Aig_ManForEachCi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
// flip one bit
@ -644,7 +644,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
for ( f = 0; f < p->nFrames; f++ )
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
// copy the latch info
// copy the latch info
k = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
@ -665,7 +665,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
@ -697,7 +697,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
@ -763,7 +763,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
@ -794,7 +794,7 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
@ -828,7 +828,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
@ -857,7 +857,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
@ -886,7 +886,7 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
@ -919,7 +919,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
@ -946,7 +946,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
@ -971,7 +971,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p )
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
@ -996,7 +996,7 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
@ -1035,7 +1035,7 @@ p->nSimRounds++;
Synopsis [Converts simulation information to be not normallized.]
Description []
SideEffects []
SeeAlso []
@ -1067,7 +1067,7 @@ void Ssw_SmlUnnormalize( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
@ -1108,7 +1108,7 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
@ -1139,7 +1139,7 @@ p->nSimRounds++;
Synopsis [Allocates simulation manager.]
Description []
SideEffects []
SeeAlso []
@ -1164,7 +1164,7 @@ Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
Synopsis [Allocates simulation manager.]
Description []
SideEffects []
SeeAlso []
@ -1180,7 +1180,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p )
Synopsis [Get simulation data.]
Description []
SideEffects []
SeeAlso []
@ -1202,7 +1202,7 @@ Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p )
Synopsis [Deallocates simulation manager.]
Description []
SideEffects []
SeeAlso []
@ -1219,7 +1219,7 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
Synopsis [Performs simulation of the uninitialized circuit.]
Description []
SideEffects []
SeeAlso []
@ -1239,7 +1239,7 @@ Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
Synopsis [Performs simulation of the initialized circuit.]
Description []
SideEffects []
SeeAlso []
@ -1260,7 +1260,7 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
Synopsis [Performs next round of sequential simulation.]
Description []
SideEffects []
SeeAlso []
@ -1279,7 +1279,7 @@ void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
Synopsis [Returns the number of frames simulated in the manager.]
Description []
SideEffects []
SeeAlso []
@ -1295,7 +1295,7 @@ int Ssw_SmlNumFrames( Ssw_Sml_t * p )
Synopsis [Returns the total number of simulation words.]
Description []
SideEffects []
SeeAlso []
@ -1312,7 +1312,7 @@ int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p )
Description [The simulation info is normalized unless procedure
Ssw_SmlUnnormalize() is called in advance.]
SideEffects []
SeeAlso []
@ -1329,7 +1329,7 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Creates sequential counter-example from the simulation info.]
Description []
SideEffects []
SeeAlso []
@ -1391,7 +1391,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
@ -1404,4 +1404,3 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
ABC_NAMESPACE_IMPL_END

11
src/proof/ssw/sswSimSat.c
View File

@ -62,17 +62,17 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
// make sure refinement happened
if ( Aig_ObjIsConst1(pRepr) )
if ( Aig_ObjIsConst1(pRepr) )
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
}
p->timeSimSat += clock() - clk;
@ -105,13 +105,13 @@ void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr,
{
assert( RetValue1 );
if ( RetValue1 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
@ -122,4 +122,3 @@ p->timeSimSat += clock() - clk;
ABC_NAMESPACE_IMPL_END

23
src/proof/ssw/sswSweep.c
View File

@ -98,7 +98,7 @@ void Ssw_CheckConstraints( Ssw_Man_t * p )
Counter++;
}
}
printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
Abc_Print( 1, "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
}
/**Function*************************************************************
@ -148,7 +148,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
Synopsis [Saves one counter-example into internal storage.]
Description []
SideEffects []
SeeAlso []
@ -178,14 +178,14 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
{
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
clock_t clk;
@ -202,7 +202,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_
assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return 0;
return 0;
// add constraints on demand
if ( !fBmc && p->pPars->fDynamic )
{
@ -248,7 +248,7 @@ p->timeMarkCones += clock() - clk;
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
{
printf( "Ssw_ManSweepNode(): Failed to refine representative.\n" );
Abc_Print( 1, "Ssw_ManSweepNode(): Failed to refine representative.\n" );
}
return 1;
}
@ -299,7 +299,7 @@ clk = clock();
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
break;
// transfer latch input to the latch outputs
// transfer latch input to the latch outputs
Aig_ManForEachCo( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
// build logic cones for register outputs
@ -340,14 +340,14 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
pFile = fopen( pBuffer, "w" );
if ( pFile == NULL )
{
printf( "Cannot open file %s for writing.\n", pBuffer );
Abc_Print( 1, "Cannot open file %s for writing.\n", pBuffer );
return;
}
fclose( pFile );
pNew = Saig_ManCreateEquivMiter( p, vPairs );
Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
Aig_ManStop( pNew );
printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
Abc_Print( 1, "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
}
@ -363,7 +363,7 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p )
{
{
static int Counter;
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
@ -412,7 +412,7 @@ p->timeReduce += clock() - clk;
if ( Saig_ObjIsLo(p->pAig, pObj) )
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
else if ( Aig_ObjIsNode(pObj) )
{
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
@ -435,4 +435,3 @@ p->timeReduce += clock() - clk;
ABC_NAMESPACE_IMPL_END

15
src/proof/ssw/sswUnique.c
View File

@ -61,7 +61,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
// Vec_IntPush( p->vDiffPairs, 1 );
else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
Vec_IntPush( p->vDiffPairs, 1 );
else
else
{
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
Vec_IntPush( p->vDiffPairs, RetValue!=1 );
@ -72,7 +72,7 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
Counter = 0;
Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
Counter += RetValue;
// printf( "The number of different register pairs = %d.\n", Counter );
// Abc_Print( 1, "The number of different register pairs = %d.\n", Counter );
}
@ -96,7 +96,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
// compute the first support in terms of LOs
ppObjs[0] = pRepr;
ppObjs[0] = pRepr;
ppObjs[1] = pObj;
Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
// keep only LOs
@ -116,7 +116,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
Vec_PtrShrink( p->vCommon, k );
if ( fVerbose )
printf( "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
Abc_Print( 1, "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
fFeasible? "yes": "no " );
@ -129,10 +129,10 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
if ( Value0 != Value1 )
RetValue = 0;
if ( fVerbose )
printf( "%d", Value0 ^ Value1 );
Abc_Print( 1, "%d", Value0 ^ Value1 );
}
if ( fVerbose )
printf( "\n" );
Abc_Print( 1, "\n" );
return RetValue && fFeasible;
}
@ -166,7 +166,7 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
}
if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
{
// printf( "Skipped\n" );
// Abc_Print( 1, "Skipped\n" );
return 0;
}
// create CNF
@ -194,4 +194,3 @@ int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int
ABC_NAMESPACE_IMPL_END