ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
FxchDiv.c
Go to the documentation of this file.
1
18
19#include "Fxch.h"
20
21ABC_NAMESPACE_IMPL_START
22
24// FUNCTION DEFINITIONS
26static inline int Fxch_DivNormalize( Vec_Int_t* vCubeFree )
27{
28 int * L = Vec_IntArray(vCubeFree);
29 int RetValue = 0, LitA0 = -1, LitB0 = -1, LitA1 = -1, LitB1 = -1;
30 assert( Vec_IntSize(vCubeFree) == 4 );
31 if ( Abc_LitIsCompl(L[0]) != Abc_LitIsCompl(L[1]) && (L[0] >> 2) == (L[1] >> 2) ) // diff cubes, same vars
32 {
33 if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[3]) )
34 return -1;
35 LitA0 = Abc_Lit2Var(L[0]), LitB0 = Abc_Lit2Var(L[1]);
36 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[2]) )
37 {
38 assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[3]) );
39 LitA1 = Abc_Lit2Var(L[2]), LitB1 = Abc_Lit2Var(L[3]);
40 }
41 else
42 {
43 assert( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) );
44 assert( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[2]) );
45 LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[2]);
46 }
47 }
48 else if ( Abc_LitIsCompl(L[1]) != Abc_LitIsCompl(L[2]) && (L[1] >> 2) == (L[2] >> 2) )
49 {
50 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[3]) )
51 return -1;
52 LitA0 = Abc_Lit2Var(L[1]), LitB0 = Abc_Lit2Var(L[2]);
53 if ( Abc_LitIsCompl(L[1]) == Abc_LitIsCompl(L[0]) )
54 LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[3]);
55 else
56 LitA1 = Abc_Lit2Var(L[3]), LitB1 = Abc_Lit2Var(L[0]);
57 }
58 else if ( Abc_LitIsCompl(L[2]) != Abc_LitIsCompl(L[3]) && (L[2] >> 2) == (L[3] >> 2) )
59 {
60 if ( Abc_LitIsCompl(L[0]) == Abc_LitIsCompl(L[1]) )
61 return -1;
62 LitA0 = Abc_Lit2Var(L[2]), LitB0 = Abc_Lit2Var(L[3]);
63 if ( Abc_LitIsCompl(L[2]) == Abc_LitIsCompl(L[0]) )
64 LitA1 = Abc_Lit2Var(L[0]), LitB1 = Abc_Lit2Var(L[1]);
65 else
66 LitA1 = Abc_Lit2Var(L[1]), LitB1 = Abc_Lit2Var(L[0]);
67 }
68 else
69 return -1;
70 assert( LitA0 == Abc_LitNot(LitB0) );
71 if ( Abc_LitIsCompl(LitA0) )
72 {
73 ABC_SWAP( int, LitA0, LitB0 );
74 ABC_SWAP( int, LitA1, LitB1 );
75 }
76 assert( !Abc_LitIsCompl(LitA0) );
77 if ( Abc_LitIsCompl(LitA1) )
78 {
79 LitA1 = Abc_LitNot(LitA1);
80 LitB1 = Abc_LitNot(LitB1);
81 RetValue = 1;
82 }
83 assert( !Abc_LitIsCompl(LitA1) );
84 // arrange literals in such as a way that
85 // - the first two literals are control literals from different cubes
86 // - the third literal is non-complented data input
87 // - the forth literal is possibly complemented data input
88 L[0] = Abc_Var2Lit( LitA0, 0 );
89 L[1] = Abc_Var2Lit( LitB0, 1 );
90 L[2] = Abc_Var2Lit( LitA1, 0 );
91 L[3] = Abc_Var2Lit( LitB1, 1 );
92 return RetValue;
93}
94
112int Fxch_DivCreate( Fxch_Man_t* pFxchMan,
113 Fxch_SubCube_t* pSubCube0,
114 Fxch_SubCube_t* pSubCube1 )
115{
116 int Base = 0;
117
118 int SC0_Lit0,
119 SC0_Lit1,
120 SC1_Lit0,
121 SC1_Lit1;
122
123 int Cube0Size,
124 Cube1Size;
125
126 Vec_IntClear( pFxchMan->vCubeFree );
127
128 SC0_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit0 );
129 SC0_Lit1 = 0;
130 SC1_Lit0 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit0 );
131 SC1_Lit1 = 0;
132
133 if ( pSubCube0->iLit1 == 0 && pSubCube1->iLit1 == 0 )
134 {
135 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
136 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
137 }
138 else if ( pSubCube0->iLit1 > 0 && pSubCube1->iLit1 > 0 )
139 {
140 int RetValue;
141
142 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
143 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
144
145 if ( SC0_Lit0 < SC1_Lit0 )
146 {
147 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 0 ) );
148 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 1 ) );
149 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 0 ) );
150 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 1 ) );
151 }
152 else
153 {
154 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit0, 0 ) );
155 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit0, 1 ) );
156 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC1_Lit1, 0 ) );
157 Vec_IntPush( pFxchMan->vCubeFree, Abc_Var2Lit( SC0_Lit1, 1 ) );
158 }
159
160 RetValue = Fxch_DivNormalize( pFxchMan->vCubeFree );
161 if ( RetValue == -1 )
162 return -1;
163 }
164 else
165 {
166 if ( pSubCube0->iLit1 > 0 )
167 {
168 SC0_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube0->iCube, pSubCube0->iLit1 );
169
170 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
171 if ( SC0_Lit0 == Abc_LitNot( SC1_Lit0 ) )
172 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit1 );
173 else if ( SC0_Lit1 == Abc_LitNot( SC1_Lit0 ) )
174 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
175 }
176 else
177 {
178 SC1_Lit1 = Fxch_ManGetLit( pFxchMan, pSubCube1->iCube, pSubCube1->iLit1 );
179
180 Vec_IntPush( pFxchMan->vCubeFree, SC0_Lit0 );
181 if ( SC1_Lit0 == Abc_LitNot( SC0_Lit0 ) )
182 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit1 );
183 else if ( SC1_Lit1 == Abc_LitNot( SC0_Lit0 ) )
184 Vec_IntPush( pFxchMan->vCubeFree, SC1_Lit0 );
185 }
186 }
187
188 if ( Vec_IntSize( pFxchMan->vCubeFree ) == 0 )
189 return -1;
190
191 if ( Vec_IntSize ( pFxchMan->vCubeFree ) == 2 )
192 {
193 Vec_IntSort( pFxchMan->vCubeFree, 0 );
194
195 Vec_IntWriteEntry( pFxchMan->vCubeFree, 0, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 0 ), 0 ) );
196 Vec_IntWriteEntry( pFxchMan->vCubeFree, 1, Abc_Var2Lit( Vec_IntEntry( pFxchMan->vCubeFree, 1 ), 1 ) );
197 }
198
199 Cube0Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube0->iCube ) );
200 Cube1Size = Vec_IntSize( Fxch_ManGetCube( pFxchMan, pSubCube1->iCube ) );
201 if ( Vec_IntSize( pFxchMan->vCubeFree ) % 2 == 0 )
202 {
203 Base = Abc_MinInt( Cube0Size, Cube1Size )
204 -( Vec_IntSize( pFxchMan->vCubeFree ) / 2) - 1; /* 1 or 2 Lits, 1 SOP NodeID */
205 }
206 else
207 return -1;
208
209 return Base;
210}
211
228int Fxch_DivAdd( Fxch_Man_t* pFxchMan,
229 int fUpdate,
230 int fSingleCube,
231 int fBase )
232{
233 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
234
235 /* Verify if the divisor already exist */
236 if ( iDiv == Vec_FltSize( pFxchMan->vDivWeights ) )
237 {
238 Vec_WecPushLevel( pFxchMan->vDivCubePairs );
239
240 /* Assign initial weight */
241 if ( fSingleCube )
242 {
243 Vec_FltPush( pFxchMan->vDivWeights,
244 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
245 -0.001 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
246 }
247 else
248 {
249 Vec_FltPush( pFxchMan->vDivWeights,
250 -Vec_IntSize( pFxchMan->vCubeFree ) + 0.9
251 -0.0009 * Fxch_ManComputeLevelDiv( pFxchMan, pFxchMan->vCubeFree ) );
252 }
253
254 }
255
256 /* Increment weight */
257 if ( fSingleCube )
258 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, 1 );
259 else
260 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 );
261
262 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
263
264 if ( fUpdate )
265 if ( pFxchMan->vDivPrio )
266 {
267 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
268 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
269 else
270 Vec_QuePush( pFxchMan->vDivPrio, iDiv );
271 }
272
273 return iDiv;
274}
275
291int Fxch_DivRemove( Fxch_Man_t* pFxchMan,
292 int fUpdate,
293 int fSingleCube,
294 int fBase )
295{
296 int iDiv = Hsh_VecManAdd( pFxchMan->pDivHash, pFxchMan->vCubeFree );
297
298 assert( iDiv < Vec_FltSize( pFxchMan->vDivWeights ) );
299
300 /* Decrement weight */
301 if ( fSingleCube )
302 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -1 );
303 else
304 Vec_FltAddToEntry( pFxchMan->vDivWeights, iDiv, -( fBase + Vec_IntSize( pFxchMan->vCubeFree ) - 1 ) );
305
306 if ( fUpdate )
307 if ( pFxchMan->vDivPrio )
308 {
309 if ( Vec_QueIsMember( pFxchMan->vDivPrio, iDiv ) )
310 Vec_QueUpdate( pFxchMan->vDivPrio, iDiv );
311 }
312
313 return iDiv;
314}
315
339void Fxch_DivSepareteCubes( Vec_Int_t* vDiv,
340 Vec_Int_t* vCube0,
341 Vec_Int_t* vCube1 )
342{
343 int* pArray;
344 int i,
345 Lit;
346
347 Vec_IntForEachEntry( vDiv, Lit, i )
348 if ( Abc_LitIsCompl(Lit) )
349 Vec_IntPush( vCube1, Abc_Lit2Var( Lit ) );
350 else
351 Vec_IntPush( vCube0, Abc_Lit2Var( Lit ) );
352
353 if ( ( Vec_IntSize( vDiv ) == 4 ) && ( Vec_IntSize( vCube0 ) == 3 ) )
354 {
355 assert( Vec_IntSize( vCube1 ) == 3 );
356
357 pArray = Vec_IntArray( vCube0 );
358 if ( pArray[1] > pArray[2] )
359 ABC_SWAP( int, pArray[1], pArray[2] );
360
361 pArray = Vec_IntArray( vCube1 );
362 if ( pArray[1] > pArray[2] )
363 ABC_SWAP( int, pArray[1], pArray[2] );
364 }
365}
366
380int Fxch_DivRemoveLits( Vec_Int_t* vCube0,
381 Vec_Int_t* vCube1,
382 Vec_Int_t* vDiv,
383 int *fCompl )
384{
385 int i,
386 Lit,
387 CountP = 0,
388 CountN = 0,
389 Count = 0,
390 ret = 0;
391
392 Vec_IntForEachEntry( vDiv, Lit, i )
393 if ( Abc_LitIsCompl( Abc_Lit2Var( Lit ) ) )
394 CountN += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
395 else
396 CountP += Vec_IntRemove1( vCube0, Abc_Lit2Var( Lit ) );
397
398 Vec_IntForEachEntry( vDiv, Lit, i )
399 Count += Vec_IntRemove1( vCube1, Abc_Lit2Var( Lit ) );
400
401 if ( Vec_IntSize( vDiv ) == 2 )
402 Vec_IntForEachEntry( vDiv, Lit, i )
403 {
404 Vec_IntRemove1( vCube0, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
405 Vec_IntRemove1( vCube1, Abc_LitNot( Abc_Lit2Var( Lit ) ) );
406 }
407
408 ret = Count + CountP + CountN;
409
410 if ( Vec_IntSize( vDiv ) == 4 )
411 {
412 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
413 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) ),
414 Lit2 = Abc_Lit2Var( Vec_IntEntry( vDiv, 2 ) ),
415 Lit3 = Abc_Lit2Var( Vec_IntEntry( vDiv, 3 ) );
416
417 if ( Lit0 == Abc_LitNot( Lit1 ) && Lit2 == Abc_LitNot( Lit3 ) && CountN == 1 )
418 *fCompl = 1;
419
420 if ( Lit0 == Abc_LitNot( Lit1 ) && ret == 2 )
421 {
422 *fCompl = 1;
423
424 Vec_IntForEachEntry( vDiv, Lit, i )
425 ret += Vec_IntRemove1( vCube0, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
426
427 Vec_IntForEachEntry( vDiv, Lit, i )
428 ret += Vec_IntRemove1( vCube1, ( Abc_Lit2Var( Lit ) ^ (fCompl && i > 1) ) );
429 }
430 }
431
432 return ret;
433}
434
446void Fxch_DivPrint( Fxch_Man_t* pFxchMan,
447 int iDiv )
448{
449 Vec_Int_t* vDiv = Hsh_VecReadEntry( pFxchMan->pDivHash, iDiv );
450 int i,
451 Lit;
452
453 printf( "Div %7d : ", iDiv );
454 printf( "Weight %12.5f ", Vec_FltEntry( pFxchMan->vDivWeights, iDiv ) );
455
456 Vec_IntForEachEntry( vDiv, Lit, i )
457 if ( !Abc_LitIsCompl( Lit ) )
458 printf( "%d(1)", Abc_Lit2Var( Lit ) );
459
460 printf( " + " );
461
462 Vec_IntForEachEntry( vDiv, Lit, i )
463 if ( Abc_LitIsCompl( Lit ) )
464 printf( "%d(2)", Abc_Lit2Var( Lit ) );
465
466 printf( " Lits =%7d ", pFxchMan->nLits );
467 printf( "Divs =%8d \n", Hsh_VecSize( pFxchMan->pDivHash ) );
468}
469
470int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv )
471{
472 int Lit0 = Abc_Lit2Var( Vec_IntEntry( vDiv, 0 ) ),
473 Lit1 = Abc_Lit2Var( Vec_IntEntry( vDiv, 1 ) );
474
475 if ( ( Vec_IntSize( vDiv ) == 2 ) && ( Lit0 == Abc_LitNot( Lit1 ) ) )
476 return 0;
477
478 return 1;
479}
480
484
485ABC_NAMESPACE_IMPL_END
Fxch_DivAdd
int Fxch_DivAdd(Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
Definition FxchDiv.c:228
Fxch_DivRemoveLits
int Fxch_DivRemoveLits(Vec_Int_t *vCube0, Vec_Int_t *vCube1, Vec_Int_t *vDiv, int *fCompl)
Definition FxchDiv.c:380
Fxch_DivIsNotConstant1
int Fxch_DivIsNotConstant1(Vec_Int_t *vDiv)
Definition FxchDiv.c:470
Fxch_DivCreate
int Fxch_DivCreate(Fxch_Man_t *pFxchMan, Fxch_SubCube_t *pSubCube0, Fxch_SubCube_t *pSubCube1)
Definition FxchDiv.c:112
Fxch_DivSepareteCubes
void Fxch_DivSepareteCubes(Vec_Int_t *vDiv, Vec_Int_t *vCube0, Vec_Int_t *vCube1)
Definition FxchDiv.c:339
Fxch_DivPrint
void Fxch_DivPrint(Fxch_Man_t *pFxchMan, int iDiv)
Definition FxchDiv.c:446
Fxch_DivRemove
int Fxch_DivRemove(Fxch_Man_t *pFxchMan, int fUpdate, int fSingleCube, int fBase)
Definition FxchDiv.c:291
Fxch_ManComputeLevelDiv
int Fxch_ManComputeLevelDiv(Fxch_Man_t *pFxchMan, Vec_Int_t *vCubeFree)
Definition FxchMan.c:312
Fxch_SubCube_t
struct Fxch_SubCube_t_ Fxch_SubCube_t
Definition Fxch.h:38
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Fxch_Man_t
struct Fxch_Man_t_ Fxch_Man_t
TYPEDEF DECLARATIONS ///.
Definition plaFxch.c:42
Fxch_Man_t_::vDivWeights
Vec_Flt_t * vDivWeights
Definition Fxch.h:104
Fxch_Man_t_::pDivHash
Hsh_VecMan_t * pDivHash
Definition Fxch.h:103
Fxch_Man_t_::nLits
int nLits
Definition plaFxch.c:66
Fxch_Man_t_::vCubeFree
Vec_Int_t * vCubeFree
Definition Fxch.h:119
Fxch_Man_t_::vDivPrio
Vec_Que_t * vDivPrio
Definition Fxch.h:105
Fxch_Man_t_::vDivCubePairs
Vec_Wec_t * vDivCubePairs
Definition Fxch.h:106
Fxch_SubCube_t_::iLit1
uint32_t iLit1
Definition Fxch.h:64
Fxch_SubCube_t_::iLit0
uint32_t iLit0
Definition Fxch.h:63
Fxch_SubCube_t_::iCube
uint32_t iCube
Definition Fxch.h:62
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54