ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ivyShow.c
Go to the documentation of this file.
1
20
21#include "ivy.h"
22
24
25
29
30static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold );
31
35
47void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
48{
49 extern void Abc_ShowFile( char * FileNameDot, int fKeepDot );
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, 0 );
67}
68
81void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold )
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}
335
336
340
341
343
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
char * Extra_TimeStamp()
void Ivy_ManShow(Ivy_Man_t *pMan, int fHaig, Vec_Ptr_t *vBold)
FUNCTION DEFINITIONS ///.
Definition ivyShow.c:47
#define Ivy_ManForEachCo(p, pObj, i)
Definition ivy.h:399
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition ivy.h:46
#define Ivy_ManForEachObj(p, pObj, i)
Definition ivy.h:393
struct Ivy_Obj_t_ Ivy_Obj_t
Definition ivy.h:47
#define Ivy_ManForEachCi(p, pObj, i)
Definition ivy.h:396
int Ivy_ManSetLevels(Ivy_Man_t *p, int fHaig)
Definition ivyDfs.c:457
unsigned fMarkB
Definition ivy.h:79
Ivy_Obj_t * pEquiv
Definition ivy.h:93
int Id
Definition ivy.h:75
unsigned Level
Definition ivy.h:84
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