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

Merged alanmi/abc into default

This commit is contained in:
Bruno Schmitt 2017-02-15 17:19:52 -08:00
parent 088aabc102 ab387953ab
commit 7811f1bb07
15 changed files with 1374 additions and 271 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -819,6 +819,10 @@ SOURCE=.\src\base\wlc\wlcStdin.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcUif.c
# End Source File
# Begin Source File
SOURCE=.\src\base\wlc\wlcWin.c
# End Source File
# Begin Source File

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

@ -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 );

37
src/aig/gia/giaDup.c
View File

@ -2169,6 +2169,43 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
return pNew;
}
/**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.]

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

@ -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 );

1
src/base/wlc/module.make
View File

@ -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

25
src/base/wlc/wlc.h
View File

@ -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 ========================================================*/

534
src/base/wlc/wlcAbs.c
View File

@ -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++ )
{
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 );
Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
Wlc_Obj_t * pObj; int i, Count[4] = {0};
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 ( 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 ( k == i )
break;
if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
{
Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
}
if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
continue;
}
Vec_IntFree( vMultis );
if ( Vec_IntSize( vPairs ) > 0 )
return vPairs;
Vec_IntFree( vPairs );
return NULL;
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;
}
}
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 [Abstracts nodes by replacing their outputs with new PIs.]
Synopsis [Marks nodes to be included in the abstracted network.]
Description [If array is NULL, abstract all multipliers.]
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 []
***********************************************************************/
Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
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 )
{
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 );
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 ( 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;
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 [Adds UIF constraints to node pairs and updates POs.]
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_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
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 * 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 );
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 [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 )
{
// 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 );
Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
}
// update each PO to point to the new node
Wlc_NtkForEachPo( p, pObj, i )
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 )
{
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 ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
}
// 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;
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_NtkAbsCore( 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;
}
////////////////////////////////////////////////////////////////////////

298
src/base/wlc/wlcAbs2.c
View File

@ -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 []
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 []
***********************************************************************/
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.]
Description []
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 ///
////////////////////////////////////////////////////////////////////////

2
src/base/wlc/wlcBlast.c
View File

@ -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 );
}

143
src/base/wlc/wlcCom.c
View File

@ -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 [-AMXF num] [-vh]\n" );
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: %%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;
}

91
src/base/wlc/wlcNtk.c
View File

@ -94,6 +94,30 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
/// 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->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.]
@ -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 ///
////////////////////////////////////////////////////////////////////////

290
src/base/wlc/wlcUif.c Normal file
View File

@ -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

194
src/proof/cec/cecSimBack.c Normal file
View File

@ -0,0 +1,194 @@
/**CFile****************************************************************
FileName [cecSimBack.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Backward simulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecSimBack.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cecInt.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ObjSatVerify( Gia_Man_t * p, Gia_Obj_t * pRoot, int Value )
{
Gia_Obj_t * pObj;
int i, RetValue = 1;
printf( "Obj = %4d Value = %d ", Gia_ObjId(p, pRoot), Value );
Gia_ObjTerSimSet0( Gia_ManConst0(p) );
Gia_ManForEachCi( p, pObj, i )
if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
Gia_ObjTerSimSetX( pObj ), printf( "x" );
else if ( pObj->fMark0 )
Gia_ObjTerSimSet1( pObj ), printf( "1" );
else
Gia_ObjTerSimSet0( pObj ), printf( "0" );
printf( " " );
Gia_ManForEachAnd( p, pObj, i )
Gia_ObjTerSimAnd( pObj );
if ( Value ? Gia_ObjTerSimGet1(pRoot) : Gia_ObjTerSimGet0(pRoot) )
printf( "Verification successful.\n" );
else
printf( "Verification failed.\n" ), RetValue = 0;
return RetValue;
}
/**Function*************************************************************
Synopsis [Return 1 if pObj can have Value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Cec_ManCheckSat2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, word Value, Vec_Wrd_t * vValues )
{
Gia_Obj_t * pFan0, * pFan1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return Value == (int)pObj->fMark0;
Gia_ObjSetTravIdCurrent(p, pObj);
pObj->fMark0 = Value;
if ( !Gia_ObjIsAnd(pObj) )
return 1;
pFan0 = Gia_ObjFanin0(pObj);
pFan1 = Gia_ObjFanin1(pObj);
if ( Value )
{
return Cec_ManCheckSat2_rec( p, pFan0, !Gia_ObjFaninC0(pObj), vValues ) &&
Cec_ManCheckSat2_rec( p, pFan1, !Gia_ObjFaninC1(pObj), vValues );
}
if ( Gia_ObjIsTravIdCurrent(p, pFan0) ) // already assigned
{
if ( Gia_ObjFaninC0(pObj) == (int)pFan0->fMark0 ) // justified
return 1;
return Cec_ManCheckSat2_rec( p, pFan1, Gia_ObjFaninC1(pObj), vValues );
}
if ( Gia_ObjIsTravIdCurrent(p, pFan1) ) // already assigned
{
if ( Gia_ObjFaninC1(pObj) == (int)pFan1->fMark0 ) // justified
return 1;
return Cec_ManCheckSat2_rec( p, pFan0, Gia_ObjFaninC0(pObj), vValues );
}
return Cec_ManCheckSat2_rec( p, pFan0, Gia_ObjFaninC0(pObj), vValues );
}
word Cec_ManCheckSat2( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Vec_Wrd_t * vValues )
{
return 0;
}
/**Function*************************************************************
Synopsis [Return 1 if pObj can have Value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManCheckSat_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value )
{
Gia_Obj_t * pFan0, * pFan1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return Value == (int)pObj->fMark0;
Gia_ObjSetTravIdCurrent(p, pObj);
pObj->fMark0 = Value;
if ( !Gia_ObjIsAnd(pObj) )
return 1;
pFan0 = Gia_ObjFanin0(pObj);
pFan1 = Gia_ObjFanin1(pObj);
if ( Value )
{
return Cec_ManCheckSat_rec( p, pFan0, !Gia_ObjFaninC0(pObj) ) &&
Cec_ManCheckSat_rec( p, pFan1, !Gia_ObjFaninC1(pObj) );
}
if ( Gia_ObjIsTravIdCurrent(p, pFan0) ) // already assigned
{
if ( Gia_ObjFaninC0(pObj) == (int)pFan0->fMark0 ) // justified
return 1;
return Cec_ManCheckSat_rec( p, pFan1, Gia_ObjFaninC1(pObj) );
}
if ( Gia_ObjIsTravIdCurrent(p, pFan1) ) // already assigned
{
if ( Gia_ObjFaninC1(pObj) == (int)pFan1->fMark0 ) // justified
return 1;
return Cec_ManCheckSat_rec( p, pFan0, Gia_ObjFaninC0(pObj) );
}
return Cec_ManCheckSat_rec( p, pFan0, Gia_ObjFaninC0(pObj) );
}
void Cec_ManSimBack( Gia_Man_t * p )
{
abctime clk = Abc_Clock();
Vec_Wrd_t * vValues = Vec_WrdStart( Gia_ManObjNum(p) );
Gia_Obj_t * pObj;
int i, Count = 0;
word Res;
Gia_ManSetPhase( p );
//Gia_ManForEachAnd( p, pObj, i )
// printf( "%d", pObj->fPhase );
//printf( "\n" );
//return;
Gia_ManForEachAnd( p, pObj, i )
{
Gia_ManIncrementTravId(p);
//Gia_ManCleanMark0( p );
Res = Cec_ManCheckSat_rec( p, pObj, !pObj->fPhase );
//if ( Res )
// Cec_ObjSatVerify( p, pObj, !pObj->fPhase );
//Res = Cec_ManCheckSat2_rec( p, pObj, !pObj->fPhase ? ~(word)0 : 0, vValues );
//if ( Res )
// Cec_ObjSatVerify2( p, pObj, !pObj->fPhase, Res );
Count += (int)(Res > 0);
}
Vec_WrdFree( vValues );
printf( "Obj = %6d. SAT = %6d. ", Gia_ManAndNum(p), Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

13
src/proof/pdr/pdrInv.c
View File

@ -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 );

2
src/proof/pdr/pdrMan.c
View File

@ -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 )