Skip to content

A
abc
Commit d4fecf91 by Alan Mishchenko
Options

Version abc80121

parent 61850d59
Showing with 687 additions and 377 deletions
src/aig/fra/fraSec.c
......@@ -276,7 +276,7 @@ PRT( "Time", clock() - clkTotal );
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
sprintf( pFileName, "sm%03d.aig", Counter++ );
Ioa_WriteAiger( pNew, pFileName, 0 );
Ioa_WriteAiger( pNew, pFileName, 0, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}
Aig_ManStop( pNew );
......
src/aig/ioa/ioa.h
......@@ -36,7 +36,7 @@ extern "C" {
#include <time.h>
#include "vec.h"
#include "bar.h"
//#include "bar.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
......@@ -62,7 +62,7 @@ extern "C" {
/*=== ioaReadAig.c ========================================================*/
extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck );
/*=== ioaWriteAig.c =======================================================*/
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols );
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
/*=== ioaUtil.c =======================================================*/
extern int Ioa_FileSize( char * pFileName );
extern char * Ioa_FileNameGeneric( char * FileName );
......
src/aig/ioa/ioaReadAig.c
......@@ -25,14 +25,69 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
unsigned Ioa_ReadAigerDecode( char ** ppPos );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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 Ioa_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));
}
/**Function*************************************************************
Synopsis [Decodes the encoded array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
{
Vec_Int_t * vLits;
int Lit, LitPrev, Diff, i;
vLits = Vec_IntAlloc( nEntries );
LitPrev = Ioa_ReadAigerDecode( ppPos );
Vec_IntPush( vLits, LitPrev );
for ( i = 1; i < nEntries; i++ )
{
// Diff = Lit - LitPrev;
// Diff = (Lit < LitPrev)? -Diff : Diff;
// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
Diff = Ioa_ReadAigerDecode( ppPos );
Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
Lit = Diff + LitPrev;
Vec_IntPush( vLits, Lit );
LitPrev = Lit;
}
return vLits;
}
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Description []
......@@ -44,8 +99,9 @@ unsigned Ioa_ReadAigerDecode( char ** ppPos );
***********************************************************************/
Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
{
Bar_Progress_t * pProgress;
// Bar_Progress_t * pProgress;
FILE * pFile;
Vec_Int_t * vLits = NULL;
Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
Aig_Obj_t * pObj, * pNode0, * pNode1;
Aig_Man_t * pManNew;
......@@ -61,7 +117,7 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
fclose( pFile );
// check if the input file format is correct
if ( strncmp(pContents, "aig", 3) != 0 )
if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
{
fprintf( stdout, "Wrong input file format.\n" );
return NULL;
......@@ -127,21 +183,27 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
// Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
// printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
}
*/
*/
// 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++;
if ( pContents[3] == ' ' ) // standard AIGER
{
// scroll to the beginning of the binary data
for ( i = 0; i < nLatches + nOutputs; )
if ( *pCur++ == '\n' )
i++;
}
else // modified AIGER
{
vLits = Ioa_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
}
// create the AND gates
pProgress = Bar_ProgressStart( stdout, nAnds );
// pProgress = Bar_ProgressStart( stdout, nAnds );
for ( i = 0; i < nAnds; i++ )
{
Bar_ProgressUpdate( pProgress, i, NULL );
// Bar_ProgressUpdate( pProgress, i, NULL );
uLit = ((i + 1 + nInputs + nLatches) << 1);
uLit1 = uLit - Ioa_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
......@@ -151,33 +213,50 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
}
Bar_ProgressStop( pProgress );
// Bar_ProgressStop( pProgress );
// remember the place where symbols begin
pSymbols = pCur;
// read the latch driver literals
vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
pCur = pDrivers;
// Aig_ManForEachLatchInput( pManNew, pObj, i )
for ( i = 0; i < nLatches; i++ )
if ( pContents[3] == ' ' ) // standard AIGER
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
// Aig_ObjAddFanin( pObj, pNode0 );
Vec_PtrPush( vDrivers, pNode0 );
pCur = pDrivers;
for ( i = 0; i < nLatches; i++ )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Vec_PtrPush( vDrivers, pNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Vec_PtrPush( vDrivers, pNode0 );
}
}
// read the PO driver literals
// Aig_ManForEachPo( pManNew, pObj, i )
for ( i = 0; i < nOutputs; i++ )
else
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
// Aig_ObjAddFanin( pObj, pNode0 );
Vec_PtrPush( vDrivers, pNode0 );
// read the latch driver literals
for ( i = 0; i < nLatches; i++ )
{
uLit0 = Vec_IntEntry( vLits, i );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Vec_PtrPush( vDrivers, pNode0 );
}
// read the PO driver literals
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = Vec_IntEntry( vLits, i+nLatches );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Vec_PtrPush( vDrivers, pNode0 );
}
Vec_IntFree( vLits );
}
// create the POs
for ( i = 0; i < nOutputs; i++ )
Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
......@@ -280,31 +359,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
}
/**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 Ioa_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 ///
////////////////////////////////////////////////////////////////////////
......
src/aig/ioa/ioaWriteAig.c
......@@ -125,11 +125,9 @@ Binary Format Definition
*/
static unsigned Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return (unsigned)pObj->pData; }
static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->pData = (void *)Num; }
int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
static int Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
static int Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return pObj->iData; }
static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->iData = Num; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -137,6 +135,111 @@ int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
/**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 Ioa_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;
}
/**Function*************************************************************
Synopsis [Create the array of literals to be written.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ioa_WriteAigerLiterals( Aig_Man_t * pMan )
{
Vec_Int_t * vLits;
Aig_Obj_t * pObj, * pDriver;
int i;
vLits = Vec_IntAlloc( Aig_ManPoNum(pMan) );
Aig_ManForEachLiSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
Aig_ManForEachPoSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
Vec_IntPush( vLits, Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
return vLits;
}
/**Function*************************************************************
Synopsis [Creates the binary encoded array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
{
Vec_Str_t * vBinary;
int Pos = 0, Lit, LitPrev, Diff, i;
vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
LitPrev = Vec_IntEntry( vLits, 0 );
Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev );
Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
{
Diff = Lit - LitPrev;
Diff = (Lit < LitPrev)? -Diff : Diff;
Diff = (Diff << 1) | (int)(Lit < LitPrev);
Pos = Ioa_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff );
LitPrev = Lit;
if ( Pos + 10 > vBinary->nCap )
Vec_StrGrow( vBinary, vBinary->nCap+1 );
}
vBinary->nSize = Pos;
/*
// verify
{
extern Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries );
char * pPos = Vec_StrArray( vBinary );
Vec_Int_t * vTemp = Ioa_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
for ( i = 0; i < Vec_IntSize(vLits); i++ )
{
int Entry1 = Vec_IntEntry(vLits,i);
int Entry2 = Vec_IntEntry(vTemp,i);
assert( Entry1 == Entry2 );
}
Vec_IntFree( vTemp );
}
*/
return vBinary;
}
/**Function*************************************************************
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
......@@ -146,9 +249,9 @@ int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
SeeAlso []
***********************************************************************/
void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact )
{
Bar_Progress_t * pProgress;
// Bar_Progress_t * pProgress;
FILE * pFile;
Aig_Obj_t * pObj, * pDriver;
int i, nNodes, Pos, nBufferSize;
......@@ -180,7 +283,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
Ioa_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",
fprintf( pFile, "aig%s %u %u %u %u %u\n",
fCompact? "2" : "",
Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan),
Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManRegNum(pMan),
......@@ -191,34 +295,45 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
// 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
Aig_ManForEachLiSeq( pMan, pObj, i )
if ( !fCompact )
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
// write latch drivers
Aig_ManForEachLiSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
// write PO drivers
Aig_ManForEachPoSeq( pMan, pObj, i )
// write PO drivers
Aig_ManForEachPoSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
}
else
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
Vec_Int_t * vLits = Ioa_WriteAigerLiterals( pMan );
Vec_Str_t * vBinary = Ioa_WriteEncodeLiterals( vLits );
fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
// write the nodes into the buffer
Pos = 0;
nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
pBuffer = ALLOC( char, nBufferSize );
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
pBuffer = ALLOC( unsigned char, nBufferSize );
// pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
Aig_ManForEachNode( pMan, pObj, i )
{
Bar_ProgressUpdate( pProgress, i, NULL );
// Bar_ProgressUpdate( pProgress, i, NULL );
uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
assert( uLit0 < uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
if ( Pos > nBufferSize - 10 )
{
printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
......@@ -227,7 +342,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
}
}
assert( Pos < nBufferSize );
Bar_ProgressStop( pProgress );
// Bar_ProgressStop( pProgress );
// write the buffer
fwrite( pBuffer, 1, Pos, pFile );
......@@ -251,40 +366,11 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
fprintf( pFile, "c\n" );
if ( pMan->pName )
fprintf( pFile, ".model %s\n", pMan->pName );
fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "This file was produced by the AIG package on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "For information about AIGER 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 Ioa_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 ///
////////////////////////////////////////////////////////////////////////
......
src/aig/tim/tim.c
......@@ -45,7 +45,7 @@ struct Tim_Man_t_
{
Vec_Ptr_t * vBoxes; // the timing boxes
Vec_Ptr_t * vDelayTables; // pointers to the delay tables
Mem_Flex_t * pMemObj; // memory manager for boxes
Mem_Flex_t * pMemObj; // memory manager for boxes
int nTravIds; // traversal ID of the manager
int nPis; // the number of PIs
int nPos; // the number of POs
......@@ -74,13 +74,27 @@ struct Tim_Obj_t_
float timeReq; // required time of the object
};
static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i ) { assert( i < p->nPis ); return p->pPis + i; }
static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i ) { assert( i < p->nPos ); return p->pPos + i; }
static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i ) { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); }
static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i ) { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); }
static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i ) { return p->pPos + pBox->Inouts[i]; }
static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i ) { return p->pPis + pBox->Inouts[pBox->nInputs+i]; }
#define Tim_ManBoxForEachInput( p, pBox, pObj, i ) \
for ( i = 0; (i < (pBox)->nInputs) && ((pObj) = Tim_ManBoxInput(p, pBox, i)); i++ )
#define Tim_ManBoxForEachOutput( p, pBox, pObj, i ) \
for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the network manager.]
Synopsis [Starts the timing manager.]
Description []
......@@ -113,7 +127,7 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
/**Function*************************************************************
Synopsis [Stops the network manager.]
Synopsis [Stops the timing manager.]
Description []
......@@ -141,7 +155,7 @@ void Tim_ManStop( Tim_Man_t * p )
/**Function*************************************************************
Synopsis [Increments the trav ID of the manager.]
Synopsis [Sets the vector of timing tables associated with the manager.]
Description []
......@@ -252,7 +266,7 @@ void Tim_ManIncrementTravId( Tim_Man_t * p )
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Synopsis [Initializes arrival time of the PI.]
Description []
......@@ -269,7 +283,7 @@ void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Synopsis [Initializes required time of the PO.]
Description []
......@@ -286,7 +300,7 @@ void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
/**Function*************************************************************
Synopsis [Creates the new timing box.]
Synopsis [Updates arrival time of the PO.]
Description []
......@@ -305,7 +319,7 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
/**Function*************************************************************
Synopsis [Returns PI arrival time.]
Synopsis [Updates required time of the PI.]
Description []
......@@ -314,52 +328,18 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
SeeAlso []
***********************************************************************/
float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
{
Tim_Box_t * pBox;
Tim_Obj_t * pObj;
float * pDelays;
float DelayMax;
int i, k;
assert( iPi < p->nPis );
if ( p->pPis[iPi].iObj2Box < 0 )
return p->pPis[iPi].timeArr;
pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
// check if box timing is updated
if ( pBox->TravId == p->nTravIds )
{
assert( pBox->TravId == p->nTravIds );
return p->pPis[iPi].timeArr;
}
pBox->TravId = p->nTravIds;
// update box timing
// get the arrival times of the inputs of the box (POs)
for ( i = 0; i < pBox->nInputs; i++ )
{
pObj = p->pPos + pBox->Inouts[i];
if ( pObj->TravId != p->nTravIds )
printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
}
// compute the required times for each output of the box (PIs)
for ( i = 0; i < pBox->nOutputs; i++ )
{
pDelays = pBox->pDelayTable + i * pBox->nInputs;
DelayMax = -AIG_INFINITY;
for ( k = 0; k < pBox->nInputs; k++ )
{
pObj = p->pPos + pBox->Inouts[k];
DelayMax = AIG_MAX( DelayMax, pObj->timeArr + pDelays[k] );
}
pObj = p->pPis + pBox->Inouts[pBox->nInputs+i];
pObj->timeArr = DelayMax;
pObj->TravId = p->nTravIds;
}
return p->pPis[iPi].timeArr;
assert( p->pPis[iPi].TravId != p->nTravIds );
p->pPis[iPi].timeReq = Delay;
p->pPis[iPi].TravId = p->nTravIds;
}
/**Function*************************************************************
Synopsis [Returns PO required time.]
Synopsis [Returns PI arrival time.]
Description []
......@@ -368,12 +348,33 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
SeeAlso []
***********************************************************************/
void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
{
assert( iPi < p->nPis );
assert( p->pPis[iPi].TravId != p->nTravIds );
p->pPis[iPi].timeReq = Delay;
p->pPis[iPi].TravId = p->nTravIds;
Tim_Box_t * pBox;
Tim_Obj_t * pObj, * pObjRes;
float * pDelays, DelayBest;
int i, k;
// consider the main PI or the already processed PI
pBox = Tim_ManPiBox( p, iPi );
if ( pBox == NULL || pBox->TravId == p->nTravIds )
return Tim_ManPi(p, iPi)->timeArr;
// update box timing
pBox->TravId = p->nTravIds;
// get the arrival times of the inputs of the box (POs)
Tim_ManBoxForEachInput( p, pBox, pObj, i )
if ( pObj->TravId != p->nTravIds )
printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
// compute the required times for each output of the box (PIs)
Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
{
pDelays = pBox->pDelayTable + i * pBox->nInputs;
DelayBest = -AIG_INFINITY;
Tim_ManBoxForEachInput( p, pBox, pObj, k )
DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
pObjRes->timeArr = DelayBest;
pObjRes->TravId = p->nTravIds;
}
return Tim_ManPi(p, iPi)->timeArr;
}
/**Function*************************************************************
......@@ -389,7 +390,33 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
***********************************************************************/
float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
{
return 0.0;
Tim_Box_t * pBox;
Tim_Obj_t * pObj, * pObjRes;
float * pDelays, DelayBest;
int i, k;
// consider the main PO or the already processed PO
pBox = Tim_ManPoBox( p, iPo );
if ( pBox == NULL || pBox->TravId == p->nTravIds )
return Tim_ManPo(p, iPo)->timeReq;
// update box timing
pBox->TravId = p->nTravIds;
// get the arrival times of the inputs of the box (POs)
Tim_ManBoxForEachOutput( p, pBox, pObj, i )
if ( pObj->TravId != p->nTravIds )
printf( "Tim_ManGetPoRequired(): PI required times of the box are not up to date!\n" );
// compute the required times for each output of the box (PIs)
Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
{
DelayBest = AIG_INFINITY;
Tim_ManBoxForEachOutput( p, pBox, pObj, k )
{
pDelays = pBox->pDelayTable + k * pBox->nInputs;
DelayBest = AIG_MIN( DelayBest, pObj->timeReq + pDelays[i] );
}
pObjRes->timeReq = DelayBest;
pObjRes->TravId = p->nTravIds;
}
return Tim_ManPo(p, iPo)->timeReq;
}
......
src/base/abci/abc.c
......@@ -6384,7 +6384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern void Abc_NtkDarTestBlif( char * pFileName );
......@@ -6543,6 +6543,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for logic circuits.\n" );
return 0;
}
*/
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
......@@ -6555,7 +6556,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
// Abc_NtkDarHaigRecord( pNtk );
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
......@@ -10363,8 +10364,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// disable cut-expansion if edge-based heuristics are selected
if ( pPars->fEdge )
pPars->fExpRed = 0;
// if ( pPars->fEdge )
// pPars->fExpRed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
......
src/base/io/io.c
......@@ -1174,17 +1174,22 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
int fWriteSymbols;
int fCompact;
int c;
fWriteSymbols = 1;
fCompact = 1;
fWriteSymbols = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF )
{
switch ( c )
{
case 's':
fWriteSymbols ^= 1;
break;
case 'c':
fCompact ^= 1;
break;
case 'h':
goto usage;
default:
......@@ -1196,23 +1201,19 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
// get the output file name
pFileName = argv[globalUtilOptind];
// call the corresponding file writer
if ( fWriteSymbols )
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER );
else
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
return 1;
}
Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 );
fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
return 1;
}
Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" );
fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
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;
......
src/base/io/io.h
......@@ -87,7 +87,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcWriteAiger.c =========================================================*/
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols );
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
/*=== abcWriteBaf.c ===========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
......
src/base/io/ioReadAiger.c
......@@ -25,14 +25,68 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
unsigned Io_ReadAigerDecode( char ** ppPos );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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));
}
/**Function*************************************************************
Synopsis [Decodes the encoded array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries )
{
Vec_Int_t * vLits;
int Lit, LitPrev, Diff, i;
vLits = Vec_IntAlloc( nEntries );
LitPrev = Io_ReadAigerDecode( ppPos );
Vec_IntPush( vLits, LitPrev );
for ( i = 1; i < nEntries; i++ )
{
// Diff = Lit - LitPrev;
// Diff = (Lit < LitPrev)? -Diff : Diff;
// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev);
Diff = Io_ReadAigerDecode( ppPos );
Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1;
Lit = Diff + LitPrev;
Vec_IntPush( vLits, Lit );
LitPrev = Lit;
}
return vLits;
}
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Description []
......@@ -47,6 +101,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
ProgressBar * pProgress;
FILE * pFile;
Vec_Ptr_t * vNodes, * vTerms;
Vec_Int_t * vLits = NULL;
Abc_Obj_t * pObj, * pNode0, * pNode1;
Abc_Ntk_t * pNtkNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
......@@ -61,7 +116,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
fclose( pFile );
// check if the input file format is correct
if ( strncmp(pContents, "aig", 3) != 0 )
if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
{
fprintf( stdout, "Wrong input file format.\n" );
return NULL;
......@@ -125,13 +180,20 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
}
// 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++;
if ( pContents[3] == ' ' ) // standard AIGER
{
// 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++;
}
else // modified AIGER
{
vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
}
// create the AND gates
pProgress = Extra_ProgressBarStart( stdout, nAnds );
......@@ -154,21 +216,39 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// read the latch driver literals
pCur = pDrivers;
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
if ( pContents[3] == ' ' ) // standard AIGER
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
// printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
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 PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
else
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
// read the latch driver literals
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = Vec_IntEntry( vLits, i );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Abc_ObjAddFanin( pObj, pNode0 );
}
// read the PO driver literals
Abc_NtkForEachPo( pNtkNew, pObj, i )
{
uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) );
pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
Abc_ObjAddFanin( pObj, pNode0 );
}
Vec_IntFree( vLits );
}
// read the names if present
......@@ -278,30 +358,6 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
}
/**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 ///
......
src/base/io/ioUtil.c
......@@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
return;
}
if ( FileType == IO_FILE_AIGER )
Io_WriteAiger( pNtk, pFileName, 1 );
Io_WriteAiger( pNtk, pFileName, 1, 0 );
else // if ( FileType == IO_FILE_BAF )
Io_WriteBaf( pNtk, pFileName );
return;
......
src/base/io/ioWriteAiger.c
......@@ -129,14 +129,116 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (V
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; }
int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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;
}
/**Function*************************************************************
Synopsis [Create the array of literals to be written.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vLits;
Abc_Obj_t * pObj, * pDriver;
int i;
vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
Abc_NtkForEachLatchInput( pNtk, pObj, i )
{
pDriver = Abc_ObjFanin0(pObj);
Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
}
Abc_NtkForEachPo( pNtk, pObj, i )
{
pDriver = Abc_ObjFanin0(pObj);
Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
}
return vLits;
}
/**Function*************************************************************
Synopsis [Creates the binary encoded array of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
{
Vec_Str_t * vBinary;
int Pos = 0, Lit, LitPrev, Diff, i;
vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
LitPrev = Vec_IntEntry( vLits, 0 );
Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev );
Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
{
Diff = Lit - LitPrev;
Diff = (Lit < LitPrev)? -Diff : Diff;
Diff = (Diff << 1) | (int)(Lit < LitPrev);
Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff );
LitPrev = Lit;
if ( Pos + 10 > vBinary->nCap )
Vec_StrGrow( vBinary, vBinary->nCap+1 );
}
vBinary->nSize = Pos;
/*
// verify
{
extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries );
char * pPos = Vec_StrArray( vBinary );
Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) );
for ( i = 0; i < Vec_IntSize(vLits); i++ )
{
int Entry1 = Vec_IntEntry(vLits,i);
int Entry2 = Vec_IntEntry(vTemp,i);
assert( Entry1 == Entry2 );
}
}
*/
return vBinary;
}
/**Function*************************************************************
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
......@@ -146,7 +248,7 @@ int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
SeeAlso []
***********************************************************************/
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
{
ProgressBar * pProgress;
FILE * pFile;
......@@ -179,7 +281,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
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",
fprintf( pFile, "aig%s %u %u %u %u %u\n",
fCompact? "2" : "",
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
Abc_NtkPiNum(pNtk),
Abc_NtkLatchNum(pNtk),
......@@ -190,24 +293,34 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
// 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 )
if ( !fCompact )
{
pDriver = Abc_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 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 PO drivers
Abc_NtkForEachPo( pNtk, pObj, i )
else
{
pDriver = Abc_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk );
Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits );
fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile );
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
// 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 );
pBuffer = ALLOC( unsigned char, nBufferSize );
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_AigForEachAnd( pNtk, pObj, i )
{
......@@ -216,8 +329,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
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 );
Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) );
Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) );
if ( Pos > nBufferSize - 10 )
{
printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
......@@ -255,35 +368,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
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 ///
////////////////////////////////////////////////////////////////////////
......
src/map/if/if.h
......@@ -326,8 +326,13 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r
extern int If_ManPerformMapping( If_Man_t * p );
extern int If_ManPerformMappingComb( If_Man_t * p );
/*=== ifCut.c ============================================================*/
extern int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
extern void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
extern void If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
extern void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
extern void If_CutLift( If_Cut_t * pCut );
extern void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
extern float If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
......@@ -339,12 +344,6 @@ extern float If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
extern void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
extern void If_CutLift( If_Cut_t * pCut );
extern void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc );
extern void If_ManSortCuts( If_Man_t * p, int Mode );
/*=== ifMan.c =============================================================*/
extern If_Man_t * If_ManStart( If_Par_t * pPars );
extern void If_ManRestart( If_Man_t * p );
......
src/map/if/ifMan.c
......@@ -68,8 +68,8 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
// p->pMemSet = Mem_FixedStart( p->nSetBytes );
// report expected memory usage
if ( p->pPars->fVerbose )
printf( "Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n",
4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
printf( "K = %d. Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d.\n",
p->pPars->nLutSize, 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes );
// room for temporary truth tables
p->puTemp[0] = p->pPars->fTruth? ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
......
src/map/if/ifReduce.c
......@@ -150,6 +150,7 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
int CostBef, CostAft, i;
float DelayOld, AreaBef, AreaAft;
pCut = If_ObjCutBest(pObj);
pCut->Delay = If_CutDelay( p, pCut );
assert( pCut->Delay <= pObj->Required + p->fEpsilon );
if ( pObj->nRefs == 0 )
return;
......@@ -449,8 +450,8 @@ int If_ManImproveNodeFaninCompact_int( If_Man_t * p, If_Obj_t * pObj, int nLimit
return 1;
if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact1(p, pObj, nLimit, vFront, vVisited) )
return 1;
if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
return 1;
// if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) )
// return 1;
assert( Vec_PtrSize(vFront) <= nLimit );
return 0;
}
......
src/map/if/ifUtil.c
......@@ -212,7 +212,7 @@ void If_ManComputeRequired( If_Man_t * p )
Vec_PtrForEachEntry( p->vMapped, pObj, i )
If_CutPropagateRequired( p, If_ObjCutBest(pObj), pObj->Required );
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
......
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