summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaDup.c37
-rw-r--r--src/base/abci/abc.c10
-rw-r--r--src/base/wlc/module.make1
-rw-r--r--src/base/wlc/wlc.h25
-rw-r--r--src/base/wlc/wlcAbs.c484
-rw-r--r--src/base/wlc/wlcAbs2.c298
-rw-r--r--src/base/wlc/wlcBlast.c2
-rw-r--r--src/base/wlc/wlcCom.c143
-rw-r--r--src/base/wlc/wlcNtk.c91
-rw-r--r--src/base/wlc/wlcUif.c290
-rw-r--r--src/proof/pdr/pdrInv.c13
-rw-r--r--src/proof/pdr/pdrMan.c2
13 files changed, 1151 insertions, 246 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6677e0ad..c183432a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1229,6 +1229,7 @@ extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int f
extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
+extern Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 56d1d29d..ee709df4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2171,6 +2171,43 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
/**Function*************************************************************
+ Synopsis [Permute inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ for ( i = 0; i < Gia_ManPiNum(p) - nPpis - nExtra; i++ ) // regular PIs
+ Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+ for ( i = Gia_ManPiNum(p) - nExtra; i < Gia_ManPiNum(p); i++ ) // extra PIs due to DC values
+ Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+ for ( i = Gia_ManPiNum(p) - nPpis - nExtra; i < Gia_ManPiNum(p) - nExtra; i++ ) // pseudo-PIs
+ Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+ for ( i = Gia_ManPiNum(p); i < Gia_ManCiNum(p); i++ ) // flop outputs
+ Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+ assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+ Gia_ManForEachAnd( p, pObj, i )
+ pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates AIG in the DFS order.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bb0b8c8d..af5d0ccf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26171,7 +26171,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
{
switch ( c )
{
@@ -26219,10 +26219,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nConfGenLimit < 0 )
goto usage;
break;
- case 'R':
+ case 'Q':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRestLimit = atoi(argv[globalUtilOptind]);
@@ -26366,7 +26366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
+ Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26374,7 +26374,7 @@ usage:
Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit );
- Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
+ Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap );
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 3485bd4d..c4330264 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -10,5 +10,6 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcSim.c \
src/base/wlc/wlcShow.c \
src/base/wlc/wlcStdin.c \
+ src/base/wlc/wlcUif.c \
src/base/wlc/wlcWin.c \
src/base/wlc/wlcWriteVer.c
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 21ba73a3..91dc0573 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -158,6 +158,7 @@ struct Wlc_Ntk_t_
Vec_Int_t vCopies; // object first bits
Vec_Int_t vBits; // object mapping into AIG nodes
Vec_Int_t vLevels; // object levels
+ Vec_Int_t vRefs; // object reference counters
};
typedef struct Wlc_Par_t_ Wlc_Par_t;
@@ -167,7 +168,10 @@ struct Wlc_Par_t_
int nBitsMul; // multiplier bit-widht
int nBitsMux; // MUX bit-width
int nBitsFlop; // flop bit-width
- int fVerbose; // verbose output`
+ int nIterMax; // the max number of iterations
+ int fXorOutput; // XOR outputs of word-level miter
+ int fVerbose; // verbose output
+ int fPdrVerbose; // verbose output
};
static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; }
@@ -272,19 +276,15 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
////////////////////////////////////////////////////////////////////////
/*=== wlcAbs.c ========================================================*/
-extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
-extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
-extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
-extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
-extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
+extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcAbs2.c ========================================================*/
-extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
-extern Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcBlast.c ========================================================*/
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth );
/*=== wlcCom.c ========================================================*/
extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
/*=== wlcNtk.c ========================================================*/
+extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
extern char * Wlc_ObjTypeName( Wlc_Obj_t * p );
extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc );
extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
@@ -311,6 +311,9 @@ extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int
extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
extern void Wlc_NtkShortNames( Wlc_Ntk_t * p );
+extern int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p );
+extern void Wlc_NtkSetRefs( Wlc_Ntk_t * p );
+extern int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew );
/*=== wlcReadSmt.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
@@ -321,6 +324,12 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
/*=== wlcReadVer.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
+/*=== wlcUif.c ========================================================*/
+extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
+extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
+extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
+extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
/*=== wlcWin.c =============================================================*/
extern void Wlc_WinProfileArith( Wlc_Ntk_t * p );
/*=== wlcWriteVer.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index ce6b8de9..318df4dd 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [wlcAbs.c]
+ FileName [wlcAbs1.c]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,11 +14,14 @@
Date [Ver. 1.0. Started - August 22, 2014.]
- Revision [$Id: wlcAbs.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+ Revision [$Id: wlcAbs1.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
***********************************************************************/
#include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
@@ -32,253 +35,370 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
- Synopsis [Check if two objects have the same input/output signatures.]
+ Synopsis [Mark operators that meet the abstraction criteria.]
- Description []
+ Description [This procedure returns the array of objects (vLeaves) that
+ should be abstracted because of their high bit-width. It uses input array (vUnmark)
+ to not abstract those objects that have been refined in the previous rounds.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
{
- Wlc_Obj_t * pFanin, * pFanin2; int k;
- if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
- return 0;
- if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
- return 0;
- if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
- return 0;
- for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+ Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ Wlc_Obj_t * pObj; int i, Count[4] = {0};
+ Wlc_NtkForEachObj( p, pObj, i )
{
- pFanin = Wlc_ObjFanin(p, pObj, k);
- pFanin2 = Wlc_ObjFanin(p, pObj2, k);
- if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
- return 0;
- if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
- return 0;
+ if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+ continue;
+ if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_MUX )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++;
+ continue;
+ }
+ if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
+ continue;
+ }
}
- return 1;
+ if ( fVerbose )
+ printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+ return vLeaves;
}
/**Function*************************************************************
- Synopsis [Collect IDs of the multipliers.]
+ Synopsis [Marks nodes to be included in the abstracted network.]
- Description []
+ Description [Marks all objects that will be included in the abstracted model.
+ Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+ a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+ set of flops present as flops in the abstracted network.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+ int i, iFanin;
+ if ( pObj->Mark )
+ return;
+ pObj->Mark = 1;
+ if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
+ {
+ assert( !Wlc_ObjIsPi(pObj) );
+ Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ if ( Wlc_ObjIsCi(pObj) )
+ {
+ if ( Wlc_ObjIsPi(pObj) )
+ Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) );
+ else
+ Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ Wlc_ObjForEachFanin( pObj, iFanin, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
+}
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
{
- Wlc_Obj_t * pObj; int i;
- Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkCleanMarks( p );
+ Wlc_NtkForEachCo( p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
Wlc_NtkForEachObj( p, pObj, i )
- if ( pObj->Type == WLC_OBJ_ARI_MULTI )
- Vec_IntPush( vBoxIds, i );
- if ( Vec_IntSize( vBoxIds ) > 0 )
- return vBoxIds;
- Vec_IntFree( vBoxIds );
- return NULL;
+ Count += pObj->Mark;
+// printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n",
+// Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops),
+// Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) );
+ Vec_IntSort( vPisOld, 0 );
+ Vec_IntSort( vPisNew, 0 );
+ Vec_IntSort( vFlops, 0 );
+ Wlc_NtkCleanMarks( p );
}
/**Function*************************************************************
- Synopsis [Returns all pairs of uifable multipliers.]
+ Synopsis [Derive word-level abstracted model based on the parameter values.]
- Description []
+ Description [Retuns the word-level abstracted network and the set of pseudo-PIs
+ (vPisNew), which were created during abstraction. If the abstraction is
+ satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+ and their MFFC cones will be listed in the array (vUnmark), which will
+ force the abstraction to not stop at these pseudo-PIs in the future.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
{
- Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
- Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
- Wlc_Obj_t * pObj, * pObj2; int i, k;
- // iterate through unique pairs
- Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
- Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
- {
- if ( k == i )
- break;
- if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
- {
- Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
- Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
- }
- }
- Vec_IntFree( vMultis );
- if ( Vec_IntSize( vPairs ) > 0 )
- return vPairs;
- Vec_IntFree( vPairs );
- return NULL;
+ Wlc_Ntk_t * pNtkNew = NULL;
+ Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
+ Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
+ Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
+ Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
+ Vec_BitFree( vLeaves );
+ pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+ Vec_IntFree( vPisOld );
+ Vec_IntFree( vFlops );
+ if ( pvPisNew )
+ *pvPisNew = vPisNew;
+ else
+ Vec_IntFree( vPisNew );
+ return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Find what objects need to be un-abstracted.]
+ Description [Returns a subset of pseudo-PIs (vPisNew), which will be
+ prevented from being abstracted in the future rounds of abstraction.
+ The AIG manager (pGia) is a bit-level view of the abstracted model.
+ The counter-example (pCex) is used to find waht PPIs to refine.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+ Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+ Abc_Cex_t * pCexCare;
+ Wlc_Obj_t * pObj;
+ // count the number of bit-level PPIs and map them into word-level objects they were derived from
+ int f, i, b, nRealPis, nPpiBits = 0;
+ Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+ Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+ // since PPIs are ordered last, the previous bits are real PIs
+ nRealPis = pCex->nPis - nPpiBits;
+ // find the care-set
+ pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+ assert( pCexCare->nPis == pCex->nPis );
+ // detect care PPIs
+ for ( f = 0; f <= pCexCare->iFrame; f++ )
+ for ( i = nRealPis; i < pCexCare->nPis; i++ )
+ if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+ Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+ Abc_CexFree( pCexCare );
+ Vec_IntFree( vMap );
+ if ( Vec_IntSize(vRefine) == 0 )// real CEX
+ Vec_IntFreeP( &vRefine );
+ return vRefine;
+}
/**Function*************************************************************
- Synopsis [Abstracts nodes by replacing their outputs with new PIs.]
+ Synopsis [Mark MFFC cones of the un-abstracted objects.]
- Description [If array is NULL, abstract all multipliers.]
+ Description [The MFFC cones of the objects in vRefine are traversed
+ and all their nodes are marked in vUnmark.]
SideEffects []
SeeAlso []
***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
{
- Vec_Int_t * vNodes = vNodesInit;
- Wlc_Ntk_t * pNew;
- Wlc_Obj_t * pObj;
- int i, k, iObj, iFanin;
- // get multipliers if not given
- if ( vNodes == NULL )
- vNodes = Wlc_NtkCollectMultipliers( p );
- if ( vNodes == NULL )
- return NULL;
- // mark nodes
- Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
- pObj->Mark = 1;
- // iterate through the nodes in the DFS order
- Wlc_NtkCleanCopy( p );
- Wlc_NtkForEachObj( p, pObj, i )
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
{
- if ( i == Vec_IntSize(&p->vCopies) )
- break;
- if ( pObj->Mark ) {
- // clean
- pObj->Mark = 0;
- // add fresh PI with the same number of bits
- iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
- }
- else {
- // update fanins
- Wlc_ObjForEachFanin( pObj, iFanin, k )
- Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
- // node to remain
- iObj = i;
- }
- Wlc_ObjSetCopy( p, i, iObj );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
+ }
+ return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
}
- // POs do not change in this procedure
- if ( vNodes != vNodesInit )
- Vec_IntFree( vNodes );
- // reconstruct topological order
- pNew = Wlc_NtkDupDfs( p, 0, 1 );
- return pNew;
+ return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int Count1, Count2;
+ // if this is a flop output, compute MFFC of the corresponding flop input
+ while ( Wlc_ObjIsCi(pNode) )
+ {
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ pNode = Wlc_ObjFo2Fi(p, pNode);
+ }
+ assert( !Wlc_ObjIsCi(pNode) );
+ // dereference the node (and set the bits in vUnmark)
+ Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+ // reference it back
+ Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+ assert( Count1 == Count2 );
+ return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+ Wlc_Obj_t * pObj; int i, nNodes = 0;
+ if ( Vec_IntSize(&p->vRefs) == 0 )
+ Wlc_NtkSetRefs( p );
+ Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+ nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+ return nNodes;
}
/**Function*************************************************************
- Synopsis [Adds UIF constraints to node pairs and updates POs.]
+ Synopsis [Performs abstraction.]
- Description []
+ Description [Derives initial abstraction based on user-specified
+ parameter values, which tell what is the smallest bit-width of a
+ primitive that is being abstracted away. Currently only add/sub,
+ mul/div, mux, and flop are supported with individual parameters.
+ The second step is to refine the initial abstraction until the
+ point when the property is proved.]
SideEffects []
SeeAlso []
***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
- Vec_Int_t * vPairs = vPairsInit;
- Wlc_Ntk_t * pNew;
- Wlc_Obj_t * pObj, * pObj2;
- Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
- int i, k, iObj, iObj2, iObjNew, iObjNew2;
- int iFanin, iFanin2, iFaninNew;
- // get multiplier pairs if not given
- if ( vPairs == NULL )
- vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
- if ( vPairs == NULL )
- return NULL;
- // sanity checks
- assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
- // iterate through node pairs
- vFanins = Vec_IntAlloc( 100 );
- vCompares = Vec_IntAlloc( 100 );
- vUifConstrs = Vec_IntAlloc( 100 );
- Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+ abctime clk = Abc_Clock();
+ int nIters, nNodes, nDcFlops, RetValue = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
+ pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
+ pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
- // get two nodes
- pObj = Wlc_NtkObj( p, iObj );
- pObj2 = Wlc_NtkObj( p, iObj2 );
- assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
- // create fanin comparator nodes
- Vec_IntClear( vCompares );
- Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
{
- iFanin2 = Wlc_ObjFaninId( pObj2, k );
- Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
- iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
- Vec_IntPush( vCompares, iFaninNew );
- // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
- // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
- pObj = Wlc_NtkObj( p, iObj );
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
}
- // concatenate fanin comparators
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
- // create reduction-OR node
- Vec_IntFill( vFanins, 1, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
- // craete output comparator node
- Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
- iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
- // create implication node (iObjNew is already complemented above)
- Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
- // save the constraint
- Vec_IntPush( vUifConstrs, iObjNew );
- }
- // derive the AND of the UIF contraints
- assert( Vec_IntSize(vUifConstrs) > 0 );
- if ( Vec_IntSize(vUifConstrs) == 1 )
- iObjNew = Vec_IntEntry( vUifConstrs, 0 );
- else
- {
- // concatenate
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
- // create reduction-AND node
- Vec_IntFill( vFanins, 1, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
- }
- // update each PO to point to the new node
- Wlc_NtkForEachPo( p, pObj, i )
- {
- iObj = Wlc_ObjId(p, pObj);
- Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
- // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
- // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
- pObj = Wlc_NtkObj( p, iObj );
- // update PO/CO arrays
- assert( Vec_IntEntry(&p->vPos, i) == iObj );
- assert( Vec_IntEntry(&p->vCos, i) == iObj );
- Vec_IntWriteEntry( &p->vPos, i, iObjNew );
- Vec_IntWriteEntry( &p->vCos, i, iObjNew );
- // transfer the PO attribute
- Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
- assert( pObj->fIsPo );
- pObj->fIsPo = 0;
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+ RetValue = Pdr_ManSolve( pAig, pPdrPars );
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+ Aig_ManStop( pAig );
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ break;
+ }
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
}
- // cleanup
- Vec_IntFree( vUifConstrs );
- Vec_IntFree( vCompares );
- Vec_IntFree( vFanins );
- if ( vPairs != vPairsInit )
- Vec_IntFree( vPairs );
- // reconstruct topological order
- pNew = Wlc_NtkDupDfs( p, 0, 1 );
- return pNew;
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
index f5a7b46d..9bccdf62 100644
--- a/src/base/wlc/wlcAbs2.c
+++ b/src/base/wlc/wlcAbs2.c
@@ -19,6 +19,9 @@
***********************************************************************/
#include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
@@ -26,56 +29,31 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct Wabs_Par_t_ Wabs_Par_t;
-struct Wabs_Par_t_
-{
- Wlc_Ntk_t * pNtk;
- Wlc_Par_t * pPars;
- Vec_Bit_t * vLeaves;
-};
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
-{
- memset( pPars, 0, sizeof(Wlc_Par_t) );
- pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
- pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
- pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
- pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
- pPars->fVerbose = 0; // verbose output`
-}
-
-/**Function*************************************************************
-
- Synopsis [Mark operators that meet the criteria.]
+ Synopsis [Mark operators that meet the abstraction criteria.]
- Description []
+ Description [This procedure returns the array of objects (vLeaves) that
+ should be abstracted because of their high bit-width. It uses input array (vUnmark)
+ to not abstract those objects that have been refined in the previous rounds.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
{
Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
Wlc_Obj_t * pObj; int i, Count[4] = {0};
Wlc_NtkForEachObj( p, pObj, i )
{
+ if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+ continue;
if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
@@ -101,7 +79,8 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
continue;
}
}
- printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+ if ( fVerbose )
+ printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
return vLeaves;
}
@@ -109,14 +88,17 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Synopsis [Marks nodes to be included in the abstracted network.]
- Description []
+ Description [Marks all objects that will be included in the abstracted model.
+ Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+ a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+ set of flops present as flops in the abstracted network.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
{
int i, iFanin;
if ( pObj->Mark )
@@ -139,8 +121,7 @@ void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeav
Wlc_ObjForEachFanin( pObj, iFanin, i )
Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
}
-
-void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
{
Wlc_Obj_t * pObj;
int i, Count = 0;
@@ -162,31 +143,264 @@ void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOl
/**Function*************************************************************
- Synopsis [Derive abstraction based on the parameter values.]
+ Synopsis [Derive word-level abstracted model based on the parameter values.]
- Description []
+ Description [Retuns the word-level abstracted network and the set of pseudo-PIs
+ (vPisNew), which were created during abstraction. If the abstraction is
+ satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+ and their MFFC cones will be listed in the array (vUnmark), which will
+ force the abstraction to not stop at these pseudo-PIs in the future.]
SideEffects []
SeeAlso []
***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
{
Wlc_Ntk_t * pNtkNew = NULL;
Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
- Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars );
+ Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
Vec_BitFree( vLeaves );
pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
Vec_IntFree( vPisOld );
- Vec_IntFree( vPisNew );
Vec_IntFree( vFlops );
+ if ( pvPisNew )
+ *pvPisNew = vPisNew;
+ else
+ Vec_IntFree( vPisNew );
return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Find what objects need to be un-abstracted.]
+
+ Description [Returns a subset of pseudo-PIs (vPisNew), which will be
+ prevented from being abstracted in the future rounds of abstraction.
+ The AIG manager (pGia) is a bit-level view of the abstracted model.
+ The counter-example (pCex) is used to find waht PPIs to refine.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+ Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+ Abc_Cex_t * pCexCare;
+ Wlc_Obj_t * pObj;
+ // count the number of bit-level PPIs and map them into word-level objects they were derived from
+ int f, i, b, nRealPis, nPpiBits = 0;
+ Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+ Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+ // since PPIs are ordered last, the previous bits are real PIs
+ nRealPis = pCex->nPis - nPpiBits;
+ // find the care-set
+ pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+ assert( pCexCare->nPis == pCex->nPis );
+ // detect care PPIs
+ for ( f = 0; f <= pCexCare->iFrame; f++ )
+ for ( i = nRealPis; i < pCexCare->nPis; i++ )
+ if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+ Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+ Abc_CexFree( pCexCare );
+ Vec_IntFree( vMap );
+ if ( Vec_IntSize(vRefine) == 0 )// real CEX
+ Vec_IntFreeP( &vRefine );
+ return vRefine;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Mark MFFC cones of the un-abstracted objects.]
+
+ Description [The MFFC cones of the objects in vRefine are traversed
+ and all their nodes are marked in vUnmark.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
+ }
+ return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+ }
+ return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int Count1, Count2;
+ // if this is a flop output, compute MFFC of the corresponding flop input
+ while ( Wlc_ObjIsCi(pNode) )
+ {
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ pNode = Wlc_ObjFo2Fi(p, pNode);
+ }
+ assert( !Wlc_ObjIsCi(pNode) );
+ // dereference the node (and set the bits in vUnmark)
+ Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+ // reference it back
+ Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+ assert( Count1 == Count2 );
+ return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+ Wlc_Obj_t * pObj; int i, nNodes = 0;
+ if ( Vec_IntSize(&p->vRefs) == 0 )
+ Wlc_NtkSetRefs( p );
+ Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+ nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+ return nNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs abstraction.]
+
+ Description [Derives initial abstraction based on user-specified
+ parameter values, which tell what is the smallest bit-width of a
+ primitive that is being abstracted away. Currently only add/sub,
+ mul/div, mux, and flop are supported with individual parameters.
+ The second step is to refine the initial abstraction until the
+ point when the property is proved.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ abctime clk = Abc_Clock();
+ int nIters, nNodes, nDcFlops, RetValue = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
+ pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
+ pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
+ {
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
+ {
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
+ }
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+ RetValue = Pdr_ManSolve( pAig, pPdrPars );
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+ Aig_ManStop( pAig );
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ break;
+ }
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
+ }
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 67d7c902..f4de8ee6 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1418,7 +1418,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
}
else
{
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 0 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 346a9076..97717b09 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -33,6 +33,7 @@ static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv )
static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -74,6 +75,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 );
@@ -458,7 +460,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -506,9 +508,26 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBitsFlop < 0 )
goto usage;
break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -520,17 +539,133 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
return 0;
}
- pNtk = Wlc_NtkAbs( pNtk, pPars );
- Wlc_AbcUpdateNtk( pAbc, pNtk );
+ Wlc_NtkAbsCore( pNtk, pPars );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+ Abc_Print( -2, "\t abstraction for word-level networks\n" );
+ Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+ Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
+ Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
+ Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Wlc_Par_t Pars, * pPars = &Pars;
+ int c;
+ Wlc_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsAdd < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMul < 0 )
+ goto usage;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMux < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsFlop < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkAbsCore2( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%abs [-AMXF num] [-vh]\n" );
+ Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\n" );
Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 86b0c17e..e6ab0739 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -96,6 +96,30 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Wlc_Par_t) );
+ pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
+ pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
+ pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
+ pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
+ pPars->nIterMax = 1000; // the max number of iterations
+ pPars->fXorOutput = 1; // XOR outputs of word-level miter
+ pPars->fVerbose = 0; // verbose output`
+ pPars->fPdrVerbose = 0; // show verbose PDR output
+}
+
+/**Function*************************************************************
+
Synopsis [Working with models.]
Description []
@@ -227,6 +251,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
ABC_FREE( p->vCopies.pArray );
ABC_FREE( p->vBits.pArray );
ABC_FREE( p->vLevels.pArray );
+ ABC_FREE( p->vRefs.pArray );
ABC_FREE( p->pInits );
ABC_FREE( p->pObjs );
ABC_FREE( p->pName );
@@ -912,7 +937,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vP
if ( p->pSpec )
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
- Wlc_NtkTransferNames( pNew, p );
+ //Wlc_NtkTransferNames( pNew, p );
return pNew;
}
@@ -1129,6 +1154,70 @@ void Wlc_NtkShortNames( Wlc_Ntk_t * p )
}
}
+/**Function*************************************************************
+
+ Synopsis [Count the number of flops initialized to DC value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p )
+{
+ int i, nFlops, Count = 0;
+ if ( p->pInits == NULL )
+ return 0;
+ nFlops = strlen(p->pInits);
+ for ( i = 0; i < nFlops; i++ )
+ Count += (p->pInits[i] == 'x' || p->pInits[i] == 'X');
+ return Count;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create references.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkSetRefs( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj; int i, k, Fanin;
+ Vec_IntFill( &p->vRefs, Wlc_NtkObjNumMax(p), 0 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ Wlc_ObjForEachFanin( pObj, Fanin, k )
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+ Wlc_NtkForEachCo( p, pObj, i )
+ Vec_IntAddToEntry( &p->vRefs, Wlc_ObjId(p, pObj), 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [This procedure simply count the number of PPI bits.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew )
+{
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ Count += Wlc_ObjRange(pObj);
+ return Count;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcUif.c b/src/base/wlc/wlcUif.c
new file mode 100644
index 00000000..78451c17
--- /dev/null
+++ b/src/base/wlc/wlcUif.c
@@ -0,0 +1,290 @@
+/**CFile****************************************************************
+
+ FileName [wlcUif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Verilog parser.]
+
+ Synopsis [Abstraction for word-level networks.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: wlcUif.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Check if two objects have the same input/output signatures.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+{
+ Wlc_Obj_t * pFanin, * pFanin2; int k;
+ if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
+ return 0;
+ if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
+ return 0;
+ if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
+ return 0;
+ for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+ {
+ pFanin = Wlc_ObjFanin(p, pObj, k);
+ pFanin2 = Wlc_ObjFanin(p, pObj2, k);
+ if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
+ return 0;
+ if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect IDs of the multipliers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj; int i;
+ Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+ Vec_IntPush( vBoxIds, i );
+ if ( Vec_IntSize( vBoxIds ) > 0 )
+ return vBoxIds;
+ Vec_IntFree( vBoxIds );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns all pairs of uifable multipliers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+{
+ Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
+ Wlc_Obj_t * pObj, * pObj2; int i, k;
+ // iterate through unique pairs
+ Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
+ Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
+ {
+ if ( k == i )
+ break;
+ if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
+ {
+ Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
+ Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
+ }
+ }
+ Vec_IntFree( vMultis );
+ if ( Vec_IntSize( vPairs ) > 0 )
+ return vPairs;
+ Vec_IntFree( vPairs );
+ return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Abstracts nodes by replacing their outputs with new PIs.]
+
+ Description [If array is NULL, abstract all multipliers.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+{
+ Vec_Int_t * vNodes = vNodesInit;
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj;
+ int i, k, iObj, iFanin;
+ // get multipliers if not given
+ if ( vNodes == NULL )
+ vNodes = Wlc_NtkCollectMultipliers( p );
+ if ( vNodes == NULL )
+ return NULL;
+ // mark nodes
+ Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
+ pObj->Mark = 1;
+ // iterate through the nodes in the DFS order
+ Wlc_NtkCleanCopy( p );
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ if ( i == Vec_IntSize(&p->vCopies) )
+ break;
+ if ( pObj->Mark ) {
+ // clean
+ pObj->Mark = 0;
+ // add fresh PI with the same number of bits
+ iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
+ }
+ else {
+ // update fanins
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+ // node to remain
+ iObj = i;
+ }
+ Wlc_ObjSetCopy( p, i, iObj );
+ }
+ // POs do not change in this procedure
+ if ( vNodes != vNodesInit )
+ Vec_IntFree( vNodes );
+ // reconstruct topological order
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds UIF constraints to node pairs and updates POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+{
+ Vec_Int_t * vPairs = vPairsInit;
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj, * pObj2;
+ Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
+ int i, k, iObj, iObj2, iObjNew, iObjNew2;
+ int iFanin, iFanin2, iFaninNew;
+ // get multiplier pairs if not given
+ if ( vPairs == NULL )
+ vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
+ if ( vPairs == NULL )
+ return NULL;
+ // sanity checks
+ assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
+ // iterate through node pairs
+ vFanins = Vec_IntAlloc( 100 );
+ vCompares = Vec_IntAlloc( 100 );
+ vUifConstrs = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+ {
+ // get two nodes
+ pObj = Wlc_NtkObj( p, iObj );
+ pObj2 = Wlc_NtkObj( p, iObj2 );
+ assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
+ // create fanin comparator nodes
+ Vec_IntClear( vCompares );
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ {
+ iFanin2 = Wlc_ObjFaninId( pObj2, k );
+ Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
+ iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
+ Vec_IntPush( vCompares, iFaninNew );
+ // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
+ // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+ pObj = Wlc_NtkObj( p, iObj );
+ }
+ // concatenate fanin comparators
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
+ // create reduction-OR node
+ Vec_IntFill( vFanins, 1, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
+ // craete output comparator node
+ Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
+ iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
+ // create implication node (iObjNew is already complemented above)
+ Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
+ // save the constraint
+ Vec_IntPush( vUifConstrs, iObjNew );
+ }
+ // derive the AND of the UIF contraints
+ assert( Vec_IntSize(vUifConstrs) > 0 );
+ if ( Vec_IntSize(vUifConstrs) == 1 )
+ iObjNew = Vec_IntEntry( vUifConstrs, 0 );
+ else
+ {
+ // concatenate
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
+ // create reduction-AND node
+ Vec_IntFill( vFanins, 1, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
+ }
+ // update each PO to point to the new node
+ Wlc_NtkForEachPo( p, pObj, i )
+ {
+ iObj = Wlc_ObjId(p, pObj);
+ Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
+ // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
+ // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+ pObj = Wlc_NtkObj( p, iObj );
+ // update PO/CO arrays
+ assert( Vec_IntEntry(&p->vPos, i) == iObj );
+ assert( Vec_IntEntry(&p->vCos, i) == iObj );
+ Vec_IntWriteEntry( &p->vPos, i, iObjNew );
+ Vec_IntWriteEntry( &p->vCos, i, iObjNew );
+ // transfer the PO attribute
+ Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
+ assert( pObj->fIsPo );
+ pObj->fIsPo = 0;
+ }
+ // cleanup
+ Vec_IntFree( vUifConstrs );
+ Vec_IntFree( vCompares );
+ Vec_IntFree( vFanins );
+ if ( vPairs != vPairsInit )
+ Vec_IntFree( vPairs );
+ // reconstruct topological order
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 554add9b..baade033 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
+ {
+ printf( "Frame " );
+ printf( "Clauses " );
+ printf( "Max Queue " );
+ printf( "Flops " );
+ printf( "Cex " );
+ printf( "Time" );
+ printf( "\n" );
return;
+ }
if ( Abc_FrameIsBatchMode() && !fClose )
return;
// count the total length of the printout
@@ -81,9 +90,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
for ( i = ThisSize; i < 70; i++ )
Abc_Print( 1, " " );
Abc_Print( 1, "%5d", p->nQueMax );
- Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
+ Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
if ( p->pPars->fUseAbs )
- Abc_Print( 1, "%5d", p->nCexes );
+ Abc_Print( 1, "%4d", p->nCexes );
Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
if ( p->pPars->fSolveAll )
Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index c19041ee..abe8c0a8 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -455,7 +455,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
int i, f, Lit, Flop, nFrames = 0;
int nPis = Saig_ManPiNum(p->pAig);
int nFfRefined = 0;
- if ( !p->pPars->fUseAbs )
+ if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
return Pdr_ManDeriveCex(p);
// restore previous map
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 15:44:38 +0000