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

Version abc70217

This commit is contained in:
Alan Mishchenko 2007-02-17 08:01:00 -08:00
parent 607c253cd2
commit 50e0d1dea5
43 changed files with 4571 additions and 129887 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -8,7 +8,7 @@ PROG := abc
MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/ver \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/aig/mem src/aig/ec \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret src/opt/res src/opt/kit \

32
abc.dsp
View File

@ -50,7 +50,7 @@ BSC32=bscmake.exe
# ADD BSC32 /nologo
LINK32=link.exe
# ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /machine:I386
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe"
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /profile /machine:I386 /out:"_TEST/abc.exe"
!ELSEIF "$(CFG)" == "abc - Win32 Debug"
@ -75,7 +75,7 @@ BSC32=bscmake.exe
# ADD BSC32 /nologo
LINK32=link.exe
# ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /pdbtype:sept
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib lib/libhmetis.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
!ENDIF
@ -194,6 +194,10 @@ SOURCE=.\src\base\abci\abcBmc.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcCas.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcClpBdd.c
# End Source File
# Begin Source File
@ -302,6 +306,10 @@ SOURCE=.\src\base\abci\abcProve.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcQuant.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcReconv.c
# End Source File
# Begin Source File
@ -1153,6 +1161,22 @@ SOURCE=.\src\bdd\reo\reoTransfer.c
SOURCE=.\src\bdd\reo\reoUnits.c
# End Source File
# End Group
# Begin Group "cas"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\bdd\cas\cas.h
# End Source File
# Begin Source File
SOURCE=.\src\bdd\cas\casCore.c
# End Source File
# Begin Source File
SOURCE=.\src\bdd\cas\casDec.c
# End Source File
# End Group
# End Group
# Begin Group "sat"
@ -2006,6 +2030,10 @@ SOURCE=.\src\misc\extra\extraBddAuto.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraBddCas.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraBddKmap.c
# End Source File
# Begin Source File

2
abc.rc
View File

@ -122,4 +122,6 @@ alias tt "rh a/quip_opt/nut_001_opt.blif"
alias ttb "wh a/quip_opt/nut_001_opt.blif 1.blif"
alias ttv "wh a/quip_opt/nut_001_opt.blif 1.v"
alias reach "st; ps; compress2; ps; qrel; ps; qreach -v; ps"

10
src/base/abc/abc.h
View File

@ -393,6 +393,8 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Ab
static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) ); }
static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) ); }
// checking the AIG node types
static inline bool Abc_AigNodeIsConst( Abc_Obj_t * pNode ) { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk)); return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1; }
@ -527,11 +529,9 @@ extern void Abc_AigPrintNode( Abc_Obj_t * pNode );
extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
extern void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
extern void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan );
extern Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
extern void Abc_AigUpdateStop( Abc_Aig_t * pMan );
extern void Abc_AigUpdateReset( Abc_Aig_t * pMan );
extern void Abc_AigUpdateAdd( Abc_Aig_t * pMan, Abc_Obj_t * pObj );
extern Vec_Ptr_t * Abc_AigUpdateRead( Abc_Aig_t * pMan );
/*=== abcAttach.c ==========================================================*/
extern int Abc_NtkAttach( Abc_Ntk_t * pNtk );
/*=== abcBalance.c ==========================================================*/
@ -555,6 +555,7 @@ extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
@ -623,7 +624,7 @@ extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
/*=== abcMiter.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
extern void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
extern Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
extern Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
extern Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
@ -831,6 +832,7 @@ extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
extern void Abc_NtkCleanData( Abc_Ntk_t * pNtk );
extern int Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
extern void Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );

81
src/base/abc/abcAig.c
View File

@ -59,7 +59,8 @@ struct Abc_Aig_t_
Vec_Ptr_t * vStackReplaceNew; // the nodes to be used for replacement
Vec_Vec_t * vLevels; // the nodes to be updated
Vec_Vec_t * vLevelsR; // the nodes to be updated
Vec_Ptr_t * vUpdates; // the added and removed nodes
Vec_Ptr_t * vAddedCells; // the added nodes
Vec_Ptr_t * vUpdatedNets; // the nodes whose fanouts have changed
int nStrash0;
int nStrash1;
@ -163,8 +164,10 @@ void Abc_AigFree( Abc_Aig_t * pMan )
assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
// free the table
if ( pMan->vUpdates )
Vec_PtrFree( pMan->vUpdates );
if ( pMan->vAddedCells )
Vec_PtrFree( pMan->vAddedCells );
if ( pMan->vUpdatedNets )
Vec_PtrFree( pMan->vUpdatedNets );
Vec_VecFree( pMan->vLevels );
Vec_VecFree( pMan->vLevelsR );
Vec_PtrFree( pMan->vStackReplaceOld );
@ -326,8 +329,8 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
// Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
pAnd->pCopy = NULL;
// add the node to the list of updated nodes
if ( pMan->vUpdates )
Vec_PtrPush( pMan->vUpdates, pAnd );
if ( pMan->vAddedCells )
Vec_PtrPush( pMan->vAddedCells, pAnd );
return pAnd;
}
@ -366,8 +369,8 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
// Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
pAnd->pCopy = NULL;
// add the node to the list of updated nodes
if ( pMan->vUpdates )
Vec_PtrPush( pMan->vUpdates, pAnd );
// if ( pMan->vAddedCells )
// Vec_PtrPush( pMan->vAddedCells, pAnd );
return pAnd;
}
@ -548,9 +551,6 @@ void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
// delete the cuts if defined
if ( pThis->pNtk->pManCut )
Abc_NodeFreeCuts( pThis->pNtk->pManCut, pThis );
// add the node to the list of updated nodes
if ( pMan->vUpdates )
Vec_PtrPush( pMan->vUpdates, pThis );
}
/**Function*************************************************************
@ -961,6 +961,13 @@ void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
pNode0 = Abc_ObjFanin0( pNode );
pNode1 = Abc_ObjFanin1( pNode );
// add the node to the list of updated nodes
if ( pMan->vUpdatedNets )
{
Vec_PtrPushUnique( pMan->vUpdatedNets, pNode0 );
Vec_PtrPushUnique( pMan->vUpdatedNets, pNode1 );
}
// remove the node from the table
Abc_AigAndDelete( pMan, pNode );
// if the node is in the level structure, remove it
@ -1368,10 +1375,13 @@ void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan )
Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets )
{
assert( pMan->vUpdates == NULL );
return pMan->vUpdates = Vec_PtrAlloc( 1000 );
assert( pMan->vAddedCells == NULL );
pMan->vAddedCells = Vec_PtrAlloc( 1000 );
pMan->vUpdatedNets = Vec_PtrAlloc( 1000 );
*pvUpdatedNets = pMan->vUpdatedNets;
return pMan->vAddedCells;
}
/**Function*************************************************************
@ -1387,8 +1397,11 @@ Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan )
***********************************************************************/
void Abc_AigUpdateStop( Abc_Aig_t * pMan )
{
assert( pMan->vUpdates != NULL );
Vec_PtrFree( pMan->vUpdates );
assert( pMan->vAddedCells != NULL );
Vec_PtrFree( pMan->vAddedCells );
Vec_PtrFree( pMan->vUpdatedNets );
pMan->vAddedCells = NULL;
pMan->vUpdatedNets = NULL;
}
/**Function*************************************************************
@ -1404,41 +1417,9 @@ void Abc_AigUpdateStop( Abc_Aig_t * pMan )
***********************************************************************/
void Abc_AigUpdateReset( Abc_Aig_t * pMan )
{
assert( pMan->vUpdates != NULL );
Vec_PtrClear( pMan->vUpdates );
}
/**Function*************************************************************
Synopsis [Add a new update.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigUpdateAdd( Abc_Aig_t * pMan, Abc_Obj_t * pObj )
{
if ( pMan->vUpdates )
Vec_PtrPush( pMan->vUpdates, pObj );
}
/**Function*************************************************************
Synopsis [Read the updates array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_AigUpdateRead( Abc_Aig_t * pMan )
{
return pMan->vUpdates;
assert( pMan->vAddedCells != NULL );
Vec_PtrClear( pMan->vAddedCells );
Vec_PtrClear( pMan->vUpdatedNets );
}
////////////////////////////////////////////////////////////////////////

70
src/base/abc/abcDfs.c
View File

@ -199,6 +199,76 @@ Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
return vNodes;
}
/**Function*************************************************************
Synopsis [Performs DFS for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDfsReverseNodes_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
{
Abc_Obj_t * pFanout;
int i;
assert( !Abc_ObjIsNet(pNode) );
// if this node is already visited, skip
if ( Abc_NodeIsTravIdCurrent( pNode ) )
return;
// mark the node as visited
Abc_NodeSetTravIdCurrent( pNode );
// skip the CI
if ( Abc_ObjIsCo(pNode) )
return;
assert( Abc_ObjIsNode( pNode ) );
// visit the transitive fanin of the node
pNode = Abc_ObjFanout0Ntk(pNode);
Abc_ObjForEachFanout( pNode, pFanout, i )
Abc_NtkDfsReverseNodes_rec( pFanout, vNodes );
// add the node after the fanins have been added
// Vec_PtrPush( vNodes, pNode );
Vec_PtrFillExtra( vNodes, pNode->Level + 1, NULL );
pNode->pCopy = Vec_PtrEntry( vNodes, pNode->Level );
Vec_PtrWriteEntry( vNodes, pNode->Level, pNode );
}
/**Function*************************************************************
Synopsis [Returns the levelized array of TFO nodes.]
Description [Collects the levelized array of internal nodes, leaving out CIs/COs.
However it marks both CIs and COs with the current TravId.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pFanout;
int i, k;
assert( Abc_NtkIsStrash(pNtk) );
// set the traversal ID
Abc_NtkIncrementTravId( pNtk );
// start the array of nodes
vNodes = Vec_PtrStart( Abc_AigLevel(pNtk) + 1 );
for ( i = 0; i < nNodes; i++ )
{
pObj = ppNodes[i];
assert( Abc_ObjIsCi(pObj) );
Abc_NodeSetTravIdCurrent( pObj );
pObj = Abc_ObjFanout0Ntk(pObj);
Abc_ObjForEachFanout( pObj, pFanout, k )
Abc_NtkDfsReverseNodes_rec( pFanout, vNodes );
}
return vNodes;
}
/**Function*************************************************************

19
src/base/abc/abcUtil.c
View File

@ -484,6 +484,25 @@ void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk )
pObj->pCopy = NULL;
}
/**Function*************************************************************
Synopsis [Cleans the copy field of all objects.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCleanData( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
Abc_NtkForEachObj( pNtk, pObj, i )
pObj->pData = NULL;
}
/**Function*************************************************************
Synopsis [Counts the number of nodes having non-trivial copies.]

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

@ -67,6 +67,7 @@ static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -96,6 +97,10 @@ static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -203,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
@ -232,6 +238,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "Various", "qvar", Abc_CommandQuaVar, 1 );
Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 );
Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 );
Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 );
@ -3234,6 +3244,109 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, nLutSize;
int fCheck;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nLutSize = 12;
fCheck = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Kcvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nLutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLutSize < 0 )
goto usage;
break;
case 'c':
fCheck ^= 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_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Can only collapse a logic network or an AIG.\n" );
return 1;
}
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
{
fprintf( pErr, "Cascade synthesis has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: cascade [-K <num>] [-cvh]\n" );
fprintf( pErr, "\t performs LUT cascade synthesis for the current network\n" );
fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize );
fprintf( pErr, "\t-c : check equivalence after synthesis [default = %s]\n", fCheck? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t \n");
fprintf( pErr, " A lookup-table cascade is a programmable architecture developed by\n");
fprintf( pErr, " Professor Tsutomu Sasao (sasao@cse.kyutech.ac.jp) at Kyushu Institute\n");
fprintf( pErr, " of Technology. This work received Takeda Techno-Entrepreneurship Award:\n");
fprintf( pErr, " http://www.lsi-cad.com/sasao/photo/takeda.html\n");
fprintf( pErr, "\t \n");
return 1;
}
/**Function*************************************************************
@ -5536,6 +5649,293 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, iVar, fVerbose, RetValue;
extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
iVar = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
iVar = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iVar < 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_NtkGetChoiceNum( pNtk ) )
{
fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
return 1;
}
// get the strashed network
pNtkRes = Abc_NtkStrash( pNtk, 0, 1 );
RetValue = Abc_NtkQuantify( pNtkRes, iVar, fVerbose );
// clean temporary storage for the cofactors
Abc_NtkCleanData( pNtkRes );
Abc_AigCleanup( pNtkRes->pManFunc );
// check the result
if ( !RetValue )
{
fprintf( pErr, "Command has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: qvar [-I num] [-vh]\n" );
fprintf( pErr, "\t quantifies one variable using the AIG\n" );
fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar );
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandQuaRel( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, iVar, fInputs, fVerbose;
extern Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
iVar = 0;
fInputs = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Iqvh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
iVar = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iVar < 0 )
goto usage;
break;
case 'q':
fInputs ^= 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_NtkGetChoiceNum( pNtk ) )
{
fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "This command works only for sequential circuits.\n" );
return 1;
}
// get the strashed network
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtk, 0, 1 );
pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose );
Abc_NtkDelete( pNtk );
}
else
pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose );
// check if the result is available
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: qrel [-qvh]\n" );
fprintf( pErr, "\t computes transition relation of the sequential network\n" );
// fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar );
fprintf( pErr, "\t-q : perform quantification of inputs [default = %s]\n", fInputs? "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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandQuaReach( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, nIters, fVerbose;
extern Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtk, int nIters, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nIters = 256;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIters < 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_NtkGetChoiceNum( pNtk ) )
{
fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" );
return 1;
}
if ( !Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "This command works only for combinational transition relations.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
if ( Abc_NtkPoNum(pNtk) > 1 )
{
fprintf( pErr, "The transition relation should have one output.\n" );
return 1;
}
if ( Abc_NtkPiNum(pNtk) % 2 != 0 )
{
fprintf( pErr, "The transition relation should have an even number of inputs.\n" );
return 1;
}
pNtkRes = Abc_NtkReachability( pNtk, nIters, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: qreach [-I num] [-vh]\n" );
fprintf( pErr, "\t computes unreachable states using AIG-based quantification\n" );
fprintf( pErr, "\t assumes that the current network is a transition relation\n" );
fprintf( pErr, "\t assumes that the initial state is composed of all zeros\n" );
fprintf( pErr, "\t-I num : the number of image computations to perform [default = %d]\n", nIters );
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;
}
/**Function*************************************************************

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

@ -74,7 +74,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
// print the size of the BDDs
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// allocate additional variables
for ( i = 0; i < nInputs; i++ )

111
src/base/abci/abcCas.c Normal file
View File

@ -0,0 +1,111 @@
/**CFile****************************************************************
FileName [abcCas.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Decomposition of shared BDDs into LUT cascade.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
/*
This LUT cascade synthesis algorithm is described in the paper:
A. Mishchenko and T. Sasao, "Encoding of Boolean functions and its
application to LUT cascade synthesis", Proc. IWLS '02, pp. 115-120.
http://www.eecs.berkeley.edu/~alanmi/publications/2002/iwls02_enc.pdf
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose )
{
DdManager * dd;
DdNode ** ppOutputs;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode;
char * pFileGeneric;
int fBddSizeMax = 500000;
int fReorder = 1;
int i, clk = clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
return NULL;
if ( fVerbose )
{
DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
PRT( "BDD construction time", clock() - clk );
}
// collect global BDDs
dd = Abc_NtkGlobalBddMan( pNtk );
ppOutputs = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
ppOutputs[i] = Abc_ObjGlobalBdd(pNode);
// call the decomposition
pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec );
if ( !Abc_CascadeExperiment( pFileGeneric, dd, ppOutputs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), nLutSize, fCheck, fVerbose ) )
{
// the LUT size is too small
}
// for now, duplicate the network
pNtkNew = Abc_NtkDup( pNtk );
// cleanup
Abc_NtkFreeGlobalBdds( pNtk, 1 );
free( ppOutputs );
free( pFileGeneric );
// if ( pNtk->pExdc )
// pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkCollapse: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -54,7 +54,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
if ( fVerbose )
{
DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
printf( "The shared BDD size is %d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
PRT( "BDD construction time", clock() - clk );
}

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

@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
if ( dd == NULL )
return NULL;
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// transform the result of mapping into a BDD network
pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
Extra_StopManager( dd );

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

@ -294,7 +294,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 )
{
char Buffer[1000];
Abc_Ntk_t * pNtkMiter;
@ -313,7 +313,8 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
// start the new network
pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
// sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
sprintf( Buffer, "product" );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
// perform strashing
@ -324,10 +325,13 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
pRoot1 = Abc_NtkPo(pNtk1,0);
pRoot2 = Abc_NtkPo(pNtk2,0);
pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) );
pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ^ fCompl2 );
// create the miter of the two outputs
pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
if ( fOr )
pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 );
else
pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
// make sure that everything is okay

36
src/base/abci/abcPlace.c
View File

@ -120,7 +120,7 @@ float Abc_PlaceEvaluateCut( Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins )
SeeAlso []
***********************************************************************/
void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld )
void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets )
{
Abc_Obj_t * pObj, * pFanin;
int i, k;
@ -130,24 +130,26 @@ void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld )
vCells = Vec_PtrAlloc( 16 );
vNets = Vec_PtrAlloc( 32 );
// go through the modified nodes
Vec_PtrForEachEntry( vUpdates, pObj, i )
// go through the new nodes
Vec_PtrForEachEntry( vAddedCells, pObj, i )
{
if ( pObj->Id > nNodesOld ) // pObj is a new node
{
Abc_PlaceCreateCell( pObj, 1 );
Abc_PlaceUpdateNet( pObj );
assert( !Abc_ObjIsComplement(pObj) );
Abc_PlaceCreateCell( pObj, 1 );
Abc_PlaceUpdateNet( pObj );
// add the new cell and its fanin nets to temporary storage
Vec_PtrPush( vCells, &(cells[pObj->Id]) );
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) );
}
else // pObj is an old node
{
Abc_PlaceUpdateNet( Abc_ObjFanin0(pObj) );
Abc_PlaceUpdateNet( Abc_ObjFanin1(pObj) );
}
// add the new cell and its fanin nets to temporary storage
Vec_PtrPush( vCells, &(cells[pObj->Id]) );
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) );
}
// go through the modified nets
Vec_PtrForEachEntry( vUpdatedNets, pObj, i )
{
assert( !Abc_ObjIsComplement(pObj) );
if ( Abc_ObjType(pObj) == ABC_OBJ_NONE ) // dead node
continue;
Abc_PlaceUpdateNet( pObj );
}
// update the placement

389
src/base/abci/abcQuant.c Normal file
View File

@ -0,0 +1,389 @@
/**CFile****************************************************************
FileName [abcQuant.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [AIG-based variable quantification.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Existentially quantifies one variable.]
Description []
SideEffects [This procedure creates dangling nodes in the AIG.]
SeeAlso []
***********************************************************************/
int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pNext, * pFanin;
int i;
assert( Abc_NtkIsStrash(pNtk) );
assert( iVar < Abc_NtkCiNum(pNtk) );
// collect the internal nodes
pObj = Abc_NtkCi( pNtk, iVar );
vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 );
// assign the cofactors of the CI node to be constants
pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) );
pObj->pData = Abc_AigConst1(pNtk);
// quantify the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj )
{
pFanin = Abc_ObjFanin0(pObj);
if ( !Abc_NodeIsTravIdCurrent(pFanin) )
pFanin->pCopy = pFanin->pData = pFanin;
pFanin = Abc_ObjFanin1(pObj);
if ( !Abc_NodeIsTravIdCurrent(pFanin) )
pFanin->pCopy = pFanin->pData = pFanin;
pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) );
}
}
Vec_PtrFree( vNodes );
// update the affected COs
Abc_NtkForEachCo( pNtk, pObj, i )
{
if ( !Abc_NodeIsTravIdCurrent(pObj) )
continue;
pFanin = Abc_ObjFanin0(pObj);
// get the result of quantification
pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
if ( Abc_ObjRegular(pNext) == pFanin )
continue;
// update the fanins of the CO
Abc_ObjPatchFanin( pObj, pFanin, pNext );
// if ( Abc_ObjFanoutNum(pFanin) == 0 )
// Abc_AigDeleteNode( pNtk->pManFunc, pFanin );
}
// make sure the node has no fanouts
// pObj = Abc_NtkCi( pNtk, iVar );
// assert( Abc_ObjFanoutNum(pObj) == 0 );
return 1;
}
/**Function*************************************************************
Synopsis [Constructs the transition relation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
{
char Buffer[1000];
Vec_Ptr_t * vPairs;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pMiter;
int i, nLatches;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) );
nLatches = Abc_NtkLatchNum(pNtk);
// start the network
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
// duplicate the name and the spec
sprintf( Buffer, "%s_TR", pNtk->pName );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
// pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Abc_NtkCleanCopy( pNtk );
// create current state variables
Abc_NtkForEachLatchOutput( pNtk, pObj, i )
{
pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
}
// create next state variables
Abc_NtkForEachLatchInput( pNtk, pObj, i )
Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL );
// create PI variables
Abc_NtkForEachPi( pNtk, pObj, i )
Abc_NtkDupObj( pNtkNew, pObj, 1 );
// restrash the nodes (assuming a topological order of the old network)
Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
// create the function of the primary output
assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
vPairs = Vec_PtrAlloc( 2*nLatches );
Abc_NtkForEachLatchInput( pNtk, pObj, i )
{
Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
}
pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
Vec_PtrFree( vPairs );
// add the primary output
Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) );
Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL );
// quantify inputs
if ( fInputs )
{
assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches );
for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
Abc_NtkQuantify( pNtkNew, i, fVerbose );
Abc_NtkCleanData( pNtkNew );
Abc_AigCleanup( pNtkNew->pManFunc );
for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
{
pObj = Abc_NtkPi( pNtkNew, i );
assert( Abc_ObjFanoutNum(pObj) == 0 );
Abc_NtkDeleteObj( pObj );
}
}
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkTransRel: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Performs one image computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkInitialState( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pMiter;
int i, nVars = Abc_NtkPiNum(pNtk)/2;
assert( Abc_NtkIsStrash(pNtk) );
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
// compute the all-zero state in terms of the CS variables
pMiter = Abc_AigConst1(pNtkNew);
for ( i = 0; i < nVars; i++ )
pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) );
// add the PO
Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Swaps current state and next state variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkSwapVariables( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1;
int i, nVars = Abc_NtkPiNum(pNtk)/2;
assert( Abc_NtkIsStrash(pNtk) );
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
// update the PIs
for ( i = 0; i < nVars; i++ )
{
pObj0 = Abc_NtkPi( pNtk, i );
pObj1 = Abc_NtkPi( pNtk, i+nVars );
pMiter = pObj0->pCopy;
pObj0->pCopy = pObj1->pCopy;
pObj1->pCopy = pMiter;
}
// restrash
Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
// add the PO
pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) );
Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Performs reachability analisys.]
Description [Assumes that the input is the transition relation.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
{
Abc_Obj_t * pObj;
Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp;
int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev;
int fFixedPoint = 0;
int fSynthesis = 1;
assert( Abc_NtkIsStrash(pNtkRel) );
assert( Abc_NtkLatchNum(pNtkRel) == 0 );
assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 );
// compute the network composed of the initial states
pNtkFront = Abc_NtkInitialState( pNtkRel );
pNtkReached = Abc_NtkDup( pNtkFront );
//Abc_NtkShow( pNtkReached, 0, 0, 0 );
if ( fVerbose )
printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) );
// perform iterations of reachability analysis
nNodesPrev = Abc_NtkNodeNum(pNtkFront);
nVars = Abc_NtkPiNum(pNtkRel)/2;
for ( i = 0; i < nIters; i++ )
{
clk = clock();
// get the set of next states
pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 );
Abc_NtkDelete( pNtkFront );
// quantify the current state variables
for ( v = 0; v < nVars; v++ )
{
Abc_NtkQuantify( pNtkNext, v, fVerbose );
if ( fSynthesis && (v % 3 == 2) )
{
Abc_NtkCleanData( pNtkNext );
Abc_AigCleanup( pNtkNext->pManFunc );
Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
}
}
Abc_NtkCleanData( pNtkNext );
Abc_AigCleanup( pNtkNext->pManFunc );
if ( fSynthesis )
{
Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 );
pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
}
// map the next states into the current states
pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext );
Abc_NtkDelete( pNtkTemp );
// check the termination condition
if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) )
{
fFixedPoint = 1;
printf( "Fixed point is reached!\n" );
Abc_NtkDelete( pNtkNext );
break;
}
// compute new front
pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 );
Abc_NtkDelete( pNtkNext );
// add the reached states
pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 );
Abc_NtkDelete( pNtkTemp );
// compress the size of Front
nNodesOld = Abc_NtkNodeNum(pNtkFront);
if ( fSynthesis )
{
Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 );
pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 );
pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
}
nNodesNew = Abc_NtkNodeNum(pNtkFront);
// print statistics
if ( fVerbose )
{
printf( "I = %3d : Reached = %6d Front = %6d FrontM = %6d %6.2f %% ",
i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew );
PRT( "T", clock() - clk );
}
nNodesPrev = Abc_NtkNodeNum(pNtkFront);
}
if ( !fFixedPoint )
fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters );
// report the stats
if ( fVerbose )
{
// nMints = 1;
// fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
}
// complement the output to represent the set of unreachable states
Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 );
// remove next state variables
for ( i = 2*nVars - 1; i >= nVars; i-- )
{
pObj = Abc_NtkPi( pNtkReached, i );
assert( Abc_ObjFanoutNum(pObj) == 0 );
Abc_NtkDeleteObj( pObj );
}
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkReached ) )
{
printf( "Abc_NtkReachability: The network check has failed.\n" );
Abc_NtkDelete( pNtkReached );
return NULL;
}
return pNtkReached;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

8
src/base/abci/abcRewrite.c
View File

@ -38,7 +38,7 @@ static void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
extern void Abc_PlaceBegin( Abc_Ntk_t * pNtk );
extern void Abc_PlaceEnd( Abc_Ntk_t * pNtk );
extern void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld );
extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -61,7 +61,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
Cut_Man_t * pManCut;
Rwr_Man_t * pManRwr;
Abc_Obj_t * pNode;
Vec_Ptr_t * vUpdates = NULL;
Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
Dec_Graph_t * pGraph;
int i, nNodes, nGain, fCompl;
int clk, clkStart = clock();
@ -74,7 +74,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
if ( fPlaceEnable )
{
Abc_PlaceBegin( pNtk );
vUpdates = Abc_AigUpdateStart( pNtk->pManFunc );
vAddedCells = Abc_AigUpdateStart( pNtk->pManFunc, &vUpdatedNets );
}
// start the rewriting manager
@ -132,7 +132,7 @@ Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
// use the array of changed nodes to update placement
if ( fPlaceEnable )
Abc_PlaceUpdate( vUpdates, nNodes );
Abc_PlaceUpdate( vAddedCells, vUpdatedNets );
}
Extra_ProgressBarStop( pProgress );
Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );

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

@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
// print warning about choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" );
// start the new network (constants and CIs are already mappined after this step
// start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
// restrash the nodes (assuming a topological order of the old network)
Abc_NtkForEachNode( pNtk, pObj, i )

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

@ -84,7 +84,7 @@ clkBdd = clock() - clk;
// pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
// print the size of the BDDs
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// perform naive BDD-based computation
if ( fUseNaive )

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

@ -62,7 +62,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
if ( dd == NULL )
return 0;
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// create the transition relation (dereferenced global BDDs)
bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose ); Cudd_Ref( bRelation );
@ -221,7 +221,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
{
DdNode * bRelation, * bReached, * bCubeCs;
DdNode * bCurrent, * bNext, * bTemp;
int nIters;
int nIters, nMints;
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
@ -258,9 +258,9 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
// report the stats
if ( fVerbose )
{
fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
fprintf( stdout, "The number of minterms in the reachable state set = %d.\n",
(int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) );
nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) );
}
//PRB( dd, bReached );
Cudd_Deref( bReached );

2
src/base/abci/module.make
View File

@ -3,6 +3,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcAuto.c \
src/base/abci/abcBalance.c \
src/base/abci/abcBmc.c \
src/base/abci/abcCas.c \
src/base/abci/abcClpBdd.c \
src/base/abci/abcClpSop.c \
src/base/abci/abcCut.c \
@ -29,6 +30,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcPlace.c \
src/base/abci/abcPrint.c \
src/base/abci/abcProve.c \
src/base/abci/abcQuant.c \
src/base/abci/abcReconv.c \
src/base/abci/abcRefactor.c \
src/base/abci/abcRenode.c \

62
src/bdd/cas/cas.h Normal file
View File

@ -0,0 +1,62 @@
/**CFile****************************************************************
FileName [cas.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cas.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CAS_H__
#define __CAS_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define MAXINPUTS 1024
#define MAXOUTPUTS 1024
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== zzz.c ==========================================================*/
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1263
src/bdd/cas/casCore.c Normal file
View File

File diff suppressed because it is too large Load Diff

508
src/bdd/cas/casDec.c Normal file
View File

@ -0,0 +1,508 @@
/**CFile****************************************************************
FileName [casDec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
Synopsis [BDD-based decomposition with encoding.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Spring 2002.]
Revision [$Id: casDec.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <time.h>
#include "extra.h"
#include "cas.h"
////////////////////////////////////////////////////////////////////////
/// type definitions ///
////////////////////////////////////////////////////////////////////////
typedef struct
{
int nIns; // the number of LUT variables
int nInsP; // the number of inputs coming from the previous LUT
int nCols; // the number of columns in this LUT
int nMulti; // the column multiplicity, [log2(nCols)]
int nSimple; // the number of outputs implemented as direct connections to inputs of the previous block
int Level; // the starting level in the ADD in this LUT
// DdNode ** pbVarsIn[32]; // the BDDs of the elementary input variables
// DdNode ** pbVarsOut[32]; // the BDDs of the elementary output variables
// char * pNamesIn[32]; // the names of input variables
// char * pNamesOut[32]; // the names of output variables
DdNode ** pbCols; // the array of columns represented by BDDs
DdNode ** pbCodes; // the array of codes (in terms of pbVarsOut)
DdNode ** paNodes; // the array of starting ADD nodes on the next level (also referenced)
DdNode * bRelation; // the relation after encoding
// the relation depends on the three groups of variables:
// (1) variables on top represent the outputs of the previous cascade
// (2) variables in the middle represent the primary inputs
// (3) variables below (CVars) represent the codes
//
// the replacement is done after computing the relation
} LUT;
////////////////////////////////////////////////////////////////////////
/// static functions ///
////////////////////////////////////////////////////////////////////////
// the LUT-2-BLIF writing function
void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName );
// the function to write a DD (BDD or ADD) as a network of MUXES
extern void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
extern void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
////////////////////////////////////////////////////////////////////////
/// static varibles ///
////////////////////////////////////////////////////////////////////////
static int s_LutSize = 15;
static int s_nFuncVars;
long s_EncodingTime;
long s_EncSearchTime;
long s_EncComputeTime;
////////////////////////////////////
// temporary output variables
//FILE * pTable;
//long s_ReadingTime;
//long s_RemappingTime;
////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// debugging macros ///
////////////////////////////////////////////////////////////////////////
#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" )
////////////////////////////////////////////////////////////////////////
/// EXTERNAL FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose )
// aFunc is a 0-1 ADD for the given function
// pNames (nNames) are the input variable names
// FileName is the name of the output file for the LUT network
// dynamic variable reordering should be disabled when this function is running
{
static LUT * pLuts[MAXINPUTS]; // the LUT cascade
static int Profile[MAXINPUTS]; // the profile filled in with the info about the BDD width
static int Permute[MAXINPUTS]; // the array to store a temporary permutation of variables
LUT * p; // the current LUT
int i, v;
DdNode * bCVars[32]; // these are variables for the codes
int nVarsRem; // the number of remaining variables
int PrevMulti; // column multiplicity on the previous level
int fLastLut; // flag to signal the last LUT
int nLuts;
int nLutsTotal = 0;
int nLutOutputs = 0;
int nLutOutputsOrig = 0;
long clk1;
s_LutSize = nLutSize;
s_nFuncVars = nNames;
// get the profile
clk1 = clock();
Extra_ProfileWidth( dd, aFunc, Profile, -1 );
// for ( v = 0; v < nNames; v++ )
// printf( "Level = %2d, Width = %2d\n", v+1, Profile[v] );
//printf( "\n" );
// mark-up the LUTs
// assuming that the manager has exactly nNames vars (new vars have not been introduced yet)
nVarsRem = nNames; // the number of remaining variables
PrevMulti = 0; // column multiplicity on the previous level
fLastLut = 0;
nLuts = 0;
do
{
p = (LUT*) malloc( sizeof(LUT) );
memset( p, 0, sizeof(LUT) );
if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT
{
p->nIns = nVarsRem + PrevMulti;
p->nInsP = PrevMulti;
p->nCols = 2;
p->nMulti = 1;
p->Level = nNames-nVarsRem;
nVarsRem = 0;
PrevMulti = 1;
fLastLut = 1;
}
else // this is not the last LUT
{
p->nIns = s_LutSize;
p->nInsP = PrevMulti;
p->nCols = Profile[nNames-(nVarsRem-(s_LutSize-PrevMulti))];
p->nMulti = Extra_Base2Log(p->nCols);
p->Level = nNames-nVarsRem;
nVarsRem = nVarsRem-(s_LutSize-PrevMulti);
PrevMulti = p->nMulti;
}
if ( p->nMulti >= s_LutSize )
{
printf( "The LUT size is too small\n" );
return 0;
}
nLutOutputsOrig += p->nMulti;
//if ( fVerbose )
//printf( "Stage %2d: In = %3d, InP = %3d, Cols = %5d, Multi = %2d, Level = %2d\n",
// nLuts+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->Level );
// there should be as many columns, codes, and nodes, as there are columns on this level
p->pbCols = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
p->pbCodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
p->paNodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
pLuts[nLuts] = p;
nLuts++;
}
while ( !fLastLut );
//if ( fVerbose )
//printf( "The number of cascades = %d\n", nLuts );
//fprintf( pTable, "%d ", nLuts );
// add the new variables at the bottom
for ( i = 0; i < s_LutSize; i++ )
bCVars[i] = Cudd_bddNewVar(dd);
// for each LUT - assign the LUT and encode the columns
s_EncodingTime = 0;
for ( i = 0; i < nLuts; i++ )
{
int RetValue;
DdNode * bVars[32];
int nVars;
DdNode * bVarsInCube;
DdNode * bVarsCCube;
DdNode * bVarsCube;
int CutLevel;
p = pLuts[i];
// compute the columns of this LUT starting from the given set of nodes with the given codes
// (these codes have been remapped to depend on the topmost variables in the manager)
// for the first LUT, start with the constant 1 BDD
CutLevel = p->Level + p->nIns - p->nInsP;
if ( i == 0 )
RetValue = Extra_bddNodePathsUnderCutArray(
dd, &aFunc, &(b1), 1,
p->paNodes, p->pbCols, CutLevel );
else
RetValue = Extra_bddNodePathsUnderCutArray(
dd, pLuts[i-1]->paNodes, pLuts[i-1]->pbCodes, pLuts[i-1]->nCols,
p->paNodes, p->pbCols, CutLevel );
assert( RetValue == p->nCols );
// at this point, we have filled out p->paNodes[] and p->pbCols[] of this LUT
// pLuts[i-1]->paNodes depended on normal vars
// pLuts[i-1]->pbCodes depended on the topmost variables
// the resulting p->paNodes depend on normal ADD nodes
// the resulting p->pbCols depend on normal vars and topmost variables in the manager
// perform the encoding
// create the cube of these variables
// collect the topmost variables of the manager
nVars = p->nInsP;
for ( v = 0; v < nVars; v++ )
bVars[v] = dd->vars[ dd->invperm[v] ];
bVarsCCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsCCube );
// collect the primary input variables involved in this LUT
nVars = p->nIns - p->nInsP;
for ( v = 0; v < nVars; v++ )
bVars[v] = dd->vars[ dd->invperm[p->Level+v] ];
bVarsInCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsInCube );
// get the cube
bVarsCube = Cudd_bddAnd( dd, bVarsInCube, bVarsCCube ); Cudd_Ref( bVarsCube );
Cudd_RecursiveDeref( dd, bVarsInCube );
Cudd_RecursiveDeref( dd, bVarsCCube );
// get the encoding relation
if ( i == nLuts -1 )
{
DdNode * bVar;
assert( p->nMulti == 1 );
assert( p->nCols == 2 );
assert( Cudd_IsConstant( p->paNodes[0] ) );
assert( Cudd_IsConstant( p->paNodes[1] ) );
bVar = ( p->paNodes[0] == a1 )? bCVars[0]: Cudd_Not( bCVars[0] );
p->bRelation = Cudd_bddIte( dd, bVar, p->pbCols[0], p->pbCols[1] ); Cudd_Ref( p->bRelation );
}
else
{
long clk2 = clock();
// p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation );
p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation );
s_EncodingTime += clock() - clk2;
}
// update the number of LUT outputs
nLutOutputs += (p->nMulti - p->nSimple);
nLutsTotal += p->nMulti;
//if ( fVerbose )
//printf( "Stage %2d: Simple = %d\n", i+1, p->nSimple );
if ( fVerbose )
printf( "Stage %3d: In = %3d InP = %3d Cols = %5d Multi = %2d Simple = %2d Level = %3d\n",
i+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->nSimple, p->Level );
// get the codes from the relation (these are not necessarily cubes)
{
int c;
for ( c = 0; c < p->nCols; c++ )
{
p->pbCodes[c] = Cudd_bddAndAbstract( dd, p->bRelation, p->pbCols[c], bVarsCube ); Cudd_Ref( p->pbCodes[c] );
}
}
Cudd_RecursiveDeref( dd, bVarsCube );
// remap the codes to depend on the topmost varibles of the manager
// useful as a preparation for the next step
{
DdNode ** pbTemp;
int k, v;
pbTemp = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
// create the identical permutation
for ( v = 0; v < dd->size; v++ )
Permute[v] = v;
// use the topmost variables of the manager
// to represent the previous level codes
for ( v = 0; v < p->nMulti; v++ )
Permute[bCVars[v]->index] = dd->invperm[v];
Extra_bddPermuteArray( dd, p->pbCodes, pbTemp, p->nCols, Permute );
// the array pbTemp comes already referenced
// deref the old codes and assign the new ones
for ( k = 0; k < p->nCols; k++ )
{
Cudd_RecursiveDeref( dd, p->pbCodes[k] );
p->pbCodes[k] = pbTemp[k];
}
free( pbTemp );
}
}
if ( fVerbose )
printf( "LUTs: Total = %5d. Final = %5d. Simple = %5d. (%6.2f %%) ",
nLutsTotal, nLutOutputs, nLutsTotal-nLutOutputs, 100.0*(nLutsTotal-nLutOutputs)/nLutsTotal );
if ( fVerbose )
printf( "Memory = %6.2f Mb\n", 1.0*nLutOutputs*(1<<nLutSize)/(1<<20) );
// printf( "\n" );
//fprintf( pTable, "%d ", nLutOutputsOrig );
//fprintf( pTable, "%d ", nLutOutputs );
if ( fVerbose )
{
printf( "Pure decomposition time = %.2f sec\n", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
printf( "Encoding time = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
// printf( "Encoding search time = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) );
// printf( "Encoding compute time = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) );
}
//fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
//fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) );
// write LUTs into the BLIF file
clk1 = clock();
if ( fCheck )
{
FILE * pFile;
// start the file
pFile = fopen( FileName, "w" );
fprintf( pFile, ".model %s\n", FileName );
fprintf( pFile, ".inputs" );
for ( i = 0; i < nNames; i++ )
fprintf( pFile, " %s", pNames[i] );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs F" );
fprintf( pFile, "\n" );
// write the DD into the file
WriteLUTSintoBLIFfile( pFile, dd, pLuts, nLuts, bCVars, pNames, nNames, FileName );
fprintf( pFile, ".end\n" );
fclose( pFile );
if ( fVerbose )
printf( "Output file writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
}
// updo the LUT cascade
for ( i = 0; i < nLuts; i++ )
{
p = pLuts[i];
for ( v = 0; v < p->nCols; v++ )
{
Cudd_RecursiveDeref( dd, p->pbCols[v] );
Cudd_RecursiveDeref( dd, p->pbCodes[v] );
Cudd_RecursiveDeref( dd, p->paNodes[v] );
}
Cudd_RecursiveDeref( dd, p->bRelation );
free( p->pbCols );
free( p->pbCodes );
free( p->paNodes );
free( p );
}
return 1;
}
void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName )
{
int i, v, o;
static char * pNamesLocalIn[MAXINPUTS];
static char * pNamesLocalOut[MAXINPUTS];
static char Buffer[100];
DdNode * bCube, * bCof, * bFunc;
LUT * p;
// go through all the LUTs
for ( i = 0; i < nLuts; i++ )
{
// get the pointer to the LUT
p = pLuts[i];
if ( i == nLuts -1 )
{
assert( p->nMulti == 1 );
}
fprintf( pFile, "#----------------- LUT #%d ----------------------\n", i );
// fill in the names for the current LUT
// write the outputs of the previous LUT
if ( i != 0 )
for ( v = 0; v < p->nInsP; v++ )
{
sprintf( Buffer, "LUT%02d_%02d", i-1, v );
pNamesLocalIn[dd->invperm[v]] = Extra_UtilStrsav( Buffer );
}
// write the primary inputs of the current LUT
for ( v = 0; v < p->nIns - p->nInsP; v++ )
pNamesLocalIn[dd->invperm[p->Level+v]] = Extra_UtilStrsav( pNames[dd->invperm[p->Level+v]] );
// write the outputs of the current LUT
for ( v = 0; v < p->nMulti; v++ )
{
sprintf( Buffer, "LUT%02d_%02d", i, v );
if ( i != nLuts - 1 )
pNamesLocalOut[v] = Extra_UtilStrsav( Buffer );
else
pNamesLocalOut[v] = Extra_UtilStrsav( "F" );
}
// write LUT outputs
// get the prefix
sprintf( Buffer, "L%02d_", i );
// get the cube of encoding variables
bCube = Extra_bddBitsToCube( dd, (1<<p->nMulti)-1, p->nMulti, bCVars, 1 ); Cudd_Ref( bCube );
// write each output of the LUT
for ( o = 0; o < p->nMulti; o++ )
{
// get the cofactor of this output
bCof = Cudd_Cofactor( dd, p->bRelation, bCVars[o] ); Cudd_Ref( bCof );
// quantify the remaining variables to get the function
bFunc = Cudd_bddExistAbstract( dd, bCof, bCube ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bCof );
// write BLIF
sprintf( Buffer, "L%02d_%02d_", i, o );
// WriteDDintoBLIFfileReorder( dd, pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
// does not work well; the advantage is marginal (30%), the run time is huge...
WriteDDintoBLIFfile( pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
Cudd_RecursiveDeref( dd, bFunc );
}
Cudd_RecursiveDeref( dd, bCube );
// clean up the previous local names
for ( v = 0; v < dd->size; v++ )
{
if ( pNamesLocalIn[v] )
free( pNamesLocalIn[v] );
pNamesLocalIn[v] = NULL;
}
for ( v = 0; v < p->nMulti; v++ )
free( pNamesLocalOut[v] );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/bdd/cas/module.make Normal file
View File

@ -0,0 +1,2 @@
SRC += src/bdd/cas/casCore.c \
src/bdd/cas/casDec

14
src/misc/extra/extra.h
View File

@ -147,6 +147,19 @@ extern DdNode * extraBddSpaceFromMatrixNeg( DdManager * dd, DdNode * zA );
extern DdNode * Extra_bddSpaceReduce( DdManager * dd, DdNode * bFunc, DdNode * bCanonVars );
extern DdNode ** Extra_bddSpaceExorGates( DdManager * dd, DdNode * bFuncRed, DdNode * zEquations );
/*=== extraBddCas.c =============================================================*/
/* performs the binary encoding of the set of function using the given vars */
extern DdNode * Extra_bddEncodingBinary( DdManager * dd, DdNode ** pbFuncs, int nFuncs, DdNode ** pbVars, int nVars );
/* solves the column encoding problem using a sophisticated method */
extern DdNode * Extra_bddEncodingNonStrict( DdManager * dd, DdNode ** pbColumns, int nColumns, DdNode * bVarsCol, DdNode ** pCVars, int nMulti, int * pSimple );
/* collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root */
extern st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel );
/* collects the nodes under the cut starting from the given set of ADD nodes */
extern int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel );
/* 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 );
/*=== extraBddMisc.c ========================================================*/
extern DdNode * Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
@ -174,6 +187,7 @@ extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars );
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 );
/*=== extraBddKmap.c ================================================================*/

1230
src/misc/extra/extraBddCas.c Normal file
View File

File diff suppressed because it is too large Load Diff

140
src/misc/extra/extraBddMisc.c
View File

@ -50,6 +50,7 @@
// file "extraDdTransfer.c"
static DdNode * extraTransferPermuteRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute );
static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute );
static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * table, DdNode * node, int *permut ) );
// file "cuddUtils.c"
static void ddSupportStep(DdNode *f, int *support);
@ -916,6 +917,49 @@ DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F )
} /* end of Extra_zddPrimes */
/**Function********************************************************************
Synopsis [Permutes the variables of the array of BDDs.]
Description [Given a permutation in array permut, creates a new BDD
with permuted variables. There should be an entry in array permut
for each variable in the manager. The i-th entry of permut holds the
index of the variable that is to substitute the i-th variable.
The DDs in the resulting array are already referenced.]
SideEffects [None]
SeeAlso [Cudd_addPermute Cudd_bddSwapVariables]
******************************************************************************/
void Extra_bddPermuteArray( DdManager * manager, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut )
{
DdHashTable *table;
int i, k;
do
{
manager->reordered = 0;
table = cuddHashTableInit( manager, 1, 2 );
/* permute the output functions one-by-one */
for ( i = 0; i < nNodes; i++ )
{
bNodesOut[i] = cuddBddPermuteRecur( manager, table, bNodesIn[i], permut );
if ( bNodesOut[i] == NULL )
{
/* deref the array of the already computed outputs */
for ( k = 0; k < i; k++ )
Cudd_RecursiveDeref( manager, bNodesOut[k] );
break;
}
cuddRef( bNodesOut[i] );
}
/* Dispose of local cache. */
cuddHashTableQuit( table );
}
while ( manager->reordered == 1 );
} /* end of Extra_bddPermuteArray */
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
@ -1467,6 +1511,102 @@ DdNode* extraZddPrimes( DdManager *dd, DdNode* F )
}
} /* end of extraZddPrimes */
/**Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddPermute.]
Description [ Recursively puts the BDD in the order given in the array permut.
Checks for trivial cases to terminate recursion, then splits on the
children of this node. Once the solutions for the children are
obtained, it puts into the current position the node from the rest of
the BDD that should be here. Then returns this BDD.
The key here is that the node being visited is NOT put in its proper
place by this instance, but rather is switched when its proper position
is reached in the recursion tree.<p>
The DdNode * that is returned is the same BDD as passed in as node,
but in the new order.]
SideEffects [None]
SeeAlso [Cudd_bddPermute cuddAddPermuteRecur]
******************************************************************************/
static DdNode *
cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
DdHashTable * table /* computed table */ ,
DdNode * node /* BDD to be reordered */ ,
int *permut /* permutation array */ )
{
DdNode *N, *T, *E;
DdNode *res;
int index;
statLine( manager );
N = Cudd_Regular( node );
/* Check for terminal case of constant node. */
if ( cuddIsConstant( N ) )
{
return ( node );
}
/* If problem already solved, look up answer and return. */
if ( N->ref != 1 && ( res = cuddHashTableLookup1( table, N ) ) != NULL )
{
#ifdef DD_DEBUG
bddPermuteRecurHits++;
#endif
return ( Cudd_NotCond( res, N != node ) );
}
/* Split and recur on children of this node. */
T = cuddBddPermuteRecur( manager, table, cuddT( N ), permut );
if ( T == NULL )
return ( NULL );
cuddRef( T );
E = cuddBddPermuteRecur( manager, table, cuddE( N ), permut );
if ( E == NULL )
{
Cudd_IterDerefBdd( manager, T );
return ( NULL );
}
cuddRef( E );
/* Move variable that should be in this position to this position
** by retrieving the single var BDD for that variable, and calling
** cuddBddIteRecur with the T and E we just created.
*/
index = permut[N->index];
res = cuddBddIteRecur( manager, manager->vars[index], T, E );
if ( res == NULL )
{
Cudd_IterDerefBdd( manager, T );
Cudd_IterDerefBdd( manager, E );
return ( NULL );
}
cuddRef( res );
Cudd_IterDerefBdd( manager, T );
Cudd_IterDerefBdd( manager, E );
/* Do not keep the result if the reference count is only 1, since
** it will not be visited again.
*/
if ( N->ref != 1 )
{
ptrint fanout = ( ptrint ) N->ref;
cuddSatDec( fanout );
if ( !cuddHashTableInsert1( table, N, res, fanout ) )
{
Cudd_IterDerefBdd( manager, res );
return ( NULL );
}
}
cuddDeref( res );
return ( Cudd_NotCond( res, N != node ) );
} /* end of cuddBddPermuteRecur */
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/misc/extra/module.make
View File

@ -1,4 +1,5 @@
SRC += src/misc/extra/extraBddAuto.c \
src/misc/extra/extraBddCas.c \
src/misc/extra/extraBddKmap.c \
src/misc/extra/extraBddMisc.c \
src/misc/extra/extraBddSymm.c \

35
src/phys/place/1.txt
View File

@ -1,35 +0,0 @@
Volume in drive C is IBM_PRELOAD
Volume Serial Number is 20EA-F780
Directory of C:\_projects\abc\src\phys\place
02/16/2007 11:01 AM <DIR> .
02/16/2007 11:01 AM <DIR> ..
01/23/2007 10:02 PM 165 1.c
02/16/2007 11:01 AM 0 1.txt
02/10/2007 05:52 PM 1,103,488 ac97_emap.fastplace.pl
02/09/2007 04:37 PM 362,675 ac97_emap.initial.pl
02/09/2007 03:34 PM 1,247,692 ac97_emap.nets
02/09/2007 03:34 PM 294,862 ac97_emap.nodes
02/13/2007 12:19 AM 670,459 ac97_emap.pl
02/10/2007 05:52 PM 1,184 hpwl
02/10/2007 01:52 AM 551 libhmetis.h
02/13/2007 12:25 AM 625 Makefile
02/13/2007 12:16 AM 9,552 place_base.c
02/16/2007 10:29 AM 3,801 place_base.h
02/13/2007 12:08 AM 8,175 place_bin.c
02/13/2007 12:16 AM 9,263 place_genqp.c
02/13/2007 12:08 AM 4,950 place_gordian.c
02/13/2007 12:18 AM 1,886 place_gordian.h
02/13/2007 12:08 AM 514 place_legalize.c
02/13/2007 12:08 AM 4,900 place_pads.c
02/13/2007 12:17 AM 36,942 place_partition.c
02/13/2007 12:08 AM 29,189 place_qpsolver.c
02/13/2007 12:08 AM 4,882 place_qpsolver.h
02/13/2007 12:08 AM 9,454 place_test.c
02/12/2007 05:01 PM 1,577 README
02/10/2007 04:26 PM 114 test.nets
02/10/2007 04:25 PM 112 test.nodes
02/11/2007 03:31 PM 130 test.pl
26 File(s) 3,807,142 bytes
2 Dir(s) 1,486,884,864 bytes free

16989
src/phys/place/ac97_emap.fastplace.pl
View File

File diff suppressed because it is too large Load Diff

16972
src/phys/place/ac97_emap.initial.pl
View File

File diff suppressed because it is too large Load Diff

61818
src/phys/place/ac97_emap.nets
View File

File diff suppressed because it is too large Load Diff

16973
src/phys/place/ac97_emap.nodes
View File

File diff suppressed because it is too large Load Diff

16971
src/phys/place/ac97_emap.pl
View File

File diff suppressed because it is too large Load Diff

4
src/phys/place/module.make
View File

@ -5,4 +5,6 @@ SRC += src/phys/place/place_base.c \
src/phys/place/place_legalize.c \
src/phys/place/place_pads.c \
src/phys/place/place_partition.c \
src/phys/place/place_qpsolver.c
src/phys/place/place_qpsolver.c \
src/phys/place/place_io.c \
src/phys/place/place_inc.c

5
src/phys/place/place_base.c
View File

@ -112,6 +112,8 @@ void addConcreteNet(ConcreteNet *net) {
assert(net);
assert(net->m_id >= 0);
if (net->m_id >= g_place_concreteNetsSize) {
g_place_concreteNetsSize = (net->m_id > g_place_concreteNetsSize ?
net->m_id : g_place_concreteNetsSize);
g_place_concreteNetsSize *= 1.5;
g_place_concreteNetsSize += 20;
g_place_concreteNets = (ConcreteNet**)realloc(g_place_concreteNets,
@ -122,6 +124,7 @@ void addConcreteNet(ConcreteNet *net) {
memset(&(g_place_concreteNets[g_place_numNets]), 0,
sizeof(ConcreteNet*)*(net->m_id+1-g_place_numNets));
g_place_numNets = net->m_id+1;
assert(g_place_numNets <= g_place_concreteNetsSize);
}
g_place_concreteNets[net->m_id] = net;
}
@ -150,6 +153,8 @@ void addConcreteCell(ConcreteCell *cell) {
assert(cell);
assert(cell->m_id >= 0);
if (cell->m_id >= g_place_concreteCellsSize) {
g_place_concreteCellsSize = (cell->m_id > g_place_concreteCellsSize ?
cell->m_id : g_place_concreteCellsSize);
g_place_concreteCellsSize *= 1.5;
g_place_concreteCellsSize += 20;
g_place_concreteCells = (ConcreteCell**)realloc(g_place_concreteCells,

24
src/phys/place/place_base.h
View File

@ -6,7 +6,7 @@
// ahurst@eecs.berkeley.edu
//
/*===================================================================*/
#if !defined(PLACE_BASE_H_)
#define PLACE_BASE_H_
@ -37,7 +37,9 @@ typedef struct Rect {
typedef struct AbstractCell {
char *m_label; // string description
float m_width, m_height; // dimensions
bool m_pad; // a pad (external I/O) cell?
} AbstractCell;
@ -45,11 +47,15 @@ typedef struct AbstractCell {
// --- ConcreteCell - a design object
typedef struct ConcreteCell {
AbstractCell *m_parent; // cell type
char *m_label; // string description
int m_id; // a unique ID (see below)
char *m_label; // string description
AbstractCell *m_parent; // cell type
bool m_fixed; // position is fixed?
float m_x, m_y; // center of cell
int m_data;
} ConcreteCell;
@ -57,9 +63,13 @@ typedef struct ConcreteCell {
typedef struct ConcreteNet {
int m_id; // a unique ID (see below)
int m_numTerms; // num. of connected cells
ConcreteCell **m_terms; // connected cells
float m_weight; // relative weight
int m_data;
} ConcreteNet;
@ -102,15 +112,17 @@ void globalPlace();
void globalIncremental();
void globalFixDensity(int numBins, float maxMovement);
float fastUnplace(ConcreteCell *cell); // UNIMPLEMENTED
float fastPlace(int numCells, ConcreteCell *cells []); // UNIMPLEMENTED
float fastEstimate(int numCells, ConcreteCell *cells []); // UNIMPLEMENTED
float fastEstimate(ConcreteCell *cell,
int numNets, ConcreteNet *nets[]);
float fastTopoPlace(int numCells, ConcreteCell *cells[],
int numNets, ConcreteNet *nets[]);
Rect getNetBBox(const ConcreteNet *net);
float getNetWirelength(const ConcreteNet *net);
float getTotalWirelength();
float getCellArea(const ConcreteCell *cell);
void writeBookshelf(const char *filename);
// comparative qsort-style functions
int netSortByL(const void *a, const void *b);

30
src/phys/place/place_bin.c
View File

@ -13,6 +13,8 @@
#include <limits.h>
#include <assert.h>
//#define DEBUG
#include "place_base.h"
// --------------------------------------------------------------------
@ -93,7 +95,9 @@ void spreadDensityX(int numBins, float maxMovement) {
memcpy(binCells, &(allCells[yBinStart]), sizeof(ConcreteCell*)*yBinCount);
qsort(binCells, yBinCount, sizeof(ConcreteCell*), cellSortByX);
// printf("y-bin %d count=%d area=%f\n",y,yBinCount, yBinArea);
#if defined(DEBUG)
printf("y-bin %d count=%d area=%f\n",y,yBinCount, yBinArea);
#endif
x = 0;
xBinCount = 0, xBinStart = 0;
@ -109,6 +113,8 @@ void spreadDensityX(int numBins, float maxMovement) {
xBinCount++;
curOldEdge = xCell->m_x;
printf("%.3f ", xCell->m_x);
// have we filled up an x-bin?
if (xCumArea >= yBinArea*(x+1)/numBins && xBinArea > 0) {
curNewEdge = lastNewEdge + g_place_coreBounds.w*xBinArea/yBinArea;
@ -118,21 +124,28 @@ void spreadDensityX(int numBins, float maxMovement) {
if ((curNewEdge-curOldEdge)>maxMovement) curNewEdge = curOldEdge + maxMovement;
if ((curOldEdge-curNewEdge)>maxMovement) curNewEdge = curOldEdge - maxMovement;
#if defined(DEBUG)
printf("->\tx-bin %d count=%d area=%f (%f,%f)->(%f,%f)\n",x, xBinCount, xBinArea,
curOldEdge, lastOldEdge, curNewEdge, lastNewEdge);
#endif
stretch = (curNewEdge-lastNewEdge)/(curOldEdge-lastOldEdge);
// stretch!
for(c3=xBinStart; c3<xBinStart+xBinCount; c3++) {
binCells[c3]->m_x = lastNewEdge+(binCells[c3]->m_x-lastOldEdge)*stretch;
// force within core
if (curOldEdge == lastOldEdge)
binCells[c3]->m_x = lastNewEdge+(c3-xBinStart)*(curNewEdge-lastNewEdge);
else
binCells[c3]->m_x = lastNewEdge+(binCells[c3]->m_x-lastOldEdge)*stretch;
// force within core
w = binCells[c3]->m_parent->m_width*0.5;
if (binCells[c3]->m_x-w < g_place_coreBounds.x)
binCells[c3]->m_x = g_place_coreBounds.x+w;
if (binCells[c3]->m_x+w > g_place_coreBounds.x+g_place_coreBounds.w)
binCells[c3]->m_x = g_place_coreBounds.x+g_place_coreBounds.w-w;
}
lastOldEdge = curOldEdge;
lastNewEdge = curNewEdge;
x++;
@ -141,7 +154,7 @@ void spreadDensityX(int numBins, float maxMovement) {
xBinStart = c2+1;
}
}
y++;
yBinCount = 0;
yBinArea = 0;
@ -228,6 +241,7 @@ void spreadDensityY(int numBins, float maxMovement) {
if ((curNewEdge-curOldEdge)>maxMovement) curNewEdge = curOldEdge + maxMovement;
if ((curOldEdge-curNewEdge)>maxMovement) curNewEdge = curOldEdge - maxMovement;
if (curOldEdge == lastOldEdge) continue; // hmmm
stretch = (curNewEdge-lastNewEdge)/(curOldEdge-lastOldEdge);
// stretch!

106
src/phys/place/place_inc.c Normal file
View File

@ -0,0 +1,106 @@
/*===================================================================*/
//
// place_inc.c
//
// Aaron P. Hurst, 2003-2007
// ahurst@eecs.berkeley.edu
//
/*===================================================================*/
#include <stdlib.h>
#include <limits.h>
#include <assert.h>
#include <string.h>
#include "place_base.h"
#include "place_gordian.h"
inline int sqHashId(int id, int max) {
return ((id * (id+17)) % max);
}
#if 0
// --------------------------------------------------------------------
// fastPlace()
//
/// The first cell is assumed to be the "output".
// --------------------------------------------------------------------
float fastPlace(int numCells, ConcreteCell *cells[],
int numNets, ConcreteNet *nets[]) {
int n, t, c, i, local_id = 0, pass;
const int NUM_PASSES = 4;
int *cell_numTerms = calloc(numCells, sizeof(int));
ConcreteNet **cell_terms;
ConcreteNet *net;
Rect outputBox;
outputBox = getNetBBox(nets[0]);
// assign local ids
// put cells in reasonable initial location
for(n=0; n<numNets; n++)
for(t=0; nets[n]->m_numTerms; t++)
nets[n]->m_terms[t]->m_data = -1;
for(c=0; c<numCells; c++) {
cells[c]->m_data = local_id;
cells[c]->m_x = outputBox.x + 0.5*outputBox.w;
cells[c]->m_y = outputBox.y + 0.5*outputBox.h;
}
// build reverse map of cells to nets
for(n=0; n<numNets; n++)
for(t=0; nets[n]->m_numTerms; t++) {
local_id = nets[n]->m_terms[t]->m_data;
if (local_id >= 0)
cell_numTerms[local_id]++;
}
for(c=0; c<numCells; c++) {
cell_terms[c] = malloc(sizeof(ConcreteNet*)*cell_numTerms[c]);
cell_numTerms[c] = 0;
}
for(n=0; n<numNets; n++)
for(t=0; nets[n]->m_numTerms; t++) {
local_id = nets[n]->m_terms[t]->m_data;
if (local_id >= 0)
cell_terms[cell_numTerms[local_id]++] = nets[n];
}
// topological order?
// iterative linear
for(pass=0; pass<NUM_PASSES; pass++)
for(c=0; c<numCells; c++) {
for(n=0; n<cell_numTerms[c]; n++) {
net = cell_terms[c];
for(t=0; t<net->m_numTerms; t++);
}
}
}
#endif
// --------------------------------------------------------------------
// fastEstimate()
//
// --------------------------------------------------------------------
float fastEstimate(ConcreteCell *cell,
int numNets, ConcreteNet *nets[]) {
float len = 0;
int n;
Rect box;
assert(cell);
for(n=0; n<numNets; n++) {
box = getNetBBox(nets[n]);
if (cell->m_x < box.x) len += (box.x - cell->m_x);
if (cell->m_x > box.x+box.w) len += (cell->m_x-box.x-box.w);
if (cell->m_y < box.y) len += (box.x - cell->m_y);
if (cell->m_y > box.y+box.h) len += (cell->m_y-box.y-box.h);
}
return len;
}

94
src/phys/place/place_io.c Normal file
View File

@ -0,0 +1,94 @@
/*===================================================================*/
//
// place_io.c
//
// Aaron P. Hurst, 2003-2007
// ahurst@eecs.berkeley.edu
//
/*===================================================================*/
#include <stdlib.h>
#include <limits.h>
#include <assert.h>
#include <string.h>
#include <stdio.h>
#include "place_base.h"
// --------------------------------------------------------------------
// writeBookshelfNodes()
//
// --------------------------------------------------------------------
void writeBookshelfNodes(const char *filename) {
int c = 0;
int numNodes, numTerms;
FILE *nodesFile = fopen(filename, "w");
if (!nodesFile) {
printf("ERROR: Could not open .nodes file\n");
exit(1);
}
numNodes = numTerms = 0;
for(c=0; c<g_place_numCells; c++) if (g_place_concreteCells[c]) {
numNodes++;
if (g_place_concreteCells[c]->m_parent->m_pad)
numTerms++;
}
fprintf(nodesFile, "UCLA nodes 1.0\n");
fprintf(nodesFile, "NumNodes : %d\n", numNodes);
fprintf(nodesFile, "NumTerminals : %d\n", numTerms);
for(c=0; c<g_place_numCells; c++) if (g_place_concreteCells[c]) {
fprintf(nodesFile, "CELL%d %f %f %s\n",
g_place_concreteCells[c]->m_id,
g_place_concreteCells[c]->m_parent->m_width,
g_place_concreteCells[c]->m_parent->m_height,
(g_place_concreteCells[c]->m_parent->m_pad ? " terminal" : ""));
}
fclose(nodesFile);
}
// --------------------------------------------------------------------
// writeBookshelfPl()
//
// --------------------------------------------------------------------
void writeBookshelfPl(const char *filename) {
int c = 0;
FILE *plFile = fopen(filename, "w");
if (!plFile) {
printf("ERROR: Could not open .pl file\n");
exit(1);
}
fprintf(plFile, "UCLA pl 1.0\n");
for(c=0; c<g_place_numCells; c++) if (g_place_concreteCells[c]) {
fprintf(plFile, "CELL%d %f %f : N %s\n",
g_place_concreteCells[c]->m_id,
g_place_concreteCells[c]->m_x,
g_place_concreteCells[c]->m_y,
(g_place_concreteCells[c]->m_fixed ? "\\FIXED" : ""));
}
fclose(plFile);
}
// --------------------------------------------------------------------
// writeBookshelf()
//
// --------------------------------------------------------------------
void writeBookshelf(const char *filename) {
writeBookshelfNodes("out.nodes");
writeBookshelfPl("out.pl");
}

9
src/phys/place/test.nets
View File

@ -1,9 +0,0 @@
UCLA nets 1.0
NumNets : 2
NumPins : 4
NetDegree 2 :
0 pin : 0 0
3 pin : 0 0
NetDegree 2 :
2 pin : 0 0
3 pin : 0 0

7
src/phys/place/test.nodes
View File

@ -1,7 +0,0 @@
UCLA nodes 1.0
NumNodes : 4
NumTerminals : 3
0 1.0 1.0 terminal
1 1.0 1.0 terminal
2 1.0 1.0 terminal
3 1.0 1.0

5
src/phys/place/test.pl
View File

@ -1,5 +0,0 @@
UCLA pl 1.0
0 0.000000 0.000000 : N \FIXED
1 5.000000 5.000000 : N \FIXED
2 0.000000 5.000000 : N \FIXED
3 4.500000 2.500000 : N