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

Changes to read multi-output testcases described using AIGER 1.9.

This commit is contained in:
Alan Mishchenko 2011-11-06 23:15:27 -08:00
parent c345a60ee7
commit d2ced9f82e
12 changed files with 431 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/aig/aig.h
View File

@ -689,6 +689,7 @@ extern void Aig_ManSetPhase( Aig_Man_t * pAig );
extern Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig );
extern void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
extern void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
extern void Aig_ManInvertConstraints( Aig_Man_t * pAig );
/*=== aigWin.c =========================================================*/
extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );

23
src/aig/aig/aigUtil.c
View File

@ -1565,6 +1565,29 @@ void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
}
}
/**Function*************************************************************
Synopsis [Complements the constraint outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManInvertConstraints( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj;
int i;
if ( Aig_ManConstrNum(pAig) == 0 )
return;
Saig_ManForEachPo( pAig, pObj, i )
{
if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
Aig_ObjChild0Flip( pObj );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

2
src/aig/gia/gia.h
View File

@ -819,6 +819,8 @@ extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;
extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );

158
src/aig/gia/giaAiger.c
View File

@ -350,6 +350,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
int iObj, iNode0, iNode1;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
char * pContents, * pName;
unsigned uLit0, uLit1, uLit;
@ -370,25 +371,76 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
return NULL;
}
// read the file type
pCur = (unsigned char *)pContents; while ( *pCur++ != ' ' );
// read the parameters (M I L O A + B C J F)
pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
nTotal = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
nInputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
nLatches = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
nOutputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
nAnds = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
if ( *pCur == ' ' )
{
assert( nOutputs == 0 );
// read the number of properties
pCur++;
nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nBad;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nConstr;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nJust;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nFair;
}
if ( *pCur != '\n' )
{
fprintf( stdout, "The parameter line is in a wrong format.\n" );
ABC_FREE( pContents );
return NULL;
}
pCur++;
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
fprintf( stdout, "The number of objects does not match.\n" );
ABC_FREE( pContents );
fprintf( stdout, "The paramters are wrong.\n" );
return NULL;
}
if ( nJust || nFair )
{
fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
ABC_FREE( pContents );
return NULL;
}
if ( nConstr )
{
if ( nConstr == 1 )
fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
else
fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
}
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
@ -396,6 +448,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Gia_UtilStrsav( pFileName );
ABC_FREE( pName );
pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_IntAlloc( 1 + nTotal );
@ -548,6 +601,10 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
}
Vec_IntFree( vNodes );
// update polarity of the additional outputs
if ( nBad || nConstr || nJust || nFair )
Gia_ManInvertConstraints( pNew );
// skipping the comments
/*
// check the result
@ -580,31 +637,81 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
int iObj, iNode0, iNode1;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
unsigned uLit0, uLit1, uLit;
// read the file type
pCur = (unsigned char *)pContents; while ( *pCur++ != ' ' );
// read the parameters (M I L O A + B C J F)
pCur = (unsigned char *)pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
nTotal = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
nInputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
nLatches = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
nOutputs = atoi( (char *)pCur ); while ( *pCur++ != ' ' );
nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
nAnds = atoi( (char *)pCur ); while ( *pCur++ != '\n' );
nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
if ( *pCur == ' ' )
{
assert( nOutputs == 0 );
// read the number of properties
pCur++;
nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nBad;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nConstr;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nJust;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nFair;
}
if ( *pCur != '\n' )
{
fprintf( stdout, "The parameter line is in a wrong format.\n" );
return NULL;
}
pCur++;
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
ABC_FREE( pContents );
fprintf( stdout, "The paramters are wrong.\n" );
fprintf( stdout, "The number of objects does not match.\n" );
return NULL;
}
if ( nJust || nFair )
{
fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
return NULL;
}
if ( nConstr )
{
if ( nConstr == 1 )
fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
else
fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
}
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_IntAlloc( 1 + nTotal );
@ -903,6 +1010,11 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
return NULL;
}
*/
// update polarity of the additional outputs
if ( nBad || nConstr || nJust || nFair )
Gia_ManInvertConstraints( pNew );
// clean the PO drivers
if ( vPoTypes )
{
@ -1243,14 +1355,19 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
p = pInit;
// write the header "M I L O A" where M = I + L + A
fprintf( pFile, "aig%s %u %u %u %u %u\n",
fprintf( pFile, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Gia_ManCiNum(p) + Gia_ManAndNum(p),
Gia_ManPiNum(p),
Gia_ManRegNum(p),
Gia_ManPoNum(p),
Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
Gia_ManAndNum(p) );
// write the extended header "B C J F"
if ( Gia_ManConstrNum(p) )
fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
fprintf( pFile, "\n" );
Gia_ManInvertConstraints( p );
if ( !fCompact )
{
// write latch drivers
@ -1268,6 +1385,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
Gia_ManInvertConstraints( p );
// write the nodes into the buffer
Pos = 0;
@ -1372,6 +1490,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
fwrite( Buffer, 1, 4, pFile );
fwrite( p->pSwitching, 1, nSize, pFile );
}
/*
// write constraints
if ( p->nConstrs )
{
@ -1380,6 +1499,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
fprintf( pFile, "c" );
fwrite( Buffer, 1, 4, pFile );
}
*/
// write name
if ( p->pName )
fprintf( pFile, "n%s%c", p->pName, '\0' );

24
src/aig/gia/giaUtil.c
View File

@ -1224,6 +1224,30 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
return RetValue;
}
/**Function*************************************************************
Synopsis [Complements the constraint outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManInvertConstraints( Gia_Man_t * pAig )
{
Gia_Obj_t * pObj;
int i;
if ( Gia_ManConstrNum(pAig) == 0 )
return;
Gia_ManForEachPo( pAig, pObj, i )
{
if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
Gia_ObjFlipFaninC0( pObj );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

71
src/aig/ioa/ioaReadAig.c
View File

@ -109,6 +109,7 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Aig_Obj_t * pObj, * pNode0, * pNode1;
Aig_Man_t * pNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
char * pDrivers, * pSymbols, * pCur;//, * pType;
unsigned uLit0, uLit1, uLit;
@ -119,27 +120,77 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
return NULL;
}
// read the file type
pCur = pContents; while ( *pCur++ != ' ' );
// read the parameters (M I L O A + B C J F)
pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
if ( *pCur == ' ' )
{
assert( nOutputs == 0 );
// read the number of properties
pCur++;
nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nBad;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nConstr;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nJust;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nFair;
}
if ( *pCur != '\n' )
{
fprintf( stdout, "The parameter line is in a wrong format.\n" );
return NULL;
}
pCur++;
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
fprintf( stdout, "The paramters are wrong.\n" );
fprintf( stdout, "The number of objects does not match.\n" );
return NULL;
}
if ( nJust || nFair )
{
fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
return NULL;
}
if ( nConstr )
{
if ( nConstr == 1 )
fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
else
fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
}
// allocate the empty AIG
pNew = Aig_ManStart( nAnds );
pNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@ -352,6 +403,10 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
Aig_ManCleanup( pNew );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
// update polarity of the additional outputs
if ( nBad || nConstr || nJust || nFair )
Aig_ManInvertConstraints( pNew );
// check the result
if ( fCheck && !Aig_ManCheck( pNew ) )
{

10
src/aig/ioa/ioaWriteAig.c
View File

@ -466,18 +466,23 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
Ioa_ObjSetAigerNum( pObj, nNodes++ );
// write the header "M I L O A" where M = I + L + A
fprintf( pFile, "aig%s %u %u %u %u %u\n",
fprintf( pFile, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan),
Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManRegNum(pMan),
Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManConstrNum(pMan) ? 0 : Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManNodeNum(pMan) );
// write the extended header "B C J F"
if ( Aig_ManConstrNum(pMan) )
fprintf( pFile, " %u %u", Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
fprintf( pFile, "\n" );
// 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
Aig_ManInvertConstraints( pMan );
if ( !fCompact )
{
// write latch drivers
@ -502,6 +507,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
Aig_ManInvertConstraints( pMan );
// write the nodes into the buffer
Pos = 0;

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

@ -938,6 +938,8 @@ extern ABC_DLL Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
extern ABC_DLL void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkInvertConstraints( Abc_Ntk_t * pNtk );
/*=== abcVerify.c ==========================================================*/
extern ABC_DLL int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );

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

@ -1909,6 +1909,30 @@ void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk )
}
}
/**Function*************************************************************
Synopsis [Complements the constraint outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkInvertConstraints( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
if ( Abc_NtkConstrNum(pNtk) == 0 )
return;
Abc_NtkForEachPo( pNtk, pObj, i )
{
if ( i >= Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
Abc_ObjXorFaninC( pObj, 0 );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -20033,6 +20033,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFrames;
int nConfs;
int nProps;
int fRemove;
int fStruct;
int fInvert;
int fOldAlgo;
@ -20045,13 +20046,14 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
nFrames = 1;
nConfs = 1000;
nProps = 1000;
fRemove = 0;
fStruct = 0;
fInvert = 0;
fOldAlgo = 0;
fVerbose = 0;
nConstrs = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNsiavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF )
{
switch ( c )
{
@ -20099,6 +20101,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConstrs < 0 )
goto usage;
break;
case 'r':
fRemove ^= 1;
break;
case 's':
fStruct ^= 1;
break;
@ -20132,21 +20137,26 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
if ( fRemove )
{
if ( Abc_NtkConstrNum(pNtk) == 0 )
{
Abc_Print( -1, "Constraints are not defined.\n" );
return 0;
}
Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );
pNtk->nConstrs = 0;
return 0;
}
// consider the case of already defined constraints
if ( Abc_NtkConstrNum(pNtk) > 0 )
{
extern void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose );
if ( fInvert )
{
Abc_Obj_t * pObj;
int i;
Abc_NtkForEachPo( pNtk, pObj, i )
{
if ( i >= Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
Abc_ObjXorFaninC( pObj, 0 );
}
Abc_NtkInvertConstraints( pNtk );
if ( Abc_NtkConstrNum(pNtk) == 1 )
Abc_Print( 1, "The outputs of %d constraint is complemented.\n", Abc_NtkConstrNum(pNtk) );
Abc_Print( 1, "The output of %d constraint is complemented.\n", Abc_NtkConstrNum(pNtk) );
else
Abc_Print( 1, "The outputs of %d constraints are complemented.\n", Abc_NtkConstrNum(pNtk) );
}
@ -20175,7 +20185,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: constr [-FCPN num] [-isavh]\n" );
Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" );
Abc_Print( -2, "\t a toolkit for constraint manipulation\n" );
Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" );
Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" );
@ -20183,6 +20193,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
Abc_Print( -2, "\t-N num : manually set the last <num> POs to be constraints [default = %d]\n", nConstrs );
Abc_Print( -2, "\t-r : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" );
Abc_Print( -2, "\t-a : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" );

124
src/base/io/ioReadAiger.c
View File

@ -233,7 +233,9 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
Vec_Int_t * vLits = NULL;
Abc_Obj_t * pObj, * pNode0, * pNode1;
Abc_Ntk_t * pNtkNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize = -1, iTerm, nDigits, i;
int nTotal, nInputs, nOutputs, nLatches, nAnds;
int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
int nFileSize = -1, iTerm, nDigits, i;
char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
unsigned uLit0, uLit1, uLit;
@ -257,36 +259,88 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
{
fprintf( stdout, "Wrong input file format.\n" );
free( pContents );
ABC_FREE( pContents );
return NULL;
}
// read the parameters (M I L O A + B C J F)
pCur = pContents; while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of objects
nTotal = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of inputs
nInputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of latches
nLatches = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of outputs
nOutputs = atoi( pCur ); while ( *pCur != ' ' ) pCur++; pCur++;
// read the number of nodes
nAnds = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
if ( *pCur == ' ' )
{
assert( nOutputs == 0 );
// read the number of properties
pCur++;
nBad = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nBad;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nConstr = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nConstr;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nJust = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nJust;
}
if ( *pCur == ' ' )
{
// read the number of properties
pCur++;
nFair = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
nOutputs += nFair;
}
if ( *pCur != '\n' )
{
fprintf( stdout, "The parameter line is in a wrong format.\n" );
ABC_FREE( pContents );
return NULL;
}
pCur++;
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
fprintf( stdout, "The number of objects does not match.\n" );
ABC_FREE( pContents );
return NULL;
}
if ( nJust || nFair )
{
fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
ABC_FREE( pContents );
return NULL;
}
if ( nConstr )
{
if ( nConstr == 1 )
fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
else
fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
}
// 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 );
ABC_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.\n" );
return NULL;
}
pNtkNew->nConstrs = nConstr;
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@ -359,7 +413,25 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
{
Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
uLit0 = atoi( pCur ); while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
if ( *pCur == ' ' ) // read initial value
{
pCur++;
if ( atoi( pCur ) == 1 )
Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
else if ( atoi( pCur ) == 0 )
Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
else
Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
}
if ( *pCur != '\n' )
{
fprintf( stdout, "The initial value of latch number %d is not recongnized.\n", i );
return NULL;
}
pCur++;
pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
Abc_ObjAddFanin( pObj, pNode0 );
}
@ -403,7 +475,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
vTerms = pNtkNew->vPis;
else if ( *pCur == 'l' )
vTerms = pNtkNew->vBoxes;
else if ( *pCur == 'o' )
else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
vTerms = pNtkNew->vPos;
else
{
@ -486,6 +558,10 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
// remove the extra nodes
Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
// update polarity of the additional outputs
if ( nBad || nConstr || nJust || nFair )
Abc_NtkInvertConstraints( pNtkNew );
// check the result
if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
{

31
src/base/io/ioWriteAiger.c
View File

@ -296,18 +296,23 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
Io_ObjSetAigerNum( pObj, nNodes++ );
// write the header "M I L O A" where M = I + L + A
fprintf( pFile, "aig%s %u %u %u %u %u\n",
fprintf( pFile, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
Abc_NtkPiNum(pNtk),
Abc_NtkLatchNum(pNtk),
Abc_NtkPoNum(pNtk),
Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Abc_NtkNodeNum(pNtk) );
// write the extended header "B C J F"
if ( Abc_NtkConstrNum(pNtk) )
fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
fprintf( pFile, "\n" );
// 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
Abc_NtkInvertConstraints( pNtk );
if ( !fCompact )
{
// write latch drivers
@ -331,6 +336,7 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
Abc_NtkInvertConstraints( pNtk );
// write the nodes into the buffer
Pos = 0;
@ -427,30 +433,35 @@ void Io_WriteAigerGz( 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
gzprintf( pFile, "aig %u %u %u %u %u\n",
gzprintf( pFile, "aig %u %u %u %u %u",
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
Abc_NtkPiNum(pNtk),
Abc_NtkLatchNum(pNtk),
Abc_NtkPoNum(pNtk),
Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Abc_NtkNodeNum(pNtk) );
// write the extended header "B C J F"
if ( Abc_NtkConstrNum(pNtk) )
gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
gzprintf( pFile, "\n" );
// 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_NtkInvertConstraints( pNtk );
Abc_NtkForEachLatchInput( pNtk, pObj, i )
{
pDriver = Abc_ObjFanin0(pObj);
gzprintf( 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);
gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
}
Abc_NtkInvertConstraints( pNtk );
// write the nodes into the buffer
Pos = 0;
@ -628,18 +639,23 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
Io_ObjSetAigerNum( pObj, nNodes++ );
// write the header "M I L O A" where M = I + L + A
fprintfBz2Aig( &b, "aig%s %u %u %u %u %u\n",
fprintfBz2Aig( &b, "aig%s %u %u %u %u %u",
fCompact? "2" : "",
Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk),
Abc_NtkPiNum(pNtk),
Abc_NtkLatchNum(pNtk),
Abc_NtkPoNum(pNtk),
Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
Abc_NtkNodeNum(pNtk) );
// write the extended header "B C J F"
if ( Abc_NtkConstrNum(pNtk) )
fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
fprintfBz2Aig( &b, "\n" );
// 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
Abc_NtkInvertConstraints( pNtk );
if ( !fCompact )
{
// write latch drivers
@ -675,6 +691,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
Vec_StrFree( vBinary );
Vec_IntFree( vLits );
}
Abc_NtkInvertConstraints( pNtk );
// write the nodes into the buffer
Pos = 0;