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

Version abc70817

This commit is contained in:
Alan Mishchenko 2007-08-17 08:01:00 -07:00
parent 29c9b0c0c4
commit 9e4213e202
32 changed files with 3190 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
abc.dsp
View File

@ -2558,6 +2558,10 @@ SOURCE=.\src\aig\fra\fra.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraCec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraClass.c
# End Source File
# Begin Source File
@ -2570,6 +2574,10 @@ SOURCE=.\src\aig\fra\fraCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraImp.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraInd.c
# End Source File
# Begin Source File
@ -2578,10 +2586,18 @@ SOURCE=.\src\aig\fra\fraMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraPart.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraSat.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraSec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraSim.c
# End Source File
# End Group
@ -2770,6 +2786,10 @@ SOURCE=.\src\aig\aig\aigRepr.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigRet.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigSeq.c
# End Source File
# Begin Source File

21
src/aig/aig/aig.h
View File

@ -126,6 +126,7 @@ struct Aig_Man_t_
void * pData; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
int fAddStrash; // performs additional strashing
// timing statistics
int time1;
int time2;
@ -149,7 +150,16 @@ static inline int Aig_TruthWordNum( int nVars ) { return nVars
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Aig_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
return (uWord & 0x0000FFFF) + (uWord>>16);
}
static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); }
@ -328,6 +338,10 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF
// iterator over the latch inputs
#define Aig_ManForEachLiSeq( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
// iterator over the latch input and outputs
#define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k ) \
for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1) \
&& (((pObjLo)=Aig_ManLo(p, k)), 1); k++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@ -358,10 +372,14 @@ extern void Aig_ManFanoutStop( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered );
extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p );
@ -414,8 +432,11 @@ extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p );
/*=== aigRet.c ========================================================*/
extern Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
extern Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
/*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/

330
src/aig/aig/aigMan.c
View File

@ -170,6 +170,54 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
return pNew;
}
/**Function*************************************************************
Synopsis [Remaps the manager.]
Description [Map in the array specifies for each CI nodes the node that
should be used after remapping.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjMapped;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// implement the mapping
Aig_ManForEachPi( p, pObj, i )
{
pObjMapped = Vec_PtrEntry( vMap, i );
pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
}
// duplicate internal nodes
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = Aig_ObjChild0Copy(pObj);
else if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// add the POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Extracts the miter composed of XOR of the two nodes.]
@ -246,6 +294,110 @@ void Aig_ManStop( Aig_Man_t * p )
free( p );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
// collect latch input corresponding to unmarked PI (latch output)
if ( Aig_ObjIsPi(pObj) )
{
Vec_PtrPush( vNodes, pObj->pNext );
return;
}
if ( Aig_ObjIsPo(pObj) )
{
Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
return;
}
assert( Aig_ObjIsNode(pObj) );
Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManSeqCleanup( Aig_Man_t * p )
{
Vec_Ptr_t * vNodes, * vCis, * vCos;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, nTruePis, nTruePos;
assert( Aig_ManBufNum(p) == 0 );
// mark the PIs
Aig_ManIncrementTravId( p );
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
Aig_ManForEachPiSeq( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
// prepare to collect nodes reachable from POs
vNodes = Vec_PtrAlloc( 100 );
Aig_ManForEachPoSeq( p, pObj, i )
Vec_PtrPush( vNodes, pObj );
// remember latch inputs in latch outputs
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
pObjLo->pNext = pObjLi;
// mark the nodes reachable from these nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
Aig_ManSeqCleanup_rec( p, pObj, vNodes );
assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
// clean latch output pointers
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
pObjLo->pNext = NULL;
// if some latches are removed, update PIs/POs
if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
{
// collect new CIs/COs
vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPi( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCis, pObj );
vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCos, pObj );
else
Aig_ObjDisconnect( p, pObj );
// remember the number of true PIs/POs
nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
// set the new number of registers
p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
// create new PIs/POs
assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
Vec_PtrFree( p->vPis ); p->vPis = vCis;
Vec_PtrFree( p->vPos ); p->vPos = vCos;
p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
}
Vec_PtrFree( vNodes );
// remove dangling nodes
return Aig_ManCleanup( p );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
@ -275,6 +427,42 @@ int Aig_ManCleanup( Aig_Man_t * p )
return nNodesOld - Aig_ManNodeNum(p);
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManCountMergeRegs( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pFanin;
int i, Counter = 0, Const0 = 0, Const1 = 0;
Aig_ManIncrementTravId( p );
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
if ( Aig_ObjIsConst1(pFanin) )
{
if ( Aig_ObjFaninC0(pObj) )
Const0++;
else
Const1++;
}
if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
continue;
Aig_ObjSetTravIdCurrent(p, pFanin);
Counter++;
}
printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n",
Aig_ManRegNum(p), Counter, Const0, Const1 );
return 0;
}
/**Function*************************************************************
Synopsis [Stops the AIG manager.]
@ -302,6 +490,148 @@ void Aig_ManPrintStats( Aig_Man_t * p )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Checks how many latches can be reduced.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManReduceLachesCount( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pFanin;
int i, Counter = 0;
assert( Aig_ManRegNum(p) > 0 );
Aig_ManForEachObj( p, pObj, i )
assert( !pObj->fMarkA && !pObj->fMarkB );
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
if ( Aig_ObjFaninC0(pObj) )
{
if ( pFanin->fMarkB )
Counter++;
else
pFanin->fMarkB = 1;
}
else
{
if ( pFanin->fMarkA )
Counter++;
else
pFanin->fMarkA = 1;
}
}
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
pFanin->fMarkA = pFanin->fMarkB = 0;
}
return Counter;
}
/**Function*************************************************************
Synopsis [Reduces the latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
{
Vec_Ptr_t * vMap;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
int * pMapping, i;
// start mapping by adding the true PIs
vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPiSeq( p, pObj, i )
Vec_PtrPush( vMap, pObj );
// create mapping of fanin nodes into the corresponding latch outputs
pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
pFanin = Aig_ObjFanin0(pObjLi);
if ( Aig_ObjFaninC0(pObjLi) )
{
if ( pFanin->fMarkB )
{
Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
}
else
{
pFanin->fMarkB = 1;
pMapping[2*pFanin->Id + 1] = i;
Vec_PtrPush( vMap, pObjLo );
}
}
else
{
if ( pFanin->fMarkA )
{
Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
}
else
{
pFanin->fMarkA = 1;
pMapping[2*pFanin->Id] = i;
Vec_PtrPush( vMap, pObjLo );
}
}
}
free( pMapping );
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
pFanin->fMarkA = pFanin->fMarkB = 0;
}
return vMap;
}
/**Function*************************************************************
Synopsis [Reduces the latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
{
Aig_Man_t * pTemp;
Vec_Ptr_t * vMap;
int nSaved, nCur;
for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
{
if ( fVerbose )
{
printf( "Saved = %5d. ", nCur );
printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
}
vMap = Aig_ManReduceLachesOnce( p );
p = Aig_ManRemap( pTemp = p, vMap );
Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
if ( fVerbose )
{
printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
printf( "\n" );
}
}
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

83
src/aig/aig/aigOper.c
View File

@ -148,6 +148,89 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1);
if ( Aig_Regular(p1) == p->pConst1 )
return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1);
// check not so trivial cases
if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) )
{ // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf
Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD;
pFanA = Aig_ObjChild0(Aig_Regular(p0));
pFanB = Aig_ObjChild1(Aig_Regular(p0));
pFanC = Aig_ObjChild0(Aig_Regular(p1));
pFanD = Aig_ObjChild1(Aig_Regular(p1));
if ( Aig_IsComplement(p0) )
{
if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
return p1;
if ( pFanB == p1 )
return Aig_And( p, Aig_Not(pFanA), pFanB );
if ( pFanA == p1 )
return Aig_And( p, Aig_Not(pFanB), pFanA );
}
else
{
if ( pFanA == Aig_Not(p1) || pFanB == Aig_Not(p1) )
return Aig_Not(p->pConst1);
if ( pFanA == p1 || pFanB == p1 )
return p0;
}
if ( Aig_IsComplement(p1) )
{
if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
return p0;
if ( pFanD == p0 )
return Aig_And( p, Aig_Not(pFanC), pFanD );
if ( pFanC == p0 )
return Aig_And( p, Aig_Not(pFanD), pFanC );
}
else
{
if ( pFanC == Aig_Not(p0) || pFanD == Aig_Not(p0) )
return Aig_Not(p->pConst1);
if ( pFanC == p0 || pFanD == p0 )
return p1;
}
if ( !Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
{
if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
return Aig_Not(p->pConst1);
if ( pFanA == pFanC || pFanB == pFanC )
return Aig_And( p, p0, pFanD );
if ( pFanB == pFanC || pFanB == pFanD )
return Aig_And( p, pFanA, p1 );
if ( pFanA == pFanD || pFanB == pFanD )
return Aig_And( p, p0, pFanC );
if ( pFanA == pFanC || pFanA == pFanD )
return Aig_And( p, pFanB, p1 );
}
else if ( Aig_IsComplement(p0) && !Aig_IsComplement(p1) )
{
if ( pFanA == Aig_Not(pFanC) || pFanA == Aig_Not(pFanD) || pFanB == Aig_Not(pFanC) || pFanB == Aig_Not(pFanD) )
return p1;
if ( pFanB == pFanC || pFanB == pFanD )
return Aig_And( p, Aig_Not(pFanA), p1 );
if ( pFanA == pFanC || pFanA == pFanD )
return Aig_And( p, Aig_Not(pFanB), p1 );
}
else if ( !Aig_IsComplement(p0) && Aig_IsComplement(p1) )
{
if ( pFanC == Aig_Not(pFanA) || pFanC == Aig_Not(pFanB) || pFanD == Aig_Not(pFanA) || pFanD == Aig_Not(pFanB) )
return p0;
if ( pFanD == pFanA || pFanD == pFanB )
return Aig_And( p, Aig_Not(pFanC), p0 );
if ( pFanC == pFanA || pFanC == pFanB )
return Aig_And( p, Aig_Not(pFanD), p0 );
}
else // if ( Aig_IsComplement(p0) && Aig_IsComplement(p1) )
{
if ( pFanA == pFanD && pFanB == Aig_Not(pFanC) )
return Aig_Not(pFanA);
if ( pFanB == pFanC && pFanA == Aig_Not(pFanD) )
return Aig_Not(pFanB);
if ( pFanA == pFanC && pFanB == Aig_Not(pFanD) )
return Aig_Not(pFanA);
if ( pFanB == pFanD && pFanA == Aig_Not(pFanC) )
return Aig_Not(pFanB);
}
}
// check if it can be an EXOR gate
// if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
// return Aig_Exor( p, pFan0, pFan1 );

552
src/aig/aig/aigRet.c Normal file
View File

@ -0,0 +1,552 @@
/**CFile****************************************************************
FileName [aigRet.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Retiming of AIGs.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigRet.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// init values
typedef enum {
RTM_VAL_NONE, // 0: non-existent value
RTM_VAL_ZERO, // 1: initial value 0
RTM_VAL_ONE, // 2: initial value 1
RTM_VAL_VOID // 3: unused value
} Rtm_Init_t;
typedef struct Rtm_Man_t_ Rtm_Man_t;
struct Rtm_Man_t_
{
// network representation
Vec_Ptr_t * vObjs; // retiming objects
Vec_Ptr_t * vPis; // PIs only
Vec_Ptr_t * vPos; // POs only
Aig_MmFlex_t * pMem; // the memory manager
// storage for overflow latches
unsigned * pExtra;
unsigned * pExtraFree;
};
typedef struct Rtm_Edg_t_ Rtm_Edg_t;
struct Rtm_Edg_t_
{
unsigned long nLats : 12; // the number of latches
unsigned long LData : 20; // the latches themselves
};
typedef struct Rtm_Obj_t_ Rtm_Obj_t;
struct Rtm_Obj_t_
{
void * pCopy; // the copy of this object
unsigned long Type : 3; // object type
unsigned long fMark : 1; // multipurpose mark
unsigned long fCompl0 : 1; // complemented attribute of the first edge
unsigned long fCompl1 : 1; // complemented attribute of the second edge
unsigned long nFanins : 8; // the number of fanins
unsigned Num : 18; // the retiming number of this node
int Id; // ID of this object
int Temp; // temporary usage
int nFanouts; // the number of fanouts
void * pFanio[0]; // fanins and their edges (followed by fanouts and pointers to their edges)
};
static Rtm_Init_t Rtm_InitNot( Rtm_Init_t Val ) { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
static Rtm_Init_t Rtm_InitNotCond( Rtm_Init_t Val, int c ) { return c ? Rtm_InitNot(Val) : Val; }
static Rtm_Init_t Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE; if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
static Rtm_Obj_t * Rtm_ObjFanin( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*i]; }
static Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i ) { return (Rtm_Obj_t *)pObj->pFanio[2*(pObj->nFanins+i)]; }
static Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1); }
static Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i ) { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
static Rtm_Init_t Rtm_ObjGetFirst( Rtm_Edg_t * pEdge ) { return pEdge->LData & 3; }
static Rtm_Init_t Rtm_ObjGetLast( Rtm_Edg_t * pEdge ) { return (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; }
static Rtm_Init_t Rtm_ObjGetOne( Rtm_Edg_t * pEdge, int i ) { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (2 * i)) & 3; }
static Rtm_Init_t Rtm_ObjRemFirst( Rtm_Edg_t * pEdge ) { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
static Rtm_Init_t Rtm_ObjRemLast( Rtm_Edg_t * pEdge ) { int Val = (pEdge->LData >> (2 *(pEdge->nLats-1))) & 3; pEdge->LData ^= Val << (2 *(pEdge->nLats-1)); assert(pEdge->nLats > 0); pEdge->nLats--; return Val; }
static void Rtm_ObjAddFirst( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData = (pEdge->LData << 2) | Lat; pEdge->nLats++; }
static void Rtm_ObjAddLast( Rtm_Edg_t * pEdge, Rtm_Init_t Lat ) { assert( Lat < 4 ); pEdge->LData |= Lat << (2*pEdge->nLats); pEdge->nLats++; }
// iterator over the primary inputs
#define Rtm_ManForEachPi( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPis, pObj, i )
// iterator over the primary outputs
#define Rtm_ManForEachPo( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPos, pObj, i )
// iterator over all objects, including those currently not used
#define Rtm_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i )
// iterate through the fanins
#define Rtm_ObjForEachFanin( pObj, pFanin, i ) \
for ( i = 0; i < (int)(pObj)->nFanins && ((pFanin = Rtm_ObjFanin(pObj, i)), 1); i++ )
// iterate through the fanouts
#define Rtm_ObjForEachFanout( pObj, pFanout, i ) \
for ( i = 0; i < (int)(pObj)->nFanouts && ((pFanout = Rtm_ObjFanout(pObj, i)), 1); i++ )
// iterate through the fanin edges
#define Rtm_ObjForEachFaninEdge( pObj, pEdge, i ) \
for ( i = 0; i < (int)(pObj)->nFanins && ((pEdge = Rtm_ObjEdge(pObj, i)), 1); i++ )
// iterate through the fanout edges
#define Rtm_ObjForEachFanoutEdge( pObj, pEdge, i ) \
for ( i = 0; i < (int)(pObj)->nFanouts && ((pEdge = Rtm_ObjFanoutEdge(pObj, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the retiming manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Rtm_Man_t * Rtm_ManAlloc( Aig_Man_t * p )
{
Rtm_Man_t * pRtm;
// start the manager
pRtm = ALLOC( Rtm_Man_t, 1 );
memset( pRtm, 0, sizeof(Rtm_Man_t) );
// perform initializations
pRtm->vObjs = Vec_PtrAlloc( Aig_ManObjNum(p) );
pRtm->vPis = Vec_PtrAlloc( Aig_ManPiNum(p) );
pRtm->vPos = Vec_PtrAlloc( Aig_ManPoNum(p) );
pRtm->pMem = Aig_MmFlexStart();
return pRtm;
}
/**Function*************************************************************
Synopsis [Allocates the retiming manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rtm_ManFree( Rtm_Man_t * p )
{
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
Aig_MmFlexStop( p->pMem, 0 );
free( p );
}
/**Function*************************************************************
Synopsis [Counts the maximum number of latches on an edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Rtm_ManLatchMax( Rtm_Man_t * p )
{
Rtm_Obj_t * pObj;
Rtm_Edg_t * pEdge;
int nLatchMax = 0, i, k;
Rtm_ManForEachObj( p, pObj, i )
Rtm_ObjForEachFaninEdge( pObj, pEdge, k )
nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
return nLatchMax;
}
/**Function*************************************************************
Synopsis [Allocates the retiming object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Rtm_Obj_t * Rtm_ObjAlloc( Rtm_Man_t * pRtm, int nFanins, int nFanouts )
{
Rtm_Obj_t * pObj;
int Size = sizeof(Rtm_Obj_t) + sizeof(Rtm_Obj_t *) * (nFanins + nFanouts) * 2;
pObj = (Rtm_Obj_t *)Aig_MmFlexEntryFetch( pRtm->pMem, Size );
memset( pObj, 0, sizeof(Rtm_Obj_t) );
pObj->Type = (int)(nFanins == 1 && nFanouts == 0); // mark PO
pObj->Num = nFanins; // temporary
pObj->Temp = nFanouts;
pObj->Id = Vec_PtrSize(pRtm->vObjs);
Vec_PtrPush( pRtm->vObjs, pObj );
return pObj;
}
/**Function*************************************************************
Synopsis [Allocates the retiming object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rtm_ObjAddFanin( Rtm_Obj_t * pObj, Rtm_Obj_t * pFanin, int fCompl )
{
pObj->pFanio[ 2*pObj->nFanins ] = pFanin;
pObj->pFanio[ 2*pObj->nFanins + 1 ] = NULL;
pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) ] = pObj;
pFanin->pFanio[ 2*(pFanin->Num + pFanin->nFanouts) + 1 ] = pObj->pFanio + 2*pObj->nFanins + 1;
if ( pObj->nFanins == 0 )
pObj->fCompl0 = fCompl;
else if ( pObj->nFanins == 1 )
pObj->fCompl1 = fCompl;
else
assert( 0 );
pObj->nFanins++;
pFanin->nFanouts++;
assert( pObj->nFanins <= pObj->Num );
assert( pFanin->nFanouts <= pFanin->Temp );
}
/**Function*************************************************************
Synopsis [Check the possibility of forward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Rtm_ObjCheckRetimeFwd( Rtm_Obj_t * pObj )
{
Rtm_Edg_t * pEdge;
int i;
Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
if ( pEdge->nLats == 0 )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Check the possibility of forward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
{
Rtm_Obj_t * pFanin;
int i, Degree = 0;
Rtm_ObjForEachFanin( pObj, pFanin, i )
Degree = AIG_MAX( Degree, (int)pFanin->Num );
return Degree + 1;
}
/**Function*************************************************************
Synopsis [Performs forward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rtm_ObjRetimeFwd( Rtm_Obj_t * pObj )
{
Rtm_Init_t ValTotal, ValCur;
Rtm_Edg_t * pEdge;
int i;
assert( Rtm_ObjCheckRetimeFwd(pObj) );
// extract values and compute the result
ValTotal = RTM_VAL_ONE;
Rtm_ObjForEachFaninEdge( pObj, pEdge, i )
{
ValCur = Rtm_ObjRemFirst( pEdge );
ValCur = Rtm_InitNotCond( ValCur, i? pObj->fCompl1 : pObj->fCompl0 );
ValTotal = Rtm_InitAnd( ValTotal, ValCur );
}
// insert the result in the fanout values
Rtm_ObjForEachFanoutEdge( pObj, pEdge, i )
{
if ( pEdge->nLats >= 10 )
printf( "Rtm_ObjRetimeFwd(); More than 10 latches on the edge!\n" );
Rtm_ObjAddLast( pEdge, ValTotal );
}
}
/**Function*************************************************************
Synopsis [Derive retiming manager from the given AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
{
Rtm_Man_t * pRtm;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i;
assert( Aig_ManRegNum(p) > 0 );
assert( Aig_ManBufNum(p) == 0 );
// allocate the manager
pRtm = Rtm_ManAlloc( p );
// allocate objects
pObj = Aig_ManConst1(p);
pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs );
Aig_ManForEachPiSeq( p, pObj, i )
{
pObj->pData = Rtm_ObjAlloc( pRtm, 0, pObj->nRefs );
Vec_PtrPush( pRtm->vPis, pObj->pData );
}
Aig_ManForEachPoSeq( p, pObj, i )
{
pObj->pData = Rtm_ObjAlloc( pRtm, 1, 0 );
Vec_PtrPush( pRtm->vPos, pObj->pData );
}
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pData = Rtm_ObjAlloc( pRtm, 1, pObj->nRefs );
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pData = Rtm_ObjAlloc( pRtm, 1, 1 );
Aig_ManForEachNode( p, pObj, i )
pObj->pData = Rtm_ObjAlloc( pRtm, 2, pObj->nRefs );
// connect objects
Aig_ManForEachPoSeq( p, pObj, i )
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Aig_ManForEachLiSeq( p, pObj, i )
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
Rtm_ObjAddFanin( pObjLo->pData, pObjLi->pData, 0 );
Aig_ManForEachNode( p, pObj, i )
{
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
}
// set registers
Aig_ManForEachLoSeq( p, pObj, i )
Rtm_ObjAddFirst( Rtm_ObjEdge(pObj->pData, 0), RTM_VAL_ZERO );
return pRtm;
}
/**Function*************************************************************
Synopsis [Derive AIG manager after retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Obj_t * pObjRtm, int * pLatches )
{
Rtm_Edg_t * pEdge;
Aig_Obj_t * pRes, * pFanin;
int k, Val;
if ( pObjRtm->pCopy )
return pObjRtm->pCopy;
// get the inputs
pRes = Aig_ManConst1( pNew );
Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
{
if ( pEdge->nLats == 0 )
pFanin = Rtm_ManToAig_rec( pNew, Rtm_ObjFanin(pObjRtm, k), pLatches );
else
{
Val = Rtm_ObjGetFirst( pEdge );
pFanin = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + pEdge->nLats - 1 );
pFanin = Aig_NotCond( pFanin, Val == RTM_VAL_ONE );
}
pFanin = Aig_NotCond( pFanin, k ? pObjRtm->fCompl1 : pObjRtm->fCompl0 );
pRes = Aig_And( pNew, pRes, pFanin );
}
return pObjRtm->pCopy = pRes;
}
/**Function*************************************************************
Synopsis [Derive AIG manager after retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObjNew;
Rtm_Obj_t * pObjRtm;
Rtm_Edg_t * pEdge;
int i, k, m, Val, nLatches, * pLatches;
// count latches and mark the first latch on each edge
pLatches = ALLOC( int, 2 * Vec_PtrSize(pRtm->vObjs) );
nLatches = 0;
Rtm_ManForEachObj( pRtm, pObjRtm, i )
Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
{
pLatches[2*pObjRtm->Id + k] = Vec_PtrSize(pRtm->vPis) + nLatches;
nLatches += pEdge->nLats;
}
// create the new manager
pNew = Aig_ManStart( Vec_PtrSize(pRtm->vObjs) + nLatches );
// create PIs/POs and latches
pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
pObjRtm->pCopy = Aig_ManConst1(pNew);
Rtm_ManForEachPi( pRtm, pObjRtm, i )
pObjRtm->pCopy = Aig_ObjCreatePi(pNew);
for ( i = 0; i < nLatches; i++ )
Aig_ObjCreatePi(pNew);
// create internal nodes
Rtm_ManForEachObj( pRtm, pObjRtm, i )
Rtm_ManToAig_rec( pNew, pObjRtm, pLatches );
// create POs
Rtm_ManForEachPo( pRtm, pObjRtm, i )
Aig_ObjCreatePo( pNew, pObjRtm->pCopy );
// connect latches
Rtm_ManForEachObj( pRtm, pObjRtm, i )
Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
{
if ( pEdge->nLats == 0 )
continue;
pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy;
for ( m = 0; m < (int)pEdge->nLats; m++ )
{
Val = Rtm_ObjGetOne( pEdge, pEdge->nLats - 1 - m );
pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
Aig_ObjCreatePo( pNew, pObjNew );
pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m );
pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
}
assert( Aig_Regular(pObjNew)->nRefs > 0 );
}
free( pLatches );
pNew->nRegs = nLatches;
// remove useless nodes
Aig_ManCleanup( pNew );
if ( !Aig_ManCheck( pNew ) )
printf( "Rtm_ManToAig: The network check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Performs forward retiming with the given limit on depth.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Rtm_ManRetimeFwd( Aig_Man_t * p, int nStepsMax, int fVerbose )
{
Vec_Ptr_t * vQueue;
Aig_Man_t * pNew;
Rtm_Man_t * pRtm;
Rtm_Obj_t * pObj, * pFanout;
Aig_Obj_t * pObjAig;
int i, k, Degree, DegreeMax = 0;
// create the retiming manager
pRtm = Rtm_ManFromAig( p );
// set the current retiming number
Rtm_ManForEachObj( pRtm, pObj, i )
{
assert( pObj->nFanins == pObj->Num );
assert( pObj->nFanouts == pObj->Temp );
pObj->Num = 0;
}
// put the LOs on the queue
vQueue = Vec_PtrAlloc( 1000 );
Aig_ManForEachLoSeq( p, pObjAig, i )
{
pObj = pObjAig->pData;
pObj->fMark = 1;
Vec_PtrPush( vQueue, pObj );
}
// perform retiming
DegreeMax = 0;
Vec_PtrForEachEntry( vQueue, pObj, i )
{
pObj->fMark = 0;
// retime the node
Rtm_ObjRetimeFwd( pObj );
// check if its fanouts should be retimed
Rtm_ObjForEachFanout( pObj, pFanout, k )
{
if ( pFanout->fMark ) // skip aleady scheduled
continue;
if ( pFanout->Type ) // skip POs
continue;
if ( !Rtm_ObjCheckRetimeFwd( pFanout ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeFwd( pFanout );
DegreeMax = AIG_MAX( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pFanout->fMark = 1;
pFanout->Num = Degree;
Vec_PtrPush( vQueue, pFanout );
}
}
if ( fVerbose )
printf( "Performed %d fwd latch moves of max depth %d and max latch count %d.\n",
Vec_PtrSize(vQueue), DegreeMax, Rtm_ManLatchMax(pRtm) );
Vec_PtrFree( vQueue );
// get the new manager
pNew = Rtm_ManToAig( pRtm );
Rtm_ManFree( pRtm );
// group the registers
pNew = Aig_ManReduceLaches( pNew, fVerbose );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

221
src/aig/aig/aigSeq.c
View File

@ -24,6 +24,70 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define AIG_XVS0 1
#define AIG_XVS1 2
#define AIG_XVSX 3
static inline void Aig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
static inline int Aig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
static inline int Aig_XsimInv( int Value )
{
if ( Value == AIG_XVS0 )
return AIG_XVS1;
if ( Value == AIG_XVS1 )
return AIG_XVS0;
assert( Value == AIG_XVSX );
return AIG_XVSX;
}
static inline int Aig_XsimAnd( int Value0, int Value1 )
{
if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
return AIG_XVS0;
if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
return AIG_XVSX;
assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
return AIG_XVS1;
}
static inline int Aig_XsimRand2()
{
return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
}
static inline int Aig_XsimRand3()
{
int RetValue;
do {
RetValue = rand() & 3;
} while ( RetValue == 0 );
return RetValue;
}
static inline int Aig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
{
int RetValue;
RetValue = Aig_ObjGetXsim(Aig_ObjFanin0(pObj));
return Aig_ObjFaninC0(pObj)? Aig_XsimInv(RetValue) : RetValue;
}
static inline int Aig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
{
int RetValue;
RetValue = Aig_ObjGetXsim(Aig_ObjFanin1(pObj));
return Aig_ObjFaninC1(pObj)? Aig_XsimInv(RetValue) : RetValue;
}
static inline void Aig_XsimPrint( FILE * pFile, int Value )
{
if ( Value == AIG_XVS0 )
{
fprintf( pFile, "0" );
return;
}
if ( Value == AIG_XVS1 )
{
fprintf( pFile, "1" );
return;
}
assert( Value == AIG_XVSX );
fprintf( pFile, "x" );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -493,6 +557,163 @@ int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
}
/**Function*************************************************************
Synopsis [Cycles the circuit to create a new initial state.]
Description [Simulates the circuit with random input for the given
number of timeframes to get a better initial state.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
{
int nRounds = 1000; // limit on the number of ternary simulation rounds
Vec_Ptr_t * vMap;
Vec_Ptr_t * vStates;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
unsigned * pState, * pPrev;
int i, k, f, fConstants, Value, nWords, nCounter;
// allocate storage for states
nWords = Aig_BitWordNum( 2*Aig_ManRegNum(p) );
vStates = Vec_PtrAllocSimInfo( nRounds, nWords );
// initialize the values
Aig_ObjSetXsim( Aig_ManConst1(p), AIG_XVS1 );
Aig_ManForEachPiSeq( p, pObj, i )
Aig_ObjSetXsim( pObj, AIG_XVSX );
Aig_ManForEachLoSeq( p, pObj, i )
Aig_ObjSetXsim( pObj, AIG_XVS0 );
// simulate for the given number of timeframes
for ( f = 0; f < nRounds; f++ )
{
// collect this state
pState = Vec_PtrEntry( vStates, f );
memset( pState, 0, sizeof(unsigned) * nWords );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
Value = Aig_ObjGetXsim(pObjLo);
if ( Value & 1 )
Aig_InfoSetBit( pState, 2 * i );
if ( Value & 2 )
Aig_InfoSetBit( pState, 2 * i + 1 );
// Aig_XsimPrint( stdout, Value );
}
// printf( "\n" );
// check if this state exists
for ( i = f - 1; i >= 0; i-- )
{
pPrev = Vec_PtrEntry( vStates, i );
if ( !memcmp( pPrev, pState, sizeof(unsigned) * nWords ) )
break;
}
if ( i >= 0 )
break;
// simulate internal nodes
Aig_ManForEachNode( p, pObj, i )
Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
// transfer the latch values
Aig_ManForEachLiSeq( p, pObj, i )
Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
}
if ( f == nRounds )
{
printf( "Aig_ManTernarySimulate(): Did not reach a fixed point.\n" );
Vec_PtrFree( vStates );
return NULL;
}
// OR all the states
pState = Vec_PtrEntry( vStates, 0 );
for ( i = 1; i <= f; i++ )
{
pPrev = Vec_PtrEntry( vStates, i );
for ( k = 0; k < nWords; k++ )
pState[k] |= pPrev[k];
}
// check if there are constants
fConstants = 0;
if ( 2*Aig_ManRegNum(p) == 32*nWords )
{
for ( i = 0; i < nWords; i++ )
if ( pState[i] != ~0 )
fConstants = 1;
}
else
{
for ( i = 0; i < nWords - 1; i++ )
if ( pState[i] != ~0 )
fConstants = 1;
if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(nWords-1) ) )
fConstants = 1;
}
if ( fConstants == 0 )
{
Vec_PtrFree( vStates );
return NULL;
}
// start mapping by adding the true PIs
vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPiSeq( p, pObj, i )
Vec_PtrPush( vMap, pObj );
// find constant registers
nCounter = 0;
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
nCounter += (Value == 1 || Value == 2);
if ( Value == 1 )
Vec_PtrPush( vMap, Aig_ManConst0(p) );
else if ( Value == 2 )
Vec_PtrPush( vMap, Aig_ManConst1(p) );
else if ( Value == 3 )
Vec_PtrPush( vMap, pObjLo );
else
assert( 0 );
// Aig_XsimPrint( stdout, Value );
}
// printf( "\n" );
Vec_PtrFree( vStates );
if ( fVerbose )
printf( "Detected %d constants after %d iterations.\n", nCounter, f );
return vMap;
}
/**Function*************************************************************
Synopsis [Reduces the circuit using ternary simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
{
Aig_Man_t * pTemp;
Vec_Ptr_t * vMap;
while ( vMap = Aig_ManTernarySimulate( p, fVerbose ) )
{
if ( fVerbose )
printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
p = Aig_ManRemap( pTemp = p, vMap );
Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
if ( fVerbose )
printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
}
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/aig/module.make
View File

@ -13,5 +13,5 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
src/aig/aig/aigTruth.c \
src/aig/aig/aigUtil.c \
src/aig/aig/aigWin.c
src/aig/aig/aigUtil.c \
src/aig/aig/aigWin.c

1
src/aig/bdc/bdcInt.h
View File

@ -76,7 +76,6 @@ struct Bdc_Isf_t_
unsigned * puOff; // off-set
};
typedef struct Bdc_Man_t_ Bdc_Man_t;
struct Bdc_Man_t_
{
// external parameters

10
src/aig/fra/fra.h
View File

@ -71,6 +71,7 @@ struct Fra_Par_t_
int nBTLimitMiter; // conflict limit at an output
int nFramesK; // the number of timeframes to unroll
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
};
// FRAIG equivalence classes
@ -101,6 +102,7 @@ struct Fra_Man_t_
int nFramesAll; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
// simulation info
void * pSim; // the simulation manager
unsigned * pSimWords; // memory for simulation information
int nSimWords; // the number of simulation words
// counter example storage
@ -187,21 +189,23 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
extern void Fra_ClassesPrepare( Fra_Cla_t * p );
extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
extern void Fra_ClassesLatchCorr( Fra_Man_t * p );
/*=== fraCnf.c ========================================================*/
extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
/*=== fraDfs.c ========================================================*/
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose );
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@ -214,6 +218,8 @@ extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSec.c ========================================================*/
extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
/*=== fraSim.c ========================================================*/
extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );

48
src/aig/fra/fraCec.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [fraCec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [CEC engined based on fraiging.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

42
src/aig/fra/fraClass.c
View File

@ -250,7 +250,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
SeeAlso []
***********************************************************************/
void Fra_ClassesPrepare( Fra_Cla_t * p )
void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
{
Aig_Obj_t ** ppTable, ** ppNexts;
Aig_Obj_t * pObj, * pTemp;
@ -266,8 +266,16 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
Vec_PtrClear( p->vClasses1 );
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
if ( fLatchCorr )
{
if ( !Aig_ObjIsPi(pObj) )
continue;
}
else
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
}
//printf( "%3d : ", pObj->Id );
//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
//printf( "\n" );
@ -312,7 +320,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
// allocate room for classes
p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
p->pMemClassesFree = p->pMemClasses + 2*nEntries;
// copy the entries into storage in the topological order
Vec_PtrClear( p->vClasses );
nEntries = 0;
@ -563,6 +571,32 @@ void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
Vec_PtrPush( p->vClasses, pClass );
}
/**Function*************************************************************
Synopsis [Creates latch correspondence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesLatchCorr( Fra_Man_t * p )
{
Aig_Obj_t * pObj;
int i, nEntries = 0;
Vec_PtrClear( p->pCla->vClasses1 );
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
{
Vec_PtrPush( p->pCla->vClasses1, pObj );
Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
}
// allocate room for classes
p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

63
src/aig/fra/fraCore.c
View File

@ -28,6 +28,63 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reports the status of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigMiterStatus( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pObjNew;
int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
if ( p->pData )
return 0;
Aig_ManForEachPoSeq( p, pObj, i )
{
pObjNew = Aig_ObjChild0(pObj);
// check if the output is constant 0
if ( pObjNew == Aig_ManConst0(p) )
{
CountConst0++;
continue;
}
// check if the output is constant 1
if ( pObjNew == Aig_ManConst1(p) )
{
CountNonConst0++;
continue;
}
// check if the output can be constant 0
if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
{
CountNonConst0++;
continue;
}
CountUndecided++;
}
/*
if ( p->pParams->fVerbose )
{
printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
printf( "Const0 = %d. ", CountConst0 );
printf( "NonConst0 = %d. ", CountNonConst0 );
printf( "Undecided = %d. ", CountUndecided );
printf( "\n" );
}
*/
if ( CountNonConst0 )
return 0;
if ( CountUndecided )
return -1;
return 1;
}
/**Function*************************************************************
Synopsis [Write speculative miter for one node.]
@ -121,9 +178,9 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vTimeouts, pObj );
// simulate the counter-example and return the Fraig node
Fra_Resimulate( p );
assert( Fra_ClassObjRepr(pObj) != pObjRepr );
if ( Fra_ClassObjRepr(pObj) == pObjRepr )
printf( "Fra_FraigNode(): Error in class refinement!\n" );
assert( Fra_ClassObjRepr(pObj) != pObjRepr );
}
/**Function*************************************************************
@ -196,7 +253,7 @@ clk = clock();
Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
// collect initial states
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
@ -228,7 +285,7 @@ p->timeTrav += clock() - clk2;
}
p->timeTotal = clock() - clk;
// collect final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
Fra_ManStop( p );

826
src/aig/fra/fraImp.c Normal file
View File

@ -0,0 +1,826 @@
/**CFile****************************************************************
FileName [fraImp.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Detecting and proving implications.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// simulation manager
typedef struct Sml_Man_t_ Sml_Man_t;
struct Sml_Man_t_
{
Aig_Man_t * pAig;
int nFrames;
int nWordsFrame;
int nWordsTotal;
unsigned pData[0];
};
static inline unsigned * Sml_ObjSim( Sml_Man_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
static inline int Sml_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
static inline int Sml_ImpRight( int Imp ) { return Imp >> 16; }
static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
static int * s_ImpCost = NULL;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sml_Man_t * Sml_ManStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame )
{
Sml_Man_t * p;
assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
p = (Sml_Man_t *)malloc( sizeof(Sml_Man_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame );
memset( p, 0, sizeof(Sml_Man_t) + sizeof(unsigned) * nFrames * nWordsFrame );
p->nFrames = nFrames;
p->nWordsFrame = nWordsFrame;
p->nWordsTotal = nFrames * nWordsFrame;
return p;
}
/**Function*************************************************************
Synopsis [Deallocates simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_ManStop( Sml_Man_t * p )
{
free( p );
}
/**Function*************************************************************
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_ManAssignRandom( Sml_Man_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
assert( Aig_ObjIsPi(pObj) );
pSims = Sml_ObjSim( p, pObj->Id );
for ( i = 0; i < p->nWordsTotal; i++ )
pSims[i] = Fra_ObjRandomSim();
}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_ManAssignConst( Sml_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
{
unsigned * pSims;
int i;
assert( Aig_ObjIsPi(pObj) );
pSims = Sml_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
}
/**Function*************************************************************
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_ManInitialize( Sml_Man_t * p, int fInit )
{
Aig_Obj_t * pObj;
int i;
if ( fInit )
{
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
// assign random info for primary inputs
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Sml_ManAssignRandom( p, pObj );
// assign the initial state for the latches
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Sml_ManAssignConst( p, pObj, 0, 0 );
}
else
{
Aig_ManForEachPi( p->pAig, pObj, i )
Sml_ManAssignRandom( p, pObj );
}
}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_ManAssignDist1( Sml_Man_t * p, unsigned * pPat )
{
Aig_Obj_t * pObj;
int f, i, k, Limit, nTruePis;
assert( p->nFrames > 0 );
if ( p->nFrames == 1 )
{
// copy the PI info
Aig_ManForEachPi( p->pAig, pObj, i )
Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
}
else
{
// copy the PI info for each frame
nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
for ( f = 0; f < p->nFrames; f++ )
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
// copy the latch info
k = 0;
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
// flip one bit of the last frame
if ( p->nFrames == 2 )
{
Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
// Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
}
}
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_NodeSimulate( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
int nSimWords = p->nWordsFrame;
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
assert( iFrame == 0 || nSimWords < p->nWordsTotal );
// get hold of the simulation information
pSims = Fra_ObjSim(pObj) + nSimWords * iFrame;
pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
// get complemented attributes of the children using their random info
fCompl = pObj->fPhase;
fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
// simulate
if ( fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (pSims0[i] | pSims1[i]);
else
for ( i = 0; i < nSimWords; i++ )
pSims[i] = ~(pSims0[i] | pSims1[i]);
}
else if ( fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (pSims0[i] | ~pSims1[i]);
else
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (~pSims0[i] & pSims1[i]);
}
else if ( !fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (~pSims0[i] | pSims1[i]);
else
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (pSims0[i] & ~pSims1[i]);
}
else // if ( !fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < nSimWords; i++ )
pSims[i] = ~(pSims0[i] & pSims1[i]);
else
for ( i = 0; i < nSimWords; i++ )
pSims[i] = (pSims0[i] & pSims1[i]);
}
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_NodeCopyFanin( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
{
unsigned * pSims, * pSims0;
int fCompl, fCompl0, i;
int nSimWords = p->nWordsFrame;
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsPo(pObj) );
assert( iFrame == 0 || nSimWords < p->nWordsTotal );
// get hold of the simulation information
pSims = Sml_ObjSim(p, pObj->Id) + nSimWords * iFrame;
pSims0 = Sml_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + nSimWords * iFrame;
// get complemented attributes of the children using their random info
fCompl = pObj->fPhase;
fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
// copy information as it is
if ( fCompl0 )
for ( i = 0; i < nSimWords; i++ )
pSims[i] = ~pSims0[i];
else
for ( i = 0; i < nSimWords; i++ )
pSims[i] = pSims0[i];
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_NodeTransferNext( Sml_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
{
unsigned * pSims0, * pSims1;
int i, nSimWords = p->nWordsFrame;
assert( !Aig_IsComplement(pOut) );
assert( !Aig_IsComplement(pIn) );
assert( Aig_ObjIsPo(pOut) );
assert( Aig_ObjIsPi(pIn) );
assert( iFrame == 0 || nSimWords < p->nWordsTotal );
// get hold of the simulation information
pSims0 = Sml_ObjSim(p, pOut->Id) + nSimWords * iFrame;
pSims1 = Sml_ObjSim(p, pIn->Id) + nSimWords * (iFrame+1);
// copy information as it is
for ( i = 0; i < nSimWords; i++ )
pSims1[i] = pSims0[i];
}
/**Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
***********************************************************************/
void Sml_SimulateOne( Sml_Man_t * p )
{
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int f, i, clk;
clk = clock();
for ( f = 0; f < p->nFrames; f++ )
{
// simulate the nodes
Aig_ManForEachNode( p->pAig, pObj, i )
Sml_NodeSimulate( p, pObj, f );
if ( f == p->nFrames - 1 )
break;
// copy simulation info into outputs
Aig_ManForEachLiSeq( p->pAig, pObj, i )
Sml_NodeCopyFanin( p, pObj, f );
// copy simulation info into the inputs
// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
// Sml_NodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
Sml_NodeTransferNext( p, pObjLi, pObjLo, f );
}
//p->timeSim += clock() - clk;
//p->nSimRounds++;
}
/**Function*************************************************************
Synopsis [Performs simulation of the uninitialized circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sml_Man_t * Sml_ManSimulateComb( Aig_Man_t * pAig, int nWords )
{
Sml_Man_t * p;
p = Sml_ManStart( pAig, 1, nWords );
Sml_ManInitialize( p, 0 );
Sml_SimulateOne( p );
return p;
}
/**Function*************************************************************
Synopsis [Performs simulation of the initialized circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
{
Sml_Man_t * p;
p = Sml_ManStart( pAig, nFrames, nWords );
Sml_ManInitialize( p, 1 );
Sml_SimulateOne( p );
return p;
}
/**Function*************************************************************
Synopsis [Counts the number of 1s in each siminfo of each node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Sml_ManCountOnes( Sml_Man_t * p )
{
Aig_Obj_t * pObj;
unsigned * pSim;
int i, k, * pnBits;
pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
memset( pnBits, 0, sizeof(int) * Aig_ManObjIdMax(p->pAig) + 1 );
Aig_ManForEachObj( p->pAig, pObj, i )
{
pSim = Sml_ObjSim( p, i );
for ( k = 0; k < p->nWordsTotal; k++ )
pnBits[i] += Aig_WordCountOnes( pSim[k] );
}
return pnBits;
}
/**Function*************************************************************
Synopsis [Counts the number of 1s in the reverse implication.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right )
{
unsigned * pSimL, * pSimR;
int k, Counter = 0;
pSimL = Sml_ObjSim( p, Left );
pSimR = Sml_ObjSim( p, Right );
for ( k = 0; k < p->nWordsTotal; k++ )
Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
return Counter;
}
/**Function*************************************************************
Synopsis [Returns 1 if implications holds.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Sml_ObjSim( p, Left );
pSimR = Sml_ObjSim( p, Right );
for ( k = 0; k < p->nWordsTotal; k++ )
if ( pSimL[k] & ~pSimR[k] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns the array of nodes sorted by the number of 1s.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
{
Aig_Obj_t * pObj;
Vec_Ptr_t * vNodes;
int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
// count 1s in each node's siminfo
pnBits = Sml_ManCountOnes( p );
// count number of nodes having that many 1s
nBits = p->nWordsTotal * 32;
assert( nBits >= 32 );
nNodes = 0;
pnNodes = ALLOC( int, nBits );
memset( pnNodes, 0, sizeof(int) * nBits );
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( i == 0 ) continue;
assert( pnBits[i] < nBits ); // "<" because of normalized info
pnNodes[pnBits[i]]++;
nNodes++;
}
// allocate memory for all the nodes
pMemory = ALLOC( int, nNodes + nBits );
// markup the memory for each node
vNodes = Vec_PtrAlloc( nBits );
Vec_PtrPush( vNodes, pMemory );
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( i == 0 ) continue;
pMemory += pnBits[i-1] + 1;
Vec_PtrPush( vNodes, pMemory );
}
// add the nodes
memset( pnNodes, 0, sizeof(int) * nBits );
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( i == 0 ) continue;
pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
pMemory[ pnNodes[pnBits[i]]++ ] = i;
}
// add 0s in the end
nTotal = 0;
Vec_PtrForEachEntry( vNodes, pMemory, i )
{
pMemory[ pnNodes[i]++ ] = 0;
nTotal += pnNodes[i];
}
assert( nTotal == nNodes + nBits );
return vNodes;
}
/**Function*************************************************************
Synopsis [Compares two implications using their cost.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sml_CompareCost( int * pNum1, int * pNum2 )
{
int Cost1 = s_ImpCost[*pNum1];
int Cost2 = s_ImpCost[*pNum2];
if ( Cost1 > Cost2 )
return -1;
if ( Cost1 < Cost2 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Compares two implications using their largest ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
{
int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
if ( Max1 < Max2 )
return -1;
if ( Max1 > Max2 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Derives implication candidates.]
Description [Implication candidates have the property that
(1) they hold using sequential simulation information
(2) they do not hold using combinational simulation information
(3) they have as high expressive power as possible (heuristically)
- this means they are relatively far in terms of Humming distance
meaning their complement covers a larger Boolean space
- they are easy to disprove combinationally
meaning they cover relatively a larger sequential subspace.]
SideEffects [The managers should have the first pattern (000...)]
SeeAlso []
***********************************************************************/
Vec_Int_t * Sml_ManImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit )
{
Sml_Man_t * pSeq, * pComb;
Vec_Int_t * vImps, * vTemp;
Vec_Ptr_t * vNodes;
int * pNodesI, * pNodesK, * pNumbers;
int i, k, Imp;
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Sml_ManSimulateComb( p->pManAig, 32 );
pSeq = Sml_ManSimulateSeq( p->pManAig, 32, 1 );
// get the nodes sorted by the number of 1s
vNodes = Sml_ManSortUsingOnes( pSeq );
// compute implications and their costs
s_ImpCost = ALLOC( int, nImpMaxLimit );
vImps = Vec_IntAlloc( nImpMaxLimit );
for ( k = pSeq->nWordsTotal * 32 - 1; k >= 0; k-- )
for ( i = k - 1; i >= 0; i-- )
{
for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
{
if ( Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) &&
!Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
{
Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
s_ImpCost[ Vec_IntSize(vImps) ] = Sml_NodeNotImpCost(pComb, *pNodesI, *pNodesK);
Vec_IntPush( vImps, Imp );
}
if ( Vec_IntSize(vImps) == nImpMaxLimit )
goto finish;
}
}
finish:
Sml_ManStop( pComb );
Sml_ManStop( pSeq );
// sort implications by their cost
pNumbers = ALLOC( int, Vec_IntSize(vImps) );
for ( i = 0; i < Vec_IntSize(vImps); i++ )
pNumbers[i] = i;
qsort( (void *)pNumbers, Vec_IntSize(vImps), sizeof(int),
(int (*)(const void *, const void *)) Sml_CompareCost );
// reorder implications
vTemp = Vec_IntAlloc( nImpUseLimit );
for ( i = 0; i < nImpUseLimit; i++ )
Vec_IntPush( vTemp, Vec_IntEntry( vImps, pNumbers[i] ) );
Vec_IntFree( vImps ); vImps = vTemp;
// dealloc
free( pNumbers );
free( s_ImpCost ); s_ImpCost = NULL;
free( Vec_PtrEntry(vNodes, 0) );
Vec_PtrFree( vNodes );
// order implications by the max ID involved
qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int),
(int (*)(const void *, const void *)) Sml_CompareMaxId );
return vImps;
}
// the following three procedures are called to
// - add implications to the SAT solver
// - check implications using the SAT solver
// - refine implications using after a cex is generated
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
{
sat_solver * pSat = p->pSat;
Aig_Obj_t * pLeft, * pRight;
Aig_Obj_t * pLeftF, * pRightF;
int pLits[2], Imp, Left, Right, i, f, status;
Vec_IntForEachEntry( vImps, Imp, i )
{
// get the corresponding nodes
pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
// add constraints in each timeframe
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map these info fraig
pLeftF = Fra_ObjFraig( pLeft, f );
pRightF = Fra_ObjFraig( pRight, f );
// get the corresponding SAT numbers
Left = Fra_ObjSatNum( Aig_Regular(pLeftF) );
Right = Fra_ObjSatNum( Aig_Regular(pRightF) );
assert( Left > 0 && Left < p->nSatVars );
assert( Right > 0 && Right < p->nSatVars );
// get the constaint
// L => R L' v R L & R'
pLits[0] = 2 * Left + !Aig_ObjPhaseReal(pLeftF);
pLits[1] = 2 * Right + Aig_ObjPhaseReal(pRightF);
// add contraint to solver
if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
{
sat_solver_delete( pSat );
p->pSat = NULL;
return;
}
}
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
sat_solver_delete( pSat );
p->pSat = NULL;
}
}
/**Function*************************************************************
Synopsis [Check implications for the node (if they are present).]
Description [Returns the new position in the array.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
{
Aig_Obj_t * pLeft, * pRight;
int i, Imp, Left, Right, Max;
Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
{
Left = Sml_ImpLeft(Imp);
Right = Sml_ImpRight(Imp);
Max = AIG_MAX( Left, Right );
assert( Max >= pNode->Id );
if ( Max > pNode->Id )
return i;
// get the corresponding nodes
pLeft = Aig_ManObj( p->pManAig, Left );
pRight = Aig_ManObj( p->pManAig, Right );
// check the implication
// - if true, a clause is added
// - if false, a cex is simulated
// Fra_NodesAreImp( p, pLeft, pRight );
// make sure the implication is refined
assert( Vec_IntEntry(vImps, Pos) == 0 );
}
return i;
}
/**Function*************************************************************
Synopsis [Removes those implications that no longer hold.]
Description [Returns 1 if refinement has happened.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
{
Aig_Obj_t * pLeft, * pRight;
int Imp, i, RetValue = 0;
Vec_IntForEachEntry( vImps, Imp, i )
{
if ( Imp == 0 )
continue;
// get the corresponding nodes
pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
// check if implication holds using this simulation info
if ( !Sml_NodeCheckImp(p->pSim, pLeft->Id, pRight->Id) )
{
Vec_IntWriteEntry( vImps, i, 0 );
RetValue = 1;
}
}
return RetValue;
}
/**Function*************************************************************
Synopsis [Removes empty implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ImpCompactArray( Vec_Int_t * vImps )
{
int i, k, Imp;
k = 0;
Vec_IntForEachEntry( vImps, Imp, i )
if ( Imp )
Vec_IntWriteEntry( vImps, k++, Imp );
Vec_IntShrink( vImps, k );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

34
src/aig/fra/fraInd.c
View File

@ -198,7 +198,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose )
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter )
{
Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars;
@ -208,7 +208,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
int nIter, i, clk = clock(), clk2;
if ( Aig_ManNodeNum(pManAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
return Aig_ManDup(pManAig, 1);
}
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
@ -216,14 +219,18 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
// get parameters
Fra_ParamsDefaultSeq( pPars );
pPars->nFramesK = nFramesK;
pPars->fVerbose = fVerbose;
pPars->fRewrite = fRewrite;
pPars->nFramesK = nFramesK;
pPars->fVerbose = fVerbose;
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using K initialized frames
Fra_Simulate( p, 1 );
// if ( fLatchCorr )
// Fra_ClassesLatchCorr( p );
// else
Fra_Simulate( p, 1 );
// refine e-classes using sequential simulation?
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
@ -239,6 +246,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
p->pManFraig = Fra_FramesWithClasses( p );
//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
// perform AIG rewriting
if ( p->pPars->fRewrite )
Fra_FraigInductionRewrite( p );
@ -252,8 +261,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
}
// convert the manager to SAT solver (the last nLatches outputs are inputs)
pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
// pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = Cnf_DataWriteIntoSolver( pCnf );
@ -278,7 +287,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
Fra_ObjSetFaninVec( pObj, (void *)1 );
}
Cnf_DataFree( pCnf );
/*
/*
Aig_ManForEachObj( p->pManFraig, pObj, i )
{
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
@ -300,6 +309,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig );
Aig_ManSeqCleanup( pManAigNew );
// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += clock() - clk2;
p->timeTotal = clock() - clk;
// get the final stats
@ -309,9 +320,10 @@ p->timeTotal = clock() - clk;
// free the manager
Fra_ManStop( p );
// check the output
if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
printf( "Proved output constant 0.\n" );
// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
// printf( "Proved output constant 0.\n" );
if ( pnIter ) *pnIter = nIter;
return pManAigNew;
}

1
src/aig/fra/fraMan.c
View File

@ -86,6 +86,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
pPars->nFramesK = 1; // the number of timeframes to unroll
pPars->fConeBias = 0;
pPars->fRewrite = 0;
pPars->fLatchCorr = 0;
}
/**Function*************************************************************

177
src/aig/fra/fraPart.c Normal file
View File

@ -0,0 +1,177 @@
/**CFile****************************************************************
FileName [fraPart.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Partitioning for induction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
{
ProgressBar * pProgress;
Vec_Vec_t * vSupps, * vSuppsIn;
Vec_Ptr_t * vSuppsNew;
Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
Vec_Int_t * vOverNew, * vQuantNew;
Aig_Obj_t * pObj;
int i, k, nCommon, CountOver, CountQuant;
int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
double Ratio, R;
int clk;
nTotalSupp = 0;
nTotalSupp2 = 0;
Ratio = 0.0;
// compute supports
clk = clock();
vSupps = Aig_ManSupports( p );
PRT( "Supports", clock() - clk );
// remove last entry
Aig_ManForEachPo( p, pObj, i )
{
vSup = Vec_VecEntry( vSupps, i );
Vec_IntPop( vSup );
// remember support
// pObj->pNext = (Aig_Obj_t *)vSup;
}
// create reverse supports
clk = clock();
vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
Aig_ManForEachPo( p, pObj, i )
{
vSup = Vec_VecEntry( vSupps, i );
Vec_IntForEachEntry( vSup, Entry, k )
Vec_VecPush( vSuppsIn, Entry, (void *)i );
}
PRT( "Inverse ", clock() - clk );
clk = clock();
// compute extended supports
Largest = 0;
vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) );
vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
// get old supports
vSup = Vec_VecEntry( vSupps, i );
if ( Vec_IntSize(vSup) < 2 )
continue;
// compute new supports
CountOver = CountQuant = 0;
vSupNew = Vec_IntDup( vSup );
// go through the nodes where the first var appears
Aig_ManForEachPo( p, pObj, k )
// iVar = Vec_IntEntry( vSup, 0 );
// vSupIn = Vec_VecEntry( vSuppsIn, iVar );
// Vec_IntForEachEntry( vSupIn, Entry, k )
{
// pObj = Aig_ManObj( p, Entry );
// get support of this output
// vSup2 = (Vec_Int_t *)pObj->pNext;
vSup2 = Vec_VecEntry( vSupps, k );
// count the number of common vars
nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
if ( nCommon < 2 )
continue;
if ( nCommon > nComLim )
{
vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
Vec_IntFree( vTemp );
CountOver++;
}
else
CountQuant++;
}
// save the results
Vec_PtrPush( vSuppsNew, vSupNew );
Vec_IntPush( vOverNew, CountOver );
Vec_IntPush( vQuantNew, CountQuant );
if ( Largest < Vec_IntSize(vSupNew) )
Largest = Vec_IntSize(vSupNew);
nTotalSupp += Vec_IntSize(vSup);
nTotalSupp2 += Vec_IntSize(vSupNew);
if ( Vec_IntSize(vSup) )
R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
else
R = 0;
Ratio += R;
if ( R < 5.0 )
continue;
printf( "%6d : ", i );
printf( "S = %5d. ", Vec_IntSize(vSup) );
printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
printf( "R = %7.2f. ", R );
printf( "Over = %5d. ", CountOver );
printf( "Quant = %5d. ", CountQuant );
printf( "\n" );
/*
Vec_IntForEachEntry( vSupNew, Entry, k )
printf( "%d ", Entry );
printf( "\n" );
*/
}
Extra_ProgressBarStop( pProgress );
PRT( "Scanning", clock() - clk );
// print cumulative statistics
printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
Ratio/Aig_ManPoNum(p), Largest );
Vec_VecFree( vSupps );
Vec_VecFree( vSuppsIn );
Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
Vec_IntFree( vOverNew );
Vec_IntFree( vQuantNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

95
src/aig/fra/fraSec.c Normal file
View File

@ -0,0 +1,95 @@
/**CFile****************************************************************
FileName [fraSec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Performs SEC based on seq sweeping.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
if ( nFramesFix )
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
}
else
{
// perform seq sweeping while increasing the number of frames
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
if ( RetValue == 1 )
printf( "UNSAT " );
else
printf( "UNDECIDED " );
PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
break;
Aig_ManStop( pNew );
}
}
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
Aig_ManStop( pNew );
// report the miter
if ( RetValue == 1 )
printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT. " );
else
printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
PRT( "Time", clock() - clkTotal );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

11
src/aig/fra/fraSim.c
View File

@ -537,7 +537,7 @@ int Fra_SelectBestPat( Fra_Man_t * p )
***********************************************************************/
void Fra_SimulateOne( Fra_Man_t * p )
{
Aig_Obj_t * pObj;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int f, i, clk;
clk = clock();
for ( f = 0; f < p->nFramesAll; f++ )
@ -551,9 +551,10 @@ clk = clock();
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
Fra_NodeCopyFanin( p, pObj, f );
// copy simulation info into the inputs
for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
// for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
// Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, i )
Fra_NodeTransferNext( p, pObjLi, pObjLo, f );
}
p->timeSim += clock() - clk;
p->nSimRounds++;
@ -627,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit )
// start the classes
Fra_AssignRandom( p, fInit );
Fra_SimulateOne( p );
Fra_ClassesPrepare( p->pCla );
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
// Fra_ClassesPrint( p->pCla, 0 );
//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );

5
src/aig/fra/module.make
View File

@ -1,7 +1,10 @@
SRC += src/aig/fra/fraClass.c \
SRC += src/aig/fra/fraCec.c \
src/aig/fra/fraClass.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
src/aig/fra/fraSim.c

83
src/base/abc/abcNtk.c
View File

@ -1086,6 +1086,89 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
}
/**Function*************************************************************
Synopsis [Removes POs with suppsize less than 2 and PIs without fanout.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i, k, m;
// filter POs
k = m = 0;
Abc_NtkForEachCo( pNtk, pObj, i )
{
if ( Abc_ObjIsPo(pObj) )
{
// remove constant nodes and PI pointers
if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 )
{
Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) );
if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 && !Abc_ObjIsPi(Abc_ObjFanin0(pObj)) )
Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 );
pNtk->vObjs->pArray[pObj->Id] = NULL;
pObj->Id = (1<<26)-1;
pNtk->nObjCounts[pObj->Type]--;
pNtk->nObjs--;
Abc_ObjRecycle( pObj );
continue;
}
// remove buffers/inverters of PIs
if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 1 )
{
if ( Abc_ObjIsPi(Abc_ObjFanin0(Abc_ObjFanin0(pObj))) )
{
Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) );
if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 )
Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 );
pNtk->vObjs->pArray[pObj->Id] = NULL;
pObj->Id = (1<<26)-1;
pNtk->nObjCounts[pObj->Type]--;
pNtk->nObjs--;
Abc_ObjRecycle( pObj );
continue;
}
}
Vec_PtrWriteEntry( pNtk->vPos, m++, pObj );
}
Vec_PtrWriteEntry( pNtk->vCos, k++, pObj );
}
Vec_PtrShrink( pNtk->vPos, m );
Vec_PtrShrink( pNtk->vCos, k );
// filter PIs
k = m = 0;
Abc_NtkForEachCi( pNtk, pObj, i )
{
if ( Abc_ObjIsPi(pObj) )
{
if ( Abc_ObjFanoutNum(pObj) == 0 )
{
pNtk->vObjs->pArray[pObj->Id] = NULL;
pObj->Id = (1<<26)-1;
pNtk->nObjCounts[pObj->Type]--;
pNtk->nObjs--;
Abc_ObjRecycle( pObj );
continue;
}
Vec_PtrWriteEntry( pNtk->vPis, m++, pObj );
}
Vec_PtrWriteEntry( pNtk->vCis, k++, pObj );
}
Vec_PtrShrink( pNtk->vPis, m );
Vec_PtrShrink( pNtk->vCis, k );
return Abc_NtkDup( pNtk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

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

@ -93,6 +93,7 @@ static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -171,6 +172,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -257,6 +259,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 );
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
@ -335,6 +338,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
@ -5134,6 +5138,84 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandTrim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, nLevels;
extern Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nLevels = 10;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
{
switch ( c )
{
/*
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nLevels = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLevels < 0 )
goto usage;
break;
*/
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for logic circuits.\n" );
return 0;
}
pNtkRes = Abc_NtkTrim( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "The command has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: trim [-h]\n" );
fprintf( pErr, "\t removes POs fed by PIs and constants, and PIs w/o fanout\n" );
// fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
@ -6085,6 +6167,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -6200,10 +6284,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Network should be strashed. Command has failed.\n" );
return 1;
}
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
*/
pNtkRes = NULL;
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@ -6211,7 +6301,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: test [-h]\n" );
@ -6627,6 +6716,11 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
Abc_NtkIvyCuts( pNtk, nInputs );
return 0;
@ -6690,6 +6784,11 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@ -6790,6 +6889,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDRewrite( pNtk, pPars );
if ( pNtkRes == NULL )
{
@ -6904,6 +7008,11 @@ int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 )
{
fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" );
@ -6986,6 +7095,11 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose );
if ( pNtkRes == NULL )
{
@ -7054,6 +7168,11 @@ int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose );
if ( pNtkRes == NULL )
{
@ -7124,6 +7243,11 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@ -7192,6 +7316,11 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose );
if ( pNtkRes == NULL )
@ -7273,6 +7402,11 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose );
if ( pNtkRes == NULL )
@ -7359,6 +7493,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
if ( pNtkRes == NULL )
@ -7453,6 +7592,11 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose );
if ( pNtkRes == NULL )
@ -7557,6 +7701,11 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "The number of leaves is infeasible.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose );
if ( pNtkRes == NULL )
@ -7728,6 +7877,11 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@ -10417,9 +10571,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nMaxIters;
int fForward;
int fBackward;
int fOneStep;
int fVerbose;
int Mode;
extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose );
extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -10429,10 +10584,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
Mode = 5;
fForward = 0;
fBackward = 0;
fOneStep = 0;
fVerbose = 0;
nMaxIters = 15;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbsvh" ) ) != EOF )
{
switch ( c )
{
@ -10453,6 +10609,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
fBackward ^= 1;
break;
case 's':
fOneStep ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -10497,7 +10656,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
// convert the network into an SOP network
pNtkRes = Abc_NtkToLogic( pNtk );
// perform the retiming
Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose );
Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fOneStep, fVerbose );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
@ -10517,7 +10676,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform the retiming
Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose );
Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fOneStep, fVerbose );
return 0;
usage:
@ -10532,6 +10691,7 @@ usage:
fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
fprintf( pErr, "\t-f : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" );
fprintf( pErr, "\t-b : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" );
fprintf( pErr, "\t-s : enables retiming one step only in mode 4 [default = %s]\n", fOneStep? "yes": "no" );
fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@ -10816,21 +10976,23 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int fExdc;
int fImp;
int fRewrite;
int fLatchCorr;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose );
extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFramesK = 1;
fExdc = 1;
fImp = 0;
fRewrite = 0;
fVerbose = 0;
nFramesK = 1;
fExdc = 1;
fImp = 0;
fRewrite = 0;
fLatchCorr = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF )
{
switch ( c )
{
@ -10854,6 +11016,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fRewrite ^= 1;
break;
case 'l':
fLatchCorr ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -10883,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose );
pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@ -10894,11 +11059,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" );
fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
// fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@ -10919,11 +11085,12 @@ usage:
int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtk, * pNtkRes, * pTemp;
int c;
int fLatchSweep;
int fAutoSweep;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -10964,14 +11131,31 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
// modify the current network
Abc_NtkCleanupSeq( pNtk, fLatchSweep, fAutoSweep, fVerbose );
// get the new network
pNtkRes = Abc_NtkDup( pNtk );
Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose );
if ( fLatchSweep )
{
pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 );
Abc_NtkDelete( pTemp );
pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose );
Abc_NtkDelete( pTemp );
}
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential cleanup has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: scleanup [-lavh]\n" );
fprintf( pErr, "\t performs sequential cleanup\n" );
fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" );
fprintf( pErr, "\t - removes and shared latches driven by constants\n" );
fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" );
fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" );
fprintf( pErr, "\t (the latter may change sequential behaviour)\n" );
fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
@ -11402,17 +11586,17 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
printf( "The network has no latches. Used combinational command \"cec\".\n" );
return 0;
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
{
printf( "The network has no latches. Used combinational command \"cec\".\n" );
return 0;
}
// perform equivalence checking
if ( fRetime )
Abc_NtkSecRetime( pNtk1, pNtk2 );
@ -11443,6 +11627,97 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
int fDelete1, fDelete2;
char ** pArgvNew;
int nArgcNew;
int c;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 0; // if 0, iterates through frames
fVerbose = 1;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames <= 0 )
goto usage;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
default:
goto usage;
}
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
{
printf( "The network has no latches. Used combinational command \"cec\".\n" );
return 0;
}
// perform verification
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose );
if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 0;
usage:
fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
return 1;
}
/**Function*************************************************************
Synopsis []

238
src/base/abci/abcDar.c
View File

@ -23,6 +23,7 @@
#include "dar.h"
#include "cnf.h"
#include "fra.h"
#include "fraig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -79,11 +80,13 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
if ( Abc_LatchIsInit1(pObj) )
Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
// perform the conversion of the internal nodes (assumes DFS ordering)
// pMan->fAddStrash = 1;
Abc_NtkForEachNode( pNtk, pObj, i )
{
pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
// printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
}
pMan->fAddStrash = 0;
// create the POs
Abc_NtkForEachCo( pNtk, pObj, i )
Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
@ -121,6 +124,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Ntk_t * pNtkNew;
Aig_Obj_t * pObj;
int i;
assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
@ -143,6 +147,59 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description [This procedure should be called after seq sweeping,
which changes the number of registers.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i;
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPiSeq( pMan, pObj, i )
pObj->pData = Abc_NtkCi(pNtkNew, i);
// create as many latches as there are registers in the manager
Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
{
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
Abc_ObjAddFanin( pObjNew, pObjLi->pData );
Abc_ObjAddFanin( pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
}
Abc_NtkAddDummyBoxNames( pNtkNew );
// rebuild the AIG
vNodes = Aig_ManDfs( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
else
pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
@ -367,55 +424,23 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
***********************************************************************/
Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;//, * pTemp;
// int * pArray;
Abc_Ntk_t * pNtkAig = NULL;
Aig_Man_t * pMan;
extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
assert( Abc_NtkIsStrash(pNtk) );
// convert to the AIG manager
pMan = Abc_NtkToDar( pNtk, 0 );
if ( pMan == NULL )
return NULL;
if ( !Aig_ManCheck( pMan ) )
{
printf( "Abc_NtkDar: AIG check has failed.\n" );
Aig_ManStop( pMan );
return NULL;
}
// perform balance
Aig_ManPrintStats( pMan );
/*
pArray = Abc_NtkGetLatchValues(pNtk);
Aig_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
free( pArray );
*/
// Aig_ManDumpBlif( pMan, "aig_temp.blif" );
// pMan->pPars = Dar_ManDefaultRwrPars();
Dar_ManRewrite( pMan, NULL );
Aig_ManPrintStats( pMan );
// Dar_ManComputeCuts( pMan );
/*
{
extern Aig_Cnf_t * Aig_ManDeriveCnf( Aig_Man_t * p );
extern void Aig_CnfFree( Aig_Cnf_t * pCnf );
Aig_Cnf_t * pCnf;
pCnf = Aig_ManDeriveCnf( pMan );
Aig_CnfFree( pCnf );
}
*/
// convert from the AIG manager
if ( Aig_ManLatchNum(pMan) )
pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
else
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
if ( pNtkAig == NULL )
return NULL;
// perform computation
// Fra_ManPartitionTest( pMan, 4 );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
// make sure everything is okay
if ( !Abc_NtkCheck( pNtkAig ) )
if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
{
printf( "Abc_NtkDar: The network check has failed.\n" );
Abc_NtkDelete( pNtkAig );
@ -867,23 +892,146 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose )
Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0 );
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan->nRegs = Abc_NtkLatchNum(pNtk);
// pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose );
pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
else
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose )
{
Fraig_Params_t Params;
Aig_Man_t * pMan;
Abc_Ntk_t * pMiter, * pTemp;
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return 0;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return 0;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
return 1;
}
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
// so fraiging does not reduce the number of functions represented by nodes
Fraig_ParamsSetDefault( &Params );
pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
Abc_NtkDelete( pTemp );
// derive the AIG manager
pMan = Abc_NtkToDar( pMiter, 1 );
Abc_NtkDelete( pMiter );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return -1;
}
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan = Aig_ManReduceLaches( pMan, fVerbose );
pMan = Aig_ManConstReduce( pMan, fVerbose );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
// pMan = Aig_ManConstReduce( pMan, 1 );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

1
src/base/abci/abcMiter.c
View File

@ -98,6 +98,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
Abc_AigCleanup(pNtkMiter->pManFunc);
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkMiter ) )

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

@ -322,7 +322,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n",
Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 );
fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) );
}
/**Function*************************************************************

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

@ -27,7 +27,7 @@
////////////////////////////////////////////////////////////////////////
static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///

4
src/base/abci/abcXsim.c
View File

@ -139,7 +139,11 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
fprintf( stdout, " : " );
Abc_NtkForEachLatch( pNtk, pObj, i )
{
// if ( Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) != XVSX )
// printf( " %s=", Abc_ObjName(pObj) );
Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) );
}
fprintf( stdout, " : " );
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );

125
src/base/io/ioReadAiger.c
View File

@ -121,8 +121,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Abc_ObjAddFanin( pNode1, pObj );
Vec_PtrPush( vNodes, pNode1 );
// assign names to latch and its input
Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
// Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
// printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
}
@ -142,7 +141,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
uLit = ((i + 1 + nInputs + nLatches) << 1);
uLit1 = uLit - Io_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
assert( uLit1 > uLit0 );
// assert( uLit1 > uLit0 );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
@ -171,67 +170,85 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
// read the names if present
pCur = pSymbols;
while ( pCur < pContents + nFileSize && *pCur != 'c' )
if ( *pCur != 'c' )
{
// get the terminal type
pType = pCur;
if ( *pCur == 'i' )
vTerms = pNtkNew->vPis;
else if ( *pCur == 'l' )
vTerms = pNtkNew->vBoxes;
else if ( *pCur == 'o' )
vTerms = pNtkNew->vPos;
else
int Counter = 0;
while ( pCur < pContents + nFileSize && *pCur != 'c' )
{
fprintf( stdout, "Wrong terminal type.\n" );
return NULL;
}
// get the terminal number
iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
// get the node
if ( iTerm >= Vec_PtrSize(vTerms) )
// get the terminal type
pType = pCur;
if ( *pCur == 'i' )
vTerms = pNtkNew->vPis;
else if ( *pCur == 'l' )
vTerms = pNtkNew->vBoxes;
else if ( *pCur == 'o' )
vTerms = pNtkNew->vPos;
else
{
fprintf( stdout, "Wrong terminal type.\n" );
return NULL;
}
// get the terminal number
iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
// get the node
if ( iTerm >= Vec_PtrSize(vTerms) )
{
fprintf( stdout, "The number of terminal is out of bound.\n" );
return NULL;
}
pObj = Vec_PtrEntry( vTerms, iTerm );
if ( *pType == 'l' )
pObj = Abc_ObjFanout0(pObj);
// assign the name
pName = pCur; while ( *pCur++ != '\n' );
// assign this name
*(pCur-1) = 0;
Abc_ObjAssignName( pObj, pName, NULL );
if ( *pType == 'l' )
{
Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
}
// mark the node as named
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
}
// assign the remaining names
Abc_NtkForEachPi( pNtkNew, pObj, i )
{
fprintf( stdout, "The number of terminal is out of bound.\n" );
return NULL;
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Counter++;
}
pObj = Vec_PtrEntry( vTerms, iTerm );
if ( *pType == 'l' )
pObj = Abc_ObjFanout0(pObj);
// assign the name
pName = pCur; while ( *pCur++ != '\n' );
// assign this name
*(pCur-1) = 0;
Abc_ObjAssignName( pObj, pName, NULL );
if ( *pType == 'l' )
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
// mark the node as named
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
}
Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" );
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" );
Counter++;
}
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Counter++;
}
if ( Counter )
printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
}
else
{
// printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
Abc_NtkShortNames( pNtkNew );
}
// skipping the comments
free( pContents );
Vec_PtrFree( vNodes );
// assign the remaining names
Abc_NtkForEachPi( pNtkNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
}
Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL );
}
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
}
// remove the extra nodes
Abc_AigCleanup( pNtkNew->pManFunc );

6
src/base/io/ioWriteAiger.c
View File

@ -163,6 +163,12 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
return;
}
// set the node numbers to be used in the output file
nNodes = 0;

16
src/opt/ret/retCore.c
View File

@ -41,7 +41,7 @@ int timeRetime = 0;
SeeAlso []
***********************************************************************/
int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose )
int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose )
{
int nLatches = Abc_NtkLatchNum(pNtk);
int nLevels = Abc_NtkLevel(pNtk);
@ -62,26 +62,26 @@ int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOn
switch ( Mode )
{
case 1: // forward
RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, fVerbose );
RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, 0, fVerbose );
break;
case 2: // backward
RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, fVerbose );
RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, 0, fVerbose );
break;
case 3: // min-area
RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose );
break;
case 4: // min-delay
if ( !fBackwardOnly )
RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose );
RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fOneStep, fVerbose );
if ( !fForwardOnly )
RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose );
RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fOneStep, fVerbose );
break;
case 5: // min-area + min-delay
RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose );
if ( !fBackwardOnly )
RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose );
RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, 0, fVerbose );
if ( !fForwardOnly )
RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose );
RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, 0, fVerbose );
break;
case 6: // Pan's algorithm
RetValue = Abc_NtkRetimeLValue( pNtk, 500, fVerbose );
@ -121,7 +121,7 @@ int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk )
// fprintf( stdout, "Abc_NtkRetimeDebug(): Network check has failed.\n" );
// Io_WriteBlifLogic( pNtk, "debug_temp.blif", 1 );
pNtkRet = Abc_NtkDup( pNtk );
Abc_NtkRetime( pNtkRet, 3, 0, 1, 0 ); // debugging backward flow
Abc_NtkRetime( pNtkRet, 3, 0, 1, 0, 0 ); // debugging backward flow
return !Abc_NtkSecFraig( pNtk, pNtkRet, 10000, 3, 0 );
}

4
src/opt/ret/retDelay.c
View File

@ -63,7 +63,7 @@ int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimi
Synopsis [Returns the best delay and the number of best iteration.]
Description []
Description []
SideEffects []
@ -145,7 +145,7 @@ if ( fVerbose && !fInitial )
if ( fVerbose && !fInitial )
printf( "%s : Starting delay = %3d. Final delay = %3d. IterBest = %2d (out of %2d).\n",
fForward? "Forward " : "Backward", DelayStart, DelayBest, IterBest, nIterLimit );
*pIterBest = IterBest;
*pIterBest = (nIterLimit == 1) ? 1 : IterBest;
return DelayBest;
}

4
src/opt/ret/retIncrem.c
View File

@ -41,7 +41,7 @@ static int Abc_NtkRetimeOneWay( Abc_Ntk_t * pNtk, int fForward, int fVerbose );
SeeAlso []
***********************************************************************/
int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose )
int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fOneStep, int fVerbose )
{
Abc_Ntk_t * pNtkCopy = NULL;
Vec_Ptr_t * vBoxes;
@ -55,7 +55,7 @@ int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int
Abc_NtkOrderCisCos( pNtk );
if ( fMinDelay )
{
nIterLimit = 2 * Abc_NtkLevel(pNtk);
nIterLimit = fOneStep? 1 : 2 * Abc_NtkLevel(pNtk);
pNtkCopy = Abc_NtkDup( pNtk );
tLatches = Abc_NtkRetimePrepareLatches( pNtkCopy );
st_free_table( tLatches );

4
src/opt/ret/retInt.h
View File

@ -46,11 +46,11 @@
/*=== retArea.c ========================================================*/
extern int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose );
/*=== retCore.c ========================================================*/
extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose );
extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose );
/*=== retDelay.c ========================================================*/
extern int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimit, int fForward, int fVerbose );
/*=== retDirect.c ========================================================*/
extern int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose );
extern int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fOneStep, int fVerbose );
extern void Abc_NtkRetimeShareLatches( Abc_Ntk_t * pNtk, int fInitial );
extern int Abc_NtkRetimeNodeIsEnabled( Abc_Obj_t * pObj, int fForward );
extern void Abc_NtkRetimeNode( Abc_Obj_t * pObj, int fForward, int fInitial );