summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigMan.c1
-rw-r--r--src/aig/bbr/bbrCex.c1
-rw-r--r--src/aig/bbr/bbrImage.c38
-rw-r--r--src/aig/cnf/cnf.h2
-rw-r--r--src/aig/cnf/cnfUtil.c44
-rw-r--r--src/aig/gia/gia.h34
-rw-r--r--src/aig/gia/giaAig.c24
-rw-r--r--src/aig/gia/giaAig.h1
-rw-r--r--src/aig/gia/module.make2
-rw-r--r--src/aig/ntl/ntlReadBlif.c12
-rw-r--r--src/aig/saig/saig.h3
-rw-r--r--src/aig/saig/saigAbs.c122
-rw-r--r--src/aig/saig/saigBmc.c251
-rw-r--r--src/aig/saig/saigDup.c121
-rw-r--r--src/aig/saig/saigSimExt.c10
-rw-r--r--src/aig/ssw/sswSim.c2
17 files changed, 552 insertions, 117 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 56e2336a..45b509dc 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -156,6 +156,7 @@ struct Aig_Man_t_
Vec_Int_t * vEquPairs;
Vec_Vec_t * vClockDoms;
Vec_Int_t * vProbs; // probability of node being 1
+ Vec_Int_t * vCiNumsOrig; // original CI names
// timing statistics
int time1;
int time2;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 11d3f3d7..01b29f5f 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -211,6 +211,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
if ( p->vClockDoms) Vec_VecFree( p->vClockDoms );
if ( p->vProbs ) Vec_IntFree( p->vProbs );
+ if ( p->vCiNumsOrig)Vec_IntFree( p->vCiNumsOrig );
ABC_FREE( p->pFastSim );
ABC_FREE( p->pData );
ABC_FREE( p->pSeqModel );
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index 4555570a..947c393c 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -54,6 +54,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
int i, v, RetValue, nPiOffset;
char * pValues;
int clk = clock();
+//printf( "\nDeriving counter-example.\n" );
// allocate room for the counter-example
pCex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index aed302eb..c16a8ff4 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -232,6 +232,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
// clean the partitions
Bbr_DeleteParts_rec( pTree->pRoot );
ABC_FREE( pParts );
+
return pTree;
}
@@ -729,13 +730,26 @@ int Bbr_BuildTreeNode( DdManager * dd,
iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
if ( iVarBest == -1 )
return 0;
-
+/*
+for ( v = 0; v < nVars; v++ )
+{
+ DdNode * bSupp;
+ if ( pVars[v] == NULL )
+ continue;
+ printf( "%3d :", v );
+ printf( "%3d ", pVars[v]->nParts );
+ bSupp = Cudd_Support( dd, pVars[v]->bParts ); Cudd_Ref( bSupp );
+ Bbr_bddPrint( dd, bSupp ); printf( "\n" );
+ Cudd_RecursiveDeref( dd, bSupp );
+}
+*/
pVar = pVars[iVarBest];
// this var cannot appear in one partition only
nSupp = Cudd_SupportSize( dd, pVar->bParts );
assert( nSupp == pVar->nParts );
assert( nSupp != 1 );
+//printf( "var = %d supp = %d\n\n", iVarBest, nSupp );
// if it appears in only two partitions, quantify it
if ( pVar->nParts == 2 )
@@ -773,6 +787,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
pNode1 = pNodes[iNode1];
pNode2 = pNodes[iNode2];
+//printf( "smallest bdds with this var: %d %d\n", iNode1, iNode2 );
/*
// it is not possible that a var appears only in these two
// otherwise, it would have a different cost
@@ -789,6 +804,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
// clean the old nodes
pNodes[iNode1] = pNode;
pNodes[iNode2] = NULL;
+//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 );
// update the variables that appear in pNode[iNode2]
for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
@@ -941,9 +957,29 @@ int Bbr_FindBestVariable( DdManager * dd,
CostBest = 100000000000000.0;
iVarBest = -1;
+
+ // check if there are two-variable partitions
+ for ( v = 0; v < nVars; v++ )
+ if ( pVars[v] && pVars[v]->nParts == 2 )
+ {
+ CostCur = 0;
+ for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+ CostCur += pNodes[bTemp->index]->pPart->nNodes *
+ pNodes[bTemp->index]->pPart->nNodes;
+ if ( CostBest > CostCur )
+ {
+ CostBest = CostCur;
+ iVarBest = v;
+ }
+ }
+ if ( iVarBest >= 0 )
+ return iVarBest;
+
+ // find other partition
for ( v = 0; v < nVars; v++ )
if ( pVars[v] )
{
+ assert( pVars[v]->nParts > 1 );
CostCur = 0;
for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
CostCur += pNodes[bTemp->index]->pPart->nNodes *
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 4343bf9a..f7d1d38c 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -157,6 +157,8 @@ extern void Cnf_ManPostprocess( Cnf_Man_t * p );
/*=== cnfUtil.c ========================================================*/
extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
+extern Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
+extern Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
/*=== cnfWrite.c ========================================================*/
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
index 3738fee5..7da9fb47 100644
--- a/src/aig/cnf/cnfUtil.c
+++ b/src/aig/cnf/cnfUtil.c
@@ -182,6 +182,50 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
return vMapped;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the array of CI IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+{
+ Vec_Int_t * vCiIds;
+ Aig_Obj_t * pObj;
+ int i;
+ vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+ Aig_ManForEachPi( p, pObj, i )
+ Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+ return vCiIds;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of CI IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+{
+ Vec_Int_t * vCoIds;
+ Aig_Obj_t * pObj;
+ int i;
+ vCoIds = Vec_IntAlloc( Aig_ManPoNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
+ return vCoIds;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index f8c1fe91..f023366a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -136,6 +136,7 @@ struct Gia_Man_t_
unsigned char* pSwitching; // switching activity for each object
Gia_Plc_t * pPlacement; // placement of the objects
int * pTravIds; // separate traversal ID representation
+ int nTravIdsAlloc; // the number of trav IDs allocated
Vec_Ptr_t * vNamesIn; // the input names
Vec_Ptr_t * vNamesOut; // the output names
};
@@ -167,7 +168,6 @@ struct Gia_ParFra_t_
};
-
// simulation parameters
typedef struct Gia_ParSim_t_ Gia_ParSim_t;
struct Gia_ParSim_t_
@@ -197,6 +197,7 @@ static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |=
static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
+static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; }
static inline int Gia_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -320,14 +321,29 @@ static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t *
static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); }
static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); }
-static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1; }
-static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) { p->nTravIds++; }
-static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; }
-static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; }
-static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); }
-static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); }
-static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { p->pTravIds[Id] = p->nTravIds; }
-static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { return (p->pTravIds[Id] == p->nTravIds); }
+static inline void Gia_ManResetTravIdArray( Gia_Man_t * p )
+{
+ ABC_FREE( p->pTravIds );
+ p->nTravIdsAlloc = Gia_ManObjNum(p);
+ p->pTravIds = ABC_CALLOC( int, p->nTravIdsAlloc );
+ p->nTravIds = 1;
+}
+static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p )
+{
+ while ( p->nTravIdsAlloc < Gia_ManObjNum(p) )
+ {
+ p->nTravIdsAlloc *= 2;
+ p->pTravIds = ABC_REALLOC( int, p->pTravIds, p->nTravIdsAlloc );
+ memset( p->pTravIds + p->nTravIdsAlloc/2, 0, sizeof(int) * p->nTravIdsAlloc/2 );
+ }
+ p->nTravIds++;
+}
+static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; }
+static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; }
+static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); }
+static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); }
+static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; }
+static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); }
// AIG construction
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 07e74e34..fa9030c5 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -361,6 +361,30 @@ void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
}
}
+/**Function*************************************************************
+
+ Synopsis [Applied DC2 to the GIA manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p )
+{
+ extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
+ Gia_Man_t * pGia;
+ Aig_Man_t * pNew, * pTemp;
+ pNew = Gia_ManToAig( p, 0 );
+ pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 );
+ Aig_ManStop( pTemp );
+ pGia = Gia_ManFromAig( pNew );
+ Aig_ManStop( pNew );
+ return pGia;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 0e29bf06..8cef5c7e 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -52,6 +52,7 @@ extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices );
extern Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta );
extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
+extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p );
#ifdef __cplusplus
}
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 79bfa2fb..0245b0f1 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -1,4 +1,5 @@
SRC += src/aig/gia/gia.c \
+ src/aig/gia/giaAbs.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaCof.c \
@@ -11,6 +12,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaEnable.c \
src/aig/gia/giaEquiv.c \
src/aig/gia/giaEra.c \
+ src/aig/gia/giaEra2.c \
src/aig/gia/giaFanout.c \
src/aig/gia/giaForce.c \
src/aig/gia/giaFrames.c \
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index f94595b8..2e8a8096 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -272,12 +272,12 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
Ioa_ReadMod_t * p;
p = ABC_ALLOC( Ioa_ReadMod_t, 1 );
memset( p, 0, sizeof(Ioa_ReadMod_t) );
- p->vInputs = Vec_PtrAlloc( 8 );
- p->vOutputs = Vec_PtrAlloc( 8 );
- p->vLatches = Vec_PtrAlloc( 8 );
- p->vNames = Vec_PtrAlloc( 8 );
- p->vSubckts = Vec_PtrAlloc( 8 );
- p->vDelays = Vec_PtrAlloc( 8 );
+ p->vInputs = Vec_PtrAlloc( 8 );
+ p->vOutputs = Vec_PtrAlloc( 8 );
+ p->vLatches = Vec_PtrAlloc( 8 );
+ p->vNames = Vec_PtrAlloc( 8 );
+ p->vSubckts = Vec_PtrAlloc( 8 );
+ p->vDelays = Vec_PtrAlloc( 8 );
p->vTimeInputs = Vec_PtrAlloc( 8 );
p->vTimeOutputs = Vec_PtrAlloc( 8 );
return p;
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b77a4292..f72a3074 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
#include "aig.h"
+#include "giaAbs.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -90,7 +91,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose );
+extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 844d6f24..2fac60f5 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -686,6 +686,30 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
/**Function*************************************************************
+ Synopsis [Find the first PI corresponding to the flop.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ assert( pAbs->vCiNumsOrig != NULL );
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) )
+ return i;
+ }
+ return -1;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs proof-based abstraction using BMC of the given depth.]
Description []
@@ -701,9 +725,9 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
- Vec_Int_t * vFlopsNew, * vPiToReg;
- Aig_Obj_t * pObj;
- int i, Entry, iFlop;
+ Vec_Int_t * vFlopsNew;//, * vPiToReg;
+// Aig_Obj_t * pObj;
+ int i, Entry;//, iFlop;
if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
@@ -727,8 +751,8 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
return NULL;
if ( pnUseStart )
*pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame;
-// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
- vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
+// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
+ vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
if ( Vec_IntSize(vFlopsNew) == 0 )
{
printf( "Discovered a true counter-example!\n" );
@@ -739,7 +763,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
if ( fVerbose )
printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) );
// vFlopsNew contains PI number that should be kept in pAbs
-
+/*
// for each additional PI, collect the number of a register it stands for
Vec_IntForEachEntry( vFlops, Entry, i )
{
@@ -773,6 +797,20 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
Vec_IntSort( vFlops, 0 );
Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
assert( Vec_IntEntry(vFlops, i-1) != Entry );
+*/
+ // add to the abstraction
+ Vec_IntForEachEntry( vFlopsNew, Entry, i )
+ {
+ Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
+ assert( Entry >= Saig_ManPiNum(p) );
+ assert( Entry < Aig_ManPiNum(p) );
+ Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
+ }
+ Vec_IntFree( vFlopsNew );
+
+ Vec_IntSort( vFlops, 0 );
+ Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
+ assert( Vec_IntEntry(vFlops, i-1) != Entry );
return Saig_ManAbstraction( p, vFlops );
}
@@ -788,7 +826,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
+Vec_Int_t * Saig_ManProofAbstraction_int( Aig_Man_t * p, Gia_ParAbs_t * pPars )
{
Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf;
@@ -800,10 +838,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
assert( Aig_ManRegNum(p) > 0 );
Aig_ManSetPioNumbers( p );
- if ( fSkipProof )
+ if ( pPars->fSkipProof )
{
// assert( 0 );
- if ( fVerbose )
+ if ( pPars->fVerbose )
printf( "Performing counter-example-based refinement.\n" );
// vFlops = Vec_IntStartNatural( 100 );
// Vec_IntPush( vFlops, 0 );
@@ -811,12 +849,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
}
else
{
- if ( fVerbose )
- printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
- if ( fDynamic )
+ if ( pPars->fVerbose )
+ printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax );
+ if ( pPars->fDynamic )
{
// create CNF for the frames
- vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose );
+ vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose );
// create dynamic solver
pSat = Saig_AbsCreateSolverDyn( p, vFrames );
}
@@ -825,15 +863,15 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
// create CNF for the AIG
pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
// create SAT solver for the unrolled AIG
- pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+ pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax );
}
- if ( fVerbose )
+ if ( pPars->fVerbose )
{
printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses );
ABC_PRT( "Time", clock() - clk2 );
}
// compute UNSAT core
- vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
+ vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose );
sat_solver_delete( pSat );
if ( vCore == NULL )
{
@@ -841,18 +879,18 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
return NULL;
}
// collect registers
- if ( fDynamic )
+ if ( pPars->fDynamic )
{
vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
Saig_AbsFreeCnfs( vFrames );
}
else
{
- vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
+ vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore );
Cnf_DataFree( pCnf );
}
Vec_IntFree( vCore );
- if ( fVerbose )
+ if ( pPars->fVerbose )
{
printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
ABC_PRT( "Time", clock() - clk );
@@ -872,10 +910,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
// create the resulting AIG
pResult = Saig_ManAbstraction( p, vFlops );
- if ( fExtend )
+ if ( pPars->fExtend )
{
int nUseStart = 0;
- if ( !fVerbose )
+ if ( !pPars->fVerbose )
{
printf( "Init : " );
Aig_ManPrintStats( pResult );
@@ -883,13 +921,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
- pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose );
+ pTemp = Saig_ManProofRefine( p, pResult, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fUseStart?&nUseStart:NULL, pPars->fVerbose );
if ( pTemp == NULL )
break;
Aig_ManStop( pResult );
pResult = pTemp;
printf( "ITER %4d : ", Iter );
- if ( !fVerbose )
+ if ( !pPars->fVerbose )
Aig_ManPrintStats( pResult );
// else
// printf( " -----------------------------------------------------\n" );
@@ -897,26 +935,52 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
// check if the ratio is reached
- if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
+ if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
{
- printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
+ printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
Aig_ManStop( pResult );
pResult = NULL;
break;
}
}
}
- Vec_IntFree( vFlops );
// write the final result
if ( pResult )
+ Aig_ManStop( pResult );
+ else
{
- Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
- printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
+ Vec_IntFree( vFlops );
+ vFlops = NULL;
}
- return pResult;
+ return vFlops;
}
+/**Function*************************************************************
+ Synopsis [Performs proof-based abstraction using BMC of the given depth.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars )
+{
+ Vec_Int_t * vFlops;
+ Aig_Man_t * pAbs = NULL;
+ vFlops = Saig_ManProofAbstraction_int( p, pPars );
+ // write the final result
+ if ( vFlops )
+ {
+ pAbs = Saig_ManAbstraction( p, vFlops );
+ Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
+ printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
+ Vec_IntFree( vFlops );
+ }
+ return pAbs;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index a37be3ad..ac1cbe5b 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -45,6 +45,7 @@ struct Saig_Bmc_t_
// node mapping
int nObjs; // the largest number of an AIG object
Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
+// Vec_Str_t * vAig2Frm2; // mapping of AIG nodees into Frames nodes
// SAT solver
sat_solver * pSat; // SAT solver
int nSatVars; // the number of used SAT variables
@@ -71,6 +72,170 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#define ABS_ZER 1
+#define ABS_ONE 2
+#define ABS_UND 3
+
+static inline int Abs_ManSimInfoNot( int Value )
+{
+ if ( Value == ABS_ZER )
+ return ABS_ONE;
+ if ( Value == ABS_ONE )
+ return ABS_ZER;
+ return ABS_UND;
+}
+
+static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
+{
+ if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
+ return ABS_ZER;
+ if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
+ return ABS_ONE;
+ return ABS_UND;
+}
+
+static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
+{
+ unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame );
+ return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
+}
+
+static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
+{
+ unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame );
+ assert( Value >= ABS_ZER && Value <= ABS_UND );
+ Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
+ pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+ int Value0, Value1, Value;
+ Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
+ if ( Value )
+ return Value;
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ assert( Saig_ObjIsLo(p, pObj) );
+ Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
+ Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
+ return Value;
+ }
+ Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
+ if ( Aig_ObjFaninC0(pObj) )
+ Value0 = Abs_ManSimInfoNot( Value0 );
+ if ( Aig_ObjIsPo(pObj) )
+ {
+ Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
+ return Value0;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ if ( Value0 == ABS_ZER )
+ Value = ABS_ZER;
+ else
+ {
+ Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
+ if ( Aig_ObjFaninC1(pObj) )
+ Value1 = Abs_ManSimInfoNot( Value1 );
+ Value = Abs_ManSimInfoAnd( Value0, Value1 );
+ }
+ Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
+ assert( Value );
+ return Value;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs ternary simulation for one design.]
+
+ Description [The returned array contains the result of ternary
+ simulation for all the frames where the output could be proved 0.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
+{
+ Vec_Ptr_t * vSimInfo;
+ Aig_Obj_t * pObj;
+ int i, f, nFramesLimit, nFrameWords;
+ int clk = clock();
+ assert( Aig_ManRegNum(p) > 0 );
+ // the maximum number of frames will be determined to use at most 200Mb of RAM
+ nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
+ nFramesLimit = ABC_MIN( nFramesLimit, nFramesMax );
+ nFrameWords = Aig_BitWordNum( 2 * Aig_ManObjNum(p) );
+ // allocate simulation info
+ vSimInfo = Vec_PtrAlloc( nFramesLimit );
+ for ( f = 0; f < nFramesLimit; f++ )
+ {
+ Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
+ if ( f == 0 )
+ {
+ Saig_ManForEachLo( p, pObj, i )
+ Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
+ }
+ Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
+ Saig_ManForEachPi( p, pObj, i )
+ Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
+ Saig_ManForEachPo( p, pObj, i )
+ Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
+ // check if simulation has derived at least one fail or unknown
+ Saig_ManForEachPo( p, pObj, i )
+ if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
+ {
+ if ( fVerbose )
+ {
+ printf( "Ternary sim found non-zero output in frame %d. Used %5.2f Mb. ",
+ f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
+ ABC_PRT( "Time", clock() - clk );
+ }
+ return vSimInfo;
+ }
+ }
+ if ( fVerbose )
+ {
+ printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f Mb. ",
+ nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
+ ABC_PRT( "Time", clock() - clk );
+ }
+ return vSimInfo;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Free the array of simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abs_ManFreeAray( Vec_Ptr_t * p )
+{
+ void * pTemp;
+ int i;
+ Vec_PtrForEachEntry( p, pTemp, i )
+ ABC_FREE( pTemp );
+ Vec_PtrFree( p );
+}
+
+
/**Function*************************************************************
Synopsis [Create manager.]
@@ -135,8 +300,32 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
***********************************************************************/
void Saig_BmcManStop( Saig_Bmc_t * p )
{
+// Aig_Obj_t * pObj;
+// int i, f, Counter = 0;
+// int i, Counter = 0;
+// for ( i = 0; i < p->vAig2Frm2->nSize; i++ )
+// Counter += (p->vAig2Frm2->pArray[i] != 0);
+// for ( i = 0; i < p->vAig2Frm->nSize; i++ )
+// Counter += (p->vAig2Frm->pArray[i] != NULL);
+// printf( "Objs = %d. Nodes = %d. Frames = %d. Used = %d. Non-empty = %d.\n",
+// p->nObjs, Aig_ManNodeNum(p->pAig), p->iFrameLast, p->vAig2Frm->nSize, Counter );
+
+/*
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ int Last = -1;
+ for ( f = 0; f <= p->iFrameLast; f++ )
+ if ( Saig_BmcObjFrame( p, pObj, f ) )
+ Last = f;
+ if ( i % 50 == 0 )
+ printf( "%d ", Last );
+ }
+ printf( "\n" );
+*/
+
Aig_ManStop( p->pFrm );
Vec_PtrFree( p->vAig2Frm );
+// Vec_StrFree( p->vAig2Frm2 );
Vec_IntFree( p->vObj2Var );
sat_solver_delete( p->pSat );
Vec_PtrFree( p->vTargets );
@@ -207,44 +396,6 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalConstruct_rec_OLD( 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_OLD( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
- else if ( Aig_ObjIsPo( pObj ) )
- {
- Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i );
- pRes = Saig_BmcObjChild0( p, pObj, i );
- }
- else
- {
- Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i );
- Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin1(pObj), i );
- pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
- }
- assert( pRes != AIG_VISITED );
- 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, Vec_Ptr_t * vVisited )
{
Aig_Obj_t * pRes;
@@ -263,8 +414,13 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
else
{
Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
- Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
- pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
+ if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
+ pRes = Aig_ManConst0(p->pFrm);
+ else
+ {
+ Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
+ pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
+ }
}
assert( pRes != NULL );
Saig_BmcObjSetFrame( p, pObj, i, pRes );
@@ -288,7 +444,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
{
Aig_Obj_t * pTarget;
Aig_Obj_t * pObj, * pRes;
- int i, iFrame;
+ int i, iFrame, Counter;
int nNodes = Aig_ManObjNum( p->pFrm );
Vec_PtrClear( p->vTargets );
p->iFramePrev = p->iFrameLast;
@@ -309,13 +465,18 @@ void Saig_BmcInterval( Saig_Bmc_t * p )
Aig_ObjCreatePo( p->pFrm, pTarget );
Aig_ManCleanup( p->pFrm );
// check if the node is gone
+ Counter = 0;
Vec_PtrForEachEntry( p->vVisited, pObj, i )
{
iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ );
pRes = Saig_BmcObjFrame( p, pObj, iFrame );
if ( Aig_ObjIsNone( Aig_Regular(pRes) ) )
+ {
Saig_BmcObjSetFrame( p, pObj, iFrame, NULL );
+ Counter++;
+ }
}
+// printf( "%d ", Counter );
}
}
}
@@ -564,7 +725,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
Aig_ManPrintStats( p->pFrm );
Aig_ManCleanup( p->pFrm );
Aig_ManPrintStats( p->pFrm );
-}
+}
/**Function*************************************************************
@@ -584,6 +745,11 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa
Cnf_Dat_t * pCnf;
int nOutsSolved = 0;
int Iter, RetValue, clk = clock(), clk2;
+/*
+ Vec_Ptr_t * vSimInfo;
+ vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
+ Abs_ManFreeAray( vSimInfo );
+*/
p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
if ( fVerbose )
{
@@ -593,6 +759,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa
printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
}
+
for ( Iter = 0; ; Iter++ )
{
clk2 = clock();
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index e6534a1f..e261fca1 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -70,7 +70,7 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
/**Function*************************************************************
- Synopsis [Numbers of flops included in the abstraction.]
+ Synopsis [Duplicates the AIG manager recursively.]
Description []
@@ -79,55 +79,130 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
+Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
- Aig_Man_t * pAigNew;//, * pTemp;
+ if ( pObj->pData )
+ return pObj->pData;
+ Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
+ Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
+ return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Trims the model by removing PIs without fanout.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i, fAllPisHaveNoRefs;
+ // check the refs of PIs
+ fAllPisHaveNoRefs = 1;
+ Saig_ManForEachPi( p, pObj, i )
+ if ( pObj->nRefs )
+ fAllPisHaveNoRefs = 0;
+ // start the new manager
+ pNew = Aig_ManStart( Aig_ManObjNum(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ // start mapping of the CI numbers
+ pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) );
+ // map const and primary inputs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManForEachPi( p, pObj, i )
+ if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
+ {
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
+ }
+ Aig_ManForEachNode( p, pObj, i )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Aig_ManForEachPo( p, pObj, i )
+ pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs abstraction of the AIG to preserve the included flops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
+{
+ Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, Entry;
+ Aig_ManCleanData( p );
// start the new manager
- pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
- pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ pNew = Aig_ManStart( Aig_ManNodeNum(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
// map the constant node
- Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
// label included flops
Vec_IntForEachEntry( vFlops, Entry, i )
{
- pObjLi = Saig_ManLi( pAig, Entry );
+ pObjLi = Saig_ManLi( p, Entry );
assert( pObjLi->fMarkA == 0 );
pObjLi->fMarkA = 1;
- pObjLo = Saig_ManLo( pAig, Entry );
+ pObjLo = Saig_ManLo( p, Entry );
assert( pObjLo->fMarkA == 0 );
pObjLo->fMarkA = 1;
}
// create variables for PIs
- Aig_ManForEachPi( pAig, pObj, i )
+ assert( p->vCiNumsOrig == NULL );
+ pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) );
+ Aig_ManForEachPi( p, pObj, i )
if ( !pObj->fMarkA )
- pObj->pData = Aig_ObjCreatePi( pAigNew );
+ {
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ Vec_IntPush( pNew->vCiNumsOrig, i );
+ }
// create variables for LOs
- Aig_ManForEachPi( pAig, pObj, i )
+ Aig_ManForEachPi( p, pObj, i )
if ( pObj->fMarkA )
{
pObj->fMarkA = 0;
- pObj->pData = Aig_ObjCreatePi( pAigNew );
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ Vec_IntPush( pNew->vCiNumsOrig, i );
}
// add internal nodes
- Aig_ManForEachNode( pAig, pObj, i )
- pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+// Aig_ManForEachNode( p, pObj, i )
+// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create POs
- Saig_ManForEachPo( pAig, pObj, i )
- Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ Saig_ManForEachPo( p, pObj, i )
+ {
+ Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
// create LIs
- Aig_ManForEachPo( pAig, pObj, i )
+ Aig_ManForEachPo( p, pObj, i )
if ( pObj->fMarkA )
{
pObj->fMarkA = 0;
- Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
- Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
- Aig_ManSeqCleanup( pAigNew );
-// pAigNew = Aig_ManDupSimpleDfs( pTemp = pAigNew );
-// Aig_ManStop( pTemp );
- return pAigNew;
+ Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
+ Aig_ManSeqCleanup( pNew );
+ // remove PIs without fanout
+ pNew = Saig_ManTrimPis( pTemp = pNew );
+ Aig_ManStop( pTemp );
+ return pNew;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index 97b91b1d..22d5d6b8 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -247,7 +247,7 @@ void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo
SeeAlso []
***********************************************************************/
-Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
{
Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
int i, f, Value;
@@ -262,7 +262,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t
vVis = Vec_IntAlloc( 1000 );
vVis2 = Vec_IntAlloc( 1000 );
vUndo = Vec_IntAlloc( 1000 );
- for ( i = iFirstPi; i < Saig_ManPiNum(p); i++ )
+ for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
{
Vec_IntClear( vUndo );
for ( f = pCex->iFrame; f >= 0; f-- )
@@ -297,7 +297,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t
SeeAlso []
***********************************************************************/
-Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, int fVerbose )
+Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, int fVerbose )
{
Vec_Int_t * vRes;
Vec_Ptr_t * vSimInfo;
@@ -305,10 +305,10 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_C
Aig_ManFanoutStart( p );
vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) );
clk = clock();
- vRes = Saig_ManExtendCounterExample( p, iFirstPi, pCex, vSimInfo, fVerbose );
+ vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
if ( fVerbose )
{
- printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) );
+ printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
ABC_PRT( "Time", clock() - clk );
}
Vec_PtrFree( vSimInfo );
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 0e99b1e8..cf5270dd 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -1285,7 +1285,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
// assert( Aig_ManRegNum(pAig) > 0 );
- assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
+// assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 21:48:55 +0000