Skip to content

A
abc
Commit ddc6d1c1 by Alan Mishchenko
Options

Version abc70828

parent 28467823
Showing with 2220 additions and 560 deletions
abc.dsp
......@@ -2586,6 +2586,10 @@ SOURCE=.\src\aig\fra\fraInd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraLcr.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraMan.c
# End Source File
# Begin Source File
......@@ -2794,6 +2798,10 @@ SOURCE=.\src\aig\aig\aigRet.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigScl.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigSeq.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -128,6 +128,8 @@ struct Aig_Man_t_
int fCatchExor; // enables EXOR nodes
int fAddStrash; // performs additional strashing
Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes
void (*pImpFunc) (void*, void*); // implication checking precedure
void * pImpData; // implication checking data
// timing statistics
int time1;
int time2;
......@@ -298,6 +300,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over the primary outputs
#define Aig_ManForEachPo( p, pObj, i ) \
Vec_PtrForEachEntry( p->vPos, pObj, i )
// iterator over the assertions
#define Aig_ManForEachAssert( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
// iterator over all objects, including those currently not used
#define Aig_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
......@@ -373,15 +378,12 @@ extern void Aig_ManFanoutStop( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
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 );
......@@ -436,6 +438,11 @@ 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_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
/*=== aigScl.c ==========================================================*/
extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigShow.c ========================================================*/
......
src/aig/aig/aigMan.c
......@@ -172,54 +172,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
/**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.]
Description []
......@@ -306,110 +258,6 @@ void Aig_ManStop( Aig_Man_t * p )
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.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManCleanup( Aig_Man_t * p )
{
Vec_Ptr_t * vObjs;
......@@ -430,42 +278,6 @@ int Aig_ManCleanup( Aig_Man_t * 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.]
Description []
......@@ -491,149 +303,6 @@ 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 ///
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/aigPart.c
......@@ -321,7 +321,7 @@ Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan )
}
assert( 0 );
}
printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
//printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
Part_ManStop( p );
// sort supports by size
Vec_VecSort( vSupps, 1 );
......
src/aig/aig/aigRepr.c
......@@ -253,7 +253,7 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
***********************************************************************/
Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
{
int fOrdered = 1;
int fOrdered = 0;
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
......
src/aig/aig/aigScl.c 0 → 100644
/**CFile****************************************************************
FileName [aigScl.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [Sequential cleanup.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigScl.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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 [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.]
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 [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, Diffs = 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;
}
}
// count fanins that have both attributes
Aig_ManForEachLiSeq( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
Diffs += pFanin->fMarkA && pFanin->fMarkB;
pFanin->fMarkA = pFanin->fMarkB = 0;
}
// printf( "Diffs = %d.\n", Diffs );
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 ///
////////////////////////////////////////////////////////////////////////
src/aig/aig/aigTsim.c
......@@ -24,7 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define TSI_MAX_ROUNDS 10000
#define TSI_MAX_ROUNDS 1000
#define AIG_XVS0 1
#define AIG_XVS1 2
......@@ -340,7 +340,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
}
if ( f == TSI_MAX_ROUNDS )
{
printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS );
printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
Aig_TsiStop( pTsi );
return NULL;
}
......
src/aig/aig/aigUtil.c
......@@ -662,7 +662,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
{
FILE * pFile;
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj, * pConst1 = NULL;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
int i, nDigits, Counter = 0;
if ( Aig_ManPoNum(p) == 0 )
{
......@@ -687,14 +687,22 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
fprintf( pFile, ".model test\n" );
// write PIs
fprintf( pFile, ".inputs" );
Aig_ManForEachPi( p, pObj, i )
Aig_ManForEachPiSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
// write POs
fprintf( pFile, ".outputs" );
Aig_ManForEachPo( p, pObj, i )
Aig_ManForEachPoSeq( p, pObj, i )
fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
fprintf( pFile, "\n" );
// write latches
if ( Aig_ManRegNum(p) )
{
fprintf( pFile, "\n" );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData );
fprintf( pFile, "\n" );
}
// write nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
......
src/aig/aig/module.make
......@@ -9,6 +9,8 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigOrder.c \
src/aig/aig/aigPart.c \
src/aig/aig/aigRepr.c \
src/aig/aig/aigRet.c \
src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
......
src/aig/fra/fra.h
......@@ -77,6 +77,7 @@ struct Fra_Par_t_
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
int fWriteImps; // record implications
};
// FRAIG equivalence classes
......@@ -148,7 +149,6 @@ struct Fra_Man_t_
// statistics
int nSimRounds;
int nNodesMiter;
int nLitsZero;
int nLitsBeg;
int nLitsEnd;
int nNodesBeg;
......@@ -202,6 +202,10 @@ static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pN
static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; }
static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
......@@ -222,7 +226,7 @@ extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFai
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
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_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
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 );
......@@ -233,18 +237,24 @@ extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
/*=== fraCnf.c ========================================================*/
extern void Fra_CnfNodeAddToSolver( 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 );
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 Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
extern void Fra_ImpCompactArray( Vec_Int_t * vImps );
extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
......@@ -259,7 +269,7 @@ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, A
extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
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 );
extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
/*=== fraSim.c ========================================================*/
extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
......
src/aig/fra/fraBmc.c
......@@ -31,6 +31,8 @@ struct Fra_Bmc_t_
int nPref; // the size of the prefix
int nDepth; // the depth of the frames
int nFramesAll; // the total number of timeframes
// implications to be filtered
Vec_Int_t * vImps;
// AIG managers
Aig_Man_t * pAig; // the original AIG manager
Aig_Man_t * pAigFrames; // initialized timeframes
......@@ -67,7 +69,6 @@ static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse
int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
Fra_Man_t * p = pObj0->pData;
// Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig;
Aig_Obj_t * pObjFrames0, * pObjFrames1;
Aig_Obj_t * pObjFraig0, * pObjFraig1;
int i;
......@@ -102,6 +103,69 @@ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
}
/**Function*************************************************************
Synopsis [Refines implications using BMC.]
Description [The input is the combinational FRAIG manager,
which is used to FRAIG the timeframes. ]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
{
Aig_Obj_t * pLeft, * pRight;
Aig_Obj_t * pLeftT, * pRightT;
Aig_Obj_t * pLeftF, * pRightF;
int i, f, Imp, Left, Right;
int fComplL, fComplR;
assert( p->nFramesAll == 1 );
assert( p->pManAig == pBmc->pAigFrames );
Vec_IntForEachEntry( pBmc->vImps, Imp, i )
{
if ( Imp == 0 )
continue;
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
// get the corresponding nodes
pLeft = Aig_ManObj( pBmc->pAig, Left );
pRight = Aig_ManObj( pBmc->pAig, Right );
// iterate through the timeframes
for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
{
// get timeframes nodes
pLeftT = Bmc_ObjFrames( pLeft, f );
pRightT = Bmc_ObjFrames( pRight, f );
// get the corresponding FRAIG nodes
pLeftF = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
// get the complemented attributes
fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
if ( fComplL != fComplR )
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
break;
}
// check the implication
// - if true, a clause is added
// - if false, a cex is simulated
// make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
{
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
break;
}
}
}
Fra_ImpCompactArray( pBmc->vImps );
}
/**Function*************************************************************
......@@ -125,8 +189,6 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
p->nFramesAll = nPref + nDepth;
p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
// p->pObjToFraig = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
// memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
return p;
}
......@@ -215,34 +277,6 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
/**Function*************************************************************
Synopsis [Constructs FRAIG manager for the initialized timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
{
Aig_Man_t * pFraig;
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = 100000;
pPars->fVerbose = 0;
pPars->fProve = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 0;
pFraig = Fra_FraigPerform( p->pAigFrames, pPars );
p->pObjToFraig = p->pAigFrames->pObjCopies;
p->pAigFrames->pObjCopies = NULL;
return pFraig;
}
/**Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
Description []
......@@ -255,12 +289,22 @@ Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
{
Aig_Obj_t * pObj;
int i, clk = clock();
int i, nImpsOld, clk = clock();
assert( p->pBmc == NULL );
// derive and fraig the frames
p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc );
// if implications are present, configure the AIG manager to check them
if ( p->pCla->vImps )
{
p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications;
p->pBmc->pAigFrames->pImpData = p->pBmc;
p->pBmc->vImps = p->pCla->vImps;
nImpsOld = Vec_IntSize(p->pCla->vImps);
}
p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
p->pBmc->pAigFrames->pObjCopies = NULL;
// annotate frames nodes with pointers to the manager
Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
pObj->pData = p;
......@@ -271,19 +315,31 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll,
Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
PRT( "Time", clock() - clk );
printf( "Before BMC: " ); Fra_ClassesPrint( p->pCla, 0 );
printf( "Before BMC: " );
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
printf( "Imp = %5d. ", nImpsOld );
printf( "\n" );
}
// refine the classes
p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
Fra_ClassesRefine( p->pCla );
Fra_ClassesRefine1( p->pCla );
Fra_ClassesRefine1( p->pCla, 1, NULL );
p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
// report the results
if ( p->pPars->fVerbose )
{
printf( "After BMC: " ); Fra_ClassesPrint( p->pCla, 0 );
printf( "After BMC: " );
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
// free the BMC manager
Fra_BmcStop( p->pBmc );
......
src/aig/fra/fraClass.c
......@@ -520,10 +520,10 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
SeeAlso []
***********************************************************************/
int Fra_ClassesRefine1( Fra_Cla_t * p )
int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
{
Aig_Obj_t * pObj, ** ppClass;
int i, k, nRefis;
int i, k, nRefis = 1;
// check if there is anything to refine
if ( Vec_PtrSize(p->vClasses1) == 0 )
return 0;
......@@ -565,7 +565,10 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
assert( ppClass[0] != NULL );
Vec_PtrPush( p->vClasses, ppClass );
// iteratively refine this class
nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
if ( fRefineNewClass )
nRefis += Fra_RefineClassLastIter( p, p->vClasses );
else if ( pSkipped )
(*pSkipped)++;
return nRefis;
}
......
src/aig/fra/fraCore.c
......@@ -246,7 +246,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vTimeouts, pObj );
// verify that the counter-example satisfies all the constraints
// if ( p->vCex )
// Fra_FraigVerifyCounterEx( p, p->vCex );
// Fra_FraigVerifyCounterEx( p, p->vCex );
// simulate the counter-example and return the Fraig node
Fra_SmlResimulate( p );
if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
......@@ -334,12 +334,15 @@ clk = clock();
if ( p->pPars->fChoicing )
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->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
Fra_FraigSweep( p );
// call back the procedure to check implications
if ( pManAig->pImpFunc )
pManAig->pImpFunc( p, pManAig->pImpData );
// finalize the fraiged manager
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
......@@ -397,6 +400,32 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
pPars->fChoicing = 1;
return Fra_FraigPerform( pManAig, pPars );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
{
Aig_Man_t * pFraig;
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = nConfMax;
pPars->fVerbose = 0;
pPars->fProve = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 0;
pFraig = Fra_FraigPerform( pManAig, pPars );
return pFraig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/fra/fraImp.c
......@@ -24,10 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
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; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -43,19 +39,35 @@ static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16)
SeeAlso []
***********************************************************************/
static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
{
unsigned * pSim;
int k, Counter = 0;
pSim = Fra_ObjSim( p, Node );
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
Counter += Aig_WordCountOnes( pSim[k] );
return Counter;
}
/**Function*************************************************************
Synopsis [Counts the number of 1s in each siminfo of each node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
unsigned * pSim;
int i, k, * pnBits;
int i, * 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 = Fra_ObjSim( p, i );
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
pnBits[i] += Aig_WordCountOnes( pSim[k] );
}
pnBits[i] = Fra_SmlCountOnesOne( p, i );
return pnBits;
}
......@@ -106,6 +118,27 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
Synopsis [Counts the number of 1s in the reverse implication.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
{
unsigned * pSimL, * pSimR;
int k;
pSimL = Fra_ObjSim( p, Left );
pSimR = Fra_ObjSim( p, Right );
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
pResult[k] |= pSimL[k] & ~pSimR[k];
}
/**Function*************************************************************
Synopsis [Returns the array of nodes sorted by the number of 1s.]
Description []
......@@ -284,7 +317,6 @@ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
***********************************************************************/
Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
{
// Aig_Obj_t * pObj;
int nSimWords = 64;
Fra_Sml_t * pSeq, * pComb;
Vec_Int_t * vImps, * vTemp;
......@@ -293,21 +325,13 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
// get the nodes sorted by the number of 1s
vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
/*
Aig_ManForEachObj( p->pManAig, pObj, i )
{
printf( "%6s", Aig_ObjIsPi(pObj)? "pi" : (Aig_ObjIsNode(pObj)? "node" : "other" ) );
printf( "%d (%d) :\n", i, pObj->fPhase );
Extra_PrintBinary( stdout, Fra_ObjSim( pComb, i ), 64 ); printf( "\n" );
Extra_PrintBinary( stdout, Fra_ObjSim( pSeq, i ), 64 ); printf( "\n" );
}
*/
// count the total number of implications
for ( k = nSimWords * 32; k > 0; k-- )
for ( i = k - 1; i > 0; i-- )
......@@ -335,10 +359,8 @@ Aig_ManForEachObj( p->pManAig, pObj, i )
nImpsComb++;
continue;
}
// printf( "d=%d c=%d ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
nImpsCollected++;
Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
......@@ -368,13 +390,16 @@ finish:
(int (*)(const void *, const void *)) Sml_CompareMaxId );
if ( p->pPars->fVerbose )
{
printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d. Cost = [%d < %d < %d] ",
nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
CostMin, CostRange, CostMax );
PRT( "Time", clock() - clk );
}
return vImps;
}
// the following three procedures are called to
// - add implications to the SAT solver
// - check implications using the SAT solver
......@@ -401,8 +426,8 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
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) );
pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
// check if all the nodes are present
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
......@@ -431,7 +456,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
// get the complemented attributes
fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
// get the constaint
// get the constraint
// L => R L' v R (complement = L & R')
pLits[0] = 2 * Left + !fComplL;
pLits[1] = 2 * Right + fComplR;
......@@ -476,8 +501,8 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
{
if ( Imp == 0 )
continue;
Left = Sml_ImpLeft(Imp);
Right = Sml_ImpRight(Imp);
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
Max = AIG_MAX( Left, Right );
assert( Max >= pNode->Id );
if ( Max > pNode->Id )
......@@ -494,9 +519,6 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
// assert( fComplL == fComplR );
// if ( fComplL != fComplR )
// printf( "Fra_ImpCheckForNode(): Unexpected situation!\n" );
if ( fComplL != fComplR )
Vec_IntWriteEntry( vImps, i, 0 );
continue;
......@@ -507,6 +529,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
{
p->pCla->fRefinement = 1;
Fra_SmlResimulate( p );
if ( Vec_IntEntry(vImps, i) != 0 )
printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
......@@ -536,8 +559,8 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
if ( Imp == 0 )
continue;
// get the corresponding nodes
pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
// check if implication holds using this simulation info
if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
{
......@@ -569,6 +592,113 @@ void Fra_ImpCompactArray( Vec_Int_t * vImps )
Vec_IntShrink( vImps, k );
}
/**Function*************************************************************
Synopsis [Determines the ratio of the state space by computed implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
{
int nSimWords = 64;
Fra_Sml_t * pComb;
unsigned * pResult;
double Ratio = 0.0;
int Left, Right, Imp, i;
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return Ratio;
// simulate the AIG manager with combinational patterns
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
// go through the implications and collect where they do not hold
pResult = Fra_ObjSim( pComb, 0 );
assert( pResult[0] == 0 );
Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
{
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
}
// count the number of ones in this area
Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
Fra_SmlStop( pComb );
return Ratio;
}
/**Function*************************************************************
Synopsis [Returns the number of failed implications.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
{
int nSimWords = 2000;
Fra_Sml_t * pSeq;
char * pfFails;
int Left, Right, Imp, i, Counter;
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return 0;
// simulate the AIG manager with combinational patterns
pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
// go through the implications and check how many of them do not hold
pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
{
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
}
// count how many has failed
Counter = 0;
for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
Counter += pfFails[i];
free( pfFails );
return Counter;
}
/**Function*************************************************************
Synopsis [Record proven implications in the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
{
Aig_Obj_t * pLeft, * pRight, * pMiter;
int nPosOld, Imp, i;
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return;
// go through the implication
nPosOld = Aig_ManPoNum(pNew);
Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
{
pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
// record the implication: L' + R
pMiter = Aig_Or( pNew,
Aig_NotCond(pLeft->pData, !pLeft->fPhase),
Aig_NotCond(pRight->pData, pRight->fPhase) );
Aig_ObjCreatePo( pNew, pMiter );
}
pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fraInd.c
......@@ -177,6 +177,61 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
{
Aig_Obj_t * pObj, ** pLatches;
int i, k, f, nNodesOld;
// set copy pointer of each object to point to itself
Aig_ManForEachObj( p, pObj, i )
pObj->pData = pObj;
// iterate and add objects
nNodesOld = Aig_ManObjIdMax(p);
pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
for ( f = 0; f < nFrames; f++ )
{
// clean latch inputs and outputs
Aig_ManForEachLiSeq( p, pObj, i )
pObj->pData = NULL;
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pData = NULL;
// save the latch input values
k = 0;
Aig_ManForEachLiSeq( p, pObj, i )
{
if ( Aig_ObjFanin0(pObj)->pData )
pLatches[k++] = Aig_ObjChild0Copy(pObj);
else
pLatches[k++] = NULL;
}
// insert them as the latch output values
k = 0;
Aig_ManForEachLoSeq( p, pObj, i )
pObj->pData = pLatches[k++];
// create the next time frame of nodes
Aig_ManForEachNode( p, pObj, i )
{
if ( i > nNodesOld )
break;
if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
pObj->pData = NULL;
}
}
free( pLatches );
}
/**Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
......@@ -186,7 +241,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
......@@ -201,8 +256,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew;
// Vec_Int_t * vImps;
int nNodesBeg, nRegsBeg, Temp;
int nIter, i, clk = clock(), clk2;
if ( Aig_ManNodeNum(pManAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
......@@ -212,6 +268,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
nNodesBeg = Aig_ManNodeNum(pManAig);
nRegsBeg = Aig_ManRegNum(pManAig);
// enhance the AIG by adding timeframes
// Fra_FramesAddMore( pManAig, 3 );
// get parameters
Fra_ParamsDefaultSeq( pPars );
......@@ -222,6 +284,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
pPars->fUseImps = fUseImps;
pPars->fWriteImps = fWriteImps;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
......@@ -255,19 +318,19 @@ PRT( "Time", clock() - clk );
p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
}
// perform BMC (for the min number of frames)
Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
//Fra_ClassesPrint( p->pCla, 1 );
// p->vCex = Vec_IntAlloc( 1000 );
// select the most expressive implications
if ( pPars->fUseImps )
p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
// perform BMC (for the min number of frames)
Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
//Fra_ClassesPrint( p->pCla, 1 );
// if ( p->vCex == NULL )
// p->vCex = Vec_IntAlloc( 1000 );
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig);
// dump AIG of the timeframes
// pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
......@@ -279,6 +342,8 @@ PRT( "Time", clock() - clk );
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
{
int nLitsOld = Fra_ClassesCountLits(p->pCla);
int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
......@@ -325,13 +390,13 @@ PRT( "Time", clock() - clk );
// report the intermediate results
if ( fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. %s = %6d. NR = %6d.\n",
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
p->pCla->vImps? "I" : "N",
p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig),
Aig_ManNodeNum(p->pManFraig) );
}
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
if ( p->pCla->vImps )
printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) );
}
// perform sweeping
p->nSatCallsRecent = 0;
......@@ -341,18 +406,40 @@ PRT( "Time", clock() - clk );
assert( p->vTimeouts == NULL );
if ( p->vTimeouts )
printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
// cleanup
Fra_ManClean( p );
// if ( nIter == 3 )
// break;
// check if refinement has happened
// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
if ( p->pCla->fRefinement &&
nLitsOld == Fra_ClassesCountLits(p->pCla) &&
nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) )
{
printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
break;
}
}
// Fra_ClassesPrint( p->pCla, 1 );
// Fra_ClassesSelectRepr( p->pCla );
// check implications using simulation
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
int clk = clock();
if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
PRT( "Time", clock() - clk );
}
// move the classes into representatives and reduce AIG
clk2 = clock();
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig );
// add implications to the manager
if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
Fra_ImpRecordInManager( p, pManAigNew );
// cleanup the new manager
Aig_ManSeqCleanup( pManAigNew );
// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += clock() - clk2;
......
src/aig/fra/fraLcr.c 0 → 100644
/**CFile****************************************************************
FileName [fraLcorr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Latch correspondence computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Fra_Lcr_t_ Fra_Lcr_t;
struct Fra_Lcr_t_
{
// original AIG
Aig_Man_t * pAig;
// equivalence class representation
Fra_Cla_t * pCla;
// partitioning information
Vec_Ptr_t * vParts; // output partitions
int * pInToOutPart; // mapping of PI num into PO partition num
int * pInToOutNum; // mapping of PI num into the num of this PO in the partition
// AIGs for the partitions
Vec_Ptr_t * vFraigs;
// other variables
int fRefining;
// parameters
int nFramesP;
int fVerbose;
// statistics
int nIters;
int nLitsBeg;
int nLitsEnd;
int nNodesBeg;
int nNodesEnd;
int nRegsBeg;
int nRegsEnd;
// runtime
int timeSim;
int timePart;
int timeTrav;
int timeFraig;
int timeUpdate;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates the retiming manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
{
Fra_Lcr_t * p;
p = ALLOC( Fra_Lcr_t, 1 );
memset( p, 0, sizeof(Fra_Lcr_t) );
p->pAig = pAig;
p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
p->vFraigs = Vec_PtrAlloc( 1000 );
return p;
}
/**Function*************************************************************
Synopsis [Prints stats for the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lcr_ManPrint( Fra_Lcr_t * p )
{
printf( "Iterations = %d. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG partitioning", p->timePart );
PRT( "AIG rebuiding ", p->timeTrav );
PRT( "FRAIGing ", p->timeFraig );
PRT( "AIG updating ", p->timeUpdate );
PRT( "TOTAL RUNTIME ", p->timeTotal );
}
/**Function*************************************************************
Synopsis [Deallocates the retiming manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lcr_ManFree( Fra_Lcr_t * p )
{
Aig_Obj_t * pObj;
int i;
if ( p->fVerbose )
Lcr_ManPrint( p );
Aig_ManForEachPi( p->pAig, pObj, i )
pObj->pNext = NULL;
Vec_PtrFree( p->vFraigs );
if ( p->pCla ) Fra_ClassesStop( p->pCla );
if ( p->vParts ) Vec_VecFree( (Vec_Vec_t *)p->vParts );
free( p->pInToOutPart );
free( p->pInToOutNum );
free( p );
}
/**Function*************************************************************
Synopsis [Prepare the AIG for class computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
{
Fra_Man_t * p;
Aig_Obj_t * pObj;
int i;
p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = p;
return p;
}
/**Function*************************************************************
Synopsis [Prepare the AIG for class computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
Aig_ManForEachPi( pAig, pObj, i )
pObj->pData = p;
}
/**Function*************************************************************
Synopsis [Compares two nodes for equivalence after partitioned fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
Fra_Man_t * pTemp = pObj0->pData;
Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
Aig_Man_t * pFraig;
Aig_Obj_t * pOut0, * pOut1;
int nPart0, nPart1;
assert( Aig_ObjIsPi(pObj0) );
assert( Aig_ObjIsPi(pObj1) );
// find the partition to which these nodes belong
nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext];
nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext];
// if this is the result of refinement of the class created const-1 nodes
// the nodes may end up in different partions - we assume them equivalent
if ( nPart0 != nPart1 )
{
assert( 0 );
return 1;
}
assert( nPart0 == nPart1 );
pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
// get the fraig outputs
pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] );
pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] );
return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
}
/**Function*************************************************************
Synopsis [Compares the node with a constant after partioned fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
{
Fra_Man_t * pTemp = pObj->pData;
Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
Aig_Man_t * pFraig;
Aig_Obj_t * pOut;
int nPart;
assert( Aig_ObjIsPi(pObj) );
// find the partition to which these nodes belong
nPart = pLcr->pInToOutPart[(int)pObj->pNext];
pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
// get the fraig outputs
pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] );
return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
}
/**Function*************************************************************
Synopsis [Give the AIG and classes, reduces AIG for partitioning.]
Description [Ignores registers that are not in the classes.
Places candidate equivalent classes of registers into single outputs
(for ease of partitioning). The resulting combinational AIG contains
outputs in the same order as equivalence classes of registers,
followed by constant-1 registers. Preserves the set of all inputs.
Complemented attributes of the outputs do not matter because we need
then only for collecting the structural info.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
int i, c, Offset;
// remember the numbers of the inputs of the original AIG
Aig_ManForEachPi( pLcr->pAig, pObj, i )
{
pObj->pData = pLcr;
pObj->pNext = (Aig_Obj_t *)i;
}
// compute the LO/LI offset
Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
// create the PIs
Aig_ManCleanData( pLcr->pAig );
pNew = Aig_ManStartFrom( pLcr->pAig );
// go over the equivalence classes
Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
{
pMiter = Aig_ManConst0(pNew);
for ( c = 0; ppClass[c]; c++ )
{
assert( Aig_ObjIsPi(ppClass[c]) );
pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext );
pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
pMiter = Aig_Exor( pNew, pMiter, pObjNew );
}
Aig_ObjCreatePo( pNew, pMiter );
}
// go over the constant candidates
Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
{
assert( Aig_ObjIsPi(pObj) );
pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext );
pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
Aig_ObjCreatePo( pNew, pMiter );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Remaps partitions into the inputs of original AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum )
{
Vec_Int_t * vOne, * vOneNew;
Aig_Obj_t ** ppClass, * pObjPi;
int Out, Offset, i, k, c;
// compute the LO/LI offset
Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
Vec_PtrForEachEntry( vParts, vOne, i )
{
vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
Vec_IntForEachEntry( vOne, Out, k )
{
if ( Out < Vec_PtrSize(pCla->vClasses) )
{
ppClass = Vec_PtrEntry( pCla->vClasses, Out );
for ( c = 0; ppClass[c]; c++ )
{
pInToOutPart[(int)ppClass[c]->pNext] = i;
pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext );
}
}
else
{
pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
pInToOutPart[(int)pObjPi->pNext] = i;
pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew);
Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext );
}
}
// replace the class
Vec_PtrWriteEntry( vParts, i, vOneNew );
Vec_IntFree( vOne );
}
}
/**Function*************************************************************
Synopsis [Creates AIG of one partition with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return pObj->pData;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsPi(pObj) )
{
// Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
if ( pRepr == NULL )
pObj->pData = Aig_ObjCreatePi( pNew );
else
{
pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
}
return pObj->pData;
}
Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
/**Function*************************************************************
Synopsis [Creates AIG of one partition with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int Out, i;
// create new AIG for this partition
pNew = Aig_ManStartFrom( p->pAig );
Aig_ManIncrementTravId( p->pAig );
Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
Vec_IntForEachEntry( vPart, Out, i )
{
pObj = Aig_ManPo( p->pAig, Out );
if ( pObj->fMarkA )
{
pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
}
else
pObjNew = Aig_ManConst1( pNew );
Aig_ObjCreatePo( pNew, pObjNew );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Marks the nodes belonging to the equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassNodesMark( Fra_Lcr_t * p )
{
Aig_Obj_t * pObj, ** ppClass;
int i, c, Offset;
// compute the LO/LI offset
Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
// mark the nodes remaining in the classes
Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
{
pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
pObj->fMarkA = 1;
}
Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
{
for ( c = 0; ppClass[c]; c++ )
{
pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
pObj->fMarkA = 1;
}
}
}
/**Function*************************************************************
Synopsis [Unmarks the nodes belonging to the equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
{
Aig_Obj_t * pObj, ** ppClass;
int i, c, Offset;
// compute the LO/LI offset
Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
// mark the nodes remaining in the classes
Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
{
pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
pObj->fMarkA = 0;
}
Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
{
for ( c = 0; ppClass[c]; c++ )
{
pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
pObj->fMarkA = 0;
}
}
}
/**Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
{
int nPartSize = 200;
int fReprSelect = 0;
Fra_Lcr_t * p;
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Vec_Int_t * vPart;
Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
int i, nIter, clk = clock(), clk2, clk3;
if ( Aig_ManNodeNum(pAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
return Aig_ManDup(pAig, 1);
}
assert( Aig_ManLatchNum(pAig) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
// start the manager
p = Lcr_ManAlloc( pAig );
p->nFramesP = nFramesP;
p->fVerbose = fVerbose;
// simulate the AIG
clk2 = clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
pTemp = Fra_LcrAigPrepare( p->pAig );
pTemp->pBmc = (Fra_Bmc_t *)p;
pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 );
if ( fVerbose )
{
PRT( "Time", clock() - clk2 );
p->timeSim += clock() - clk2;
}
// get preliminary info about equivalence classes
pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
Fra_ClassesPrepare( p->pCla, 1 );
p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
Fra_SmlStop( pTemp->pSml );
// partition the AIG for latch correspondence computation
clk2 = clock();
if ( fVerbose )
printf( "Partitioning AIG ... " );
pAigPart = Fra_LcrDeriveAigForPartitioning( p );
p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
Aig_ManStop( pAigPart );
if ( fVerbose )
{
PRT( "Time", clock() - clk2 );
p->timePart += clock() - clk2;
}
// get the initial stats
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(p->pAig);
p->nRegsBeg = Aig_ManRegNum(p->pAig);
// perforn interative reduction of the partitions
p->fRefining = 1;
for ( nIter = 0; p->fRefining; nIter++ )
{
p->fRefining = 0;
clk3 = clock();
// derive AIGs for each partition
Fra_ClassNodesMark( p );
Vec_PtrClear( p->vFraigs );
Vec_PtrForEachEntry( p->vParts, vPart, i )
{
clk2 = clock();
pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += clock() - clk2;
clk2 = clock();
pAigNew = Fra_FraigEquivence( pAigPart, nConfMax );
p->timeFraig += clock() - clk2;
Vec_PtrPush( p->vFraigs, pAigNew );
Aig_ManStop( pAigPart );
}
Fra_ClassNodesUnmark( p );
// report the intermediate results
if ( fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. Part = %3d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
PRT( "T", clock() - clk3 );
}
// refine the classes
Fra_LcrAigPrepareTwo( p->pAig, pTemp );
if ( Fra_ClassesRefine( p->pCla ) )
p->fRefining = 1;
if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
p->fRefining = 1;
// clean the fraigs
Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
Aig_ManStop( pAigPart );
// repartition if needed
if ( 1 )
{
clk2 = clock();
Vec_VecFree( (Vec_Vec_t *)p->vParts );
pAigPart = Fra_LcrDeriveAigForPartitioning( p );
p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
Aig_ManStop( pAigPart );
p->timePart += clock() - clk2;
}
}
free( pTemp );
p->nIters = nIter;
// move the classes into representatives and reduce AIG
clk2 = clock();
// Fra_ClassesPrint( p->pCla, 1 );
if ( fReprSelect )
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, NULL );
pAigNew = Aig_ManDupRepr( p->pAig );
Aig_ManSeqCleanup( pAigNew );
// Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += clock() - clk2;
p->timeTotal = clock() - clk;
// get the final stats
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pAigNew);
p->nRegsEnd = Aig_ManRegNum(pAigNew);
Lcr_ManFree( p );
if ( pnIter ) *pnIter = nIter;
return pAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/fra/fraMan.c
......@@ -181,6 +181,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
assert( p->pManFraig == NULL );
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
pManFraig->nRegs = p->pManAig->nRegs;
pManFraig->nAsserts = p->pManAig->nAsserts;
// set the pointers to the available fraig nodes
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
Aig_ManForEachPi( p->pManAig, pObj, i )
......@@ -271,9 +273,9 @@ void Fra_ManPrint( Fra_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
......
src/aig/fra/fraSec.c
......@@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
......@@ -48,7 +48,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
}
else
{
......@@ -56,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
......@@ -89,6 +89,136 @@ PRT( "Time", clock() - clkTotal );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
pNew = Aig_ManDup( p, 1 );
if ( fVerbose )
{
printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
}
//Aig_ManDumpBlif( pNew, "after.blif" );
// perform sequential cleanup
clk = clock();
pNew = Aig_ManReduceLaches( pNew, 0 );
pNew = Aig_ManConstReduce( pNew, 0 );
if ( fVerbose )
{
printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
// perform forward retiming
if ( fRetimeFirst )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
}
// run latch correspondence
clk = clock();
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
// perform fraiging
clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 1000 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
// perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue == -1 )
for ( nFrames = 1; ; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
break;
// perform rewriting
clk = clock();
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Dar_ManRewriteDefault( pTemp = pNew );
if ( fVerbose )
{
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
// perform retiming
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
Aig_ManStop( pTemp );
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
}
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
Aig_ManStop( pNew );
// report the miter
if ( RetValue == 1 )
printf( "Networks are equivalent. " );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT. " );
else
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fraSim.c
......@@ -199,7 +199,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
Aig_ManForEachPi( p->pManFraig, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
Aig_InfoSetBit( p->pPatWords, i );
/*
if ( p->vCex )
{
Vec_IntClear( p->vCex );
......@@ -208,7 +208,6 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
}
*/
/*
printf( "Pattern: " );
......@@ -608,7 +607,7 @@ void Fra_SmlResimulate( Fra_Man_t * p )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
if ( p->pCla->vImps )
nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
p->timeRef += clock() - clk;
......@@ -652,7 +651,7 @@ printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
......@@ -663,7 +662,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
......@@ -677,7 +676,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
p->timeRef += clock() - clk;
if ( fVerbose )
printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
......@@ -704,7 +703,6 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
Fra_Sml_t * p;
assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
p->pAig = pAig;
......
src/aig/fra/module.make
......@@ -5,6 +5,7 @@ SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
......
src/base/abc/abc.h
......@@ -869,6 +869,7 @@ extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFree
extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
extern void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
......
src/base/abc/abcUtil.c
......@@ -148,6 +148,33 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
/**Function*************************************************************
Synopsis [Reads the number of cubes of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
int i, nCubes, nCubePairs = 0;
assert( Abc_NtkHasSop(pNtk) );
Abc_NtkForEachNode( pNtk, pNode, i )
{
if ( Abc_NodeIsConst(pNode) )
continue;
assert( pNode->pData );
nCubes = Abc_SopGetCubeNum( pNode->pData );
nCubePairs += nCubes * (nCubes - 1) / 2;
}
return nCubePairs;
}
/**Function*************************************************************
Synopsis [Reads the number of literals in the SOPs of the nodes.]
Description []
......
src/base/abci/abc.c
......@@ -123,6 +123,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -166,6 +167,7 @@ static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -326,12 +328,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
......@@ -339,6 +340,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", "dprove", Abc_CommandDProve, 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 );
......@@ -2588,22 +2590,34 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
p = ALLOC( Fxu_Data_t, 1 );
memset( p, 0, sizeof(Fxu_Data_t) );
// set the defaults
p->nPairsMax = 30000;
p->nNodesExt = 10000;
p->fOnlyS = 0;
p->fOnlyD = 0;
p->fUse0 = 0;
p->fUseCompl = 1;
p->fVerbose = 0;
p->nSingleMax = 20000;
p->nPairsMax = 30000;
p->nNodesExt = 10000;
p->fOnlyS = 0;
p->fOnlyD = 0;
p->fUse0 = 0;
p->fUseCompl = 1;
p->fVerbose = 0;
Extra_UtilGetoptReset();
while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF )
while ( (c = Extra_UtilGetopt(argc, argv, "SDNsdzcvh")) != EOF )
{
switch (c)
{
case 'L':
case 'S':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
p->nSingleMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( p->nSingleMax < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
p->nPairsMax = atoi(argv[globalUtilOptind]);
......@@ -2643,7 +2657,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
default:
goto usage;
}
}
}
if ( pNtk == NULL )
{
......@@ -2673,10 +2687,11 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n");
fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
fprintf( pErr, "\t performs unate fast extract on the current network\n");
fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );
fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );
fprintf( pErr, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
fprintf( pErr, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
......@@ -6175,7 +6190,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nLevels = 128;
nLevels = 1000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
{
......@@ -6293,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 );
pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -8674,7 +8689,7 @@ int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
......@@ -10975,12 +10990,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFramesP;
int nFramesK;
int nMaxImps;
int fExdc;
int fUseImps;
int fRewrite;
int fLatchCorr;
int fWriteImps;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -10990,13 +11005,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
nFramesP = 0;
nFramesK = 1;
nMaxImps = 5000;
fExdc = 1;
fUseImps = 0;
fRewrite = 0;
fLatchCorr = 0;
fWriteImps = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PFIirlevh" ) ) != EOF )
{
switch ( c )
{
......@@ -11033,9 +11048,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nMaxImps <= 0 )
goto usage;
break;
case 'e':
fExdc ^= 1;
break;
case 'i':
fUseImps ^= 1;
break;
......@@ -11045,6 +11057,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
fLatchCorr ^= 1;
break;
case 'e':
fWriteImps ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -11069,12 +11084,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Sequential sweep works only for structurally hashed networks (run \"strash\").\n" );
return 1;
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
// get the new network
pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose );
pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
......@@ -11085,15 +11100,120 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" );
fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "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-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nFramesP;
int nConfMax;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFramesP = 0;
nConfMax = 10000;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
{
switch ( c )
{
case 'P':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
nFramesP = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesP < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
// get the new network
pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
fprintf( pErr, "\t computes latch correspondence using 1-step induction\n" );
fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -11113,12 +11233,12 @@ usage:
int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes, * pTemp;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fLatchSweep;
int fAutoSweep;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -11153,23 +11273,13 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) )
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for logic networks.\n" );
fprintf( pErr, "Only works for structrally hashed networks.\n" );
return 1;
}
// modify the current network
// 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 );
}
pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential cleanup has failed.\n" );
......@@ -11180,14 +11290,14 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: scleanup [-lavh]\n" );
fprintf( pErr, "usage: scleanup [-lvh]\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 stuck-at and identical latches (latch sweep)\n" );
fprintf( pErr, "\t - replaces autonomous logic by free PI variables\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" );
fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -11291,9 +11401,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int nFrames;
int fInputs;
int fXInputs;
int fXState;
int fVerbose;
extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -11301,10 +11412,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 10;
fInputs = 0;
fXInputs = 0;
fXState = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Fisvh" ) ) != EOF )
{
switch ( c )
{
......@@ -11320,7 +11432,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
break;
case 'i':
fInputs ^= 1;
fXInputs ^= 1;
break;
case 's':
fXState ^= 1;
break;
case 'v':
fVerbose ^= 1;
......@@ -11343,14 +11458,15 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
fprintf( pErr, "usage: xsim [-F num] [-isvh]\n" );
fprintf( pErr, "\t performs X-valued simulation of the AIG\n" );
fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
fprintf( pErr, "\t-i : toggle X-valued representation of inputs [default = %s]\n", fXInputs? "yes": "no" );
fprintf( pErr, "\t-s : toggle X-valued representation of state [default = %s]\n", fXState? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -11674,11 +11790,12 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
int fRetimeFirst;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose );
extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -11686,10 +11803,11 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 0; // if 0, iterates through frames
fVerbose = 1;
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -11704,6 +11822,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFrames <= 0 )
goto usage;
break;
case 'r':
fRetimeFirst ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
......@@ -11727,18 +11848,19 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform verification
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose );
Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, 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, "usage: dsec [-F num] [-rwvh] <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-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "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");
......@@ -11746,6 +11868,95 @@ usage:
fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fRetimeFirst;
int fVerbose;
int fVeryVerbose;
int nFrames;
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, 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
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != 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 'r':
fRetimeFirst ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
default:
goto usage;
}
}
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
printf( "The network has no latches. Used combinational command \"iprove\".\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
return 0;
}
// perform verification
Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
return 0;
usage:
fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
......
src/base/abci/abcDar.c
......@@ -122,6 +122,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj;
int i;
assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
......@@ -141,7 +142,19 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
{
if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
break;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
// if there are assertions, add them
if ( pMan->nAsserts > 0 )
Aig_ManForEachAssert( pMan, pObj, i )
{
pObjNew = Abc_NtkCreateAssert(pNtkNew);
Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
......@@ -194,7 +207,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Vec_PtrFree( vNodes );
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
{
if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
break;
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
// if there are assertions, add them
if ( pMan->nAsserts > 0 )
Aig_ManForEachAssert( pMan, pObj, i )
{
pObjNew = Abc_NtkCreateAssert(pNtkNew);
Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;
......@@ -892,7 +917,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
......@@ -916,7 +941,7 @@ PRT( "Initial fraiging time", clock() - clk );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
......@@ -929,6 +954,34 @@ PRT( "Initial fraiging time", clock() - clk );
/**Function*************************************************************
Synopsis [Computes latch correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
Aig_ManStop( pTemp );
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 []
......@@ -938,11 +991,40 @@ PRT( "Initial fraiging time", clock() - clk );
SeeAlso []
***********************************************************************/
int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose )
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Fraig_Params_t Params;
Aig_Man_t * pMan;
Abc_Ntk_t * pMiter, * pTemp;
int RetValue;
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return -1;
}
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return RetValue;
}
/**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 fRetimeFirst, 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
......@@ -971,6 +1053,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
return 1;
}
// commented out because something became non-inductive
/*
// 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
......@@ -978,7 +1062,25 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
Params.nBTLimit = 100000;
pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
Abc_NtkDelete( pTemp );
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;
}
*/
// derive the AIG manager
pMan = Abc_NtkToDar( pMiter, 1 );
Abc_NtkDelete( pMiter );
......@@ -990,7 +1092,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose );
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
Aig_ManStop( pMan );
return RetValue;
}
......@@ -1006,15 +1108,19 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose )
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, 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 );
Aig_ManSeqCleanup( pMan );
if ( fLatchSweep )
{
pMan = Aig_ManReduceLaches( pMan, fVerbose );
pMan = Aig_ManConstReduce( pMan, fVerbose );
}
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
......@@ -1038,6 +1144,8 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
// Aig_ManReduceLachesCount( pMan );
pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
Aig_ManStop( pTemp );
......
src/base/abci/abcPrint.c
......@@ -213,6 +213,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
printf( "Total nodes = %6d %6.2f Mb Changes = %6d.\n",
s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges );
*/
// if ( Abc_NtkHasSop(pNtk) )
// printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
}
/**Function*************************************************************
......
src/base/abci/abcStrash.c
......@@ -233,7 +233,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
// perform strashing
nNewCis = 0;
Abc_NtkCleanCopy( pNtk2 );
Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
if ( Abc_NtkIsStrash(pNtk2) )
Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
Abc_NtkForEachCi( pNtk2, pObj, i )
{
pName = Abc_ObjName(pObj);
......
src/base/abci/abcXsim.c
......@@ -103,7 +103,7 @@ static inline void Abc_XsimPrint( FILE * pFile, int Value )
SeeAlso []
***********************************************************************/
void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose )
{
Abc_Obj_t * pObj;
int i, f;
......@@ -111,20 +111,26 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
srand( 0x12341234 );
// start simulation
Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
if ( fInputs )
if ( fXInputs )
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, XVSX );
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
}
else
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
}
if ( fXState )
{
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
}
else
{
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
}
// simulate and print the result
fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
for ( f = 0; f < nFrames; f++ )
......@@ -147,14 +153,24 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
fprintf( stdout, " : " );
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
if ( Abc_NtkAssertNum(pNtk) )
{
fprintf( stdout, " : " );
Abc_NtkForEachAssert( pNtk, pObj, i )
Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
}
fprintf( stdout, "\n" );
// assign input values
if ( fInputs )
if ( fXInputs )
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, XVSX );
}
else
{
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
}
// transfer the latch values
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
......
src/opt/fxu/fxu.c
......@@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
Fxu_Single * pSingle;
Fxu_Double * pDouble;
int Weight1, Weight2, Weight3;
int Counter = 0;
s_MemoryTotal = 0;
s_MemoryPeak = 0;
......@@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
{
Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
if ( pData->fVerbose )
printf( "Best single = %3d.\n", Weight1 );
printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
Fxu_UpdateSingle( p );
else
......@@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
{
Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
if ( pData->fVerbose )
printf( "Best double = %3d.\n", Weight2 );
printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
Fxu_UpdateDouble( p );
else
......@@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
if ( pData->fVerbose )
printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 );
printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
//Fxu_Select( p, &pSingle, &pDouble );
if ( Weight1 >= Weight2 )
......@@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
// select the best single and double
Weight3 = Fxu_Select( p, &pSingle, &pDouble );
if ( pData->fVerbose )
printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n",
Weight2, Weight1, Weight3 );
printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r",
Counter++, Weight2, Weight1, Weight3 );
if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
Fxu_Update( p, pSingle, pDouble );
......@@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
}
if ( pData->fVerbose )
printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 );
printf( "Total single = %3d. Total double = %3d. Total compl = %3d. \n",
p->nDivs1, p->nDivs2, p->nDivs3 );
// create the new covers
if ( pData->nNodesNew )
......
src/opt/fxu/fxu.h
......@@ -55,7 +55,8 @@ struct FxuDataStruct
bool fUseCompl; // set to 1 to have complement taken into account
bool fVerbose; // set to 1 to have verbose output
int nNodesExt; // the number of divisors to extract
int nPairsMax; // the maximum number of cube pairs to consider
int nSingleMax; // the max number of single-cube divisors to consider
int nPairsMax; // the max number of double-cube divisors to consider
// the input information
Vec_Ptr_t * vSops; // the SOPs for each node in the network
Vec_Ptr_t * vFanins; // the fanins of each node in the network
......
src/opt/fxu/fxuCreate.c
......@@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
// consider the case when cube pairs should be preprocessed
// before adding them to the set of divisors
// if ( pData->fVerbose )
// printf( "The total number of cube pairs is %d.\n", nPairsTotal );
if ( nPairsTotal > 10000000 )
{
printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
printf( "that the user changes the network by reducing the size of logic node and\n" );
printf( "consequently the number of cube pairs to be processed by this command.\n" );
printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
return NULL;
}
if ( nPairsTotal > pData->nPairsMax )
if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
return NULL;
// if ( pData->fVerbose )
// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
// add the var pairs to the heap
Fxu_MatrixComputeSingles( p );
Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
// print stats
if ( pData->fVerbose )
......@@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
p->lVars.nItems, p->lCubes.nItems );
fprintf( stdout, "Lits = %d Density = %.5f%%\n",
p->nEntries, Density );
fprintf( stdout, "1-cube divisors = %6d. ", p->lSingles.nItems );
fprintf( stdout, "2-cube divisors = %6d. ", p->nDivsTotal );
fprintf( stdout, "Cube pairs = %6d.", nPairsTotal );
fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal );
fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal );
fprintf( stdout, "\n" );
}
// Fxu_MatrixPrint( stdout, p );
......
src/opt/fxu/fxuInt.h
......@@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words
// the single cube divisors
Fxu_ListSingle lSingles; // the linked list of single cube divisors
Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
int nWeightLimit;// the limit on weight of single cube divisors collected
int nSingleTotal;// the total number of single cube divisors
// storage for cube pairs
Fxu_Pair *** pppPairs;
Fxu_Pair ** ppPairs;
......@@ -459,7 +461,7 @@ extern void Fxu_PairClearStorage( Fxu_Cube * pCube );
extern Fxu_Pair * Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
extern void Fxu_PairAdd( Fxu_Pair * pPair );
/*===== fxuSingle.c ====================================================*/
extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p );
extern void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
extern void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
extern int Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
/*===== fxuMatrix.c ====================================================*/
......
src/opt/fxu/fxuSingle.c
......@@ -17,11 +17,14 @@
***********************************************************************/
#include "fxuInt.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -38,12 +41,130 @@
SeeAlso []
***********************************************************************/
void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
{
Fxu_Var * pVar;
// iterate through the columns in the matrix
Vec_Ptr_t * vSingles;
int i, k;
// set the weight limit
p->nWeightLimit = 1 - fUse0;
// iterate through columns in the matrix and collect single-cube divisors
vSingles = Vec_PtrAlloc( 10000 );
Fxu_MatrixForEachVariable( p, pVar )
Fxu_MatrixComputeSinglesOne( p, pVar );
Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
// check if divisors should be filtered
if ( Vec_PtrSize(vSingles) > nSingleMax )
{
int * pWeigtCounts, nDivCount, Weight, i, c;;
assert( Vec_PtrSize(vSingles) % 3 == 0 );
// count how many divisors have the given weight
pWeigtCounts = ALLOC( int, 1000 );
memset( pWeigtCounts, 0, sizeof(int) * 1000 );
for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
{
Weight = (int)Vec_PtrEntry(vSingles, i);
if ( Weight >= 999 )
pWeigtCounts[999]++;
else
pWeigtCounts[Weight]++;
}
// select the bound on the weight (above this bound, singles will be included)
nDivCount = 0;
for ( c = 999; c >= 0; c-- )
{
nDivCount += pWeigtCounts[c];
if ( nDivCount >= nSingleMax )
break;
}
free( pWeigtCounts );
// collect singles with the given costs
k = 0;
for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
{
Weight = (int)Vec_PtrEntry(vSingles, i);
if ( Weight < c )
continue;
Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
if ( k/3 == nSingleMax )
break;
}
Vec_PtrShrink( vSingles, k );
// adjust the weight limit
p->nWeightLimit = c;
}
// collect the selected divisors
assert( Vec_PtrSize(vSingles) % 3 == 0 );
for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
{
Fxu_MatrixAddSingle( p,
Vec_PtrEntry(vSingles,i),
Vec_PtrEntry(vSingles,i+1),
(int)Vec_PtrEntry(vSingles,i+2) );
}
Vec_PtrFree( vSingles );
}
/**Function*************************************************************
Synopsis [Adds the single-cube divisors associated with a new column.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles )
{
Fxu_Lit * pLitV, * pLitH;
Fxu_Var * pVar2;
int Coin;
int WeightCur;
// start collecting the affected vars
Fxu_MatrixRingVarsStart( p );
// go through all the literals of this variable
for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
// for this literal, go through all the horizontal literals
for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
{
// get another variable
pVar2 = pLitH->pVar;
// skip the var if it is already used
if ( pVar2->pOrder )
continue;
// skip the var if it belongs to the same node
// if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
// continue;
// collect the var
Fxu_MatrixRingVarsAdd( p, pVar2 );
}
// stop collecting the selected vars
Fxu_MatrixRingVarsStop( p );
// iterate through the selected vars
Fxu_MatrixForEachVarInRing( p, pVar2 )
{
// count the coincidence
Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
assert( Coin > 0 );
// get the new weight
WeightCur = Coin - 2;
// peformance fix (August 24, 2007)
if ( WeightCur >= p->nWeightLimit )
{
Vec_PtrPush( vSingles, pVar2 );
Vec_PtrPush( vSingles, pVar );
Vec_PtrPush( vSingles, (void *)WeightCur );
}
}
// unmark the vars
Fxu_MatrixRingVarsUnmark( p );
}
/**Function*************************************************************
......@@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
***********************************************************************/
void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
{
// int * pValue2Node = p->pValue2Node;
Fxu_Lit * pLitV, * pLitH;
Fxu_Var * pVar2;
int Coin;
// int CounterAll;
// int CounterTest;
int WeightCur;
// start collecting the affected vars
......@@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
{
// get another variable
pVar2 = pLitH->pVar;
// CounterAll++;
// skip the var if it is already used
if ( pVar2->pOrder )
continue;
......@@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
// iterate through the selected vars
Fxu_MatrixForEachVarInRing( p, pVar2 )
{
// CounterTest++;
// count the coincidence
Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
assert( Coin > 0 );
// get the new weight
WeightCur = Coin - 2;
if ( WeightCur >= 0 )
// peformance fix (August 24, 2007)
// if ( WeightCur >= 0 )
// Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
if ( WeightCur >= p->nWeightLimit )
Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
}
// unmark the vars
Fxu_MatrixRingVarsUnmark( p );
}
......
src/opt/fxu/fxuUpdate.c
......@@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
{
Fxu_Single * pSingle, * pSingle2;
int WeightNew;
int Counter = 0;
Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
{
// if at least one of the variables is marked, recalculate
if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
{
Counter++;
// get the new weight
WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
if ( WeightNew >= 0 )
......@@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
}
}
}
// printf( "Called procedure %d times.\n", Counter );
}
/**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment