ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kitIsop.c
Go to the documentation of this file.
1
20
21#include "kit.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30// ISOP computation fails if intermediate memory usage exceed this limit
31#define KIT_ISOP_MEM_LIMIT (1<<20)
32
33// static procedures to compute ISOP
34static unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
35static unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
36
40
55int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth, int fReturnTt )
56{
57 Kit_Sop_t cRes, * pcRes = &cRes;
58 Kit_Sop_t cRes2, * pcRes2 = &cRes2;
59 unsigned * pResult;
60 int RetValue = 0;
61 assert( nVars >= 0 && nVars <= 16 );
62 // prepare memory manager
63 Vec_IntClear( vMemory );
64 Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
65 // compute ISOP for the direct polarity
66 Kit_TruthNot( puTruth0, puTruth0, nVars );
67 pResult = Kit_TruthIsop_rec( puTruth1, puTruth0, nVars, pcRes, vMemory );
68 Kit_TruthNot( puTruth0, puTruth0, nVars );
69 if ( pcRes->nCubes == -1 )
70 {
71 vMemory->nSize = -1;
72 return -1;
73 }
74 assert( Kit_TruthIsImply( puTruth1, pResult, nVars ) );
75 Kit_TruthNot( puTruth0, puTruth0, nVars );
76 assert( Kit_TruthIsImply( pResult, puTruth0, nVars ) );
77 Kit_TruthNot( puTruth0, puTruth0, nVars );
78 if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
79 {
80 vMemory->pArray[0] = 0;
81 Vec_IntShrink( vMemory, pcRes->nCubes );
82 return 0;
83 }
84 if ( fTryBoth )
85 {
86 // compute ISOP for the complemented polarity
87 Kit_TruthNot( puTruth1, puTruth1, nVars );
88 pResult = Kit_TruthIsop_rec( puTruth0, puTruth1, nVars, pcRes2, vMemory );
89 Kit_TruthNot( puTruth1, puTruth1, nVars );
90 if ( pcRes2->nCubes >= 0 )
91 {
92 assert( Kit_TruthIsImply( puTruth0, pResult, nVars ) );
93 Kit_TruthNot( puTruth1, puTruth1, nVars );
94 assert( Kit_TruthIsImply( pResult, puTruth1, nVars ) );
95 Kit_TruthNot( puTruth1, puTruth1, nVars );
96 if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
97 {
98 RetValue = 1;
99 pcRes = pcRes2;
100 }
101 }
102 }
103// printf( "%d ", vMemory->nSize );
104 // move the cover representation to the beginning of the memory buffer
105 if ( fReturnTt )
106 {
107 int nWords = Kit_TruthWordNum( nVars );
108 memmove( vMemory->pArray, pResult, nWords * sizeof(unsigned) );
109 Vec_IntShrink( vMemory, nWords );
110 }
111 else
112 {
113 memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
114 Vec_IntShrink( vMemory, pcRes->nCubes );
115 }
116 return RetValue;
117}
118
119
134int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth )
135{
136 Kit_Sop_t cRes, * pcRes = &cRes;
137 Kit_Sop_t cRes2, * pcRes2 = &cRes2;
138 unsigned * pResult;
139 int RetValue = 0;
140 assert( nVars >= 0 && nVars <= 16 );
141 // if nVars < 5, make sure it does not depend on those vars
142// for ( i = nVars; i < 5; i++ )
143// assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
144 // prepare memory manager
145 Vec_IntClear( vMemory );
146 Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
147 // compute ISOP for the direct polarity
148 pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
149 if ( pcRes->nCubes == -1 )
150 {
151 vMemory->nSize = -1;
152 return -1;
153 }
154 assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
155 if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
156 {
157 vMemory->pArray[0] = 0;
158 Vec_IntShrink( vMemory, pcRes->nCubes );
159 return 0;
160 }
161 if ( fTryBoth )
162 {
163 // compute ISOP for the complemented polarity
164 Kit_TruthNot( puTruth, puTruth, nVars );
165 pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
166 if ( pcRes2->nCubes >= 0 )
167 {
168 assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
169 if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
170 {
171 RetValue = 1;
172 pcRes = pcRes2;
173 }
174 }
175 Kit_TruthNot( puTruth, puTruth, nVars );
176 }
177// printf( "%d ", vMemory->nSize );
178 // move the cover representation to the beginning of the memory buffer
179 memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
180 Vec_IntShrink( vMemory, pcRes->nCubes );
181 return RetValue;
182}
183void Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl )
184{
185 int i, k, Entry, Literal;
186 if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
187 {
188 printf( "Constant %d\n", Vec_IntSize(vCover) );
189 return;
190 }
191 Vec_IntForEachEntry( vCover, Entry, i )
192 {
193 for ( k = 0; k < nVars; k++ )
194 {
195 Literal = 3 & (Entry >> (k << 1));
196 if ( Literal == 1 ) // neg literal
197 printf( "0" );
198 else if ( Literal == 2 ) // pos literal
199 printf( "1" );
200 else if ( Literal == 0 )
201 printf( "-" );
202 else assert( 0 );
203 }
204 printf( " %d\n", !fCompl );
205 }
206}
207void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
208{
209 int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
210 Kit_TruthIsopPrintCover( vCover, nVars, fCompl );
211}
212
224unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
225{
226 Kit_Sop_t cRes0, cRes1, cRes2;
227 Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
228 unsigned * puRes0, * puRes1, * puRes2;
229 unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
230 int i, k, Var, nWords, nWordsAll;
231// assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
232 // allocate room for the resulting truth table
233 nWordsAll = Kit_TruthWordNum( nVars );
234 pTemp = Vec_IntFetch( vStore, nWordsAll );
235 if ( pTemp == NULL )
236 {
237 pcRes->nCubes = -1;
238 return NULL;
239 }
240 // check for constants
241 if ( Kit_TruthIsConst0( puOn, nVars ) )
242 {
243 pcRes->nLits = 0;
244 pcRes->nCubes = 0;
245 pcRes->pCubes = NULL;
246 Kit_TruthClear( pTemp, nVars );
247 return pTemp;
248 }
249 if ( Kit_TruthIsConst1( puOnDc, nVars ) )
250 {
251 pcRes->nLits = 0;
252 pcRes->nCubes = 1;
253 pcRes->pCubes = Vec_IntFetch( vStore, 1 );
254 if ( pcRes->pCubes == NULL )
255 {
256 pcRes->nCubes = -1;
257 return NULL;
258 }
259 pcRes->pCubes[0] = 0;
260 Kit_TruthFill( pTemp, nVars );
261 return pTemp;
262 }
263 assert( nVars > 0 );
264 // find the topmost var
265 for ( Var = nVars-1; Var >= 0; Var-- )
266 if ( Kit_TruthVarInSupport( puOn, nVars, Var ) ||
267 Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
268 break;
269 assert( Var >= 0 );
270 // consider a simple case when one-word computation can be used
271 if ( Var < 5 )
272 {
273 unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
274 for ( i = 0; i < nWordsAll; i++ )
275 pTemp[i] = uRes;
276 return pTemp;
277 }
278 assert( Var >= 5 );
279 nWords = Kit_TruthWordNum( Var );
280 // cofactor
281 puOn0 = puOn; puOn1 = puOn + nWords;
282 puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords;
283 pTemp0 = pTemp; pTemp1 = pTemp + nWords;
284 // solve for cofactors
285 Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
286 puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
287 if ( pcRes0->nCubes == -1 )
288 {
289 pcRes->nCubes = -1;
290 return NULL;
291 }
292 Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
293 puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
294 if ( pcRes1->nCubes == -1 )
295 {
296 pcRes->nCubes = -1;
297 return NULL;
298 }
299 Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
300 Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
301 Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
302 Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
303 puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
304 if ( pcRes2->nCubes == -1 )
305 {
306 pcRes->nCubes = -1;
307 return NULL;
308 }
309 // create the resulting cover
310 pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
311 pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
312 pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
313 if ( pcRes->pCubes == NULL )
314 {
315 pcRes->nCubes = -1;
316 return NULL;
317 }
318 k = 0;
319 for ( i = 0; i < pcRes0->nCubes; i++ )
320 pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
321 for ( i = 0; i < pcRes1->nCubes; i++ )
322 pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
323 for ( i = 0; i < pcRes2->nCubes; i++ )
324 pcRes->pCubes[k++] = pcRes2->pCubes[i];
325 assert( k == pcRes->nCubes );
326 // create the resulting truth table
327 Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
328 Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
329 // copy the table if needed
330 nWords <<= 1;
331 for ( i = 1; i < nWordsAll/nWords; i++ )
332 for ( k = 0; k < nWords; k++ )
333 pTemp[i*nWords + k] = pTemp[k];
334 // verify in the end
335// assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
336// assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
337 return pTemp;
338}
339
351unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
352{
353 unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
354 Kit_Sop_t cRes0, cRes1, cRes2;
355 Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
356 unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
357 int i, k, Var;
358 assert( nVars <= 5 );
359 assert( (uOn & ~uOnDc) == 0 );
360 if ( uOn == 0 )
361 {
362 pcRes->nLits = 0;
363 pcRes->nCubes = 0;
364 pcRes->pCubes = NULL;
365 return 0;
366 }
367 if ( uOnDc == 0xFFFFFFFF )
368 {
369 pcRes->nLits = 0;
370 pcRes->nCubes = 1;
371 pcRes->pCubes = Vec_IntFetch( vStore, 1 );
372 if ( pcRes->pCubes == NULL )
373 {
374 pcRes->nCubes = -1;
375 return 0;
376 }
377 pcRes->pCubes[0] = 0;
378 return 0xFFFFFFFF;
379 }
380 assert( nVars > 0 );
381 // find the topmost var
382 for ( Var = nVars-1; Var >= 0; Var-- )
383 if ( Kit_TruthVarInSupport( &uOn, 5, Var ) ||
384 Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
385 break;
386 assert( Var >= 0 );
387 // cofactor
388 uOn0 = uOn1 = uOn;
389 uOnDc0 = uOnDc1 = uOnDc;
390 Kit_TruthCofactor0( &uOn0, Var + 1, Var );
391 Kit_TruthCofactor1( &uOn1, Var + 1, Var );
392 Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
393 Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
394 // solve for cofactors
395 uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
396 if ( pcRes0->nCubes == -1 )
397 {
398 pcRes->nCubes = -1;
399 return 0;
400 }
401 uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
402 if ( pcRes1->nCubes == -1 )
403 {
404 pcRes->nCubes = -1;
405 return 0;
406 }
407 uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
408 if ( pcRes2->nCubes == -1 )
409 {
410 pcRes->nCubes = -1;
411 return 0;
412 }
413 // create the resulting cover
414 pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
415 pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
416 pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
417 if ( pcRes->pCubes == NULL )
418 {
419 pcRes->nCubes = -1;
420 return 0;
421 }
422 k = 0;
423 for ( i = 0; i < pcRes0->nCubes; i++ )
424 pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
425 for ( i = 0; i < pcRes1->nCubes; i++ )
426 pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
427 for ( i = 0; i < pcRes2->nCubes; i++ )
428 pcRes->pCubes[k++] = pcRes2->pCubes[i];
429 assert( k == pcRes->nCubes );
430 // derive the final truth table
431 uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
432// assert( (uOn & ~uRes2) == 0 );
433// assert( (uRes2 & ~uOnDc) == 0 );
434 return uRes2;
435}
436
437
441
442
443ABC_NAMESPACE_IMPL_END
444
nWords
int nWords
Definition abcNpn.c:127
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
Var
int Var
Definition exorList.c:228
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Kit_TruthIsopPrint
void Kit_TruthIsopPrint(unsigned *puTruth, int nVars, Vec_Int_t *vCover, int fTryBoth)
Definition kitIsop.c:207
KIT_ISOP_MEM_LIMIT
#define KIT_ISOP_MEM_LIMIT
DECLARATIONS ///.
Definition kitIsop.c:31
Kit_TruthIsop2
int Kit_TruthIsop2(unsigned *puTruth0, unsigned *puTruth1, int nVars, Vec_Int_t *vMemory, int fTryBoth, int fReturnTt)
FUNCTION DEFINITIONS ///.
Definition kitIsop.c:55
Kit_TruthIsopPrintCover
void Kit_TruthIsopPrintCover(Vec_Int_t *vCover, int nVars, int fCompl)
Definition kitIsop.c:183
Kit_TruthCofactor0
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:368
Kit_Sop_t
typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t
INCLUDES ///.
Definition kit.h:54
Kit_TruthCofactor1
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:470
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:270
assert
#define assert(ex)
Definition util_old.h:213
memmove
char * memmove()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54