Skip to content

A
abc
Commit 2fd3c1a2 by Alan Mishchenko
Options

Version abc60820

parent eb2a5b43
Showing with 4072 additions and 233 deletions
abc.dsp
......@@ -242,6 +242,10 @@ SOURCE=.\src\base\abci\abcNtbdd.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcOrder.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcPga.c
# End Source File
# Begin Source File
......@@ -2150,7 +2154,7 @@ SOURCE=.\src\temp\ivy\ivyResyn.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\ivyRwrPre.c
SOURCE=.\src\temp\ivy\ivyRwr.c
# End Source File
# Begin Source File
......@@ -2158,6 +2162,10 @@ SOURCE=.\src\temp\ivy\ivySeq.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\ivyShow.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ivy\ivyTable.c
# End Source File
# Begin Source File
......@@ -2253,6 +2261,30 @@ SOURCE=.\src\temp\mem\mem.c
SOURCE=.\src\temp\mem\mem.h
# End Source File
# End Group
# Begin Group "ver"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\temp\ver\ver.h
# End Source File
# Begin Source File
SOURCE=.\src\temp\ver\verCore.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ver\verFormula.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ver\verParse.c
# End Source File
# Begin Source File
SOURCE=.\src\temp\ver\verStream.c
# End Source File
# End Group
# End Group
# End Group
# Begin Group "Header Files"
......
abc.rc
......@@ -2,8 +2,8 @@
#set check # checks intermediate networks
#set checkfio # prints warnings when fanins/fanouts are duplicated
#set checkread # checks new networks after reading from file
#set backup # saves backup networks retrived by "undo" and "recall"
#set savesteps 1 # sets the maximum number of backup networks to save
set backup # saves backup networks retrived by "undo" and "recall"
set savesteps 1 # sets the maximum number of backup networks to save
set progressbar # display the progress bar
# program names for internal calls
......@@ -49,6 +49,8 @@ alias rb read_bench
alias ret retime
alias rp read_pla
alias rv read_verilog
alias rvv read_ver
alias rvl read_verlib
alias rsup read_super mcnc5_old.super
alias rlib read_library
alias rw rewrite
......
src/base/abc/abc.h
......@@ -462,6 +462,7 @@ 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 bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
......@@ -503,6 +504,7 @@ extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
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_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 );
......@@ -519,6 +521,7 @@ extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
......
src/base/abc/abcDfs.c
......@@ -256,6 +256,37 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int i;
// set the traversal ID
Abc_NtkIncrementTravId( pNtk );
// start the array of nodes
vNodes = Vec_PtrAlloc( 100 );
// go through the PO nodes and call for each of them
Abc_NtkForEachCo( pNtk, pNode, i )
Abc_NtkNodeSupport_rec( Abc_ObjFanin0(pNode), vNodes );
// add unused CIs
Abc_NtkForEachCi( pNtk, pNode, i )
if ( !Abc_NodeIsTravIdCurrent( pNode ) )
Vec_PtrPush( vNodes, pNode );
assert( Vec_PtrSize(vNodes) == Abc_NtkCiNum(pNtk) );
return vNodes;
}
/**Function*************************************************************
Synopsis [Returns the set of CI nodes in the support of the given nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes )
{
Vec_Ptr_t * vNodes;
......
src/base/abc/abcNetlist.c
......@@ -54,10 +54,10 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
if ( pNtk->tName2Model )
return Abc_NtkNetlistToLogicHie( pNtk );
// start the network
if ( !Abc_NtkHasMapping(pNtk) )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
else
if ( Abc_NtkHasMapping(pNtk) )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
else
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, pNtk->ntkFunc );
// duplicate the nodes
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_NtkDupObj(pNtkNew, pObj);
......
src/base/abc/abcNtk.c
......@@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
}
else if ( Abc_NtkHasMapping(pNtk) )
pNtk->pManFunc = Abc_FrameReadLibGen();
else
else if ( !Abc_NtkHasBlackbox(pNtk) )
assert( 0 );
// allocate constant node
if ( !Abc_NtkIsNetlist(pNtk) )
......
src/base/abc/abcObj.c
......@@ -409,6 +409,29 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName )
/**Function*************************************************************
Synopsis [Returns the net with the given name.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet;
int ObjId;
assert( !Abc_NtkIsNetlist(pNtk) );
ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL );
if ( ObjId == -1 )
return NULL;
pNet = Abc_NtkObj( pNtk, ObjId );
return pNet;
}
/**Function*************************************************************
Synopsis [Finds or creates the net.]
Description []
......@@ -568,7 +591,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
else if ( Abc_NtkHasMapping(pNtk) )
pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen());
else
else if ( !Abc_NtkHasBlackbox(pNtk) )
assert( 0 );
return pNode;
}
......@@ -596,7 +619,7 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
else if ( Abc_NtkHasMapping(pNtk) )
pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen());
else
else if ( !Abc_NtkHasBlackbox(pNtk) )
assert( 0 );
return pNode;
}
......
src/base/abc/abcShow.c
......@@ -30,7 +30,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_ShowFile( char * FileNameDot );
extern void Abc_ShowFile( char * FileNameDot );
static void Abc_ShowGetFileName( char * pName, char * pBuffer );
////////////////////////////////////////////////////////////////////////
......
src/base/abc/abcUtil.c
......@@ -251,7 +251,12 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
TotalArea = 0.0;
Abc_NtkForEachNode( pNtk, pNode, i )
{
assert( pNode->pData );
// assert( pNode->pData );
if ( pNode->pData == NULL )
{
printf( "Node without mapping is encountered.\n" );
continue;
}
TotalArea += Mio_GateReadArea( pNode->pData );
}
return TotalArea;
......
src/base/abci/abc.c
......@@ -74,6 +74,7 @@ static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
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_CommandOneOutput ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -192,6 +193,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 );
Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 );
Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 );
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", "cone", Abc_CommandOneOutput, 1 );
......@@ -1627,6 +1629,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int fVerbose;
int fBddSizeMax;
int fDualRail;
int fReorder;
......@@ -1637,11 +1640,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 1;
fReorder = 1;
fDualRail = 0;
fBddSizeMax = 1000000;
fBddSizeMax = 50000000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Brdvh" ) ) != EOF )
{
switch ( c )
{
......@@ -1659,6 +1663,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDualRail ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'r':
fReorder ^= 1;
break;
......@@ -1683,11 +1690,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
......@@ -1700,11 +1707,12 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" );
fprintf( pErr, "usage: collapse [-B num] [-rdvh]\n" );
fprintf( pErr, "\t collapses the network by constructing global BDDs\n" );
fprintf( pErr, "\t-B num : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
fprintf( pErr, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
fprintf( pErr, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
......@@ -3462,6 +3470,93 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr, * pFile;
Abc_Ntk_t * pNtk;
char * pFileName;
int c;
int fReverse;
int fVerbose;
extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fReverse = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
{
switch ( c )
{
case 'r':
fReverse ^= 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 )
// {
// printf( "Currently this procedure does not work for sequential networks.\n" );
// return 1;
// }
// if the var order file is given, implement this order
pFileName = NULL;
if ( argc == globalUtilOptind + 1 )
{
pFileName = argv[globalUtilOptind];
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
return 1;
}
fclose( pFile );
}
if ( pFileName )
Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
else
Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: order [-rvh] <file>\n" );
fprintf( pErr, "\t computes a good static CI variable order\n" );
fprintf( pErr, "\t-r : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
......@@ -4583,7 +4678,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
// run the command
// pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
// pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -5105,21 +5201,36 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c, fUpdateLevel, fVerbose;
extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose );
int c, fUseZeroCost, fVerbose, nIters;
extern Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fUpdateLevel = 1;
nIters = 3;
fUseZeroCost = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "zvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
goto usage;
}
nIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIters < 0 )
goto usage;
break;
case 'z':
fUseZeroCost ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -5140,7 +5251,7 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
pNtkRes = Abc_NtkIvyHaig( pNtk, fVerbose );
pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -5151,9 +5262,10 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: haig [-vh]\n" );
fprintf( pErr, "\t prints HAIG stats after one round of sequential rewriting\n" );
// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "usage: haig [-Izvh]\n" );
fprintf( pErr, "\t prints HAIG stats after sequential rewriting\n" );
fprintf( pErr, "\t-I num : the number of rewriting iterations [default = %d]\n", nIters );
fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/abcClpBdd.c
......@@ -46,14 +46,17 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
int clk = clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
return NULL;
if ( fVerbose )
printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
{
printf( "The shared BDD size is %d nodes. ", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
PRT( "BDD construction time", clock() - clk );
}
// create the new network
if ( fDualRail )
......
src/base/abci/abcIvy.c
......@@ -27,7 +27,7 @@
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
static Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
static Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig );
static Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
......@@ -120,17 +120,17 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq )
Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig )
{
Abc_Ntk_t * pNtkAig;
int nNodes, fCleanup = 1;
// convert from the AIG manager
if ( fSeq )
pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan, fHaig );
else
pNtkAig = Abc_NtkFromAig( pNtk, pMan );
// report the cleanup results
if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
......@@ -163,11 +163,11 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
......@@ -179,21 +179,28 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int fVerbose )
Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
int i;
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
Ivy_ManHaigStart( pMan );
Ivy_ManRewriteSeq( pMan, 0, fVerbose );
Ivy_ManHaigPrintStats( pMan );
Ivy_ManHaigStop( pMan );
Ivy_ManHaigStart( pMan, fVerbose );
Ivy_ManRewriteSeq( pMan, 0, 0 );
for ( i = 1; i < nIters; i++ )
Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
Ivy_ManHaigPostprocess( pMan, fVerbose );
// write working AIG into the current network
// pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
// write HAIG into the current network
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 );
// pNtkAig = Abc_NtkIvyAfterHaig( pNtk, pMan, 1 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
Ivy_ManHaigStop( pMan );
Ivy_ManStop( pMan );
return pNtkAig;
}
......@@ -239,7 +246,7 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
if ( pMan == NULL )
return NULL;
Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
......@@ -263,7 +270,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
if ( pMan == NULL )
return NULL;
Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
// Ivy_ManRewriteSeq( pMan, 1, 0 );
// Ivy_ManRewriteSeq( pMan, 1, 0 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
......@@ -288,7 +297,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
return NULL;
pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
Ivy_ManStop( pTemp );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
......@@ -474,14 +483,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig )
{
Vec_Int_t * vNodes, * vLatches;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
Ivy_Obj_t * pNode;
Ivy_Obj_t * pNode, * pTemp;
int i;
assert( Ivy_ManLatchNum(pMan) > 0 );
// assert( Ivy_ManLatchNum(pMan) > 0 );
// perform strashing
pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
......@@ -493,7 +502,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
{
pObjNew = Abc_NtkCreateLatch( pNtk );
if ( Ivy_ObjInit(pNode) == IVY_INIT_DC )
if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC )
Abc_LatchSetInitDc( pObjNew );
else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
Abc_LatchSetInit1( pObjNew );
......@@ -505,14 +514,14 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
// rebuild the AIG
Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
{
// add the first fanins
// add the first fanin
pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
if ( Ivy_ObjIsBuf(pNode) )
{
pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
continue;
}
// add the first second
// add the second fanin
pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
// create the new node
if ( Ivy_ObjIsExor(pNode) )
......@@ -520,6 +529,22 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
else
pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
pNode->TravId = Abc_EdgeFromNode( pObjNew );
// process the choice nodes
if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
{
pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
pFaninNew->fPhase = 0;
assert( !Ivy_IsComplement(pNode->pEquiv) );
for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
pFaninNew->pData = pFaninNew1;
pFaninNew = pFaninNew1;
}
pFaninNew->pData = NULL;
// printf( "Writing choice node %d.\n", pNode->Id );
}
}
// connect the PO nodes
Abc_NtkForEachPo( pNtkOld, pObj, i )
......
src/base/abci/abcMiter.c
......@@ -27,7 +27,6 @@
static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
static void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
......
src/base/abci/abcNtbdd.c
......@@ -246,35 +246,47 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
{
ProgressBar * pProgress;
Vec_Ptr_t * vFuncsGlob;
Abc_Obj_t * pNode;
Abc_Obj_t * pNode, * pFanin;
DdNode * bFunc;
DdManager * dd;
int i, Counter;
int i, k, Counter;
// remove dangling nodes
Abc_AigCleanup( pNtk->pManFunc );
// start the manager
assert( pNtk->pManGlob == NULL );
dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// set reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
// set the elementary variables
// clean storage for local BDDs
Abc_NtkCleanCopy( pNtk );
// set the elementary variables
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (Abc_Obj_t *)dd->vars[i];
if ( Abc_ObjFanoutNum(pNode) > 0 )
{
pNode->pCopy = (Abc_Obj_t *)dd->vars[i];
Cudd_Ref( dd->vars[i] );
}
// assign the constant node BDD
pNode = Abc_NtkConst1( pNtk );
pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one );
if ( Abc_ObjFanoutNum(pNode) > 0 )
{
pNode->pCopy = (Abc_Obj_t *)dd->one;
Cudd_Ref( dd->one );
}
// collect the global functions of the COs
vFuncsGlob = Vec_PtrAlloc( 100 );
Counter = 0;
vFuncsGlob = Vec_PtrAlloc( 100 );
if ( fLatchOnly )
{
// construct the BDDs
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pNode, i )
{
// Extra_ProgressBarUpdate( pProgress, i, NULL );
bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
if ( bFunc == NULL )
{
......@@ -295,7 +307,6 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
{
// Extra_ProgressBarUpdate( pProgress, i, NULL );
bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
if ( bFunc == NULL )
{
......@@ -305,12 +316,12 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
Cudd_Quit( dd );
return NULL;
}
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
/*
// derefence the intermediate BDDs
Abc_NtkForEachNode( pNtk, pNode, i )
if ( pNode->pCopy )
......@@ -318,6 +329,22 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
pNode->pCopy = NULL;
}
*/
/*
// make sure all nodes are derefed
Abc_NtkForEachObj( pNtk, pNode, i )
{
if ( pNode->pCopy != NULL )
printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id );
if ( pNode->vFanouts.nSize > 0 )
printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id );
}
*/
// reset references
Abc_NtkForEachObj( pNtk, pNode, i )
Abc_ObjForEachFanin( pNode, pFanin, k )
pFanin->vFanouts.nSize++;
// reorder one more time
if ( fReorder )
{
......@@ -326,6 +353,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
}
pNtk->pManGlob = dd;
pNtk->vFuncsGlob = vFuncsGlob;
// Cudd_PrintInfo( dd, stdout );
return dd;
}
......@@ -342,7 +370,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
***********************************************************************/
DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
{
DdNode * bFunc, * bFunc0, * bFunc1;
DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
assert( !Abc_ObjIsComplement(pNode) );
if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
{
......@@ -353,29 +381,87 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
return NULL;
}
// if the result is available return
if ( pNode->pCopy )
return (DdNode *)pNode->pCopy;
// compute the result for both branches
bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc0 == NULL )
return NULL;
Cudd_Ref( bFunc0 );
bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc1 == NULL )
return NULL;
Cudd_Ref( bFunc1 );
bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
// get the final result
bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bFunc0 );
Cudd_RecursiveDeref( dd, bFunc1 );
// set the result
assert( pNode->pCopy == NULL );
pNode->pCopy = (Abc_Obj_t *)bFunc;
// increment the progress bar
if ( pProgress )
Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
if ( pNode->pCopy == NULL )
{
Abc_Obj_t * pNodeC, * pNode0, * pNode1;
pNode0 = Abc_ObjFanin0(pNode);
pNode1 = Abc_ObjFanin1(pNode);
// check for the special case when it is MUX/EXOR
// if ( 0 )
if ( pNode0->pCopy == NULL && pNode1->pCopy == NULL &&
Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 &&
Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 &&
Abc_NodeIsMuxType(pNode) )
{
// deref the fanins
pNode0->vFanouts.nSize--;
pNode1->vFanouts.nSize--;
// recognize the MUX
pNodeC = Abc_NodeRecognizeMux( pNode, &pNode1, &pNode0 );
assert( Abc_ObjFanoutNum(pNodeC) > 1 );
// dereference the control once (the second time it will be derefed when BDDs are computed)
pNodeC->vFanouts.nSize--;
// compute the result for all branches
bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFuncC == NULL )
return NULL;
Cudd_Ref( bFuncC );
bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc0 == NULL )
return NULL;
Cudd_Ref( bFunc0 );
bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc1 == NULL )
return NULL;
Cudd_Ref( bFunc1 );
// complement the branch BDDs
bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjIsComplement(pNode0) );
bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjIsComplement(pNode1) );
// get the final result
bFunc = Cudd_bddIte( dd, bFuncC, bFunc1, bFunc0 ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bFunc0 );
Cudd_RecursiveDeref( dd, bFunc1 );
Cudd_RecursiveDeref( dd, bFuncC );
// add the number of used nodes
(*pCounter) += 3;
}
else
{
// compute the result for both branches
bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc0 == NULL )
return NULL;
Cudd_Ref( bFunc0 );
bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose );
if ( bFunc1 == NULL )
return NULL;
Cudd_Ref( bFunc1 );
bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
// get the final result
bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bFunc0 );
Cudd_RecursiveDeref( dd, bFunc1 );
// add the number of used nodes
(*pCounter)++;
}
// set the result
assert( pNode->pCopy == NULL );
pNode->pCopy = (Abc_Obj_t *)bFunc;
// increment the progress bar
if ( pProgress )
Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
}
// prepare the return value
bFunc = (DdNode *)pNode->pCopy;
// dereference BDD at the node
if ( --pNode->vFanouts.nSize == 0 )
{
Cudd_Deref( bFunc );
pNode->pCopy = NULL;
}
return bFunc;
}
......
src/base/abci/abcOrder.c 0 → 100644
/**CFile****************************************************************
FileName [abcOrder.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Exploring static BDD variable orders.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcOrder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Changes the order of primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose )
{
Vec_Ptr_t * vSupp;
vSupp = Abc_NtkSupport( pNtk );
Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
Vec_PtrFree( vSupp );
}
/**Function*************************************************************
Synopsis [Implements the given variable order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose )
{
char Buffer[1000];
FILE * pFile;
Vec_Ptr_t * vSupp;
Abc_Obj_t * pObj;
pFile = fopen( pFileName, "r" );
vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) );
while ( fscanf( pFile, "%s", Buffer ) == 1 )
{
pObj = Abc_NtkFindTerm( pNtk, Buffer );
if ( pObj == NULL || !Abc_ObjIsCi(pObj) )
{
printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer );
Vec_PtrFree( vSupp );
fclose( pFile );
return;
}
Vec_PtrPush( vSupp, pObj );
}
fclose( pFile );
if ( Vec_PtrSize(vSupp) != Abc_NtkCiNum(pNtk) )
{
printf( "The number of names in the order (%d) is not the same as the number of PIs (%d).\n", Vec_PtrSize(vSupp), Abc_NtkCiNum(pNtk) );
Vec_PtrFree( vSupp );
return;
}
Abc_NtkChangeCiOrder( pNtk, vSupp, fReverse );
Vec_PtrFree( vSupp );
}
/**Function*************************************************************
Synopsis [Changes the order of primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkChangeCiOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vSupp, int fReverse )
{
Abc_Obj_t * pObj;
int i;
assert( Vec_PtrSize(vSupp) == Abc_NtkCiNum(pNtk) );
// order CIs using the array
if ( fReverse )
Vec_PtrForEachEntry( vSupp, pObj, i )
Vec_PtrWriteEntry( pNtk->vCis, Vec_PtrSize(vSupp)-1-i, pObj );
else
Vec_PtrForEachEntry( vSupp, pObj, i )
Vec_PtrWriteEntry( pNtk->vCis, i, pObj );
// order PIs accordingly
Vec_PtrClear( pNtk->vPis );
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjIsPi(pObj) )
Vec_PtrPush( pNtk->vPis, pObj );
// Abc_NtkForEachCi( pNtk, pObj, i )
// printf( "%s ", Abc_ObjName(pObj) );
// printf( "\n" );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/module.make
......@@ -15,6 +15,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcMap.c \
src/base/abci/abcMiter.c \
src/base/abci/abcNtbdd.c \
src/base/abci/abcOrder.c \
src/base/abci/abcPga.c \
src/base/abci/abcPrint.c \
src/base/abci/abcProve.c \
......
src/base/io/io.c
......@@ -32,6 +32,8 @@ static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVer ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
......@@ -45,6 +47,7 @@ static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
////////////////////////////////////////////////////////////////////////
......@@ -71,6 +74,8 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_ver", IoCommandReadVer, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verlib", IoCommandReadVerLib, 0 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
......@@ -84,6 +89,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
}
......@@ -659,6 +665,209 @@ usage:
SeeAlso []
***********************************************************************/
int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pTemp;
st_table * tDesign;
char * FileName;
FILE * pFile;
int fCheck;
int c;
extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
}
fclose( pFile );
// set the new network
tDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
if ( tDesign == NULL )
{
fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
return 1;
}
if ( st_count(tDesign) == 1 )
{
st_generator * gen;
char * pName;
// find the network
st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
{
st_free_gen(gen);
break;
}
st_free_table( tDesign );
// convert it into a logic network
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
}
else
{
printf( "The design includes more than one module and is currently not used.\n" );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: read_ver [-ch] <file>\n" );
fprintf( pAbc->Err, "\t read a network in structural verilog (using current library)\n" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pTemp;
st_table * tDesign;
char * FileName;
FILE * pFile;
int fCheck;
int c;
extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
extern void Ver_ParseFreeLibrary( st_table * pLibVer );
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
}
fclose( pFile );
// set the new network
tDesign = Ver_ParseFile( FileName, NULL, fCheck );
if ( tDesign == NULL )
{
fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
return 1;
}
printf( "The library contains %d gates.\n", st_count(tDesign) );
// convert gates into AIGs
{
st_table * tLibrary;
st_generator * gen;
char * pName;
// transform the gates into the library AIGs
tLibrary = st_init_table( strcmp, st_strhash );
st_foreach_item( tDesign, gen, (char**)&pName, (char**)&pNtk )
{
// convert the netlist into SOP logic network
pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
Abc_NtkDelete( pTemp );
// perform structural hashing
pNtk = Abc_NtkStrash( pTemp = pNtk, 0, 1 );
Abc_NtkDelete( pTemp );
// insert the new network into the new library
st_insert( tLibrary, pNtk->pName, (char *)pNtk );
}
st_free_table( tDesign );
// free old library
if ( Abc_FrameReadLibVer() )
Ver_ParseFreeLibrary( Abc_FrameReadLibVer() );
// read new library
Abc_FrameSetLibVer( tLibrary );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: read_verlib [-ch] <file>\n" );
fprintf( pAbc->Err, "\t read a gate library in structural verilog\n" );
fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pTemp;
......@@ -1472,6 +1681,61 @@ usage:
SeeAlso []
***********************************************************************/
int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
{
st_table * tLibrary;
char * FileName;
int c;
extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[globalUtilOptind];
// derive the netlist
tLibrary = Abc_FrameReadLibVer();
if ( tLibrary == NULL )
{
fprintf( pAbc->Out, "Verilog library is not specified.\n" );
return 0;
}
Io_WriteVerilogLibrary( tLibrary, FileName );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_verlib [-h] <file>\n" );
fprintf( pAbc->Err, "\t write the current verilog library\n" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
......
src/base/io/ioReadBlif.c
......@@ -43,6 +43,7 @@ struct Io_ReadBlif_t_
// the error message
FILE * Output; // the output stream
char sError[1000]; // the error string generated during parsing
int fError; // set to 1 when error occurs
};
static Io_ReadBlif_t * Io_ReadBlifFile( char * pFileName );
......@@ -182,7 +183,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
return NULL;
}
}
else
else if ( !p->fError )
Abc_NtkFinalizeRead( pNtkMaster );
// return the master network
return pNtkMaster;
......@@ -273,7 +274,11 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
if ( p->vTokens == NULL ) // some files do not have ".end" in the end
break;
if ( fStatus == 1 )
{
Extra_ProgressBarStop( pProgress );
Abc_NtkDelete( pNtk );
return NULL;
}
}
if ( p->pNtkMaster == NULL )
Extra_ProgressBarStop( pProgress );
......@@ -487,6 +492,16 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
// set the pointer to the functionality of the node
Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, p->vCubes->pArray) );
// check the size
if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum(Abc_ObjData(pNode)) )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
sprintf( p->sError, "The number of fanins (%d) of node %s is different from SOP size (%d).",
Abc_ObjFaninNum(pNode), Abc_ObjName(Abc_ObjFanout(pNode,0)), Abc_SopGetVarNum(Abc_ObjData(pNode)) );
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
// return the last array of tokens
*pvTokens = vTokens;
return 0;
......@@ -735,6 +750,7 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
***********************************************************************/
void Io_ReadBlifPrintErrorMessage( Io_ReadBlif_t * p )
{
p->fError = 1;
if ( p->LineCur == 0 ) // the line number is not given
fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
else // print the error message with the line number
......
src/base/io/ioWriteVer.c
......@@ -36,6 +36,7 @@ static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -73,6 +74,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
}
// write the equations for the network
fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
Io_WriteVerilogInt( pFile, pNtk );
fprintf( pFile, "\n" );
fclose( pFile );
......@@ -80,6 +82,49 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
/**Function*************************************************************
Synopsis [Write verilog.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
{
FILE * pFile;
st_generator * gen;
Abc_Ntk_t * pNtk, * pNetlist;
char * pName;
// start the output stream
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "Io_WriteVerilogLibrary(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
fprintf( pFile, "\n" );
// write modules
st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
{
// create netlist
pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
// write the equations for the network
Io_WriteVerilogInt( pFile, pNetlist );
fprintf( pFile, "\n" );
// delete the netlist
Abc_NtkDelete( pNetlist );
}
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Writes verilog.]
Description []
......@@ -92,7 +137,6 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
{
// write inputs and outputs
fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) );
Io_WriteVerilogPis( pFile, pNtk, 3 );
fprintf( pFile, ",\n " );
......@@ -111,9 +155,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
Io_WriteVerilogRegs( pFile, pNtk, 4 );
fprintf( pFile, ";\n" );
}
if ( Io_WriteVerilogWiresCount(pNtk) > 0 )
{
fprintf( pFile, " wire" );
Io_WriteVerilogWires( pFile, pNtk, 4 );
fprintf( pFile, ";\n" );
}
// write the nodes
if ( Abc_NtkHasMapping(pNtk) )
Io_WriteVerilogGates( pFile, pNtk );
......@@ -205,7 +252,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
/**Function*************************************************************
Synopsis [Writes the wires.]
Synopsis [Counts the number of wires.]
Description []
......@@ -214,15 +261,10 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
SeeAlso []
***********************************************************************/
void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pTerm, * pNet;
int LineLength;
int AddedLength;
int NameCounter;
int i, Counter, nNodes;
// count the number of wires
int i, nNodes;
nNodes = Abc_NtkLatchNum(pNtk);
Abc_NtkForEachNode( pNtk, pTerm, i )
{
......@@ -233,6 +275,30 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
continue;
nNodes++;
}
return nNodes;
}
/**Function*************************************************************
Synopsis [Writes the wires.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
{
Abc_Obj_t * pTerm, * pNet;
int LineLength;
int AddedLength;
int NameCounter;
int i, Counter, nNodes;
// count the number of wires
nNodes = Io_WriteVerilogWiresCount( pNtk );
// write the wires
Counter = 0;
......
src/base/main/libSupport.c
......@@ -44,42 +44,71 @@ void open_libs() {
#else
DIR* dirp;
struct dirent* dp;
char *env, *init_p, *p;
int done;
env = getenv ("ABC_LIB_PATH");
if (env == NULL) {
printf("Warning: ABC_LIB_PATH not defined. Looking into the current directory.\n");
init_p = malloc (2*sizeof(char));
init_p[0]='.'; init_p[1] = 0;
} else {
init_p = malloc ((strlen(env)+1)*sizeof(char));
strcpy (init_p, env);
}
dirp = opendir(".");
while ((dp = readdir(dirp)) != NULL) {
// Extract directories and read libraries
done = 0;
p = init_p;
while (!done) {
char *endp = strchr (p,':');
if (endp == NULL) done = 1; // last directory in the list
else *endp = 0; // end of string
dirp = opendir(p);
if (dirp == NULL) {
printf("Warning: directory in ABC_LIB_PATH does not exist (%s).\n", p);
continue;
}
while ((dp = readdir(dirp)) != NULL) {
if ((strncmp("libabc_", dp->d_name, 7) == 0) &&
(strcmp(".so", dp->d_name + strlen(dp->d_name) - 3) == 0)) {
// make sure we don't overflow the handle array
if (curr_lib >= MAX_LIBS) {
printf("Warning: maximum number of ABC libraries (%d) exceeded. Not loading %s.\n",
MAX_LIBS,
dp->d_name);
}
// attempt to load it
else {
char* szPrefixed = malloc((strlen(dp->d_name) + 3) * sizeof(char));
strcpy(szPrefixed, "./");
strcat(szPrefixed, dp->d_name);
libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
// did the load succeed?
if (libHandles[curr_lib] != 0) {
printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
curr_lib++;
} else {
printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
}
free(szPrefixed);
// make sure we don't overflow the handle array
if (curr_lib >= MAX_LIBS) {
printf("Warning: maximum number of ABC libraries (%d) exceeded. Not loading %s.\n",
MAX_LIBS,
dp->d_name);
}
// attempt to load it
else {
char* szPrefixed = malloc((strlen(dp->d_name) + strlen(p) + 2) *
sizeof(char));
sprintf(szPrefixed, "%s/", p);
strcat(szPrefixed, dp->d_name);
libHandles[curr_lib] = dlopen(szPrefixed, RTLD_NOW | RTLD_LOCAL);
// did the load succeed?
if (libHandles[curr_lib] != 0) {
printf("Loaded ABC library: %s (Abc library extension #%d)\n", szPrefixed, curr_lib);
curr_lib++;
} else {
printf("Warning: failed to load ABC library %s:\n\t%s\n", szPrefixed, dlerror());
}
free(szPrefixed);
}
}
}
closedir(dirp);
p = endp+1;
}
closedir(dirp);
#endif
free(init_p);
#endif
// null terminate the list of handles
libHandles[curr_lib] = 0;
}
......
src/base/main/main.h
......@@ -97,6 +97,7 @@ extern int Abc_FrameReadNtkStoreSize();
extern void * Abc_FrameReadLibLut();
extern void * Abc_FrameReadLibGen();
extern void * Abc_FrameReadLibSuper();
extern void * Abc_FrameReadLibVer();
extern void * Abc_FrameReadManDd();
extern void * Abc_FrameReadManDec();
extern char * Abc_FrameReadFlag( char * pFlag );
......@@ -107,6 +108,7 @@ extern void Abc_FrameSetNtkStoreSize( int nStored );
extern void Abc_FrameSetLibLut( void * pLib );
extern void Abc_FrameSetLibGen( void * pLib );
extern void Abc_FrameSetLibSuper( void * pLib );
extern void Abc_FrameSetLibVer( void * pLib );
extern void Abc_FrameSetFlag( char * pFlag, char * pValue );
#ifdef __cplusplus
......
src/base/main/mainFrame.c
......@@ -48,6 +48,7 @@ int Abc_FrameReadNtkStoreSize() { return s_GlobalFrame->nSt
void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; }
void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; }
void * Abc_FrameReadLibSuper() { return s_GlobalFrame->pLibSuper; }
void * Abc_FrameReadLibVer() { return s_GlobalFrame->pLibVer; }
void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; }
void * Abc_FrameReadManDec() { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart(); return s_GlobalFrame->pManDec; }
char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); }
......@@ -57,6 +58,7 @@ void Abc_FrameSetNtkStoreSize( int nStored ) { s_GlobalFrame->nStored =
void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; }
void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; }
void Abc_FrameSetLibSuper( void * pLib ) { s_GlobalFrame->pLibSuper = pLib; }
void Abc_FrameSetLibVer( void * pLib ) { s_GlobalFrame->pLibVer = pLib; }
void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); }
/**Function*************************************************************
......@@ -135,11 +137,13 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
{
extern void Rwt_ManGlobalStop();
extern void undefine_cube_size();
extern void Ver_ParseFreeLibrary( st_table * pLibVer );
// extern void Ivy_TruthManStop();
// Abc_HManStop();
undefine_cube_size();
Rwt_ManGlobalStop();
// Ivy_TruthManStop();
if ( p->pLibVer ) Ver_ParseFreeLibrary( p->pLibVer );
if ( p->pManDec ) Dec_ManStop( p->pManDec );
if ( p->dd ) Extra_StopManager( p->dd );
Abc_FrameDeleteAllNetworks( p );
......
src/base/main/mainInt.h
......@@ -72,6 +72,7 @@ struct Abc_Frame_t_
void * pLibLut; // the current LUT library
void * pLibGen; // the current genlib
void * pLibSuper; // the current supergate library
void * pLibVer; // the current Verilog library
};
////////////////////////////////////////////////////////////////////////
......
src/base/temp.c 0 → 100644
/**Function*************************************************************
Synopsis [Command procedure to allow for static BDD variable ordering.]
Description [This procedure should be integrated in "abc\src\base\abci\abc.c"
similar to how procedure Abc_CommandReorder() is currently integrated.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr, * pFile;
Abc_Ntk_t * pNtk;
char * pFileName;
int c;
int fReverse;
int fVerbose;
extern void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, int fVerbose );
extern void Abc_NtkFindCiOrder( Abc_Ntk_t * pNtk, int fReverse, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fReverse = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
{
switch ( c )
{
case 'r':
fReverse ^= 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 the var order file is given, implement this order
pFileName = NULL;
if ( argc == globalUtilOptind + 1 )
{
pFileName = argv[globalUtilOptind];
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
fprintf( pErr, "Cannot open file \"%s\" with the BDD variable order.\n", pFileName );
return 1;
}
fclose( pFile );
}
if ( pFileName )
Abc_NtkImplementCiOrder( pNtk, pFileName, fReverse, fVerbose );
else
Abc_NtkFindCiOrder( pNtk, fReverse, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: order [-rvh] <file>\n" );
fprintf( pErr, "\t computes a good static CI variable order\n" );
fprintf( pErr, "\t-r : toggle reverse ordering [default = %s]\n", fReverse? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t<file> : (optional) file with the given variable order\n" );
return 1;
}
src/temp/ivy/ivy.h
......@@ -114,6 +114,7 @@ struct Ivy_Man_t_
void * pData; // the temporary data
void * pCopy; // the temporary data
Ivy_Man_t * pHaig; // history AIG if present
int nClassesSkip; // the number of skipped classes
// memory management
Vec_Ptr_t * vChunks; // allocated memory pieces
Vec_Ptr_t * vPages; // memory pages used by nodes
......@@ -395,7 +396,9 @@ extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t *
extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
/*=== ivyCheck.c ========================================================*/
extern int Ivy_ManCheck( Ivy_Man_t * p );
extern int Ivy_ManCheckFanoutNums( Ivy_Man_t * p );
extern int Ivy_ManCheckFanouts( Ivy_Man_t * p );
extern int Ivy_ManCheckChoices( Ivy_Man_t * p );
/*=== ivyCut.c ==========================================================*/
extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
......@@ -406,6 +409,7 @@ extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront,
extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p );
extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p );
extern int Ivy_ManIsAcyclic( Ivy_Man_t * p );
extern int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig );
/*=== ivyDsd.c ==========================================================*/
extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
......@@ -422,10 +426,10 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
/*=== ivyHaig.c ==========================================================*/
extern void Ivy_ManHaigStart( Ivy_Man_t * p );
extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
extern void Ivy_ManHaigStop( Ivy_Man_t * p );
extern void Ivy_ManHaigPrintStats( Ivy_Man_t * p );
extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
extern void Ivy_ManHaigSimulate( Ivy_Man_t * p );
......@@ -477,6 +481,8 @@ extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int f
extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
/*=== ivySeq.c =========================================================*/
extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
/*=== ivyShow.c =========================================================*/
extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig );
/*=== ivyTable.c ========================================================*/
extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
......@@ -497,6 +503,8 @@ extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj,
extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj );
extern void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig );
extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
#ifdef __cplusplus
}
......
src/temp/ivy/ivyCheck.c
......@@ -142,6 +142,29 @@ int Ivy_ManCheck( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
int Ivy_ManCheckFanoutNums( Ivy_Man_t * p )
{
Ivy_Obj_t * pObj;
int i, Counter = 0;
Ivy_ManForEachObj( p, pObj, i )
if ( Ivy_ObjIsNode(pObj) )
Counter += (Ivy_ObjRefs(pObj) == 0);
if ( Counter )
printf( "Sequential AIG has %d dangling nodes.\n", Counter );
return Counter;
}
/**Function*************************************************************
Synopsis [Verifies the fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ManCheckFanouts( Ivy_Man_t * p )
{
Vec_Ptr_t * vFanouts;
......@@ -215,6 +238,34 @@ int Ivy_ManCheckFanouts( Ivy_Man_t * p )
return RetValue;
}
/**Function*************************************************************
Synopsis [Checks that each choice node has exactly one node with fanouts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ManCheckChoices( Ivy_Man_t * p )
{
Ivy_Obj_t * pObj, * pTemp;
int i;
Ivy_ManForEachObj( p->pHaig, pObj, i )
{
if ( Ivy_ObjRefs(pObj) == 0 )
continue;
// count the number of nodes in the loop
assert( !Ivy_IsComplement(pObj->pEquiv) );
for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
if ( Ivy_ObjRefs(pTemp) > 1 )
printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/temp/ivy/ivyDfs.c
......@@ -39,18 +39,35 @@
SeeAlso []
***********************************************************************/
void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
void Ivy_ManDfs_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
{
if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
return;
if ( Ivy_ObjIsMarkA(pObj) )
return;
Ivy_ObjSetMarkA(pObj);
if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
{
if ( p->pHaig == NULL && pObj->pEquiv )
Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
return;
}
//printf( "visiting node %d\n", pObj->Id );
/*
if ( pObj->Id == 87 || pObj->Id == 90 )
{
int y = 0;
}
*/
assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
if ( !Ivy_ObjIsBuf(pObj) )
Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes );
Ivy_ManDfs_rec( p, Ivy_ObjFanin1(pObj), vNodes );
if ( p->pHaig == NULL && pObj->pEquiv )
Ivy_ManDfs_rec( p, Ivy_Regular(pObj->pEquiv), vNodes );
Vec_IntPush( vNodes, pObj->Id );
//printf( "adding node %d with fanins %d and %d and equiv %d (refs = %d)\n",
// pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id,
// pObj->pEquiv? Ivy_Regular(pObj->pEquiv)->Id: -1, Ivy_ObjRefs(pObj) );
}
/**Function*************************************************************
......@@ -76,9 +93,11 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
// collect the nodes
vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
Ivy_ManForEachPo( p, pObj, i )
Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
// unmark the collected nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
// Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
// Ivy_ObjClearMarkA(pObj);
Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjClearMarkA(pObj);
// make sure network does not have dangling nodes
assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
......@@ -101,7 +120,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
Vec_Int_t * vNodes, * vLatches;
Ivy_Obj_t * pObj;
int i;
assert( Ivy_ManLatchNum(p) > 0 );
// assert( Ivy_ManLatchNum(p) > 0 );
// make sure the nodes are not marked
Ivy_ManForEachObj( p, pObj, i )
assert( !pObj->fMarkA && !pObj->fMarkB );
......@@ -112,15 +131,23 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
// collect the nodes
vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
Ivy_ManForEachPo( p, pObj, i )
Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
// unmark the collected nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
// Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
// Ivy_ObjClearMarkA(pObj);
Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjClearMarkA(pObj);
// make sure network does not have dangling nodes
// assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
*pvLatches = vLatches;
// temporary!!!
if ( pvLatches == NULL )
Vec_IntFree( vLatches );
else
*pvLatches = vLatches;
return vNodes;
}
......@@ -261,47 +288,64 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
SeeAlso []
***********************************************************************/
int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
// skip the node if it is already visited
if ( Ivy_ObjIsTravIdPrevious(p, pObj) )
return 1;
assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
// make sure the node is not visited
assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
// check if the node is part of the combinational loop
if ( Ivy_ObjIsTravIdCurrent(p, pNode) )
if ( Ivy_ObjIsTravIdCurrent(p, pObj) )
{
fprintf( stdout, "Manager contains combinational loop!\n" );
fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n", Ivy_ObjId(pNode) );
fprintf( stdout, " %d", Ivy_ObjId(pNode) );
fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n", Ivy_ObjId(pObj) );
fprintf( stdout, " %d", Ivy_ObjId(pObj) );
return 0;
}
// mark this node as a node on the current path
Ivy_ObjSetTravIdCurrent( p, pNode );
// check if the fanin is visited
if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
Ivy_ObjSetTravIdCurrent( p, pObj );
// explore equivalent nodes if pObj is the main node
if ( p->pHaig == NULL && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
{
// traverse the fanin's cone searching for the loop
if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
Ivy_Obj_t * pTemp;
assert( !Ivy_IsComplement(pObj->pEquiv) );
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
// return as soon as the loop is detected
fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) );
return 0;
// traverse the fanin's cone searching for the loop
if ( !Ivy_ManIsAcyclic_rec(p, pTemp) )
{
// return as soon as the loop is detected
fprintf( stdout, " -> (%d", Ivy_ObjId(pObj) );
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
fprintf( stdout, " %d", Ivy_ObjId(pTemp) );
fprintf( stdout, ")" );
return 0;
}
}
}
// check if the fanin is visited
if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) )
// quite if it is a CI node
if ( Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) )
{
// traverse the fanin's cone searching for the loop
if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
{
// return as soon as the loop is detected
fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin1(pNode)) );
return 0;
}
// mark this node as a visited node
Ivy_ObjSetTravIdPrevious( p, pObj );
return 1;
}
assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
// traverse the fanin's cone searching for the loop
if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
{
// return as soon as the loop is detected
fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
return 0;
}
// traverse the fanin's cone searching for the loop
if ( Ivy_ObjIsNode(pObj) && !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pObj)) )
{
// return as soon as the loop is detected
fprintf( stdout, " -> %d", Ivy_ObjId(pObj) );
return 0;
}
// mark this node as a visited node
Ivy_ObjSetTravIdPrevious( p, pNode );
Ivy_ObjSetTravIdPrevious( p, pObj );
return 1;
}
......@@ -325,30 +369,123 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
***********************************************************************/
int Ivy_ManIsAcyclic( Ivy_Man_t * p )
{
Ivy_Obj_t * pNode;
Ivy_Obj_t * pObj;
int fAcyclic, i;
// set the traversal ID for this DFS ordering
Ivy_ManIncrementTravId( p );
Ivy_ManIncrementTravId( p );
// pNode->TravId == pNet->nTravIds means "pNode is on the path"
// pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path"
// pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited"
// pObj->TravId == pNet->nTravIds means "pObj is on the path"
// pObj->TravId == pNet->nTravIds - 1 means "pObj is visited but is not on the path"
// pObj->TravId < pNet->nTravIds - 1 means "pObj is not visited"
// traverse the network to detect cycles
fAcyclic = 1;
Ivy_ManForEachCo( p, pNode, i )
Ivy_ManForEachCo( p, pObj, i )
{
if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) )
continue;
// traverse the output logic cone
if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) )
if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) )
continue;
// stop as soon as the first loop is detected
fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) );
fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) );
break;
}
return fAcyclic;
}
/**Function*************************************************************
Synopsis [Sets the levels of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ManSetLevels_rec( Ivy_Obj_t * pObj, int fHaig )
{
// quit if the node is visited
if ( Ivy_ObjIsMarkA(pObj) )
return pObj->Level;
Ivy_ObjSetMarkA(pObj);
// quit if this is a CI
if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
return 0;
assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
// get levels of the fanins
Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
if ( !Ivy_ObjIsBuf(pObj) )
Ivy_ManSetLevels_rec( Ivy_ObjFanin1(pObj), fHaig );
// get level of the node
if ( Ivy_ObjIsBuf(pObj) )
pObj->Level = 1 + Ivy_ObjFanin0(pObj)->Level;
else if ( Ivy_ObjIsNode(pObj) )
pObj->Level = Ivy_ObjLevelNew( pObj );
else assert( 0 );
// get level of other choices
if ( fHaig && pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
{
Ivy_Obj_t * pTemp;
unsigned LevelMax = pObj->Level;
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
Ivy_ManSetLevels_rec( pTemp, fHaig );
LevelMax = IVY_MAX( LevelMax, pTemp->Level );
}
// get this level
pObj->Level = LevelMax;
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
pTemp->Level = LevelMax;
}
return pObj->Level;
}
/**Function*************************************************************
Synopsis [Sets the levels of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig )
{
Ivy_Obj_t * pObj;
int i, LevelMax;
// check if CIs have choices
if ( fHaig )
{
Ivy_ManForEachCi( p, pObj, i )
if ( pObj->pEquiv )
printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id );
}
// clean the levels
Ivy_ManForEachObj( p, pObj, i )
pObj->Level = 0;
// compute the levels
LevelMax = 0;
Ivy_ManForEachCo( p, pObj, i )
{
Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
}
// compute levels of nodes without fanout
Ivy_ManForEachObj( p, pObj, i )
if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 )
{
Ivy_ManSetLevels_rec( pObj, fHaig );
LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
}
// clean the marks
Ivy_ManForEachObj( p, pObj, i )
Ivy_ObjClearMarkA(pObj);
return LevelMax;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/temp/ivy/ivyHaig.c
......@@ -26,16 +26,17 @@
/*
HAIGing rules in working AIG:
- The node points to the representative of its class
- The pointer can be complemented if they have different polarity
- Each node in the working AIG has a pointer to the corresponding node in HAIG
(this node is not necessarily the representative of the equivalence class of HAIG nodes)
- This pointer is complemented if the AIG node and its corresponding HAIG node have different phase
Choice node rules in HAIG:
- Equivalent nodes are linked into a ring
- Exactly one node in the ring has fanouts (this node is called representative)
- Pointer going from a node to the next node in the ring is complemented
if the first node is complemented, compared to the representative node
- The representative node always has non-complemented pointer to the next node
- New nodes are inserted into the ring before the representative node
- Exactly one node in the ring has fanouts (this node is called the representative)
- The pointer going from a node to the next node in the ring is complemented
if the first node is complemented, compared to the representative node of the equivalence class
- (consequence of the above) The representative node always has non-complemented pointer to the next node
- New nodes are inserted into the ring immediately after the representative node
*/
// returns the representative node of the given HAIG node
......@@ -52,7 +53,7 @@ static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
if ( Ivy_ObjRefs(pTemp) > 0 )
break;
// return the representative node
assert( pTemp != pObj );
assert( Ivy_ObjRefs(pTemp) > 0 );
return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
}
......@@ -65,8 +66,8 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
assert( Ivy_ObjRefs(pObj) > 0 );
if ( pObj->pEquiv == NULL )
return 1;
Counter = 1;
assert( !Ivy_IsComplement(pObj->pEquiv) );
Counter = 1;
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
Counter++;
return Counter;
......@@ -87,10 +88,28 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
void Ivy_ManHaigStart( Ivy_Man_t * p )
void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose )
{
Vec_Int_t * vLatches;
Ivy_Obj_t * pObj;
int i;
assert( p->pHaig == NULL );
p->pHaig = Ivy_ManDup( p );
if ( fVerbose )
{
printf( "Starting : " );
Ivy_ManPrintStats( p->pHaig );
}
// collect latches of design D and set their values to be DC
vLatches = Vec_IntAlloc( 100 );
Ivy_ManForEachLatch( p->pHaig, pObj, i )
{
pObj->Init = IVY_INIT_DC;
Vec_IntPush( vLatches, pObj->Id );
}
p->pHaig->pData = vLatches;
}
/**Function*************************************************************
......@@ -131,6 +150,7 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
Ivy_Obj_t * pObj;
int i;
assert( p->pHaig != NULL );
Vec_IntFree( p->pHaig->pData );
Ivy_ManStop( p->pHaig );
p->pHaig = NULL;
// remove dangling pointers to the HAIG objects
......@@ -151,17 +171,54 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
***********************************************************************/
void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
Ivy_Obj_t * pEquiv0, * pEquiv1;
assert( p->pHaig != NULL );
assert( !Ivy_IsComplement(pObj) );
if ( Ivy_ObjType(pObj) == IVY_BUF )
pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
else if ( Ivy_ObjType(pObj) == IVY_LATCH )
pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
{
// pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
pEquiv0 = Ivy_ObjChild0Equiv(pObj);
pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, pObj->Init );
}
else if ( Ivy_ObjType(pObj) == IVY_AND )
pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
{
// pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
pEquiv0 = Ivy_ObjChild0Equiv(pObj);
pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
pEquiv1 = Ivy_ObjChild1Equiv(pObj);
pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
}
else assert( 0 );
// make sure the node points to the representative
pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
// pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
}
/**Function*************************************************************
Synopsis [Checks if the old node is in the TFI of the new node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_ObjIsInTfi_rec( Ivy_Obj_t * pObjNew, Ivy_Obj_t * pObjOld, int Levels )
{
if ( pObjNew == pObjOld )
return 1;
if ( Levels == 0 || Ivy_ObjIsCi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
return 0;
if ( Ivy_ObjIsInTfi_rec( Ivy_ObjFanin0(pObjNew), pObjOld, Levels - 1 ) )
return 1;
if ( Ivy_ObjIsNode(pObjNew) && Ivy_ObjIsInTfi_rec( Ivy_ObjFanin1(pObjNew), pObjOld, Levels - 1 ) )
return 1;
return 0;
}
/**Function*************************************************************
......@@ -180,10 +237,16 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
int fCompl;
//printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );
assert( p->pHaig != NULL );
// get pointers to the classes
assert( !Ivy_IsComplement(pObjOld) );
// get pointers to the representatives of pObjOld and pObjNew
pObjOldHaig = pObjOld->pEquiv;
pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
// get the classes
pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
// get regular pointers
pObjOldHaigR = Ivy_Regular(pObjOldHaig);
pObjNewHaigR = Ivy_Regular(pObjNewHaig);
......@@ -192,17 +255,41 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
// if the class is the same, nothing to do
if ( pObjOldHaigR == pObjNewHaigR )
return;
// combine classes
// assume the second node does not belong to a class
assert( pObjNewHaigR->pEquiv == NULL );
// if the second node belongs to a class, do not merge classes (for the time being)
if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL ||
Ivy_ObjRefs(pObjNewHaigR) > 0 || Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
{
/*
if ( pObjNewHaigR->pEquiv != NULL )
printf( "c" );
if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
printf( "f" );
printf( " " );
*/
p->pHaig->nClassesSkip++;
return;
}
// add this node to the class of pObjOldHaig
assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
if ( pObjOldHaigR->pEquiv == NULL )
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
else
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
pObjOldHaigR->pEquiv = pObjNewHaigR;
//printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
// update the class of the new node
Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
// Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
//printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
// if ( pObjOldHaigR->Id == 13 )
// {
// Ivy_ManShow( p, 0 );
// Ivy_ManShow( p->pHaig, 1 );
// }
// if ( !Ivy_ManIsAcyclic( p->pHaig ) )
// printf( "HAIG contains a cycle\n" );
}
/**Function*************************************************************
......@@ -227,17 +314,16 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
if ( Ivy_ObjIsTerm(pObj) || i == 0 )
continue;
if ( Ivy_ObjRefs(pObj) == 0 )
{
assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
continue;
}
Counter = Ivy_HaigObjCountClass( pObj );
nChoiceNodes += (int)(Counter > 1);
nChoices += Counter - 1;
// if ( Counter > 1 )
// printf( "Choice node %d %s\n", pObj->Id, Ivy_ObjIsLatch(pObj)? "(latch)": "" );
}
*pnChoices = nChoices;
return nChoiceNodes;
}
}
/**Function*************************************************************
......@@ -250,19 +336,35 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
SeeAlso []
***********************************************************************/
void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose )
{
int nChoices, nChoiceNodes;
assert( p->pHaig != NULL );
printf( "Original : " );
Ivy_ManPrintStats( p );
printf( "HAIG : " );
Ivy_ManPrintStats( p->pHaig );
// print choice node stats
nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
Ivy_ManHaigSimulate( p );
if ( fVerbose )
{
printf( "Final : " );
Ivy_ManPrintStats( p );
printf( "HAIG : " );
Ivy_ManPrintStats( p->pHaig );
// print choice node stats
nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n",
nChoiceNodes, nChoices, p->pHaig->nClassesSkip );
}
if ( Ivy_ManIsAcyclic( p->pHaig ) )
{
if ( fVerbose )
printf( "HAIG is acyclic\n" );
}
else
printf( "HAIG contains a cycle\n" );
if ( fVerbose )
Ivy_ManHaigSimulate( p );
}
......@@ -289,6 +391,32 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
/**Function*************************************************************
Synopsis [Applies the simulation rules.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Ivy_Init_t Ivy_ManHaigSimulateChoice( Ivy_Init_t In0, Ivy_Init_t In1 )
{
assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
if ( (In0 == IVY_INIT_0 && In1 == IVY_INIT_1) || (In0 == IVY_INIT_1 && In1 == IVY_INIT_0) )
{
printf( "Compatibility fails.\n" );
return IVY_INIT_0;
}
if ( In0 == IVY_INIT_DC && In1 == IVY_INIT_DC )
return IVY_INIT_DC;
if ( In0 != IVY_INIT_DC )
return In0;
return In1;
}
/**Function*************************************************************
Synopsis [Simulate HAIG using modified 3-valued simulation.]
Description []
......@@ -300,39 +428,85 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
***********************************************************************/
void Ivy_ManHaigSimulate( Ivy_Man_t * p )
{
Vec_Int_t * vNodes, * vLatches;
Ivy_Obj_t * pObj;
Vec_Int_t * vNodes, * vLatches, * vLatchesD;
Ivy_Obj_t * pObj, * pTemp;
Ivy_Init_t In0, In1;
int i, k, Counter;
int fVerbose = 0;
// check choices
Ivy_ManCheckChoices( p );
// switch to HAIG
assert( p->pHaig != NULL );
p = p->pHaig;
if ( fVerbose )
Ivy_ManForEachPi( p, pObj, i )
printf( "Setting PI %d\n", pObj->Id );
// collect latches and nodes in the DFS order
vNodes = Ivy_ManDfsSeq( p, &vLatches );
if ( fVerbose )
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
// set the PI values
Ivy_ManConst1(p)->Init = IVY_INIT_0;
Ivy_ManConst1(p)->Init = IVY_INIT_1;
Ivy_ManForEachPi( p, pObj, i )
pObj->Init = IVY_INIT_0;
// set the latch values
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = IVY_INIT_DC;
// set the latches of D to be determinate
vLatchesD = p->pData;
Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
pObj->Init = IVY_INIT_0;
// perform several rounds of simulation
for ( k = 0; k < 5; k++ )
for ( k = 0; k < 10; k++ )
{
// count the number of non-determinate values
Counter = 0;
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
Counter += ( pObj->Init == IVY_INIT_DC );
printf( "Iter %d : Non-determinate = %d\n", k, Counter );
printf( "Iter %d : Non-determinate = %d\n", k, Counter );
// simulate the internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
{
if ( fVerbose )
printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
// simulate the equivalence class if the node is a representative
if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
{
if ( fVerbose )
printf( "Processing choice node %d\n", pObj->Id );
In0 = pObj->Init;
assert( !Ivy_IsComplement(pObj->pEquiv) );
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
if ( fVerbose )
printf( "Processing secondary node %d\n", pTemp->Id );
In1 = Ivy_InitNotCond( pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
}
pObj->Init = In0;
}
}
// simulate the latches
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
{
pObj->Level = Ivy_ObjFanin0(pObj)->Init;
if ( fVerbose )
printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
}
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = pObj->Level, pObj->Level = 0;
}
......
src/temp/ivy/ivyMan.c
......@@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart()
Ivy_ManStartMemory( p );
// create the constant node
p->pConst1 = Ivy_ManFetchMemory( p );
p->pConst1->fPhase = 1;
// p->pConst1->fPhase = 1;
Vec_PtrPush( p->vObjs, p->pConst1 );
p->nCreated = 1;
// start the table
......@@ -118,6 +118,9 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
// free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
// make sure structural hashing did not change anything
assert( Ivy_ManNodeNum(p) == Ivy_ManNodeNum(pNew) );
assert( Ivy_ManLatchNum(p) == Ivy_ManLatchNum(pNew) );
// check the resulting network
if ( !Ivy_ManCheck(pNew) )
printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
......@@ -182,7 +185,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
SideEffects []
SeeAlso []
SeeAlso []
***********************************************************************/
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
......
src/temp/ivy/ivyObj.c
......@@ -114,6 +114,11 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
// update node counters of the manager
p->nObjs[Ivy_ObjType(pObj)]++;
p->nCreated++;
// printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
// Ivy_ObjPrintVerbose( pObj, p->pHaig==NULL );
// printf( "\n" );
// if HAIG is defined, create a corresponding node
if ( p->pHaig )
Ivy_ManHaigCreateObj( p, pObj );
......@@ -192,8 +197,6 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
// add the first fanin
pObj->pFanin0 = NULL;
pObj->pFanin1 = NULL;
// Ivy_ManCheckFanouts( p );
}
/**Function*************************************************************
......@@ -324,7 +327,14 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
assert( pObjOld != Ivy_Regular(pObjNew) );
// if HAIG is defined, create the choice node
if ( p->pHaig )
{
// if ( pObjOld->Id == 31 )
// {
// Ivy_ManShow( p, 0 );
// Ivy_ManShow( p->pHaig, 1 );
// }
Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
}
// if the new object is complemented or already used, add the buffer
if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
......@@ -388,6 +398,19 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
Vec_PtrPush( p->vBufs, pObjOld );
// Ivy_ManCheckFanouts( p );
// printf( "\n" );
/*
if ( p->pHaig )
{
int x;
Ivy_ManShow( p, 0 );
Ivy_ManShow( p->pHaig, 1 );
x = 0;
}
*/
// if ( Ivy_ManCheckFanoutNums(p) )
// {
// int x = 0;
// }
}
/**Function*************************************************************
......
src/temp/ivy/ivyRwrPre.c → src/temp/ivy/ivyRwr.c
/**CFile****************************************************************
FileName [ivyRwtPre.c]
FileName [ivyRwt.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
Revision [$Id: ivyRwt.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
......
src/temp/ivy/ivySeq.c
......@@ -58,6 +58,9 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
Ivy_Obj_t * pNode;
int i, nNodes, nGain;
int clk, clkStart = clock();
// set the DC latch values
Ivy_ManForEachLatch( p, pNode, i )
pNode->Init = IVY_INIT_DC;
// start the rewriting manager
pManRwt = Rwt_ManStart( 0 );
p->pData = pManRwt;
......@@ -92,12 +95,6 @@ clk = clock();
Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
/*
if ( !Ivy_ManIsAcyclic(p) )
{
int x = 0;
}
*/
}
}
Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
......@@ -109,6 +106,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
p->pData = NULL;
// fix the levels
Ivy_ManResetLevels( p );
// if ( Ivy_ManCheckFanoutNums(p) )
// printf( "Ivy_ManRewritePre(): The check has failed.\n" );
// check
if ( !Ivy_ManCheck(p) )
printf( "Ivy_ManRewritePre(): The check has failed.\n" );
......@@ -139,7 +138,8 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
Dec_Graph_t * pGraph;
Ivy_Store_t * pStore;
Ivy_Cut_t * pCut;
Ivy_Obj_t * pFanin;
Ivy_Obj_t * pFanin;//, * pFanout;
Vec_Ptr_t * vFanout;
unsigned uPhase, uTruthBest, uTruth;
char * pPerm;
int nNodesSaved, nNodesSaveCur;
......@@ -154,6 +154,7 @@ p->timeCut += clock() - clk;
// go through the cuts
clk = clock();
vFanout = Vec_PtrAlloc( 100 );
for ( c = 1; c < pStore->nCuts; c++ )
{
pCut = pStore->pCuts + c;
......@@ -193,6 +194,9 @@ clk2 = clock();
// label MFFC with current ID
Ivy_ManIncrementTravId( pMan );
nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode );
// label fanouts with the current ID
// Ivy_ObjForEachFanout( pMan, pNode, vFanout, pFanout, i )
// Ivy_ObjSetTravIdCurrent( pMan, pFanout );
// unmark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
......@@ -233,11 +237,19 @@ p->timeEval += clock() - clk2;
Vec_PtrPush( p->vFanins, pFanin );
}
}
Vec_PtrFree( vFanout );
p->timeRes += clock() - clk;
if ( GainBest == -1 )
return -1;
/*
printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
for ( i = 0; i < pCut->nSize; i++ )
printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
printf( " }\n" );
*/
// copy the leaves
Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
......@@ -250,10 +262,9 @@ p->timeRes += clock() - clk;
if ( GainBest > 0 )
{
Ivy_Cut_t * pCut = p->pCut;
printf( "Useful cut : {" );
printf( "Node %5d. Using cut : {", Ivy_ObjId(pNode) );
for ( i = 0; i < pCut->nSize; i++ )
printf( " %5d[%2d](%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]),
Ivy_ObjRefs( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) );
printf( " %5d(%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
printf( " }\n" );
}
*/
......@@ -974,18 +985,19 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
SideEffects []
SeeAlso []
SeeAlso []
***********************************************************************/
static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
{
int iLeaf;
int nLats, iLeaf;
assert( !Ivy_IsComplement(pFanin) );
if ( !Ivy_ObjIsLatch(pFanin) )
return Ivy_LeafCreate( pFanin->Id, 0 );
iLeaf = Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
assert( Ivy_LeafLat(iLeaf) < IVY_LEAF_MASK );
return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
iLeaf = Ivy_CutReadLeaf(Ivy_ObjFanin0(pFanin));
nLats = Ivy_LeafLat(iLeaf);
assert( nLats < IVY_LEAF_MASK );
return 1 + iLeaf;
}
/**Function*************************************************************
......
src/temp/ivy/ivyShow.c 0 → 100644
/**CFile****************************************************************
FileName [ivyShow.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Visualization of HAIG.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivyShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
{
extern void Abc_ShowFile( char * FileNameDot );
static Counter = 0;
char FileNameDot[200];
FILE * pFile;
// create the file name
// Ivy_ShowGetFileName( pMan->pName, FileNameDot );
sprintf( FileNameDot, "temp%02d.dot", Counter++ );
// check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
return;
}
fclose( pFile );
// generate the file
Ivy_WriteDotAig( pMan, FileNameDot, fHaig );
// visualize the file
Abc_ShowFile( FileNameDot );
}
/**Function*************************************************************
Synopsis [Writes the graph structure of AIG for DOT.]
Description [Useful for graph visualization using tools such as GraphViz:
http://www.graphviz.org/]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
{
FILE * pFile;
Ivy_Obj_t * pNode, * pTemp, * pPrev;
int LevelMax, Level, i;
if ( Ivy_ManNodeNum(pMan) > 200 )
{
fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )
{
fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
return;
}
// compute levels
LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
// write the DOT header
fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" );
fprintf( pFile, "\n" );
fprintf( pFile, "digraph AIG {\n" );
fprintf( pFile, "size = \"7.5,10\";\n" );
// fprintf( pFile, "ranksep = 0.5;\n" );
// fprintf( pFile, "nodesep = 0.5;\n" );
fprintf( pFile, "center = true;\n" );
// fprintf( pFile, "orientation = landscape;\n" );
// fprintf( pFile, "edge [fontsize = 10];\n" );
// fprintf( pFile, "edge [dir = none];\n" );
fprintf( pFile, "edge [dir = back];\n" );
fprintf( pFile, "\n" );
// labels on the left of the picture
fprintf( pFile, "{\n" );
fprintf( pFile, " node [shape = plaintext];\n" );
fprintf( pFile, " edge [style = invis];\n" );
fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
// generate node names with labels
for ( Level = LevelMax; Level >= 0; Level-- )
{
// the visible node name
fprintf( pFile, " Level%d", Level );
fprintf( pFile, " [label = " );
// label name
fprintf( pFile, "\"" );
fprintf( pFile, "\"" );
fprintf( pFile, "];\n" );
}
// genetate the sequence of visible/invisible nodes to mark levels
fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
for ( Level = LevelMax; Level >= 0; Level-- )
{
// the visible node name
fprintf( pFile, " Level%d", Level );
// the connector
if ( Level != 0 )
fprintf( pFile, " ->" );
else
fprintf( pFile, ";" );
}
fprintf( pFile, "\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate title box on top
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
fprintf( pFile, " LevelTitle1;\n" );
fprintf( pFile, " title1 [shape=plaintext,\n" );
fprintf( pFile, " fontsize=20,\n" );
fprintf( pFile, " fontname = \"Times-Roman\",\n" );
fprintf( pFile, " label=\"" );
fprintf( pFile, "%s", "AIG structure visualized by ABC" );
fprintf( pFile, "\\n" );
fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate statistics box
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
fprintf( pFile, " LevelTitle2;\n" );
fprintf( pFile, " title2 [shape=plaintext,\n" );
fprintf( pFile, " fontsize=18,\n" );
fprintf( pFile, " fontname = \"Times-Roman\",\n" );
fprintf( pFile, " label=\"" );
fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Ivy_ManNodeNum(pMan), LevelMax );
fprintf( pFile, "\\n" );
fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" );
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate the COs
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", LevelMax );
// generate the CO nodes
Ivy_ManForEachCo( pMan, pNode, i )
{
if ( fHaig || pNode->pEquiv == NULL )
fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
(Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
else
fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
(Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":""),
Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"invtriangle") );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate nodes of each rank
for ( Level = LevelMax - 1; Level > 0; Level-- )
{
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", Level );
Ivy_ManForEachObj( pMan, pNode, i )
{
if ( (int)pNode->Level != Level )
continue;
if ( fHaig || pNode->pEquiv == NULL )
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
else
fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
fprintf( pFile, ", shape = ellipse" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
}
// generate the CI nodes
fprintf( pFile, "{\n" );
fprintf( pFile, " rank = same;\n" );
// the labeling node of this level
fprintf( pFile, " Level%d;\n", 0 );
// generate constant node
if ( Ivy_ObjRefs(Ivy_ManConst1(pMan)) > 0 )
{
pNode = Ivy_ManConst1(pMan);
// check if the costant node is present
fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id );
fprintf( pFile, ", shape = ellipse" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
// generate the CI nodes
Ivy_ManForEachCi( pMan, pNode, i )
{
if ( fHaig || pNode->pEquiv == NULL )
fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
(Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":"") );
else
fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
(Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":""),
Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"triangle") );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
// generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Ivy_ManForEachCo( pMan, pNode, i )
fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
// generate edges
Ivy_ManForEachObj( pMan, pNode, i )
{
if ( !Ivy_ObjIsNode(pNode) && !Ivy_ObjIsCo(pNode) && !Ivy_ObjIsBuf(pNode) )
continue;
// generate the edge from this node to the next
fprintf( pFile, "Node%d%s", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Ivy_ObjFaninId0(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin0(pNode))? "_out":"") );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Ivy_ObjFaninC0(pNode)? "dotted" : "bold" );
// if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
if ( !Ivy_ObjIsNode(pNode) )
continue;
// generate the edge from this node to the next
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d%s", Ivy_ObjFaninId1(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin1(pNode))? "_out":"") );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Ivy_ObjFaninC1(pNode)? "dotted" : "bold" );
// if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
// generate the edges between the equivalent nodes
if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
{
pPrev = pNode;
for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
{
fprintf( pFile, "Node%d", pPrev->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", pTemp->Id );
fprintf( pFile, " [style = %s]", Ivy_IsComplement(pTemp->pEquiv)? "dotted" : "bold" );
fprintf( pFile, ";\n" );
pPrev = pTemp;
}
// connect the last node with the first
fprintf( pFile, "Node%d", pPrev->Id );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " [style = %s]", Ivy_IsComplement(pPrev->pEquiv)? "dotted" : "bold" );
fprintf( pFile, ";\n" );
}
}
fprintf( pFile, "}" );
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ivy/ivyTable.c
......@@ -167,7 +167,7 @@ void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew )
return;
pPlace = Ivy_TableFind( p, pObj );
assert( *pPlace == pObj->Id ); // node should be in the table
*pPlace = ObjIdNew;
*pPlace = ObjIdNew;
}
/**Function*************************************************************
......@@ -203,7 +203,7 @@ int Ivy_TableCountEntries( Ivy_Man_t * p )
void Ivy_TableResize( Ivy_Man_t * p )
{
int * pTableOld, * pPlace;
int nTableSizeOld, Counter, e, clk;
int nTableSizeOld, Counter, nEntries, e, clk;
clk = clock();
// save the old table
pTableOld = p->pTable;
......@@ -224,7 +224,8 @@ clk = clock();
assert( *pPlace == 0 ); // should not be in the table
*pPlace = pTableOld[e];
}
assert( Counter == Ivy_ManHashObjNum(p) );
nEntries = Ivy_ManHashObjNum(p);
// assert( Counter == nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
......
src/temp/ivy/ivyUtil.c
......@@ -612,6 +612,98 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
}
/**Function*************************************************************
Synopsis [Prints node in HAIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ObjPrintVerbose( Ivy_Obj_t * pObj, int fHaig )
{
Ivy_Obj_t * pTemp;
assert( !Ivy_IsComplement(pObj) );
printf( "Node %5d : ", Ivy_ObjId(pObj) );
if ( Ivy_ObjIsConst1(pObj) )
printf( "constant 1" );
else if ( Ivy_ObjIsPi(pObj) )
printf( "PI" );
else if ( Ivy_ObjIsPo(pObj) )
printf( "PO" );
else if ( Ivy_ObjIsLatch(pObj) )
printf( "latch %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
else if ( Ivy_ObjIsBuf(pObj) )
printf( "buffer %d%s", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
else
printf( "AND( %5d%s, %5d%s )",
Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "),
Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
if ( !fHaig )
{
if ( pObj->pEquiv == NULL )
printf( " HAIG node not given" );
else
printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
return;
}
if ( pObj->pEquiv == NULL )
return;
// there are choices
if ( Ivy_ObjRefs(pObj) > 0 )
{
// print equivalence class
printf( " { %5d ", pObj->Id );
assert( !Ivy_IsComplement(pObj->pEquiv) );
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
printf( " }" );
return;
}
// this is a secondary node
for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
assert( Ivy_ObjRefs(pTemp) > 0 );
printf( " class of %d", pTemp->Id );
}
/**Function*************************************************************
Synopsis [Prints node in HAIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
{
Vec_Int_t * vNodes;
Ivy_Obj_t * pObj;
int i;
printf( "PIs: " );
Ivy_ManForEachPi( p, pObj, i )
printf( " %d", pObj->Id );
printf( "\n" );
printf( "POs: " );
Ivy_ManForEachPo( p, pObj, i )
printf( " %d", pObj->Id );
printf( "\n" );
printf( "Latches: " );
Ivy_ManForEachLatch( p, pObj, i )
printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
printf( "\n" );
vNodes = Ivy_ManDfsSeq( p, NULL );
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
Ivy_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
printf( "\n" );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/temp/ivy/module.make
......@@ -12,7 +12,7 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyObj.c \
src/temp/ivy/ivyOper.c \
src/temp/ivy/ivyResyn.c \
src/temp/ivy/ivyRwrPre.c \
src/temp/ivy/ivyRwr.c \
src/temp/ivy/ivySeq.c \
src/temp/ivy/ivyTable.c \
src/temp/ivy/ivyUtil.c
src/temp/ver/ver.h 0 → 100644
/**CFile****************************************************************
FileName [ver.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: ver.h,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VER_H__
#define __VER_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Ver_Man_t_ Ver_Man_t;
typedef struct Ver_Stream_t_ Ver_Stream_t;
struct Ver_Man_t_
{
// input file stream
char * pFileName;
Ver_Stream_t * pReader;
ProgressBar * pProgress;
// current network and library
Abc_Ntk_t * pNtkCur; // the network under construction
st_table * pLibrary; // the current design library
st_table * pGateLib; // the current technology library
// error recovery
FILE * Output;
int fTopLevel;
int fError;
char sError[2000];
// intermediate structures
Vec_Ptr_t * vNames;
Vec_Ptr_t * vStackFn;
Vec_Int_t * vStackOp;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== verCore.c ========================================================*/
extern st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck );
extern void Ver_ParsePrintErrorMessage( Ver_Man_t * p );
/*=== verFormula.c ========================================================*/
extern DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
/*=== verParse.c ========================================================*/
extern int Ver_ParseSkipComments( Ver_Man_t * p );
extern char * Ver_ParseGetName( Ver_Man_t * p );
/*=== verStream.c ========================================================*/
extern Ver_Stream_t * Ver_StreamAlloc( char * pFileName );
extern void Ver_StreamFree( Ver_Stream_t * p );
extern char * Ver_StreamGetFileName( Ver_Stream_t * p );
extern int Ver_StreamGetFileSize( Ver_Stream_t * p );
extern int Ver_StreamGetCurPosition( Ver_Stream_t * p );
extern int Ver_StreamGetLineNumber( Ver_Stream_t * p );
extern int Ver_StreamIsOkey( Ver_Stream_t * p );
extern char Ver_StreamScanChar( Ver_Stream_t * p );
extern char Ver_StreamPopChar( Ver_Stream_t * p );
extern void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip );
extern void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop );
extern char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/verCore.c 0 → 100644
/**CFile****************************************************************
FileName [verCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Parses several flavors of structural Verilog.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: verCore.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// types of verilog signals
typedef enum {
VER_SIG_NONE = 0,
VER_SIG_INPUT,
VER_SIG_OUTPUT,
VER_SIG_INOUT,
VER_SIG_REG,
VER_SIG_WIRE
} Ver_SignalType_t;
static void Ver_ParseFreeData( Ver_Man_t * p );
static void Ver_ParseInternal( Ver_Man_t * p, int fCheck );
static int Ver_ParseModule( Ver_Man_t * p );
static int Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType );
static int Ver_ParseAssign( Ver_Man_t * p );
static int Ver_ParseAlways( Ver_Man_t * p );
static int Ver_ParseInitial( Ver_Man_t * p );
static int Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate );
static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
static Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [File parser.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
st_table * Ver_ParseFile( char * pFileName, st_table * pGateLib, int fCheck )
{
Ver_Man_t * p;
st_table * pLibrary;
// start the file reader
p = ALLOC( Ver_Man_t, 1 );
memset( p, 0, sizeof(Ver_Man_t) );
p->pFileName = pFileName;
p->pReader = Ver_StreamAlloc( pFileName );
p->pLibrary = st_init_table( st_ptrcmp, st_ptrhash );
p->pGateLib = pGateLib;
p->Output = stdout;
p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) );
p->vNames = Vec_PtrAlloc( 100 );
p->vStackFn = Vec_PtrAlloc( 100 );
p->vStackOp = Vec_IntAlloc( 100 );
// parse the file
Ver_ParseInternal( p, fCheck );
// stop the parser
assert( p->pNtkCur == NULL );
pLibrary = p->pLibrary;
Ver_StreamFree( p->pReader );
Extra_ProgressBarStop( p->pProgress );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vStackFn );
Vec_IntFree( p->vStackOp );
free( p );
return pLibrary;
}
/**Function*************************************************************
Synopsis [File parser.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_ParseFreeLibrary( st_table * pLibVer )
{
st_generator * gen;
Abc_Ntk_t * pNtk;
char * pName;
st_foreach_item( pLibVer, gen, (char**)&pName, (char**)&pNtk )
Abc_NtkDelete( pNtk );
st_free_table( pLibVer );
}
/**Function*************************************************************
Synopsis [File parser.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_ParseFreeData( Ver_Man_t * p )
{
if ( p->pNtkCur )
{
Abc_NtkDelete( p->pNtkCur );
p->pNtkCur = NULL;
}
if ( p->pLibrary )
{
Ver_ParseFreeLibrary( p->pLibrary );
p->pLibrary = NULL;
}
}
/**Function*************************************************************
Synopsis [File parser.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck )
{
char * pToken;
while ( 1 )
{
// get the next token
pToken = Ver_ParseGetName( pMan );
if ( pToken == NULL )
break;
if ( strcmp( pToken, "module" ) )
{
sprintf( pMan->sError, "Cannot read \"module\" directive." );
Ver_ParsePrintErrorMessage( pMan );
return;
}
// parse the module
if ( !Ver_ParseModule( pMan ) )
return;
// check the network for correctness
if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
{
pMan->fTopLevel = 1;
sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName );
Ver_ParsePrintErrorMessage( pMan );
return;
}
// add the module to the hash table
if ( st_is_member( pMan->pLibrary, pMan->pNtkCur->pName ) )
{
pMan->fTopLevel = 1;
sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName );
Ver_ParsePrintErrorMessage( pMan );
return;
}
st_insert( pMan->pLibrary, pMan->pNtkCur->pName, (char *)pMan->pNtkCur );
pMan->pNtkCur = NULL;
}
}
/**Function*************************************************************
Synopsis [Prints the error message including the file name and line number.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
{
p->fError = 1;
if ( p->fTopLevel ) // the line number is not given
fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
else // print the error message with the line number
fprintf( p->Output, "%s (line %d): %s\n",
p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
// free the data
Ver_ParseFreeData( p );
}
/**Function*************************************************************
Synopsis [Parses one Verilog module.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseModule( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk, * pNtkTemp;
char * pWord;
int RetValue;
char Symbol;
// start the current network
assert( pMan->pNtkCur == NULL );
pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX );
// pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BDD );
// get the network name
pWord = Ver_ParseGetName( pMan );
pNtk->pName = Extra_UtilStrsav( pWord );
pNtk->pSpec = Extra_UtilStrsav( pMan->pFileName );
// create constant nodes and nets
Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
Ver_ParseCreateConst( pNtk, "1'b0", 0 );
Ver_ParseCreateConst( pNtk, "1'b1", 1 );
// make sure we stopped at the opening paranthesis
if ( Ver_StreamScanChar(p) != '(' )
{
sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", pNtk->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// skip to the end of parantheses
while ( 1 )
{
Ver_StreamSkipToChars( p, ",/)" );
while ( Ver_StreamScanChar(p) == '/' )
{
Ver_ParseSkipComments( pMan );
Ver_StreamSkipToChars( p, ",/)" );
}
Symbol = Ver_StreamPopChar(p);
if ( Symbol== ')' )
break;
}
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
Symbol = Ver_StreamPopChar(p);
assert( Symbol == ';' );
// parse the inputs/outputs/registers/wires/inouts
while ( 1 )
{
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
if ( !strcmp( pWord, "input" ) )
RetValue = Ver_ParseSignal( pMan, VER_SIG_INPUT );
else if ( !strcmp( pWord, "output" ) )
RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT );
else if ( !strcmp( pWord, "reg" ) )
RetValue = Ver_ParseSignal( pMan, VER_SIG_REG );
else if ( !strcmp( pWord, "wire" ) )
RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE );
else if ( !strcmp( pWord, "inout" ) )
RetValue = Ver_ParseSignal( pMan, VER_SIG_INOUT );
else
break;
if ( RetValue == 0 )
return 0;
}
// parse the remaining statements
while ( 1 )
{
Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
if ( !strcmp( pWord, "assign" ) )
RetValue = Ver_ParseAssign( pMan );
else if ( !strcmp( pWord, "always" ) )
RetValue = Ver_ParseAlways( pMan );
else if ( !strcmp( pWord, "initial" ) )
RetValue = Ver_ParseInitial( pMan );
else if ( !strcmp( pWord, "endmodule" ) )
{
// if nothing is known, set the functionality to be black box
Abc_NtkFinalizeRead( pNtk );
break;
}
else if ( pMan->pGateLib && st_lookup(pMan->pGateLib, pWord, (char**)&pNtkTemp) ) // gate library
RetValue = Ver_ParseGate( pMan, pNtkTemp );
else if ( pMan->pLibrary && st_lookup(pMan->pLibrary, pWord, (char**)&pNtkTemp) ) // current design
RetValue = Ver_ParseGate( pMan, pNtkTemp );
else
{
printf( "Cannot find \"%s\".\n", pWord );
Ver_StreamSkipToChars( p, ";" );
Ver_StreamPopChar(p);
// sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord );
// Ver_ParsePrintErrorMessage( pMan );
// return 0;
}
if ( RetValue == 0 )
return 0;
// get new word
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
}
if ( pNtk->ntkFunc == ABC_FUNC_BDD )
{
Abc_Obj_t * pObj;
pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b0" ) );
pObj->pData = Cudd_ReadLogicZero( pNtk->pManFunc );
pObj = Abc_ObjFanin0( Abc_NtkFindNet( pNtk, "1'b1" ) );
pObj->pData = Cudd_ReadOne( pNtk->pManFunc );
Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) );
Cudd_Ref( Cudd_ReadOne( pNtk->pManFunc ) );
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk = pMan->pNtkCur;
char * pWord;
char Symbol;
while ( 1 )
{
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
Ver_ParseCreatePi( pNtk, pWord );
if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
Ver_ParseCreatePo( pNtk, pWord );
if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
Abc_NtkFindOrCreateNet( pNtk, pWord );
Symbol = Ver_StreamPopChar(p);
if ( Symbol == ',' )
continue;
if ( Symbol == ';' )
return 1;
break;
}
sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseAssign( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNode, * pNet;
char * pWord, * pName, * pEquation;
DdNode * bFunc;
char Symbol;
int i, Length;
// convert from the mapped netlist into the BDD netlist
if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
{
pNtk->ntkFunc = ABC_FUNC_BDD;
pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
}
else if ( pNtk->ntkFunc != ABC_FUNC_BDD )
{
sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
while ( 1 )
{
// get the name of the output signal
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// get the fanout net
pNet = Abc_NtkFindNet( pNtk, pWord );
if ( pNet == NULL )
{
sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// get the equal sign
if ( Ver_StreamPopChar(p) != '=' )
{
sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// skip the comments
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
// get the second name
pEquation = Ver_StreamGetWord( p, ",;" );
if ( pEquation == NULL )
return 0;
// parse the formula
bFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
if ( bFunc == NULL )
{
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
Cudd_Ref( bFunc );
// create the node with the given inputs
pNode = Abc_NtkCreateNode( pMan->pNtkCur );
pNode->pData = bFunc;
Abc_ObjAddFanin( pNet, pNode );
// connect to fanin nets
for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
{
// get the name of this signal
Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
pName = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
pName[Length] = 0;
// find the corresponding net
pNet = Abc_NtkFindNet( pNtk, pName );
if ( pNet == NULL )
{
sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d is not defined).", pWord, pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
Abc_ObjAddFanin( pNode, pNet );
}
Symbol = Ver_StreamPopChar(p);
if ( Symbol == ',' )
continue;
if ( Symbol == ';' )
return 1;
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseAlways( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNet, * pNet2;
char * pWord, * pWord2;
char Symbol;
// parse the directive
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
if ( strcmp( pWord, "begin" ) )
{
sprintf( pMan->sError, "Cannot parse the always statement (expected \"begin\")." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// iterate over the initial states
while ( 1 )
{
// get the name of the output signal
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// look for the end of directive
if ( !strcmp( pWord, "end" ) )
break;
// get the fanout net
pNet = Abc_NtkFindNet( pNtk, pWord );
if ( pNet == NULL )
{
sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// get the equal sign
if ( Ver_StreamPopChar(p) != '=' )
{
sprintf( pMan->sError, "Cannot read the always statement for %s (expected equality sign).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// skip the comments
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
// get the second name
pWord2 = Ver_ParseGetName( pMan );
if ( pWord2 == NULL )
return 0;
// get the fanin net
pNet2 = Abc_NtkFindNet( pNtk, pWord2 );
if ( pNet2 == NULL )
{
sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// create the latch
Ver_ParseCreateLatch( pNtk, pNet2->pData, pNet->pData );
// remove the last symbol
Symbol = Ver_StreamPopChar(p);
assert( Symbol == ';' );
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseInitial( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNode, * pNet;
char * pWord, * pEquation;
char Symbol;
// parse the directive
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
if ( strcmp( pWord, "begin" ) )
{
sprintf( pMan->sError, "Cannot parse the initial statement (expected \"begin\")." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// iterate over the initial states
while ( 1 )
{
// get the name of the output signal
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// look for the end of directive
if ( !strcmp( pWord, "end" ) )
break;
// get the fanout net
pNet = Abc_NtkFindNet( pNtk, pWord );
if ( pNet == NULL )
{
sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// get the equal sign
if ( Ver_StreamPopChar(p) != '=' )
{
sprintf( pMan->sError, "Cannot read the initial statement for %s (expected equality sign).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// skip the comments
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
// get the second name
pEquation = Ver_StreamGetWord( p, ";" );
if ( pEquation == NULL )
return 0;
// find the corresponding latch
pNode = Abc_ObjFanin0(pNet);
assert( Abc_ObjIsLatch(pNode) );
// set the initial state
if ( pEquation[0] == '2' )
Abc_LatchSetInitDc( pNode );
else if ( pEquation[0] == '1')
Abc_LatchSetInit1( pNode );
else if ( pEquation[0] == '0' )
Abc_LatchSetInit0( pNode );
else
{
sprintf( pMan->sError, "Incorrect initial value of the latch %s (expected equality sign).", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// remove the last symbol
Symbol = Ver_StreamPopChar(p);
assert( Symbol == ';' );
}
return 1;
}
/**Function*************************************************************
Synopsis [Parses one directive.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
{
Ver_Stream_t * p = pMan->pReader;
Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNetFormal, * pNetActual;
Abc_Obj_t * pObj, * pNode;
char * pWord, Symbol;
int i, fCompl;
// convert from the mapped netlist into the BDD netlist
if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
{
pNtk->ntkFunc = ABC_FUNC_MAP;
pNtk->pManFunc = pMan->pGateLib;
}
else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
{
sprintf( pMan->sError, "The network %s appears to contain both mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// clean the PI/PO pointers
Abc_NtkForEachPi( pNtkGate, pObj, i )
pObj->pCopy = NULL;
Abc_NtkForEachPo( pNtkGate, pObj, i )
pObj->pCopy = NULL;
// parse the directive and set the pointers to the PIs/POs of the gate
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// this is gate name - throw it away
if ( Ver_StreamPopChar(p) != '(' )
{
sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// parse pairs of formal/actural inputs
while ( 1 )
{
// process one pair of formal/actual parameters
if ( Ver_StreamPopChar(p) != '.' )
{
sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// parse the formal name
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// get the formal net
if ( Abc_NtkIsNetlist(pNtkGate) )
pNetFormal = Abc_NtkFindNet( pNtkGate, pWord );
else // if ( Abc_NtkIsStrash(pNtkGate) )
pNetFormal = Abc_NtkFindTerm( pNtkGate, pWord );
if ( pNetFormal == NULL )
{
sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// open the paranthesis
if ( Ver_StreamPopChar(p) != '(' )
{
sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// parse the actual name
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
// check if the name is complemented
fCompl = (pWord[0] == '~');
if ( fCompl )
pWord++;
// get the actual net
pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord );
if ( pNetActual == NULL )
{
sprintf( pMan->sError, "Actual net is missing in gate %s.", pWord );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// close the paranthesis
if ( Ver_StreamPopChar(p) != ')' )
{
sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// process the pair
if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net
Abc_ObjFanin0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) ) // P0 net
{
assert( fCompl == 0 );
Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
}
else
{
sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
Symbol = Ver_StreamPopChar(p);
if ( Symbol == ')' )
break;
// skip comma
if ( Symbol != ',' )
{
sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
Ver_ParseSkipComments( pMan );
}
// check if it is the end of gate
Ver_ParseSkipComments( pMan );
if ( Ver_StreamPopChar(p) != ';' )
{
sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
// make sure each input net is driven
Abc_NtkForEachPi( pNtkGate, pObj, i )
if ( pObj->pCopy == NULL )
{
sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjFanout0(pObj)->pData, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
/*
// make sure each output net is driving something
Abc_NtkForEachPo( pNtkGate, pObj, i )
if ( pObj->pCopy == NULL )
{
sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjFanin0(pObj)->pData, pNtkGate->pName );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
*/
// create a new node
pNode = Abc_NtkCreateNode( pMan->pNtkCur );
// connect to fanin nets
Abc_NtkForEachPi( pNtkGate, pObj, i )
Abc_ObjAddFanin( pNode, pObj->pCopy );
// connect to fanout nets
Abc_NtkForEachPo( pNtkGate, pObj, i )
if ( pObj->pCopy )
Abc_ObjAddFanin( pObj->pCopy, pNode );
// set the functionality
pNode->pData = pNtkGate;
return 1;
}
/**Function*************************************************************
Synopsis [Creates PI terminal and net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet, * pTerm;
// get the PI net
pNet = Abc_NtkFindNet( pNtk, pName );
if ( pNet )
printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
// add the PI node
pTerm = Abc_NtkCreatePi( pNtk );
Abc_ObjAddFanin( pNet, pTerm );
return pTerm;
}
/**Function*************************************************************
Synopsis [Creates PO terminal and net.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet, * pTerm;
// get the PO net
pNet = Abc_NtkFindNet( pNtk, pName );
if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
pNet = Abc_NtkFindOrCreateNet( pNtk, pName );
// add the PO node
pTerm = Abc_NtkCreatePo( pNtk );
Abc_ObjAddFanin( pTerm, pNet );
return pTerm;
}
/**Function*************************************************************
Synopsis [Create a constant 0 node driving the net with this name.]
Description [Assumes that the net already exists.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Ver_ParseCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
{
Abc_Obj_t * pNet, * pTerm;
pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk);
pNet = Abc_NtkFindNet(pNtk, pName); assert( pNet );
Abc_ObjAddFanin( pNet, pTerm );
return pTerm;
}
/**Function*************************************************************
Synopsis [Create a latch with the given input/output.]
Description [By default, the latch value is unknown (ABC_INIT_NONE).]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
{
Abc_Obj_t * pLatch, * pNet;
// create a new latch and add it to the network
pLatch = Abc_NtkCreateLatch( pNtk );
// get the LI net
pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
Abc_ObjAddFanin( pLatch, pNet );
// get the LO net
pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
Abc_ObjAddFanin( pNet, pLatch );
return pLatch;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/verFormula.c 0 → 100644
/**CFile****************************************************************
FileName [verFormula.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Formula parser to read Verilog assign statements.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// the list of operation symbols to be used in expressions
#define VER_PARSE_SYM_OPEN '(' // opening paranthesis
#define VER_PARSE_SYM_CLOSE ')' // closing paranthesis
#define VER_PARSE_SYM_CONST0 '0' // constant 0
#define VER_PARSE_SYM_CONST1 '1' // constant 1
#define VER_PARSE_SYM_NEGBEF1 '!' // negation before the variable
#define VER_PARSE_SYM_NEGBEF2 '~' // negation before the variable
#define VER_PARSE_SYM_AND '&' // logic AND
#define VER_PARSE_SYM_OR '|' // logic OR
#define VER_PARSE_SYM_XOR '^' // logic XOR
#define VER_PARSE_SYM_MUX1 '?' // first symbol of MUX
#define VER_PARSE_SYM_MUX2 ':' // second symbol of MUX
// the list of opcodes (also specifying operation precedence)
#define VER_PARSE_OPER_NEG 10 // negation
#define VER_PARSE_OPER_AND 9 // logic AND
#define VER_PARSE_OPER_XOR 8 // logic EXOR (a'b | ab')
#define VER_PARSE_OPER_OR 7 // logic OR
#define VER_PARSE_OPER_EQU 6 // equvalence (a'b'| ab )
#define VER_PARSE_OPER_MUX 5 // MUX (a'b | ac )
#define VER_PARSE_OPER_MARK 1 // OpStack token standing for an opening paranthesis
// these are values of the internal Flag
#define VER_PARSE_FLAG_START 1 // after the opening parenthesis
#define VER_PARSE_FLAG_VAR 2 // after operation is received
#define VER_PARSE_FLAG_OPER 3 // after operation symbol is received
#define VER_PARSE_FLAG_OPERMUX 4 // after operation symbol is received
#define VER_PARSE_FLAG_ERROR 5 // when error is detected
static DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper );
static int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Parser of the formula encountered in assign statements.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Ver_FormulaParser( char * pFormula, DdManager * dd, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
{
DdNode * bFunc, * bTemp;
char * pTemp;
int nParans, Flag;
int Oper, Oper1, Oper2;
int v;
// clear the stacks and the names
Vec_PtrClear( vNames );
Vec_PtrClear( vStackFn );
Vec_IntClear( vStackOp );
// make sure that the number of opening and closing parantheses is the same
nParans = 0;
for ( pTemp = pFormula; *pTemp; pTemp++ )
if ( *pTemp == '(' )
nParans++;
else if ( *pTemp == ')' )
nParans--;
if ( nParans != 0 )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." );
return NULL;
}
// add parantheses
pTemp = pFormula + strlen(pFormula) + 2;
*pTemp-- = 0; *pTemp = ')';
while ( --pTemp != pFormula )
*pTemp = *(pTemp - 1);
*pTemp = '(';
// perform parsing
Flag = VER_PARSE_FLAG_START;
for ( pTemp = pFormula; *pTemp; pTemp++ )
{
switch ( *pTemp )
{
// skip all spaces, tabs, and end-of-lines
case ' ':
case '\t':
case '\r':
case '\n':
case '\\': // skip name opening statement
continue;
// treat Constant 0 as a variable
case VER_PARSE_SYM_CONST0:
Vec_PtrPush( vStackFn, b0 ); Cudd_Ref( b0 );
if ( Flag == VER_PARSE_FLAG_VAR )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
Flag = VER_PARSE_FLAG_VAR;
break;
// the same for Constant 1
case VER_PARSE_SYM_CONST1:
Vec_PtrPush( vStackFn, b1 ); Cudd_Ref( b1 );
if ( Flag == VER_PARSE_FLAG_VAR )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
Flag = VER_PARSE_FLAG_VAR;
break;
case VER_PARSE_SYM_NEGBEF1:
case VER_PARSE_SYM_NEGBEF2:
if ( Flag == VER_PARSE_FLAG_VAR )
{// if NEGBEF follows a variable, AND is assumed
sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
break;
case VER_PARSE_SYM_AND:
case VER_PARSE_SYM_OR:
case VER_PARSE_SYM_XOR:
case VER_PARSE_SYM_MUX1:
case VER_PARSE_SYM_MUX2:
if ( Flag != VER_PARSE_FLAG_VAR )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
if ( *pTemp == VER_PARSE_SYM_AND )
Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
else if ( *pTemp == VER_PARSE_SYM_OR )
Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
else if ( *pTemp == VER_PARSE_SYM_XOR )
Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
else if ( *pTemp == VER_PARSE_SYM_MUX1 )
Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
// else if ( *pTemp == VER_PARSE_SYM_MUX2 )
// Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
Flag = VER_PARSE_FLAG_OPER;
break;
case VER_PARSE_SYM_OPEN:
if ( Flag == VER_PARSE_FLAG_VAR )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
// after an opening bracket, it feels like starting over again
Flag = VER_PARSE_FLAG_START;
break;
case VER_PARSE_SYM_CLOSE:
if ( Vec_IntSize( vStackOp ) )
{
while ( 1 )
{
if ( !Vec_IntSize( vStackOp ) )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
Oper = Vec_IntPop( vStackOp );
if ( Oper == VER_PARSE_OPER_MARK )
break;
// skip the second MUX operation
// if ( Oper == VER_PARSE_OPER_MUX2 )
// {
// Oper = Vec_IntPop( vStackOp );
// assert( Oper == VER_PARSE_OPER_MUX1 );
// }
// perform the given operation
if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper ) == NULL )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
return NULL;
}
}
}
else
{
sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
Flag = VER_PARSE_FLAG_ERROR;
break;
}
if ( Flag != VER_PARSE_FLAG_ERROR )
Flag = VER_PARSE_FLAG_VAR;
break;
default:
// scan the next name
v = Ver_FormulaParserFindVar( pTemp, vNames );
pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
// assume operation AND, if vars follow one another
if ( Flag == VER_PARSE_FLAG_VAR )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
return NULL;
}
bTemp = Cudd_bddIthVar(dd, v);
Vec_PtrPush( vStackFn, bTemp ); Cudd_Ref( bTemp );
Flag = VER_PARSE_FLAG_VAR;
break;
}
if ( Flag == VER_PARSE_FLAG_ERROR )
break; // error exit
else if ( Flag == VER_PARSE_FLAG_START )
continue; // go on parsing
else if ( Flag == VER_PARSE_FLAG_VAR )
while ( 1 )
{ // check if there are negations in the OpStack
if ( !Vec_IntSize(vStackOp) )
break;
Oper = Vec_IntPop( vStackOp );
if ( Oper != VER_PARSE_OPER_NEG )
{
Vec_IntPush( vStackOp, Oper );
break;
}
else
{
Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
}
}
else // if ( Flag == VER_PARSE_FLAG_OPER )
while ( 1 )
{ // execute all the operations in the OpStack
// with precedence higher or equal than the last one
Oper1 = Vec_IntPop( vStackOp ); // the last operation
if ( !Vec_IntSize(vStackOp) )
{ // if it is the only operation, push it back
Vec_IntPush( vStackOp, Oper1 );
break;
}
Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
if ( Oper2 >= Oper1 )
{ // if Oper2 precedence is higher or equal, execute it
if ( Ver_FormulaParserTopOper( dd, vStackFn, Oper2 ) == NULL )
{
sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
return NULL;
}
Vec_IntPush( vStackOp, Oper1 ); // push the last operation back
}
else
{ // if Oper2 precedence is lower, push them back and done
Vec_IntPush( vStackOp, Oper2 );
Vec_IntPush( vStackOp, Oper1 );
break;
}
}
}
if ( Flag != VER_PARSE_FLAG_ERROR )
{
if ( Vec_PtrSize(vStackFn) )
{
bFunc = Vec_PtrPop(vStackFn);
if ( !Vec_PtrSize(vStackFn) )
if ( !Vec_IntSize(vStackOp) )
{
Cudd_Deref( bFunc );
return bFunc;
}
else
sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
else
sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
}
else
sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
}
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bFunc );
return NULL;
}
/**Function*************************************************************
Synopsis [Performs the operation on the top entries in the stack.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Ver_FormulaParserTopOper( DdManager * dd, Vec_Ptr_t * vStackFn, int Oper )
{
DdNode * bArg0, * bArg1, * bArg2, * bFunc;
// perform the given operation
bArg2 = Vec_PtrPop( vStackFn );
bArg1 = Vec_PtrPop( vStackFn );
if ( Oper == VER_PARSE_OPER_AND )
bFunc = Cudd_bddAnd( dd, bArg1, bArg2 );
else if ( Oper == VER_PARSE_OPER_XOR )
bFunc = Cudd_bddXor( dd, bArg1, bArg2 );
else if ( Oper == VER_PARSE_OPER_OR )
bFunc = Cudd_bddOr( dd, bArg1, bArg2 );
else if ( Oper == VER_PARSE_OPER_EQU )
bFunc = Cudd_bddXnor( dd, bArg1, bArg2 );
else if ( Oper == VER_PARSE_OPER_MUX )
{
bArg0 = Vec_PtrPop( vStackFn );
bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bArg0 );
Cudd_Deref( bFunc );
}
else
return NULL;
Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bArg1 );
Cudd_RecursiveDeref( dd, bArg2 );
Vec_PtrPush( vStackFn, bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Returns the index of the new variable found.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
{
char * pTemp, * pTemp2;
int nLength, nLength2, i;
// find the end of the string delimited by other characters
pTemp = pString;
while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' &&
*pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE &&
*pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 &&
*pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR &&
*pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
pTemp++;
// look for this string in the array
nLength = pTemp - pString;
for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
{
nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 );
if ( nLength2 != nLength )
continue;
pTemp2 = Vec_PtrEntry( vNames, 2*i + 1 );
if ( strncmp( pTemp, pTemp2, nLength ) )
continue;
return i;
}
// could not find - add and return the number
Vec_PtrPush( vNames, (void *)nLength );
Vec_PtrPush( vNames, pString );
return i;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/verParse.c 0 → 100644
/**CFile****************************************************************
FileName [verParse.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Performs some Verilog parsing tasks.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: verParse.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Skips the comments of they are present.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_ParseSkipComments( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
char Symbol;
// skip spaces
Ver_StreamSkipChars( p, " \t\n\r" );
if ( !Ver_StreamIsOkey(pMan->pReader) )
return 1;
// read the first symbol
Symbol = Ver_StreamScanChar( p );
if ( Symbol != '/' )
return 1;
Ver_StreamPopChar( p );
// read the second symbol
Symbol = Ver_StreamScanChar( p );
if ( Symbol == '/' )
{ // skip till the end of line
Ver_StreamSkipToChars( p, "\n" );
return Ver_ParseSkipComments( pMan );
}
if ( Symbol == '*' )
{ // skip till the next occurance of */
Ver_StreamPopChar( p );
do {
Ver_StreamSkipToChars( p, "*" );
Ver_StreamPopChar( p );
} while ( Ver_StreamScanChar( p ) != '/' );
Ver_StreamPopChar( p );
return Ver_ParseSkipComments( pMan );
}
sprintf( pMan->sError, "Cannot parse after symbol \"/\"." );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
/**Function*************************************************************
Synopsis [Parses a Verilog name that can be being with a slash.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ver_ParseGetName( Ver_Man_t * pMan )
{
Ver_Stream_t * p = pMan->pReader;
char Symbol;
char * pWord;
if ( !Ver_StreamIsOkey(p) )
return NULL;
if ( !Ver_ParseSkipComments( pMan ) )
return NULL;
Symbol = Ver_StreamScanChar( p );
if ( Symbol == '\\' )
Ver_StreamPopChar( p );
pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
if ( !Ver_ParseSkipComments( pMan ) )
return NULL;
return pWord;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/verStream.c 0 → 100644
/**CFile****************************************************************
FileName [verStream.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Input file stream, which knows nothing about Verilog.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: verStream.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define VER_BUFFER_SIZE 1048576 // 1M - size of the data chunk stored in memory
#define VER_OFFSET_SIZE 4096 // 4K - load new data when less than this is left
#define VER_WORD_SIZE 4096 // 4K - the largest token that can be returned
#define VER_MINIMUM(a,b) (((a) < (b))? (a) : (b))
struct Ver_Stream_t_
{
// the input file
char * pFileName; // the input file name
FILE * pFile; // the input file pointer
int nFileSize; // the total number of bytes in the file
int nFileRead; // the number of bytes currently read from file
int nLineCounter; // the counter of lines processed
// temporary storage for data
char * pBuffer; // the buffer
int nBufferSize; // the size of the buffer
char * pBufferCur; // the current reading position
char * pBufferEnd; // the first position not used by currently loaded data
char * pBufferStop; // the position where loading new data will be done
// tokens given to the user
char pChars[VER_WORD_SIZE+5]; // temporary storage for a word (plus end-of-string and two parantheses)
int nChars; // the total number of characters in the word
// status of the parser
int fStop; // this flag goes high when the end of file is reached
};
static void Ver_StreamReload( Ver_Stream_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the file reader for the given file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ver_Stream_t * Ver_StreamAlloc( char * pFileName )
{
Ver_Stream_t * p;
FILE * pFile;
int nCharsToRead;
// check if the file can be opened
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Ver_StreamAlloc(): Cannot open input file \"%s\".\n", pFileName );
return NULL;
}
// start the file reader
p = ALLOC( Ver_Stream_t, 1 );
memset( p, 0, sizeof(Ver_Stream_t) );
p->pFileName = pFileName;
p->pFile = pFile;
// get the file size, in bytes
fseek( pFile, 0, SEEK_END );
p->nFileSize = ftell( pFile );
rewind( pFile );
// allocate the buffer
p->pBuffer = ALLOC( char, VER_BUFFER_SIZE+1 );
p->nBufferSize = VER_BUFFER_SIZE;
p->pBufferCur = p->pBuffer;
// determine how many chars to read
nCharsToRead = VER_MINIMUM(p->nFileSize, VER_BUFFER_SIZE);
// load the first part into the buffer
fread( p->pBuffer, nCharsToRead, 1, p->pFile );
p->nFileRead = nCharsToRead;
// set the ponters to the end and the stopping point
p->pBufferEnd = p->pBuffer + nCharsToRead;
p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
// start the arrays
p->nLineCounter = 1; // 1-based line counting
return p;
}
/**Function*************************************************************
Synopsis [Loads new data into the file reader.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_StreamReload( Ver_Stream_t * p )
{
int nCharsUsed, nCharsToRead;
assert( !p->fStop );
assert( p->pBufferCur > p->pBufferStop );
assert( p->pBufferCur < p->pBufferEnd );
// figure out how many chars are still not processed
nCharsUsed = p->pBufferEnd - p->pBufferCur;
// move the remaining data to the beginning of the buffer
memmove( p->pBuffer, p->pBufferCur, nCharsUsed );
p->pBufferCur = p->pBuffer;
// determine how many chars we will read
nCharsToRead = VER_MINIMUM( p->nBufferSize - nCharsUsed, p->nFileSize - p->nFileRead );
// read the chars
fread( p->pBuffer + nCharsUsed, nCharsToRead, 1, p->pFile );
p->nFileRead += nCharsToRead;
// set the ponters to the end and the stopping point
p->pBufferEnd = p->pBuffer + nCharsUsed + nCharsToRead;
p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
}
/**Function*************************************************************
Synopsis [Stops the file reader.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_StreamFree( Ver_Stream_t * p )
{
if ( p->pFile )
fclose( p->pFile );
FREE( p->pBuffer );
free( p );
}
/**Function*************************************************************
Synopsis [Returns the file size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ver_StreamGetFileName( Ver_Stream_t * p )
{
return p->pFileName;
}
/**Function*************************************************************
Synopsis [Returns the file size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_StreamGetFileSize( Ver_Stream_t * p )
{
return p->nFileSize;
}
/**Function*************************************************************
Synopsis [Returns the current reading position.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_StreamGetCurPosition( Ver_Stream_t * p )
{
return p->nFileRead - (p->pBufferEnd - p->pBufferCur);
}
/**Function*************************************************************
Synopsis [Returns the line number for the given token.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_StreamGetLineNumber( Ver_Stream_t * p )
{
return p->nLineCounter;
}
/**Function*************************************************************
Synopsis [Returns current symbol.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ver_StreamIsOkey( Ver_Stream_t * p )
{
return !p->fStop;
}
/**Function*************************************************************
Synopsis [Returns current symbol.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char Ver_StreamScanChar( Ver_Stream_t * p )
{
assert( !p->fStop );
return *p->pBufferCur;
}
/**Function*************************************************************
Synopsis [Returns current symbol and moves to the next.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char Ver_StreamPopChar( Ver_Stream_t * p )
{
assert( !p->fStop );
// check if the new data should to be loaded
if ( p->pBufferCur > p->pBufferStop )
Ver_StreamReload( p );
// check if there are symbols left
if ( p->pBufferCur == p->pBufferEnd ) // end of file
{
p->fStop = 1;
return -1;
}
return *p->pBufferCur++;
}
/**Function*************************************************************
Synopsis [Skips the current symbol and all symbols from the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip )
{
char * pChar, * pTemp;
assert( !p->fStop );
assert( pCharsToSkip != NULL );
// check if the new data should to be loaded
if ( p->pBufferCur > p->pBufferStop )
Ver_StreamReload( p );
// skip the symbols
for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
{
// count the lines
if ( *pChar == '\n' )
p->nLineCounter++;
// skip symbols as long as they are in the list
for ( pTemp = pCharsToSkip; *pTemp; pTemp++ )
if ( *pChar == *pTemp )
break;
if ( *pTemp == 0 ) // pChar is not found in the list
{
p->pBufferCur = pChar;
return;
}
}
// the file is finished or the last part continued
// through VER_OFFSET_SIZE chars till the end of the buffer
if ( p->pBufferStop == p->pBufferEnd ) // end of file
{
p->fStop = 1;
return;
}
printf( "Ver_StreamSkipSymbol() failed to parse the file \"%s\".\n", p->pFileName );
}
/**Function*************************************************************
Synopsis [Skips all symbols until encountering one from the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop )
{
char * pChar, * pTemp;
assert( !p->fStop );
assert( pCharsToStop != NULL );
// check if the new data should to be loaded
if ( p->pBufferCur > p->pBufferStop )
Ver_StreamReload( p );
// skip the symbols
for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
{
// count the lines
if ( *pChar == '\n' )
p->nLineCounter++;
// skip symbols as long as they are NOT in the list
for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
if ( *pChar == *pTemp )
break;
if ( *pTemp == 0 ) // pChar is not found in the list
continue;
// the symbol is found - move position and return
p->pBufferCur = pChar;
return;
}
// the file is finished or the last part continued
// through VER_OFFSET_SIZE chars till the end of the buffer
if ( p->pBufferStop == p->pBufferEnd ) // end of file
{
p->fStop = 1;
return;
}
printf( "Ver_StreamSkipToSymbol() failed to parse the file \"%s\".\n", p->pFileName );
}
/**Function*************************************************************
Synopsis [Returns current word delimited by the set of symbols.]
Description [Modifies the stream by inserting 0 at the first encounter
of one of the symbols in the list.]
SideEffects []
SeeAlso []
***********************************************************************/
char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop )
{
char * pChar, * pTemp;
if ( p->fStop )
return NULL;
assert( pCharsToStop != NULL );
// check if the new data should to be loaded
if ( p->pBufferCur > p->pBufferStop )
Ver_StreamReload( p );
// skip the symbols
p->nChars = 0;
for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
{
// count the lines
if ( *pChar == '\n' )
p->nLineCounter++;
// skip symbols as long as they are NOT in the list
for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
if ( *pChar == *pTemp )
break;
if ( *pTemp == 0 ) // pChar is not found in the list
{
p->pChars[p->nChars++] = *pChar;
if ( p->nChars == VER_WORD_SIZE )
return NULL;
continue;
}
// the symbol is found - move the position, set the word end, return the word
p->pBufferCur = pChar;
p->pChars[p->nChars] = 0;
return p->pChars;
}
// the file is finished or the last part continued
// through VER_OFFSET_SIZE chars till the end of the buffer
if ( p->pBufferStop == p->pBufferEnd ) // end of file
{
p->fStop = 1;
p->pChars[p->nChars] = 0;
return p->pChars;
}
printf( "Ver_StreamGetWord() failed to parse the file \"%s\".\n", p->pFileName );
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/verWords.c 0 → 100644
/**CFile****************************************************************
FileName [verWords.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Handles keywords that are currently supported.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: verWords.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/temp/ver/ver_.c 0 → 100644
/**CFile****************************************************************
FileName [ver_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Verilog parser.]
Synopsis [Parses several flavors of structural Verilog.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 19, 2006.]
Revision [$Id: ver_.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ver.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
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