#include "ivy.h"
Go to the source code of this file.
Functions | |
static void | Ivy_WriteDotAig (Ivy_Man_t *pMan, char *pFileName, int fHaig, Vec_Ptr_t *vBold) |
void | Ivy_ManShow (Ivy_Man_t *pMan, int fHaig, Vec_Ptr_t *vBold) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 44 of file ivyShow.c.
00045 { 00046 extern void Abc_ShowFile( char * FileNameDot ); 00047 static Counter = 0; 00048 char FileNameDot[200]; 00049 FILE * pFile; 00050 // create the file name 00051 // Ivy_ShowGetFileName( pMan->pName, FileNameDot ); 00052 sprintf( FileNameDot, "temp%02d.dot", Counter++ ); 00053 // check that the file can be opened 00054 if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) 00055 { 00056 fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); 00057 return; 00058 } 00059 fclose( pFile ); 00060 // generate the file 00061 Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); 00062 // visualize the file 00063 Abc_ShowFile( FileNameDot ); 00064 }
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 [
] DECLARATIONS ///
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 78 of file ivyShow.c.
00079 { 00080 FILE * pFile; 00081 Ivy_Obj_t * pNode, * pTemp, * pPrev; 00082 int LevelMax, Level, i; 00083 00084 if ( Ivy_ManNodeNum(pMan) > 200 ) 00085 { 00086 fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" ); 00087 return; 00088 } 00089 if ( (pFile = fopen( pFileName, "w" )) == NULL ) 00090 { 00091 fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); 00092 return; 00093 } 00094 00095 // mark the nodes 00096 if ( vBold ) 00097 Vec_PtrForEachEntry( vBold, pNode, i ) 00098 pNode->fMarkB = 1; 00099 00100 // compute levels 00101 LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig ); 00102 00103 // write the DOT header 00104 fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" ); 00105 fprintf( pFile, "\n" ); 00106 fprintf( pFile, "digraph AIG {\n" ); 00107 fprintf( pFile, "size = \"7.5,10\";\n" ); 00108 // fprintf( pFile, "ranksep = 0.5;\n" ); 00109 // fprintf( pFile, "nodesep = 0.5;\n" ); 00110 fprintf( pFile, "center = true;\n" ); 00111 // fprintf( pFile, "orientation = landscape;\n" ); 00112 // fprintf( pFile, "edge [fontsize = 10];\n" ); 00113 // fprintf( pFile, "edge [dir = none];\n" ); 00114 fprintf( pFile, "edge [dir = back];\n" ); 00115 fprintf( pFile, "\n" ); 00116 00117 // labels on the left of the picture 00118 fprintf( pFile, "{\n" ); 00119 fprintf( pFile, " node [shape = plaintext];\n" ); 00120 fprintf( pFile, " edge [style = invis];\n" ); 00121 fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); 00122 fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); 00123 // generate node names with labels 00124 for ( Level = LevelMax; Level >= 0; Level-- ) 00125 { 00126 // the visible node name 00127 fprintf( pFile, " Level%d", Level ); 00128 fprintf( pFile, " [label = " ); 00129 // label name 00130 fprintf( pFile, "\"" ); 00131 fprintf( pFile, "\"" ); 00132 fprintf( pFile, "];\n" ); 00133 } 00134 00135 // genetate the sequence of visible/invisible nodes to mark levels 00136 fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); 00137 for ( Level = LevelMax; Level >= 0; Level-- ) 00138 { 00139 // the visible node name 00140 fprintf( pFile, " Level%d", Level ); 00141 // the connector 00142 if ( Level != 0 ) 00143 fprintf( pFile, " ->" ); 00144 else 00145 fprintf( pFile, ";" ); 00146 } 00147 fprintf( pFile, "\n" ); 00148 fprintf( pFile, "}" ); 00149 fprintf( pFile, "\n" ); 00150 fprintf( pFile, "\n" ); 00151 00152 // generate title box on top 00153 fprintf( pFile, "{\n" ); 00154 fprintf( pFile, " rank = same;\n" ); 00155 fprintf( pFile, " LevelTitle1;\n" ); 00156 fprintf( pFile, " title1 [shape=plaintext,\n" ); 00157 fprintf( pFile, " fontsize=20,\n" ); 00158 fprintf( pFile, " fontname = \"Times-Roman\",\n" ); 00159 fprintf( pFile, " label=\"" ); 00160 fprintf( pFile, "%s", "AIG structure visualized by ABC" ); 00161 fprintf( pFile, "\\n" ); 00162 fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" ); 00163 fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); 00164 fprintf( pFile, "\"\n" ); 00165 fprintf( pFile, " ];\n" ); 00166 fprintf( pFile, "}" ); 00167 fprintf( pFile, "\n" ); 00168 fprintf( pFile, "\n" ); 00169 00170 // generate statistics box 00171 fprintf( pFile, "{\n" ); 00172 fprintf( pFile, " rank = same;\n" ); 00173 fprintf( pFile, " LevelTitle2;\n" ); 00174 fprintf( pFile, " title2 [shape=plaintext,\n" ); 00175 fprintf( pFile, " fontsize=18,\n" ); 00176 fprintf( pFile, " fontname = \"Times-Roman\",\n" ); 00177 fprintf( pFile, " label=\"" ); 00178 fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Ivy_ManNodeNum(pMan), LevelMax ); 00179 fprintf( pFile, "\\n" ); 00180 fprintf( pFile, "\"\n" ); 00181 fprintf( pFile, " ];\n" ); 00182 fprintf( pFile, "}" ); 00183 fprintf( pFile, "\n" ); 00184 fprintf( pFile, "\n" ); 00185 00186 // generate the COs 00187 fprintf( pFile, "{\n" ); 00188 fprintf( pFile, " rank = same;\n" ); 00189 // the labeling node of this level 00190 fprintf( pFile, " Level%d;\n", LevelMax ); 00191 // generate the CO nodes 00192 Ivy_ManForEachCo( pMan, pNode, i ) 00193 { 00194 if ( fHaig || pNode->pEquiv == NULL ) 00195 fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id, 00196 (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") ); 00197 else 00198 fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, 00199 (Ivy_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":""), 00200 Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" ); 00201 fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"invtriangle") ); 00202 fprintf( pFile, ", color = coral, fillcolor = coral" ); 00203 fprintf( pFile, "];\n" ); 00204 } 00205 fprintf( pFile, "}" ); 00206 fprintf( pFile, "\n" ); 00207 fprintf( pFile, "\n" ); 00208 00209 // generate nodes of each rank 00210 for ( Level = LevelMax - 1; Level > 0; Level-- ) 00211 { 00212 fprintf( pFile, "{\n" ); 00213 fprintf( pFile, " rank = same;\n" ); 00214 // the labeling node of this level 00215 fprintf( pFile, " Level%d;\n", Level ); 00216 Ivy_ManForEachObj( pMan, pNode, i ) 00217 { 00218 if ( (int)pNode->Level != Level ) 00219 continue; 00220 if ( fHaig || pNode->pEquiv == NULL ) 00221 fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); 00222 else 00223 fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, 00224 Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" ); 00225 fprintf( pFile, ", shape = ellipse" ); 00226 if ( vBold && pNode->fMarkB ) 00227 fprintf( pFile, ", style = filled" ); 00228 fprintf( pFile, "];\n" ); 00229 } 00230 fprintf( pFile, "}" ); 00231 fprintf( pFile, "\n" ); 00232 fprintf( pFile, "\n" ); 00233 } 00234 00235 // generate the CI nodes 00236 fprintf( pFile, "{\n" ); 00237 fprintf( pFile, " rank = same;\n" ); 00238 // the labeling node of this level 00239 fprintf( pFile, " Level%d;\n", 0 ); 00240 // generate constant node 00241 if ( Ivy_ObjRefs(Ivy_ManConst1(pMan)) > 0 ) 00242 { 00243 pNode = Ivy_ManConst1(pMan); 00244 // check if the costant node is present 00245 fprintf( pFile, " Node%d [label = \"Const1\"", pNode->Id ); 00246 fprintf( pFile, ", shape = ellipse" ); 00247 fprintf( pFile, ", color = coral, fillcolor = coral" ); 00248 fprintf( pFile, "];\n" ); 00249 } 00250 // generate the CI nodes 00251 Ivy_ManForEachCi( pMan, pNode, i ) 00252 { 00253 if ( fHaig || pNode->pEquiv == NULL ) 00254 fprintf( pFile, " Node%d%s [label = \"%d%s\"", pNode->Id, 00255 (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":"") ); 00256 else 00257 fprintf( pFile, " Node%d%s [label = \"%d%s(%d%s)\"", pNode->Id, 00258 (Ivy_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Ivy_ObjIsLatch(pNode)? "_out":""), 00259 Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" ); 00260 fprintf( pFile, ", shape = %s", (Ivy_ObjIsLatch(pNode)? "box":"triangle") ); 00261 fprintf( pFile, ", color = coral, fillcolor = coral" ); 00262 fprintf( pFile, "];\n" ); 00263 } 00264 fprintf( pFile, "}" ); 00265 fprintf( pFile, "\n" ); 00266 fprintf( pFile, "\n" ); 00267 00268 // generate invisible edges from the square down 00269 fprintf( pFile, "title1 -> title2 [style = invis];\n" ); 00270 Ivy_ManForEachCo( pMan, pNode, i ) 00271 fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") ); 00272 00273 // generate edges 00274 Ivy_ManForEachObj( pMan, pNode, i ) 00275 { 00276 if ( !Ivy_ObjIsNode(pNode) && !Ivy_ObjIsCo(pNode) && !Ivy_ObjIsBuf(pNode) ) 00277 continue; 00278 // generate the edge from this node to the next 00279 fprintf( pFile, "Node%d%s", pNode->Id, (Ivy_ObjIsLatch(pNode)? "_in":"") ); 00280 fprintf( pFile, " -> " ); 00281 fprintf( pFile, "Node%d%s", Ivy_ObjFaninId0(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin0(pNode))? "_out":"") ); 00282 fprintf( pFile, " [" ); 00283 fprintf( pFile, "style = %s", Ivy_ObjFaninC0(pNode)? "dotted" : "bold" ); 00284 // if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) 00285 // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) ); 00286 fprintf( pFile, "]" ); 00287 fprintf( pFile, ";\n" ); 00288 if ( !Ivy_ObjIsNode(pNode) ) 00289 continue; 00290 // generate the edge from this node to the next 00291 fprintf( pFile, "Node%d", pNode->Id ); 00292 fprintf( pFile, " -> " ); 00293 fprintf( pFile, "Node%d%s", Ivy_ObjFaninId1(pNode), (Ivy_ObjIsLatch(Ivy_ObjFanin1(pNode))? "_out":"") ); 00294 fprintf( pFile, " [" ); 00295 fprintf( pFile, "style = %s", Ivy_ObjFaninC1(pNode)? "dotted" : "bold" ); 00296 // if ( Ivy_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) 00297 // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) ); 00298 fprintf( pFile, "]" ); 00299 fprintf( pFile, ";\n" ); 00300 // generate the edges between the equivalent nodes 00301 if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 ) 00302 { 00303 pPrev = pNode; 00304 for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) ) 00305 { 00306 fprintf( pFile, "Node%d", pPrev->Id ); 00307 fprintf( pFile, " -> " ); 00308 fprintf( pFile, "Node%d", pTemp->Id ); 00309 fprintf( pFile, " [style = %s]", Ivy_IsComplement(pTemp->pEquiv)? "dotted" : "bold" ); 00310 fprintf( pFile, ";\n" ); 00311 pPrev = pTemp; 00312 } 00313 // connect the last node with the first 00314 fprintf( pFile, "Node%d", pPrev->Id ); 00315 fprintf( pFile, " -> " ); 00316 fprintf( pFile, "Node%d", pNode->Id ); 00317 fprintf( pFile, " [style = %s]", Ivy_IsComplement(pPrev->pEquiv)? "dotted" : "bold" ); 00318 fprintf( pFile, ";\n" ); 00319 } 00320 } 00321 00322 fprintf( pFile, "}" ); 00323 fprintf( pFile, "\n" ); 00324 fprintf( pFile, "\n" ); 00325 fclose( pFile ); 00326 00327 // unmark nodes 00328 if ( vBold ) 00329 Vec_PtrForEachEntry( vBold, pNode, i ) 00330 pNode->fMarkB = 0; 00331 }