summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.c281
-rw-r--r--src/base/abc/abc.h25
-rw-r--r--src/base/abc/abcAig.c55
-rw-r--r--src/base/abc/abcCollapse.c53
-rw-r--r--src/base/abc/abcCreate.c2
-rw-r--r--src/base/abc/abcDsd.c74
-rw-r--r--src/base/abc/abcFraig.c2
-rw-r--r--src/base/abc/abcFunc.c51
-rw-r--r--src/base/abc/abcMiter.c4
-rw-r--r--src/base/abc/abcPrint.c4
-rw-r--r--src/base/abc/abcReconv.c430
-rw-r--r--src/base/abc/abcRefactor.c4
-rw-r--r--src/base/abc/abcRefs.c4
-rw-r--r--src/base/abc/abcShow.c211
-rw-r--r--src/base/abc/abcStrash.c6
-rw-r--r--src/base/abc/abcSweep.c2
-rw-r--r--src/base/abc/abcSymm.c202
-rw-r--r--src/base/abc/abcUnreach.c7
-rw-r--r--src/base/abc/abcUtil.c23
-rw-r--r--src/base/abc/module.make1
-rw-r--r--src/base/io/io.c295
-rw-r--r--src/base/io/io.h8
-rw-r--r--src/base/io/ioRead.c2
-rw-r--r--src/base/io/ioReadEqn.c254
-rw-r--r--src/base/io/ioWriteBlif.c5
-rw-r--r--src/base/io/ioWriteCnf.c4
-rw-r--r--src/base/io/ioWriteDot.c322
-rw-r--r--src/base/io/ioWriteEqn.c261
-rw-r--r--src/base/io/ioWriteGml.c116
-rw-r--r--src/base/io/module.make4
30 files changed, 2437 insertions, 275 deletions
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 7c949ee0..0d911e79 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -36,8 +36,11 @@ static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSymms ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -105,8 +108,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "print_symm", Abc_CommandPrintSymms, 0 );
Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "show_aig", Abc_CommandShowAig, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 );
@@ -297,9 +303,10 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: print_io [-h]\n" );
+ fprintf( pErr, "usage: print_io [-h] <node>\n" );
fprintf( pErr, "\t prints the PIs/POs or fanins/fanouts of a node\n" );
fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\tnode : the node to print fanins/fanouts\n");
return 1;
}
@@ -629,13 +636,85 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fUseBdds;
+ int fNaive;
+ int fVerbose;
+ extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
+
+ pNtk = Abc_FrameReadNet(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fUseBdds = 1;
+ fNaive = 0;
+ fVerbose = 0;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'b':
+ fUseBdds ^= 1;
+ break;
+ case 'n':
+ fNaive ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command works only for AIGs.\n" );
+ return 1;
+ }
+ Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: print_symm [-nbvh]\n" );
+ fprintf( pErr, "\t computes symmetries of the PO functions\n" );
+ fprintf( pErr, "\t-b : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" );
+ fprintf( pErr, "\t-n : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );
+ fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
int c;
- extern void Abc_NodePrintBdd( Abc_Obj_t * pNode );
+ extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -662,7 +741,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsBddLogic(pNtk) )
{
- fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
+ fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" );
return 1;
}
@@ -678,7 +757,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
return 1;
}
- Abc_NodePrintBdd( pNode );
+ Abc_NodeShowBdd( pNode );
return 0;
usage:
@@ -693,6 +772,168 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pNode;
+ int c;
+ int nNodeSizeMax;
+ int nConeSizeMax;
+ extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax );
+
+ pNtk = Abc_FrameReadNet(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nNodeSizeMax = 10;
+ nConeSizeMax = ABC_INFINITY;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( util_optind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nNodeSizeMax = atoi(argv[util_optind]);
+ util_optind++;
+ if ( nNodeSizeMax < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( util_optind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConeSizeMax = atoi(argv[util_optind]);
+ util_optind++;
+ if ( nConeSizeMax < 0 )
+ goto usage;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Visualizing cuts only works for AIGs.\n" );
+ return 1;
+ }
+ if ( argc != util_optind + 1 )
+ {
+ fprintf( pErr, "Wrong number of auguments.\n" );
+ goto usage;
+ }
+
+ pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+ if ( pNode == NULL )
+ {
+ fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+ return 1;
+ }
+ Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: show_cut [-N num] [-C num] [-h] <node>\n" );
+ fprintf( pErr, " visualizes the cut of a node using DOT and GSVIEW\n" );
+#ifdef WIN32
+ fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+ fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+ fprintf( pErr, "\t-N num : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax );
+ fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );
+ fprintf( pErr, "\tnode : the node to consider\n");
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
+
+ pNtk = Abc_FrameReadNet(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" );
+ return 1;
+ }
+ Abc_NtkShowAig( pNtk );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: show_aig [-h]\n" );
+ fprintf( pErr, " visualizes the AIG with choices using DOT and GSVIEW\n" );
+#ifdef WIN32
+ fprintf( pErr, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+ fprintf( pErr, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -745,7 +986,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes = Abc_NtkCollapse( pNtk, 1 );
else
{
- pNtk = Abc_NtkStrash( pNtk, 0 );
+ pNtk = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkCollapse( pNtk, 1 );
Abc_NtkDelete( pNtk );
}
@@ -783,6 +1024,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fAllNodes;
+ int fCleanup;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -790,14 +1032,18 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAllNodes = 0;
+ fCleanup = 1;
util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF )
+ while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF )
{
switch ( c )
{
case 'a':
fAllNodes ^= 1;
break;
+ case 'c':
+ fCleanup ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -812,7 +1058,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkStrash( pNtk, fAllNodes );
+ pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Strashing has failed.\n" );
@@ -823,9 +1069,10 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: strash [-ah]\n" );
+ fprintf( pErr, "usage: strash [-ach]\n" );
fprintf( pErr, "\t transforms combinational logic into an AIG\n" );
fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
+ fprintf( pErr, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -882,7 +1129,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pNtkTemp = Abc_NtkStrash( pNtk, 0 );
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtkTemp == NULL )
{
fprintf( pErr, "Strashing before balancing has failed.\n" );
@@ -1274,7 +1521,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( !Abc_NtkIsStrash(pNtk) )
{
- pNtkNew = Abc_NtkStrash( pNtk, 0 );
+ pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
Abc_NtkDelete( pNtkNew );
}
@@ -1732,7 +1979,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
// get the new network
if ( !Abc_NtkIsStrash(pNtk) )
{
- pNtkTemp = Abc_NtkStrash( pNtk, 0 );
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
Abc_NtkDelete( pNtkTemp );
}
@@ -2424,7 +2671,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
else
{
- pNtk = Abc_NtkStrash( pNtk, 0 );
+ pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
Abc_NtkDelete( pNtk );
}
@@ -2845,7 +3092,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
- pNtk = Abc_NtkStrash( pNtk, 0 );
+ pNtk = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtk == NULL )
{
fprintf( pErr, "Strashing before mapping has failed.\n" );
@@ -3087,8 +3334,10 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: sc [-h]\n" );
- fprintf( pErr, "\t performs superchoicing\n" );
- fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\t performs superchoicing\n" );
+ fprintf( pErr, "\t (accumulate: \"r file.blif; rsup; b; sc; f -ac; wb file_sc.blif\")\n" );
+ fprintf( pErr, "\t (map without supergate library: \"r file_sc.blif; ft; map\")\n" );
+ fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -3146,7 +3395,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
// strash and balance the network
- pNtk = Abc_NtkStrash( pNtk, 0 );
+ pNtk = Abc_NtkStrash( pNtk, 0, 0 );
if ( pNtk == NULL )
{
fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index a3f7ddb7..ab457cc9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -51,7 +51,7 @@ typedef enum {
ABC_TYPE_OTHER // 5: unused
} Abc_NtkType_t;
-// functionality types
+// network functionality
typedef enum {
ABC_FUNC_NONE, // 0: unknown
ABC_FUNC_SOP, // 1: sum-of-products
@@ -155,13 +155,16 @@ struct Abc_Ntk_t_
int nPos; // the number of primary outputs
// the functionality manager
void * pManFunc; // AIG manager, BDD manager, or memory manager for SOPs
+ // the global functions (BDDs)
+ void * pManGlob; // the BDD manager
+ Vec_Ptr_t * vFuncsGlob; // the BDDs of CO functions
// the timing manager (for mapped networks)
Abc_ManTime_t * pManTime; // stores arrival/required times for all nodes
// the cut manager (for AIGs)
void * pManCut; // stores information about the cuts computed for the nodes
// level information (for AIGs)
int LevelMax; // maximum number of levels
- Vec_Int_t * vLevelsR; // level in the reverse topological order
+ Vec_Int_t * vLevelsR; // level in the reverse topological order
// the external don't-care if given
Abc_Ntk_t * pExdc; // the EXDC network
// miscellaneous data members
@@ -401,8 +404,11 @@ extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld
extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
extern void Abc_AigPrintNode( Abc_Obj_t * pNode );
+extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
/*=== abcAttach.c ==========================================================*/
extern int Abc_NtkAttach( Abc_Ntk_t * pNtk );
+/*=== abcBalance.c ==========================================================*/
+extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
/*=== abcCheck.c ==========================================================*/
extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk );
extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
@@ -410,7 +416,7 @@ extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t *
/*=== abcCollapse.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
-extern void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
+extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
/*=== abcCreate.c ==========================================================*/
extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@@ -475,6 +481,7 @@ extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager
extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
/*=== abcLatch.c ==========================================================*/
extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
@@ -519,13 +526,15 @@ extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
/*=== abcReconv.c ==========================================================*/
-extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax );
+extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
extern void Abc_NtkManCutStop( Abc_ManCut_t * p );
-extern Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p );
+extern Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
+extern void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
-extern void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult );
+extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
/*=== abcRefs.c ==========================================================*/
extern int Abc_NodeMffcSize( Abc_Obj_t * pNode );
extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
@@ -576,12 +585,11 @@ extern bool Abc_SopCheck( char * pSop, int nFanins );
extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
/*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
extern Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
extern int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
-extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
/*=== abcSweep.c ==========================================================*/
extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
@@ -643,6 +651,7 @@ extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollect
extern void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk );
extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f71c0a15..9588f1e0 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -705,8 +705,10 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
assert( iFanin == 0 || iFanin == 1 );
// get the new fanin
pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
+ assert( Abc_ObjRegular(pFanin1) != pFanout );
// get another fanin
pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
+ assert( Abc_ObjRegular(pFanin2) != pFanout );
// check if the node with these fanins exists
if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
{ // such node exists (it may be a constant)
@@ -732,6 +734,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
Abc_ObjRemoveFanins( pFanout );
// recreate the old fanout with new fanins and add it to the table
Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+ assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
// schedule the updated fanout for updating direct level
assert( pFanout->fMarkA == 0 );
@@ -876,6 +879,7 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
if ( pNode == NULL )
continue;
assert( Abc_ObjIsNode(pNode) );
+ assert( (int)pNode->Level == i );
// clean the mark
assert( pNode->fMarkA == 1 );
pNode->fMarkA = 0;
@@ -931,6 +935,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
if ( pNode == NULL )
continue;
assert( Abc_ObjIsNode(pNode) );
+ assert( Abc_NodeReadReverseLevel(pNode) == i );
// clean the mark
assert( pNode->fMarkB == 1 );
pNode->fMarkB = 0;
@@ -1113,6 +1118,56 @@ void Abc_AigPrintNode( Abc_Obj_t * pNode )
printf( "\n" );
}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the node has a combination loop of depth 1 or 2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
+{
+ Abc_Obj_t * pFanin0, * pFanin1;
+ Abc_Obj_t * pChild00, * pChild01;
+ Abc_Obj_t * pChild10, * pChild11;
+ if ( !Abc_NodeIsAigAnd(pNode) )
+ return 1;
+ pFanin0 = Abc_ObjFanin0(pNode);
+ pFanin1 = Abc_ObjFanin1(pNode);
+ if ( pRoot == pFanin0 || pRoot == pFanin1 )
+ return 0;
+ if ( Abc_ObjIsCi(pFanin0) )
+ {
+ pChild00 = NULL;
+ pChild01 = NULL;
+ }
+ else
+ {
+ pChild00 = Abc_ObjFanin0(pFanin0);
+ pChild01 = Abc_ObjFanin1(pFanin0);
+ if ( pRoot == pChild00 || pRoot == pChild01 )
+ return 0;
+ }
+ if ( Abc_ObjIsCi(pFanin1) )
+ {
+ pChild10 = NULL;
+ pChild11 = NULL;
+ }
+ else
+ {
+ pChild10 = Abc_ObjFanin0(pFanin1);
+ pChild11 = Abc_ObjFanin1(pFanin1);
+ if ( pRoot == pChild10 || pRoot == pChild11 )
+ return 0;
+ }
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index e07636cc..a6eda7b3 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -25,7 +25,7 @@
////////////////////////////////////////////////////////////////////////
static DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
-static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
////////////////////////////////////////////////////////////////////////
@@ -47,26 +47,26 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
{
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
- DdManager * dd;
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
- dd = Abc_NtkGlobalBdds( pNtk, 0 );
- if ( dd == NULL )
+ if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
return NULL;
if ( fVerbose )
- printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+ printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
// create the new network
- pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
- Abc_NtkFreeGlobalBdds( dd, pNtk );
+ pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
+ Abc_NtkFreeGlobalBdds( pNtk );
if ( pNtkNew == NULL )
{
- Cudd_Quit( dd );
+ Cudd_Quit( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
return NULL;
}
- Extra_StopManager( dd );
+ Extra_StopManager( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
// make the network minimum base
Abc_NtkMinimumBase( pNtkNew );
@@ -96,12 +96,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
{
int fReorder = 1;
ProgressBar * pProgress;
+ Vec_Ptr_t * vFuncsGlob;
Abc_Obj_t * pNode;
DdNode * bFunc;
DdManager * dd;
int i;
// start the manager
+ assert( pNtk->pManGlob == NULL );
dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
@@ -114,6 +116,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
pNode = Abc_AigConst1( pNtk->pManFunc );
pNode->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one );
+ vFuncsGlob = Vec_PtrAlloc( 100 );
if ( fLatchOnly )
{
// construct the BDDs
@@ -129,8 +132,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_Quit( dd );
return NULL;
}
- bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
- pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc );
+ bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
+ Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
@@ -149,8 +152,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_Quit( dd );
return NULL;
}
- bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
- pNode->pNext = (Abc_Obj_t *)bFunc; Cudd_Ref( bFunc );
+ bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc );
+ Vec_PtrPush( vFuncsGlob, bFunc );
}
Extra_ProgressBarStop( pProgress );
}
@@ -168,6 +171,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
Cudd_AutodynDisable( dd );
}
+ pNtk->pManGlob = dd;
+ pNtk->vFuncsGlob = vFuncsGlob;
return dd;
}
@@ -223,11 +228,12 @@ DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
{
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
+ DdManager * dd = pNtk->pManGlob;
int i;
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@@ -238,7 +244,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
Abc_NtkForEachCo( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
- pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
+ pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
@@ -281,17 +287,16 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
SeeAlso []
***********************************************************************/
-void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
{
- Abc_Obj_t * pNode;
+ DdNode * bFunc;
int i;
- Abc_NtkForEachCo( pNtk, pNode, i )
- {
- if ( pNode->pNext == NULL )
- continue;
- Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
- pNode->pNext = NULL;
- }
+ assert( pNtk->pManGlob );
+ assert( pNtk->vFuncsGlob );
+ Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
+ Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
+ Vec_PtrFree( pNtk->vFuncsGlob );
+ pNtk->vFuncsGlob = NULL;
}
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9186ec5a..d6500803 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -818,7 +818,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
// find the internal node
if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
{
- printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName );
+ printf( "Name \"%s\" is not found among CIs/COs (internal name looks like this: \"[integer]\").\n", pName );
return NULL;
}
Num = atoi( pName + 1 );
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index d1445e75..ccb52ffa 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -25,8 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
-static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose );
+static Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
static void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
static Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
@@ -58,25 +57,25 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
{
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
- DdManager * dd;
assert( Abc_NtkIsStrash(pNtk) );
// perform FPGA mapping
- dd = Abc_NtkGlobalBdds( pNtk, 0 );
- if ( dd == NULL )
+ if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
return NULL;
if ( fVerbose )
- printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+ printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
// transform the result of mapping into a BDD network
- pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort );
+ pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
if ( pNtkNew == NULL )
{
- Cudd_Quit( dd );
+ Cudd_Quit( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
return NULL;
}
- Extra_StopManager( dd );
+ Extra_StopManager( pNtk->pManGlob );
+ pNtk->pManGlob = NULL;
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
@@ -99,17 +98,33 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
{
+ DdManager * dd = pNtk->pManGlob;
Dsd_Manager_t * pManDsd;
Abc_Ntk_t * pNtkNew;
+ DdNode * bFunc;
char ** ppNamesCi, ** ppNamesCo;
+ Abc_Obj_t * pObj;
+ int i;
+
+ // complement the global functions
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ bFunc = Vec_PtrEntry(pNtk->vFuncsGlob, i);
+ Vec_PtrWriteEntry(pNtk->vFuncsGlob, i, Cudd_NotCond(bFunc, Abc_ObjFaninC0(pObj)) );
+ }
// perform the decomposition
- pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
- Abc_NtkFreeGlobalBdds( dd, pNtk );
+ assert( Vec_PtrSize(pNtk->vFuncsGlob) == Abc_NtkCoNum(pNtk) );
+ pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
+ Dsd_Decompose( pManDsd, (DdNode **)pNtk->vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
+ Abc_NtkFreeGlobalBdds( pNtk );
if ( pManDsd == NULL )
+ {
+ Cudd_Quit( dd );
return NULL;
+ }
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@@ -119,6 +134,8 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
// finalize the new network
Abc_NtkFinalize( pNtk, pNtkNew );
+ // fix the problem with complemented and duplicated CO edges
+ Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
if ( fPrint )
{
@@ -136,39 +153,6 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
/**Function*************************************************************
- Synopsis [Performs DSD by creating the manager and decomposing the functions.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose )
-{
- Dsd_Manager_t * pManDsd;
- DdNode ** pbFuncsGlo;
- Abc_Obj_t * pNode;
- int i;
-
- // collect global functions into the array
- pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
- Abc_NtkForEachCo( pNtk, pNode, i )
- {
- pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) );
-//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) );
- }
-
- // start the DSD manager and decompose global functions
- pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
- Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) );
- FREE( pbFuncsGlo );
- return pManDsd;
-}
-
-/**Function*************************************************************
-
Synopsis [Constructs the decomposed network.]
Description []
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index bb7d8cfa..83735e47 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -433,7 +433,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
if ( pStore == NULL )
{
// start the stored network
- pStore = Abc_NtkStrash( pNtk, 0 );
+ pStore = Abc_NtkStrash( pNtk, 0, 0 );
if ( pStore == NULL )
{
printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index f616a258..44acb699 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -128,6 +128,57 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins )
return bRes;
}
+/**Function*************************************************************
+
+ Synopsis [Removes complemented SOP covers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
+{
+ DdManager * dd;
+ DdNode * bFunc;
+ Vec_Str_t * vCube;
+ Abc_Obj_t * pNode;
+ int nFaninsMax, fFound, i;
+
+ assert( Abc_NtkIsSopLogic(pNtk) );
+
+ // check if there are nodes with complemented SOPs
+ fFound = 0;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( Abc_SopIsComplement(pNode->pData) )
+ {
+ fFound = 1;
+ break;
+ }
+ if ( !fFound )
+ return;
+
+ // start the BDD package
+ nFaninsMax = Abc_NtkGetFaninMax( pNtk );
+ if ( nFaninsMax == 0 )
+ printf( "Warning: The network has only constant nodes.\n" );
+ dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+
+ // change the cover of negated nodes
+ vCube = Vec_StrAlloc( 100 );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( Abc_SopIsComplement(pNode->pData) )
+ {
+ bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); Cudd_Ref( bFunc );
+ pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 );
+ Cudd_RecursiveDeref( dd, bFunc );
+ assert( !Abc_SopIsComplement(pNode->pData) );
+ }
+ Vec_StrFree( vCube );
+ Extra_StopManager( dd );
+}
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index b8bcec4d..a0426dc2 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abc/abcMiter.c
@@ -55,8 +55,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
return NULL;
// make sure the circuits are strashed
- fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
- fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
+ fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
+ fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
if ( pNtk1 && pNtk2 )
pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 337dd43b..c7599f11 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -44,8 +44,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
{
int Num;
- fprintf( pFile, "%-15s:", pNtk->pName );
- fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+ fprintf( pFile, "%-13s:", pNtk->pName );
+ fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
if ( !Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
index e02ccba0..ea662799 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abc/abcReconv.c
@@ -30,14 +30,19 @@ struct Abc_ManCut_t_
// user specified parameters
int nNodeSizeMax; // the limit on the size of the supernode
int nConeSizeMax; // the limit on the size of the containing cone
+ int nNodeFanStop; // the limit on the size of the supernode
+ int nConeFanStop; // the limit on the size of the containing cone
// internal parameters
- Vec_Ptr_t * vFaninsNode; // fanins of the supernode
- Vec_Ptr_t * vFaninsCone; // fanins of the containing cone
+ Vec_Ptr_t * vNodeLeaves; // fanins of the collapsed node (the cut)
+ Vec_Ptr_t * vConeLeaves; // fanins of the containing cone
Vec_Ptr_t * vVisited; // the visited nodes
+ Vec_Vec_t * vLevels; // the data structure to compute TFO nodes
+ Vec_Ptr_t * vNodesTfo; // the nodes in the TFO of the cut
};
-static int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit );
-static void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+static int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
+static int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
+static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -92,45 +97,142 @@ static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
SeeAlso []
***********************************************************************/
-static inline void Abc_NodesUnmarkBoth( Vec_Ptr_t * vVisited )
+static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
{
Abc_Obj_t * pNode;
int i;
Vec_PtrForEachEntry( vVisited, pNode, i )
- pNode->fMarkA = pNode->fMarkB = 0;
+ pNode->fMarkB = 0;
}
/**Function*************************************************************
- Synopsis [Evaluate the fanin cost.]
+ Synopsis [Evaluate the cost of removing the node from the set of leaves.]
- Description [Returns the number of fanins that will be brought in.
- Returns large number if the node cannot be added.]
+ Description [Returns the number of new leaves that will be brought in.
+ Returns large number if the node cannot be removed from the set of leaves.]
SideEffects []
SeeAlso []
***********************************************************************/
-static inline int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
+static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
{
- Abc_Obj_t * pFanout;
- int i;
- assert( pNode->fMarkA == 1 ); // this node is in the TFI
- assert( pNode->fMarkB == 1 ); // this node is in the constructed cone
- // check the PI node
+ int Cost;
+ // make sure the node is in the construction zone
+ assert( pNode->fMarkB == 1 );
+ // cannot expand over the PI node
+ if ( Abc_ObjIsCi(pNode) )
+ return 999;
+ // get the cost of the cone
+ Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+ // always accept if the number of leaves does not increase
+ if ( Cost < 2 )
+ return Cost;
+ // skip nodes with many fanouts
+ if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+ return 999;
+ // return the number of nodes that will be on the leaves if this node is removed
+ return Cost;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluate the cost of removing the node from the set of leaves.]
+
+ Description [Returns the number of new leaves that will be brought in.
+ Returns large number if the node cannot be removed from the set of leaves.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit,
+ Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
+{
+ Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
+ Abc_Obj_t * pGrand, * pGrandToAdd;
+ // make sure the node is in the construction zone
+ assert( pNode->fMarkB == 1 );
+ // cannot expand over the PI node
if ( Abc_ObjIsCi(pNode) )
return 999;
// skip nodes with many fanouts
- if ( Abc_ObjFanoutNum(pNode) > 5 )
+// if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+// return 999;
+ // get the children
+ pFanin0 = Abc_ObjFanin0(pNode);
+ pFanin1 = Abc_ObjFanin1(pNode);
+ assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
+ // count the number of unique grandchildren that will be included
+ // return infinite cost if this number if more than 1
+ if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
return 999;
- // check the fanouts
- Abc_ObjForEachFanout( pNode, pFanout, i )
- if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // the fanout is in the TFI but not in the cone
+ // consider the special case when a non-CI fanin can be dropped
+ if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
+ {
+ *ppLeafToAdd = pFanin1;
+ *pNodeToMark1 = pFanin0;
+ *pNodeToMark2 = NULL;
+ return 1;
+ }
+ if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
+ {
+ *ppLeafToAdd = pFanin0;
+ *pNodeToMark1 = pFanin1;
+ *pNodeToMark2 = NULL;
+ return 1;
+ }
+
+ // make the first node CI if any
+ if ( Abc_ObjIsCi(pFanin1) )
+ pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
+ // consider the first node
+ pGrandToAdd = NULL;
+ if ( Abc_ObjIsCi(pFanin0) )
+ {
+ *pNodeToMark1 = NULL;
+ pGrandToAdd = pFanin0;
+ }
+ else
+ {
+ *pNodeToMark1 = pFanin0;
+ pGrand = Abc_ObjFanin0(pFanin0);
+ if ( !pGrand->fMarkB )
+ {
+ if ( pGrandToAdd && pGrandToAdd != pGrand )
+ return 999;
+ pGrandToAdd = pGrand;
+ }
+ pGrand = Abc_ObjFanin1(pFanin0);
+ if ( !pGrand->fMarkB )
+ {
+ if ( pGrandToAdd && pGrandToAdd != pGrand )
+ return 999;
+ pGrandToAdd = pGrand;
+ }
+ }
+ // consider the second node
+ *pNodeToMark2 = pFanin1;
+ pGrand = Abc_ObjFanin0(pFanin1);
+ if ( !pGrand->fMarkB )
+ {
+ if ( pGrandToAdd && pGrandToAdd != pGrand )
+ return 999;
+ pGrandToAdd = pGrand;
+ }
+ pGrand = Abc_ObjFanin1(pFanin1);
+ if ( !pGrand->fMarkB )
+ {
+ if ( pGrandToAdd && pGrandToAdd != pGrand )
return 999;
- // the fanouts are in the TFI and inside the constructed cone
- // return the number of fanins that will be on the boundary if this node is added
- return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+ pGrandToAdd = pGrand;
+ }
+ assert( pGrandToAdd != NULL );
+ *ppLeafToAdd = pGrandToAdd;
+ return 1;
}
@@ -153,117 +255,206 @@ Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain
assert( !Abc_ObjIsComplement(pRoot) );
assert( Abc_ObjIsNode(pRoot) );
- // mark TFI using fMarkA
+ // start the visited nodes and mark them
Vec_PtrClear( p->vVisited );
- Abc_NodesMarkCollect_rec( pRoot, p->vVisited );
-
- // start the cut
- Vec_PtrClear( p->vFaninsNode );
- Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin0(pRoot) );
- Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin1(pRoot) );
+ Vec_PtrPush( p->vVisited, pRoot );
+ Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
+ Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
pRoot->fMarkB = 1;
Abc_ObjFanin0(pRoot)->fMarkB = 1;
Abc_ObjFanin1(pRoot)->fMarkB = 1;
+ // start the cut
+ Vec_PtrClear( p->vNodeLeaves );
+ Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
+ Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
+
// compute the cut
- while ( Abc_NodeFindCut_int( p->vFaninsNode, p->nNodeSizeMax ) );
- assert( Vec_PtrSize(p->vFaninsNode) <= p->nNodeSizeMax );
+ while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
+ assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
// return if containing cut is not requested
if ( !fContain )
{
- // unmark TFI using fMarkA and fMarkB
- Abc_NodesUnmarkBoth( p->vVisited );
- return p->vFaninsNode;
+ // unmark both fMarkA and fMarkB in tbe TFI
+ Abc_NodesUnmarkB( p->vVisited );
+ return p->vNodeLeaves;
}
+//printf( "\n\n\n" );
// compute the containing cut
assert( p->nNodeSizeMax < p->nConeSizeMax );
// copy the current boundary
- Vec_PtrClear( p->vFaninsCone );
- Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
- Vec_PtrPush( p->vFaninsCone, pNode );
+ Vec_PtrClear( p->vConeLeaves );
+ Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i )
+ Vec_PtrPush( p->vConeLeaves, pNode );
// compute the containing cut
- while ( Abc_NodeFindCut_int( p->vFaninsCone, p->nConeSizeMax ) );
- assert( Vec_PtrSize(p->vFaninsCone) <= p->nConeSizeMax );
+ while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
+ assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
// unmark TFI using fMarkA and fMarkB
- Abc_NodesUnmarkBoth( p->vVisited );
- return p->vFaninsNode;
+ Abc_NodesUnmarkB( p->vVisited );
+ return p->vNodeLeaves;
}
/**Function*************************************************************
- Synopsis [Finds a reconvergence-driven cut.]
+ Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
- Description []
+ Description [This procedure looks at the current leaves and tries to change
+ one leaf at a time in such a way that the cut grows as little as possible.
+ In evaluating the fanins, this procedure looks only at their immediate
+ predecessors (this is why it is called a one-level construction procedure).]
SideEffects []
SeeAlso []
***********************************************************************/
-int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
+int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
{
Abc_Obj_t * pNode, * pFaninBest, * pNext;
int CostBest, CostCur, i;
-// int fFlagProb = (rand() & 1);
- int fFlagProb = 1;
// find the best fanin
CostBest = 100;
pFaninBest = NULL;
- if ( fFlagProb )
- {
- Vec_PtrForEachEntry( vFanins, pNode, i )
- {
- CostCur = Abc_NodeGetFaninCost( pNode );
- if ( CostBest > CostCur )
- {
- CostBest = CostCur;
- pFaninBest = pNode;
- }
- }
- }
- else
+//printf( "Evaluating fanins of the cut:\n" );
+ Vec_PtrForEachEntry( vLeaves, pNode, i )
{
- Vec_PtrForEachEntry( vFanins, pNode, i )
+ CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
+//printf( " Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
+ if ( CostBest > CostCur )
{
- CostCur = Abc_NodeGetFaninCost( pNode );
- if ( CostBest >= CostCur )
- {
- CostBest = CostCur;
- pFaninBest = pNode;
- }
+ CostBest = CostCur;
+ pFaninBest = pNode;
}
+ if ( CostBest == 0 )
+ break;
}
if ( pFaninBest == NULL )
return 0;
+// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
assert( CostBest < 3 );
- if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+ if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
return 0;
+// return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
assert( Abc_ObjIsNode(pFaninBest) );
// remove the node from the array
- Vec_PtrRemove( vFanins, pFaninBest );
+ Vec_PtrRemove( vLeaves, pFaninBest );
+//printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) );
+
// add the left child to the fanins
pNext = Abc_ObjFanin0(pFaninBest);
if ( !pNext->fMarkB )
{
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
pNext->fMarkB = 1;
- Vec_PtrPush( vFanins, pNext );
+ Vec_PtrPush( vLeaves, pNext );
+ Vec_PtrPush( vVisited, pNext );
}
// add the right child to the fanins
pNext = Abc_ObjFanin1(pFaninBest);
if ( !pNext->fMarkB )
{
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
pNext->fMarkB = 1;
- Vec_PtrPush( vFanins, pNext );
+ Vec_PtrPush( vLeaves, pNext );
+ Vec_PtrPush( vVisited, pNext );
}
- assert( vFanins->nSize <= nSizeLimit );
+ assert( vLeaves->nSize <= nSizeLimit );
// keep doing this
return 1;
}
/**Function*************************************************************
+ Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+ Description [This procedure looks at the current leaves and tries to change
+ one leaf at a time in such a way that the cut grows as little as possible.
+ In evaluating the fanins, this procedure looks across two levels of fanins
+ (this is why it is called a two-level construction procedure).]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
+{
+ Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
+ int CostCur, i;
+ // find the best fanin
+ Vec_PtrForEachEntry( vLeaves, pNode, i )
+ {
+ CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
+ if ( CostCur < 2 )
+ break;
+ }
+ if ( CostCur > 2 )
+ return 0;
+ // remove the node from the array
+ Vec_PtrRemove( vLeaves, pNode );
+ // add the node to the leaves
+ if ( pLeafToAdd )
+ {
+ assert( !pLeafToAdd->fMarkB );
+ pLeafToAdd->fMarkB = 1;
+ Vec_PtrPush( vLeaves, pLeafToAdd );
+ Vec_PtrPush( vVisited, pLeafToAdd );
+ }
+ // mark the other nodes
+ if ( pNodeToMark1 )
+ {
+ assert( !pNodeToMark1->fMarkB );
+ pNodeToMark1->fMarkB = 1;
+ Vec_PtrPush( vVisited, pNodeToMark1 );
+ }
+ if ( pNodeToMark2 )
+ {
+ assert( !pNodeToMark2->fMarkB );
+ pNodeToMark2->fMarkB = 1;
+ Vec_PtrPush( vVisited, pNodeToMark2 );
+ }
+ // keep doing this
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Get the nodes contained in the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
+{
+ Abc_Obj_t * pTemp;
+ int i;
+ // mark the fanins of the cone
+ Abc_NodesMark( vLeaves );
+ // collect the nodes in the DFS order
+ Vec_PtrClear( vVisited );
+ // add the fanins
+ if ( fIncludeFanins )
+ Vec_PtrForEachEntry( vLeaves, pTemp, i )
+ Vec_PtrPush( vVisited, pTemp );
+ // add other nodes
+ for ( i = 0; i < nRoots; i++ )
+ Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
+ // unmark both sets
+ Abc_NodesUnmark( vLeaves );
+ Abc_NodesUnmark( vVisited );
+}
+
+/**Function*************************************************************
+
Synopsis [Marks the TFI cone.]
Description []
@@ -273,22 +464,21 @@ int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
SeeAlso []
***********************************************************************/
-void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
{
if ( pNode->fMarkA == 1 )
return;
// visit transitive fanin
if ( Abc_ObjIsNode(pNode) )
{
- Abc_NodesMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
- Abc_NodesMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+ Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+ Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
}
assert( pNode->fMarkA == 0 );
pNode->fMarkA = 1;
Vec_PtrPush( vVisited, pNode );
}
-
/**Function*************************************************************
Synopsis [Returns BDD representing the logic function of the cone.]
@@ -300,20 +490,14 @@ void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
SeeAlso []
***********************************************************************/
-DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
{
DdNode * bFunc0, * bFunc1, * bFunc;
int i;
- // mark the fanins of the cone
- Abc_NodesMark( vFanins );
- // collect the nodes in the DFS order
- Vec_PtrClear( vVisited );
- Abc_NodesMarkCollect_rec( pNode, vVisited );
- // unmark both sets
- Abc_NodesUnmark( vFanins );
- Abc_NodesUnmark( vVisited );
+ // get the nodes in the cut without fanins in the DFS order
+ Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 );
// set the elementary BDDs
- Vec_PtrForEachEntry( vFanins, pNode, i )
+ Vec_PtrForEachEntry( vLeaves, pNode, i )
pNode->pCopy = (Abc_Obj_t *)pbVars[i];
// compute the BDDs for the collected nodes
Vec_PtrForEachEntry( vVisited, pNode, i )
@@ -347,15 +531,8 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
Abc_Obj_t * pNode;
int i;
- // mark the fanins of the cone
- Abc_NodesMark( vLeaves );
- // collect the nodes in the DFS order
- Vec_PtrClear( vVisited );
- Vec_PtrForEachEntry( vRoots, pNode, i )
- Abc_NodesMarkCollect_rec( pNode, vVisited );
- // unmark both sets
- Abc_NodesUnmark( vLeaves );
- Abc_NodesUnmark( vVisited );
+ // get the nodes in the cut without fanins in the DFS order
+ Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
// set the elementary BDDs
Vec_PtrForEachEntry( vLeaves, pNode, i )
pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
@@ -400,16 +577,20 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
SeeAlso []
***********************************************************************/
-Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
+Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
{
Abc_ManCut_t * p;
p = ALLOC( Abc_ManCut_t, 1 );
memset( p, 0, sizeof(Abc_ManCut_t) );
- p->vFaninsNode = Vec_PtrAlloc( 100 );
- p->vFaninsCone = Vec_PtrAlloc( 100 );
+ p->vNodeLeaves = Vec_PtrAlloc( 100 );
+ p->vConeLeaves = Vec_PtrAlloc( 100 );
p->vVisited = Vec_PtrAlloc( 100 );
+ p->vLevels = Vec_VecAlloc( 100 );
+ p->vNodesTfo = Vec_PtrAlloc( 100 );
p->nNodeSizeMax = nNodeSizeMax;
p->nConeSizeMax = nConeSizeMax;
+ p->nNodeFanStop = nNodeFanStop;
+ p->nConeFanStop = nConeFanStop;
return p;
}
@@ -426,9 +607,11 @@ Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
***********************************************************************/
void Abc_NtkManCutStop( Abc_ManCut_t * p )
{
- Vec_PtrFree( p->vFaninsNode );
- Vec_PtrFree( p->vFaninsCone );
+ Vec_PtrFree( p->vNodeLeaves );
+ Vec_PtrFree( p->vConeLeaves );
Vec_PtrFree( p->vVisited );
+ Vec_VecFree( p->vLevels );
+ Vec_PtrFree( p->vNodesTfo );
free( p );
}
@@ -443,9 +626,25 @@ void Abc_NtkManCutStop( Abc_ManCut_t * p )
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
+Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
+{
+ return p->vConeLeaves;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the leaves of the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
{
- return p->vFaninsCone;
+ return p->vVisited;
}
@@ -466,27 +665,27 @@ Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
SeeAlso []
***********************************************************************/
-void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
- Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult )
+Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
{
+ Abc_Ntk_t * pNtk = pRoot->pNtk;
Vec_Ptr_t * vVec;
Abc_Obj_t * pNode, * pFanout;
int i, k, v, LevelMin;
assert( Abc_NtkIsStrash(pNtk) );
// assuming that the structure is clean
- Vec_VecForEachLevel( vLevels, vVec, i )
+ Vec_VecForEachLevel( p->vLevels, vVec, i )
assert( vVec->nSize == 0 );
// put fanins into the structure while labeling them
Abc_NtkIncrementTravId( pNtk );
- LevelMin = ABC_INFINITY;
- Vec_PtrForEachEntry( vFanins, pNode, i )
+ LevelMin = -1;
+ Vec_PtrForEachEntry( vLeaves, pNode, i )
{
if ( pNode->Level > (unsigned)LevelMax )
continue;
Abc_NodeSetTravIdCurrent( pNode );
- Vec_VecPush( vLevels, pNode->Level, pNode );
+ Vec_VecPush( p->vLevels, pNode->Level, pNode );
if ( LevelMin < (int)pNode->Level )
LevelMin = pNode->Level;
}
@@ -497,9 +696,11 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
Abc_NodeMffcLabel( pRoot );
// go through the levels up
- Vec_PtrClear( vResult );
- Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax )
+ Vec_PtrClear( p->vNodesTfo );
+ Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin )
{
+ if ( i > LevelMax )
+ break;
// if the node is not marked, it is not a fanin
if ( !Abc_NodeIsTravIdCurrent(pNode) )
{
@@ -508,7 +709,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
!Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
continue;
// save the node in the TFO and label it
- Vec_PtrPush( vResult, pNode );
+ Vec_PtrPush( p->vNodesTfo, pNode );
Abc_NodeSetTravIdCurrent( pNode );
}
// go through the fanouts and add them to the structure if they meet the conditions
@@ -521,13 +722,18 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue;
// add it to the structure but do not mark it (until tested later)
- Vec_VecPush( vLevels, pFanout->Level, pFanout );
+ Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
}
}
// clear the levelized structure
- Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax )
+ Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
+ {
+ if ( i > LevelMax )
+ break;
Vec_PtrClear( vVec );
+ }
+ return p->vNodesTfo;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 7e387b47..9a413bb1 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -96,9 +96,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
assert( Abc_NtkIsStrash(pNtk) );
// start the managers
- pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
+ pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
- pManRef->vLeaves = Abc_NtkManCutReadLeaves( pManCut );
+ pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut );
Abc_NtkStartReverseLevels( pNtk );
// resynthesize each node once
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 081ccfaa..dfcc3ae5 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -174,6 +174,10 @@ void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm,
// create the new structure of nodes
assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm );
+ // in some cases, the new node may have a minor redundancy
+ // (has to do with the precomputed subgraph library)
+ if ( !Abc_AigNodeIsAcyclic( Abc_ObjRegular(pNodeNew), pNode ) )
+ return;
// remove the old nodes
Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew );
// compare the gains
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 730aca90..38840de0 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -18,22 +18,27 @@
***********************************************************************/
-#include "abc.h"
#ifdef WIN32
-#include "process.h"
+#include <process.h>
#endif
+#include "abc.h"
+#include "io.h"
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-
+
+static void Abc_ShowFile( char * FileNameDot );
+static void Abc_ShowGetFileName( char * pName, char * pBuffer );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Prints the factored form of one node.]
+ Synopsis [Visualizes BDD of the node.]
Description []
@@ -42,15 +47,152 @@
SeeAlso []
***********************************************************************/
-void Abc_NodePrintBdd( Abc_Obj_t * pNode )
+void Abc_NodeShowBdd( Abc_Obj_t * pNode )
{
FILE * pFile;
Vec_Ptr_t * vNamesIn;
- char * FileNameIn;
- char * FileNameOut;
- char * FileGeneric;
- char * pCur, * pNameOut;
char FileNameDot[200];
+ char * pNameOut;
+
+ assert( Abc_NtkIsBddLogic(pNode->pNtk) );
+ // create the file names
+ Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
+ // check that the file can be opened
+ if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+ return;
+ }
+
+ // set the node names
+ vNamesIn = Abc_NodeGetFaninNames( pNode );
+ pNameOut = Abc_ObjName(pNode);
+ Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
+ Abc_NodeFreeFaninNames( vNamesIn );
+ Abc_NtkCleanCopy( pNode->pNtk );
+ fclose( pFile );
+
+ // visualize the file
+ Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Visualizes AIG with choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
+{
+ FILE * pFile;
+ Abc_Obj_t * pNode;
+ Vec_Ptr_t * vNodes;
+ char FileNameDot[200];
+ int i;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // create the file names
+ Abc_ShowGetFileName( pNtk->pName, FileNameDot );
+ // check that the file can be opened
+ if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+ return;
+ }
+
+ // collect all nodes in the network
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ Vec_PtrPush( vNodes, pNode );
+ // write the DOT file
+ Io_WriteDot( pNtk, vNodes, NULL, FileNameDot );
+ Vec_PtrFree( vNodes );
+
+ // visualize the file
+ Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Visualizes reconvergence driven cut at the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
+{
+ FILE * pFile;
+ char FileNameDot[200];
+ Abc_ManCut_t * p;
+ Vec_Ptr_t * vCutSmall;
+ Vec_Ptr_t * vCutLarge;
+ Vec_Ptr_t * vInside;
+ Vec_Ptr_t * vNodesTfo;
+ Abc_Obj_t * pTemp;
+ int i;
+
+ assert( Abc_NtkIsStrash(pNode->pNtk) );
+
+ // start the cut computation manager
+ p = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, ABC_INFINITY );
+ // get the recovergence driven cut
+ vCutSmall = Abc_NodeFindCut( p, pNode, 1 );
+ // get the containing cut
+ vCutLarge = Abc_NtkManCutReadCutLarge( p );
+ // get the array for the inside nodes
+ vInside = Abc_NtkManCutReadVisited( p );
+ // get the inside nodes of the containing cone
+ Abc_NodeConeCollect( &pNode, 1, vCutLarge, vInside, 1 );
+
+ // add the nodes in the TFO
+ vNodesTfo = Abc_NodeCollectTfoCands( p, pNode, vCutSmall, ABC_INFINITY );
+ Vec_PtrForEachEntry( vNodesTfo, pTemp, i )
+ Vec_PtrPushUnique( vInside, pTemp );
+
+ // create the file names
+ Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
+ // check that the file can be opened
+ if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+ return;
+ }
+ // add the root node to the cone (for visualization)
+ Vec_PtrPush( vCutSmall, pNode );
+ // write the DOT file
+ Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot );
+ // stop the cut computation manager
+ Abc_NtkManCutStop( p );
+
+ // visualize the file
+ Abc_ShowFile( FileNameDot );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Shows the given DOT file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_ShowFile( char * FileNameDot )
+{
+ FILE * pFile;
+ char * FileGeneric;
char FileNamePs[200];
char CommandDot[1000];
#ifndef WIN32
@@ -60,8 +202,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
char * pProgGsViewName;
int RetValue;
- assert( Abc_NtkIsBddLogic(pNode->pNtk) );
-
#ifdef WIN32
pProgDotName = "dot.exe";
pProgGsViewName = NULL;
@@ -70,34 +210,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
pProgGsViewName = "gv";
#endif
- FileNameIn = NULL;
- FileNameOut = NULL;
-
- // get the generic file name
- pNode->pCopy = NULL;
- FileGeneric = Abc_ObjName(pNode);
- // get rid of not-alpha-numeric characters
- for ( pCur = FileGeneric; *pCur; pCur++ )
- if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) )
- *pCur = '_';
- // create the file names
- sprintf( FileNameDot, "%s.dot", FileGeneric );
- sprintf( FileNamePs, "%s.ps", FileGeneric );
-
- // write the DOT file
- if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
- {
- fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
- return;
- }
- // set the node names
- vNamesIn = Abc_NodeGetFaninNames( pNode );
- pNameOut = Abc_ObjName(pNode);
- Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
- Abc_NodeFreeFaninNames( vNamesIn );
- Abc_NtkCleanCopy( pNode->pNtk );
- fclose( pFile );
-
// check that the input file is okay
if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
{
@@ -106,6 +218,12 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
}
fclose( pFile );
+ // get the generic file name
+ FileGeneric = Extra_FileNameGeneric( FileNameDot );
+ // create the PostScript file name
+ sprintf( FileNamePs, "%s.ps", FileGeneric );
+ free( FileGeneric );
+
// generate the DOT file
sprintf( CommandDot, "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot );
RetValue = system( CommandDot );
@@ -146,10 +264,9 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
#endif
}
-
/**Function*************************************************************
- Synopsis []
+ Synopsis [Derives the DOT file name.]
Description []
@@ -158,6 +275,18 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
+void Abc_ShowGetFileName( char * pName, char * pBuffer )
+{
+ char * pCur;
+ // creat the file name
+ sprintf( pBuffer, "%s.dot", pName );
+ // get rid of not-alpha-numeric characters
+ for ( pCur = pBuffer; *pCur; pCur++ )
+ if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') ||
+ (*pCur >= 'A' && *pCur <= 'Z') || (*pCur == '.')) )
+ *pCur = '_';
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 19394fb3..0a28c3c1 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -49,7 +49,7 @@ extern char * Mio_GateReadSop( void * pGate );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
+Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
{
int fCheck = 1;
Abc_Ntk_t * pNtkAig;
@@ -68,11 +68,11 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
// print warning about self-feed latches
if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
- if ( nNodes = Abc_AigCleanup(pNtkAig->pManFunc) )
+ if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
printf( "Cleanup has removed %d nodes.\n", nNodes );
// duplicate EXDC
if ( pNtk->pExdc )
- pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
+ pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
// make sure everything is okay
if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
{
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 47565241..61d65ce3 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
assert( !Abc_NtkIsStrash(pNtk) );
// derive the AIG
- pNtkAig = Abc_NtkStrash( pNtk, 0 );
+ pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
// perform fraiging of the AIG
Fraig_ParamsSetDefault( &Params );
pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );
diff --git a/src/base/abc/abcSymm.c b/src/base/abc/abcSymm.c
new file mode 100644
index 00000000..8df3a837
--- /dev/null
+++ b/src/base/abc/abcSymm.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+ FileName [abcSymm.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Computation of two-variable symmetries.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcSymm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [The top level procedure to compute symmetries.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
+{
+ if ( fUseBdds || fNaive )
+ Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
+ else
+ printf( "This option is currently not implemented.\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Symmetry computation using BDDs (both naive and smart).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
+{
+ DdManager * dd;
+ int clk, clkBdd, clkSym;
+
+ // compute the global functions
+clk = clock();
+ dd = Abc_NtkGlobalBdds( pNtk, 0 );
+ Cudd_AutodynDisable( dd );
+ Cudd_zddVarsFromBddVars( dd, 2 );
+clkBdd = clock() - clk;
+ // create the collapsed network
+clk = clock();
+ Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose );
+clkSym = clock() - clk;
+ // undo the global functions
+ Abc_NtkFreeGlobalBdds( pNtk );
+ Extra_StopManager( dd );
+ pNtk->pManGlob = NULL;
+
+PRT( "Constructing BDDs", clkBdd );
+PRT( "Computing symms ", clkSym );
+PRT( "TOTAL ", clkBdd + clkSym );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Symmetry computation using BDDs (both naive and smart).]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
+{
+ Extra_SymmInfo_t * pSymms;
+ Abc_Obj_t * pNode;
+ DdNode * bFunc;
+ int nSymms = 0;
+ int i;
+
+ // compute symmetry info for each PO
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ bFunc = pNtk->vFuncsGlob->pArray[i];
+ if ( Cudd_IsConstant(bFunc) )
+ continue;
+ if ( fNaive )
+ pSymms = Extra_SymmPairsComputeNaive( dd, bFunc );
+ else
+ pSymms = Extra_SymmPairsCompute( dd, bFunc );
+ nSymms += pSymms->nSymms;
+ if ( fVerbose )
+ {
+ printf( "Output %6s (%d): ", Abc_ObjName(pNode), pSymms->nSymms );
+ Ntk_NetworkSymmsPrint( pNtk, pSymms );
+ }
+//Extra_SymmPairsPrint( pSymms );
+ Extra_SymmPairsDissolve( pSymms );
+ }
+ printf( "The total number of symmetries is %d.\n", nSymms );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Printing symmetry groups from the symmetry data structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
+{
+ char ** pInputNames;
+ int * pVarTaken;
+ int i, k, nVars, nSize, fStart;
+
+ // get variable names
+ nVars = Abc_NtkCiNum(pNtk);
+ pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
+
+ // alloc the array of marks
+ pVarTaken = ALLOC( int, nVars );
+ memset( pVarTaken, 0, sizeof(int) * nVars );
+
+ // print the groups
+ fStart = 1;
+ nSize = pSymms->nVars;
+ for ( i = 0; i < nSize; i++ )
+ {
+ // skip the variable already considered
+ if ( pVarTaken[i] )
+ continue;
+ // find all the vars symmetric with this one
+ for ( k = 0; k < nSize; k++ )
+ {
+ if ( k == i )
+ continue;
+ if ( pSymms->pSymms[i][k] == 0 )
+ continue;
+ // vars i and k are symmetric
+ assert( pVarTaken[k] == 0 );
+ // there is a new symmetry pair
+ if ( fStart == 1 )
+ { // start a new symmetry class
+ fStart = 0;
+ printf( " { %s", pInputNames[ pSymms->pVars[i] ] );
+ // mark the var as taken
+ pVarTaken[i] = 1;
+ }
+ printf( " %s", pInputNames[ pSymms->pVars[k] ] );
+ // mark the var as taken
+ pVarTaken[k] = 1;
+ }
+ if ( fStart == 0 )
+ {
+ printf( " }" );
+ fStart = 1;
+ }
+ }
+ printf( "\n" );
+
+ free( pInputNames );
+ free( pVarTaken );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
index 04e5c96c..0fe3ec63 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abc/abcUnreach.c
@@ -91,6 +91,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
Cudd_RecursiveDeref( dd, bUnreach );
Extra_StopManager( dd );
+ pNtk->pManGlob = NULL;
// make sure that everything is okay
if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
@@ -135,13 +136,13 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
Abc_NtkForEachLatch( pNtk, pNode, i )
{
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
- bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext ); Cudd_Ref( bProd );
- bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
+ bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] ); Cudd_Ref( bProd );
+ bRel = Cudd_bddAnd( dd, bTemp = bRel, bProd ); Cudd_Ref( bRel );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
// free the global BDDs
- Abc_NtkFreeGlobalBdds( dd, pNtk );
+ Abc_NtkFreeGlobalBdds( pNtk );
// quantify the PI variables
bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) ); Cudd_Ref( bInputs );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 7d2ca107..9a2acc32 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1046,6 +1046,29 @@ Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
return vFanNums;
}
+/**Function*************************************************************
+
+ Synopsis [Collects all objects into one array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pNode;
+ int i;
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ Vec_PtrPush( vNodes, pNode );
+ return vNodes;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index d9bed264..d3d4091b 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -32,6 +32,7 @@ SRC += src/base/abc/abc.c \
src/base/abc/abcSop.c \
src/base/abc/abcStrash.c \
src/base/abc/abcSweep.c \
+ src/base/abc/abcSymm.c \
src/base/abc/abcTiming.c \
src/base/abc/abcUnreach.c \
src/base/abc/abcUtil.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 9ffbc3cf..89703214 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -29,12 +29,16 @@ static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
////////////////////////////////////////////////////////////////////////
@@ -58,12 +62,16 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
}
@@ -127,7 +135,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -199,7 +207,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -280,7 +288,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -360,7 +368,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -406,6 +414,86 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk, * pTemp;
+ char * FileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+
+ // set the new network
+ pNtk = Io_ReadEqn( FileName, fCheck );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Reading network from the equation file has failed.\n" );
+ return 1;
+ }
+
+ pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+ Abc_NtkDelete( pTemp );
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in equation format\n" );
+ fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+ fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
+ fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pTemp;
@@ -440,7 +528,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -451,7 +539,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtk = Io_ReadVerilog( FileName, fCheck );
if ( pNtk == NULL )
{
- fprintf( pAbc->Err, "Reading network from Verilog file has failed.\n" );
+ fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
return 1;
}
@@ -520,7 +608,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+ if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
@@ -764,6 +852,199 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * FileName;
+ Vec_Ptr_t * vNodes;
+ int c;
+
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pNtkCur == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
+ {
+ fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
+ Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName );
+ Vec_PtrFree( vNodes );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the AIG into a DOT file\n" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ Abc_Ntk_t * pNtk, * pNtkTemp;
+ char * FileName;
+ int c;
+
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ pNtk = pAbc->pNtkCur;
+ if ( pNtk == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
+ return 0;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ // get rid of complemented covers if present
+ if ( Abc_NtkIsSopLogic(pNtk) )
+ Abc_NtkLogicMakeDirectSops(pNtk);
+ // derive the netlist
+ pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+ if ( pNtkTemp == NULL )
+ {
+ fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
+ return 0;
+ }
+ Io_WriteEqn( pNtkTemp, FileName );
+ Abc_NtkDelete( pNtkTemp );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the current network in the equation format\n" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * FileName;
+ int c;
+
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pAbc->pNtkCur == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsLogic(pAbc->pNtkCur) && !Abc_NtkIsStrash(pAbc->pNtkCur) )
+ {
+ fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
+ return 0;
+ }
+
+ if ( argc != util_optind + 1 )
+ {
+ goto usage;
+ }
+
+ // get the input file name
+ FileName = argv[util_optind];
+ // write the file
+ Io_WriteGml( pAbc->pNtkCur, FileName );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write network using graph representation formal GML\n" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk, * pNtkTemp;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index d45b7b1b..6bf3a85c 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -53,6 +53,8 @@ extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
extern Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck );
/*=== abcReadEdif.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck );
+/*=== abcReadEqn.c ==========================================================*/
+extern Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck );
/*=== abcReadVerilog.c ==========================================================*/
extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
/*=== abcReadPla.c ==========================================================*/
@@ -73,6 +75,12 @@ extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteCnf.c ==========================================================*/
extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteDot.c ==========================================================*/
+extern void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName );
+/*=== abcWriteEqn.c ==========================================================*/
+extern void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
+/*=== abcWriteGml.c ==========================================================*/
+extern void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWritePla.c ==========================================================*/
extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 75c87a80..acf4deda 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -53,6 +53,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
pNtk = Io_ReadEdif( pFileName, fCheck );
else if ( Extra_FileNameCheckExtension( pFileName, "pla" ) )
pNtk = Io_ReadPla( pFileName, fCheck );
+ else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) )
+ pNtk = Io_ReadEqn( pFileName, fCheck );
else
{
fprintf( stderr, "Unknown file format\n" );
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
new file mode 100644
index 00000000..54890729
--- /dev/null
+++ b/src/base/io/ioReadEqn.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+ FileName [ioReadEqn.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read equation format files.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p );
+static void Io_ReadEqnStrCompact( char * pStr );
+static int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName );
+static void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Reads the network from a BENCH file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck )
+{
+ Extra_FileReader_t * p;
+ Abc_Ntk_t * pNtk;
+
+ // start the file
+ p = Extra_FileReaderAlloc( pFileName, "#", ";", "=" );
+ if ( p == NULL )
+ return NULL;
+
+ // read the network
+ pNtk = Io_ReadEqnNetwork( p );
+ Extra_FileReaderFree( p );
+ if ( pNtk == NULL )
+ return NULL;
+
+ // make sure that everything is okay with the network structure
+ if ( fCheck && !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Io_ReadEqn: The network check has failed.\n" );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+ return pNtk;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
+{
+ ProgressBar * pProgress;
+ Vec_Ptr_t * vTokens;
+ Vec_Ptr_t * vCubes, * vLits, * vVars;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pNode;
+ char * pCubesCopy, * pSopCube, * pVarName;
+ int iLine, iNum, i, k;
+
+ // allocate the empty network
+ pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
+
+ // go through the lines of the file
+ vCubes = Vec_PtrAlloc( 100 );
+ vVars = Vec_PtrAlloc( 100 );
+ vLits = Vec_PtrAlloc( 100 );
+ pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
+ for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+ {
+ Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
+
+ // check if the first token contains anything
+ Io_ReadEqnStrCompact( vTokens->pArray[0] );
+ if ( strlen(vTokens->pArray[0]) == 0 )
+ break;
+
+ // if the number of tokens is different from two, error
+ if ( vTokens->nSize != 2 )
+ {
+ printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
+ Abc_NtkDelete( pNtk );
+ return NULL;
+ }
+
+ // get the type of the line
+ if ( strncmp( vTokens->pArray[0], "INORDER", 7 ) == 0 )
+ {
+ Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
+ Vec_PtrForEachEntry( vVars, pVarName, i )
+ Io_ReadCreatePi( pNtk, pVarName );
+ }
+ else if ( strncmp( vTokens->pArray[0], "OUTORDER", 8 ) == 0 )
+ {
+ Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
+ Vec_PtrForEachEntry( vVars, pVarName, i )
+ Io_ReadCreatePo( pNtk, pVarName );
+ }
+ else
+ {
+ // remove spaces
+ pCubesCopy = vTokens->pArray[1];
+ Io_ReadEqnStrCompact( pCubesCopy );
+ // consider the case of the constant node
+ if ( (pCubesCopy[0] == '0' || pCubesCopy[0] == '1') && pCubesCopy[1] == 0 )
+ {
+ pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], NULL, 0 );
+ if ( pCubesCopy[0] == '0' )
+ pNode->pData = Abc_SopCreateConst0( pNtk->pManFunc );
+ else
+ pNode->pData = Abc_SopCreateConst1( pNtk->pManFunc );
+ continue;
+ }
+ // determine unique variables
+ pCubesCopy = util_strsav( pCubesCopy );
+ // find the names of the fanins of this node
+ Io_ReadEqnStrCutAt( pCubesCopy, "!*+", 1, vVars );
+ // create the node
+ pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], (char **)vVars->pArray, vVars->nSize );
+ // split the string into cubes
+ Io_ReadEqnStrCutAt( vTokens->pArray[1], "+", 0, vCubes );
+ // start the sop
+ pNode->pData = Abc_SopStart( pNtk->pManFunc, vCubes->nSize, vVars->nSize );
+ // read the cubes
+ i = 0;
+ Abc_SopForEachCube( pNode->pData, vVars->nSize, pSopCube )
+ {
+ // split this cube into lits
+ Io_ReadEqnStrCutAt( vCubes->pArray[i], "*", 0, vLits );
+ // read the literals
+ Vec_PtrForEachEntry( vLits, pVarName, k )
+ {
+ iNum = Io_ReadEqnStrFind( vVars, pVarName + (pVarName[0] == '!') );
+ assert( iNum >= 0 );
+ pSopCube[iNum] = '1' - (pVarName[0] == '!');
+ }
+ i++;
+ }
+ assert( i == vCubes->nSize );
+ // remove the cubes
+ free( pCubesCopy );
+ }
+ }
+ Extra_ProgressBarStop( pProgress );
+ Vec_PtrFree( vCubes );
+ Vec_PtrFree( vLits );
+ Vec_PtrFree( vVars );
+ Abc_NtkFinalizeRead( pNtk );
+ return pNtk;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Compacts the string by throwing away space-like chars.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadEqnStrCompact( char * pStr )
+{
+ char * pCur, * pNew;
+ for ( pNew = pCur = pStr; *pCur; pCur++ )
+ if ( !(*pCur == ' ' || *pCur == '\n' || *pCur == '\r' || *pCur == '\t') )
+ *pNew++ = *pCur;
+ *pNew = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Determines unique variables in the string.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName )
+{
+ char * pToken;
+ int i;
+ Vec_PtrForEachEntry( vTokens, pToken, i )
+ if ( strcmp( pToken, pName ) == 0 )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cuts the string into pieces using stop chars.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens )
+{
+ char * pToken;
+ Vec_PtrClear( vTokens );
+ for ( pToken = strtok( pStr, pStop ); pToken; pToken = strtok( NULL, pStop ) )
+ if ( !fUniqueOnly || Io_ReadEqnStrFind( vTokens, pToken ) == -1 )
+ Vec_PtrPush( vTokens, pToken );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 5135105f..7d6815b9 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -107,10 +107,7 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
Synopsis [Write one network.]
- Description [Writes a network composed of PIs, POs, internal nodes,
- and latches. The following rules are used to print the names of
- internal nodes:
- ]
+ Description []
SideEffects []
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index bb216bb6..09824f38 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -6,7 +6,7 @@
PackageName [Command processing package.]
- Synopsis [Procedures to CNF of the miter cone.]
+ Synopsis [Procedures to output CNF of the miter cone.]
Author [Alan Mishchenko]
@@ -24,8 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
new file mode 100644
index 00000000..7d88e52d
--- /dev/null
+++ b/src/base/io/ioWriteDot.c
@@ -0,0 +1,322 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteDot.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write the graph structure of AIG in DOT.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the graph structure of AIG in DOT.]
+
+ Description [Useful for graph visualization using tools such as GraphViz:
+ http://www.graphviz.org/]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName )
+{
+ FILE * pFile;
+ Abc_Obj_t * pNode, * pTemp, * pPrev;
+ int LevelMin, LevelMax, fHasCos, Level, i;
+ int Limit = 200;
+
+ if ( vNodes->nSize < 1 )
+ {
+ printf( "The set has no nodes. DOT file is not written.\n" );
+ return;
+ }
+
+ if ( vNodes->nSize > Limit )
+ {
+ printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
+ return;
+ }
+
+ // start the stream
+ if ( (pFile = fopen( pFileName, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+ return;
+ }
+
+ // mark the nodes from the set
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ pNode->fMarkC = 1;
+ if ( vNodesShow )
+ Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ pNode->fMarkB = 1;
+
+ // find the largest and the smallest levels
+ LevelMin = 10000;
+ LevelMax = -1;
+ fHasCos = 0;
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( Abc_ObjIsCo(pNode) )
+ {
+ fHasCos = 1;
+ continue;
+ }
+ if ( LevelMin > (int)pNode->Level )
+ LevelMin = pNode->Level;
+ if ( LevelMax < (int)pNode->Level )
+ LevelMax = pNode->Level;
+ }
+
+ // set the level of the CO nodes
+ if ( fHasCos )
+ {
+ LevelMax++;
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( Abc_ObjIsCo(pNode) )
+ pNode->Level = LevelMax;
+ }
+ }
+
+ // write the DOT header
+ fprintf( pFile, "# %s\n", "AIG generated by ABC" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "digraph AIG {\n" );
+ fprintf( pFile, "size = \"7.5,10\";\n" );
+// fprintf( pFile, "ranksep = 0.5;\n" );
+// fprintf( pFile, "nodesep = 0.5;\n" );
+ fprintf( pFile, "center = true;\n" );
+// fprintf( pFile, "edge [fontsize = 10];\n" );
+// fprintf( pFile, "edge [dir = none];\n" );
+ fprintf( pFile, "\n" );
+
+ // labels on the left of the picture
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " node [shape = plaintext];\n" );
+ fprintf( pFile, " edge [style = invis];\n" );
+ fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
+ fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
+ // generate node names with labels
+ for ( Level = LevelMax; Level >= LevelMin; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ fprintf( pFile, " [label = " );
+ // label name
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "];\n" );
+ }
+
+ // genetate the sequence of visible/invisible nodes to mark levels
+ fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
+ for ( Level = LevelMax; Level >= LevelMin; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ // the connector
+ if ( Level != LevelMin )
+ fprintf( pFile, " ->" );
+ else
+ fprintf( pFile, ";" );
+ }
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate title box on top
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle1;\n" );
+ fprintf( pFile, " title1 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=20,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "%s", "AIG generated by ABC" );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
+ fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate statistics box
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle2;\n" );
+ fprintf( pFile, " title2 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=18,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate the POs
+ if ( fHasCos )
+ {
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", LevelMax );
+ // generat the PO nodes
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( !Abc_ObjIsCo(pNode) )
+ continue;
+ fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
+ fprintf( pFile, ", shape = invtriangle" );
+ if ( pNode->fMarkB )
+ fprintf( pFile, ", style = filled" );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ }
+
+ // generate nodes of each rank
+ for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
+ {
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", Level );
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( (int)pNode->Level != Level )
+ continue;
+ fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
+ fprintf( pFile, ", shape = ellipse" );
+ if ( pNode->fMarkB )
+ fprintf( pFile, ", style = filled" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ }
+
+ // generate the PI nodes if any
+ if ( LevelMin == 0 )
+ {
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", LevelMin );
+ // generat the PO nodes
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( !Abc_ObjIsCi(pNode) )
+ continue;
+ fprintf( pFile, " Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
+ fprintf( pFile, ", shape = triangle" );
+ if ( pNode->fMarkB )
+ fprintf( pFile, ", style = filled" );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ }
+
+ // generate invisible edges from the square down
+ fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( (int)pNode->Level != LevelMax )
+ continue;
+ fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
+ }
+
+ // generate edges
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ if ( Abc_ObjFaninNum(pNode) == 0 )
+ continue;
+ // generate the edge from this node to the next
+ if ( Abc_ObjFanin0(pNode)->fMarkC )
+ {
+ fprintf( pFile, "Node%d", pNode->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", Abc_ObjFaninId0(pNode) );
+ fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" );
+ fprintf( pFile, ";\n" );
+ }
+ if ( Abc_ObjFaninNum(pNode) == 1 )
+ continue;
+ // generate the edge from this node to the next
+ if ( Abc_ObjFanin1(pNode)->fMarkC )
+ {
+ fprintf( pFile, "Node%d", pNode->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", Abc_ObjFaninId1(pNode) );
+ fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" );
+ fprintf( pFile, ";\n" );
+ }
+ // generate the edges between the equivalent nodes
+ pPrev = pNode;
+ for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
+ {
+ if ( pTemp->fMarkC )
+ {
+ fprintf( pFile, "Node%d", pPrev->Id );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", pTemp->Id );
+ fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" );
+ fprintf( pFile, ";\n" );
+ pPrev = pTemp;
+ }
+ }
+ }
+
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+
+ // unmark the nodes from the set
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ pNode->fMarkC = 0;
+ if ( vNodesShow )
+ Vec_PtrForEachEntry( vNodesShow, pNode, i )
+ pNode->fMarkB = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c
new file mode 100644
index 00000000..6c2893b5
--- /dev/null
+++ b/src/base/io/ioWriteEqn.c
@@ -0,0 +1,261 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteEqn.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write equation representation of the network.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the logic network in the equation format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ FILE * pFile;
+
+ assert( Abc_NtkIsSopNetlist(pNtk) );
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ printf( "Warning: only combinational portion is being written.\n" );
+
+ // start the output stream
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteEqn(): Cannot open the output file \"%s\".\n", pFileName );
+ return;
+ }
+ fprintf( pFile, "# Equations for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+
+ // write the equations for the network
+ Io_NtkWriteEqnOne( pFile, pNtk );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write one network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ ProgressBar * pProgress;
+ Abc_Obj_t * pNode;
+ int i;
+
+ // write the PIs
+ fprintf( pFile, "INORDER =" );
+ Io_NtkWriteEqnPis( pFile, pNtk );
+ fprintf( pFile, ";\n" );
+
+ // write the POs
+ fprintf( pFile, "OUTORDER =" );
+ Io_NtkWriteEqnPos( pFile, pNtk );
+ fprintf( pFile, ";\n" );
+
+ // write each internal node
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Io_NtkWriteEqnNode( pFile, pNode );
+ }
+ Extra_ProgressBarStop( pProgress );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pTerm, * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int i;
+
+ LineLength = 9;
+ NameCounter = 0;
+
+ Abc_NtkForEachCi( pNtk, pTerm, i )
+ {
+ pNet = Abc_ObjFanout0(pTerm);
+ // get the line length after this name is written
+ AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", Abc_ObjName(pNet) );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the primary input list.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pTerm, * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ int i;
+
+ LineLength = 10;
+ NameCounter = 0;
+
+ Abc_NtkForEachCo( pNtk, pTerm, i )
+ {
+ pNet = Abc_ObjFanin0(pTerm);
+ // get the line length after this name is written
+ AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+ if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \n" );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, " %s", Abc_ObjName(pNet) );
+ LineLength += AddedLength;
+ NameCounter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Write the node into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pNet;
+ int LineLength;
+ int AddedLength;
+ int NameCounter;
+ char * pCube;
+ int Value, fFirstLit, i;
+
+ fprintf( pFile, "%s = ", Abc_ObjName(pNode) );
+
+ if ( Abc_SopIsConst0(pNode->pData) )
+ {
+ fprintf( pFile, "0;\n" );
+ return;
+ }
+ if ( Abc_SopIsConst1(pNode->pData) )
+ {
+ fprintf( pFile, "1;\n" );
+ return;
+ }
+
+ NameCounter = 0;
+ LineLength = strlen(Abc_ObjName(pNode)) + 3;
+ Abc_SopForEachCube( pNode->pData, Abc_ObjFaninNum(pNode), pCube )
+ {
+ if ( pCube != pNode->pData )
+ {
+ fprintf( pFile, " + " );
+ LineLength += 3;
+ }
+
+ // add the cube
+ fFirstLit = 1;
+ Abc_CubeForEachVar( pCube, Value, i )
+ {
+ if ( Value == '-' )
+ continue;
+ pNet = Abc_ObjFanin( pNode, i );
+ // get the line length after this name is written
+ AddedLength = !fFirstLit + (Value == '0') + strlen(Abc_ObjName(pNet));
+ if ( NameCounter && LineLength + AddedLength + 6 > IO_WRITE_LINE_LENGTH )
+ { // write the line extender
+ fprintf( pFile, " \n " );
+ // reset the line length
+ LineLength = 0;
+ NameCounter = 0;
+ }
+ fprintf( pFile, "%s%s%s", (fFirstLit? "": "*"), ((Value == '0')? "!":""), Abc_ObjName(pNet) );
+ LineLength += AddedLength;
+ NameCounter++;
+ fFirstLit = 0;
+ }
+ }
+ fprintf( pFile, ";\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c
new file mode 100644
index 00000000..ab9f1143
--- /dev/null
+++ b/src/base/io/ioWriteGml.c
@@ -0,0 +1,116 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteGml.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write the graph structure of AIG in GML.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteGml.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the graph structure of AIG in GML.]
+
+ Description [Useful for graph visualization using tools such as yEd:
+ http://www.yworks.com/]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ FILE * pFile;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k;
+
+ assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
+
+ // start the output stream
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "Io_WriteGml(): Cannot open the output file \"%s\".\n", pFileName );
+ return;
+ }
+ fprintf( pFile, "# GML for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+ fprintf( pFile, "graph [\n" );
+
+ // output the POs
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+ fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FFFF\" ]\n" ); // blue
+ fprintf( pFile, " ]\n" );
+ }
+ // output the PIs
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+ fprintf( pFile, " graphics [ type \"triangle\" fill \"#00FF00\" ]\n" ); // green
+ fprintf( pFile, " ]\n" );
+ }
+ // output the latches
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ {
+ fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+ fprintf( pFile, " graphics [ type \"rectangle\" fill \"#FF0000\" ]\n" ); // red
+ fprintf( pFile, " ]\n" );
+ }
+ // output the nodes
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ fprintf( pFile, " node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+ fprintf( pFile, " graphics [ type \"ellipse\" fill \"#CCCCFF\" ]\n" ); // grey
+ fprintf( pFile, " ]\n" );
+ }
+
+ // output the edges
+ fprintf( pFile, "\n" );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ {
+ fprintf( pFile, " edge [ source %5d target %5d\n", pObj->Id, pFanin->Id );
+ fprintf( pFile, " graphics [ type \"line\" arrow \"first\" ]\n" );
+ fprintf( pFile, " ]\n" );
+ }
+ }
+
+ fprintf( pFile, "]\n" );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index cb39c481..34582473 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -3,10 +3,14 @@ SRC += src/base/io/io.c \
src/base/io/ioReadBench.c \
src/base/io/ioReadBlif.c \
src/base/io/ioReadEdif.c \
+ src/base/io/ioReadEqn.c \
src/base/io/ioReadPla.c \
src/base/io/ioReadVerilog.c \
src/base/io/ioUtil.c \
src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \
src/base/io/ioWriteCnf.c \
+ src/base/io/ioWriteDot.c \
+ src/base/io/ioWriteEqn.c \
+ src/base/io/ioWriteGml.c \
src/base/io/ioWritePla.c