abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
ivyShow.c File Reference
#include "ivy.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 		Ivy_WriteDotAig (Ivy_Man_t *pMan, char *pFileName, int fHaig, Vec_Ptr_t *vBold)
 DECLARATIONS ///. More...
 
void Ivy_ManShow (Ivy_Man_t *pMan, int fHaig, Vec_Ptr_t *vBold)
 FUNCTION DEFINITIONS ///. More...
 

Function Documentation

void Ivy_ManShow ( Ivy_Man_t *  pMan,
int  fHaig,
Vec_Ptr_t *  vBold 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file ivyShow.c.

48 {
49  extern void Abc_ShowFile( char * FileNameDot );
50  static int Counter = 0;
51  char FileNameDot[200];
52  FILE * pFile;
53  // create the file name
54 // Ivy_ShowGetFileName( pMan->pName, FileNameDot );
55  sprintf( FileNameDot, "temp%02d.dot", Counter++ );
56  // check that the file can be opened
57  if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
58  {
59  fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
60  return;
61  }
62  fclose( pFile );
63  // generate the file
64  Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
65  // visualize the file
66  Abc_ShowFile( FileNameDot );
67 }
Ivy_WriteDotAig
static ABC_NAMESPACE_IMPL_START void Ivy_WriteDotAig(Ivy_Man_t *pMan, char *pFileName, int fHaig, Vec_Ptr_t *vBold)
DECLARATIONS ///.
Definition: ivyShow.c:81
Abc_ShowFile
ABC_NAMESPACE_IMPL_START void Abc_ShowFile(char *FileNameDot)
DECLARATIONS ///.
Definition: abcShow.c:245
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
void Ivy_WriteDotAig ( Ivy_Man_t *  pMan,
char *  pFileName,
int  fHaig,
Vec_Ptr_t *  vBold 
)
static

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyShow.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Visualization of HAIG.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:
ivyShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Function*************************************************************

Synopsis [Writes the graph structure of AIG for DOT.]

Description [Useful for graph visualization using tools such as GraphViz: http://www.graphviz.org/]

SideEffects []

SeeAlso []

Definition at line 81 of file ivyShow.c.

82 {
83  FILE * pFile;
84  Ivy_Obj_t * pNode, * pTemp, * pPrev;
85  int LevelMax, Level, i;
86 
87  if ( Ivy_ManNodeNum(pMan) > 200 )
88  {
89  fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" );
90  return;
91  }
92  if ( (pFile = fopen( pFileName, "w" )) == NULL )
93  {
94  fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
95  return;
96  }
97 
98  // mark the nodes
99  if ( vBold )
100  Vec_PtrForEachEntry( Ivy_Obj_t *, vBold, pNode, i )
101  pNode->fMarkB = 1;
102 
103  // compute levels
104  LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
105 
106  // write the DOT header
107  fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" );
108  fprintf( pFile, "\n" );
109  fprintf( pFile, "digraph AIG {\n" );
110  fprintf( pFile, "size = \"7.5,10\";\n" );
111 // fprintf( pFile, "ranksep = 0.5;\n" );
112 // fprintf( pFile, "nodesep = 0.5;\n" );
113  fprintf( pFile, "center = true;\n" );
114 // fprintf( pFile, "orientation = landscape;\n" );
115 // fprintf( pFile, "edge [fontsize = 10];\n" );
116 // fprintf( pFile, "edge [dir = none];\n" );
117  fprintf( pFile, "edge [dir = back];\n" );
118  fprintf( pFile, "\n" );
119 
120  // labels on the left of the picture
121  fprintf( pFile, "{\n" );
122  fprintf( pFile, " node [shape = plaintext];\n" );
123  fprintf( pFile, " edge [style = invis];\n" );
124  fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
125  fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
126  // generate node names with labels
127  for ( Level = LevelMax; Level >= 0; Level-- )
128  {
129  // the visible node name
130  fprintf( pFile, " Level%d", Level );
131  fprintf( pFile, " [label = " );
132  // label name
133  fprintf( pFile, "\"" );
134  fprintf( pFile, "\"" );
135  fprintf( pFile, "];\n" );
136  }
137 
138  // genetate the sequence of visible/invisible nodes to mark levels
139  fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
140  for ( Level = LevelMax; Level >= 0; Level-- )
141  {
142  // the visible node name
143  fprintf( pFile, " Level%d", Level );
144  // the connector
145  if ( Level != 0 )
146  fprintf( pFile, " ->" );
147  else
148  fprintf( pFile, ";" );
149  }
150  fprintf( pFile, "\n" );
151  fprintf( pFile, "}" );
152  fprintf( pFile, "\n" );
153  fprintf( pFile, "\n" );
154 
155  // generate title box on top
156  fprintf( pFile, "{\n" );
157  fprintf( pFile, " rank = same;\n" );
158  fprintf( pFile, " LevelTitle1;\n" );
159  fprintf( pFile, " title1 [shape=plaintext,\n" );
160  fprintf( pFile, " fontsize=20,\n" );
161  fprintf( pFile, " fontname = \"Times-Roman\",\n" );
162  fprintf( pFile, " label=\"" );
163  fprintf( pFile, "%s", "AIG structure visualized by ABC" );
164  fprintf( pFile, "\\n" );
165  fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
166  fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
167  fprintf( pFile, "\"\n" );
168  fprintf( pFile, " ];\n" );
169  fprintf( pFile, "}" );
170  fprintf( pFile, "\n" );
171  fprintf( pFile, "\n" );
172 
173  // generate statistics box
174  fprintf( pFile, "{\n" );
175  fprintf( pFile, " rank = same;\n" );
176  fprintf( pFile, " LevelTitle2;\n" );
177  fprintf( pFile, " title2 [shape=plaintext,\n" );
178  fprintf( pFile, " fontsize=18,\n" );
179  fprintf( pFile, " fontname = \"Times-Roman\",\n" );
180  fprintf( pFile, " label=\"" );
181  fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Ivy_ManNodeNum(pMan), LevelMax );
182  fprintf( pFile, "\\n" );
183  fprintf( pFile, "\"\n" );
184  fprintf( pFile, " ];\n" );
185  fprintf( pFile, "}" );
186  fprintf( pFile, "\n" );
187  fprintf( pFile, "\n" );
188 
189  // generate the COs
190  fprintf( pFile, "{\n" );
191  fprintf( pFile, " rank = same;\n" );
192  // the labeling node of this level
193  fprintf( pFile, " Level%d;\n", LevelMax );
194  // generate the CO nodes
195  Ivy_ManForEachCo( pMan, pNode, i )
196  {
197  if ( fHaig || pNode->pEquiv == NULL )
198  fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
199  (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
200  else
201  fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
202  (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":""),
203  Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
204  fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"invtriangle") );
205  fprintf( pFile, ", color = coral, fillcolor = coral" );
206  fprintf( pFile, "];\n" );
207  }
208  fprintf( pFile, "}" );
209  fprintf( pFile, "\n" );
210  fprintf( pFile, "\n" );
211 
212  // generate nodes of each rank
213  for ( Level = LevelMax - 1; Level > 0; Level-- )
214  {
215  fprintf( pFile, "{\n" );
216  fprintf( pFile, " rank = same;\n" );
217  // the labeling node of this level
218  fprintf( pFile, " Level%d;\n", Level );
219  Ivy_ManForEachObj( pMan, pNode, i )
220  {
221  if ( (int)pNode->Level != Level )
222  continue;
223  if ( fHaig || pNode->pEquiv == NULL )
224  fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
225  else
226  fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
227  Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
228  fprintf( pFile, ", shape = ellipse" );
229  if ( vBold && pNode->fMarkB )
230  fprintf( pFile, ", style = filled" );
231  fprintf( pFile, "];\n" );
232  }
233  fprintf( pFile, "}" );
234  fprintf( pFile, "\n" );
235  fprintf( pFile, "\n" );
236  }
237 
238  // generate the CI nodes
239  fprintf( pFile, "{\n" );
240  fprintf( pFile, " rank = same;\n" );
241  // the labeling node of this level
242  fprintf( pFile, " Level%d;\n", 0 );
243  // generate constant node
244  if ( Ivy_ObjRefs(Ivy_ManConst1(pMan)) > 0 )
245  {
246  pNode = Ivy_ManConst1(pMan);
247  // check if the costant node is present
248  fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id );
249  fprintf( pFile, ", shape = ellipse" );
250  fprintf( pFile, ", color = coral, fillcolor = coral" );
251  fprintf( pFile, "];\n" );
252  }
253  // generate the CI nodes
254  Ivy_ManForEachCi( pMan, pNode, i )
255  {
256  if ( fHaig || pNode->pEquiv == NULL )
257  fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
258  (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":"") );
259  else
260  fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
261  (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":""),
262  Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
263  fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"triangle") );
264  fprintf( pFile, ", color = coral, fillcolor = coral" );
265  fprintf( pFile, "];\n" );
266  }
267  fprintf( pFile, "}" );
268  fprintf( pFile, "\n" );
269  fprintf( pFile, "\n" );
270 
271  // generate invisible edges from the square down
272  fprintf( pFile, "title1 -> title2 [style = invis];\n" );
273  Ivy_ManForEachCo( pMan, pNode, i )
274  fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
275 
276  // generate edges
277  Ivy_ManForEachObj( pMan, pNode, i )
278  {
279  if ( !Ivy_ObjIsNode(pNode) && !Ivy_ObjIsCo(pNode) && !Ivy_ObjIsBuf(pNode) )
280  continue;
281  // generate the edge from this node to the next
282  fprintf( pFile, "Node%d%s", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") );
283  fprintf( pFile, " -> " );
284  fprintf( pFile, "Node%d%s", Ivy_ObjFaninId0(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin0(pNode))? "_out":"") );
285  fprintf( pFile, " [" );
286  fprintf( pFile, "style = %s", Ivy_ObjFaninC0(pNode)? "dotted" : "bold" );
287 // if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
288 // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
289  fprintf( pFile, "]" );
290  fprintf( pFile, ";\n" );
291  if ( !Ivy_ObjIsNode(pNode) )
292  continue;
293  // generate the edge from this node to the next
294  fprintf( pFile, "Node%d", pNode->Id );
295  fprintf( pFile, " -> " );
296  fprintf( pFile, "Node%d%s", Ivy_ObjFaninId1(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin1(pNode))? "_out":"") );
297  fprintf( pFile, " [" );
298  fprintf( pFile, "style = %s", Ivy_ObjFaninC1(pNode)? "dotted" : "bold" );
299 // if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
300 // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
301  fprintf( pFile, "]" );
302  fprintf( pFile, ";\n" );
303  // generate the edges between the equivalent nodes
304  if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
305  {
306  pPrev = pNode;
307  for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
308  {
309  fprintf( pFile, "Node%d", pPrev->Id );
310  fprintf( pFile, " -> " );
311  fprintf( pFile, "Node%d", pTemp->Id );
312  fprintf( pFile, " [style = %s]", Ivy_IsComplement(pTemp->pEquiv)? "dotted" : "bold" );
313  fprintf( pFile, ";\n" );
314  pPrev = pTemp;
315  }
316  // connect the last node with the first
317  fprintf( pFile, "Node%d", pPrev->Id );
318  fprintf( pFile, " -> " );
319  fprintf( pFile, "Node%d", pNode->Id );
320  fprintf( pFile, " [style = %s]", Ivy_IsComplement(pPrev->pEquiv)? "dotted" : "bold" );
321  fprintf( pFile, ";\n" );
322  }
323  }
324 
325  fprintf( pFile, "}" );
326  fprintf( pFile, "\n" );
327  fprintf( pFile, "\n" );
328  fclose( pFile );
329 
330  // unmark nodes
331  if ( vBold )
332  Vec_PtrForEachEntry( Ivy_Obj_t *, vBold, pNode, i )
333  pNode->fMarkB = 0;
334 }
Ivy_IsComplement
static int Ivy_IsComplement(Ivy_Obj_t *p)
Definition: ivy.h:196
Ivy_Obj_t_::Level
unsigned Level
Definition: ivy.h:84
Ivy_ManConst1
static Ivy_Obj_t * Ivy_ManConst1(Ivy_Man_t *p)
Definition: ivy.h:199
Ivy_ManSetLevels
int Ivy_ManSetLevels(Ivy_Man_t *p, int fHaig)
Definition: ivyDfs.c:457
Ivy_ObjFaninId1
static int Ivy_ObjFaninId1(Ivy_Obj_t *pObj)
Definition: ivy.h:268
Ivy_Obj_t_::Id
int Id
Definition: ivy.h:75
Ivy_ObjIsLatch
static int Ivy_ObjIsLatch(Ivy_Obj_t *pObj)
Definition: ivy.h:241
Ivy_ObjFanin1
static Ivy_Obj_t * Ivy_ObjFanin1(Ivy_Obj_t *pObj)
Definition: ivy.h:272
Ivy_ObjFanin0
static Ivy_Obj_t * Ivy_ObjFanin0(Ivy_Obj_t *pObj)
Definition: ivy.h:271
Ivy_ObjFaninId0
static int Ivy_ObjFaninId0(Ivy_Obj_t *pObj)
Definition: ivy.h:267
Ivy_ManForEachCo
#define Ivy_ManForEachCo(p, pObj, i)
Definition: ivy.h:399
Ivy_ObjFaninC1
static int Ivy_ObjFaninC1(Ivy_Obj_t *pObj)
Definition: ivy.h:270
Ivy_ObjRefs
static int Ivy_ObjRefs(Ivy_Obj_t *pObj)
Definition: ivy.h:264
Ivy_Obj_t_
Definition: ivy.h:73
Ivy_Regular
static Ivy_Obj_t * Ivy_Regular(Ivy_Obj_t *p)
Definition: ivy.h:193
Ivy_ObjIsCo
static int Ivy_ObjIsCo(Ivy_Obj_t *pObj)
Definition: ivy.h:239
Ivy_ObjIsNode
static int Ivy_ObjIsNode(Ivy_Obj_t *pObj)
Definition: ivy.h:245
Ivy_ManForEachCi
#define Ivy_ManForEachCi(p, pObj, i)
Definition: ivy.h:396
Ivy_Obj_t_::fMarkB
unsigned fMarkB
Definition: ivy.h:79
Extra_TimeStamp
char * Extra_TimeStamp()
Definition: extraUtilFile.c:446
Ivy_ObjIsBuf
static int Ivy_ObjIsBuf(Ivy_Obj_t *pObj)
Definition: ivy.h:244
Ivy_ManNodeNum
static int Ivy_ManNodeNum(Ivy_Man_t *p)
Definition: ivy.h:227
Ivy_ManForEachObj
#define Ivy_ManForEachObj(p, pObj, i)
Definition: ivy.h:393
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ivy_ObjFaninC0
static int Ivy_ObjFaninC0(Ivy_Obj_t *pObj)
Definition: ivy.h:269
Ivy_Obj_t_::pEquiv
Ivy_Obj_t * pEquiv
Definition: ivy.h:93