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

Version abc81025

This commit is contained in:
Alan Mishchenko 2008-10-25 08:01:00 -07:00
parent 2418d9b08d
commit d2b735f794
24 changed files with 1388 additions and 1536 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abc.dsp
View File

@ -3286,6 +3286,10 @@ SOURCE=.\src\aig\saig\saigBmc.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigBmc2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigCone.c
# End Source File
# Begin Source File
@ -3482,6 +3486,10 @@ SOURCE=.\src\aig\ssw\sswInt.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswIslands.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswLcorr.c
# End Source File
# Begin Source File

4
src/aig/fra/fraCec.c
View File

@ -175,7 +175,11 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
RetValue = Fra_FraigMiterStatus( pAig );
// assert( RetValue == -1 );
if ( RetValue >= 0 )
{
pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) );
memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
return RetValue;
}
// if SAT only, solve without iteration
clk = clock();

4
src/aig/ntl/ntl.h
View File

@ -139,6 +139,7 @@ struct Ntl_Obj_t_
union { // clock / other data
Ntl_Net_t * pClock; // clock (for registers)
void * pTemp; // other data
int iTemp; // other data
};
Ntl_Net_t * pFanio[0]; // fanins/fanouts
};
@ -149,8 +150,8 @@ struct Ntl_Net_t_
void * pCopy; // the copy of this object
union {
void * pCopy2; // the copy of this object
int iTemp; // other data
float dTemp; // other data
int iTemp; // other data
};
Ntl_Obj_t * pDriver; // driver of the net
char nVisits; // the number of times the net is visited
@ -352,6 +353,7 @@ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
/*=== ntlTable.c ==========================================================*/
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern ABC_DLL void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p );
extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber );
extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );

1
src/aig/ntl/ntlEc.c
View File

@ -351,6 +351,7 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
pAig1 = Ntl_ManCollapse( pMan1, 1 );
pAig2 = Ntl_ManCollapse( pMan2, 1 );
pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 );
Aig_ManCleanup( pAig );
Aig_ManStop( pAig1 );
Aig_ManStop( pAig2 );
// cleanup

2
src/aig/ntl/ntlReadBlif.c
View File

@ -745,6 +745,7 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
return 0;
// parse the delay info
Ntl_ModelSetPioNumbers( pMod->pNtk );
Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
return 0;
@ -954,6 +955,7 @@ static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine )
{
pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
pObj = Ntl_ModelCreatePo( p->pNtk, pNet );
pNet->pCopy = pObj;
}
return 1;
}

1261
src/aig/ntl/ntlReadBlif_old.c
View File

File diff suppressed because it is too large Load Diff

77
src/aig/ntl/ntlTable.c
View File

@ -178,6 +178,27 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
return pEnt;
}
/**Function*************************************************************
Synopsis [Assigns numbers to PIs and POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p )
{
Ntl_Obj_t * pObj;
int i;
Ntl_ModelForEachPi( p, pObj, i )
pObj->iTemp = i;
Ntl_ModelForEachPo( p, pObj, i )
pObj->iTemp = i;
}
/**Function*************************************************************
Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).]
@ -189,7 +210,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
SeeAlso []
***********************************************************************/
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
@ -241,6 +262,60 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pNam
return 0;
}
/**Function*************************************************************
Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pTerm;
*pNumber = -1;
pNet = Ntl_ModelFindNet( p, pName );
if ( pNet == NULL )
return 0;
if ( fPiOnly )
{
pTerm = pNet->pDriver;
if ( pTerm && Ntl_ObjIsPi(pTerm) )
{
*pNumber = pTerm->iTemp;
return -1;
}
return 0;
}
if ( fPoOnly )
{
pTerm = pNet->pCopy;
if ( pTerm && Ntl_ObjIsPo(pTerm) )
{
*pNumber = pTerm->iTemp;
return 1;
}
return 0;
}
pTerm = pNet->pCopy;
if ( pTerm && Ntl_ObjIsPo(pTerm) )
{
*pNumber = pTerm->iTemp;
return 1;
}
pTerm = pNet->pDriver;
if ( pTerm && Ntl_ObjIsPi(pTerm) )
{
*pNumber = pTerm->iTemp;
return -1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Sets the driver of the net.]

2
src/aig/nwk/nwkCheck.c
View File

@ -55,7 +55,7 @@ int Nwk_ManCheck( Nwk_Man_t * p )
Nwk_ManForEachObj( p, pObj, i )
{
Nwk_ObjForEachFanin( pObj, pNext, k )
if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 )
if ( Nwk_ObjFanoutNum(pNext) < 100 && Nwk_ObjFindFanout( pNext, pObj ) == -1 )
printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id );
Nwk_ObjForEachFanout( pObj, pNext, k )
if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )

1
src/aig/saig/module.make
View File

@ -1,5 +1,6 @@
SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigBmc.c \
src/aig/saig/saigBmc2.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \

1
src/aig/saig/saig.h
View File

@ -99,6 +99,7 @@ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, in
extern Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
extern Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames );
extern int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
extern int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
/*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/

642
src/aig/saig/saigBmc.c
View File

@ -26,62 +26,49 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define AIG_VISITED ((Aig_Obj_t *)(PORT_PTRUINT_T)1)
typedef struct Saig_Bmc_t_ Saig_Bmc_t;
struct Saig_Bmc_t_
{
// parameters
int nFramesMax; // the max number of timeframes to consider
int nConfMaxOne; // the max number of conflicts at a target
int nConfMaxAll; // the max number of conflicts for all targets
int nNodesMax; // the max number of nodes to add
int fVerbose; // enables verbose output
// AIG managers
Aig_Man_t * pAig; // the user's AIG manager
Aig_Man_t * pFrm; // Frames manager
Vec_Ptr_t * vVisited; // nodes visited in Frames
// node mapping
int nObjs; // the largest number of an AIG object
Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
// SAT solver
sat_solver * pSat; // SAT solver
Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
int nSatVars; // the number of used SAT variables
Vec_Ptr_t * vTargets; // targets to be solved in this interval
int iFramelast; // last frame
int iOutputLast; // last output
};
static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); }
static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); }
static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); }
static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); }
static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. POs correspond to \
the property outputs in each time-frame.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
assert( Saig_ManRegNum(pAig) > 0 );
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_ManConst0( pFrames );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs for this frame
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
if ( f == nFrames - 1 )
break;
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes that are not counted yet.]
Synopsis [Create manager.]
Description []
@ -90,223 +77,374 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
SeeAlso []
***********************************************************************/
int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
{
if ( !Aig_ObjIsNode(pObj) )
return 0;
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return 0;
Aig_ObjSetTravIdCurrent(p, pObj);
return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) +
Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. POs correspond to
the property outputs in each time-frame.
The unrolling is stopped as soon as the number of nodes in the frames
exceeds the given maximum size.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
int i, f, Counter = 0;
assert( Saig_ManRegNum(pAig) > 0 );
pFrames = Aig_ManStart( nSizeMax );
Aig_ManIncrementTravId( pFrames );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_ManConst0( pFrames );
// add timeframes
Counter = 0;
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs for this frame
Saig_ManForEachPo( pAig, pObj, i )
{
pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
}
if ( Counter >= nSizeMax )
{
Aig_ManCleanup( pFrames );
return pFrames;
}
if ( f == nFrames - 1 )
break;
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Man_t * pFrames, * pAigTemp;
Saig_Bmc_t * p;
Aig_Obj_t * pObj;
int status, clk, Lit, i, RetValue = 1;
// derive the timeframes
clk = clock();
if ( nSizeMax > 0 )
int i, Lit;
assert( Aig_ManRegNum(pAig) > 0 );
p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
memset( p, 0, sizeof(Saig_Bmc_t) );
// set parameters
p->nFramesMax = 1000000;
p->nConfMaxOne = nConfMaxOne;
p->nConfMaxAll = nConfMaxAll;
p->nNodesMax = nNodesMax;
p->fVerbose = fVerbose;
p->pAig = pAig;
p->nObjs = Aig_ManObjNumMax(pAig);
// create node and variable mappings
p->vAig2Frm = Vec_PtrAlloc( 0 );
Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL );
p->vObj2Var = Vec_IntAlloc( 0 );
Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
// start the AIG manager and map primary inputs
p->pFrm = Aig_ManStart( 5 * p->nObjs );
Saig_ManForEachLo( pAig, pObj, i )
Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) );
// create SAT solver
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 2000 );
p->nSatVars = 1;
Lit = toLit( p->nSatVars );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
// other data structures
p->vTargets = Vec_PtrAlloc( 0 );
p->vVisited = Vec_PtrAlloc( 0 );
return p;
}
/**Function*************************************************************
Synopsis [Delete manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_BmcManStop( Saig_Bmc_t * p )
{
Aig_ManStop( p->pFrm );
Vec_PtrFree( p->vAig2Frm );
Vec_IntFree( p->vObj2Var );
sat_solver_delete( p->pSat );
Vec_PtrFree( p->vTargets );
Vec_PtrFree( p->vVisited );
free( p );
}
/**Function*************************************************************
Synopsis [Explores the possibility of constructing the output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
pRes = Saig_BmcObjFrame( p, pObj, i );
if ( pRes != NULL )
return pRes;
if ( Saig_ObjIsPi( p->pAig, pObj ) )
pRes = AIG_VISITED;
else if ( Saig_ObjIsLo( p->pAig, pObj ) )
pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
else if ( Aig_ObjIsPo( pObj ) )
{
pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
if ( pRes != AIG_VISITED )
pRes = Saig_BmcObjChild0( p, pObj, i );
}
else
pFrames = Saig_ManFramesBmc( pAig, nFrames );
if ( piFrame )
*piFrame = nFrames;
if ( fVerbose )
else
{
printf( "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) );
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames),
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
if ( p0 != AIG_VISITED )
p0 = Saig_BmcObjChild0( p, pObj, i );
p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
if ( p1 != AIG_VISITED )
p1 = Saig_BmcObjChild1( p, pObj, i );
if ( p0 == Aig_Not(p1) )
pRes = Aig_Not(pConst1);
else if ( Aig_Regular(p0) == pConst1 )
pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1);
else if ( Aig_Regular(p1) == pConst1 )
pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1);
else
pRes = AIG_VISITED;
if ( pRes != pConst1 && pRes != Aig_Not(pConst1) )
pRes = AIG_VISITED;
}
// rewrite the timeframes
if ( fRewrite )
Saig_BmcObjSetFrame( p, pObj, i, pRes );
return pRes;
}
/**Function*************************************************************
Synopsis [Performs the actual construction of the output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
{
Aig_Obj_t * pRes;
pRes = Saig_BmcObjFrame( p, pObj, i );
assert( pRes != NULL );
if ( pRes != AIG_VISITED )
return pRes;
if ( Saig_ObjIsPi( p->pAig, pObj ) )
pRes = Aig_ObjCreatePi(p->pFrm);
else if ( Saig_ObjIsLo( p->pAig, pObj ) )
pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
else if ( Aig_ObjIsPo( pObj ) )
{
clk = clock();
// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
Aig_ManStop( pAigTemp );
if ( fVerbose )
Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
pRes = Saig_BmcObjChild0( p, pObj, i );
}
else
{
Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
}
Saig_BmcObjSetFrame( p, pObj, i, pRes );
return pRes;
}
/**Function*************************************************************
Synopsis [Adds new AIG nodes to the frames.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_BmcInterval( Saig_Bmc_t * p )
{
Aig_Obj_t * pTarget, * pObj;
int i, nNodes = Aig_ManNodeNum( p->pFrm );
Vec_PtrClear( p->vTargets );
for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 )
{
if ( p->iOutputLast == 0 )
{
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) );
Saig_ManForEachPi( p->pAig, pObj, i )
Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) );
}
for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
{
if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax )
return;
Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
Vec_PtrPush( p->vTargets, pTarget );
}
}
// create the SAT solver
clk = clock();
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
}
/**Function*************************************************************
Synopsis [Performs the actual construction of the output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return pObj->pData;
Vec_PtrPush( p->vVisited, pObj );
if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) )
return pObj->pData = Aig_ObjCreatePi(pNew);
Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Creates AIG of the newly added nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i;
pNew = Aig_ManStart( p->nNodesMax );
Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
Vec_PtrClear( p->vVisited );
Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
Aig_ObjCreatePo( pNew, pObjNew );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Derives CNF for the newly added nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
{
Aig_Obj_t * pObj, * pObjNew;
int i, Lits[2], VarNumOld, VarNumNew;
Vec_PtrForEachEntry( p->vVisited, pObj, i )
{
pObjNew = pObj->pData;
pObj->pData = NULL;
VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
if ( VarNumNew == -1 )
continue;
VarNumOld = Saig_BmcSatNum( p, pObj );
if ( VarNumOld == 0 )
{
Saig_BmcSetSatNum( p, pObj, VarNumNew );
continue;
}
// add clauses connecting existing variables
Lits[0] = toLitCond( VarNumOld, 0 );
Lits[1] = toLitCond( VarNumNew, 1 );
if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
assert( 0 );
Lits[0] = toLitCond( VarNumOld, 1 );
Lits[1] = toLitCond( VarNumNew, 0 );
if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
assert( 0 );
}
if ( fVerbose )
{
printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
PRT( "Time", clock() - clk );
fflush( stdout );
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
if ( fVerbose )
{
printf( "The BMC problem is trivially UNSAT\n" );
fflush( stdout );
}
}
else
{
int clkPart = clock();
Aig_ManForEachPo( pFrames, pObj, i )
{
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
if ( fVerbose )
{
printf( "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
clk = clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
{
printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
PRT( "T", clock() - clkPart );
clkPart = clock();
fflush( stdout );
}
if ( status == l_False )
{
/*
Lit = lit_neg( Lit );
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue );
if ( pSat->qtail != pSat->qhead )
{
RetValue = sat_solver_simplify(pSat);
assert( RetValue );
}
*/
}
else if ( status == l_True )
{
extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
free( pModel );
Vec_IntFree( vCiIds );
// if ( piFrame )
// *piFrame = i / Saig_ManPoNum(pAig);
RetValue = 0;
break;
}
else
{
if ( piFrame )
*piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1;
break;
}
}
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Aig_ManStop( pFrames );
return RetValue;
// add CNF to the SAT solver
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
break;
if ( i < pCnf->nClauses )
printf( "SAT solver became UNSAT after adding clauses.\n" );
}
/**Function*************************************************************
Synopsis [Solves targets with the given resource limit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_BmcSolveTargets( Saig_Bmc_t * p )
{
Aig_Obj_t * pObj;
int i, VarNum, Lit, RetValue;
assert( Vec_PtrSize(p->vTargets) > 0 );
Vec_PtrForEachEntry( p->vTargets, pObj, i )
{
if ( p->pSat->stats.conflicts > p->nConfMaxAll )
return l_Undef;
VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue == l_False ) // unsat
continue;
if ( RetValue == l_Undef ) // undecided
return l_Undef;
// generate counter-example
return l_True;
}
return l_False;
}
/**Function*************************************************************
Synopsis [Performs BMC with the given parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
{
Saig_Bmc_t * p;
Aig_Man_t * pNew;
Cnf_Dat_t * pCnf;
int RetValue, clk = clock();
p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose );
while ( 1 )
{
// add new logic slice to frames
Saig_BmcInterval( p );
if ( Vec_PtrSize(p->vTargets) == 0 )
break;
// convert logic slice into new AIG
pNew = Saig_BmcIntervalToAig( p );
// derive CNF for the new AIG
pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) );
Cnf_DataLift( pCnf, p->nSatVars );
p->nSatVars += pCnf->nVars;
// add this CNF to the solver
Saig_BmcLoadCnf( p, pCnf );
Cnf_DataFree( pCnf );
Aig_ManStop( pNew );
// solve the targets
RetValue = Saig_BmcSolveTargets( p );
if ( RetValue != l_False )
break;
}
if ( RetValue == l_True )
printf( "BMC failed for output %d in frame %d. ", p->iOutputLast, p->iFramelast );
else // if ( RetValue == l_False || RetValue == l_Undef )
printf( "BMC completed for %d timeframes. ", p->iFramelast );
PRT( "Time", clock() - clk );
if ( p->iFramelast >= p->nFramesMax )
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
else
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
Saig_BmcManStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

314
src/aig/saig/saigBmc2.c Normal file
View File

@ -0,0 +1,314 @@
/**CFile****************************************************************
FileName [saigBmc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Simple BMC package.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "cnf.h"
#include "satStore.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. POs correspond to \
the property outputs in each time-frame.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
assert( Saig_ManRegNum(pAig) > 0 );
pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_ManConst0( pFrames );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs for this frame
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
if ( f == nFrames - 1 )
break;
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes that are not counted yet.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( !Aig_ObjIsNode(pObj) )
return 0;
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return 0;
Aig_ObjSetTravIdCurrent(p, pObj);
return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) +
Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
}
/**Function*************************************************************
Synopsis [Create timeframes of the manager for BMC.]
Description [The resulting manager is combinational. POs correspond to
the property outputs in each time-frame.
The unrolling is stopped as soon as the number of nodes in the frames
exceeds the given maximum size.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
int i, f, Counter = 0;
assert( Saig_ManRegNum(pAig) > 0 );
pFrames = Aig_ManStart( nSizeMax );
Aig_ManIncrementTravId( pFrames );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
pObj->pData = Aig_ManConst0( pFrames );
// add timeframes
Counter = 0;
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs for this frame
Saig_ManForEachPo( pAig, pObj, i )
{
pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
}
if ( Counter >= nSizeMax )
{
Aig_ManCleanup( pFrames );
return pFrames;
}
if ( f == nFrames - 1 )
break;
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
Aig_ManCleanup( pFrames );
return pFrames;
}
/**Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
{
sat_solver * pSat;
Cnf_Dat_t * pCnf;
Aig_Man_t * pFrames, * pAigTemp;
Aig_Obj_t * pObj;
int status, clk, Lit, i, RetValue = 1;
// derive the timeframes
clk = clock();
if ( nSizeMax > 0 )
{
pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
}
else
pFrames = Saig_ManFramesBmc( pAig, nFrames );
if ( piFrame )
*piFrame = nFrames;
if ( fVerbose )
{
printf( "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) );
printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames),
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
}
// rewrite the timeframes
if ( fRewrite )
{
clk = clock();
// pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
Aig_ManStop( pAigTemp );
if ( fVerbose )
{
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
}
}
// create the SAT solver
clk = clock();
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
}
if ( fVerbose )
{
printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
PRT( "Time", clock() - clk );
fflush( stdout );
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
if ( fVerbose )
{
printf( "The BMC problem is trivially UNSAT\n" );
fflush( stdout );
}
}
else
{
int clkPart = clock();
Aig_ManForEachPo( pFrames, pObj, i )
{
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
if ( fVerbose )
{
printf( "Solving output %2d of frame %3d ... \r",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
}
clk = clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
{
printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
PRT( "T", clock() - clkPart );
clkPart = clock();
fflush( stdout );
}
if ( status == l_False )
{
/*
Lit = lit_neg( Lit );
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue );
if ( pSat->qtail != pSat->qhead )
{
RetValue = sat_solver_simplify(pSat);
assert( RetValue );
}
*/
}
else if ( status == l_True )
{
extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
free( pModel );
Vec_IntFree( vCiIds );
// if ( piFrame )
// *piFrame = i / Saig_ManPoNum(pAig);
RetValue = 0;
break;
}
else
{
if ( piFrame )
*piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1;
break;
}
}
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Aig_ManStop( pFrames );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

159
src/aig/saig/saigMiter.c
View File

@ -49,6 +49,8 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
pNew->pName = Aig_UtilStrsav( "miter" );
Aig_ManCleanData( p0 );
Aig_ManCleanData( p1 );
// map constant nodes
Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
@ -85,7 +87,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// cleanup
Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
Aig_ManCleanup( pNew );
// Aig_ManCleanup( pNew );
return pNew;
}
@ -184,6 +186,9 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
break;
}
// create POs for this frame
Saig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
// save register inputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
@ -213,7 +218,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet )
{
Aig_Man_t * pNew, * pCopy;
Aig_Obj_t * pObj;
@ -250,7 +255,7 @@ Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
{
Aig_Man_t * pNew, * pCopy;
Aig_Obj_t * pObj;
@ -337,6 +342,9 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
Vec_PtrFree( vSet1 );
return 0;
}
if ( Aig_ObjFaninC0(pObj) )
pObj0 = Aig_Not(pObj0);
// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
{
@ -353,13 +361,83 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
// printf( "\n" );
if ( ppAig0 )
{
*ppAig0 = Aig_ManDupNodes( p, vSet0, 0 );
*ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
FREE( (*ppAig0)->pName );
(*ppAig0)->pName = Aig_UtilStrsav( "part0" );
}
if ( ppAig1 )
{
*ppAig1 = Aig_ManDupNodes( p, vSet1, 1 );
*ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
FREE( (*ppAig1)->pName );
(*ppAig1)->pName = Aig_UtilStrsav( "part1" );
}
Vec_PtrFree( vSet0 );
Vec_PtrFree( vSet1 );
return 1;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG to have constant-0 initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
{
Vec_Ptr_t * vSet0, * vSet1;
Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
int i, Counter = 0;
assert( Saig_ManRegNum(p) % 2 == 0 );
vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
Saig_ManForEachPo( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
if ( Aig_ObjIsConst1( pFanin ) )
{
if ( !Aig_ObjFaninC0(pObj) )
printf( "The output number %d of the miter is constant 1.\n", i );
Counter++;
continue;
}
if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
{
printf( "The miter cannot be demitered.\n" );
Vec_PtrFree( vSet0 );
Vec_PtrFree( vSet1 );
return 0;
}
if ( Aig_ObjFaninC0(pObj) )
pObj0 = Aig_Not(pObj0);
// printf( "%d %d ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
{
Vec_PtrPush( vSet0, pObj0 );
Vec_PtrPush( vSet1, pObj1 );
}
else
{
Vec_PtrPush( vSet0, pObj1 );
Vec_PtrPush( vSet1, pObj0 );
}
}
// printf( "Miter has %d constant outputs.\n", Counter );
// printf( "\n" );
if ( ppAig0 )
{
*ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
FREE( (*ppAig0)->pName );
(*ppAig0)->pName = Aig_UtilStrsav( "part0" );
}
if ( ppAig1 )
{
*ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
FREE( (*ppAig1)->pName );
(*ppAig1)->pName = Aig_UtilStrsav( "part1" );
}
@ -525,14 +603,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
if ( ppAig0 )
{
assert( 0 );
*ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); // not ready
*ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
FREE( (*ppAig0)->pName );
(*ppAig0)->pName = Aig_UtilStrsav( "part0" );
}
if ( ppAig1 )
{
assert( 0 );
*ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); // not ready
*ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
FREE( (*ppAig1)->pName );
(*ppAig1)->pName = Aig_UtilStrsav( "part1" );
}
@ -566,6 +644,42 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
return pMiter;
}
/**Function*************************************************************
Synopsis [Resimulates counter-example and returns the failed output number.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs )
{
Aig_Obj_t * pObj;
int i, RetValue = -1;
*pnOutputs = 0;
Aig_ManConst1(p)->fMarkA = 1;
Aig_ManForEachPi( p, pObj, i )
pObj->fMarkA = pModel[i];
Aig_ManForEachNode( p, pObj, i )
pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) &
( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) );
Aig_ManForEachPo( p, pObj, i )
pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
Aig_ManForEachPo( p, pObj, i )
if ( pObj->fMarkA )
{
if ( RetValue == -1 )
RetValue = i;
(*pnOutputs)++;
}
Aig_ManCleanMarkA(p);
return RetValue;
}
/**Function*************************************************************
Synopsis [Reduces SEC to CEC for the special case of seq synthesis.]
@ -578,12 +692,16 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
SeeAlso []
***********************************************************************/
int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose )
{
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
int nFrames = 2; // modify to enable comparison over any number of frames
int iOut, nOuts;
Aig_Man_t * pMiterCec;
int RetValue, clkTotal = clock();
Aig_ManPrintStats( pPart0 );
Aig_ManPrintStats( pPart1 );
// Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL );
// Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL );
// assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) );
if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
{
@ -605,7 +723,6 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
// transfer model if given
// if ( pNtk2 == NULL )
// pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL;
Aig_ManStop( pMiterCec );
// report the miter
if ( RetValue == 1 )
{
@ -616,6 +733,24 @@ PRT( "Time", clock() - clkTotal );
{
printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
if ( pMiterCec->pData == NULL )
printf( "Counter-example is not available.\n" );
else
{
iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts );
if ( iOut == -1 )
printf( "Counter-example verification has failed.\n" );
else
{
if ( iOut < Saig_ManPoNum(pPart0) * nFrames )
printf( "Primary output %d has failed in frame %d.\n",
iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) );
else
printf( "Flop input %d has failed in the last frame.\n",
iOut - Saig_ManPoNum(pPart0) * nFrames );
printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts );
}
}
}
else
{
@ -623,6 +758,7 @@ PRT( "Time", clock() - clkTotal );
PRT( "Time", clock() - clkTotal );
}
fflush( stdout );
Aig_ManStop( pMiterCec );
return RetValue;
}
@ -639,6 +775,7 @@ PRT( "Time", clock() - clkTotal );
***********************************************************************/
int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
{
int nFrames = 2; // modify to enable comparison over any number of frames
Aig_Man_t * pPart0, * pPart1;
int RetValue;
if ( fVerbose )
@ -657,7 +794,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
}
RetValue = Ssw_SecSpecial( pPart0, pPart1, fVerbose );
RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
return RetValue;

1
src/aig/saig/saigSynch.c
View File

@ -632,6 +632,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
pAig1z = Saig_ManDupInitZero( pAig1 );
pAig2z = Saig_ManDupInitZero( pAig2 );
pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
Aig_ManCleanup( pMiter );
Aig_ManStop( pAig1z );
Aig_ManStop( pAig2z );

1
src/aig/ssw/module.make
View File

@ -4,6 +4,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswDyn.c \
src/aig/ssw/sswIslands.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \

1
src/aig/ssw/ssw.h
View File

@ -104,6 +104,7 @@ extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );

52
src/aig/ssw/sswClass.c
View File

@ -446,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
Vec_PtrPush( p->vRefined, pObj );
// Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
assert( p->pClassSizes[pRepr->Id] == 0 );
@ -455,7 +455,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
p->nCands1--;
return;
}
Vec_PtrPush( p->vRefined, pRepr );
// Vec_PtrPush( p->vRefined, pRepr );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
assert( p->pId2Class[pRepr->Id][0] == pRepr );
assert( p->pClassSizes[pRepr->Id] >= 2 );
@ -791,6 +791,48 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
return p;
}
/**Function*************************************************************
Synopsis [Creates classes from the temporary representation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
{
Ssw_Cla_t * p;
Aig_Obj_t ** ppClassNew;
Aig_Obj_t * pObj, * pRepr;
int i;
// start the classes
p = Ssw_ClassesStart( pMiter );
// allocate memory for classes
p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
// create classes
for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
{
pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
Aig_ObjSetRepr( pMiter, pObj, pRepr );
// get room for storing the class
ppClassNew = p->pMemClasses + i;
ppClassNew[0] = pRepr;
ppClassNew[1] = pObj;
// create new class
Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
}
// prepare room for new classes
p->pMemClassesFree = NULL;
Ssw_ClassesCheck( p );
// Ssw_ClassesPrint( p, 0 );
return p;
}
/**Function*************************************************************
Synopsis [Iteratively refines the classes after simulation.]
@ -820,8 +862,8 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
// remember that this class is refined
Ssw_ClassForEachNode( p, pReprOld, pObj, i )
Vec_PtrPush( p->vRefined, pObj );
// Ssw_ClassForEachNode( p, pReprOld, pObj, i )
// Vec_PtrPush( p->vRefined, pObj );
// get the new representative
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@ -944,7 +986,7 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
{
Vec_PtrPush( p->vClassNew, pObj );
Vec_PtrPush( p->vRefined, pObj );
// Vec_PtrPush( p->vRefined, pObj );
}
}
// check if there is a new class

1
src/aig/ssw/sswInt.h
View File

@ -205,6 +205,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int n
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );

382
src/aig/ssw/sswIslands.c Normal file
View File

@ -0,0 +1,382 @@
/**CFile****************************************************************
FileName [sswIslands.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Detection of islands of difference.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Aig_ObjChild0Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin0(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_ObjChild1Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates pair of structurally equivalent nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
pObj0->pData = pObj1;
pObj1->pData = pObj0;
Vec_IntPush( vPairs, pObj0->Id );
Vec_IntPush( vPairs, pObj1->Id );
}
/**Function*************************************************************
Synopsis [Detects islands of common logic and returns them as pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose )
{
Vec_Int_t * vPairs;
Aig_Obj_t * pObj0, * pObj1, * pFanin0, * pFanin1;
int i;
assert( Aig_ManRegNum(p0) > 0 );
assert( Aig_ManRegNum(p1) > 0 );
assert( Aig_ManRegNum(p0) >= nCommonFlops );
assert( Aig_ManRegNum(p1) >= nCommonFlops );
assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
Aig_ManCleanData( p0 );
Aig_ManCleanData( p1 );
// start structural equivalence
vPairs = Vec_IntAlloc( 1000 );
Ssw_CreatePair( vPairs, Aig_ManConst1(p0), Aig_ManConst1(p1) );
Saig_ManForEachPi( p0, pObj0, i )
Ssw_CreatePair( vPairs, pObj0, Aig_ManPi(p1, i) );
Saig_ManForEachLo( p0, pObj0, i )
{
if ( i == nCommonFlops )
break;
Ssw_CreatePair( vPairs, pObj0, Saig_ManLo(p1, i) );
}
// find structurally equivalent nodes
Aig_ManForEachNode( p0, pObj0, i )
{
pFanin0 = Aig_ObjChild0Copy2( pObj0 );
pFanin1 = Aig_ObjChild1Copy2( pObj0 );
if ( pFanin0 == NULL || pFanin1 == NULL )
continue;
pObj1 = Aig_TableLookupTwo( p1, pFanin0, pFanin1 );
if ( pObj1 == NULL )
continue;
Ssw_CreatePair( vPairs, pObj0, pObj1 );
}
return vPairs;
}
/**Function*************************************************************
Synopsis [Collects additional Lis and Los.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Vec_Ptr_t * vLos )
{
Aig_Obj_t * pObjLo, * pObjLi;
int i;
Saig_ManForEachLiLo( p, pObjLo, pObjLi, i )
{
if ( i < nCommonFlops )
continue;
Vec_PtrPush( vLis, pObjLi );
Vec_PtrPush( vLos, pObjLo );
}
}
/**Function*************************************************************
Synopsis [Overlays and extends the pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_OverlayIslands( Aig_Man_t * pTo, Aig_Man_t * pFrom, Vec_Ptr_t * vLisFrom, Vec_Ptr_t * vLosFrom, Vec_Int_t * vPairs, int nCommonFlops, int fToGoesFirst )
{
Aig_Obj_t * pObjFrom, * pObjTo, * pFanin0To, * pFanin1To;
int i;
// create additional register outputs of From in To
Vec_PtrForEachEntry( vLosFrom, pObjFrom, i )
{
pObjTo = Aig_ObjCreatePi( pTo );
if( fToGoesFirst )
Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
else
Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
}
// create additional nodes of From in To
Aig_ManForEachNode( pFrom, pObjFrom, i )
{
if ( pObjFrom->pData != NULL )
continue;
pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
pFanin1To = Aig_ObjChild1Copy2( pObjFrom );
assert( pFanin0To != NULL && pFanin1To != NULL );
pObjTo = Aig_And( pTo, pFanin0To, pFanin1To );
if( fToGoesFirst )
Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
else
Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
}
// finally recreate additional register inputs
Vec_PtrForEachEntry( vLisFrom, pObjFrom, i )
{
pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
Aig_ObjCreatePo( pTo, pFanin0To );
}
// update the number of registers
Aig_ManSetRegNum( pTo, Aig_ManRegNum(pTo) + Vec_PtrSize(vLisFrom) );
}
/**Function*************************************************************
Synopsis [Overlays and extends the pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t ** ppMiter, Vec_Int_t * vPairs )
{
Aig_Man_t * pMiter;
Vec_Int_t * vPairsNew;
Aig_Obj_t * pObj0, * pObj1;
int i;
vPairsNew = Vec_IntAlloc( 1000 );
pMiter = Saig_ManCreateMiter( p0, p1, 0 );
for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
{
pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
pObj0 = pObj0->pData;
pObj1 = pObj1->pData;
assert( !Aig_IsComplement(pObj0) );
assert( !Aig_IsComplement(pObj1) );
if ( pObj0 == pObj1 )
continue;
assert( pObj0->Id < pObj1->Id );
Vec_IntPush( vPairsNew, pObj0->Id );
Vec_IntPush( vPairsNew, pObj1->Id );
}
*ppMiter = pMiter;
return vPairsNew;
}
/**Function*************************************************************
Synopsis [Solves SEC using structural similarity.]
Description [Modifies both p0 and p1 by adding extra logic.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
Ssw_Pars_t Pars;
Vec_Int_t * vPairs, * vPairsMiter;
Aig_Man_t * pMiter, * pAigNew;
Vec_Ptr_t * vLis0, * vLos0, * vLis1, * vLos1;
int nNodes, nRegs;
assert( Aig_ManRegNum(p0) > 0 );
assert( Aig_ManRegNum(p1) > 0 );
assert( Aig_ManRegNum(p0) >= nCommonFlops );
assert( Aig_ManRegNum(p1) >= nCommonFlops );
assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
// derive pairs
vPairs = Ssw_DetectIslands( p0, p1, nCommonFlops, fVerbose );
if ( fVerbose )
{
printf( "Original managers:\n" );
Aig_ManPrintStats( p0 );
Aig_ManPrintStats( p1 );
printf( "Detected %d PI pairs, %d LO pairs, and %d node pairs.\n",
Saig_ManPiNum(p0), nCommonFlops, Vec_IntSize(vPairs)/2 - Saig_ManPiNum(p0) - nCommonFlops - 1 );
}
// complete the manager with islands
vLis0 = Vec_PtrAlloc( 100 );
vLos0 = Vec_PtrAlloc( 100 );
vLis1 = Vec_PtrAlloc( 100 );
vLos1 = Vec_PtrAlloc( 100 );
Ssw_CollectExtraLiLo( p0, nCommonFlops, vLis0, vLos0 );
Ssw_CollectExtraLiLo( p1, nCommonFlops, vLis1, vLos1 );
nRegs = Saig_ManRegNum(p0);
nNodes = Aig_ManNodeNum(p0);
Ssw_OverlayIslands( p0, p1, vLis1, vLos1, vPairs, nCommonFlops, 1 );
if ( fVerbose )
printf( "Completed p0 with %d registers and %d nodes.\n",
Saig_ManRegNum(p0) - nRegs, Aig_ManNodeNum(p0) - nNodes );
nRegs = Saig_ManRegNum(p1);
nNodes = Aig_ManNodeNum(p1);
Ssw_OverlayIslands( p1, p0, vLis0, vLos0, vPairs, nCommonFlops, 0 );
if ( fVerbose )
printf( "Completed p1 with %d registers and %d nodes.\n",
Saig_ManRegNum(p1) - nRegs, Aig_ManNodeNum(p1) - nNodes );
if ( fVerbose )
{
printf( "Modified managers:\n" );
Aig_ManPrintStats( p0 );
Aig_ManPrintStats( p1 );
}
Vec_PtrFree( vLis0 );
Vec_PtrFree( vLos0 );
Vec_PtrFree( vLis1 );
Vec_PtrFree( vLos1 );
// create sequential miter
vPairsMiter = Saig_ManMiterWithIslands( p0, p1, &pMiter, vPairs );
Vec_IntFree( vPairs );
// if parameters are not given, create them
if ( pPars == NULL )
Ssw_ManSetDefaultParams( pPars = &Pars );
// start the induction manager
p = Ssw_ManCreate( pMiter, pPars );
// create equivalence classes using these IDs
p->ppClasses = Ssw_ClassesFromIslands( pMiter, vPairsMiter );
p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
// cleanup
Ssw_ManStop( p );
Aig_ManStop( pMiter );
Vec_IntFree( vPairsMiter );
return pAigNew;
}
/**Function*************************************************************
Synopsis [Solves SEC using structural similarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
{
Aig_Man_t * pAigRes;
Aig_Man_t * p0New, * p1New;
int RetValue, clk = clock();
// try the new AIGs
// printf( "Performing verification using structural similarity.\n" );
p0New = Aig_ManDupSimple( p0 );
p1New = Aig_ManDupSimple( p1 );
pAigRes = Ssw_SecWithIslandsInternal( p0New, p1New, nCommonFlops, fVerbose, pPars );
Aig_ManStop( p0New );
Aig_ManStop( p1New );
// report the results
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
else if ( RetValue == 0 )
printf( "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0New)+Aig_ManRegNum(p1New) );
PRT( "Time", clock() - clk );
// cleanup
Aig_ManStop( pAigRes );
return RetValue;
}
/**Function*************************************************************
Synopsis [Solves SEC using structural similarity for the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_SecWithIslandsMiter( Aig_Man_t * pMiter, int nCommonFlops, int fVerbose )
{
Aig_Man_t * pPart0, * pPart1;
int RetValue;
if ( fVerbose )
Aig_ManPrintStats( pMiter );
// demiter the miter
if ( !Saig_ManDemiterSimpleDiff( pMiter, &pPart0, &pPart1 ) )
{
printf( "Demitering has failed.\n" );
return -1;
}
if ( fVerbose )
{
// Aig_ManPrintStats( pPart0 );
// Aig_ManPrintStats( pPart1 );
// 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" );
}
RetValue = Ssw_SecWithIslands( pPart0, pPart1, nCommonFlops, fVerbose, NULL );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/ssw/sswPairs.c
View File

@ -276,6 +276,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
// create sequential miter
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
Aig_ManCleanup( pMiter );
// transfer information to the miter
vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
// create representation of the classes
@ -413,6 +414,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
// try the new AIGs
printf( "Performing general verification without node pairs.\n" );
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
Aig_ManCleanup( pMiter );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
Aig_ManStop( pMiter );
// report the results

6
src/base/abci/abc.c
View File

@ -7936,7 +7936,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
/*
pNtkRes = Abc_NtkDarTestNtk( pNtk );
if ( pNtkRes == NULL )
{
@ -7945,9 +7945,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
// Abc_NtkDarTest( pNtk );
Abc_NtkDarTest( pNtk );
return 0;
usage:

2
src/base/abci/abcMap.c
View File

@ -109,9 +109,9 @@ clk = clock();
// reconstruct the network after mapping
pNtkNew = Abc_NtkFromMap( pMan, pNtk );
Map_ManFree( pMan );
if ( pNtkNew == NULL )
return NULL;
Map_ManFree( pMan );
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );

0
src/map/pcm/module.make Normal file
View File

0
src/map/ply/module.make Normal file
View File