1 /**CFile****************************************************************
2
3 FileName [ioWriteSmv.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Command processing package.]
8
9 Synopsis [Procedures to write the network in SMV format.]
10
11 Author [Satrajit Chatterjee]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: ioWriteSmv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "ioAbc.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk );
31
32 static int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk );
33 static int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode );
34
35 ////////////////////////////////////////////////////////////////////////
36 /// FUNCTION DEFINITIONS ///
37 ////////////////////////////////////////////////////////////////////////
38
39 // This returns a pointer to a static area, so be careful in using results
40 // of this function i.e. don't call this twice in the same printf call.
41 //
42 // This function replaces '|' with '_' I think abc introduces '|' when
43 // flattening hierarchy. The '|' is interpreted as a or function by nusmv
44 // which is unfortunate. This probably should be fixed elsewhere.
cleanUNSAFE(const char * s)45 static char *cleanUNSAFE( const char *s )
46 {
47 char *t;
48 static char buffer[1024];
49 assert (strlen(s) < 1024);
50 strcpy(buffer, s);
51 for (t = buffer; *t != 0; ++t) *t = (*t == '|') ? '_' : *t;
52 return buffer;
53 }
54
hasPrefix(const char * needle,const char * haystack)55 static int hasPrefix(const char *needle, const char *haystack)
56 {
57 return (strncmp(haystack, needle, strlen(needle)) == 0);
58 }
59
60 /**Function*************************************************************
61
62 Synopsis [Writes the network in SMV format.]
63
64 Description []
65
66 SideEffects []
67
68 SeeAlso []
69
70 ***********************************************************************/
Io_WriteSmv(Abc_Ntk_t * pNtk,char * pFileName)71 int Io_WriteSmv( Abc_Ntk_t * pNtk, char * pFileName )
72 {
73 Abc_Ntk_t * pExdc;
74 FILE * pFile;
75 assert( Abc_NtkIsSopNetlist(pNtk) );
76 if ( !Io_WriteSmvCheckNames(pNtk) )
77 {
78 fprintf( stdout, "Io_WriteSmv(): Signal names in this benchmark contain parentheses making them impossible to reproduce in the SMV format. Use \"short_names\".\n" );
79 return 0;
80 }
81 pFile = fopen( pFileName, "w" );
82 if ( pFile == NULL )
83 {
84 fprintf( stdout, "Io_WriteSmv(): Cannot open the output file.\n" );
85 return 0;
86 }
87 fprintf( pFile, "-- benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
88 // write the network
89 Io_WriteSmvOne( pFile, pNtk );
90 // write EXDC network if it exists
91 pExdc = Abc_NtkExdc( pNtk );
92 if ( pExdc )
93 printf( "Io_WriteSmv: EXDC is not written (warning).\n" );
94 // finalize the file
95 fclose( pFile );
96 return 1;
97 }
98
99 /**Function*************************************************************
100
101 Synopsis [Writes the network in SMV format.]
102
103 Description []
104
105 SideEffects []
106
107 SeeAlso []
108
109 ***********************************************************************/
Io_WriteSmvOne(FILE * pFile,Abc_Ntk_t * pNtk)110 int Io_WriteSmvOne( FILE * pFile, Abc_Ntk_t * pNtk )
111 {
112 ProgressBar * pProgress;
113 Abc_Obj_t * pNode;
114 int i;
115
116 // write the PIs/POs/latches
117 fprintf( pFile, "MODULE main\n"); // nusmv needs top module to be main
118 fprintf ( pFile, "\n" );
119
120 fprintf( pFile, "VAR -- inputs\n");
121 Abc_NtkForEachPi( pNtk, pNode, i )
122 fprintf( pFile, " %s : boolean;\n",
123 cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
124 fprintf ( pFile, "\n" );
125
126 fprintf( pFile, "VAR -- state variables\n");
127 Abc_NtkForEachLatch( pNtk, pNode, i )
128 fprintf( pFile, " %s : boolean;\n",
129 cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) );
130 fprintf ( pFile, "\n" );
131
132 // No outputs needed for NuSMV:
133 // TODO: Add sepcs by recognizing assume_.* and assert_.*
134 //
135 // Abc_NtkForEachPo( pNtk, pNode, i )
136 // fprintf( pFile, "OUTPUT(%s)\n", Abc_ObjName(Abc_ObjFanin0(pNode)) );
137
138 // write internal nodes
139 fprintf( pFile, "DEFINE\n");
140 pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
141 Abc_NtkForEachNode( pNtk, pNode, i )
142 {
143 Extra_ProgressBarUpdate( pProgress, i, NULL );
144 Io_WriteSmvOneNode( pFile, pNode );
145 }
146 Extra_ProgressBarStop( pProgress );
147 fprintf ( pFile, "\n" );
148
149 fprintf( pFile, "ASSIGN\n");
150 Abc_NtkForEachLatch( pNtk, pNode, i )
151 {
152 int Reset = (int)(ABC_PTRUINT_T)Abc_ObjData( pNode );
153 assert (Reset >= 1);
154 assert (Reset <= 3);
155
156 if (Reset != 3)
157 {
158 fprintf( pFile, " init(%s) := %d;\n",
159 cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))),
160 Reset - 1);
161 }
162 fprintf( pFile, " next(%s) := ",
163 cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pNode)))) );
164 fprintf( pFile, "%s;\n",
165 cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(Abc_ObjFanin0(pNode)))) );
166 }
167
168 fprintf ( pFile, "\n" );
169 Abc_NtkForEachPo( pNtk, pNode, i )
170 {
171 const char *n = cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode)));
172 // fprintf( pFile, "-- output %s;\n", n );
173 if (hasPrefix("assume_fair_", n))
174 {
175 fprintf( pFile, "FAIRNESS %s;\n", n );
176 }
177 else if (hasPrefix("Assert_", n) ||
178 hasPrefix("assert_safety_", n))
179 {
180 fprintf( pFile, "INVARSPEC %s;\n", n );
181 }
182 else if (hasPrefix("assert_fair_", n))
183 {
184 fprintf( pFile, "LTLSPEC G F %s;\n", n );
185 }
186 }
187
188 return 1;
189 }
190
191 /**Function*************************************************************
192
193 Synopsis [Writes the network in SMV format.]
194
195 Description []
196
197 SideEffects []
198
199 SeeAlso []
200
201 ***********************************************************************/
Io_WriteSmvOneNode(FILE * pFile,Abc_Obj_t * pNode)202 int Io_WriteSmvOneNode( FILE * pFile, Abc_Obj_t * pNode )
203 {
204 int nFanins;
205
206 assert( Abc_ObjIsNode(pNode) );
207 nFanins = Abc_ObjFaninNum(pNode);
208 if ( nFanins == 0 )
209 { // write the constant 1 node
210 assert( Abc_NodeIsConst1(pNode) );
211 fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode)) ) );
212 fprintf( pFile, " := 1;\n" );
213 }
214 else if ( nFanins == 1 )
215 { // write the interver/buffer
216 if ( Abc_NodeIsBuf(pNode) )
217 {
218 fprintf( pFile, " %s := ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
219 fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
220 }
221 else
222 {
223 fprintf( pFile, " %s := !", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
224 fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
225 }
226 }
227 else
228 { // write the AND gate
229 fprintf( pFile, " %s", cleanUNSAFE(Abc_ObjName(Abc_ObjFanout0(pNode))) );
230 fprintf( pFile, " := %s & ", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin0(pNode))) );
231 fprintf( pFile, "%s;\n", cleanUNSAFE(Abc_ObjName(Abc_ObjFanin1(pNode))) );
232 }
233 return 1;
234 }
235
236 /**Function*************************************************************
237
238 Synopsis [Returns 1 if the names cannot be written into the bench file.]
239
240 Description []
241
242 SideEffects []
243
244 SeeAlso []
245
246 ***********************************************************************/
Io_WriteSmvCheckNames(Abc_Ntk_t * pNtk)247 int Io_WriteSmvCheckNames( Abc_Ntk_t * pNtk )
248 {
249 Abc_Obj_t * pObj;
250 char * pName;
251 int i;
252 Abc_NtkForEachObj( pNtk, pObj, i )
253 for ( pName = Nm_ManFindNameById(pNtk->pManName, i); pName && *pName; pName++ )
254 if ( *pName == '(' || *pName == ')' )
255 return 0;
256 return 1;
257 }
258
259 ////////////////////////////////////////////////////////////////////////
260 /// END OF FILE ///
261 ////////////////////////////////////////////////////////////////////////
262
263
264 ABC_NAMESPACE_IMPL_END
265
266