diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
commit | 3f4fc5e4507f7fb9df431fc116529b4c209ab97c (patch) | |
tree | d468f472a10aa98499f98c639447b7838e495476 /src/base/io | |
parent | 8e5398c501a873dffcb562a11bc19e630872c931 (diff) | |
download | abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.gz abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.bz2 abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.zip |
Version abc60407
Diffstat (limited to 'src/base/io')
-rw-r--r-- | src/base/io/ioRead.c | 3 | ||||
-rw-r--r-- | src/base/io/ioReadBench.c | 2 | ||||
-rw-r--r-- | src/base/io/ioWriteCnf.c | 40 | ||||
-rw-r--r-- | src/base/io/ioWriteDot.c | 8 | ||||
-rw-r--r-- | src/base/io/ioWriteList.c | 30 |
5 files changed, 64 insertions, 19 deletions
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c index 6422461c..70e648a7 100644 --- a/src/base/io/ioRead.c +++ b/src/base/io/ioRead.c @@ -42,6 +42,9 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck ) { Abc_Ntk_t * pNtk, * pTemp; +// extern int s_TotalNodes; +// extern int s_TotalChanges; +// s_TotalNodes = s_TotalChanges = 0; // set the new network if ( Extra_FileNameCheckExtension( pFileName, "blif" ) ) pNtk = Io_ReadBlif( pFileName, fCheck ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 1cb0ae5d..aa7f82e3 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -136,7 +136,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) ); else if ( strcmp(pType, "XOR") == 0 ) Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) ); - else if ( strcmp(pType, "NXOR") == 0 ) + else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 ) Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) ); else if ( strncmp(pType, "BUF", 3) == 0 ) Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) ); diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 9e5ceb9f..24612566 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -23,6 +23,8 @@ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * s_pNtk = NULL; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -57,15 +59,51 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" ); return 0; } + if ( Abc_NtkNodeNum(pNtk) == 0 ) + { + fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" ); + return 0; + } // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk ); + pSat = Abc_NtkMiterSatCreate( pNtk, 0 ); + if ( pSat == NULL ) + { + fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); + return 1; + } // write the clauses + s_pNtk = pNtk; Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); + s_pNtk = NULL; // free the solver solver_delete( pSat ); return 1; } +/**Function************************************************************* + + Synopsis [Output the mapping of PIs into variable numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ) +{ + extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); + Abc_Ntk_t * pNtk = s_pNtk; + Vec_Int_t * vCiIds; + Abc_Obj_t * pObj; + int i; + vCiIds = Abc_NtkGetCiSatVarNums( pNtk ); + fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" ); + Abc_NtkForEachCi( pNtk, pObj, i ) + fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) ); + Vec_IntFree( vCiIds ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index dbf157bf..ed6acb24 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -412,7 +412,13 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return; + } + } // mark the nodes from the set Vec_PtrForEachEntry( vNodes, pNode, i ) diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c index ab216eb3..f0981a8e 100644 --- a/src/base/io/ioWriteList.c +++ b/src/base/io/ioWriteList.c @@ -120,8 +120,8 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost ) if ( Abc_ObjFanoutNum( Abc_NtkConst1(pNtk) ) > 0 ) Io_WriteListEdge( pFile, Abc_NtkConst1(pNtk) ); - // write the PO edges - Abc_NtkForEachCi( pNtk, pObj, i ) + // write the PI edges + Abc_NtkForEachPi( pNtk, pObj, i ) Io_WriteListEdge( pFile, pObj ); // write the internal nodes @@ -132,7 +132,7 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost ) if ( fUseHost ) Io_WriteListHost( pFile, pNtk ); else - Abc_NtkForEachCo( pNtk, pObj, i ) + Abc_NtkForEachPo( pNtk, pObj, i ) Io_WriteListEdge( pFile, pObj ); fprintf( pFile, "\n" ); @@ -157,12 +157,13 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj ) fprintf( pFile, "%-10s > ", Abc_ObjName(pObj) ); Abc_ObjForEachFanout( pObj, pFanout, i ) { - fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) ); - if ( i == Abc_ObjFanoutNum(pObj) - 1 ) - fprintf( pFile, "." ); - else + fprintf( pFile, " %s", Abc_ObjName(pFanout) ); + fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) ); + fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) ); + if ( i != Abc_ObjFanoutNum(pObj) - 1 ) fprintf( pFile, "," ); } + fprintf( pFile, "." ); fprintf( pFile, "\n" ); } @@ -186,22 +187,19 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk ) { fprintf( pFile, "%-10s > ", Abc_ObjName(pObj) ); fprintf( pFile, " %s ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), "HOST", 0 ); - if ( i == Abc_NtkPoNum(pNtk) - 1 ) - fprintf( pFile, "." ); - else - fprintf( pFile, "," ); + fprintf( pFile, "." ); + fprintf( pFile, "\n" ); } - fprintf( pFile, "\n" ); fprintf( pFile, "%-10s > ", "HOST" ); Abc_NtkForEachPi( pNtk, pObj, i ) { - fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pObj), "HOST", Abc_ObjName(pObj), 0 ); - if ( i == Abc_NtkPiNum(pNtk) - 1 ) - fprintf( pFile, "." ); - else + fprintf( pFile, " %s", Abc_ObjName(pObj) ); + fprintf( pFile, " ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), 0 ); + if ( i != Abc_NtkPiNum(pNtk) - 1 ) fprintf( pFile, "," ); } + fprintf( pFile, "." ); fprintf( pFile, "\n" ); } |