1 /**CFile****************************************************************
2
3 FileName [wlcMem.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [Memory abstraction.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - August 22, 2014.]
16
17 Revision [$Id: wlcMem.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "wlc.h"
22 #include "sat/bsat/satStore.h"
23 #include "proof/pdr/pdr.h"
24 #include "proof/pdr/pdrInt.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis [Memory blasting.]
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Wlc_NtkMemBlast_rec(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,int iObj,Vec_Int_t * vFanins)47 void Wlc_NtkMemBlast_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
48 {
49 Wlc_Obj_t * pObj;
50 int i, iFanin;
51 if ( Wlc_ObjCopy(p, iObj) )
52 return;
53 pObj = Wlc_NtkObj( p, iObj );
54 Wlc_ObjForEachFanin( pObj, iFanin, i )
55 Wlc_NtkMemBlast_rec( pNew, p, iFanin, vFanins );
56 if ( pObj->Type == WLC_OBJ_WRITE )
57 {
58 Vec_Int_t * vTemp = Vec_IntAlloc( 1 );
59 Vec_Int_t * vBits = Vec_IntAlloc( 100 );
60 Wlc_Obj_t * pMem = Wlc_ObjFanin0(p, pObj);
61 Wlc_Obj_t * pAddr = Wlc_ObjFanin1(p, pObj);
62 Wlc_Obj_t * pData = Wlc_ObjFanin2(p, pObj);
63 int DataW = Wlc_ObjRange(pData);
64 int AddrW = Wlc_ObjRange(pAddr);
65 int nRegs = 1 << AddrW, iObjNew, iObjDec;
66 assert( nRegs * DataW == Wlc_ObjRange(pMem) );
67 assert( Wlc_ObjRange(pObj) == Wlc_ObjRange(pMem) );
68 // create decoder
69 iObjDec = Wlc_ObjAlloc( pNew, WLC_OBJ_DEC, 0, nRegs-1, 0 );
70 Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pAddr)) );
71 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjDec), vTemp );
72 // create decoder bits
73 for ( i = 0; i < nRegs; i++ )
74 {
75 int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i, i );
76 Vec_IntFill( vTemp, 1, iObjDec );
77 Vec_IntPushTwo( vTemp, i, i );
78 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
79 Vec_IntPush( vBits, iObj2 );
80 }
81 // create data words
82 Vec_IntClear( vFanins );
83 for ( i = 0; i < nRegs; i++ )
84 {
85 int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i*DataW+DataW-1, i*DataW );
86 Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pMem)) );
87 Vec_IntPushTwo( vTemp, i*DataW+DataW-1, i*DataW );
88 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
89 Vec_IntPush( vFanins, iObj2 );
90 }
91 // create MUXes of data words controlled by decoder bits
92 for ( i = 0; i < nRegs; i++ )
93 {
94 int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, DataW-1, 0 );
95 Vec_IntFill( vTemp, 1, Vec_IntEntry(vBits, i) );
96 Vec_IntPushTwo( vTemp, Wlc_ObjCopy(p, Wlc_ObjId(p, pData)), Vec_IntEntry(vFanins, i) );
97 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
98 Vec_IntWriteEntry( vFanins, i, iObj2 );
99 }
100 // concatenate the results
101 iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_CONCAT, 0, nRegs*DataW-1, 0 );
102 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
103 Wlc_ObjSetCopy( p, iObj, iObjNew );
104 Vec_IntFree( vTemp );
105 Vec_IntFree( vBits );
106 }
107 else if ( pObj->Type == WLC_OBJ_READ )
108 {
109 Vec_Int_t * vTemp = Vec_IntAlloc( 1 );
110 Wlc_Obj_t * pMem = Wlc_ObjFanin0(p, pObj);
111 Wlc_Obj_t * pAddr = Wlc_ObjFanin1(p, pObj);
112 int DataW = Wlc_ObjRange(pObj);
113 int AddrW = Wlc_ObjRange(pAddr);
114 int nRegs = 1 << AddrW, iObjNew;
115 assert( nRegs * DataW == Wlc_ObjRange(pMem) );
116 Vec_IntClear( vFanins );
117 Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjId(p, pAddr)) );
118 for ( i = 0; i < nRegs; i++ )
119 {
120 int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i*DataW+DataW-1, i*DataW );
121 Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pMem)) );
122 Vec_IntPushTwo( vTemp, i*DataW+DataW-1, i*DataW );
123 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
124 Vec_IntPush( vFanins, iObj2 );
125 }
126 iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, DataW-1, 0 );
127 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
128 Wlc_ObjSetCopy( p, iObj, iObjNew );
129 Vec_IntFree( vTemp );
130 }
131 else
132 Wlc_ObjDup( pNew, p, iObj, vFanins );
133 }
Wlc_NtkMemBlast(Wlc_Ntk_t * p)134 Wlc_Ntk_t * Wlc_NtkMemBlast( Wlc_Ntk_t * p )
135 {
136 Wlc_Ntk_t * pNew;
137 Wlc_Obj_t * pObj;
138 Vec_Int_t * vFanins;
139 int i;
140 Wlc_NtkCleanCopy( p );
141 vFanins = Vec_IntAlloc( 100 );
142 pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
143 pNew->fSmtLib = p->fSmtLib;
144 pNew->fAsyncRst = p->fAsyncRst;
145 pNew->fMemPorts = p->fMemPorts;
146 pNew->fEasyFfs = p->fEasyFfs;
147 Wlc_NtkForEachCi( p, pObj, i )
148 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
149 Wlc_NtkForEachCo( p, pObj, i )
150 Wlc_NtkMemBlast_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
151 Wlc_NtkForEachCo( p, pObj, i )
152 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
153 if ( p->vInits )
154 pNew->vInits = Vec_IntDup( p->vInits );
155 if ( p->pInits )
156 pNew->pInits = Abc_UtilStrsav( p->pInits );
157 Vec_IntFree( vFanins );
158 if ( p->pSpec )
159 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
160 return pNew;
161 }
162
163
164 /**Function*************************************************************
165
166 Synopsis [Collect memory nodes.]
167
168 Description []
169
170 SideEffects []
171
172 SeeAlso []
173
174 ***********************************************************************/
Wlc_NtkCollectMemSizes(Wlc_Ntk_t * p)175 Vec_Int_t * Wlc_NtkCollectMemSizes( Wlc_Ntk_t * p )
176 {
177 Wlc_Obj_t * pObj; int i;
178 Vec_Int_t * vMemSizes = Vec_IntAlloc( 10 );
179 Wlc_NtkForEachObj( p, pObj, i )
180 {
181 if ( Wlc_ObjType(pObj) != WLC_OBJ_WRITE && Wlc_ObjType(pObj) != WLC_OBJ_READ )
182 continue;
183 pObj = Wlc_ObjFanin( p, pObj, 0 );
184 Vec_IntPushUnique( vMemSizes, Wlc_ObjRange(pObj) );
185 }
186 return vMemSizes;
187 }
188 // remove PIs without fanout, non-driven object and their fanouts
Wlc_ObjCheckIsEmpty_rec(Wlc_Ntk_t * p,Wlc_Obj_t * pObj)189 int Wlc_ObjCheckIsEmpty_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
190 {
191 int k, iFanin;
192 if ( Wlc_ObjType(pObj) == 0 )
193 return 1;
194 if ( Wlc_ObjIsPi(pObj) )
195 return Vec_IntEntry(&p->vRefs, Wlc_ObjId(p, pObj)) == 0;
196 else if ( Wlc_ObjIsCi(pObj) )
197 return 0;
198 Wlc_ObjForEachFanin( pObj, iFanin, k )
199 if ( !Wlc_ObjCheckIsEmpty_rec(p, Wlc_NtkObj(p, iFanin)) )
200 return 0;
201 return 1;
202 }
Wlc_NtkCleanObjects(Wlc_Ntk_t * p,Vec_Int_t * vObjs)203 Vec_Int_t * Wlc_NtkCleanObjects( Wlc_Ntk_t * p, Vec_Int_t * vObjs )
204 {
205 Wlc_Obj_t * pObj; int i;
206 Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
207 Wlc_NtkSetRefs( p );
208 Wlc_NtkForEachObjVec( vObjs, p, pObj, i )
209 {
210 //printf( "Considering %d (%s)\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
211 if ( !Wlc_ObjCheckIsEmpty_rec(p, pObj) )
212 Vec_IntPush( vMemObjs, Wlc_ObjId(p, pObj) );
213 }
214 return vMemObjs;
215 }
Wlc_NtkCollectMemory(Wlc_Ntk_t * p,int fClean)216 Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p, int fClean )
217 {
218 Wlc_Obj_t * pObj; int i;
219 Vec_Int_t * vMemSizes = Wlc_NtkCollectMemSizes( p );
220 Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
221 Wlc_NtkForEachObj( p, pObj, i )
222 {
223 if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE || Wlc_ObjType(pObj) == WLC_OBJ_READ )
224 Vec_IntPush( vMemObjs, i );
225 else if ( Vec_IntFind(vMemSizes, Wlc_ObjRange(pObj)) >= 0 )
226 Vec_IntPush( vMemObjs, i );
227 }
228 Vec_IntFree( vMemSizes );
229 Vec_IntSort( vMemObjs, 0 );
230 //Wlc_NtkPrintNodeArray( p, vMemObjs );
231 if ( fClean )
232 {
233 Vec_Int_t * vTemp;
234 vMemObjs = Wlc_NtkCleanObjects( p, vTemp = vMemObjs );
235 Vec_IntFree( vTemp );
236 }
237 return vMemObjs;
238 }
Wlc_NtkPrintMemory(Wlc_Ntk_t * p)239 void Wlc_NtkPrintMemory( Wlc_Ntk_t * p )
240 {
241 Vec_Int_t * vMemory;
242 vMemory = Wlc_NtkCollectMemory( p, 1 );
243 printf( "Memory subsystem is composed of the following objects:\n" );
244 Wlc_NtkPrintNodeArray( p, vMemory );
245 Vec_IntFree( vMemory );
246 }
247
248 /**Function*************************************************************
249
250 Synopsis [Collect fanins of memory subsystem.]
251
252 Description []
253
254 SideEffects []
255
256 SeeAlso []
257
258 ***********************************************************************/
Wlc_NtkCollectMemFanins(Wlc_Ntk_t * p,Vec_Int_t * vMemObjs)259 Vec_Int_t * Wlc_NtkCollectMemFanins( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs )
260 {
261 Wlc_Obj_t * pObj; int i, k, iFanin;
262 Vec_Int_t * vMemFanins = Vec_IntAlloc( 100 );
263 Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
264 {
265 if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
266 Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
267 else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
268 {
269 Wlc_ObjForEachFanin( pObj, iFanin, k )
270 if ( k > 0 )
271 Vec_IntPush( vMemFanins, iFanin );
272 }
273 }
274 return vMemFanins;
275 }
276
277 /**Function*************************************************************
278
279 Synopsis [Abstract memory nodes.]
280
281 Description []
282
283 SideEffects []
284
285 SeeAlso []
286
287 ***********************************************************************/
Wlc_CountDcs(char * pInit)288 int Wlc_CountDcs( char * pInit )
289 {
290 int Count = 0;
291 for ( ; *pInit; pInit++ )
292 Count += (*pInit == 'x' || *pInit == 'X');
293 return Count;
294 }
Wlc_NtkDupOneObject(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Wlc_Obj_t * pObj,int TypeNew,Vec_Int_t * vFanins)295 int Wlc_NtkDupOneObject( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int TypeNew, Vec_Int_t * vFanins )
296 {
297 int iObj = Wlc_ObjId(p, pObj);
298 unsigned Type = pObj->Type;
299 int iObjNew, nFanins = Wlc_ObjFaninNum(pObj);
300 int iObjCopy = Wlc_ObjCopy(p, iObj);
301 pObj->Type = TypeNew;
302 pObj->nFanins = 0;
303 iObjNew = Wlc_ObjDup( pNew, p, iObj, vFanins );
304 pObj->Type = Type;
305 pObj->nFanins = (unsigned)nFanins;
306 if ( TypeNew == WLC_OBJ_FO )
307 {
308 Vec_IntPush( pNew->vInits, -Wlc_ObjRange(pObj) );
309 Wlc_ObjSetCopy( p, iObj, iObjCopy );
310 }
311 return iObjNew;
312 }
Wlc_NtkDupOneBuffer(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Wlc_Obj_t * pObj,int iFanin,Vec_Int_t * vFanins,int fIsFi)313 void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFanin, Vec_Int_t * vFanins, int fIsFi )
314 {
315 int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
316 Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
317 Vec_IntFill( vFanins, 1, iFanin );
318 Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
319 Wlc_ObjSetCo( pNew, pObjNew, fIsFi );
320 }
321
Wlc_NtkAbsAddToNodeFrames(Vec_Int_t * vNodeFrames,Vec_Int_t * vLevel)322 void Wlc_NtkAbsAddToNodeFrames( Vec_Int_t * vNodeFrames, Vec_Int_t * vLevel )
323 {
324 int i, Entry;
325 Vec_IntForEachEntry( vLevel, Entry, i )
326 Vec_IntPushUnique( vNodeFrames, Entry );
327 Vec_IntSort( vNodeFrames, 0 );
328 }
Wlc_NtkAbsCreateFlopOutputs(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Vec_Int_t * vNodeFrames,Vec_Int_t * vFanins)329 Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins )
330 {
331 Vec_Int_t * vNewObjs = Vec_IntAlloc( 2*Vec_IntSize(vNodeFrames) );
332 Wlc_Obj_t * pObj, * pFanin = NULL;
333 int i, Entry, iObj, iFrame;
334 Vec_IntForEachEntry( vNodeFrames, Entry, i )
335 {
336 iObj = Entry >> 11;
337 iFrame = (Entry >> 1) & 0x3FF;
338 pObj = Wlc_NtkObj( p, iObj );
339 // address
340 if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
341 pFanin = Wlc_ObjFanin0(p, pObj);
342 else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
343 pFanin = Wlc_ObjFanin1(p, pObj);
344 else assert( 0 );
345 Vec_IntPush( vNewObjs, Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) );
346 // data
347 if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
348 pFanin = NULL;
349 else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
350 pFanin = pObj;
351 else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
352 pFanin = Wlc_ObjFanin2(p, pObj);
353 else assert( 0 );
354 Vec_IntPush( vNewObjs, pFanin ? Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) : 0 );
355 }
356 assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
357 return vNewObjs;
358 }
Wlc_NtkAbsCreateFlopInputs(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Vec_Int_t * vNodeFrames,Vec_Int_t * vFanins,Vec_Int_t * vNewObjs,Wlc_Obj_t * pCounter,int AdderBits)359 void Wlc_NtkAbsCreateFlopInputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Wlc_Obj_t * pCounter, int AdderBits )
360 {
361 Wlc_Obj_t * pObj, * pFanin, * pFlop, * pCond, * pMux, * pConst;
362 int i, n, Entry, Value, iObj, iFrame;
363 Vec_IntForEachEntry( vNodeFrames, Entry, i )
364 {
365 Value = Entry & 1;
366 iObj = Entry >> 11;
367 iFrame = (Entry >> 1) & 0x3FF;
368 pObj = Wlc_NtkObj( p, iObj );
369 for ( n = 0; n < 2; n++ ) // n=0 -- address n=1 -- data
370 {
371 pFlop = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*i+n) );
372 if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
373 pFanin = Wlc_ObjCopyObj( pNew, p, n ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj) );
374 else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
375 pFanin = n ? Wlc_NtkObj(pNew, Wlc_ObjCopy(p, iObj)) : Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin1(p, pObj) );
376 else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
377 {
378 if ( n ) continue;
379 pFanin = Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin0(p, pObj) );
380 if ( Value )
381 {
382 Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pFanin) );
383 pFanin = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_NOT, 0, 0, 0));
384 Wlc_ObjAddFanins( pNew, pFanin, vFanins );
385 }
386 }
387 else assert( 0 );
388 assert( Wlc_ObjRange(pFlop) == Wlc_ObjRange(pFanin) );
389 // create constant
390 pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
391 Vec_IntFill( vFanins, 1, iFrame );
392 Wlc_ObjAddFanins( pNew, pConst, vFanins );
393 // create equality
394 pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0));
395 Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pConst), Wlc_ObjId(pNew, pCounter) );
396 Wlc_ObjAddFanins( pNew, pCond, vFanins );
397 // create MUX
398 pMux = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pFlop)-1, 0));
399 Vec_IntClear( vFanins );
400 Vec_IntPush( vFanins, Wlc_ObjId(pNew, pCond) );
401 Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFlop) );
402 Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFanin) );
403 Wlc_ObjAddFanins( pNew, pMux, vFanins );
404 Wlc_ObjSetCo( pNew, pMux, 1 );
405 }
406 }
407 }
Wlc_NtkAbsCreateLogic(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Vec_Int_t * vNodeFrames,Vec_Int_t * vFanins,Vec_Int_t * vNewObjs,Vec_Wec_t * vConstrs,Wlc_Obj_t * pConstrOut)408 void Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Vec_Wec_t * vConstrs, Wlc_Obj_t * pConstrOut )
409 {
410 Vec_Int_t * vTrace;
411 Vec_Int_t * vBitConstr = Vec_IntAlloc( 100 );
412 Vec_Int_t * vLevConstr = Vec_IntAlloc( 100 );
413 Wlc_Obj_t * pAddrs[2], * pDatas[2], * pCond, * pConstr = NULL;
414 int i, k, Entry, Index[2], iFrameLast, iFrameThis;
415 assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
416 Vec_WecForEachLevel( vConstrs, vTrace, i )
417 {
418 if ( Vec_IntSize(vTrace) == 0 )
419 continue;
420 assert( Vec_IntSize(vTrace) >= 2 );
421 Vec_IntClear( vLevConstr );
422
423 iFrameThis = (Vec_IntEntry(vTrace, 0) >> 1) & 0x3FF;
424 iFrameLast = (Vec_IntEntryLast(vTrace) >> 1) & 0x3FF;
425
426 Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vTrace, 0) );
427 Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vTrace) );
428 assert( Index[0] >= 0 && Index[1] >= 0 );
429
430 pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
431 pAddrs[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]) );
432
433 pDatas[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]+1) );
434 pDatas[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]+1) );
435
436 // redirect the source in the last time frame to point to FOs
437 if ( iFrameThis == iFrameLast )
438 {
439 pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]);
440 pDatas[0] = Wlc_ObjFo2Fi(pNew, pDatas[0]);
441 }
442
443 // redirect the sink in the last time frame to point to FOs
444 pAddrs[1] = Wlc_ObjFo2Fi(pNew, pAddrs[1]);
445 pDatas[1] = Wlc_ObjFo2Fi(pNew, pDatas[1]);
446
447 // equal addresses
448 pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0));
449 Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) );
450 Wlc_ObjAddFanins( pNew, pCond, vFanins );
451 Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
452
453 // different datas
454 pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
455 Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pDatas[0]), Wlc_ObjId(pNew, pDatas[1]) );
456 Wlc_ObjAddFanins( pNew, pCond, vFanins );
457 Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
458
459 Vec_IntForEachEntryStartStop( vTrace, Entry, k, 1, Vec_IntSize(vTrace)-1 )
460 {
461 iFrameThis = (Entry >> 1) & 0x3FF;
462 Index[0] = Vec_IntFind( vNodeFrames, Entry );
463 assert( Index[0] >= 0 );
464 pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
465 // redirect the middle in the last time frame to point to FOs
466 if ( iFrameThis == iFrameLast )
467 pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]);
468 if ( Vec_IntEntry(vNewObjs, 2*Index[0]+1) == 0 ) // MUX
469 {
470 assert( Wlc_ObjType(Wlc_NtkObj(p, Entry >> 11)) == WLC_OBJ_MUX );
471 Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pAddrs[0]) );
472 }
473 else // different addresses
474 {
475 assert( Wlc_ObjRange(pAddrs[0]) == Wlc_ObjRange(pAddrs[1]) );
476 pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
477 Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) );
478 Wlc_ObjAddFanins( pNew, pCond, vFanins );
479 Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
480 }
481 }
482
483 // create last output
484 pConstr = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vLevConstr)-1, 0) );
485 Wlc_ObjAddFanins( pNew, pConstr, vLevConstr );
486 Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
487 pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_AND, 0, 0, 0));
488 Wlc_ObjAddFanins( pNew, pConstr, vFanins );
489
490 // save the result
491 Vec_IntPush( vBitConstr, Wlc_ObjId(pNew, pConstr) );
492 }
493 if ( Vec_IntSize(vBitConstr) > 0 )
494 {
495 // create last output
496 pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vBitConstr)-1, 0));
497 Wlc_ObjAddFanins( pNew, pConstr, vBitConstr );
498 // create last output
499 Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
500 pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_OR, 0, 0, 0));
501 Wlc_ObjAddFanins( pNew, pConstr, vFanins );
502 }
503 else
504 {
505 pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, 0, 0));
506 Vec_IntFill( vFanins, 1, 0 ); // const0 - always true
507 Wlc_ObjAddFanins( pNew, pConstr, vFanins );
508 }
509 // cleanup
510 Vec_IntFree( vBitConstr );
511 Vec_IntFree( vLevConstr );
512 // add the constraint as fanin to the output
513 Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
514 Wlc_ObjAddFanins( pNew, pConstrOut, vFanins );
515 }
Wlc_NtkAbstractMemory(Wlc_Ntk_t * p,Vec_Int_t * vMemObjs,Vec_Int_t * vMemFanins,int * piFirstMemPi,int * piFirstCi,int * piFirstMemCi,Vec_Wec_t * vConstrs,Vec_Int_t * vNodeFrames)516 Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int * piFirstMemPi, int * piFirstCi, int * piFirstMemCi, Vec_Wec_t * vConstrs, Vec_Int_t * vNodeFrames )
517 {
518 Wlc_Ntk_t * pNew, * pTemp;
519 Wlc_Obj_t * pObj, * pCounter, * pConst, * pAdder, * pConstr = NULL;
520 Vec_Int_t * vNewObjs = NULL;
521 Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
522 int i, Po0, Po1, AdderBits = 16, nBits = 0;
523
524 // mark memory nodes
525 Wlc_NtkCleanMarks( p );
526 Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
527 pObj->Mark = 1;
528
529 // start new network
530 Wlc_NtkCleanCopy( p );
531 pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
532 pNew->fSmtLib = p->fSmtLib;
533 pNew->fAsyncRst = p->fAsyncRst;
534 pNew->fMemPorts = p->fMemPorts;
535 pNew->fEasyFfs = p->fEasyFfs;
536 pNew->vInits = Vec_IntAlloc( 100 );
537
538 // duplicate PIs
539 Wlc_NtkForEachPi( p, pObj, i )
540 if ( !pObj->Mark )
541 {
542 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
543 nBits += Wlc_ObjRange(pObj);
544 }
545
546 // create new PIs
547 *piFirstMemPi = nBits;
548 Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
549 if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
550 {
551 Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
552 nBits += Wlc_ObjRange(pObj);
553 }
554
555 // duplicate flop outputs
556 *piFirstCi = nBits;
557 Wlc_NtkForEachCi( p, pObj, i )
558 if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
559 {
560 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
561 Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
562 nBits += Wlc_ObjRange(pObj);
563 }
564
565 // create flop for time-frame counter
566 pCounter = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_FO, 0, AdderBits-1, 0));
567 Vec_IntPush( pNew->vInits, -AdderBits );
568 nBits += AdderBits;
569
570 // create flops for memory objects
571 *piFirstMemCi = nBits;
572 if ( vMemFanins )
573 Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
574 Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
575
576 // create flops for constraint objects
577 if ( vConstrs )
578 vNewObjs = Wlc_NtkAbsCreateFlopOutputs( pNew, p, vNodeFrames, vFanins );
579
580 // duplicate objects
581 Wlc_NtkForEachObj( p, pObj, i )
582 if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
583 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
584
585 if ( Vec_IntSize(&p->vPoPairs) )
586 {
587 // create miter for the PO pairs
588 Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
589 {
590 int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
591 int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
592 int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
593 Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
594 Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
595 Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
596 Wlc_ObjSetCo( pNew, pObjNew, 0 );
597 }
598 printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
599 Wlc_NtkForEachCo( p, pObj, i )
600 if ( pObj->fIsFi && !pObj->Mark )
601 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
602
603 // create constraint output
604 if ( vConstrs )
605 Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 );
606 }
607 else
608 {
609 // duplicate POs
610 Wlc_NtkForEachPo( p, pObj, i )
611 if ( !pObj->Mark )
612 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
613 // create constraint output
614 if ( vConstrs )
615 Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 );
616 // duplicate FIs
617 Wlc_NtkForEachCo( p, pObj, i )
618 if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
619 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
620 }
621
622 // create time-frame counter
623 pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
624 Vec_IntFill( vFanins, 1, 1 );
625 Wlc_ObjAddFanins( pNew, pConst, vFanins );
626
627 pAdder = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_ARI_ADD, 0, AdderBits-1, 0));
628 Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pCounter), Wlc_ObjId(pNew, pConst) );
629 Wlc_ObjAddFanins( pNew, pAdder, vFanins );
630 Wlc_ObjSetCo( pNew, pAdder, 1 );
631
632 // create new flop inputs
633 if ( vMemFanins )
634 Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
635 Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)), vFanins, 1 );
636
637 // create flop inputs for constraint objects
638 if ( vConstrs )
639 Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits );
640
641 // create constraint logic nodes
642 if ( vConstrs )
643 Wlc_NtkAbsCreateLogic( pNew, p, vNodeFrames, vFanins, vNewObjs, vConstrs, pConstr );
644
645 // append init states
646 pNew->pInits = Wlc_PrsConvertInitValues( pNew );
647 if ( p->pSpec )
648 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
649 //Wlc_NtkTransferNames( pNew, p );
650 Vec_IntFree( vFanins );
651 Vec_IntFreeP( &vNewObjs );
652 Wlc_NtkCleanMarks( p );
653 // derive topological order
654 pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
655 Wlc_NtkFree( pTemp );
656 return pNew;
657 }
658
659 /**Function*************************************************************
660
661 Synopsis [Derives values of memory subsystem objects under the CEX.]
662
663 Description []
664
665 SideEffects []
666
667 SeeAlso []
668
669 ***********************************************************************/
Wlc_NtkDeriveFirstTotal(Wlc_Ntk_t * p,Vec_Int_t * vMemObjs,Vec_Int_t * vMemFanins,int iFirstMemPi,int iFirstMemCi,int fVerbose)670 Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int iFirstMemPi, int iFirstMemCi, int fVerbose )
671 {
672 Vec_Int_t * vFirstTotal = Vec_IntStart( 3 * Vec_IntSize(vMemObjs) ); // contains pairs of (first CO bit: range) for each input/output of a node
673 Wlc_Obj_t * pObj, * pFanin; int i, k, iFanin, nMemFanins = 0;
674 Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
675 {
676 if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
677 {
678 //Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
679 pFanin = Wlc_ObjFanin0(p, pObj);
680 assert( Wlc_ObjRange(pFanin) == 1 );
681 Vec_IntWriteEntry( vFirstTotal, 3*i, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
682 iFirstMemCi += Wlc_ObjRange(pFanin);
683 nMemFanins++;
684 }
685 else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
686 {
687 Wlc_ObjForEachFanin( pObj, iFanin, k )
688 if ( k > 0 )
689 {
690 //Vec_IntPush( vMemFanins, iFanin );
691 pFanin = Wlc_NtkObj(p, iFanin);
692 Vec_IntWriteEntry( vFirstTotal, 3*i + k, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
693 iFirstMemCi += Wlc_ObjRange(pFanin);
694 nMemFanins++;
695 }
696 if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
697 {
698 Vec_IntWriteEntry( vFirstTotal, 3*i + 2, (iFirstMemPi << 10) | Wlc_ObjRange(pObj) );
699 iFirstMemPi += Wlc_ObjRange(pObj);
700 }
701 }
702 }
703 assert( nMemFanins == Vec_IntSize(vMemFanins) );
704 if ( fVerbose )
705 Vec_IntForEachEntry( vFirstTotal, iFanin, i )
706 {
707 printf( "Obj %5d Fanin %5d : ", i/3, i%3 );
708 printf( "%16s : %d(%d)\n", Wlc_ObjName(p, Vec_IntEntry(vMemObjs, i/3)), iFanin >> 10, iFanin & 0x3FF );
709 }
710 return vFirstTotal;
711 }
Wlc_NtkCexResim(Gia_Man_t * pAbs,Abc_Cex_t * p,Vec_Int_t * vFirstTotal,int iBit,Vec_Wrd_t * vRes,int iFrame)712 int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, int iBit, Vec_Wrd_t * vRes, int iFrame )
713 {
714 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
715 int k, b, Entry, First, nBits; word Value;
716 // assuming that flop outputs have been assigned in the previous timeframe
717 // assign primary inputs
718 Gia_ManForEachPi( pAbs, pObj, k )
719 pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
720 // simulate
721 Gia_ManForEachAnd( pAbs, pObj, k )
722 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
723 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
724 // transfer to combinational outputs
725 Gia_ManForEachCo( pAbs, pObj, k )
726 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
727 // transfer values to flop outputs
728 Gia_ManForEachRiRo( pAbs, pObjRi, pObjRo, k )
729 pObjRo->fMark0 = pObjRi->fMark0;
730 // at this point PIs and FOs area assigned according to this time-frame
731 // collect values
732 Vec_IntForEachEntry( vFirstTotal, Entry, k )
733 {
734 if ( Entry == 0 )
735 {
736 Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, ~(word)0 );
737 continue;
738 }
739 First = Entry >> 10;
740 assert( First < Gia_ManCiNum(pAbs) );
741 nBits = Entry & 0x3FF;
742 assert( nBits <= 64 );
743 Value = 0;
744 for ( b = 0; b < nBits; b++ )
745 if ( Gia_ManCi(pAbs, First+b)->fMark0 )
746 Value |= ((word)1) << b;
747 Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, Value );
748 }
749 return iBit;
750 }
Wlc_NtkConvertCex(Vec_Int_t * vFirstTotal,Gia_Man_t * pAbs,Abc_Cex_t * pCex,int fVerbose)751 Vec_Wrd_t * Wlc_NtkConvertCex( Vec_Int_t * vFirstTotal, Gia_Man_t * pAbs, Abc_Cex_t * pCex, int fVerbose )
752 {
753 Vec_Wrd_t * vValues = Vec_WrdStartFull( Vec_IntSize(vFirstTotal) * (pCex->iFrame + 1) );
754 int k, f, nBits = pCex->nRegs; word Value;
755 Gia_ManCleanMark0(pAbs); // init FOs to zero
756 for ( f = 0; f <= pCex->iFrame; f++ )
757 nBits = Wlc_NtkCexResim( pAbs, pCex, vFirstTotal, nBits, vValues, f );
758 if ( fVerbose )
759 Vec_WrdForEachEntry( vValues, Value, k )
760 {
761 if ( k % Vec_IntSize(vFirstTotal) == 0 )
762 printf( "Frame %d:\n", k/Vec_IntSize(vFirstTotal) );
763 printf( "Obj %5d Fanin %5d : ", k/3, k%3 );
764 Extra_PrintBinary( stdout, (unsigned *)&Value, 32 );
765 printf( "\n" );
766 }
767 return vValues;
768 }
769
770 /**Function*************************************************************
771
772 Synopsis [Derives the reason for failure in terms of memory values.]
773
774 Description []
775
776 SideEffects []
777
778 SeeAlso []
779
780 ***********************************************************************/
Wlc_NtkTrace_rec(Wlc_Ntk_t * p,Wlc_Obj_t * pObj,int iFrame,Vec_Int_t * vMemObjs,Vec_Wrd_t * vValues,word ValueA,Vec_Int_t * vRes)781 void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, word ValueA, Vec_Int_t * vRes )
782 {
783 int iObj = Wlc_ObjId(p, pObj);
784 int iNum = Wlc_ObjCopy( p, iObj );
785 assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
786 assert( iFrame >= 0 );
787 if ( Wlc_ObjIsPi(pObj) )
788 Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) );
789 else if ( Wlc_ObjIsCi(pObj) && iFrame == 0 )
790 {
791 int PiId = Vec_IntEntry(p->vInits, Wlc_ObjCiId(pObj)-Wlc_NtkPiNum(p) );
792 int iPiObj = Wlc_ObjId( p, Wlc_NtkPi(p, PiId) );
793 Vec_IntPush( vRes, (iPiObj << 11) | (iFrame << 1) );
794 }
795 else if ( Wlc_ObjIsCi(pObj) )
796 Wlc_NtkTrace_rec( p, Wlc_ObjFo2Fi(p, pObj), iFrame - 1, vMemObjs, vValues, ValueA, vRes );
797 else if ( Wlc_ObjType(pObj) == WLC_OBJ_BUF )
798 Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
799 else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
800 {
801 int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum);
802 int Value = (int)Vec_WrdEntry( vValues, Index );
803 assert( Value == 0 && Value == 1 );
804 Wlc_NtkTrace_rec( p, Value ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
805 Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) | Value );
806 }
807 else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
808 {
809 int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum);
810 if ( Vec_WrdEntry(vValues, Index + 1) != ValueA ) // address
811 Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
812 Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) );
813 }
814 else assert( 0 );
815 }
Wlc_NtkTrace(Wlc_Ntk_t * p,Wlc_Obj_t * pObj,int iFrame,Vec_Int_t * vMemObjs,Vec_Wrd_t * vValues)816 Vec_Int_t * Wlc_NtkTrace( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues )
817 {
818 int iObj = Wlc_ObjId( p, pObj );
819 int iNum = Wlc_ObjCopy( p, iObj );
820 Vec_Int_t * vTrace = Vec_IntAlloc( 10 );
821 assert( Wlc_ObjType(pObj) == WLC_OBJ_READ );
822 assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
823 Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, Vec_WrdEntry(vValues, 3*(iFrame*Vec_IntSize(vMemObjs) + iNum) + 1), vTrace );
824 Vec_IntPush( vTrace, (iObj << 11) | (iFrame << 1) );
825 return vTrace;
826 }
Wlc_NtkTraceCheckConfict(Wlc_Ntk_t * p,Vec_Int_t * vTrace,Vec_Int_t * vMemObjs,Vec_Wrd_t * vValues)827 int Wlc_NtkTraceCheckConfict( Wlc_Ntk_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues )
828 {
829 Wlc_Obj_t * pObjLast, * pObjFirst;
830 int iObjLast = Vec_IntEntryLast(vTrace) >> 11;
831 int iFrmLast =(Vec_IntEntryLast(vTrace) >> 1) & 0x3FF;
832 int iNumLast = Wlc_ObjCopy( p, iObjLast );
833 int iIndLast = 3*(iFrmLast*Vec_IntSize(vMemObjs) + iNumLast);
834 int iObjFirst = Vec_IntEntry(vTrace, 0) >> 11;
835 int iFrmFirst =(Vec_IntEntry(vTrace, 0) >> 1) & 0x3FF;
836 int iNumFirst = Wlc_ObjCopy( p, iObjFirst );
837 int iIndFirst = 3*(iFrmFirst*Vec_IntSize(vMemObjs) + iNumFirst);
838 assert( Vec_IntSize(vTrace) >= 2 );
839 assert( iObjLast == Vec_IntEntry(vMemObjs, iNumLast) );
840 assert( iObjFirst == Vec_IntEntry(vMemObjs, iNumFirst) );
841 pObjLast = Wlc_NtkObj(p, iObjLast);
842 pObjFirst = Wlc_NtkObj(p, iObjFirst);
843 assert( Wlc_ObjType(pObjLast) == WLC_OBJ_READ );
844 assert( Wlc_ObjType(pObjFirst) == WLC_OBJ_WRITE || Wlc_ObjIsPi(pObjFirst) );
845 if ( Wlc_ObjIsPi(pObjFirst) )
846 return 0;
847 assert( Vec_WrdEntry(vValues, iIndLast + 1) == Vec_WrdEntry(vValues, iIndFirst + 1) ); // equal addr
848 return Vec_WrdEntry(vValues, iIndLast + 2) != Vec_WrdEntry(vValues, iIndFirst + 2); // diff data
849 }
Wlc_NtkFindConflict(Wlc_Ntk_t * p,Vec_Int_t * vMemObjs,Vec_Wrd_t * vValues,int nFrames)850 Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames )
851 {
852 Wlc_Obj_t * pObj; int i, f, Entry;
853 Vec_Wec_t * vTraces = Vec_WecAlloc( 100 );
854 Vec_Int_t * vTrace, * vTrace1, * vTrace2;
855 assert( 3 * nFrames * Vec_IntSize(vMemObjs) == Vec_WrdSize(vValues) );
856 Wlc_NtkCleanCopy( p );
857 Vec_IntForEachEntry( vMemObjs, Entry, i )
858 Wlc_ObjSetCopy( p, Entry, i );
859 for ( f = 0; f < nFrames; f++ )
860 {
861 Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
862 {
863 if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
864 continue;
865 vTrace = Wlc_NtkTrace( p, pObj, f, vMemObjs, vValues );
866 if ( Wlc_NtkTraceCheckConfict( p, vTrace, vMemObjs, vValues ) )
867 {
868 Vec_WecFree( vTraces );
869 return vTrace;
870 }
871 Vec_WecPushLevel( vTraces );
872 Vec_IntAppend( Vec_WecEntryLast(vTraces), vTrace );
873 Vec_IntFree( vTrace );
874 }
875 }
876 // check if there are any common read addresses
877 Vec_WecForEachLevel( vTraces, vTrace1, i )
878 Vec_WecForEachLevelStop( vTraces, vTrace2, f, i )
879 if ( Vec_IntEntry(vTrace1, 0) == Vec_IntEntry(vTrace2, 0) )
880 {
881 int iObj1 = Vec_IntEntryLast(vTrace1) >> 11;
882 int iFrm1 =(Vec_IntEntryLast(vTrace1) >> 1) & 0x3FF;
883 int iNum1 = Wlc_ObjCopy( p, iObj1 );
884 int iInd1 = 3*(iFrm1*Vec_IntSize(vMemObjs) + iNum1);
885
886 int iObj2 = Vec_IntEntryLast(vTrace2) >> 11;
887 int iFrm2 =(Vec_IntEntryLast(vTrace2) >> 1) & 0x3FF;
888 int iNum2 = Wlc_ObjCopy( p, iObj2 );
889 int iInd2 = 3*(iFrm2*Vec_IntSize(vMemObjs) + iNum2);
890
891 assert( iObj1 == Vec_IntEntry(vMemObjs, iNum1) );
892 assert( iObj2 == Vec_IntEntry(vMemObjs, iNum2) );
893 if ( Vec_WrdEntry(vValues, iInd1 + 1) == Vec_WrdEntry(vValues, iInd2 + 1) && // equal address
894 Vec_WrdEntry(vValues, iInd1 + 2) != Vec_WrdEntry(vValues, iInd2 + 2) ) // diff data
895 {
896 vTrace = Vec_IntAlloc( 100 );
897 Vec_IntPush( vTrace, Vec_IntPop(vTrace1) );
898 Vec_IntForEachEntryStart( vTrace1, Entry, i, 1 )
899 Vec_IntPushUnique( vTrace, Entry );
900 Vec_IntForEachEntryStart( vTrace2, Entry, i, 1 )
901 Vec_IntPushUnique( vTrace, Entry );
902 Vec_WecFree( vTraces );
903 return vTrace;
904 }
905 }
906 Vec_WecFree( vTraces );
907 return NULL;
908 }
Wlc_NtkPrintConflict(Wlc_Ntk_t * p,Vec_Int_t * vTrace)909 void Wlc_NtkPrintConflict( Wlc_Ntk_t * p, Vec_Int_t * vTrace )
910 {
911 int Entry, i;
912 printf( "Memory semantics failure trace:\n" );
913 Vec_IntForEachEntry( vTrace, Entry, i )
914 printf( "%3d: entry %9d : obj %5d with name %16s in frame %d\n", i, Entry, Entry >> 11, Wlc_ObjName(p, Entry>>11), (Entry >> 1) & 0x3FF );
915 }
Wlc_NtkPrintCex(Wlc_Ntk_t * p,Wlc_Ntk_t * pAbs,Abc_Cex_t * pCex)916 void Wlc_NtkPrintCex( Wlc_Ntk_t * p, Wlc_Ntk_t * pAbs, Abc_Cex_t * pCex )
917 {
918 Wlc_Obj_t * pObj; int i, k, f, nBits = pCex ? pCex->nRegs : 0;
919 if ( pCex == NULL )
920 {
921 printf( "The CEX is NULL.\n" );
922 return;
923 }
924 for ( f = 0; f <= pCex->iFrame; f++ )
925 {
926 printf( "Frame%02d ", f );
927 Wlc_NtkForEachPi( pAbs, pObj, i )
928 {
929 printf( "PI%d:", i );
930 //printf( "%d(%d):", nBits, Wlc_ObjRange(pObj) );
931 for ( k = 0; k < Wlc_ObjRange(pObj); k++ )
932 printf( "%d", Abc_InfoHasBit(pCex->pData, nBits++) );
933 printf( " " );
934 }
935 printf( "FF:" );
936 for ( k = 0; nBits < pCex->nPis; k++ )
937 printf( "%d", Abc_InfoHasBit(pCex->pData, nBits++) );
938 printf( "\n" );
939 }
940
941 }
942
943 /**Function*************************************************************
944
945 Synopsis [Perform abstraction.]
946
947 Description []
948
949 SideEffects []
950
951 SeeAlso []
952
953 ***********************************************************************/
Wlc_NtkMemAbstractTest(Wlc_Ntk_t * p)954 Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
955 {
956 int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
957 Vec_Int_t * vRefine;
958 Vec_Int_t * vMemObjs = Wlc_NtkCollectMemory( p, 0 );
959 Vec_Int_t * vMemFanins = Wlc_NtkCollectMemFanins( p, vMemObjs );
960
961 Vec_Wec_t * vRefines = Vec_WecAlloc( 100 );
962 Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
963 Wlc_Ntk_t * pNewFull;
964
965 vRefine = Vec_WecPushLevel(vRefines);
966 Vec_IntPush( vRefine, (11 << 11) | 0 );
967 Vec_IntPush( vRefine, (10 << 11) | 0 );
968 Vec_IntPush( vRefine, ( 8 << 11) | 0 );
969 Vec_IntPush( vRefine, ( 9 << 11) | 0 );
970 Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
971
972 // pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
973 pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
974
975 Vec_WecFree( vRefines );
976 Vec_IntFree( vNodeFrames );
977
978 nDcBits = Wlc_CountDcs( pNewFull->pInits );
979 printf( "iFirstMemPi = %d iFirstCi = %d iFirstMemCi = %d nDcBits = %d\n", iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits );
980
981 Vec_IntFreeP( &vMemObjs );
982 Vec_IntFreeP( &vMemFanins );
983 return pNewFull;
984 }
985
Wlc_NtkMemAbstract(Wlc_Ntk_t * p,int nIterMax,int fDumpAbs,int fPdrVerbose,int fVerbose)986 int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose )
987 {
988 abctime clk = Abc_Clock();
989 Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig, * pTempAig;
990 Gia_Man_t * pAbsFull, * pAbs;
991 Abc_Cex_t * pCex = NULL; Vec_Wrd_t * vValues = NULL;
992 Vec_Wec_t * vRefines = Vec_WecAlloc( 100 );
993 Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
994 Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine;
995 int RetValue = -1, iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits, nIters;
996
997 vMemObjs = Wlc_NtkCollectMemory( p, 0 );
998 vMemFanins = Wlc_NtkCollectMemFanins( p, vMemObjs );
999 pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
1000 nDcBits = Wlc_CountDcs( pNewFull->pInits );
1001 vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi, fVerbose );
1002
1003 pAbsFull = Wlc_NtkBitBlast( pNewFull, NULL );
1004 assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits );
1005 Wlc_NtkFree( pNewFull );
1006
1007 // perform abstraction
1008 for ( nIters = 0; nIters < nIterMax; nIters++ )
1009 {
1010 // set up parameters to run PDR
1011 Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
1012 Pdr_ManSetDefaultParams( pPdrPars );
1013 pPdrPars->fUseAbs = 0; // use 'pdr -t' (on-the-fly abstraction)
1014 pPdrPars->fVerbose = fVerbose;
1015
1016 // derive specific abstraction
1017 pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
1018 pAbs = Wlc_NtkBitBlast( pNew, NULL );
1019 // simplify the AIG
1020 //pAbs = Gia_ManSeqStructSweep( pGiaTemp = pAbs, 1, 1, 0 );
1021 //Gia_ManStop( pGiaTemp );
1022
1023 // roll in the constraints
1024 pAig = Gia_ManToAigSimple( pAbs );
1025 Gia_ManStop( pAbs );
1026 pAig->nConstrs = 1;
1027 pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 );
1028 Aig_ManStop( pTempAig );
1029 pAbs = Gia_ManFromAigSimple( pAig );
1030 Aig_ManStop( pAig );
1031
1032 // try to prove abstracted GIA by converting it to AIG and calling PDR
1033 pAig = Gia_ManToAigSimple( pAbs );
1034 RetValue = Pdr_ManSolve( pAig, pPdrPars );
1035 pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
1036 Aig_ManStop( pAig );
1037
1038 if ( fVerbose )
1039 printf( "\nITERATIONS %d:\n", nIters );
1040 if ( fVerbose )
1041 Wlc_NtkPrintCex( p, pNew, pCex );
1042 Wlc_NtkFree( pNew );
1043
1044 if ( fDumpAbs )
1045 {
1046 char * pFileName = "mem_abs.aig";
1047 Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
1048 printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
1049 }
1050
1051 // check if proved or undecided
1052 if ( pCex == NULL )
1053 {
1054 assert( RetValue );
1055 Gia_ManStop( pAbs );
1056 break;
1057 }
1058
1059 // analyze counter-example
1060 vValues = Wlc_NtkConvertCex( vFirstTotal, pAbsFull, pCex, fVerbose );
1061 Gia_ManStop( pAbs );
1062 vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 );
1063 Vec_WrdFree( vValues );
1064 if ( vRefine == NULL ) // cannot refine
1065 break;
1066 Abc_CexFreeP( &pCex );
1067
1068 // save refinement for the future
1069 if ( fVerbose )
1070 Wlc_NtkPrintConflict( p, vRefine );
1071 Vec_WecPushLevel( vRefines );
1072 Vec_IntAppend( Vec_WecEntryLast(vRefines), vRefine );
1073 Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
1074 Vec_IntFree( vRefine );
1075 }
1076 // cleanup
1077 Gia_ManStop( pAbsFull );
1078 Vec_WecFree( vRefines );
1079 Vec_IntFreeP( &vMemObjs );
1080 Vec_IntFreeP( &vMemFanins );
1081 Vec_IntFreeP( &vFirstTotal );
1082 Vec_IntFreeP( &vNodeFrames );
1083
1084 // report the result
1085 if ( fVerbose )
1086 printf( "\n" );
1087 printf( "Abstraction " );
1088 if ( RetValue == 0 && pCex )
1089 printf( "resulted in a real CEX in frame %d", pCex->iFrame );
1090 else if ( RetValue == 1 )
1091 printf( "is successfully proved" );
1092 else
1093 printf( "timed out" );
1094 printf( " after %d iterations. ", nIters );
1095 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1096 Abc_CexFreeP( &pCex ); // return CEX in the future
1097 return RetValue;
1098 }
1099
1100
1101 /**Function*************************************************************
1102
1103 Synopsis [Collect visited objects.]
1104
1105 Description []
1106
1107 SideEffects []
1108
1109 SeeAlso []
1110
1111 ***********************************************************************/
Wlc_NtkExploreMem2_rec(Wlc_Ntk_t * p,Wlc_Obj_t * pObj,Vec_Int_t * vCollect,int nFrames)1112 int Wlc_NtkExploreMem2_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
1113 {
1114 int k, iFanin, nVisited = 0;
1115 if ( pObj->Mark == 0 )
1116 return 0;
1117 if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
1118 {
1119 Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
1120 return 1;
1121 }
1122 if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
1123 return Wlc_NtkExploreMem2_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
1124 Wlc_ObjForEachFanin( pObj, iFanin, k )
1125 nVisited += Wlc_NtkExploreMem2_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
1126 Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
1127 return nVisited + 1;
1128 }
Wlc_NtkExploreMem2(Wlc_Ntk_t * p,int nFrames)1129 void Wlc_NtkExploreMem2( Wlc_Ntk_t * p, int nFrames )
1130 {
1131 Wlc_Obj_t * pObj; int i, k, Entry, Frame, nVisited;
1132 Vec_Int_t * vCollect = Vec_IntStart( 1000 );
1133 Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
1134 Wlc_NtkCleanMarks( p );
1135 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1136 pObj->Mark = 1;
1137 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1138 {
1139 if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
1140 continue;
1141 Vec_IntClear( vCollect );
1142 nVisited = Wlc_NtkExploreMem2_rec( p, pObj, vCollect, nFrames );
1143 printf( "Obj %6d : ", Wlc_ObjId(p, pObj) );
1144 printf( "Visit = %6d ", nVisited );
1145 printf( "Pair = %6d ", Vec_IntSize(vCollect)/2 );
1146 if ( Vec_IntSize(vCollect)/2 < 10 )
1147 Vec_IntForEachEntryDouble( vCollect, Entry, Frame, k )
1148 printf( "%d(%d) ", Entry, Frame );
1149 printf( "\n" );
1150 }
1151 Vec_IntFree( vMemObjsClean );
1152 Vec_IntFree( vCollect );
1153 Wlc_NtkCleanMarks( p );
1154 }
1155
1156 /**Function*************************************************************
1157
1158 Synopsis [Collect memory flops reachable.]
1159
1160 Description []
1161
1162 SideEffects []
1163
1164 SeeAlso []
1165
1166 ***********************************************************************/
Wlc_NtkExploreMem_rec(Wlc_Ntk_t * p,Wlc_Obj_t * pObj,Vec_Int_t * vCollect,int nFrames)1167 void Wlc_NtkExploreMem_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
1168 {
1169 int k, iFanin;
1170 if ( pObj->Mark == 0 )
1171 return;
1172 if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
1173 {
1174 Vec_IntPushUnique( vCollect, Wlc_ObjId(p, pObj) );
1175 return;
1176 }
1177 if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
1178 {
1179 Wlc_NtkExploreMem_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
1180 return;
1181 }
1182 Wlc_ObjForEachFanin( pObj, iFanin, k )
1183 Wlc_NtkExploreMem_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
1184 }
Wlc_NtkExploreMem(Wlc_Ntk_t * p,int nFrames)1185 void Wlc_NtkExploreMem( Wlc_Ntk_t * p, int nFrames )
1186 {
1187 Wlc_Obj_t * pObj; int i, k, iObj;
1188 Vec_Int_t * vCollect = Vec_IntStart( 1000 );
1189 Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
1190 Wlc_NtkCleanMarks( p );
1191 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1192 pObj->Mark = 1;
1193 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1194 {
1195 if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
1196 continue;
1197 Vec_IntClear( vCollect );
1198 Wlc_NtkExploreMem_rec( p, pObj, vCollect, nFrames );
1199 printf( "Read port %6d : ", Wlc_ObjId(p, pObj) );
1200 printf( "Inputs = %6d ", Vec_IntSize(vCollect) );
1201 Vec_IntForEachEntry( vCollect, iObj, k )
1202 printf( "%d(%s) ", iObj, Wlc_ObjName(p, iObj) );
1203 printf( "\n" );
1204 }
1205 Vec_IntFree( vMemObjsClean );
1206 Vec_IntFree( vCollect );
1207 Wlc_NtkCleanMarks( p );
1208 }
1209
1210
1211 /**Function*************************************************************
1212
1213 Synopsis [For each READ find reachable CIs.]
1214
1215 Description []
1216
1217 SideEffects []
1218
1219 SeeAlso []
1220
1221 ***********************************************************************/
Wlc_NtkFindReachablePiFo(Wlc_Ntk_t * p,Vec_Int_t * vMemObjsClean,int nFrames)1222 Vec_Int_t * Wlc_NtkFindReachablePiFo( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int nFrames )
1223 {
1224 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
1225 Wlc_Obj_t * pObjR, * pObjI, * pObj;
1226 int i, j, k, f, fFanin;
1227 Wlc_NtkForEachObj( p, pObj, i )
1228 pObj->Mark2 = 0;
1229 // go through read ports
1230 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjR, i ) if ( Wlc_ObjIsRead(pObjR) )
1231 {
1232 // go through memory CIs
1233 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjI, j ) if ( Wlc_ObjIsCi(pObjI) )
1234 {
1235 // propagate bit from CI to READ
1236 pObjI->Mark2 = 1;
1237 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
1238 {
1239 if ( pObj == pObjI )
1240 continue;
1241 assert( pObj->Mark2 == 0 );
1242 Wlc_ObjForEachFanin( pObj, fFanin, f )
1243 pObj->Mark2 |= Wlc_NtkObj(p, fFanin)->Mark2;
1244 }
1245 if ( pObjR->Mark2 )
1246 Vec_IntPushThree( vRes, Wlc_ObjId(p, pObjR), Wlc_ObjId(p, pObjI), -1 );
1247 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
1248 pObj->Mark2 = 0;
1249 }
1250 }
1251 Wlc_NtkForEachObj( p, pObj, i )
1252 assert( pObj->Mark2 == 0 );
1253 return vRes;
1254 }
Wlc_NtkExtractCisForThisRead(Vec_Int_t * vReachReadCi,int iRead)1255 Vec_Int_t * Wlc_NtkExtractCisForThisRead( Vec_Int_t * vReachReadCi, int iRead )
1256 {
1257 int k;
1258 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
1259 for ( k = 0; k < Vec_IntSize(vReachReadCi)/3; k++ )
1260 {
1261 if ( iRead != Vec_IntEntry( vReachReadCi, 3*k ) )
1262 continue;
1263 Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+1 ) );
1264 Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+2 ) );
1265 }
1266 return vRes;
1267 }
Wlc_NtkCollectOneType(Wlc_Ntk_t * p,Vec_Int_t * vMemObjsClean,int Type1,int Type2)1268 Vec_Int_t * Wlc_NtkCollectOneType( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int Type1, int Type2 )
1269 {
1270 Wlc_Obj_t * pObj; int i;
1271 Vec_Int_t * vRes = Vec_IntAlloc( 100 );
1272 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1273 if ( Wlc_ObjType(pObj) == Type1 || Wlc_ObjType(pObj) == Type2 )
1274 Vec_IntPush( vRes, Wlc_ObjId(p, pObj) );
1275 return vRes;
1276 }
1277
1278 /**Function*************************************************************
1279
1280 Synopsis [Create memory constraints.]
1281
1282 Description []
1283
1284 SideEffects []
1285
1286 SeeAlso []
1287
1288 ***********************************************************************/
Wlc_NtkCreateMemoryConstr(Wlc_Ntk_t * pNew,Wlc_Ntk_t * p,Vec_Int_t * vMemObjsClean,Vec_Int_t * vReachReadCi)1289 void Wlc_NtkCreateMemoryConstr( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, Vec_Int_t * vReachReadCi )
1290 {
1291 Vec_Int_t * vReads = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_READ, -1 );
1292 Vec_Int_t * vObjCis = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_PI, WLC_OBJ_FO );
1293 Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
1294 Wlc_Obj_t * pObjR, * pObj, * pCond;
1295 int i, k, iObjCi, iObjNew = -1;
1296 // go through read ports
1297 Wlc_NtkForEachObjVec( vReads, p, pObjR, i )
1298 {
1299 // ABC_READ ( .mem_in(mem_fi1), .addr(raddr), .data(read1) ) ;
1300 // ABC_WRITE ( .mem_in(mem_fo1), .addr(waddr), .data(data), .mem_out(mem_fi1) ) ;
1301 // initialize CI related to the read port
1302 Vec_Int_t * vLocalCis = Wlc_NtkExtractCisForThisRead( vReachReadCi, Wlc_ObjId(p, pObjR) );
1303 Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
1304 Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
1305 Vec_IntForEachEntryDouble( vLocalCis, iObjCi, iObjNew, k )
1306 Wlc_ObjSetCopy( p, iObjCi, iObjNew );
1307 Vec_IntFree( vLocalCis );
1308 // implement the nodes
1309 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
1310 {
1311 if ( Wlc_ObjIsRead(pObj) || Wlc_ObjIsCi(pObj) )
1312 continue;
1313 Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
1314 if ( Wlc_ObjIsWrite(pObj) )
1315 {
1316 if ( Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) == -1 )
1317 continue;
1318 if ( Wlc_ObjRange(pObjR) != Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)) )
1319 continue;
1320 // create equality
1321 pCond = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0) );
1322 Vec_IntFillTwo( vFanins, 2, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObjR)), Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) );
1323 //printf( "%d : ", Wlc_ObjId(p,pObj) ), Vec_IntPrint( vFanins );
1324 Wlc_ObjAddFanins( pNew, pCond, vFanins );
1325 // create MUX
1326 iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
1327 Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pCond) );
1328 Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) );
1329 Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
1330 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
1331 }
1332 else if ( Wlc_ObjIsMux(pObj) )
1333 {
1334 int iFanin0New = Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj));
1335 int iFanin1New = Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj));
1336 if ( iFanin0New == -1 || iFanin1New == -1 )
1337 continue;
1338 //Wlc_NtkPrintNode( pNew, Wlc_NtkObj(pNew, iFanin0New) );
1339 assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin0New)) );
1340 assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin1New)) );
1341 iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
1342 Vec_IntFill( vFanins, 1, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
1343 Vec_IntPush( vFanins, iFanin0New );
1344 Vec_IntPush( vFanins, iFanin1New );
1345 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
1346 }
1347 else if ( Wlc_ObjIsBuf(pObj) )
1348 {
1349 iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObj) );
1350 if ( iObjNew == -1 )
1351 continue;
1352 }
1353 else assert( 0 );
1354 Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
1355 }
1356 // extract fanin
1357 iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObjR) );
1358 assert( iObjNew != -1 );
1359 Vec_IntFill( vFanins, 1, iObjNew );
1360 // add it as buffer fanin
1361 iObjNew = Wlc_ObjCopy( p, Wlc_ObjId(p, pObjR) );
1362 assert( Wlc_NtkObj(pNew, iObjNew)->Type == WLC_OBJ_BUF );
1363 Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
1364 }
1365 Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
1366 Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
1367 Vec_IntFree( vFanins );
1368 Vec_IntFree( vReads );
1369 Vec_IntFree( vObjCis );
1370 }
1371
1372 /**Function*************************************************************
1373
1374 Synopsis [Perform abstraction.]
1375
1376 Description []
1377
1378 SideEffects []
1379
1380 SeeAlso []
1381
1382 ***********************************************************************/
Wlc_NtkAbstractMem(Wlc_Ntk_t * p,int nFrames,int fVerbose)1383 Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose )
1384 {
1385 Vec_Int_t * vMemObjsAll = Wlc_NtkCollectMemory( p, 0 );
1386 Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
1387 Vec_Int_t * vReachReadCi = Wlc_NtkFindReachablePiFo( p, vMemObjsClean, nFrames );
1388 Wlc_Ntk_t * pNew, * pTemp;
1389 Wlc_Obj_t * pObj;
1390 Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
1391 int i, Po0, Po1, iObjNew;
1392
1393 assert( nFrames == 0 );
1394
1395 // mark memory nodes
1396 Wlc_NtkCleanMarks( p );
1397 Wlc_NtkForEachObjVec( vMemObjsAll, p, pObj, i )
1398 pObj->Mark = 1;
1399
1400 // start new network
1401 Wlc_NtkCleanCopy( p );
1402 pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
1403 pNew->fSmtLib = p->fSmtLib;
1404 pNew->fAsyncRst = p->fAsyncRst;
1405 pNew->fMemPorts = p->fMemPorts;
1406 pNew->fEasyFfs = p->fEasyFfs;
1407 pNew->vInits = Vec_IntAlloc( 100 );
1408
1409 // duplicate PIs
1410 Wlc_NtkForEachPi( p, pObj, i )
1411 if ( !pObj->Mark )
1412 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
1413
1414 // create new PIs
1415 assert( Vec_IntSize(vReachReadCi) % 3 == 0 );
1416 for ( i = 0; i < Vec_IntSize(vReachReadCi)/3; i++ )
1417 {
1418 pObj = Wlc_NtkObj( p, Vec_IntEntry( vReachReadCi, 3*i ) );
1419 assert( Wlc_ObjIsRead(pObj) );
1420 iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
1421 Vec_IntWriteEntry( vReachReadCi, 3*i+2, iObjNew );
1422 }
1423 //Vec_IntPrint( vReachReadCi );
1424
1425 // duplicate flop outputs
1426 Wlc_NtkForEachCi( p, pObj, i )
1427 if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
1428 {
1429 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
1430 Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
1431 }
1432
1433 /*
1434 // create flops for memory objects
1435 Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
1436 for ( k = 0; k < nFrames; k++ )
1437 Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
1438 */
1439
1440 // create buffers for read ports
1441 Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
1442 {
1443 if ( !Wlc_ObjIsRead(pObj) )
1444 continue;
1445 iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
1446 Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
1447 }
1448
1449 // duplicate objects
1450 Wlc_NtkForEachObj( p, pObj, i )
1451 if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
1452 Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
1453
1454 // create memory constraints
1455 Wlc_NtkCreateMemoryConstr( pNew, p, vMemObjsClean, vReachReadCi );
1456
1457 // create outpus
1458 if ( Vec_IntSize(&p->vPoPairs) )
1459 {
1460 // create miter for the PO pairs
1461 Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
1462 {
1463 int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
1464 int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
1465 int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
1466 Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
1467 Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
1468 Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
1469 Wlc_ObjSetCo( pNew, pObjNew, 0 );
1470 }
1471 printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
1472 Wlc_NtkForEachCo( p, pObj, i )
1473 if ( pObj->fIsFi && !pObj->Mark )
1474 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
1475 }
1476 else
1477 {
1478 // duplicate POs
1479 Wlc_NtkForEachPo( p, pObj, i )
1480 if ( !pObj->Mark )
1481 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
1482 // duplicate FIs
1483 Wlc_NtkForEachCo( p, pObj, i )
1484 if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
1485 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
1486 }
1487
1488 /*
1489 // create new flop inputs
1490 Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
1491 for ( k = 0; k < nFrames; k++ )
1492 Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj))-(nFrames-1-k), vFanins, 1 );
1493 */
1494
1495 // append init states
1496 pNew->pInits = Wlc_PrsConvertInitValues( pNew );
1497 if ( p->pSpec )
1498 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
1499 if ( Wlc_NtkHasNameId(p) )
1500 Wlc_NtkTransferNames( pNew, p );
1501 Vec_IntFree( vFanins );
1502 Vec_IntFree( vMemObjsAll );
1503 Vec_IntFree( vMemObjsClean );
1504 Vec_IntFree( vReachReadCi );
1505 Wlc_NtkCleanMarks( p );
1506 // derive topological order
1507 //printf( "Objects before = %d.\n", Wlc_NtkObjNum(pNew) );
1508 pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
1509 Wlc_NtkFree( pTemp );
1510 //printf( "Objects after = %d.\n", Wlc_NtkObjNum(pNew) );
1511 return pNew;
1512 }
1513
1514
1515
1516 ////////////////////////////////////////////////////////////////////////
1517 /// END OF FILE ///
1518 ////////////////////////////////////////////////////////////////////////
1519
1520
1521 ABC_NAMESPACE_IMPL_END
1522
1523