1 /**CFile****************************************************************
2
3 FileName [wlcAbc.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [Parses several flavors of word-level Verilog.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - August 22, 2014.]
16
17 Revision [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "wlc.h"
22 #include "base/abc/abc.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis []
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Wlc_NtkPrintInputInfo(Wlc_Ntk_t * pNtk)45 void Wlc_NtkPrintInputInfo( Wlc_Ntk_t * pNtk )
46 {
47 Wlc_Obj_t * pObj;
48 int i, k, nRange, nBeg, nEnd, nBits = 0;
49 FILE * output;
50
51 output = fopen("abc_blast_input.info","w");
52
53 Wlc_NtkForEachCi( pNtk, pObj, i )
54 {
55 nRange = Wlc_ObjRange(pObj);
56 nBeg = pObj->Beg;
57 nEnd = pObj->End;
58
59 for ( k = 0; k < nRange; k++ )
60 {
61 int index = nEnd > nBeg ? nBeg + k : nEnd + k;
62 char c = pObj->Type != WLC_OBJ_FO ? 'i' : pNtk->pInits[nBits + k];
63 fprintf(output,"%s[%d] : %c \n", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), index , c );
64 }
65 if (pObj->Type == WLC_OBJ_FO)
66 nBits += nRange;
67 }
68
69 Wlc_NtkForEachPo( pNtk, pObj, i )
70 {
71 nRange = Wlc_ObjRange(pObj);
72 nBeg = pObj->Beg;
73 nEnd = pObj->End;
74
75 for ( k = 0; k < nRange; k++ )
76 {
77 int index = nEnd > nBeg ? nBeg + k : nEnd + k;
78 fprintf(output,"%s[%d] : o \n", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), index);
79 }
80 }
81
82 fclose(output);
83 return;
84 }
85
86 /**Function*************************************************************
87
88 Synopsis []
89
90 Description []
91
92 SideEffects []
93
94 SeeAlso []
95
96 ***********************************************************************/
Wlc_NtkPrintInvStats(Wlc_Ntk_t * pNtk,Vec_Int_t * vCounts,int fVerbose)97 void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
98 {
99 Wlc_Obj_t * pObj;
100 int i, k, nNum, nRange, nBits = 0;
101 Wlc_NtkForEachCi( pNtk, pObj, i )
102 {
103 if ( pObj->Type != WLC_OBJ_FO )
104 continue;
105 nRange = Wlc_ObjRange(pObj);
106 for ( k = 0; k < nRange; k++ )
107 {
108 nNum = Vec_IntEntry(vCounts, nBits + k);
109 if ( nNum )
110 break;
111 }
112 if ( k == nRange )
113 {
114 nBits += nRange;
115 continue;
116 }
117 printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
118 for ( k = 0; k < nRange; k++ )
119 {
120 nNum = Vec_IntEntry( vCounts, nBits + k );
121 if ( nNum == 0 )
122 continue;
123 printf( " [%d] -> %d", k, nNum );
124 }
125 printf( "\n");
126 nBits += nRange;
127 }
128 //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
129 assert( Vec_IntSize(vCounts) == nBits );
130 }
131
132 /**Function*************************************************************
133
134 Synopsis []
135
136 Description []
137
138 SideEffects []
139
140 SeeAlso []
141
142 ***********************************************************************/
Wlc_NtkGetInv(Wlc_Ntk_t * pNtk,Vec_Int_t * vInv)143 Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
144 {
145 extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
146 extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
147
148 Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
149 Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
150
151 Wlc_Obj_t * pObj;
152 int i, k, nNum, nRange, nBits = 0;
153 Abc_Ntk_t * pMainNtk = NULL;
154 Abc_Obj_t * pMainObj, * pMainTemp;
155 char Buffer[5000];
156 // start the network
157 pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
158 // duplicate the name and the spec
159 pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
160 // create primary inputs
161 if ( pNtk == NULL )
162 {
163 int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
164 Vec_IntForEachEntry( vCounts, Entry, i )
165 {
166 if ( Entry == 0 )
167 continue;
168 pMainObj = Abc_NtkCreatePi( pMainNtk );
169 sprintf( Buffer, "pi%d", i );
170 Abc_ObjAssignName( pMainObj, Buffer, NULL );
171 }
172 if ( Abc_NtkPiNum(pMainNtk) != nInputs )
173 {
174 printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
175 Abc_NtkDelete( pMainNtk );
176 return NULL;
177 }
178 }
179 else
180 {
181 Wlc_NtkForEachCi( pNtk, pObj, i )
182 {
183 if ( pObj->Type != WLC_OBJ_FO )
184 continue;
185 nRange = Wlc_ObjRange(pObj);
186 for ( k = 0; k < nRange; k++ )
187 {
188 nNum = Vec_IntEntry(vCounts, nBits + k);
189 if ( nNum )
190 break;
191 }
192 if ( k == nRange )
193 {
194 nBits += nRange;
195 continue;
196 }
197 //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
198 for ( k = 0; k < nRange; k++ )
199 {
200 nNum = Vec_IntEntry( vCounts, nBits + k );
201 if ( nNum == 0 )
202 continue;
203 //printf( " [%d] -> %d", k, nNum );
204 pMainObj = Abc_NtkCreatePi( pMainNtk );
205 sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
206 Abc_ObjAssignName( pMainObj, Buffer, NULL );
207
208 }
209 //printf( "\n");
210 nBits += nRange;
211 }
212 }
213 //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
214 assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
215 // create node
216 pMainObj = Abc_NtkCreateNode( pMainNtk );
217 Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
218 Abc_ObjAddFanin( pMainObj, pMainTemp );
219 pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
220 Vec_IntFree( vCounts );
221 Vec_StrFree( vSop );
222 // create PO
223 pMainTemp = Abc_NtkCreatePo( pMainNtk );
224 Abc_ObjAddFanin( pMainTemp, pMainObj );
225 Abc_ObjAssignName( pMainTemp, "inv", NULL );
226 return pMainNtk;
227 }
228
229 /**Function*************************************************************
230
231 Synopsis [Translate current network into an invariant.]
232
233 Description []
234
235 SideEffects []
236
237 SeeAlso []
238
239 ***********************************************************************/
Wlc_NtkGetPut(Abc_Ntk_t * pNtk,Gia_Man_t * pGia)240 Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia )
241 {
242 int nRegs = Gia_ManRegNum(pGia);
243 Vec_Int_t * vRes = NULL;
244 if ( Abc_NtkPoNum(pNtk) != 1 )
245 printf( "The number of outputs is other than 1.\n" );
246 else if ( Abc_NtkNodeNum(pNtk) != 1 )
247 printf( "The number of internal nodes is other than 1.\n" );
248 else
249 {
250 Abc_Nam_t * pNames = NULL;
251 Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
252 char * pName, * pCube, * pSop = (char *)pNode->pData;
253 Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
254 int i, k, Value, nLits, Counter = 0;
255 if ( pGia->vNamesIn )
256 {
257 // hash the names
258 pNames = Abc_NamStart( 100, 16 );
259 Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i )
260 {
261 Value = Abc_NamStrFindOrAdd( pNames, pName, NULL );
262 assert( Value == i+1 );
263 //printf( "%s(%d) ", pName, i );
264 }
265 //printf( "\n" );
266 }
267 Abc_ObjForEachFanin( pNode, pFanin, i )
268 {
269 assert( Abc_ObjIsCi(pFanin) );
270 pName = Abc_ObjName(pFanin);
271 if ( pNames )
272 {
273 Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia);
274 if ( Value < 0 )
275 {
276 if ( Counter++ == 0 )
277 printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
278 Value = i;
279 }
280 }
281 else
282 {
283 for ( k = (int)strlen(pName)-1; k >= 0; k-- )
284 if ( pName[k] < '0' || pName[k] > '9' )
285 break;
286 if ( k == (int)strlen(pName)-1 )
287 {
288 if ( Counter++ == 0 )
289 printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
290 Value = i;
291 }
292 else
293 Value = atoi(pName + k + 1);
294 }
295 Vec_IntPush( vFanins, Value );
296 }
297 if ( Counter )
298 printf( "Cannot read names for %d inputs of the invariant.\n", Counter );
299 if ( pNames )
300 Abc_NamStop( pNames );
301 assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
302 vRes = Vec_IntAlloc( 1000 );
303 Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
304 Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
305 {
306 nLits = 0;
307 Abc_CubeForEachVar( pCube, Value, k )
308 if ( Value != '-' )
309 nLits++;
310 Vec_IntPush( vRes, nLits );
311 Abc_CubeForEachVar( pCube, Value, k )
312 if ( Value != '-' )
313 Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
314 }
315 Vec_IntPush( vRes, nRegs );
316 Vec_IntFree( vFanins );
317 }
318 return vRes;
319 }
320
321 ////////////////////////////////////////////////////////////////////////
322 /// END OF FILE ///
323 ////////////////////////////////////////////////////////////////////////
324
325
326 ABC_NAMESPACE_IMPL_END
327
328