ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
aigShow.c
Go to the documentation of this file.
1
20
21#include "aig.h"
22#include "misc/extra/extra.h"
23
25
26
30
34
47void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold )
48{
49 FILE * pFile;
50 Aig_Obj_t * pNode;//, * pTemp, * pPrev;
51 int LevelMax, Prev, Level, i;
52
53 if ( Aig_ManNodeNum(pMan) > 200 )
54 {
55 fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" );
56 return;
57 }
58 if ( (pFile = fopen( pFileName, "w" )) == NULL )
59 {
60 fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
61 return;
62 }
63
64 // mark the nodes
65 if ( vBold )
66 Vec_PtrForEachEntry( Aig_Obj_t *, vBold, pNode, i )
67 pNode->fMarkB = 1;
68
69 // compute levels
70// LevelMax = 1 + Aig_ManSetLevels( pMan, fHaig );
71 LevelMax = 1 + Aig_ManLevels( pMan );
72 Aig_ManForEachCo( pMan, pNode, i )
73 pNode->Level = LevelMax;
74
75 // write the DOT header
76 fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" );
77 fprintf( pFile, "\n" );
78 fprintf( pFile, "digraph AIG {\n" );
79 fprintf( pFile, "size = \"7.5,10\";\n" );
80// fprintf( pFile, "ranksep = 0.5;\n" );
81// fprintf( pFile, "nodesep = 0.5;\n" );
82 fprintf( pFile, "center = true;\n" );
83// fprintf( pFile, "orientation = landscape;\n" );
84// fprintf( pFile, "edge [fontsize = 10];\n" );
85// fprintf( pFile, "edge [dir = none];\n" );
86 fprintf( pFile, "edge [dir = back];\n" );
87 fprintf( pFile, "\n" );
88
89 // labels on the left of the picture
90 fprintf( pFile, "{\n" );
91 fprintf( pFile, " node [shape = plaintext];\n" );
92 fprintf( pFile, " edge [style = invis];\n" );
93 fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
94 fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
95 // generate node names with labels
96 for ( Level = LevelMax; Level >= 0; Level-- )
97 {
98 // the visible node name
99 fprintf( pFile, " Level%d", Level );
100 fprintf( pFile, " [label = " );
101 // label name
102 fprintf( pFile, "\"" );
103 fprintf( pFile, "\"" );
104 fprintf( pFile, "];\n" );
105 }
106
107 // genetate the sequence of visible/invisible nodes to mark levels
108 fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
109 for ( Level = LevelMax; Level >= 0; Level-- )
110 {
111 // the visible node name
112 fprintf( pFile, " Level%d", Level );
113 // the connector
114 if ( Level != 0 )
115 fprintf( pFile, " ->" );
116 else
117 fprintf( pFile, ";" );
118 }
119 fprintf( pFile, "\n" );
120 fprintf( pFile, "}" );
121 fprintf( pFile, "\n" );
122 fprintf( pFile, "\n" );
123
124 // generate title box on top
125 fprintf( pFile, "{\n" );
126 fprintf( pFile, " rank = same;\n" );
127 fprintf( pFile, " LevelTitle1;\n" );
128 fprintf( pFile, " title1 [shape=plaintext,\n" );
129 fprintf( pFile, " fontsize=20,\n" );
130 fprintf( pFile, " fontname = \"Times-Roman\",\n" );
131 fprintf( pFile, " label=\"" );
132 fprintf( pFile, "%s", "AIG structure visualized by ABC" );
133 fprintf( pFile, "\\n" );
134 fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
135// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
136 fprintf( pFile, "\"\n" );
137 fprintf( pFile, " ];\n" );
138 fprintf( pFile, "}" );
139 fprintf( pFile, "\n" );
140 fprintf( pFile, "\n" );
141
142 // generate statistics box
143 fprintf( pFile, "{\n" );
144 fprintf( pFile, " rank = same;\n" );
145 fprintf( pFile, " LevelTitle2;\n" );
146 fprintf( pFile, " title2 [shape=plaintext,\n" );
147 fprintf( pFile, " fontsize=18,\n" );
148 fprintf( pFile, " fontname = \"Times-Roman\",\n" );
149 fprintf( pFile, " label=\"" );
150 fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Aig_ManNodeNum(pMan), LevelMax );
151 fprintf( pFile, "\\n" );
152 fprintf( pFile, "\"\n" );
153 fprintf( pFile, " ];\n" );
154 fprintf( pFile, "}" );
155 fprintf( pFile, "\n" );
156 fprintf( pFile, "\n" );
157
158 // generate the COs
159 fprintf( pFile, "{\n" );
160 fprintf( pFile, " rank = same;\n" );
161 // the labeling node of this level
162 fprintf( pFile, " Level%d;\n", LevelMax );
163 // generate the CO nodes
164 Aig_ManForEachCo( pMan, pNode, i )
165 {
166/*
167 if ( fHaig || pNode->pEquiv == NULL )
168 fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
169 (Aig_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") );
170 else
171 fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
172 (Aig_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":""),
173 Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" );
174*/
175 fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
176
177 fprintf( pFile, ", shape = %s", "invtriangle" );
178 fprintf( pFile, ", color = coral, fillcolor = coral" );
179 fprintf( pFile, "];\n" );
180 }
181 fprintf( pFile, "}" );
182 fprintf( pFile, "\n" );
183 fprintf( pFile, "\n" );
184
185 // generate nodes of each rank
186 for ( Level = LevelMax - 1; Level > 0; Level-- )
187 {
188 fprintf( pFile, "{\n" );
189 fprintf( pFile, " rank = same;\n" );
190 // the labeling node of this level
191 fprintf( pFile, " Level%d;\n", Level );
192 Aig_ManForEachObj( pMan, pNode, i )
193 {
194 if ( (int)pNode->Level != Level )
195 continue;
196/*
197 if ( fHaig || pNode->pEquiv == NULL )
198 fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
199 else
200 fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
201 Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" );
202*/
203 fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
204
205 fprintf( pFile, ", shape = ellipse" );
206 if ( vBold && pNode->fMarkB )
207 fprintf( pFile, ", style = filled" );
208 fprintf( pFile, "];\n" );
209 }
210 fprintf( pFile, "}" );
211 fprintf( pFile, "\n" );
212 fprintf( pFile, "\n" );
213 }
214
215 // generate the CI nodes
216 fprintf( pFile, "{\n" );
217 fprintf( pFile, " rank = same;\n" );
218 // the labeling node of this level
219 fprintf( pFile, " Level%d;\n", 0 );
220 // generate constant node
221 if ( Aig_ObjRefs(Aig_ManConst1(pMan)) > 0 )
222 {
223 pNode = Aig_ManConst1(pMan);
224 // check if the costant node is present
225 fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id );
226 fprintf( pFile, ", shape = ellipse" );
227 fprintf( pFile, ", color = coral, fillcolor = coral" );
228 fprintf( pFile, "];\n" );
229 }
230 // generate the CI nodes
231 Aig_ManForEachCi( pMan, pNode, i )
232 {
233/*
234 if ( fHaig || pNode->pEquiv == NULL )
235 fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id,
236 (Aig_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_out":"") );
237 else
238 fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id,
239 (Aig_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Aig_ObjIsLatch(pNode)? "_out":""),
240 Aig_Regular(pNode->pEquiv)->Id, Aig_IsComplement(pNode->pEquiv)? "\'":"" );
241*/
242 fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
243
244 fprintf( pFile, ", shape = %s", "triangle" );
245 fprintf( pFile, ", color = coral, fillcolor = coral" );
246 fprintf( pFile, "];\n" );
247 }
248 fprintf( pFile, "}" );
249 fprintf( pFile, "\n" );
250 fprintf( pFile, "\n" );
251
252 // generate invisible edges from the square down
253 fprintf( pFile, "title1 -> title2 [style = invis];\n" );
254 Aig_ManForEachCo( pMan, pNode, i )
255 fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
256 // generate invisible edges among the COs
257 Prev = -1;
258 Aig_ManForEachCo( pMan, pNode, i )
259 {
260 if ( i > 0 )
261 fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, pNode->Id );
262 Prev = pNode->Id;
263 }
264
265 // generate edges
266 Aig_ManForEachObj( pMan, pNode, i )
267 {
268 if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsCo(pNode) && !Aig_ObjIsBuf(pNode) )
269 continue;
270 // generate the edge from this node to the next
271 fprintf( pFile, "Node%d", pNode->Id );
272 fprintf( pFile, " -> " );
273 fprintf( pFile, "Node%d", Aig_ObjFaninId0(pNode) );
274 fprintf( pFile, " [" );
275 fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" );
276// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
277// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
278 fprintf( pFile, "]" );
279 fprintf( pFile, ";\n" );
280 if ( !Aig_ObjIsNode(pNode) )
281 continue;
282 // generate the edge from this node to the next
283 fprintf( pFile, "Node%d", pNode->Id );
284 fprintf( pFile, " -> " );
285 fprintf( pFile, "Node%d", Aig_ObjFaninId1(pNode) );
286 fprintf( pFile, " [" );
287 fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" );
288// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
289// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
290 fprintf( pFile, "]" );
291 fprintf( pFile, ";\n" );
292/*
293 // generate the edges between the equivalent nodes
294 if ( fHaig && pNode->pEquiv && Aig_ObjRefs(pNode) > 0 )
295 {
296 pPrev = pNode;
297 for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Aig_Regular(pTemp->pEquiv) )
298 {
299 fprintf( pFile, "Node%d", pPrev->Id );
300 fprintf( pFile, " -> " );
301 fprintf( pFile, "Node%d", pTemp->Id );
302 fprintf( pFile, " [style = %s]", Aig_IsComplement(pTemp->pEquiv)? "dotted" : "bold" );
303 fprintf( pFile, ";\n" );
304 pPrev = pTemp;
305 }
306 // connect the last node with the first
307 fprintf( pFile, "Node%d", pPrev->Id );
308 fprintf( pFile, " -> " );
309 fprintf( pFile, "Node%d", pNode->Id );
310 fprintf( pFile, " [style = %s]", Aig_IsComplement(pPrev->pEquiv)? "dotted" : "bold" );
311 fprintf( pFile, ";\n" );
312 }
313*/
314 }
315
316 fprintf( pFile, "}" );
317 fprintf( pFile, "\n" );
318 fprintf( pFile, "\n" );
319 fclose( pFile );
320
321 // unmark nodes
322 if ( vBold )
323 Vec_PtrForEachEntry( Aig_Obj_t *, vBold, pNode, i )
324 pNode->fMarkB = 0;
325
326 Aig_ManForEachCo( pMan, pNode, i )
327 pNode->Level = Aig_ObjFanin0(pNode)->Level;
328}
329
341void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
342{
343 extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
344 char FileNameDot[200];
345 FILE * pFile;
346 // create the file name
347 sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName ? pMan->pName : (char *)"unknown", ".dot") );
348 // check that the file can be opened
349 if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
350 {
351 fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
352 return;
353 }
354 fclose( pFile );
355 // generate the file
356 Aig_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
357 // visualize the file
358 Abc_ShowFile( FileNameDot, 0 );
359}
360
361
365
366
368
ABC_NAMESPACE_IMPL_START void Abc_ShowFile(char *FileNameDot, int fKeepDot)
DECLARATIONS ///.
Definition abcShow.c:326
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START void Aig_WriteDotAig(Aig_Man_t *pMan, char *pFileName, int fHaig, Vec_Ptr_t *vBold)
DECLARATIONS ///.
Definition aigShow.c:47
void Aig_ManShow(Aig_Man_t *pMan, int fHaig, Vec_Ptr_t *vBold)
Definition aigShow.c:341
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
int Aig_ManLevels(Aig_Man_t *p)
Definition aigUtil.c:102
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
int Id
Definition aig.h:85
unsigned int fMarkB
Definition aig.h:80
unsigned Level
Definition aig.h:82
char * sprintf()
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55