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