Commit 64d7119d by Alan Mishchenko

Adding visualization of word-level networks Wlc_Ntk_t.

parent 7d82819d
...@@ -88,10 +88,6 @@ LINK32=link.exe ...@@ -88,10 +88,6 @@ LINK32=link.exe
# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat" # PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
# Begin Source File # Begin Source File
SOURCE=.\src\proof\acec\acecTree.c
# End Source File
# Begin Source File
SOURCE=.\src\base\main\main.c SOURCE=.\src\base\main\main.c
# End Source File # End Source File
# End Group # End Group
......
...@@ -221,7 +221,8 @@ static inline int Wlc_NtkHasNameId( Wlc_Ntk_t * p ) ...@@ -221,7 +221,8 @@ static inline int Wlc_NtkHasNameId( Wlc_Ntk_t * p )
static inline void Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vNameIds, iObj, i ); } static inline void Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vNameIds, iObj, i ); }
static inline int Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vNameIds, iObj ); } static inline int Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vNameIds, iObj ); }
static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } static inline Wlc_Obj_t * Wlc_ObjFo2Fi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkPoNum(p) + Wlc_ObjCiId(pObj) - Wlc_NtkPiNum(p)); }
static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) { return iCoId < Wlc_NtkPoNum(p) ? Wlc_NtkPo(p, iCoId) : Wlc_NtkCi(p, Wlc_NtkPiNum(p) + iCoId - Wlc_NtkPoNum(p)); }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
...@@ -283,15 +284,19 @@ extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int ...@@ -283,15 +284,19 @@ extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int
extern void Wlc_NtkFree( Wlc_Ntk_t * p ); extern void Wlc_NtkFree( Wlc_Ntk_t * p );
extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p ); extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p ); extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
extern int Wlc_NtkCountRealPis( Wlc_Ntk_t * p );
extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ); extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray ); extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose ); extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked );
extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iPo ); extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int fSeq );
extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ); extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
extern void Wlc_NtkShortNames( Wlc_Ntk_t * p );
/*=== wlcReadSmt.c ========================================================*/ /*=== wlcReadSmt.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree ); extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree ); extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
......
...@@ -173,8 +173,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit ) ...@@ -173,8 +173,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
if ( vNodes != vNodesInit ) if ( vNodes != vNodesInit )
Vec_IntFree( vNodes ); Vec_IntFree( vNodes );
// reconstruct topological order // reconstruct topological order
pNew = Wlc_NtkDupDfs( p, 0 ); pNew = Wlc_NtkDupDfs( p, 0, 1 );
Wlc_NtkTransferNames( pNew, p );
return pNew; return pNew;
} }
...@@ -278,8 +277,7 @@ Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit ) ...@@ -278,8 +277,7 @@ Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
if ( vPairs != vPairsInit ) if ( vPairs != vPairsInit )
Vec_IntFree( vPairs ); Vec_IntFree( vPairs );
// reconstruct topological order // reconstruct topological order
pNew = Wlc_NtkDupDfs( p, 0 ); pNew = Wlc_NtkDupDfs( p, 0, 1 );
Wlc_NtkTransferNames( pNew, p );
return pNew; return pNew;
} }
......
...@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START ...@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
// Word-level Verilog file parser // Word-level Verilog file parser
#define WLV_PRS_MAX_LINE 1000 #define WLV_PRS_MAX_LINE 10000
typedef struct Wlc_Prs_t_ Wlc_Prs_t; typedef struct Wlc_Prs_t_ Wlc_Prs_t;
struct Wlc_Prs_t_ struct Wlc_Prs_t_
...@@ -1265,8 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr ) ...@@ -1265,8 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
if ( !Wlc_PrsDerive( p ) ) if ( !Wlc_PrsDerive( p ) )
goto finish; goto finish;
// derive topological order // derive topological order
pNtk = Wlc_NtkDupDfs( p->pNtk, 0 ); pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
Wlc_NtkTransferNames( pNtk, p->pNtk );
pNtk->pSpec = Abc_UtilStrsav( pFileName ); pNtk->pSpec = Abc_UtilStrsav( pFileName );
finish: finish:
Wlc_PrsPrintErrorMessage( p ); Wlc_PrsPrintErrorMessage( p );
......
...@@ -143,7 +143,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -143,7 +143,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
fprintf( pFile, " fontsize=18,\n" ); fprintf( pFile, " fontsize=18,\n" );
fprintf( pFile, " fontname = \"Times-Roman\",\n" ); fprintf( pFile, " fontname = \"Times-Roman\",\n" );
fprintf( pFile, " label=\"" ); fprintf( pFile, " label=\"" );
fprintf( pFile, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkPiNum(p)-Wlc_NtkPoNum(p)-Wlc_NtkFfNum(p), LevelMax-1 ); fprintf( pFile, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkCiNum(p), LevelMax-1 );
fprintf( pFile, "\\n" ); fprintf( pFile, "\\n" );
fprintf( pFile, "\"\n" ); fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" ); fprintf( pFile, " ];\n" );
...@@ -159,8 +159,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -159,8 +159,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
// generate the CO nodes // generate the CO nodes
Wlc_NtkForEachCo( p, pNode, i ) Wlc_NtkForEachCo( p, pNode, i )
{ {
fprintf( pFile, " NodePo%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); pNode = Wlc_ObjCo2PoFo(p, i);
fprintf( pFile, ", shape = %s", "invtriangle" ); fprintf( pFile, " NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
fprintf( pFile, ", color = coral, fillcolor = coral" ); fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" ); fprintf( pFile, "];\n" );
} }
...@@ -224,7 +225,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -224,7 +225,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Wlc_NtkForEachCi( p, pNode, i ) Wlc_NtkForEachCi( p, pNode, i )
{ {
fprintf( pFile, " Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); fprintf( pFile, " Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
fprintf( pFile, ", shape = %s", "triangle" ); fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
fprintf( pFile, ", color = coral, fillcolor = coral" ); fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" ); fprintf( pFile, "];\n" );
} }
...@@ -235,11 +236,15 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -235,11 +236,15 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
// generate invisible edges from the square down // generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" ); fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Wlc_NtkForEachCo( p, pNode, i ) Wlc_NtkForEachCo( p, pNode, i )
{
pNode = Wlc_ObjCo2PoFo( p, i );
fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) ); fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) );
}
// generate invisible edges among the COs // generate invisible edges among the COs
Prev = -1; Prev = -1;
Wlc_NtkForEachCo( p, pNode, i ) Wlc_NtkForEachCo( p, pNode, i )
{ {
pNode = Wlc_ObjCo2PoFo( p, i );
if ( i > 0 ) if ( i > 0 )
fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) ); fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
Prev = Wlc_ObjId(p, pNode); Prev = Wlc_ObjId(p, pNode);
...@@ -254,22 +259,21 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -254,22 +259,21 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
} }
// generate edges // generate edges
Wlc_NtkForEachCo( p, pNode, i )
{
fprintf( pFile, "NodePo%d", Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", Wlc_ObjId(p, pNode) );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "solid" );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
Wlc_NtkForEachObj( p, pNode, i ) Wlc_NtkForEachObj( p, pNode, i )
{ {
int k, iFanin; int k, iFanin;
if ( Wlc_ObjIsCi(pNode) ) if ( Wlc_ObjIsCi(pNode) )
continue; continue;
if ( Wlc_ObjIsCo(pNode) )
{
// generate the edge from this node to the next
fprintf( pFile, "NodePo%d", i );
fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", i );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "bold" );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
// generate the edge from this node to the next // generate the edge from this node to the next
Wlc_ObjForEachFanin( pNode, iFanin, k ) Wlc_ObjForEachFanin( pNode, iFanin, k )
{ {
...@@ -277,7 +281,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold ) ...@@ -277,7 +281,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
fprintf( pFile, " -> " ); fprintf( pFile, " -> " );
fprintf( pFile, "Node%d", iFanin ); fprintf( pFile, "Node%d", iFanin );
fprintf( pFile, " [" ); fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "bold" ); fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "solid" );
if ( pNode->Type == WLC_OBJ_MUX && k == 0 )
fprintf( pFile, ", style = %s", "bold" );
fprintf( pFile, "]" ); fprintf( pFile, "]" );
fprintf( pFile, ";\n" ); fprintf( pFile, ";\n" );
} }
......
...@@ -409,7 +409,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops ) ...@@ -409,7 +409,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
fprintf( pFile, " reg%d (", i ); fprintf( pFile, " reg%d (", i );
fprintf( pFile, " .q( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); fprintf( pFile, " .q( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
fprintf( pFile, " .qbar()," ); fprintf( pFile, " .qbar()," );
fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) ); fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
fprintf( pFile, " .clk( %s ),", "1\'b0" ); fprintf( pFile, " .clk( %s ),", "1\'b0" );
fprintf( pFile, " .arst( %s ),", "1\'b0" ); fprintf( pFile, " .arst( %s ),", "1\'b0" );
if ( p->vInits ) if ( p->vInits )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment