summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/ioReadAiger.c116
-rw-r--r--src/base/io/ioWriteAiger.c31
2 files changed, 120 insertions, 27 deletions
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index a5f6fb1d..13987a1b 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -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;
}
- // 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 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" );
+ ABC_FREE( pContents );
+ 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" );
+ 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 );
+ 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 ) )
{
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 18264d6b..9ab0905e 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 16:29:09 +0000