diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.h | 2 | ||||
-rw-r--r-- | src/base/abc/abcUtil.c | 24 | ||||
-rw-r--r-- | src/base/abci/abc.c | 31 | ||||
-rw-r--r-- | src/base/io/ioReadAiger.c | 116 | ||||
-rw-r--r-- | src/base/io/ioWriteAiger.c | 31 |
5 files changed, 167 insertions, 37 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index de5bc663..aaf6d534 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 1e5777b9..e002347b 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 02694856..c5fc491f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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" ); 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; |