1 /**CFile****************************************************************
2 
3   FileName    [giaShow.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [And-Inverter Graph package.]
8 
9   Synopsis    [AIG visualization.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - May 11, 2006.]
16 
17   Revision    [$Id: giaShow.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 #include "proof/cec/cec.h"
23 #include "proof/acec/acec.h"
24 #include "misc/extra/extra.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                        DECLARATIONS                              ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 #define NODE_MAX 2000
34 
35 ////////////////////////////////////////////////////////////////////////
36 ///                     FUNCTION DEFINITIONS                         ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 /**Function*************************************************************
40 
41   Synopsis    [Writes the graph structure of AIG for DOT.]
42 
43   Description [Useful for graph visualization using tools such as GraphViz:
44   http://www.graphviz.org/]
45 
46   SideEffects []
47 
48   SeeAlso     []
49 
50 ***********************************************************************/
Gia_ShowPath(Gia_Man_t * p,char * pFileName)51 void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
52 {
53     FILE * pFile;
54     Gia_Obj_t * pNode;
55     Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
56     int i, k, iFan, LevelMax, nLevels, * pLevels, Level, Prev;
57     int nLuts = 0, nNodes = 0, nEdges = 0;
58     assert( Gia_ManHasMapping(p) );
59 
60     // set critical CO drivers
61     nLevels = Gia_ManLutLevel( p, &pLevels );
62     Gia_ManForEachCoDriverId( p, iFan, i )
63         if ( pLevels[iFan] == nLevels )
64             Vec_BitWriteEntry( vPath, iFan, 1 );
65 
66     // set critical internal nodes
67     Gia_ManForEachLutReverse( p, i )
68     {
69         nLuts++;
70         if ( !Vec_BitEntry(vPath, i) )
71             continue;
72         nNodes++;
73         Gia_LutForEachFanin( p, i, iFan, k )
74         {
75             if ( pLevels[iFan] +1 < pLevels[i] )
76                 continue;
77             assert( pLevels[iFan] + 1 == pLevels[i] );
78             Vec_BitWriteEntry( vPath, iFan, 1 );
79             nEdges++;
80             //printf( "%d -> %d\n", i, iFan );
81         }
82     }
83 
84     if ( nNodes > NODE_MAX )
85     {
86         ABC_FREE( pLevels );
87         Vec_BitFree( vPath );
88         fprintf( stdout, "Cannot visualize AIG with more than %d critical nodes.\n", NODE_MAX );
89         return;
90     }
91     if ( (pFile = fopen( pFileName, "w" )) == NULL )
92     {
93         ABC_FREE( pLevels );
94         Vec_BitFree( vPath );
95         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
96         return;
97     }
98 
99     Vec_IntFreeP( &p->vLevels );
100     p->vLevels = Vec_IntAllocArray( pLevels, Gia_ManObjNum(p) );
101 
102     // compute CO levels
103     LevelMax = 1 + nLevels;
104     Gia_ManForEachCo( p, pNode, i )
105         Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax );
106 
107     // write the DOT header
108     fprintf( pFile, "# %s\n",  "AIG structure generated by GIA package" );
109     fprintf( pFile, "\n" );
110     fprintf( pFile, "digraph AIG {\n" );
111     fprintf( pFile, "size = \"7.5,10\";\n" );
112 //  fprintf( pFile, "ranksep = 0.5;\n" );
113 //  fprintf( pFile, "nodesep = 0.5;\n" );
114     fprintf( pFile, "center = true;\n" );
115 //  fprintf( pFile, "orientation = landscape;\n" );
116 //  fprintf( pFile, "edge [fontsize = 10];\n" );
117 //  fprintf( pFile, "edge [dir = none];\n" );
118     fprintf( pFile, "edge [dir = back];\n" );
119     fprintf( pFile, "\n" );
120 
121     // labels on the left of the picture
122     fprintf( pFile, "{\n" );
123     fprintf( pFile, "  node [shape = plaintext];\n" );
124     fprintf( pFile, "  edge [style = invis];\n" );
125     fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
126     fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
127     // generate node names with labels
128     for ( Level = LevelMax; Level >= 0; Level-- )
129     {
130         // the visible node name
131         fprintf( pFile, "  Level%d", Level );
132         fprintf( pFile, " [label = " );
133         // label name
134         fprintf( pFile, "\"" );
135         fprintf( pFile, "\"" );
136         fprintf( pFile, "];\n" );
137     }
138 
139     // genetate the sequence of visible/invisible nodes to mark levels
140     fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
141     for ( Level = LevelMax; Level >= 0; Level-- )
142     {
143         // the visible node name
144         fprintf( pFile, "  Level%d",  Level );
145         // the connector
146         if ( Level != 0 )
147             fprintf( pFile, " ->" );
148         else
149             fprintf( pFile, ";" );
150     }
151     fprintf( pFile, "\n" );
152     fprintf( pFile, "}" );
153     fprintf( pFile, "\n" );
154     fprintf( pFile, "\n" );
155 
156     // generate title box on top
157     fprintf( pFile, "{\n" );
158     fprintf( pFile, "  rank = same;\n" );
159     fprintf( pFile, "  LevelTitle1;\n" );
160     fprintf( pFile, "  title1 [shape=plaintext,\n" );
161     fprintf( pFile, "          fontsize=20,\n" );
162     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
163     fprintf( pFile, "          label=\"" );
164     fprintf( pFile, "%s", "AIG structure visualized by ABC" );
165     fprintf( pFile, "\\n" );
166     fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
167 //    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
168     fprintf( pFile, "\"\n" );
169     fprintf( pFile, "         ];\n" );
170     fprintf( pFile, "}" );
171     fprintf( pFile, "\n" );
172     fprintf( pFile, "\n" );
173 
174     // generate statistics box
175     fprintf( pFile, "{\n" );
176     fprintf( pFile, "  rank = same;\n" );
177     fprintf( pFile, "  LevelTitle2;\n" );
178     fprintf( pFile, "  title2 [shape=plaintext,\n" );
179     fprintf( pFile, "          fontsize=18,\n" );
180     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
181     fprintf( pFile, "          label=\"" );
182     fprintf( pFile, "The critical path contains %d LUTs with %d critical edges and spans %d levels.", nNodes, nEdges, nLevels );
183     fprintf( pFile, "\\n" );
184     fprintf( pFile, "\"\n" );
185     fprintf( pFile, "         ];\n" );
186     fprintf( pFile, "}" );
187     fprintf( pFile, "\n" );
188     fprintf( pFile, "\n" );
189 
190     // generate the COs
191     fprintf( pFile, "{\n" );
192     fprintf( pFile, "  rank = same;\n" );
193     // the labeling node of this level
194     fprintf( pFile, "  Level%d;\n",  LevelMax );
195     // generate the CO nodes
196     Gia_ManForEachCo( p, pNode, i )
197     {
198         if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels )
199             continue;
200         assert( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels );
201         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
202         fprintf( pFile, ", shape = %s", "invtriangle" );
203         fprintf( pFile, ", color = coral, fillcolor = coral" );
204         fprintf( pFile, "];\n" );
205     }
206     fprintf( pFile, "}" );
207     fprintf( pFile, "\n" );
208     fprintf( pFile, "\n" );
209 
210     // generate nodes of each rank
211     for ( Level = LevelMax - 1; Level > 0; Level-- )
212     {
213         fprintf( pFile, "{\n" );
214         fprintf( pFile, "  rank = same;\n" );
215         // the labeling node of this level
216         fprintf( pFile, "  Level%d;\n",  Level );
217         Gia_ManForEachObj( p, pNode, i )
218         {
219             if ( (int)Gia_ObjLevel(p, pNode) != Level || !Vec_BitEntry(vPath, i) )
220                 continue;
221             fprintf( pFile, "  Node%d [label = \"%d:%d\"", i, Vec_IntSize(p->vIdsOrig)?Vec_IntEntry(p->vIdsOrig,i):i, Gia_ObjIsAnd(pNode)?Gia_ObjLutSize(p, i):0 );
222             fprintf( pFile, ", shape = ellipse" );
223             if ( pNode->fMark0 )
224                 fprintf( pFile, ", style = filled" );
225             fprintf( pFile, "];\n" );
226         }
227         fprintf( pFile, "}" );
228         fprintf( pFile, "\n" );
229         fprintf( pFile, "\n" );
230     }
231 
232     // generate the CI nodes
233     fprintf( pFile, "{\n" );
234     fprintf( pFile, "  rank = same;\n" );
235     // the labeling node of this level
236     fprintf( pFile, "  Level%d;\n",  0 );
237     // generate the CI nodes
238     Gia_ManForEachCi( p, pNode, i )
239     {
240         if ( !Vec_BitEntry(vPath, Gia_ObjId(p, pNode)) )
241             continue;
242         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
243         fprintf( pFile, ", shape = %s", "triangle" );
244         fprintf( pFile, ", color = coral, fillcolor = coral" );
245         fprintf( pFile, "];\n" );
246     }
247     fprintf( pFile, "}" );
248     fprintf( pFile, "\n" );
249     fprintf( pFile, "\n" );
250 
251     // generate invisible edges from the square down
252     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
253     Gia_ManForEachCo( p, pNode, i )
254     {
255         if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels )
256             continue;
257         fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) );
258     }
259     // generate invisible edges among the COs
260     Prev = -1;
261     Gia_ManForEachCo( p, pNode, i )
262     {
263         if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels )
264             continue;
265         assert( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels );
266         if ( Prev >= 0 )
267             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
268         Prev = Gia_ObjId(p, pNode);
269     }
270     // generate invisible edges among the CIs
271     Prev = -1;
272     Gia_ManForEachCi( p, pNode, i )
273     {
274         if ( !Vec_BitEntry(vPath, Gia_ObjId(p, pNode)) )
275             continue;
276         if ( Prev >= 0 )
277             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
278         Prev = Gia_ObjId(p, pNode);
279     }
280 
281     // generate edges
282     Gia_ManForEachObj( p, pNode, i )
283     {
284         if ( Gia_ObjIsCo(pNode) )
285         {
286             if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels )
287             {
288                 // generate the edge from this node to the next
289                 fprintf( pFile, "Node%d",  i );
290                 fprintf( pFile, " -> " );
291                 fprintf( pFile, "Node%d",  Gia_ObjFaninId0p(p, pNode) );
292                 fprintf( pFile, " [" );
293                 fprintf( pFile, "style = %s", "solid" );
294                 fprintf( pFile, "]" );
295                 fprintf( pFile, ";\n" );
296             }
297             continue;
298         }
299         if ( !Gia_ObjIsAnd(pNode) || !Vec_BitEntry(vPath, i) )
300             continue;
301         Gia_LutForEachFanin( p, i, iFan, k )
302         {
303             if ( pLevels[iFan] + 1 < pLevels[i] )
304                 continue;
305             assert( pLevels[iFan] + 1 == pLevels[i] );
306             // generate the edge from this node to the next
307             fprintf( pFile, "Node%d",  i );
308             fprintf( pFile, " -> " );
309             fprintf( pFile, "Node%d",  iFan );
310             fprintf( pFile, " [" );
311             fprintf( pFile, "style = %s", "solid" );
312             fprintf( pFile, "]" );
313             fprintf( pFile, ";\n" );
314         }
315     }
316 
317     fprintf( pFile, "}" );
318     fprintf( pFile, "\n" );
319     fprintf( pFile, "\n" );
320     fclose( pFile );
321 
322     Vec_IntFreeP( &p->vLevels );
323     Vec_BitFree( vPath );
324 }
325 
326 
327 /**Function*************************************************************
328 
329   Synopsis    [Writes the graph structure of AIG for DOT.]
330 
331   Description [Useful for graph visualization using tools such as GraphViz:
332   http://www.graphviz.org/]
333 
334   SideEffects []
335 
336   SeeAlso     []
337 
338 ***********************************************************************/
Gia_WriteDotAigSimple(Gia_Man_t * p,char * pFileName,Vec_Int_t * vBold)339 void Gia_WriteDotAigSimple( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold )
340 {
341     FILE * pFile;
342     Gia_Obj_t * pNode;//, * pTemp, * pPrev;
343     int LevelMax, Prev, Level, i;
344     int fConstIsUsed = 0;
345 
346     if ( Gia_ManAndNum(p) > NODE_MAX )
347     {
348         fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
349         return;
350     }
351     if ( (pFile = fopen( pFileName, "w" )) == NULL )
352     {
353         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
354         return;
355     }
356 
357     // mark the nodes
358     if ( vBold )
359         Gia_ManForEachObjVec( vBold, p, pNode, i )
360             pNode->fMark0 = 1;
361     else if ( p->nXors || p->nMuxes )
362         Gia_ManForEachObj( p, pNode, i )
363             if ( Gia_ObjIsXor(pNode) || Gia_ObjIsMux(p, pNode) )
364                 pNode->fMark0 = 1;
365 
366     // compute levels
367     LevelMax = 1 + Gia_ManLevelNum( p );
368     Gia_ManForEachCo( p, pNode, i )
369         Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax );
370 
371     // write the DOT header
372     fprintf( pFile, "# %s\n",  "AIG structure generated by GIA package" );
373     fprintf( pFile, "\n" );
374     fprintf( pFile, "digraph AIG {\n" );
375     fprintf( pFile, "size = \"7.5,10\";\n" );
376 //  fprintf( pFile, "ranksep = 0.5;\n" );
377 //  fprintf( pFile, "nodesep = 0.5;\n" );
378     fprintf( pFile, "center = true;\n" );
379 //  fprintf( pFile, "orientation = landscape;\n" );
380 //  fprintf( pFile, "edge [fontsize = 10];\n" );
381 //  fprintf( pFile, "edge [dir = none];\n" );
382     fprintf( pFile, "edge [dir = back];\n" );
383     fprintf( pFile, "\n" );
384 
385     // labels on the left of the picture
386     fprintf( pFile, "{\n" );
387     fprintf( pFile, "  node [shape = plaintext];\n" );
388     fprintf( pFile, "  edge [style = invis];\n" );
389     fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
390     fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
391     // generate node names with labels
392     for ( Level = LevelMax; Level >= 0; Level-- )
393     {
394         // the visible node name
395         fprintf( pFile, "  Level%d", Level );
396         fprintf( pFile, " [label = " );
397         // label name
398         fprintf( pFile, "\"" );
399         fprintf( pFile, "\"" );
400         fprintf( pFile, "];\n" );
401     }
402 
403     // genetate the sequence of visible/invisible nodes to mark levels
404     fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
405     for ( Level = LevelMax; Level >= 0; Level-- )
406     {
407         // the visible node name
408         fprintf( pFile, "  Level%d",  Level );
409         // the connector
410         if ( Level != 0 )
411             fprintf( pFile, " ->" );
412         else
413             fprintf( pFile, ";" );
414     }
415     fprintf( pFile, "\n" );
416     fprintf( pFile, "}" );
417     fprintf( pFile, "\n" );
418     fprintf( pFile, "\n" );
419 
420     // generate title box on top
421     fprintf( pFile, "{\n" );
422     fprintf( pFile, "  rank = same;\n" );
423     fprintf( pFile, "  LevelTitle1;\n" );
424     fprintf( pFile, "  title1 [shape=plaintext,\n" );
425     fprintf( pFile, "          fontsize=20,\n" );
426     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
427     fprintf( pFile, "          label=\"" );
428     fprintf( pFile, "%s", "AIG structure visualized by ABC" );
429     fprintf( pFile, "\\n" );
430     fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
431 //    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
432     fprintf( pFile, "\"\n" );
433     fprintf( pFile, "         ];\n" );
434     fprintf( pFile, "}" );
435     fprintf( pFile, "\n" );
436     fprintf( pFile, "\n" );
437 
438     // generate statistics box
439     fprintf( pFile, "{\n" );
440     fprintf( pFile, "  rank = same;\n" );
441     fprintf( pFile, "  LevelTitle2;\n" );
442     fprintf( pFile, "  title2 [shape=plaintext,\n" );
443     fprintf( pFile, "          fontsize=18,\n" );
444     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
445     fprintf( pFile, "          label=\"" );
446     fprintf( pFile, "The AIG contains %d nodes and spans %d levels.", Gia_ManAndNum(p), LevelMax-1 );
447     fprintf( pFile, "\\n" );
448     fprintf( pFile, "\"\n" );
449     fprintf( pFile, "         ];\n" );
450     fprintf( pFile, "}" );
451     fprintf( pFile, "\n" );
452     fprintf( pFile, "\n" );
453 
454     // generate the COs
455     fprintf( pFile, "{\n" );
456     fprintf( pFile, "  rank = same;\n" );
457     // the labeling node of this level
458     fprintf( pFile, "  Level%d;\n",  LevelMax );
459     // generate the CO nodes
460     Gia_ManForEachCo( p, pNode, i )
461     {
462         if ( Gia_ObjFaninId0p(p, pNode) == 0 )
463             fConstIsUsed = 1;
464 /*
465         if ( fHaig || pNode->pEquiv == NULL )
466             fprintf( pFile, "  Node%d%s [label = \"%d%s\"", pNode->Id,
467                 (Gia_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_in":"") );
468         else
469             fprintf( pFile, "  Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
470                 (Gia_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_in":""),
471                     Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" );
472 */
473         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
474 
475         fprintf( pFile, ", shape = %s", "invtriangle" );
476         fprintf( pFile, ", color = coral, fillcolor = coral" );
477         fprintf( pFile, "];\n" );
478     }
479     fprintf( pFile, "}" );
480     fprintf( pFile, "\n" );
481     fprintf( pFile, "\n" );
482 
483     // generate nodes of each rank
484     for ( Level = LevelMax - 1; Level > 0; Level-- )
485     {
486         fprintf( pFile, "{\n" );
487         fprintf( pFile, "  rank = same;\n" );
488         // the labeling node of this level
489         fprintf( pFile, "  Level%d;\n",  Level );
490         Gia_ManForEachObj( p, pNode, i )
491         {
492             if ( (int)Gia_ObjLevel(p, pNode) != Level )
493                 continue;
494 /*
495             if ( fHaig || pNode->pEquiv == NULL )
496                 fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
497             else
498                 fprintf( pFile, "  Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
499                     Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" );
500 */
501             fprintf( pFile, "  Node%d [label = \"%d\"", i, i );
502 
503             if ( Gia_ObjIsXor(pNode) )
504                 fprintf( pFile, ", shape = doublecircle" );
505             else if ( Gia_ObjIsMux(p, pNode) )
506                 fprintf( pFile, ", shape = trapezium" );
507             else
508                 fprintf( pFile, ", shape = ellipse" );
509 
510             if ( pNode->fMark0 )
511                 fprintf( pFile, ", style = filled" );
512             fprintf( pFile, "];\n" );
513         }
514         fprintf( pFile, "}" );
515         fprintf( pFile, "\n" );
516         fprintf( pFile, "\n" );
517     }
518 
519     // generate the CI nodes
520     fprintf( pFile, "{\n" );
521     fprintf( pFile, "  rank = same;\n" );
522     // the labeling node of this level
523     fprintf( pFile, "  Level%d;\n",  0 );
524     // generate constant node
525     if ( fConstIsUsed )
526     {
527         // check if the costant node is present
528         fprintf( pFile, "  Node%d [label = \"Const0\"", 0 );
529         fprintf( pFile, ", shape = ellipse" );
530         fprintf( pFile, ", color = coral, fillcolor = coral" );
531         fprintf( pFile, "];\n" );
532     }
533     // generate the CI nodes
534     Gia_ManForEachCi( p, pNode, i )
535     {
536 /*
537         if ( fHaig || pNode->pEquiv == NULL )
538             fprintf( pFile, "  Node%d%s [label = \"%d%s\"", pNode->Id,
539                 (Gia_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_out":"") );
540         else
541             fprintf( pFile, "  Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
542                 (Gia_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_out":""),
543                     Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" );
544 */
545         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
546 
547         fprintf( pFile, ", shape = %s", "triangle" );
548         fprintf( pFile, ", color = coral, fillcolor = coral" );
549         fprintf( pFile, "];\n" );
550     }
551     fprintf( pFile, "}" );
552     fprintf( pFile, "\n" );
553     fprintf( pFile, "\n" );
554 
555     // generate invisible edges from the square down
556     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
557     Gia_ManForEachCo( p, pNode, i )
558         fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) );
559     // generate invisible edges among the COs
560     Prev = -1;
561     Gia_ManForEachCo( p, pNode, i )
562     {
563         if ( i > 0 )
564             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
565         Prev = Gia_ObjId(p, pNode);
566     }
567     // generate invisible edges among the CIs
568     Prev = -1;
569     Gia_ManForEachCi( p, pNode, i )
570     {
571         if ( i > 0 )
572             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
573         Prev = Gia_ObjId(p, pNode);
574     }
575 
576     // generate edges
577     Gia_ManForEachObj( p, pNode, i )
578     {
579         if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) )
580             continue;
581         // generate the edge from this node to the next
582         fprintf( pFile, "Node%d",  i );
583         fprintf( pFile, " -> " );
584         fprintf( pFile, "Node%d",  Gia_ObjFaninId0(pNode, i) );
585         fprintf( pFile, " [" );
586         fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" );
587 //        if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL0(pNode) > 0 )
588 //        fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
589         fprintf( pFile, "]" );
590         fprintf( pFile, ";\n" );
591         if ( !Gia_ObjIsAnd(pNode) )
592             continue;
593         // generate the edge from this node to the next
594         fprintf( pFile, "Node%d",  i );
595         fprintf( pFile, " -> " );
596         fprintf( pFile, "Node%d",  Gia_ObjFaninId1(pNode, i) );
597         fprintf( pFile, " [" );
598         fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "solid" );
599 //        if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL1(pNode) > 0 )
600 //        fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
601         fprintf( pFile, "]" );
602         fprintf( pFile, ";\n" );
603 
604         if ( !Gia_ObjIsMux(p, pNode) )
605             continue;
606         // generate the edge from this node to the next
607         fprintf( pFile, "Node%d",  i );
608         fprintf( pFile, " -> " );
609         fprintf( pFile, "Node%d",  Gia_ObjFaninId2(p, i) );
610         fprintf( pFile, " [" );
611         fprintf( pFile, "style = %s", Gia_ObjFaninC2(p, pNode)? "dotted" : "bold" );
612 //        if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL1(pNode) > 0 )
613 //        fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
614         fprintf( pFile, "]" );
615         fprintf( pFile, ";\n" );
616 
617 /*
618         // generate the edges between the equivalent nodes
619         if ( fHaig && pNode->pEquiv && Gia_ObjRefs(pNode) > 0 )
620         {
621             pPrev = pNode;
622             for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Gia_Regular(pTemp->pEquiv) )
623             {
624                 fprintf( pFile, "Node%d",  pPrev->Id );
625                 fprintf( pFile, " -> " );
626                 fprintf( pFile, "Node%d",  pTemp->Id );
627                 fprintf( pFile, " [style = %s]", Gia_IsComplement(pTemp->pEquiv)? "dotted" : "solid" );
628                 fprintf( pFile, ";\n" );
629                 pPrev = pTemp;
630             }
631             // connect the last node with the first
632             fprintf( pFile, "Node%d",  pPrev->Id );
633             fprintf( pFile, " -> " );
634             fprintf( pFile, "Node%d",  pNode->Id );
635             fprintf( pFile, " [style = %s]", Gia_IsComplement(pPrev->pEquiv)? "dotted" : "solid" );
636             fprintf( pFile, ";\n" );
637         }
638 */
639     }
640 
641     fprintf( pFile, "}" );
642     fprintf( pFile, "\n" );
643     fprintf( pFile, "\n" );
644     fclose( pFile );
645 
646     // unmark nodes
647     if ( vBold )
648         Gia_ManForEachObjVec( vBold, p, pNode, i )
649             pNode->fMark0 = 0;
650     else if ( p->nXors || p->nMuxes )
651         Gia_ManCleanMark0( p );
652 
653     Vec_IntFreeP( &p->vLevels );
654 }
655 
656 /**Function*************************************************************
657 
658   Synopsis    [Writes the graph structure of AIG for DOT.]
659 
660   Description [Useful for graph visualization using tools such as GraphViz:
661   http://www.graphviz.org/]
662 
663   SideEffects []
664 
665   SeeAlso     []
666 
667 ***********************************************************************/
Gia_ShowAddOut(Vec_Int_t * vAdds,Vec_Int_t * vMapAdds,int Node)668 int Gia_ShowAddOut( Vec_Int_t * vAdds, Vec_Int_t * vMapAdds, int Node )
669 {
670     int iBox = Vec_IntEntry( vMapAdds, Node );
671     if ( iBox >= 0 )
672         return Vec_IntEntry( vAdds, 6*iBox+4 );
673     return Node;
674 }
Gia_WriteDotAig(Gia_Man_t * p,char * pFileName,Vec_Int_t * vBold,Vec_Int_t * vAdds,Vec_Int_t * vXors,Vec_Int_t * vMapAdds,Vec_Int_t * vMapXors,Vec_Int_t * vOrder)675 void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
676 {
677     FILE * pFile;
678     Gia_Obj_t * pNode;//, * pTemp, * pPrev;
679     int LevelMax, Prev, Level, i;
680     int fConstIsUsed = 0;
681     int nFadds = Ree_ManCountFadds( vAdds );
682 
683     if ( Gia_ManAndNum(p) > NODE_MAX )
684     {
685         fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
686         return;
687     }
688     if ( (pFile = fopen( pFileName, "w" )) == NULL )
689     {
690         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
691         return;
692     }
693 
694     // mark the nodes
695     if ( vBold )
696         Gia_ManForEachObjVec( vBold, p, pNode, i )
697             pNode->fMark0 = 1;
698 
699     // compute levels
700     LevelMax = 1 + p->nLevels;
701     Gia_ManForEachCo( p, pNode, i )
702         Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax );
703 
704     // write the DOT header
705     fprintf( pFile, "# %s\n",  "AIG structure generated by GIA package" );
706     fprintf( pFile, "\n" );
707     fprintf( pFile, "digraph AIG {\n" );
708     fprintf( pFile, "size = \"7.5,10\";\n" );
709 //  fprintf( pFile, "ranksep = 0.5;\n" );
710 //  fprintf( pFile, "nodesep = 0.5;\n" );
711     fprintf( pFile, "center = true;\n" );
712 //  fprintf( pFile, "orientation = landscape;\n" );
713 //  fprintf( pFile, "edge [fontsize = 10];\n" );
714 //  fprintf( pFile, "edge [dir = none];\n" );
715     fprintf( pFile, "edge [dir = back];\n" );
716     fprintf( pFile, "\n" );
717 
718     // labels on the left of the picture
719     fprintf( pFile, "{\n" );
720     fprintf( pFile, "  node [shape = plaintext];\n" );
721     fprintf( pFile, "  edge [style = invis];\n" );
722     fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
723     fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
724     // generate node names with labels
725     for ( Level = LevelMax; Level >= 0; Level-- )
726     {
727         // the visible node name
728         fprintf( pFile, "  Level%d", Level );
729         fprintf( pFile, " [label = " );
730         // label name
731         fprintf( pFile, "\"" );
732         fprintf( pFile, "\"" );
733         fprintf( pFile, "];\n" );
734     }
735 
736     // genetate the sequence of visible/invisible nodes to mark levels
737     fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
738     for ( Level = LevelMax; Level >= 0; Level-- )
739     {
740         // the visible node name
741         fprintf( pFile, "  Level%d",  Level );
742         // the connector
743         if ( Level != 0 )
744             fprintf( pFile, " ->" );
745         else
746             fprintf( pFile, ";" );
747     }
748     fprintf( pFile, "\n" );
749     fprintf( pFile, "}" );
750     fprintf( pFile, "\n" );
751     fprintf( pFile, "\n" );
752 
753     // generate title box on top
754     fprintf( pFile, "{\n" );
755     fprintf( pFile, "  rank = same;\n" );
756     fprintf( pFile, "  LevelTitle1;\n" );
757     fprintf( pFile, "  title1 [shape=plaintext,\n" );
758     fprintf( pFile, "          fontsize=20,\n" );
759     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
760     fprintf( pFile, "          label=\"" );
761     fprintf( pFile, "%s", "AIG structure visualized by ABC" );
762     fprintf( pFile, "\\n" );
763     fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
764 //    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
765     fprintf( pFile, "\"\n" );
766     fprintf( pFile, "         ];\n" );
767     fprintf( pFile, "}" );
768     fprintf( pFile, "\n" );
769     fprintf( pFile, "\n" );
770 
771     // generate statistics box
772     fprintf( pFile, "{\n" );
773     fprintf( pFile, "  rank = same;\n" );
774     fprintf( pFile, "  LevelTitle2;\n" );
775     fprintf( pFile, "  title2 [shape=plaintext,\n" );
776     fprintf( pFile, "          fontsize=18,\n" );
777     fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
778     fprintf( pFile, "          label=\"" );
779     fprintf( pFile, "The AIG contains %d nodes, %d full-adders, and %d half-adders, and spans %d levels.",
780         Gia_ManAndNum(p), nFadds, Vec_IntSize(vAdds)/6-nFadds, LevelMax-1 );
781     fprintf( pFile, "\\n" );
782     fprintf( pFile, "\"\n" );
783     fprintf( pFile, "         ];\n" );
784     fprintf( pFile, "}" );
785     fprintf( pFile, "\n" );
786     fprintf( pFile, "\n" );
787 
788     // generate the COs
789     fprintf( pFile, "{\n" );
790     fprintf( pFile, "  rank = same;\n" );
791     // the labeling node of this level
792     fprintf( pFile, "  Level%d;\n",  LevelMax );
793     // generate the CO nodes
794     Gia_ManForEachCo( p, pNode, i )
795     {
796         if ( Gia_ObjFaninId0p(p, pNode) == 0 )
797             fConstIsUsed = 1;
798         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
799 
800         fprintf( pFile, ", shape = %s", "invtriangle" );
801         fprintf( pFile, ", color = coral, fillcolor = coral" );
802         fprintf( pFile, "];\n" );
803     }
804     fprintf( pFile, "}" );
805     fprintf( pFile, "\n" );
806     fprintf( pFile, "\n" );
807 
808     // generate nodes of each rank
809     for ( Level = LevelMax - 1; Level > 0; Level-- )
810     {
811         fprintf( pFile, "{\n" );
812         fprintf( pFile, "  rank = same;\n" );
813         // the labeling node of this level
814         fprintf( pFile, "  Level%d;\n",  Level );
815         Gia_ManForEachObjVec( vOrder, p, pNode, i )
816         {
817             int iNode = Gia_ObjId( p, pNode );
818             if ( (int)Gia_ObjLevel(p, pNode) != Level )
819                 continue;
820 /*
821             fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
822             if ( Gia_ObjIsXor(pNode) )
823                 fprintf( pFile, ", shape = doublecircle" );
824             else if ( Gia_ObjIsMux(p, pNode) )
825                 fprintf( pFile, ", shape = trapezium" );
826             else
827                 fprintf( pFile, ", shape = ellipse" );
828 */
829             if ( !pNode->fMark0 && Vec_IntEntry(vMapAdds, iNode) >= 0 )
830             {
831                 int iBox = Vec_IntEntry(vMapAdds, iNode);
832                 fprintf( pFile, "  Node%d [label = \"%d_%d\"", Gia_ShowAddOut(vAdds, vMapAdds, iNode), Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
833                 if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
834                     fprintf( pFile, ", shape = octagon" );
835                 else
836                     fprintf( pFile, ", shape = doubleoctagon" );
837             }
838             else if ( Vec_IntEntry(vMapXors, iNode) >= 0 )
839             {
840                 fprintf( pFile, "  Node%d [label = \"%d\"", iNode, iNode );
841                 fprintf( pFile, ", shape = doublecircle" );
842             }
843             else if ( Gia_ObjIsXor(pNode) )
844             {
845                 fprintf( pFile, "  Node%d [label = \"%d\"", iNode, iNode );
846                 fprintf( pFile, ", shape = doublecircle" );
847             }
848             else if ( Gia_ObjIsMux(p, pNode) )
849             {
850                 fprintf( pFile, "  Node%d [label = \"%d\"", iNode, iNode );
851                 fprintf( pFile, ", shape = trapezium" );
852             }
853             else
854             {
855                 fprintf( pFile, "  Node%d [label = \"%d\"", iNode, iNode );
856                 fprintf( pFile, ", shape = ellipse" );
857             }
858             if ( pNode->fMark0 )
859                 fprintf( pFile, ", style = filled" );
860             fprintf( pFile, "];\n" );
861         }
862         fprintf( pFile, "}" );
863         fprintf( pFile, "\n" );
864         fprintf( pFile, "\n" );
865     }
866 
867     // generate the CI nodes
868     fprintf( pFile, "{\n" );
869     fprintf( pFile, "  rank = same;\n" );
870     // the labeling node of this level
871     fprintf( pFile, "  Level%d;\n",  0 );
872     // generate constant node
873     if ( fConstIsUsed )
874     {
875         // check if the costant node is present
876         fprintf( pFile, "  Node%d [label = \"Const0\"", 0 );
877         fprintf( pFile, ", shape = ellipse" );
878         fprintf( pFile, ", color = coral, fillcolor = coral" );
879         fprintf( pFile, "];\n" );
880     }
881     // generate the CI nodes
882     Gia_ManForEachCi( p, pNode, i )
883     {
884         fprintf( pFile, "  Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) );
885 
886         fprintf( pFile, ", shape = %s", "triangle" );
887         fprintf( pFile, ", color = coral, fillcolor = coral" );
888         fprintf( pFile, "];\n" );
889     }
890     fprintf( pFile, "}" );
891     fprintf( pFile, "\n" );
892     fprintf( pFile, "\n" );
893 
894     // generate invisible edges from the square down
895     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
896     Gia_ManForEachCo( p, pNode, i )
897         fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) );
898     // generate invisible edges among the COs
899     Prev = -1;
900     Gia_ManForEachCo( p, pNode, i )
901     {
902         if ( i > 0 )
903             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
904         Prev = Gia_ObjId(p, pNode);
905     }
906     // generate invisible edges among the CIs
907     Prev = -1;
908     Gia_ManForEachCi( p, pNode, i )
909     {
910         if ( i > 0 )
911             fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) );
912         Prev = Gia_ObjId(p, pNode);
913     }
914 
915     // generate edges
916     Gia_ManForEachCo( p, pNode, i )
917     {
918         int iNode = Gia_ObjId( p, pNode );
919         fprintf( pFile, "Node%d",  iNode );
920         fprintf( pFile, " -> " );
921         fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId0(pNode, iNode)) );
922         fprintf( pFile, " [" );
923         fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" );
924         fprintf( pFile, "]" );
925         fprintf( pFile, ";\n" );
926     }
927     Gia_ManForEachObjVec( vOrder, p, pNode, i )
928     {
929         int iNode = Gia_ObjId( p, pNode );
930         if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pNode)) >= 0 )
931         {
932             int k, iBox = Vec_IntEntry(vMapAdds, iNode);
933             for ( k = 0; k < 3; k++ )
934                 if ( Vec_IntEntry(vAdds, 6*iBox+k) )
935                 {
936                     int iBox2 = Vec_IntEntry(vMapAdds, Vec_IntEntry(vAdds, 6*iBox+k));
937                     int fXor2 = iBox2 >= 0 ? (int)(Vec_IntEntry(vAdds, 6*iBox2+3) == Vec_IntEntry(vAdds, 6*iBox+k)) : 0;
938                     fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, iNode) );
939                     fprintf( pFile, " -> " );
940                     fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Vec_IntEntry(vAdds, 6*iBox+k)) );
941                     fprintf( pFile, " [" );
942                     fprintf( pFile, "style = %s", fXor2? "bold" : "solid" );
943                     fprintf( pFile, "]" );
944                     fprintf( pFile, ";\n" );
945                 }
946             continue;
947         }
948         if ( Vec_IntEntry(vMapXors, Gia_ObjId(p, pNode)) >= 0 )
949         {
950             int k, iXor = Vec_IntEntry(vMapXors, iNode);
951             for ( k = 1; k < 4; k++ )
952                 if ( Vec_IntEntry(vXors, 4*iXor+k) )
953                 {
954                     int iXor2 = Vec_IntEntry(vMapXors, Vec_IntEntry(vXors, 4*iXor+k));
955                     fprintf( pFile, "Node%d",  iNode );
956                     fprintf( pFile, " -> " );
957                     fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Vec_IntEntry(vXors, 4*iXor+k)) );
958                     fprintf( pFile, " [" );
959                     fprintf( pFile, "style = %s", iXor2 >= 0? "bold" : "solid" );
960                     fprintf( pFile, "]" );
961                     fprintf( pFile, ";\n" );
962                 }
963             continue;
964         }
965         // generate the edge from this node to the next
966         fprintf( pFile, "Node%d",  iNode );
967         fprintf( pFile, " -> " );
968         fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId0(pNode, iNode)) );
969         fprintf( pFile, " [" );
970         fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" );
971         fprintf( pFile, "]" );
972         fprintf( pFile, ";\n" );
973         if ( !Gia_ObjIsAnd(pNode) )
974             continue;
975         // generate the edge from this node to the next
976         fprintf( pFile, "Node%d",  iNode );
977         fprintf( pFile, " -> " );
978         fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId1(pNode, iNode)) );
979         fprintf( pFile, " [" );
980         fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "solid" );
981         fprintf( pFile, "]" );
982         fprintf( pFile, ";\n" );
983 
984         if ( !Gia_ObjIsMux(p, pNode) )
985             continue;
986         // generate the edge from this node to the next
987         fprintf( pFile, "Node%d",  iNode );
988         fprintf( pFile, " -> " );
989         fprintf( pFile, "Node%d",  Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId2(p, iNode)) );
990         fprintf( pFile, " [" );
991         fprintf( pFile, "style = %s", Gia_ObjFaninC2(p, pNode)? "dotted" : "solid" );
992         fprintf( pFile, "]" );
993         fprintf( pFile, ";\n" );
994     }
995 
996     fprintf( pFile, "}" );
997     fprintf( pFile, "\n" );
998     fprintf( pFile, "\n" );
999     fclose( pFile );
1000 
1001     // unmark nodes
1002     if ( vBold )
1003         Gia_ManForEachObjVec( vBold, p, pNode, i )
1004             pNode->fMark0 = 0;
1005 
1006     Vec_IntFreeP( &p->vLevels );
1007 }
1008 
1009 /**Function*************************************************************
1010 
1011   Synopsis    [Returns DFS ordered array of objects and their levels.]
1012 
1013   Description []
1014 
1015   SideEffects []
1016 
1017   SeeAlso     []
1018 
1019 ***********************************************************************/
Gia_ShowMapAdds(Gia_Man_t * p,Vec_Int_t * vAdds,int fFadds,Vec_Int_t * vBold)1020 Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold )
1021 {
1022     Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) );
1023     Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry;
1024     if ( vBold )
1025         Vec_IntForEachEntry( vBold, Entry, i )
1026             Vec_BitWriteEntry( vIsBold, Entry, 1 );
1027     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
1028     {
1029         if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 )
1030             continue;
1031         if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) )
1032             continue;
1033         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i );
1034         Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i );
1035     }
1036     Vec_BitFree( vIsBold );
1037     return vMapAdds;
1038 }
Gia_ShowMapXors(Gia_Man_t * p,Vec_Int_t * vXors)1039 Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors )
1040 {
1041     Vec_Int_t * vMapXors = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
1042     for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
1043         Vec_IntWriteEntry( vMapXors, Vec_IntEntry(vXors, 4*i), i );
1044     return vMapXors;
1045 }
Gia_ShowCollectObjs_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vAdds,Vec_Int_t * vXors,Vec_Int_t * vMapAdds,Vec_Int_t * vMapXors,Vec_Int_t * vOrder)1046 int Gia_ShowCollectObjs_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
1047 {
1048     int Level0, Level1, Level2 = 0, Level = 0;
1049     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
1050         return Gia_ObjLevel(p, pObj);
1051     Gia_ObjSetTravIdCurrent(p, pObj);
1052     if ( Gia_ObjIsCi(pObj) )
1053         return 0;
1054     if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pObj)) >= 0 )
1055     {
1056         int iBox = Vec_IntEntry(vMapAdds, Gia_ObjId(p, pObj));
1057         Gia_ObjSetTravIdCurrentId(p, Vec_IntEntry(vAdds, 6*iBox+3) );
1058         Gia_ObjSetTravIdCurrentId(p, Vec_IntEntry(vAdds, 6*iBox+4) );
1059         Level0 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+0) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1060         Level1 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+1) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1061         if ( Vec_IntEntry(vAdds, 6*iBox+2) )
1062         Level2 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+2) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1063         Level = 1 + Abc_MaxInt( Abc_MaxInt(Level0, Level1), Level2 );
1064         Gia_ObjSetLevelId( p, Vec_IntEntry(vAdds, 6*iBox+3), Level );
1065         Gia_ObjSetLevelId( p, Vec_IntEntry(vAdds, 6*iBox+4), Level );
1066         pObj = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+4) );
1067     }
1068     else if ( Vec_IntEntry(vMapXors, Gia_ObjId(p, pObj)) >= 0 )
1069     {
1070         int iXor = Vec_IntEntry(vMapXors, Gia_ObjId(p, pObj));
1071         Level0 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+1) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1072         Level1 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+2) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1073         if ( Vec_IntEntry(vXors, 4*iXor+3) )
1074         Level2 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+3) ), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1075         Level = 1 + Abc_MaxInt( Abc_MaxInt(Level0, Level1), Level2 );
1076         Gia_ObjSetLevel( p, pObj, Level );
1077     }
1078     else
1079     {
1080         assert( !Gia_ObjIsMux(p, pObj) );
1081         Level0 = Gia_ShowCollectObjs_rec( p, Gia_ObjFanin0(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1082         Level1 = Gia_ShowCollectObjs_rec( p, Gia_ObjFanin1(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1083         Level = 1 + Abc_MaxInt(Level0, Level1);
1084         Gia_ObjSetLevel( p, pObj, Level );
1085     }
1086     Vec_IntPush( vOrder, Gia_ObjId(p, pObj) );
1087     p->nLevels = Abc_MaxInt( p->nLevels, Level );
1088     return Level;
1089 }
Gia_ShowCollectObjs(Gia_Man_t * p,Vec_Int_t * vAdds,Vec_Int_t * vXors,Vec_Int_t * vMapAdds,Vec_Int_t * vMapXors)1090 Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors )
1091 {
1092     Gia_Obj_t * pObj; int i;
1093     Vec_Int_t * vOrder = Vec_IntAlloc( 100 );
1094     Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
1095     p->nLevels = 0;
1096     Gia_ManIncrementTravId( p );
1097     Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
1098     Gia_ManForEachCi( p, pObj, i )
1099         Gia_ObjSetTravIdCurrent(p, pObj);
1100     Gia_ManForEachCo( p, pObj, i )
1101         Gia_ShowCollectObjs_rec( p, Gia_ObjFanin0(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder );
1102     return vOrder;
1103 }
1104 
1105 /**Function*************************************************************
1106 
1107   Synopsis    []
1108 
1109   Description []
1110 
1111   SideEffects []
1112 
1113   SeeAlso     []
1114 
1115 ***********************************************************************/
Gia_ShowProcess(Gia_Man_t * p,char * pFileName,Vec_Int_t * vBold,Vec_Int_t * vAdds,Vec_Int_t * vXors,int fFadds)1116 void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
1117 {
1118     Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold );
1119     Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
1120     Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
1121     Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );
1122     Vec_IntFree( vMapAdds );
1123     Vec_IntFree( vMapXors );
1124     Vec_IntFree( vOrder );
1125 }
Gia_ManShow(Gia_Man_t * pMan,Vec_Int_t * vBold,int fAdders,int fFadds,int fPath)1126 void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, int fPath )
1127 {
1128     extern void Abc_ShowFile( char * FileNameDot );
1129     char FileNameDot[200];
1130     FILE * pFile;
1131     Vec_Int_t * vXors = NULL, * vAdds = fAdders ? Ree_ManComputeCuts( pMan, &vXors, 0 ) : NULL;
1132     sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName, ".dot") );
1133     // check that the file can be opened
1134     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
1135     {
1136         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
1137         return;
1138     }
1139     fclose( pFile );
1140     // generate the file
1141     if ( fPath )
1142         Gia_ShowPath( pMan, FileNameDot );
1143     else if ( fAdders )
1144         Gia_ShowProcess( pMan, FileNameDot, vBold, vAdds, vXors, fFadds );
1145     else
1146         Gia_WriteDotAigSimple( pMan, FileNameDot, vBold );
1147     // visualize the file
1148     Abc_ShowFile( FileNameDot );
1149 
1150     Vec_IntFreeP( &vAdds );
1151     Vec_IntFreeP( &vXors );
1152 }
1153 
1154 
1155 
1156 
1157 
1158 ////////////////////////////////////////////////////////////////////////
1159 ///                       END OF FILE                                ///
1160 ////////////////////////////////////////////////////////////////////////
1161 
1162 
1163 ABC_NAMESPACE_IMPL_END
1164 
1165