summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/io.c105
-rw-r--r--src/base/io/io.h12
-rw-r--r--src/base/io/ioInt.h4
-rw-r--r--src/base/io/ioWriteBlif.c2
-rw-r--r--src/base/io/ioWriteDot.c2
-rw-r--r--src/base/io/ioWritePla.c19
6 files changed, 133 insertions, 11 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2725eb8a..0aa5e415 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -45,6 +45,7 @@ static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -83,6 +84,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
}
/**Function*************************************************************
@@ -1174,7 +1176,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
if ( Abc_NtkIsSopLogic(pNtk) )
Abc_NtkLogicMakeDirectSops(pNtk);
// derive the netlist
- pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+ pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
if ( pNtkTemp == NULL )
{
fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
@@ -1358,6 +1360,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
}
+ if ( Abc_NtkGetLevelNum(pNtk) > 1 )
+ {
+ fprintf( pAbc->Out, "PLA writing is available for collapsed networks.\n" );
+ return 0;
+ }
+
if ( Abc_NtkLatchNum(pNtk) > 0 )
{
fprintf( pAbc->Out, "Latches are writed at PI/PO pairs in the PLA file.\n" );
@@ -1368,11 +1376,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
{
goto usage;
}
+
// get the input file name
FileName = argv[globalUtilOptind];
// derive the netlist
- pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+ pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
if ( pNtkTemp == NULL )
{
fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1434,7 +1443,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
FileName = argv[globalUtilOptind];
// derive the netlist
- pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+ pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
if ( pNtkTemp == NULL )
{
fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1452,6 +1461,96 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * FileName;
+ int c;
+ int fNames;
+
+ fNames = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'n':
+ fNames ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ pNtk = pAbc->pNtkCur;
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( argc != globalUtilOptind + 1 )
+ {
+ goto usage;
+ }
+ // get the input file name
+ FileName = argv[globalUtilOptind];
+
+ if ( pNtk->pModel == NULL )
+ {
+ fprintf( pAbc->Out, "Counter-example is not available.\n" );
+ return 0;
+ }
+
+ // write the counter-example into the file
+ {
+ Abc_Obj_t * pObj;
+ FILE * pFile = fopen( FileName, "w" );
+ int i;
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+ return 1;
+ }
+ if ( fNames )
+ {
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
+ }
+ else
+ {
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) );
+ }
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+ }
+
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
+ fprintf( pAbc->Err, "\t writes the counter-example derived by \"prove\" or \"sat\"\n" );
+ fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
+ fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/io/io.h b/src/base/io/io.h
index fe5c237f..a9a61040 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -21,6 +21,10 @@
#ifndef __IO_H__
#define __IO_H__
+#ifdef __cplusplus
+extern "C" {
+#endif
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -94,9 +98,13 @@ extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteVerilog.c ==========================================================*/
extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-#endif
-
diff --git a/src/base/io/ioInt.h b/src/base/io/ioInt.h
index 7f4e200e..3daf3c75 100644
--- a/src/base/io/ioInt.h
+++ b/src/base/io/ioInt.h
@@ -41,9 +41,9 @@
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#endif
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-#endif
-
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 6b6c4a92..1b515a1e 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -53,7 +53,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
{
Abc_Ntk_t * pNtkTemp;
// derive the netlist
- pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+ pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
if ( pNtkTemp == NULL )
{
fprintf( stdout, "Writing BLIF has failed.\n" );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 373c4636..dbf157bf 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -412,7 +412,7 @@ 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);
+ Abc_NtkBddToSop(pNtk, 0);
// mark the nodes from the set
Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 12ac9ef7..4da8aca8 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -88,7 +88,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
nProducts = 0;
Abc_NtkForEachCo( pNtk, pNode, i )
{
- pDriver = Abc_ObjFanin0Ntk(pNode);
+ pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
if ( !Abc_ObjIsNode(pDriver) )
{
nProducts++;
@@ -138,9 +138,10 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
pCubeOut[i] = '1';
// consider special cases of nodes
- pDriver = Abc_ObjFanin0Ntk(pNode);
+ pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
if ( !Abc_ObjIsNode(pDriver) )
{
+ assert( Abc_ObjIsCi(pDriver) );
pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
pCubeIn[(int)pDriver->pCopy] = '-';
@@ -152,17 +153,29 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
continue;
}
+
+ // make sure the cover is not complemented
+ assert( !Abc_SopIsComplement( pDriver->pData ) );
+
// write the cubes
nFanins = Abc_ObjFaninNum(pDriver);
Abc_SopForEachCube( pDriver->pData, nFanins, pCube )
{
Abc_ObjForEachFanin( pDriver, pFanin, k )
+ {
+ pFanin = Abc_ObjFanin0Ntk(pFanin);
+ assert( (int)pFanin->pCopy < nInputs );
pCubeIn[(int)pFanin->pCopy] = pCube[k];
+ }
fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
}
// clean the cube for future writing
Abc_ObjForEachFanin( pDriver, pFanin, k )
+ {
+ pFanin = Abc_ObjFanin0Ntk(pFanin);
+ assert( Abc_ObjIsCi(pFanin) );
pCubeIn[(int)pFanin->pCopy] = '-';
+ }
Extra_ProgressBarUpdate( pProgress, i, NULL );
}
Extra_ProgressBarStop( pProgress );
@@ -171,6 +184,8 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
// clean the CI nodes
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = NULL;
+ free( pCubeIn );
+ free( pCubeOut );
return 1;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 15:20:07 +0000