ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
wlcUif.c
Go to the documentation of this file.
1
20
21#include "wlc.h"
22
24
28
32
45{
46 int i, iObj;
47 Vec_Int_t * vBoxes = Vec_IntAlloc( Vec_IntSize(vBoxIds) + 1 );
48 Vec_IntPush( vBoxes, Vec_IntSize(vBoxIds) );
49 Vec_IntForEachEntry( vBoxIds, iObj, i )
50 Vec_IntPush( vBoxes, Wlc_ObjNameId(p, iObj) );
51 Abc_FrameSetBoxes( Vec_IntReleaseArray(vBoxes) );
52 Vec_IntFree( vBoxes );
53}
54Vec_Int_t * Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * pCountM )
55{
56 Vec_Int_t * vBoxIds;
57 Wlc_Obj_t * pObj; int i;
58 *pCountA = *pCountM = 0;
59 if ( pPar->nAdderLimit == 0 && pPar->nMultLimit == 0 )
60 return NULL;
61 vBoxIds = Vec_IntAlloc( 100 );
62 Wlc_NtkForEachObj( p, pObj, i )
63 {
64 if ( pObj->Type == WLC_OBJ_ARI_ADD && pPar->nAdderLimit && Wlc_ObjRange(pObj) >= pPar->nAdderLimit )
65 Vec_IntPush( vBoxIds, i ), (*pCountA)++;
66 else if ( pObj->Type == WLC_OBJ_ARI_MULTI && pPar->nMultLimit && Wlc_ObjRange(pObj) >= pPar->nMultLimit )
67 Vec_IntPush( vBoxIds, i ), (*pCountM)++;
68 }
69 if ( Vec_IntSize( vBoxIds ) > 0 )
70 {
71 Wlc_NtkCollectBoxes( p, vBoxIds );
72 return vBoxIds;
73 }
74 Vec_IntFree( vBoxIds );
75 return NULL;
76}
77
90{
91 Wlc_Obj_t * pFanin, * pFanin2; int k;
92 if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
93 return 0;
94 if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
95 return 0;
96 if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
97 return 0;
98 for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
99 {
100 pFanin = Wlc_ObjFanin(p, pObj, k);
101 pFanin2 = Wlc_ObjFanin(p, pObj2, k);
102 if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
103 return 0;
104 if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
105 return 0;
106 }
107 return 1;
108}
109
122{
123 Wlc_Obj_t * pObj; int i;
124 Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
125 Wlc_NtkForEachObj( p, pObj, i )
126 if ( pObj->Type == WLC_OBJ_ARI_MULTI )
127 Vec_IntPush( vBoxIds, i );
128 if ( Vec_IntSize( vBoxIds ) > 0 )
129 return vBoxIds;
130 Vec_IntFree( vBoxIds );
131 return NULL;
132}
133
146{
148 Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
149 Wlc_Obj_t * pObj, * pObj2; int i, k;
150 // iterate through unique pairs
151 Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
152 Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
153 {
154 if ( k == i )
155 break;
156 if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
157 {
158 Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
159 Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
160 }
161 }
162 Vec_IntFree( vMultis );
163 if ( Vec_IntSize( vPairs ) > 0 )
164 return vPairs;
165 Vec_IntFree( vPairs );
166 return NULL;
167}
168
169
170
183{
184 Vec_Int_t * vNodes = vNodesInit;
185 Wlc_Ntk_t * pNew;
186 Wlc_Obj_t * pObj;
187 int i, k, iObj, iFanin;
188 // get multipliers if not given
189 if ( vNodes == NULL )
190 vNodes = Wlc_NtkCollectMultipliers( p );
191 if ( vNodes == NULL )
192 return NULL;
193 // mark nodes
194 Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
195 pObj->Mark = 1;
196 // iterate through the nodes in the DFS order
197 Wlc_NtkCleanCopy( p );
198 Wlc_NtkForEachObj( p, pObj, i )
199 {
200 if ( i == Vec_IntSize(&p->vCopies) )
201 break;
202 if ( pObj->Mark ) {
203 // clean
204 pObj->Mark = 0;
205 // add fresh PI with the same number of bits
206 iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
207 }
208 else {
209 // update fanins
210 Wlc_ObjForEachFanin( pObj, iFanin, k )
211 Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
212 // node to remain
213 iObj = i;
214 }
215 Wlc_ObjSetCopy( p, i, iObj );
216 }
217 // POs do not change in this procedure
218 if ( vNodes != vNodesInit )
219 Vec_IntFree( vNodes );
220 // reconstruct topological order
221 pNew = Wlc_NtkDupDfs( p, 0, 1 );
222 return pNew;
223}
224
237{
238 Vec_Int_t * vPairs = vPairsInit;
239 Wlc_Ntk_t * pNew;
240 Wlc_Obj_t * pObj, * pObj2;
241 Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
242 int i, k, iObj, iObj2, iObjNew, iObjNew2;
243 int iFanin, iFanin2, iFaninNew;
244 // get multiplier pairs if not given
245 if ( vPairs == NULL )
247 if ( vPairs == NULL )
248 return NULL;
249 // sanity checks
250 assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
251 // iterate through node pairs
252 vFanins = Vec_IntAlloc( 100 );
253 vCompares = Vec_IntAlloc( 100 );
254 vUifConstrs = Vec_IntAlloc( 100 );
255 Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
256 {
257 // get two nodes
258 pObj = Wlc_NtkObj( p, iObj );
259 pObj2 = Wlc_NtkObj( p, iObj2 );
260 assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
261 // create fanin comparator nodes
262 Vec_IntClear( vCompares );
263 Wlc_ObjForEachFanin( pObj, iFanin, k )
264 {
265 iFanin2 = Wlc_ObjFaninId( pObj2, k );
266 Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
267 iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
268 Vec_IntPush( vCompares, iFaninNew );
269 // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
270 // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
271 pObj = Wlc_NtkObj( p, iObj );
272 }
273 // concatenate fanin comparators
274 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
275 // create reduction-OR node
276 Vec_IntFill( vFanins, 1, iObjNew );
277 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
278 // craete output comparator node
279 Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
280 iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
281 // create implication node (iObjNew is already complemented above)
282 Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
283 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
284 // save the constraint
285 Vec_IntPush( vUifConstrs, iObjNew );
286 }
287 // derive the AND of the UIF contraints
288 assert( Vec_IntSize(vUifConstrs) > 0 );
289 if ( Vec_IntSize(vUifConstrs) == 1 )
290 iObjNew = Vec_IntEntry( vUifConstrs, 0 );
291 else
292 {
293 // concatenate
294 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
295 // create reduction-AND node
296 Vec_IntFill( vFanins, 1, iObjNew );
297 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
298 }
299 // update each PO to point to the new node
300 Wlc_NtkForEachPo( p, pObj, i )
301 {
302 iObj = Wlc_ObjId(p, pObj);
303 Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
304 iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
305 // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
306 // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
307 pObj = Wlc_NtkObj( p, iObj );
308 // update PO/CO arrays
309 assert( Vec_IntEntry(&p->vPos, i) == iObj );
310 assert( Vec_IntEntry(&p->vCos, i) == iObj );
311 Vec_IntWriteEntry( &p->vPos, i, iObjNew );
312 Vec_IntWriteEntry( &p->vCos, i, iObjNew );
313 // transfer the PO attribute
314 Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
315 assert( pObj->fIsPo );
316 pObj->fIsPo = 0;
317 }
318 // cleanup
319 Vec_IntFree( vUifConstrs );
320 Vec_IntFree( vCompares );
321 Vec_IntFree( vFanins );
322 if ( vPairs != vPairsInit )
323 Vec_IntFree( vPairs );
324 // reconstruct topological order
325 pNew = Wlc_NtkDupDfs( p, 0, 1 );
326 return pNew;
327}
328
332
333
335
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_DLL void Abc_FrameSetBoxes(int *p)
Definition mainFrame.c:125
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
int nMultLimit
Definition wlc.h:213
int nAdderLimit
Definition wlc.h:212
unsigned fIsPo
Definition wlc.h:125
unsigned Type
Definition wlc.h:121
unsigned Mark
Definition wlc.h:123
#define assert(ex)
Definition util_old.h:213
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition vecInt.h:72
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Wlc_Ntk_t * Wlc_NtkAbstractNodes(Wlc_Ntk_t *p, Vec_Int_t *vNodesInit)
Definition wlcUif.c:182
ABC_NAMESPACE_IMPL_START void Wlc_NtkCollectBoxes(Wlc_Ntk_t *p, Vec_Int_t *vBoxIds)
DECLARATIONS ///.
Definition wlcUif.c:44
Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs(Wlc_Ntk_t *p)
Definition wlcUif.c:145
Vec_Int_t * Wlc_NtkCollectAddMult(Wlc_Ntk_t *p, Wlc_BstPar_t *pPar, int *pCountA, int *pCountM)
Definition wlcUif.c:54
Wlc_Ntk_t * Wlc_NtkUifNodePairs(Wlc_Ntk_t *p, Vec_Int_t *vPairsInit)
Definition wlcUif.c:236
Vec_Int_t * Wlc_NtkCollectMultipliers(Wlc_Ntk_t *p)
Definition wlcUif.c:121
int Wlc_NtkPairIsUifable(Wlc_Ntk_t *p, Wlc_Obj_t *pObj, Wlc_Obj_t *pObj2)
Definition wlcUif.c:89
#define Wlc_NtkForEachPo(p, pPo, i)
Definition wlc.h:364
int Wlc_ObjAlloc(Wlc_Ntk_t *p, int Type, int Signed, int End, int Beg)
Definition wlcNtk.c:199
#define Wlc_NtkForEachObjVec(vVec, p, pObj, i)
Definition wlc.h:360
Wlc_Ntk_t * Wlc_NtkDupDfs(Wlc_Ntk_t *p, int fMarked, int fSeq)
Definition wlcNtk.c:986
struct Wlc_Ntk_t_ Wlc_Ntk_t
Definition wlc.h:135
#define Wlc_NtkForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition wlc.h:356
#define Wlc_ObjForEachFanin(pObj, iFanin, i)
Definition wlc.h:375
int Wlc_ObjCreate(Wlc_Ntk_t *p, int Type, int Signed, int End, int Beg, Vec_Int_t *vFanins)
Definition wlcNtk.c:219
@ WLC_OBJ_ARI_MULTI
Definition wlc.h:90
@ WLC_OBJ_REDUCT_AND
Definition wlc.h:82
@ WLC_OBJ_LOGIC_OR
Definition wlc.h:74
@ WLC_OBJ_LOGIC_AND
Definition wlc.h:73
@ WLC_OBJ_REDUCT_OR
Definition wlc.h:83
@ WLC_OBJ_COMP_NOTEQU
Definition wlc.h:77
@ WLC_OBJ_PI
Definition wlc.h:46
@ WLC_OBJ_BIT_CONCAT
Definition wlc.h:68
@ WLC_OBJ_ARI_ADD
Definition wlc.h:88
@ WLC_OBJ_COMP_EQU
Definition wlc.h:76
struct Wlc_BstPar_t_ Wlc_BstPar_t
Definition wlc.h:207
struct Wlc_Obj_t_ Wlc_Obj_t
BASIC TYPES ///.
Definition wlc.h:118