Skip to content

A
abc
Commit de81a1a1 by Alan Mishchenko
Options

Version abc80430

parent 2b98b818
Showing with 2094 additions and 62 deletions
abc.dsp
......@@ -342,6 +342,10 @@ SOURCE=.\src\base\abci\abcQuant.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcReach.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcRec.c
# End Source File
# Begin Source File
......@@ -2034,6 +2038,10 @@ SOURCE=.\src\misc\extra\extraBddCas.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraBddImage.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraBddKmap.c
# End Source File
# Begin Source File
......@@ -3250,8 +3258,16 @@ SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigRetFwd.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigRetMin.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigScl.c
# End Source File
# End Group
# End Group
# End Group
......
abc.rc
......@@ -120,7 +120,7 @@ alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
# temporaries
alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
alias reachable "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
alias chnew "st; haig_start; resyn2; haig_use"
alias chnewrs "st; haig_start; resyn2rs; haig_use"
alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
......
src/aig/aig/aigMan.c
......@@ -350,10 +350,10 @@ void Aig_ManPrintStats( Aig_Man_t * p )
***********************************************************************/
void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
{
printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%). ",
printf( "REG: Beg = %5d. End = %5d. (R =%5.1f %%) ",
Aig_ManRegNum(p), Aig_ManRegNum(pNew),
Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 );
printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).",
printf( "AND: Beg = %6d. End = %6d. (R =%5.1f %%)",
Aig_ManNodeNum(p), Aig_ManNodeNum(pNew),
Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 );
printf( "\n" );
......
src/aig/aig/aigScl.c
......@@ -451,27 +451,17 @@ 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( "Performing combinational register sweep:\n" );
for ( nSaved = 0; (nCur = Aig_ManReduceLachesCount(p)); nSaved += nCur )
{
printf( "Saved = %5d. ", nCur );
printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
}
vMap = Aig_ManReduceLachesOnce( p );
//Aig_ManPrintStats( p );
p = Aig_ManRemap( pTemp = p, vMap );
//Aig_ManPrintStats( p );
Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
//Aig_ManPrintStats( p );
//printf( "\n" );
if ( fVerbose )
{
printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
printf( "\n" );
}
Aig_ManReportImprovement( pTemp, p );
Aig_ManStop( pTemp );
if ( p->nRegs == 0 )
break;
}
......@@ -600,6 +590,8 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
***********************************************************************/
Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
{
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
Aig_Man_t * pAigInit, * pAigNew;
Aig_Obj_t * pFlop1, * pFlop2;
int i, Entry1, Entry2, nTruePis;
......@@ -633,6 +625,8 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
// Aig_ManSeqCleanup( pAigInit );
pAigNew = Aig_ManDupRepr( pAigInit, 0 );
Aig_ManSeqCleanup( pAigNew );
Saig_ManReportUselessRegisters( pAigNew );
return pAigNew;
}
......
src/aig/aig/aigTsim.c
......@@ -479,14 +479,12 @@ Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
Vec_Ptr_t * vMap;
while ( (vMap = Aig_ManTernarySimulate( p, fVerbose )) )
{
if ( fVerbose )
printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
p = Aig_ManRemap( pTemp = p, vMap );
Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
if ( fVerbose )
printf( "REnd = %5d. NEnd = %6d. \n", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
Aig_ManReportImprovement( pTemp, p );
Aig_ManStop( pTemp );
}
return p;
}
......
src/aig/mfx/mfxCore.c
......@@ -245,7 +245,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
p->nFaninMax = nFaninMax;
if ( !pPars->fResub )
{
pDecPars->nVarsMax = nFaninMax;
pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
......
src/aig/saig/module.make
SRC += src/aig/saig/saig_.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetMin.c
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
src/aig/saig/saigScl.c
src/aig/saig/saig.h
......@@ -49,6 +49,11 @@ static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->n
static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); }
static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); }
static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); }
static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); }
static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); }
static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
// iterator over the primary inputs/outputs
#define Saig_ManForEachPi( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) )
......@@ -69,6 +74,14 @@ static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig
////////////////////////////////////////////////////////////////////////
/*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/
extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
/*=== saigRetMin.c ==========================================================*/
extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
#ifdef __cplusplus
}
......
src/aig/saig/saigRetFwd.c 0 → 100644
/**CFile****************************************************************
FileName [saigRetFwd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Most-forward retiming.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigRetFwd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Aig_ObjFanoutStatic( Aig_Obj_t * pObj, int i ) { return ((Aig_Obj_t **)pObj->pData)[i]; }
static inline void Aig_ObjSetFanoutStatic( Aig_Obj_t * pObj, Aig_Obj_t * pFan ) { ((Aig_Obj_t **)pObj->pData)[pObj->nRefs++] = pFan; }
#define Aig_ObjForEachFanoutStatic( pObj, pFan, i ) \
for ( i = 0; (i < (int)(pObj)->nRefs) && ((pFan) = Aig_ObjFanoutStatic(pObj, i)); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocate static fanout for all nodes in the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p )
{
Aig_Obj_t ** ppFanouts, * pObj;
int i, nFanouts, nFanoutsAlloc;
// allocate fanouts
nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p);
ppFanouts = ALLOC( Aig_Obj_t *, nFanoutsAlloc );
// mark up storage
nFanouts = 0;
Aig_ManForEachObj( p, pObj, i )
{
pObj->pData = ppFanouts + nFanouts;
nFanouts += pObj->nRefs;
pObj->nRefs = 0;
}
assert( nFanouts < nFanoutsAlloc );
// add fanouts
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjChild0(pObj) )
Aig_ObjSetFanoutStatic( Aig_ObjFanin0(pObj), pObj );
if ( Aig_ObjChild1(pObj) )
Aig_ObjSetFanoutStatic( Aig_ObjFanin1(pObj), pObj );
}
return ppFanouts;
}
/**Function*************************************************************
Synopsis [Marks the objects reachable from the given object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManMarkAutonomous_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanout;
int i;
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
Aig_ObjForEachFanoutStatic( pObj, pFanout, i )
Aig_ManMarkAutonomous_rec( p, pFanout );
}
/**Function*************************************************************
Synopsis [Marks with current trav ID nodes reachable from Const1 and PIs.]
Description [Returns the number of unreachable registers.]
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManMarkAutonomous( Aig_Man_t * p )
{
Aig_Obj_t ** ppFanouts;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i;
// temporarily connect register outputs to register inputs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{
pObjLo->pFanin0 = pObjLi;
pObjLi->nRefs = 1;
}
// mark nodes reachable from Const1 and PIs
Aig_ManIncrementTravId( p );
ppFanouts = Aig_ManStaticFanoutStart( p );
Aig_ManMarkAutonomous_rec( p, Aig_ManConst1(p) );
Saig_ManForEachPi( p, pObj, i )
Aig_ManMarkAutonomous_rec( p, pObj );
free( ppFanouts );
// disconnect LIs/LOs and label unreachable registers
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{
assert( pObjLo->pFanin0 && pObjLi->nRefs == 1 );
pObjLo->pFanin0 = NULL;
pObjLi->nRefs = 0;
}
}
/**Function*************************************************************
Synopsis [Derives the cut for forward retiming.]
Description [Assumes topological ordering of the nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManRetimeForwardOne( Aig_Man_t * p, int * pnRegFixed, int * pnRegMoves )
{
Aig_Man_t * pNew;
Vec_Ptr_t * vCut;
Aig_Obj_t * pObj, * pFanin;
int i;
// mark the retimable nodes
Saig_ManMarkAutonomous( p );
// mark the retimable registers with the fresh trav ID
Aig_ManIncrementTravId( p );
*pnRegFixed = 0;
Saig_ManForEachLo( p, pObj, i )
if ( Aig_ObjIsTravIdPrevious(p, pObj) )
Aig_ObjSetTravIdCurrent(p, pObj);
else
(*pnRegFixed)++;
// mark all the nodes that can be retimed forward
*pnRegMoves = 0;
Aig_ManForEachNode( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin0(pObj)) && Aig_ObjIsTravIdCurrent(p, Aig_ObjFanin1(pObj)) )
{
Aig_ObjSetTravIdCurrent(p, pObj);
(*pnRegMoves)++;
}
// mark the remaining registers
Saig_ManForEachLo( p, pObj, i )
Aig_ObjSetTravIdCurrent(p, pObj);
// find the cut (all such marked objects that fanout into unmarked nodes)
vCut = Vec_PtrAlloc( 1000 );
Aig_ManIncrementTravId( p );
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsTravIdPrevious(p, pObj) )
continue;
pFanin = Aig_ObjFanin0(pObj);
if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
{
Vec_PtrPush( vCut, pFanin );
Aig_ObjSetTravIdCurrent( p, pFanin );
}
pFanin = Aig_ObjFanin1(pObj);
if ( pFanin && Aig_ObjIsTravIdPrevious(p, pFanin) )
{
Vec_PtrPush( vCut, pFanin );
Aig_ObjSetTravIdCurrent( p, pFanin );
}
}
// finally derive the new manager
pNew = Saig_ManRetimeDupForward( p, vCut );
Vec_PtrFree( vCut );
return pNew;
}
/**Function*************************************************************
Synopsis [Derives the cut for forward retiming.]
Description [Assumes topological ordering of the nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose )
{
Aig_Man_t * pNew, * pTemp;
int i, clk, nRegFixed, nRegMoves = 1;
pNew = p;
for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
{
clk = clock();
pNew = Saig_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
if ( fVerbose )
{
printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ",
i + 1, Aig_ManNodeNum(pTemp), Aig_ManRegNum(pTemp), nRegFixed, nRegMoves );
PRT( "Time", clock() - clk );
}
if ( pTemp != p )
Aig_ManStop( pTemp );
}
clk = clock();
pNew = Aig_ManReduceLaches( pNew, fVerbose );
if ( fVerbose )
{
PRT( "Register sharing time", clock() - clk );
}
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/saig/saigRetMin.c
......@@ -617,16 +617,16 @@ Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{
Vec_Ptr_t * vCut;
Aig_Man_t * pNew, * pTemp, * pCopy;
int fChanges;
int i, fChanges;
pNew = Aig_ManDup( p );
// perform several iterations of forward retiming
fChanges = 0;
if ( !fBackwardOnly )
while ( 1 )
for ( i = 0; i < nMaxIters; i++ )
{
vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
......@@ -646,7 +646,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
// perform several iterations of backward retiming
fChanges = 0;
if ( !fForwardOnly && !fInitial )
while ( 1 )
for ( i = 0; i < nMaxIters; i++ )
{
vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
......@@ -664,7 +664,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwar
fChanges = 1;
}
else if ( !fForwardOnly && fInitial )
while ( 1 )
for ( i = 0; i < nMaxIters; i++ )
{
pCopy = Aig_ManDup( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
......
src/aig/saig/saigScl.c 0 → 100644
/**CFile****************************************************************
FileName [saigScl.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Sequential cleanup.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigScl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Report registers useless for SEC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj, * pDriver;
int i, Counter1, Counter2;
// set PIO numbers
Aig_ManSetPioNumbers( pAig );
// check how many POs are driven by a register whose ref count is 1
Counter1 = 0;
Saig_ManForEachPo( pAig, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
if ( Saig_ObjIsLo(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
Counter1++;
}
// check how many PIs have ref count 1 and drive a register
Counter2 = 0;
Saig_ManForEachLi( pAig, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
if ( Saig_ObjIsPi(pAig, pDriver) && Aig_ObjRefs(pDriver) == 1 )
Counter2++;
}
if ( Counter1 )
printf( "Network has %d (out of %d) registers driving POs.\n", Counter1, Saig_ManRegNum(pAig) );
if ( Counter2 )
printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
......@@ -98,6 +98,7 @@ static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -349,6 +350,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 );
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
Cmd_CommandAdd( pAbc, "Various", "reach", Abc_CommandReach, 0 );
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 );
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
......@@ -5605,6 +5607,116 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int nBddMax;
int nIterMax;
int fPartition;
int fReorder;
int fVerbose;
int c;
extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nBddMax = 50000;
nIterMax = 1000;
fPartition = 1;
fReorder = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
{
switch ( c )
{
case 'B':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
nBddMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBddMax < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nIterMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIterMax < 0 )
goto usage;
break;
case 'p':
fPartition ^= 1;
break;
case 'r':
fReorder ^= 1;
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_NtkLatchNum(pNtk) == 0 )
{
fprintf( stdout, "The current network has no latches.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( stdout, "Reachability analysis works only for AIGs (run \"strash\").\n" );
return 1;
}
if ( Abc_NtkPoNum(pNtk) != 1 )
{
fprintf( stdout, "The sequential miter has more than one output (run \"orpos\").\n" );
return 1;
}
Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
fprintf( pErr, "\t verifies sequential miter using BDD-based reachability\n" );
fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
fprintf( pErr, "\t-p : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
......@@ -11925,10 +12037,11 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int nStepsMax;
int fFastAlgo;
int fVerbose;
int c;
int c, nMaxIters;
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -11940,13 +12053,25 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
fBackwardOnly = 0;
fInitial = 1;
nStepsMax = 100000;
fFastAlgo = 1;
fFastAlgo = 0;
nMaxIters = 20;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbiavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NSmfbiavh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
goto usage;
}
nMaxIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nMaxIters < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
......@@ -12003,11 +12128,12 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform the retiming
if ( fMinArea )
pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
else if ( fFastAlgo )
pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
else
pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
// pNtkRes = Abc_NtkDarRetimeF( pNtk, nStepsMax, fVerbose );
pNtkRes = Abc_NtkDarRetimeMostFwd( pNtk, nMaxIters, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Retiming has failed.\n" );
......@@ -12018,12 +12144,13 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dretime [-S num] [-mfbiavh]\n" );
fprintf( pErr, "\t new implementation of min-area retiming\n" );
fprintf( pErr, "\t-m : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
fprintf( pErr, "usage: dretime [-NS num] [-mfbiavh]\n" );
fprintf( pErr, "\t new implementation of min-area (or most-forward) retiming\n" );
fprintf( pErr, "\t-m : toggle min-area retiming and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" );
fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" );
fprintf( pErr, "\t-i : enables init state computation [default = %s]\n", fInitial? "yes": "no" );
fprintf( pErr, "\t-N num : the max number of one-frame iterations to perform [default = %d]\n", nMaxIters );
fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax );
fprintf( pErr, "\t-a : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
......
src/base/abci/abcDar.c
......@@ -1409,7 +1409,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
......@@ -1431,24 +1431,24 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
{
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
// pMan = Aig_ManConstReduce( pMan, 1 );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
......@@ -1465,8 +1465,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBa
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
{
extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
......@@ -1477,7 +1479,10 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
Aig_ManStop( pTemp );
// pMan = Aig_ManReduceLaches( pMan, 1 );
......@@ -1499,6 +1504,40 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
/*
......
src/base/abci/abcFpga.c
......@@ -201,7 +201,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
int i;//, nDupGates;
int i, nDupGates;
// create the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
// make the mapper point to the new network
......@@ -229,9 +229,9 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
Abc_NtkDeleteObj( pNodeNew );
// decouple the PO driver nodes to reduce the number of levels
// nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
// if ( nDupGates && Fpga_ManReadVerbose(pMan) )
// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
if ( nDupGates && Fpga_ManReadVerbose(pMan) )
printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
return pNtkNew;
}
......
src/base/abci/abcIf.c
......@@ -186,7 +186,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
Vec_Int_t * vCover;
int i;//, nDupGates;
int i, nDupGates;
// create the new network
if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
......@@ -223,9 +223,9 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
if ( pIfMan->pPars->fUseBdds )
Abc_NtkBddReorder( pNtkNew, 0 );
// decouple the PO driver nodes to reduce the number of levels
// nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
// if ( nDupGates && If_ManReadVerbose(pIfMan) )
// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
if ( nDupGates && pIfMan->pPars->fVerbose )
printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
return pNtkNew;
}
......
src/base/abci/abcReach.c 0 → 100644
/**CFile****************************************************************
FileName [abcReach.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Performs reachability analysis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the initial state and sets up the variable map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
{
DdNode ** pbVarsX, ** pbVarsY;
DdNode * bTemp, * bProd, * bVar;
Abc_Obj_t * pLatch;
int i;
// set the variable mapping for Cudd_bddVarMap()
pbVarsX = ALLOC( DdNode *, dd->size );
pbVarsY = ALLOC( DdNode *, dd->size );
bProd = b1; Cudd_Ref( bProd );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
// get the initial value of the latch
bVar = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar ); Cudd_Ref( bProd );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
FREE( pbVarsX );
FREE( pbVarsY );
Cudd_Deref( bProd );
return bProd;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
{
DdNode ** pbParts;
DdNode * bVar;
Abc_Obj_t * pNode;
int i;
// extand the BDD manager to represent NS variables
assert( dd->size == Abc_NtkCiNum(pNtk) );
Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
// enable reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
else
Cudd_AutodynDisable( dd );
// compute the transition relation
pbParts = ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] );
}
// free the global BDDs
Abc_NtkFreeGlobalBdds( pNtk, 0 );
// reorder and disable reordering
if ( fReorder )
{
if ( fVerbose )
fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
Cudd_AutodynDisable( dd );
if ( fVerbose )
fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
}
return pbParts;
}
/**Function*************************************************************
Synopsis [Computes the set of unreachable states.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
int fInternalReorder = 0;
Extra_ImageTree_t * pTree;
Extra_ImageTree2_t * pTree2;
DdNode * bReached, * bCubeCs;
DdNode * bCurrent, * bNext, * bTemp;
DdNode ** pbVarsY;
Abc_Obj_t * pLatch;
int i, nIters, nBddSize;
int nThreshold = 10000;
// collect the NS variables
// set the variable mapping for Cudd_bddVarMap()
pbVarsY = ALLOC( DdNode *, dd->size );
Abc_NtkForEachLatch( pNtk, pLatch, i )
pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
// start the image computation
bCubeCs = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) ); Cudd_Ref( bCubeCs );
if ( fPartition )
pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
else
pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
free( pbVarsY );
Cudd_RecursiveDeref( dd, bCubeCs );
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
for ( nIters = 1; nIters <= nIterMax; nIters++ )
{
// compute the next states
if ( fPartition )
bNext = Extra_bddImageCompute( pTree, bCurrent );
else
bNext = Extra_bddImageCompute2( pTree2, bCurrent );
Cudd_Ref( bNext );
Cudd_RecursiveDeref( dd, bCurrent );
// remap these states into the current state vars
bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext );
Cudd_RecursiveDeref( dd, bTemp );
// check if there are any new states
if ( Cudd_bddLeq( dd, bNext, bReached ) )
break;
// check the BDD size
nBddSize = Cudd_DagSize(bNext);
if ( nBddSize > nBddMax )
break;
// check the result
if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
{
printf( "The miter is proved REACHABLE in %d iterations. ", nIters );
Cudd_RecursiveDeref( dd, bReached );
bReached = NULL;
break;
}
// get the new states
bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// minimize the new states with the reached states
// bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
// Cudd_RecursiveDeref( dd, bTemp );
// add to the reached states
bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bNext );
if ( fVerbose )
fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
if ( fInternalReorder && fReorder && nBddSize > nThreshold )
{
if ( fVerbose )
fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
Cudd_AutodynDisable( dd );
if ( fVerbose )
fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
nThreshold *= 2;
}
if ( fVerbose )
fprintf( stdout, "\r" );
}
Cudd_RecursiveDeref( dd, bNext );
// undo the image tree
if ( fPartition )
Extra_bddImageTreeDelete( pTree );
else
Extra_bddImageTreeDelete2( pTree2 );
if ( bReached == NULL )
return NULL;
// report the stats
if ( fVerbose )
{
double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
else
fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
fflush( stdout );
}
//PRB( dd, bReached );
Cudd_Deref( bReached );
if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
printf( "The miter is proved unreachable in %d iteration. ", nIters );
return bReached;
}
/**Function*************************************************************
Synopsis [Performs reachability to see if any .]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
DdManager * dd;
DdNode ** pbParts;
DdNode * bOutput, * bReached, * bInitial;
int i, clk = clock();
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkPoNum(pNtk) == 1 );
assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
// compute the global BDDs of the latches
dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );
if ( dd == NULL )
{
printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
return;
}
if ( fVerbose )
printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// save the output BDD
bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
// create partitions
pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
// create the initial state and the variable map
bInitial = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose ); Cudd_Ref( bInitial );
// check the result
if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
printf( "The miter is proved REACHABLE in the initial state. " );
else
{
// compute the reachable states
bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
if ( bReached != NULL )
{
Cudd_Ref( bReached );
Cudd_RecursiveDeref( dd, bReached );
}
}
// cleanup
Cudd_RecursiveDeref( dd, bOutput );
Cudd_RecursiveDeref( dd, bInitial );
for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
Cudd_RecursiveDeref( dd, pbParts[i] );
free( pbParts );
Extra_StopManager( dd );
// report the runtime
PRT( "Time", clock() - clk );
fflush( stdout );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/module.make
......@@ -39,6 +39,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcQuant.c \
src/base/abci/abcRec.c \
src/base/abci/abcReconv.c \
src/base/abci/abcReach.c \
src/base/abci/abcRefactor.c \
src/base/abci/abcRenode.c \
src/base/abci/abcReorder.c \
......
src/bdd/cas/casCore.c
......@@ -52,7 +52,7 @@ DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestinatio
////////////////////////////////////////////////////////////////////////
#define PRD(p) printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 )
#define PRB(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
......
src/bdd/cas/casDec.c
......@@ -94,7 +94,7 @@ long s_EncComputeTime;
/// debugging macros ///
////////////////////////////////////////////////////////////////////////
#define PRB(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
#define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
......
src/misc/extra/extra.h
......@@ -118,6 +118,10 @@ typedef unsigned long long uint64;
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#endif
#ifndef PRB
#define PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
#endif
/*===========================================================================*/
/* Various Utilities */
/*===========================================================================*/
......@@ -162,6 +166,26 @@ extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** p
/* find the profile of a DD (the number of edges crossing each level) */
extern int Extra_ProfileWidth( DdManager * dd, DdNode * F, int * Profile, int CutLevel );
/*=== extraBddImage.c ================================================================*/
typedef struct Extra_ImageTree_t_ Extra_ImageTree_t;
extern Extra_ImageTree_t * Extra_bddImageStart(
DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
int nVars, DdNode ** pbVars, int fVerbose );
extern DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare );
extern void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree );
extern DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree );
typedef struct Extra_ImageTree2_t_ Extra_ImageTree2_t;
extern Extra_ImageTree2_t * Extra_bddImageStart2(
DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
int nVars, DdNode ** pbVars, int fVerbose );
extern DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare );
extern void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree );
extern DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree );
/*=== extraBddMisc.c ========================================================*/
extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
......@@ -190,6 +214,7 @@ extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars );
extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars );
extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F );
extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
/*=== extraBddKmap.c ================================================================*/
......
src/misc/extra/extraBddImage.c 0 → 100644
/**CFile****************************************************************
FileName [extraBddImage.c]
PackageName [extra]
Synopsis [Various reusable software utilities.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2003.]
Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "extra.h"
/*
The ideas implemented in this file are inspired by the paper:
Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple,
Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
Image Computation. ICCAD, 2001.
*/
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
typedef struct Extra_ImageNode_t_ Extra_ImageNode_t;
typedef struct Extra_ImagePart_t_ Extra_ImagePart_t;
typedef struct Extra_ImageVar_t_ Extra_ImageVar_t;
struct Extra_ImageTree_t_
{
Extra_ImageNode_t * pRoot; // the root of quantification tree
Extra_ImageNode_t * pCare; // the leaf node with the care set
DdNode * bCareSupp; // the cube to quantify from the care
int fVerbose; // the verbosity flag
int nNodesMax; // the max number of nodes in one iter
int nNodesMaxT; // the overall max number of nodes
int nIter; // the number of iterations with this tree
};
struct Extra_ImageNode_t_
{
DdManager * dd; // the manager
DdNode * bCube; // the cube to quantify
DdNode * bImage; // the partial image
Extra_ImageNode_t * pNode1; // the first branch
Extra_ImageNode_t * pNode2; // the second branch
Extra_ImagePart_t * pPart; // the partition (temporary)
};
struct Extra_ImagePart_t_
{
DdNode * bFunc; // the partition
DdNode * bSupp; // the support of this partition
int nNodes; // the number of BDD nodes
short nSupp; // the number of support variables
short iPart; // the number of this partition
};
struct Extra_ImageVar_t_
{
int iNum; // the BDD index of this variable
DdNode * bParts; // the partition numbers
int nParts; // the number of partitions
};
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
int nParts, DdNode ** pbParts, DdNode * bCare );
static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
int nParts, Extra_ImagePart_t ** pParts,
int nVars, DdNode ** pbVarsNs );
static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
int nParts, Extra_ImagePart_t ** pParts,
int nVars, Extra_ImageVar_t ** pVars );
static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
static int Extra_BuildTreeNode( DdManager * dd,
int nNodes, Extra_ImageNode_t ** pNodes,
int nVars, Extra_ImageVar_t ** pVars );
static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd,
int nNodes, Extra_ImageNode_t ** pNodes );
static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
static int Extra_FindBestVariable( DdManager * dd,
int nNodes, Extra_ImageNode_t ** pNodes,
int nVars, Extra_ImageVar_t ** pVars );
static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
int nNodes, Extra_ImageNode_t ** pNodes,
int * piNode1, int * piNode2 );
static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
int nVars, DdNode ** pbVars );
static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function*************************************************************
Synopsis [Starts the image computation using tree-based scheduling.]
Description [This procedure starts the image computation. It uses
the given care set to test-run the image computation and creates the
quantification tree by scheduling variable quantifications. The tree can
be used to compute images for other care sets without rescheduling.
In this case, Extra_bddImageCompute() should be called.]
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageTree_t * Extra_bddImageStart(
DdManager * dd, DdNode * bCare, // the care set
int nParts, DdNode ** pbParts, // the partitions for image computation
int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
{
Extra_ImageTree_t * pTree;
Extra_ImagePart_t ** pParts;
Extra_ImageVar_t ** pVars;
Extra_ImageNode_t ** pNodes;
int v;
if ( fVerbose && dd->size <= 80 )
Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
// create variables, partitions and leaf nodes
pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
// create the tree
pTree = ALLOC( Extra_ImageTree_t, 1 );
memset( pTree, 0, sizeof(Extra_ImageTree_t) );
pTree->pCare = pNodes[nParts];
pTree->fVerbose = fVerbose;
// process the nodes
while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
// make sure the variables are gone
for ( v = 0; v < dd->size; v++ )
assert( pVars[v] == NULL );
FREE( pVars );
// merge the topmost nodes
while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
// make sure the nodes are gone
for ( v = 0; v < nParts + 1; v++ )
assert( pNodes[v] == NULL );
FREE( pNodes );
// if ( fVerbose )
// Extra_bddImagePrintTree( pTree );
// set the support of the care set
pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
// clean the partitions
Extra_DeleteParts_rec( pTree->pRoot );
FREE( pParts );
return pTree;
}
/**Function*************************************************************
Synopsis [Compute the image.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
{
DdManager * dd = pTree->pCare->dd;
DdNode * bSupp, * bRem;
pTree->nIter++;
// make sure the supports are okay
bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp );
if ( bSupp != pTree->bCareSupp )
{
bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem );
if ( bRem != b1 )
{
printf( "Original care set support: " );
PRB( dd, pTree->bCareSupp );
printf( "Current care set support: " );
PRB( dd, bSupp );
Cudd_RecursiveDeref( dd, bSupp );
Cudd_RecursiveDeref( dd, bRem );
printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
return NULL;
}
Cudd_RecursiveDeref( dd, bRem );
}
Cudd_RecursiveDeref( dd, bSupp );
// remove the previous image
Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
pTree->pCare->bImage = bCare; Cudd_Ref( bCare );
// compute the image
pTree->nNodesMax = 0;
Extra_bddImageCompute_rec( pTree, pTree->pRoot );
if ( pTree->nNodesMaxT < pTree->nNodesMax )
pTree->nNodesMaxT = pTree->nNodesMax;
// if ( pTree->fVerbose )
// printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
return pTree->pRoot->bImage;
}
/**Function*************************************************************
Synopsis [Delete the tree.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
{
if ( pTree->bCareSupp )
Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
Extra_bddImageTreeDelete_rec( pTree->pRoot );
FREE( pTree );
}
/**Function*************************************************************
Synopsis [Reads the image from the tree.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
{
return pTree->pRoot->bImage;
}
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Definition of static Functions */
/*---------------------------------------------------------------------------*/
/**Function*************************************************************
Synopsis [Creates partitions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
int nParts, DdNode ** pbParts, DdNode * bCare )
{
Extra_ImagePart_t ** pParts;
int i;
// start the partitions
pParts = ALLOC( Extra_ImagePart_t *, nParts + 1 );
// create structures for each variable
for ( i = 0; i < nParts; i++ )
{
pParts[i] = ALLOC( Extra_ImagePart_t, 1 );
pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc );
pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
pParts[i]->iPart = i;
}
// add the care set as the last partition
pParts[nParts] = ALLOC( Extra_ImagePart_t, 1 );
pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc );
pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
pParts[nParts]->iPart = nParts;
return pParts;
}
/**Function*************************************************************
Synopsis [Creates variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
int nParts, Extra_ImagePart_t ** pParts,
int nVars, DdNode ** pbVars )
{
Extra_ImageVar_t ** pVars;
DdNode ** pbFuncs;
DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
int nVarsTotal, iVar, p, Counter;
// put all the functions into one array
pbFuncs = ALLOC( DdNode *, nParts );
for ( p = 0; p < nParts; p++ )
pbFuncs[p] = pParts[p]->bSupp;
bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp );
FREE( pbFuncs );
// remove the NS vars
bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs );
bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bCubeNs );
// get the number of I and CS variables to be quantified
nVarsTotal = Extra_bddSuppSize( dd, bSupp );
// start the variables
pVars = ALLOC( Extra_ImageVar_t *, dd->size );
memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
// create structures for each variable
for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
{
iVar = bSuppTemp->index;
pVars[iVar] = ALLOC( Extra_ImageVar_t, 1 );
pVars[iVar]->iNum = iVar;
// collect all the parts this var belongs to
Counter = 0;
bParts = b1; Cudd_Ref( bParts );
for ( p = 0; p < nParts; p++ )
if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
{
bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts );
Cudd_RecursiveDeref( dd, bTemp );
Counter++;
}
pVars[iVar]->bParts = bParts; // takes ref
pVars[iVar]->nParts = Counter;
}
Cudd_RecursiveDeref( dd, bSupp );
return pVars;
}
/**Function*************************************************************
Synopsis [Creates variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
int nParts, Extra_ImagePart_t ** pParts,
int nVars, Extra_ImageVar_t ** pVars )
{
Extra_ImageNode_t ** pNodes;
Extra_ImageNode_t * pNode;
DdNode * bTemp;
int i, v, iPart;
/*
DdManager * dd; // the manager
DdNode * bCube; // the cube to quantify
DdNode * bImage; // the partial image
Extra_ImageNode_t * pNode1; // the first branch
Extra_ImageNode_t * pNode2; // the second branch
Extra_ImagePart_t * pPart; // the partition (temporary)
*/
// start the partitions
pNodes = ALLOC( Extra_ImageNode_t *, nParts );
// create structures for each leaf nodes
for ( i = 0; i < nParts; i++ )
{
pNodes[i] = ALLOC( Extra_ImageNode_t, 1 );
memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
pNodes[i]->dd = dd;
pNodes[i]->pPart = pParts[i];
}
// find the quantification cubes for each leaf node
for ( v = 0; v < nVars; v++ )
{
if ( pVars[v] == NULL )
continue;
assert( pVars[v]->nParts > 0 );
if ( pVars[v]->nParts > 1 )
continue;
iPart = pVars[v]->bParts->index;
if ( pNodes[iPart]->bCube == NULL )
{
pNodes[iPart]->bCube = dd->vars[v];
Cudd_Ref( dd->vars[v] );
}
else
{
pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );
Cudd_Ref( pNodes[iPart]->bCube );
Cudd_RecursiveDeref( dd, bTemp );
}
// remove these variables
Cudd_RecursiveDeref( dd, pVars[v]->bParts );
FREE( pVars[v] );
}
// assign the leaf node images
for ( i = 0; i < nParts; i++ )
{
pNode = pNodes[i];
if ( pNode->bCube )
{
// update the partition
pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
Cudd_Ref( pParts[i]->bFunc );
Cudd_RecursiveDeref( dd, bTemp );
// update the support the partition
pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube );
Cudd_Ref( pParts[i]->bSupp );
Cudd_RecursiveDeref( dd, bTemp );
// update the numbers
pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
// get rid of the cube
// save the last (care set) quantification cube
if ( i < nParts - 1 )
{
Cudd_RecursiveDeref( dd, pNode->bCube );
pNode->bCube = NULL;
}
}
// copy the function
pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage );
}
/*
for ( i = 0; i < nParts; i++ )
{
pNode = pNodes[i];
PRB( dd, pNode->bCube );
PRB( dd, pNode->pPart->bFunc );
PRB( dd, pNode->pPart->bSupp );
printf( "\n" );
}
*/
return pNodes;
}
/**Function*************************************************************
Synopsis [Delete the partitions from the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
{
Extra_ImagePart_t * pPart;
if ( pNode->pNode1 )
Extra_DeleteParts_rec( pNode->pNode1 );
if ( pNode->pNode2 )
Extra_DeleteParts_rec( pNode->pNode2 );
pPart = pNode->pPart;
Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
FREE( pNode->pPart );
}
/**Function*************************************************************
Synopsis [Delete the partitions from the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
{
if ( pNode->pNode1 )
Extra_bddImageTreeDelete_rec( pNode->pNode1 );
if ( pNode->pNode2 )
Extra_bddImageTreeDelete_rec( pNode->pNode2 );
if ( pNode->bCube )
Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
if ( pNode->bImage )
Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
assert( pNode->pPart == NULL );
FREE( pNode );
}
/**Function*************************************************************
Synopsis [Recompute the image.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
{
DdManager * dd = pNode->dd;
DdNode * bTemp;
int nNodes;
// trivial case
if ( pNode->pNode1 == NULL )
{
if ( pNode->bCube )
{
pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube );
Cudd_Ref( pNode->bImage );
Cudd_RecursiveDeref( dd, bTemp );
}
return;
}
// compute the children
if ( pNode->pNode1 )
Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
if ( pNode->pNode2 )
Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
// clean the old image
if ( pNode->bImage )
Cudd_RecursiveDeref( dd, pNode->bImage );
pNode->bImage = NULL;
// compute the new image
if ( pNode->bCube )
pNode->bImage = Cudd_bddAndAbstract( dd,
pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
else
pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
Cudd_Ref( pNode->bImage );
if ( pTree->fVerbose )
{
nNodes = Cudd_DagSize( pNode->bImage );
if ( pTree->nNodesMax < nNodes )
pTree->nNodesMax = nNodes;
}
}
/**Function*************************************************************
Synopsis [Builds the tree.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Extra_BuildTreeNode( DdManager * dd,
int nNodes, Extra_ImageNode_t ** pNodes,
int nVars, Extra_ImageVar_t ** pVars )
{
Extra_ImageNode_t * pNode1, * pNode2;
Extra_ImageVar_t * pVar;
Extra_ImageNode_t * pNode;
DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
int iNode1, iNode2;
int iVarBest, nSupp, v;
// find the best variable
iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
if ( iVarBest == -1 )
return 0;
pVar = pVars[iVarBest];
// this var cannot appear in one partition only
nSupp = Extra_bddSuppSize( dd, pVar->bParts );
assert( nSupp == pVar->nParts );
assert( nSupp != 1 );
// if it appears in only two partitions, quantify it
if ( pVar->nParts == 2 )
{
// get the nodes
iNode1 = pVar->bParts->index;
iNode2 = cuddT(pVar->bParts)->index;
pNode1 = pNodes[iNode1];
pNode2 = pNodes[iNode2];
// get the quantification cube
bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube );
// add the variables that appear only in these partitions
for ( v = 0; v < nVars; v++ )
if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
{
// add this var
bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube );
Cudd_RecursiveDeref( dd, bTemp );
// clean this var
Cudd_RecursiveDeref( dd, pVars[v]->bParts );
FREE( pVars[v] );
}
// clean the best var
Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
FREE( pVars[iVarBest] );
// combines two nodes
pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
Cudd_RecursiveDeref( dd, bCube );
}
else // if ( pVar->nParts > 2 )
{
// find two smallest BDDs that have this var
Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
pNode1 = pNodes[iNode1];
pNode2 = pNodes[iNode2];
// it is not possible that a var appears only in these two
// otherwise, it would have a different cost
bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
for ( v = 0; v < nVars; v++ )
if ( pVars[v] && pVars[v]->bParts == bParts )
assert( 0 );
Cudd_RecursiveDeref( dd, bParts );
// combines two nodes
pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
}
// clean the old nodes
pNodes[iNode1] = pNode;
pNodes[iNode2] = NULL;
// update the variables that appear in pNode[iNode2]
for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
{
pVar = pVars[bSuppTemp->index];
if ( pVar == NULL ) // this variable is not be quantified
continue;
// quantify this var
assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
Cudd_RecursiveDeref( dd, bTemp );
// add the new var
pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
Cudd_RecursiveDeref( dd, bTemp );
// update the score
pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
}
return 1;
}
/**Function*************************************************************
Synopsis [Merges the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageNode_t * Extra_MergeTopNodes(
DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
{
Extra_ImageNode_t * pNode;
int n1 = -1, n2 = -1, n;
// find the first and the second non-empty spots
for ( n = 0; n < nNodes; n++ )
if ( pNodes[n] )
{
if ( n1 == -1 )
n1 = n;
else if ( n2 == -1 )
{
n2 = n;
break;
}
}
assert( n1 != -1 );
// check the situation when only one such node is detected
if ( n2 == -1 )
{
// save the node
pNode = pNodes[n1];
// clean the node
pNodes[n1] = NULL;
return pNode;
}
// combines two nodes
pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
// clean the old nodes
pNodes[n1] = pNode;
pNodes[n2] = NULL;
return NULL;
}
/**Function*************************************************************
Synopsis [Merges two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
{
Extra_ImageNode_t * pNode;
Extra_ImagePart_t * pPart;
// create a new partition
pPart = ALLOC( Extra_ImagePart_t, 1 );
memset( pPart, 0, sizeof(Extra_ImagePart_t) );
// create the function
pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
Cudd_Ref( pPart->bFunc );
// update the support the partition
pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
Cudd_Ref( pPart->bSupp );
// update the numbers
pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp );
pPart->nNodes = Cudd_DagSize( pPart->bFunc );
pPart->iPart = -1;
/*
PRB( dd, pNode1->pPart->bSupp );
PRB( dd, pNode2->pPart->bSupp );
PRB( dd, pPart->bSupp );
*/
// create a new node
pNode = ALLOC( Extra_ImageNode_t, 1 );
memset( pNode, 0, sizeof(Extra_ImageNode_t) );
pNode->dd = dd;
pNode->pPart = pPart;
pNode->pNode1 = pNode1;
pNode->pNode2 = pNode2;
// compute the image
pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube );
Cudd_Ref( pNode->bImage );
// save the cube
if ( bCube != b1 )
{
pNode->bCube = bCube; Cudd_Ref( bCube );
}
return pNode;
}
/**Function*************************************************************
Synopsis [Computes the best variable.]
Description [The variables is the best if the sum of squares of the
BDD sizes of the partitions, in which it participates, is the minimum.]
SideEffects []
SeeAlso []
***********************************************************************/
int Extra_FindBestVariable( DdManager * dd,
int nNodes, Extra_ImageNode_t ** pNodes,
int nVars, Extra_ImageVar_t ** pVars )
{
DdNode * bTemp;
int iVarBest, v;
double CostBest, CostCur;
CostBest = 100000000000000;
iVarBest = -1;
for ( v = 0; v < nVars; v++ )
if ( pVars[v] )
{
CostCur = 0;
for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
CostCur += pNodes[bTemp->index]->pPart->nNodes *
pNodes[bTemp->index]->pPart->nNodes;
if ( CostBest > CostCur )
{
CostBest = CostCur;
iVarBest = v;
}
}
return iVarBest;
}
/**Function*************************************************************
Synopsis [Computes two smallest partions that have this var.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
int nNodes, Extra_ImageNode_t ** pNodes,
int * piNode1, int * piNode2 )
{
DdNode * bTemp;
int iPart1, iPart2;
int CostMin1, CostMin2, Cost;
// go through the partitions
iPart1 = iPart2 = -1;
CostMin1 = CostMin2 = 1000000;
for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
{
Cost = pNodes[bTemp->index]->pPart->nNodes;
if ( CostMin1 > Cost )
{
CostMin2 = CostMin1; iPart2 = iPart1;
CostMin1 = Cost; iPart1 = bTemp->index;
}
else if ( CostMin2 > Cost )
{
CostMin2 = Cost; iPart2 = bTemp->index;
}
}
*piNode1 = iPart1;
*piNode2 = iPart2;
}
/**Function*************************************************************
Synopsis [Prints the latch dependency matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImagePrintLatchDependency(
DdManager * dd, DdNode * bCare, // the care set
int nParts, DdNode ** pbParts, // the partitions for image computation
int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!)
{
int i;
DdNode * bVarsCs, * bVarsNs;
bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs );
bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs );
printf( "The latch dependency matrix:\n" );
printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n",
nParts, dd->size, nVars );
printf( " : " );
for ( i = 0; i < dd->size; i++ )
printf( "%d", i % 10 );
printf( "\n" );
for ( i = 0; i < nParts; i++ )
Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
Cudd_RecursiveDeref( dd, bVarsCs );
Cudd_RecursiveDeref( dd, bVarsNs );
}
/**Function*************************************************************
Synopsis [Prints one row of the latch dependency matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImagePrintLatchDependencyOne(
DdManager * dd, DdNode * bFunc, // the function
DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars
int iPart )
{
DdNode * bSupport;
int v;
bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport );
printf( " %3d : ", iPart );
for ( v = 0; v < dd->size; v++ )
{
if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
{
if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
printf( "c" );
else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) )
printf( "n" );
else
printf( "i" );
}
else
printf( "." );
}
printf( "\n" );
Cudd_RecursiveDeref( dd, bSupport );
}
/**Function*************************************************************
Synopsis [Prints the tree for quenstification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
{
printf( "The quantification scheduling tree:\n" );
Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
}
/**Function*************************************************************
Synopsis [Prints the tree for quenstification scheduling.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
{
DdNode * Cube;
int i;
Cube = pNode->bCube;
if ( pNode->pNode1 == NULL )
{
printf( "<%d> ", pNode->pPart->iPart );
if ( Cube != NULL )
{
PRB( pNode->dd, Cube );
}
else
printf( "\n" );
return;
}
printf( "<*> " );
if ( Cube != NULL )
{
PRB( pNode->dd, Cube );
}
else
printf( "\n" );
for ( i = 0; i < Offset; i++ )
printf( " " );
Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
for ( i = 0; i < Offset; i++ )
printf( " " );
Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
}
struct Extra_ImageTree2_t_
{
DdManager * dd;
DdNode * bRel;
DdNode * bCube;
DdNode * bImage;
};
/**Function*************************************************************
Synopsis [Starts the monolithic image computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Extra_ImageTree2_t * Extra_bddImageStart2(
DdManager * dd, DdNode * bCare,
int nParts, DdNode ** pbParts,
int nVars, DdNode ** pbVars, int fVerbose )
{
Extra_ImageTree2_t * pTree;
DdNode * bCubeAll, * bCubeNot, * bTemp;
int i;
pTree = ALLOC( Extra_ImageTree2_t, 1 );
pTree->dd = dd;
pTree->bImage = NULL;
bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot );
pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
Cudd_RecursiveDeref( dd, bCubeAll );
Cudd_RecursiveDeref( dd, bCubeNot );
// derive the monolithic relation
pTree->bRel = b1; Cudd_Ref( pTree->bRel );
for ( i = 0; i < nParts; i++ )
{
pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
Cudd_RecursiveDeref( dd, bTemp );
}
Extra_bddImageCompute2( pTree, bCare );
return pTree;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
{
if ( pTree->bImage )
Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube );
Cudd_Ref( pTree->bImage );
return pTree->bImage;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
{
if ( pTree->bRel )
Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
if ( pTree->bCube )
Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
if ( pTree->bImage )
Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
FREE( pTree );
}
/**Function*************************************************************
Synopsis [Returns the previously computed image.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
{
return pTree->bImage;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/misc/extra/extraBddMisc.c
......@@ -961,6 +961,34 @@ void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** b
} /* end of Extra_bddPermuteArray */
/**Function********************************************************************
Synopsis [Computes the positive polarty cube composed of the first vars in the array.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
{
DdNode * bRes;
DdNode * bTemp;
int i;
bRes = b1; Cudd_Ref( bRes );
for ( i = 0; i < nVars; i++ )
{
bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes );
Cudd_RecursiveDeref( dd, bTemp );
}
Cudd_Deref( bRes );
return bRes;
}
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
......
src/misc/extra/module.make
SRC += src/misc/extra/extraBddAuto.c \
src/misc/extra/extraBddCas.c \
src/misc/extra/extraBddImage.c \
src/misc/extra/extraBddKmap.c \
src/misc/extra/extraBddMisc.c \
src/misc/extra/extraBddSymm.c \
......
src/opt/mfs/mfsCore.c
......@@ -241,21 +241,23 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
if ( pNtk->pExcare )
{
Abc_Ntk_t * pTemp;
if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
else
{
pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
p->pCare = Abc_NtkToDar( pTemp, 0 );
Abc_NtkDelete( pTemp );
p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
}
// if ( pPars->fVerbose )
{
}
if ( p->pCare != NULL )
printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
// else
// printf( "Performing optimization without constraints.\n" );
}
// prepare the BDC manager
if ( !pPars->fResub )
{
pDecPars->nVarsMax = nFaninMax;
pDecPars->nVarsMax = (nFaninMax < 3) ? 3 : nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
......
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