mirror of https://github.com/YosysHQ/abc.git
Version abc61216
This commit is contained in:
parent
ae037e4503
commit
be6a484a99
8
abc.dsp
8
abc.dsp
|
|
@ -410,6 +410,10 @@ SOURCE=.\src\base\io\ioRead.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\io\ioReadAiger.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\io\ioReadBaf.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
@ -438,6 +442,10 @@ SOURCE=.\src\base\io\ioUtil.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\io\ioWriteAiger.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\base\io\ioWriteBaf.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
2
abc.rc
2
abc.rc
|
|
@ -1,7 +1,7 @@
|
|||
# global parameters
|
||||
set check # checks intermediate networks
|
||||
#set checkfio # prints warnings when fanins/fanouts are duplicated
|
||||
#set checkread # checks new networks after reading from file
|
||||
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 progressbar # display the progress bar
|
||||
|
|
|
|||
|
|
@ -87,15 +87,16 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
|
|||
{
|
||||
char * pMemory;
|
||||
int i, nBytes;
|
||||
assert( sizeof(Ivy_Obj_t) <= 64 );
|
||||
int EntrySizeMax = 128;
|
||||
assert( sizeof(Ivy_Obj_t) <= EntrySizeMax );
|
||||
assert( p->pListFree == NULL );
|
||||
// assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
|
||||
// allocate new memory page
|
||||
nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
|
||||
nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + EntrySizeMax;
|
||||
pMemory = ALLOC( char, nBytes );
|
||||
Vec_PtrPush( p->vChunks, pMemory );
|
||||
// align memory at the 32-byte boundary
|
||||
pMemory = pMemory + 64 - (((int)pMemory) & 63);
|
||||
pMemory = pMemory + EntrySizeMax - (((int)pMemory) & (EntrySizeMax-1));
|
||||
// remember the manager in the first entry
|
||||
Vec_PtrPush( p->vPages, pMemory );
|
||||
// break the memory down into nodes
|
||||
|
|
|
|||
|
|
@ -422,6 +422,10 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
|
|||
fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( !Abc_FrameIsFlagEnabled("checkfio") )
|
||||
return Value;
|
||||
|
||||
// go through the fanins of the object and make sure fanins have this object as a fanout
|
||||
Abc_ObjForEachFanin( pObj, pFanin, i )
|
||||
{
|
||||
|
|
@ -443,9 +447,6 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
|
|||
}
|
||||
}
|
||||
|
||||
if ( !Abc_FrameIsFlagEnabled("checkfio") )
|
||||
return Value;
|
||||
|
||||
// make sure fanins are not duplicated
|
||||
for ( i = 0; i < pObj->vFanins.nSize; i++ )
|
||||
for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
|
||||
|
|
@ -706,10 +707,10 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
|
|||
// for each PI of pNet1 find corresponding PI of pNet2 and reorder them
|
||||
Abc_NtkForEachBox( pNtk1, pObj1, i )
|
||||
{
|
||||
if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) ) != 0 )
|
||||
if ( strcmp( Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) ) != 0 )
|
||||
{
|
||||
printf( "Box #%d is different in network 1 ( \"%s\") and in network 2 (\"%s\").\n",
|
||||
i, Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkBox(pNtk2,i)) );
|
||||
i, Abc_ObjName(Abc_ObjFanout0(pObj1)), Abc_ObjName(Abc_ObjFanout0(Abc_NtkBox(pNtk2,i))) );
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -320,7 +320,7 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
|
|||
Abc_NtkForEachPo( pNtk, pObj, i )
|
||||
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
|
||||
Abc_NtkForEachBox( pNtk, pObj, i )
|
||||
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
|
||||
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(Abc_ObjFanout0(pObj));
|
||||
// order objects alphabetically
|
||||
qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *),
|
||||
(int (*)(const void *, const void *)) Abc_NodeCompareNames );
|
||||
|
|
|
|||
|
|
@ -7542,7 +7542,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pPars->fTruth = 0;
|
||||
pPars->nLatches = pNtk? Abc_NtkLatchNum(pNtk) : 0;
|
||||
pPars->fLiftLeaves = 0;
|
||||
pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
|
||||
pPars->pLutLib = Abc_FrameReadLibLut();
|
||||
pPars->pTimesArr = NULL;
|
||||
pPars->pTimesArr = NULL;
|
||||
pPars->pFuncCost = NULL;
|
||||
|
|
@ -7562,6 +7562,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
globalUtilOptind++;
|
||||
if ( pPars->nLutSize < 0 )
|
||||
goto usage;
|
||||
// if the LUT size is specified, disable library
|
||||
pPars->pLutLib = NULL;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
|
|
@ -7709,7 +7711,7 @@ usage:
|
|||
sprintf( LutSize, "library" );
|
||||
else
|
||||
sprintf( LutSize, "%d", pPars->nLutSize );
|
||||
fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrstvh]\n" );
|
||||
fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" );
|
||||
fprintf( pErr, "\t performs FPGA technology mapping of the network\n" );
|
||||
fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
|
||||
fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
|
||||
|
|
@ -7720,7 +7722,7 @@ usage:
|
|||
fprintf( pErr, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
|
||||
fprintf( pErr, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
|
||||
fprintf( pErr, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
|
||||
fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
|
||||
// fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
|
||||
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
fprintf( pErr, "\t-h : prints the command usage\n");
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
|
|||
/*
|
||||
{
|
||||
FILE * pTable;
|
||||
pTable = fopen( "a/seqmap__stats.txt", "a+" );
|
||||
pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
|
||||
fprintf( pTable, "%s ", pNtk->pName );
|
||||
fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
|
||||
fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
|
||||
|
|
|
|||
168
src/base/io/io.c
168
src/base/io/io.c
|
|
@ -26,6 +26,7 @@
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
|
|
@ -37,6 +38,7 @@ 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 );
|
||||
|
||||
static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
|
||||
|
|
@ -71,6 +73,7 @@ extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fC
|
|||
void Io_Init( Abc_Frame_t * pAbc )
|
||||
{
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
|
||||
|
|
@ -82,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
|
||||
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
|
||||
|
|
@ -157,7 +161,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -177,7 +181,80 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t read the network from file in Verilog/BLIF/BENCH format\n" );
|
||||
fprintf( pAbc->Err, "\t read the network from file in BLIF/BENCH/PLA/BAF/AIGER format\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 IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Abc_Ntk_t * pNtk;
|
||||
char * FileName;
|
||||
FILE * pFile;
|
||||
int fCheck;
|
||||
int c;
|
||||
|
||||
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, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
}
|
||||
fclose( pFile );
|
||||
|
||||
// set the new network
|
||||
pNtk = Io_ReadAiger( FileName, fCheck );
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pAbc->Err, "Reading network from the AIGER file has failed.\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
// replace the current network
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t read the network in the AIGER format (http://fmv.jku.at/aiger)\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" );
|
||||
|
|
@ -229,7 +306,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -240,7 +317,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pNtk = Io_ReadBaf( FileName, fCheck );
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pAbc->Err, "Reading network from BAF file has failed.\n" );
|
||||
fprintf( pAbc->Err, "Reading network from the BAF file has failed.\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
@ -302,7 +379,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -383,7 +460,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -463,7 +540,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -543,7 +620,7 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -626,7 +703,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -709,7 +786,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -799,7 +876,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -875,7 +952,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
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" ) )
|
||||
if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
|
||||
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
|
||||
fprintf( pAbc->Err, "\n" );
|
||||
return 1;
|
||||
|
|
@ -981,6 +1058,65 @@ usage:
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
|
||||
{
|
||||
Abc_Ntk_t * pNtk;
|
||||
char * FileName;
|
||||
int c;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
|
||||
pNtk = pAbc->pNtkCur;
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
fprintf( pAbc->Out, "Empty network.\n" );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( argc != globalUtilOptind + 1 )
|
||||
{
|
||||
goto usage;
|
||||
}
|
||||
FileName = argv[globalUtilOptind];
|
||||
|
||||
// check the network type
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
fprintf( pAbc->Out, "Writing AIGER is only possible for structurally hashed AIGs.\n" );
|
||||
return 0;
|
||||
}
|
||||
Io_WriteAiger( pNtk, FileName );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: write_aiger [-lh] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -1026,7 +1162,7 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
// check the network type
|
||||
if ( !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
fprintf( pAbc->Out, "Currently can only write strashed combinational AIGs.\n" );
|
||||
fprintf( pAbc->Out, "Writing BAF is only possible for structurally hashed AIGs.\n" );
|
||||
return 0;
|
||||
}
|
||||
Io_WriteBaf( pNtk, FileName );
|
||||
|
|
@ -1036,7 +1172,7 @@ usage:
|
|||
fprintf( pAbc->Err, "usage: write_baf [-lh] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .baf)\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
@ -1102,7 +1238,7 @@ usage:
|
|||
fprintf( pAbc->Err, "\t write the network into a BLIF file\n" );
|
||||
fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
@ -1176,7 +1312,7 @@ usage:
|
|||
fprintf( pAbc->Err, "\t write the network in BENCH format\n" );
|
||||
// fprintf( pAbc->Err, "\t-l : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -51,6 +51,8 @@ extern "C" {
|
|||
|
||||
/*=== abcRead.c ==========================================================*/
|
||||
extern Abc_Ntk_t * Io_Read( char * pFileName, int fCheck );
|
||||
/*=== abcReadAiger.c ==========================================================*/
|
||||
extern Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck );
|
||||
/*=== abcReadBaf.c ==========================================================*/
|
||||
extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck );
|
||||
/*=== abcReadBlif.c ==========================================================*/
|
||||
|
|
@ -75,6 +77,8 @@ extern Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bo
|
|||
extern Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
|
||||
extern Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
|
||||
extern FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
|
||||
/*=== abcWriteAiger.c ==========================================================*/
|
||||
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
|
||||
/*=== abcWriteBaf.c ==========================================================*/
|
||||
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
|
||||
/*=== abcWriteBlif.c ==========================================================*/
|
||||
|
|
|
|||
|
|
@ -60,6 +60,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
|
|||
pNtk = Io_ReadEqn( pFileName, fCheck );
|
||||
else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) )
|
||||
return Io_ReadBaf( pFileName, fCheck );
|
||||
else if ( Extra_FileNameCheckExtension( pFileName, "aig" ) )
|
||||
return Io_ReadAiger( pFileName, fCheck );
|
||||
else
|
||||
{
|
||||
fprintf( stderr, "Unknown file format\n" );
|
||||
|
|
|
|||
|
|
@ -0,0 +1,273 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [ioReadAiger.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Command processing package.]
|
||||
|
||||
Synopsis [Procedures to read binary AIGER format developed by
|
||||
Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - December 16, 2006.]
|
||||
|
||||
Revision [$Id: ioReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "io.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static unsigned Io_ReadAigerDecode( char ** ppPos );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Reads the AIG in the binary AIGER format.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
|
||||
{
|
||||
ProgressBar * pProgress;
|
||||
FILE * pFile;
|
||||
Vec_Ptr_t * vNodes, * vTerms;
|
||||
Abc_Obj_t * pObj, * pNode0, * pNode1;
|
||||
Abc_Ntk_t * pNtkNew;
|
||||
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
|
||||
char * pContents, * pDrivers, * pSymbols, * pCur, * pName, * pType;
|
||||
unsigned uLit0, uLit1, uLit;
|
||||
|
||||
// read the file into the buffer
|
||||
nFileSize = Extra_FileSize( pFileName );
|
||||
pFile = fopen( pFileName, "rb" );
|
||||
pContents = ALLOC( char, nFileSize );
|
||||
fread( pContents, nFileSize, 1, pFile );
|
||||
fclose( pFile );
|
||||
|
||||
// check if the input file format is correct
|
||||
if ( strncmp(pContents, "aig", 3) != 0 )
|
||||
{
|
||||
fprintf( stdout, "Wrong input file format." );
|
||||
return NULL;
|
||||
}
|
||||
|
||||
// allocate the empty AIG
|
||||
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
|
||||
pName = Extra_FileNameGeneric( pFileName );
|
||||
pNtkNew->pName = Extra_UtilStrsav( pName );
|
||||
pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
|
||||
free( pName );
|
||||
|
||||
|
||||
// read the file type
|
||||
pCur = pContents; while ( *pCur++ != ' ' );
|
||||
// read the number of objects
|
||||
nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
|
||||
// read the number of inputs
|
||||
nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
|
||||
// read the number of latches
|
||||
nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
|
||||
// read the number of outputs
|
||||
nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
|
||||
// read the number of nodes
|
||||
nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
|
||||
// check the parameters
|
||||
if ( nTotal != nInputs + nLatches + nAnds )
|
||||
{
|
||||
fprintf( stdout, "The paramters are wrong." );
|
||||
return NULL;
|
||||
}
|
||||
|
||||
// prepare the array of nodes
|
||||
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
|
||||
Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
|
||||
|
||||
// create the PIs
|
||||
for ( i = 0; i < nInputs; i++ )
|
||||
{
|
||||
pObj = Abc_NtkCreatePi(pNtkNew);
|
||||
Vec_PtrPush( vNodes, pObj );
|
||||
}
|
||||
// create the POs
|
||||
for ( i = 0; i < nOutputs; i++ )
|
||||
{
|
||||
pObj = Abc_NtkCreatePo(pNtkNew);
|
||||
}
|
||||
// create the latches
|
||||
nDigits = Extra_Base10Log( nLatches );
|
||||
for ( i = 0; i < nLatches; i++ )
|
||||
{
|
||||
pObj = Abc_NtkCreateLatch(pNtkNew);
|
||||
Abc_LatchSetInit0( pObj );
|
||||
pNode0 = Abc_NtkCreateBi(pNtkNew);
|
||||
pNode1 = Abc_NtkCreateBo(pNtkNew);
|
||||
Abc_ObjAddFanin( pObj, pNode0 );
|
||||
Abc_ObjAddFanin( pNode1, pObj );
|
||||
Vec_PtrPush( vNodes, pNode1 );
|
||||
// assign names to latch and its input
|
||||
Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
|
||||
}
|
||||
|
||||
// remember the beginning of latch/PO literals
|
||||
pDrivers = pCur;
|
||||
|
||||
// scroll to the beginning of the binary data
|
||||
for ( i = 0; i < nLatches + nOutputs; )
|
||||
if ( *pCur++ == '\n' )
|
||||
i++;
|
||||
|
||||
// create the AND gates
|
||||
pProgress = Extra_ProgressBarStart( stdout, nAnds );
|
||||
for ( i = 0; i < nAnds; i++ )
|
||||
{
|
||||
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
||||
uLit = ((i + 1 + nInputs + nLatches) << 1);
|
||||
uLit1 = uLit - Io_ReadAigerDecode( &pCur );
|
||||
uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
|
||||
assert( uLit1 > uLit0 );
|
||||
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
|
||||
pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
|
||||
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
|
||||
Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
|
||||
}
|
||||
Extra_ProgressBarStop( pProgress );
|
||||
|
||||
// remember the place where symbols begin
|
||||
pSymbols = pCur;
|
||||
|
||||
// read the latch driver literals
|
||||
pCur = pDrivers;
|
||||
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
|
||||
{
|
||||
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
|
||||
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
|
||||
Abc_ObjAddFanin( pObj, pNode0 );
|
||||
}
|
||||
// read the PO driver literals
|
||||
Abc_NtkForEachPo( pNtkNew, pObj, i )
|
||||
{
|
||||
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
|
||||
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) );
|
||||
Abc_ObjAddFanin( pObj, pNode0 );
|
||||
}
|
||||
|
||||
// read the names if present
|
||||
pCur = pSymbols;
|
||||
while ( pCur < pContents + nFileSize && *pCur != 'c' )
|
||||
{
|
||||
// get the terminal type
|
||||
pType = pCur;
|
||||
if ( *pCur == 'i' )
|
||||
vTerms = pNtkNew->vPis;
|
||||
else if ( *pCur == 'l' )
|
||||
vTerms = pNtkNew->vBoxes;
|
||||
else if ( *pCur == 'o' )
|
||||
vTerms = pNtkNew->vPos;
|
||||
else
|
||||
{
|
||||
fprintf( stdout, "Wrong terminal type." );
|
||||
return NULL;
|
||||
}
|
||||
// get the terminal number
|
||||
iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
|
||||
// get the node
|
||||
if ( iTerm >= Vec_PtrSize(vTerms) )
|
||||
{
|
||||
fprintf( stdout, "The number of terminal is out of bound." );
|
||||
return NULL;
|
||||
}
|
||||
pObj = Vec_PtrEntry( vTerms, iTerm );
|
||||
if ( *pType == 'l' )
|
||||
pObj = Abc_ObjFanout0(pObj);
|
||||
// assign the name
|
||||
pName = pCur; while ( *pCur++ != '\n' );
|
||||
// assign this name
|
||||
*(pCur-1) = 0;
|
||||
Abc_ObjAssignName( pObj, pName, NULL );
|
||||
if ( *pType == 'l' )
|
||||
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
|
||||
// mark the node as named
|
||||
pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
|
||||
}
|
||||
// skipping the comments
|
||||
free( pContents );
|
||||
Vec_PtrFree( vNodes );
|
||||
|
||||
// assign the remaining names
|
||||
Abc_NtkForEachPi( pNtkNew, pObj, i )
|
||||
{
|
||||
if ( pObj->pCopy ) continue;
|
||||
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
|
||||
}
|
||||
Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
|
||||
{
|
||||
if ( pObj->pCopy ) continue;
|
||||
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
|
||||
Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL );
|
||||
}
|
||||
Abc_NtkForEachPo( pNtkNew, pObj, i )
|
||||
{
|
||||
if ( pObj->pCopy ) continue;
|
||||
Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
|
||||
}
|
||||
|
||||
// remove the extra nodes
|
||||
// Abc_AigCleanup( pNtkNew->pManFunc );
|
||||
|
||||
// check the result
|
||||
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
|
||||
{
|
||||
printf( "Io_ReadAiger: The network check has failed.\n" );
|
||||
Abc_NtkDelete( pNtkNew );
|
||||
return NULL;
|
||||
}
|
||||
return pNtkNew;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Extracts one unsigned AIG edge from the input buffer.]
|
||||
|
||||
Description [This procedure is a slightly modified version of Armin Biere's
|
||||
procedure "unsigned decode (FILE * file)". ]
|
||||
|
||||
SideEffects [Updates the current reading position.]
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
unsigned Io_ReadAigerDecode( char ** ppPos )
|
||||
{
|
||||
unsigned x = 0, i = 0;
|
||||
unsigned char ch;
|
||||
|
||||
// while ((ch = getnoneofch (file)) & 0x80)
|
||||
while ((ch = *(*ppPos)++) & 0x80)
|
||||
x |= (ch & 0x7f) << (7 * i++);
|
||||
|
||||
return x | (ch << (7 * i));
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -30,7 +30,7 @@
|
|||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes the AIG in the binary format.]
|
||||
Synopsis [Reads the AIG in the binary format.]
|
||||
|
||||
Description []
|
||||
|
||||
|
|
@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
|
|||
Vec_PtrFree( vNodes );
|
||||
|
||||
// remove the extra nodes
|
||||
Abc_AigCleanup( pNtkNew->pManFunc );
|
||||
// Abc_AigCleanup( pNtkNew->pManFunc );
|
||||
|
||||
// check the result
|
||||
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
|
||||
|
|
|
|||
|
|
@ -0,0 +1,281 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [ioWriteAiger.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Command processing package.]
|
||||
|
||||
Synopsis [Procedures to write binary AIGER format developed by
|
||||
Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - December 16, 2006.]
|
||||
|
||||
Revision [$Id: ioWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "io.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*
|
||||
The following is taken from the AIGER format description,
|
||||
which can be found at http://fmv.jku.at/aiger
|
||||
*/
|
||||
|
||||
|
||||
/*
|
||||
The AIGER And-Inverter Graph (AIG) Format Version 20061129
|
||||
----------------------------------------------------------
|
||||
Armin Biere, Johannes Kepler University, 2006
|
||||
|
||||
This report describes the AIG file format as used by the AIGER library.
|
||||
The purpose of this report is not only to motivate and document the
|
||||
format, but also to allow independent implementations of writers and
|
||||
readers by giving precise and unambiguous definitions.
|
||||
|
||||
...
|
||||
|
||||
Introduction
|
||||
|
||||
The name AIGER contains as one part the acronym AIG of And-Inverter
|
||||
Graphs and also if pronounced in German sounds like the name of the
|
||||
'Eiger', a mountain in the Swiss alps. This choice should emphasize the
|
||||
origin of this format. It was first openly discussed at the Alpine
|
||||
Verification Meeting 2006 in Ascona as a way to provide a simple, compact
|
||||
file format for a model checking competition affiliated to CAV 2007.
|
||||
|
||||
...
|
||||
|
||||
Binary Format Definition
|
||||
|
||||
The binary format is semantically a subset of the ASCII format with a
|
||||
slightly different syntax. The binary format may need to reencode
|
||||
literals, but translating a file in binary format into ASCII format and
|
||||
then back in to binary format will result in the same file.
|
||||
|
||||
The main differences of the binary format to the ASCII format are as
|
||||
follows. After the header the list of input literals and all the
|
||||
current state literals of a latch can be omitted. Furthermore the
|
||||
definitions of the AND gates are binary encoded. However, the symbol
|
||||
table and the comment section are as in the ASCII format.
|
||||
|
||||
The header of an AIGER file in binary format has 'aig' as format
|
||||
identifier, but otherwise is identical to the ASCII header. The standard
|
||||
file extension for the binary format is therefore '.aig'.
|
||||
|
||||
A header for the binary format is still in ASCII encoding:
|
||||
|
||||
aig M I L O A
|
||||
|
||||
Constants, variables and literals are handled in the same way as in the
|
||||
ASCII format. The first simplifying restriction is on the variable
|
||||
indices of inputs and latches. The variable indices of inputs come first,
|
||||
followed by the pseudo-primary inputs of the latches and then the variable
|
||||
indices of all LHS of AND gates:
|
||||
|
||||
input variable indices 1, 2, ... , I
|
||||
latch variable indices I+1, I+2, ... , (I+L)
|
||||
AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
|
||||
|
||||
The corresponding unsigned literals are
|
||||
|
||||
input literals 2, 4, ... , 2*I
|
||||
latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
|
||||
AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
|
||||
|
||||
All literals have to be defined, and therefore 'M = I + L + A'. With this
|
||||
restriction it becomes possible that the inputs and the current state
|
||||
literals of the latches do not have to be listed explicitly. Therefore,
|
||||
after the header only the list of 'L' next state literals follows, one per
|
||||
latch on a single line, and then the 'O' outputs, again one per line.
|
||||
|
||||
In the binary format we assume that the AND gates are ordered and respect
|
||||
the child parent relation. AND gates with smaller literals on the LHS
|
||||
come first. Therefore we can assume that the literals on the right-hand
|
||||
side of a definition of an AND gate are smaller than the LHS literal.
|
||||
Furthermore we can sort the literals on the RHS, such that the larger
|
||||
literal comes first. A definition thus consists of three literals
|
||||
|
||||
lhs rhs0 rhs1
|
||||
|
||||
with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
|
||||
pairwise different to avoid combinational self loops. Since the LHS
|
||||
indices of the definitions are all consecutive (as even integers),
|
||||
the binary format does not have to keep 'lhs'. In addition, we can use
|
||||
the order restriction and only write the differences 'delta0' and 'delta1'
|
||||
instead of 'rhs0' and 'rhs1', with
|
||||
|
||||
delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
|
||||
|
||||
The differences will all be strictly positive, and in practice often very
|
||||
small. We can take advantage of this fact by the simple little-endian
|
||||
encoding of unsigned integers of the next section. After the binary delta
|
||||
encoding of the RHSs of all AND gates, the optional symbol table and
|
||||
optional comment section start in the same format as in the ASCII case.
|
||||
|
||||
...
|
||||
|
||||
*/
|
||||
|
||||
static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
|
||||
static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)pObj->pCopy; }
|
||||
static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (void *)Num; }
|
||||
|
||||
static int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Writes the AIG in the binary AIGER format.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
|
||||
{
|
||||
ProgressBar * pProgress;
|
||||
FILE * pFile;
|
||||
Abc_Obj_t * pObj, * pDriver;
|
||||
int i, nNodes, Pos, nBufferSize;
|
||||
unsigned char * pBuffer;
|
||||
unsigned uLit0, uLit1, uLit;
|
||||
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
// start the output stream
|
||||
pFile = fopen( pFileName, "wb" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
fprintf( stdout, "Io_WriteBaf(): Cannot open the output file \"%s\".\n", pFileName );
|
||||
return;
|
||||
}
|
||||
|
||||
// set the node numbers to be used in the output file
|
||||
nNodes = 0;
|
||||
Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
|
||||
Abc_NtkForEachCi( pNtk, pObj, i )
|
||||
Io_ObjSetAigerNum( pObj, nNodes++ );
|
||||
Abc_AigForEachAnd( pNtk, pObj, i )
|
||||
Io_ObjSetAigerNum( pObj, nNodes++ );
|
||||
|
||||
// write the header "M I L O A" where M = I + L + A
|
||||
fprintf( pFile, "aig %u %u %u %u %u\n",
|
||||
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
|
||||
Abc_NtkPiNum(pNtk),
|
||||
Abc_NtkLatchNum(pNtk),
|
||||
Abc_NtkPoNum(pNtk),
|
||||
Abc_NtkNodeNum(pNtk) );
|
||||
|
||||
// if the driver node is a constant, we need to complement the literal below
|
||||
// because, in the AIGER format, literal 0/1 is represented as number 0/1
|
||||
// while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
|
||||
|
||||
// write latch drivers
|
||||
Abc_NtkForEachLatchInput( pNtk, pObj, i )
|
||||
{
|
||||
pDriver = Abc_ObjFanin0(pObj);
|
||||
fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
|
||||
}
|
||||
|
||||
// write PO drivers
|
||||
Abc_NtkForEachPo( pNtk, pObj, i )
|
||||
{
|
||||
pDriver = Abc_ObjFanin0(pObj);
|
||||
fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
|
||||
}
|
||||
|
||||
// write the nodes into the buffer
|
||||
Pos = 0;
|
||||
nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
|
||||
pBuffer = ALLOC( char, nBufferSize );
|
||||
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
|
||||
Abc_AigForEachAnd( pNtk, pObj, i )
|
||||
{
|
||||
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
||||
uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
|
||||
uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
|
||||
uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
|
||||
assert( uLit0 < uLit1 );
|
||||
Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
|
||||
Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
|
||||
if ( Pos > nBufferSize - 10 )
|
||||
{
|
||||
printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
|
||||
fclose( pFile );
|
||||
return;
|
||||
}
|
||||
}
|
||||
assert( Pos < nBufferSize );
|
||||
Extra_ProgressBarStop( pProgress );
|
||||
|
||||
// write the buffer
|
||||
fwrite( pBuffer, 1, Pos, pFile );
|
||||
free( pBuffer );
|
||||
|
||||
// write the symbol table
|
||||
// write PIs
|
||||
Abc_NtkForEachPi( pNtk, pObj, i )
|
||||
fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
|
||||
// write latches
|
||||
Abc_NtkForEachLatch( pNtk, pObj, i )
|
||||
fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
|
||||
// write POs
|
||||
Abc_NtkForEachPo( pNtk, pObj, i )
|
||||
fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
|
||||
|
||||
// write the comment
|
||||
fprintf( pFile, "c\n" );
|
||||
fprintf( pFile, "%s\n", pNtk->pName );
|
||||
fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() );
|
||||
fprintf( pFile, "For information about the format, refer to %s\n", "http://fmv.jku.at/aiger" );
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Adds one unsigned AIG edge to the output buffer.]
|
||||
|
||||
Description [This procedure is a slightly modified version of Armin Biere's
|
||||
procedure "void encode (FILE * file, unsigned x)" ]
|
||||
|
||||
SideEffects [Returns the current writing position.]
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
|
||||
{
|
||||
unsigned char ch;
|
||||
while (x & ~0x7f)
|
||||
{
|
||||
ch = (x & 0x7f) | 0x80;
|
||||
// putc (ch, file);
|
||||
pBuffer[Pos++] = ch;
|
||||
x >>= 7;
|
||||
}
|
||||
ch = x;
|
||||
// putc (ch, file);
|
||||
pBuffer[Pos++] = ch;
|
||||
return Pos;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -1,5 +1,6 @@
|
|||
SRC += src/base/io/io.c \
|
||||
src/base/io/ioRead.c \
|
||||
src/base/io/ioReadAiger.c \
|
||||
src/base/io/ioReadBaf.c \
|
||||
src/base/io/ioReadBench.c \
|
||||
src/base/io/ioReadBlif.c \
|
||||
|
|
@ -8,6 +9,7 @@ SRC += src/base/io/io.c \
|
|||
src/base/io/ioReadPla.c \
|
||||
src/base/io/ioReadVerilog.c \
|
||||
src/base/io/ioUtil.c \
|
||||
src/base/io/ioWriteAiger.c \
|
||||
src/base/io/ioWriteBaf.c \
|
||||
src/base/io/ioWriteBench.c \
|
||||
src/base/io/ioWriteBlif.c \
|
||||
|
|
|
|||
|
|
@ -340,7 +340,7 @@ float Fpga_CutGetAreaRefed( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
|
|||
return 0;
|
||||
aResult = Fpga_CutDeref( pMan, NULL, pCut, 0 );
|
||||
aResult2 = Fpga_CutRef( pMan, NULL, pCut, 0 );
|
||||
assert( aResult == aResult2 );
|
||||
assert( Fpga_FloatEqual( pMan, aResult, aResult2 ) );
|
||||
return aResult;
|
||||
}
|
||||
|
||||
|
|
@ -362,7 +362,7 @@ float Fpga_CutGetAreaDerefed( Fpga_Man_t * pMan, Fpga_Cut_t * pCut )
|
|||
return 0;
|
||||
aResult2 = Fpga_CutRef( pMan, NULL, pCut, 0 );
|
||||
aResult = Fpga_CutDeref( pMan, NULL, pCut, 0 );
|
||||
assert( aResult == aResult2 );
|
||||
assert( Fpga_FloatEqual( pMan, aResult, aResult2 ) );
|
||||
return aResult;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -278,6 +278,10 @@ struct Fpga_NodeVecStruct_t_
|
|||
pFanout = pFanout2, \
|
||||
pFanout2 = Fpga_NodeReadNextFanout(pNode, pFanout) )
|
||||
|
||||
static inline Fpga_FloatMoreThan( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 > Arg2 + p->fEpsilon; }
|
||||
static inline Fpga_FloatLessThan( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 < Arg2 - p->fEpsilon; }
|
||||
static inline Fpga_FloatEqual( Fpga_Man_t * p, float Arg1, float Arg2 ) { return Arg1 > Arg2 - p->fEpsilon && Arg1 < Arg2 + p->fEpsilon; }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// GLOBAL VARIABLES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -140,7 +140,7 @@ clk = clock();
|
|||
Fpga_CutGetParameters( p, pCut );
|
||||
//p->time2 += clock() - clk;
|
||||
// drop the cut if it does not meet the required times
|
||||
if ( pCut->tArrival > pNode->tRequired )
|
||||
if ( Fpga_FloatMoreThan(p, pCut->tArrival, pNode->tRequired) )
|
||||
continue;
|
||||
// if no cut is assigned, use the current one
|
||||
if ( pNode->pCutBest == NULL )
|
||||
|
|
@ -152,11 +152,11 @@ clk = clock();
|
|||
// (1) delay oriented mapping (first traversal), delay first, area-flow as a tie-breaker
|
||||
// (2) area recovery (subsequent traversals), area-flow first, delay as a tie-breaker
|
||||
if ( (fDelayOriented &&
|
||||
(pNode->pCutBest->tArrival > pCut->tArrival ||
|
||||
pNode->pCutBest->tArrival == pCut->tArrival && pNode->pCutBest->aFlow > pCut->aFlow)) ||
|
||||
(Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) ||
|
||||
Fpga_FloatEqual(p, pNode->pCutBest->tArrival, pCut->tArrival) && Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) )) ||
|
||||
(!fDelayOriented &&
|
||||
(pNode->pCutBest->aFlow > pCut->aFlow ||
|
||||
pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival)) )
|
||||
(Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
|
||||
Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival))) )
|
||||
{
|
||||
pNode->pCutBest = pCut;
|
||||
}
|
||||
|
|
@ -289,7 +289,7 @@ clk = clock();
|
|||
pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
|
||||
//p->time2 += clock() - clk;
|
||||
// drop the cut if it does not meet the required times
|
||||
if ( pCut->tArrival > pNode->tRequired )
|
||||
if ( Fpga_FloatMoreThan( p, pCut->tArrival, pNode->tRequired ) )
|
||||
continue;
|
||||
// get the area of this cut
|
||||
pCut->aFlow = Fpga_CutGetAreaDerefed( p, pCut );
|
||||
|
|
@ -300,8 +300,8 @@ clk = clock();
|
|||
continue;
|
||||
}
|
||||
// choose the best cut as follows: exact area first, delay as a tie-breaker
|
||||
if ( pNode->pCutBest->aFlow > pCut->aFlow ||
|
||||
pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival )
|
||||
if ( Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
|
||||
Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) )
|
||||
{
|
||||
pNode->pCutBest = pCut;
|
||||
}
|
||||
|
|
@ -410,7 +410,7 @@ clk = clock();
|
|||
pCut->tArrival = Fpga_TimeCutComputeArrival( p, pCut );
|
||||
//p->time2 += clock() - clk;
|
||||
// drop the cut if it does not meet the required times
|
||||
if ( pCut->tArrival > pNode->tRequired )
|
||||
if ( Fpga_FloatMoreThan( p, pCut->tArrival, pNode->tRequired ) )
|
||||
continue;
|
||||
// get the area of this cut
|
||||
pCut->aFlow = Fpga_CutGetSwitchDerefed( p, pNode, pCut );
|
||||
|
|
@ -421,8 +421,8 @@ clk = clock();
|
|||
continue;
|
||||
}
|
||||
// choose the best cut as follows: exact area first, delay as a tie-breaker
|
||||
if ( pNode->pCutBest->aFlow > pCut->aFlow ||
|
||||
pNode->pCutBest->aFlow == pCut->aFlow && pNode->pCutBest->tArrival > pCut->tArrival )
|
||||
if ( Fpga_FloatMoreThan(p, pNode->pCutBest->aFlow, pCut->aFlow) ||
|
||||
Fpga_FloatEqual(p, pNode->pCutBest->aFlow, pCut->aFlow) && Fpga_FloatMoreThan(p, pNode->pCutBest->tArrival, pCut->tArrival) )
|
||||
{
|
||||
pNode->pCutBest = pCut;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -273,10 +273,10 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r
|
|||
#define If_ObjForEachCutStart( pObj, pCut, i, Start ) \
|
||||
for ( i = Start; (i < (int)(pObj)->nCuts) && ((pCut) = (pObj)->Cuts + i); i++ )
|
||||
// iterator over the leaves of the cut
|
||||
//#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
|
||||
// for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
|
||||
#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
|
||||
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
|
||||
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
|
||||
//#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \
|
||||
// for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
|
||||
// iterator over the leaves of the sequential cut
|
||||
#define If_CutForEachLeafSeq( p, pCut, pLeaf, Shift, i ) \
|
||||
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i] >> 8)) && (((Shift) = ((pCut)->pLeaves[i] & 255)) >= 0); i++ )
|
||||
|
|
|
|||
|
|
@ -257,9 +257,11 @@ static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t
|
|||
pC->pLeaves[k++] = pC1->pLeaves[i];
|
||||
pC->nLeaves++;
|
||||
}
|
||||
/*
|
||||
assert( pC->nLeaves <= pC->nLimit );
|
||||
for ( i = 1; i < (int)pC->nLeaves; i++ )
|
||||
assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
|
||||
*/
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
@ -574,7 +576,8 @@ float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
|
|||
assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
|
||||
aResult2 = If_CutRef( p, pCut, nLevels );
|
||||
aResult = If_CutDeref( p, pCut, nLevels );
|
||||
assert( aResult == aResult2 );
|
||||
assert( aResult > aResult2 - p->fEpsilon );
|
||||
assert( aResult < aResult2 + p->fEpsilon );
|
||||
return aResult;
|
||||
}
|
||||
|
||||
|
|
@ -595,7 +598,8 @@ float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
|
|||
assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
|
||||
aResult2 = If_CutDeref( p, pCut, nLevels );
|
||||
aResult = If_CutRef( p, pCut, nLevels );
|
||||
assert( aResult == aResult2 );
|
||||
assert( aResult > aResult2 - p->fEpsilon );
|
||||
assert( aResult < aResult2 + p->fEpsilon );
|
||||
return aResult;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -189,38 +189,43 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
|
|||
pCut = p->ppCuts[iCut];
|
||||
// generate cuts
|
||||
for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
|
||||
If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
|
||||
{
|
||||
assert( pTemp->nCuts > 1 );
|
||||
assert( pTemp == pObj || pTemp->nRefs == 0 );
|
||||
// copy the cut into storage
|
||||
If_CutCopy( pCut, pCutTemp );
|
||||
// check if this cut is contained in any of the available cuts
|
||||
if ( If_CutFilter( p, pCut ) )
|
||||
continue;
|
||||
// the cuts have been successfully merged
|
||||
// check if the cut satisfies the required times
|
||||
assert( pCut->Delay == If_CutDelay( p, pCut ) );
|
||||
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
|
||||
continue;
|
||||
// set the phase attribute
|
||||
pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
|
||||
// compute area of the cut (this area may depend on the application specific cost)
|
||||
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
|
||||
pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
|
||||
// make sure the cut is the last one (after filtering it may not be so)
|
||||
assert( pCut == p->ppCuts[iCut] );
|
||||
p->ppCuts[iCut] = p->ppCuts[p->nCuts];
|
||||
p->ppCuts[p->nCuts] = pCut;
|
||||
// count the cut
|
||||
p->nCuts++;
|
||||
// prepare room for the next cut
|
||||
iCut = p->nCuts;
|
||||
pCut = p->ppCuts[iCut];
|
||||
If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
|
||||
{
|
||||
assert( pTemp->nCuts > 1 );
|
||||
assert( pTemp == pObj || pTemp->nRefs == 0 );
|
||||
// copy the cut into storage
|
||||
If_CutCopy( pCut, pCutTemp );
|
||||
// check if this cut is contained in any of the available cuts
|
||||
if ( If_CutFilter( p, pCut ) )
|
||||
continue;
|
||||
// the cuts have been successfully merged
|
||||
// check if the cut satisfies the required times
|
||||
assert( pCut->Delay == If_CutDelay( p, pCut ) );
|
||||
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
|
||||
continue;
|
||||
// set the phase attribute
|
||||
pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
|
||||
// compute area of the cut (this area may depend on the application specific cost)
|
||||
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
|
||||
pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
|
||||
// make sure the cut is the last one (after filtering it may not be so)
|
||||
assert( pCut == p->ppCuts[iCut] );
|
||||
p->ppCuts[iCut] = p->ppCuts[p->nCuts];
|
||||
p->ppCuts[p->nCuts] = pCut;
|
||||
// count the cut
|
||||
p->nCuts++;
|
||||
// prepare room for the next cut
|
||||
iCut = p->nCuts;
|
||||
pCut = p->ppCuts[iCut];
|
||||
// quit if we exceeded the number of cuts
|
||||
if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
|
||||
break;
|
||||
}
|
||||
// quit if we exceeded the number of cuts
|
||||
if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
|
||||
break;
|
||||
}
|
||||
}
|
||||
assert( p->nCuts > 0 );
|
||||
// sort if we have more cuts
|
||||
If_ManSortCuts( p, Mode );
|
||||
|
|
|
|||
|
|
@ -96,7 +96,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
|
|||
// print the statistic into a file
|
||||
{
|
||||
FILE * pTable;
|
||||
pTable = fopen( "a/seqmap__stats.txt", "a+" );
|
||||
pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
|
||||
fprintf( pTable, "%d ", p->Period );
|
||||
fprintf( pTable, "\n" );
|
||||
fclose( pTable );
|
||||
|
|
@ -198,7 +198,7 @@ int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
|
|||
// report the results
|
||||
if ( p->pPars->fVerbose )
|
||||
{
|
||||
p->AreaGlo = p->pPars->fLiftLeaves? If_ManScanMappingSeq(p) : If_ManScanMapping(p);
|
||||
p->AreaGlo = p->pPars->fLiftLeaves? 0/*If_ManScanMappingSeq(p)*/ : If_ManScanMapping(p);
|
||||
printf( "Attempt = %2d. Iters = %3d. Area = %10.2f. Fi = %6.2f. ", p->nAttempts, c, p->AreaGlo, (float)p->Period );
|
||||
if ( fConverged )
|
||||
printf( " Feasible" );
|
||||
|
|
@ -358,7 +358,9 @@ int If_ManPrepareMappingSeq( If_Man_t * p )
|
|||
pCut->Delay -= p->Period;
|
||||
pCut->fCompl ^= pObj->fCompl0;
|
||||
|
||||
pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
|
||||
// there is a bug here, which shows when there are choices...
|
||||
// pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
|
||||
pTemp = If_ManObj(p, pCut->pLeaves[0]);
|
||||
assert( !If_ObjIsLatch(pTemp) );
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -186,7 +186,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
|
|||
If_Obj_t * pLeaf;
|
||||
int i, j, best_i, temp;
|
||||
// start the trivial permutation and collect pin delays
|
||||
If_CutForEachLeaf( p, pCut, pLeaf, i );
|
||||
If_CutForEachLeaf( p, pCut, pLeaf, i )
|
||||
{
|
||||
pPinPerm[i] = i;
|
||||
pPinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
|
||||
|
|
@ -206,8 +206,12 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
|
|||
pPinPerm[best_i] = temp;
|
||||
}
|
||||
// verify
|
||||
assert( pPinPerm[0] < pCut->nLeaves );
|
||||
for ( i = 1; i < (int)pCut->nLeaves; i++ )
|
||||
{
|
||||
assert( pPinPerm[i] < (int)pCut->nLeaves );
|
||||
assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
|
||||
}
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -269,7 +269,11 @@ float If_ManScanMappingSeq_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vMapp
|
|||
If_Cut_t * pCutBest;
|
||||
float aArea;
|
||||
int i, Shift;
|
||||
if ( pObj->nRefs++ || If_ObjIsCi(pObj) || If_ObjIsConst1(pObj) )
|
||||
// treat latches transparently
|
||||
if ( If_ObjIsLatch(pObj) )
|
||||
return If_ManScanMappingSeq_rec( p, If_ObjFanin0(pObj), vMapped );
|
||||
// consider trivial cases
|
||||
if ( pObj->nRefs++ || If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) )
|
||||
return 0.0;
|
||||
// store the node in the structure by level
|
||||
assert( If_ObjIsAnd(pObj) );
|
||||
|
|
|
|||
|
|
@ -388,10 +388,11 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
|
|||
int i;
|
||||
if ( p->nSize >= nSize )
|
||||
return;
|
||||
if ( p->nSize < 2 * nSize )
|
||||
assert( p->nSize < nSize );
|
||||
if ( 2 * p->nSize > nSize )
|
||||
Vec_PtrGrow( p, 2 * nSize );
|
||||
else
|
||||
Vec_PtrGrow( p, p->nSize );
|
||||
Vec_PtrGrow( p, nSize );
|
||||
for ( i = p->nSize; i < nSize; i++ )
|
||||
p->pArray[i] = Entry;
|
||||
p->nSize = nSize;
|
||||
|
|
|
|||
|
|
@ -127,6 +127,14 @@ clkIter = clock() - clk;
|
|||
NodeLag = Abc_NodeComputeLag( Abc_NodeGetLValue(pNode), FiBest );
|
||||
Vec_IntWriteEntry( vLags, pNode->Id, NodeLag );
|
||||
}
|
||||
/*
|
||||
Abc_NtkForEachPo( pNtk, pNode, i )
|
||||
printf( "%d ", Abc_NodeGetLValue(Abc_ObjFanin0(pNode)) );
|
||||
printf( "\n" );
|
||||
Abc_NtkForEachLatch( pNtk, pNode, i )
|
||||
printf( "%d/%d ", Abc_NodeGetLValue(Abc_ObjFanout0(pNode)), Abc_NodeGetLValue(Abc_ObjFanout0(pNode)) + FiBest );
|
||||
printf( "\n" );
|
||||
*/
|
||||
|
||||
// print the result
|
||||
// if ( fVerbose )
|
||||
|
|
@ -134,7 +142,7 @@ clkIter = clock() - clk;
|
|||
/*
|
||||
{
|
||||
FILE * pTable;
|
||||
pTable = fopen( "a/seqmap__stats.txt", "a+" );
|
||||
pTable = fopen( "iscas/seqmap__stats2.txt", "a+" );
|
||||
fprintf( pTable, "%d ", FiBest );
|
||||
fprintf( pTable, "\n" );
|
||||
fclose( pTable );
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@
|
|||
static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
|
||||
static int Rwr_CutIsBoolean( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
|
||||
static int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut );
|
||||
static int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
|
|
@ -186,6 +187,13 @@ p->timeRes += clock() - clk;
|
|||
// copy the leaves
|
||||
Vec_PtrForEachEntry( p->vFanins, pFanin, i )
|
||||
Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
|
||||
/*
|
||||
printf( "(" );
|
||||
Vec_PtrForEachEntry( p->vFanins, pFanin, i )
|
||||
printf( " %d", Abc_ObjRegular(pFanin)->vFanouts.nSize - 1 );
|
||||
printf( " ) " );
|
||||
*/
|
||||
// printf( "%d ", Rwr_NodeGetDepth_rec( pNode, p->vFanins ) );
|
||||
|
||||
p->nScores[p->pMap[uTruthBest]]++;
|
||||
p->nNodesGained += GainBest;
|
||||
|
|
@ -384,6 +392,32 @@ int Rwr_CutCountNumNodes( Abc_Obj_t * pObj, Cut_Cut_t * pCut )
|
|||
return Counter;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns depth of the cut.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves )
|
||||
{
|
||||
Abc_Obj_t * pLeaf;
|
||||
int i, Depth0, Depth1;
|
||||
if ( Abc_ObjIsCi(pObj) )
|
||||
return 0;
|
||||
Vec_PtrForEachEntry( vLeaves, pLeaf, i )
|
||||
if ( pObj == Abc_ObjRegular(pLeaf) )
|
||||
return 0;
|
||||
Depth0 = Rwr_NodeGetDepth_rec( Abc_ObjFanin0(pObj), vLeaves );
|
||||
Depth1 = Rwr_NodeGetDepth_rec( Abc_ObjFanin1(pObj), vLeaves );
|
||||
return 1 + ABC_MAX( Depth0, Depth1 );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
Loading…
Reference in New Issue