1 /**CFile****************************************************************
2
3 FileName [kitIsop.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Computation kit.]
8
9 Synopsis [ISOP computation based on Morreale's algorithm.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Dec 6, 2006.]
16
17 Revision [$Id: kitIsop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "kit.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
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
34 static unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
35 static unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
36
37 ////////////////////////////////////////////////////////////////////////
38 /// FUNCTION DEFINITIONS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 /**Function*************************************************************
42
43 Synopsis [Computes ISOP from TT.]
44
45 Description [Returns the cover in vMemory. Uses the rest of array in vMemory
46 as an intermediate memory storage. Returns the cover with -1 cubes, if the
47 the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of
48 intermediate data).]
49
50 SideEffects []
51
52 SeeAlso []
53
54 ***********************************************************************/
Kit_TruthIsop2(unsigned * puTruth0,unsigned * puTruth1,int nVars,Vec_Int_t * vMemory,int fTryBoth)55 int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth )
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 memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
106 Vec_IntShrink( vMemory, pcRes->nCubes );
107 return RetValue;
108 }
109
110
111 /**Function*************************************************************
112
113 Synopsis [Computes ISOP from TT.]
114
115 Description [Returns the cover in vMemory. Uses the rest of array in vMemory
116 as an intermediate memory storage. Returns the cover with -1 cubes, if the
117 the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of
118 intermediate data).]
119
120 SideEffects []
121
122 SeeAlso []
123
124 ***********************************************************************/
Kit_TruthIsop(unsigned * puTruth,int nVars,Vec_Int_t * vMemory,int fTryBoth)125 int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth )
126 {
127 Kit_Sop_t cRes, * pcRes = &cRes;
128 Kit_Sop_t cRes2, * pcRes2 = &cRes2;
129 unsigned * pResult;
130 int RetValue = 0;
131 assert( nVars >= 0 && nVars <= 16 );
132 // if nVars < 5, make sure it does not depend on those vars
133 // for ( i = nVars; i < 5; i++ )
134 // assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
135 // prepare memory manager
136 Vec_IntClear( vMemory );
137 Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
138 // compute ISOP for the direct polarity
139 pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
140 if ( pcRes->nCubes == -1 )
141 {
142 vMemory->nSize = -1;
143 return -1;
144 }
145 assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
146 if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
147 {
148 vMemory->pArray[0] = 0;
149 Vec_IntShrink( vMemory, pcRes->nCubes );
150 return 0;
151 }
152 if ( fTryBoth )
153 {
154 // compute ISOP for the complemented polarity
155 Kit_TruthNot( puTruth, puTruth, nVars );
156 pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
157 if ( pcRes2->nCubes >= 0 )
158 {
159 assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
160 if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
161 {
162 RetValue = 1;
163 pcRes = pcRes2;
164 }
165 }
166 Kit_TruthNot( puTruth, puTruth, nVars );
167 }
168 // printf( "%d ", vMemory->nSize );
169 // move the cover representation to the beginning of the memory buffer
170 memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
171 Vec_IntShrink( vMemory, pcRes->nCubes );
172 return RetValue;
173 }
Kit_TruthIsopPrintCover(Vec_Int_t * vCover,int nVars,int fCompl)174 void Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl )
175 {
176 int i, k, Entry, Literal;
177 if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
178 {
179 printf( "Constant %d\n", Vec_IntSize(vCover) );
180 return;
181 }
182 Vec_IntForEachEntry( vCover, Entry, i )
183 {
184 for ( k = 0; k < nVars; k++ )
185 {
186 Literal = 3 & (Entry >> (k << 1));
187 if ( Literal == 1 ) // neg literal
188 printf( "0" );
189 else if ( Literal == 2 ) // pos literal
190 printf( "1" );
191 else if ( Literal == 0 )
192 printf( "-" );
193 else assert( 0 );
194 }
195 printf( " %d\n", !fCompl );
196 }
197 }
Kit_TruthIsopPrint(unsigned * puTruth,int nVars,Vec_Int_t * vCover,int fTryBoth)198 void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
199 {
200 int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
201 Kit_TruthIsopPrintCover( vCover, nVars, fCompl );
202 }
203
204 /**Function*************************************************************
205
206 Synopsis [Computes ISOP 6 variables or more.]
207
208 Description []
209
210 SideEffects []
211
212 SeeAlso []
213
214 ***********************************************************************/
Kit_TruthIsop_rec(unsigned * puOn,unsigned * puOnDc,int nVars,Kit_Sop_t * pcRes,Vec_Int_t * vStore)215 unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
216 {
217 Kit_Sop_t cRes0, cRes1, cRes2;
218 Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
219 unsigned * puRes0, * puRes1, * puRes2;
220 unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
221 int i, k, Var, nWords, nWordsAll;
222 // assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
223 // allocate room for the resulting truth table
224 nWordsAll = Kit_TruthWordNum( nVars );
225 pTemp = Vec_IntFetch( vStore, nWordsAll );
226 if ( pTemp == NULL )
227 {
228 pcRes->nCubes = -1;
229 return NULL;
230 }
231 // check for constants
232 if ( Kit_TruthIsConst0( puOn, nVars ) )
233 {
234 pcRes->nLits = 0;
235 pcRes->nCubes = 0;
236 pcRes->pCubes = NULL;
237 Kit_TruthClear( pTemp, nVars );
238 return pTemp;
239 }
240 if ( Kit_TruthIsConst1( puOnDc, nVars ) )
241 {
242 pcRes->nLits = 0;
243 pcRes->nCubes = 1;
244 pcRes->pCubes = Vec_IntFetch( vStore, 1 );
245 if ( pcRes->pCubes == NULL )
246 {
247 pcRes->nCubes = -1;
248 return NULL;
249 }
250 pcRes->pCubes[0] = 0;
251 Kit_TruthFill( pTemp, nVars );
252 return pTemp;
253 }
254 assert( nVars > 0 );
255 // find the topmost var
256 for ( Var = nVars-1; Var >= 0; Var-- )
257 if ( Kit_TruthVarInSupport( puOn, nVars, Var ) ||
258 Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
259 break;
260 assert( Var >= 0 );
261 // consider a simple case when one-word computation can be used
262 if ( Var < 5 )
263 {
264 unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
265 for ( i = 0; i < nWordsAll; i++ )
266 pTemp[i] = uRes;
267 return pTemp;
268 }
269 assert( Var >= 5 );
270 nWords = Kit_TruthWordNum( Var );
271 // cofactor
272 puOn0 = puOn; puOn1 = puOn + nWords;
273 puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords;
274 pTemp0 = pTemp; pTemp1 = pTemp + nWords;
275 // solve for cofactors
276 Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
277 puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
278 if ( pcRes0->nCubes == -1 )
279 {
280 pcRes->nCubes = -1;
281 return NULL;
282 }
283 Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
284 puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
285 if ( pcRes1->nCubes == -1 )
286 {
287 pcRes->nCubes = -1;
288 return NULL;
289 }
290 Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
291 Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
292 Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
293 Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
294 puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
295 if ( pcRes2->nCubes == -1 )
296 {
297 pcRes->nCubes = -1;
298 return NULL;
299 }
300 // create the resulting cover
301 pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
302 pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
303 pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
304 if ( pcRes->pCubes == NULL )
305 {
306 pcRes->nCubes = -1;
307 return NULL;
308 }
309 k = 0;
310 for ( i = 0; i < pcRes0->nCubes; i++ )
311 pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
312 for ( i = 0; i < pcRes1->nCubes; i++ )
313 pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
314 for ( i = 0; i < pcRes2->nCubes; i++ )
315 pcRes->pCubes[k++] = pcRes2->pCubes[i];
316 assert( k == pcRes->nCubes );
317 // create the resulting truth table
318 Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
319 Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
320 // copy the table if needed
321 nWords <<= 1;
322 for ( i = 1; i < nWordsAll/nWords; i++ )
323 for ( k = 0; k < nWords; k++ )
324 pTemp[i*nWords + k] = pTemp[k];
325 // verify in the end
326 // assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
327 // assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
328 return pTemp;
329 }
330
331 /**Function*************************************************************
332
333 Synopsis [Computes ISOP for 5 variables or less.]
334
335 Description []
336
337 SideEffects []
338
339 SeeAlso []
340
341 ***********************************************************************/
Kit_TruthIsop5_rec(unsigned uOn,unsigned uOnDc,int nVars,Kit_Sop_t * pcRes,Vec_Int_t * vStore)342 unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
343 {
344 unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
345 Kit_Sop_t cRes0, cRes1, cRes2;
346 Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
347 unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
348 int i, k, Var;
349 assert( nVars <= 5 );
350 assert( (uOn & ~uOnDc) == 0 );
351 if ( uOn == 0 )
352 {
353 pcRes->nLits = 0;
354 pcRes->nCubes = 0;
355 pcRes->pCubes = NULL;
356 return 0;
357 }
358 if ( uOnDc == 0xFFFFFFFF )
359 {
360 pcRes->nLits = 0;
361 pcRes->nCubes = 1;
362 pcRes->pCubes = Vec_IntFetch( vStore, 1 );
363 if ( pcRes->pCubes == NULL )
364 {
365 pcRes->nCubes = -1;
366 return 0;
367 }
368 pcRes->pCubes[0] = 0;
369 return 0xFFFFFFFF;
370 }
371 assert( nVars > 0 );
372 // find the topmost var
373 for ( Var = nVars-1; Var >= 0; Var-- )
374 if ( Kit_TruthVarInSupport( &uOn, 5, Var ) ||
375 Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
376 break;
377 assert( Var >= 0 );
378 // cofactor
379 uOn0 = uOn1 = uOn;
380 uOnDc0 = uOnDc1 = uOnDc;
381 Kit_TruthCofactor0( &uOn0, Var + 1, Var );
382 Kit_TruthCofactor1( &uOn1, Var + 1, Var );
383 Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
384 Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
385 // solve for cofactors
386 uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
387 if ( pcRes0->nCubes == -1 )
388 {
389 pcRes->nCubes = -1;
390 return 0;
391 }
392 uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
393 if ( pcRes1->nCubes == -1 )
394 {
395 pcRes->nCubes = -1;
396 return 0;
397 }
398 uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
399 if ( pcRes2->nCubes == -1 )
400 {
401 pcRes->nCubes = -1;
402 return 0;
403 }
404 // create the resulting cover
405 pcRes->nLits = pcRes0->nLits + pcRes1->nLits + pcRes2->nLits + pcRes0->nCubes + pcRes1->nCubes;
406 pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
407 pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
408 if ( pcRes->pCubes == NULL )
409 {
410 pcRes->nCubes = -1;
411 return 0;
412 }
413 k = 0;
414 for ( i = 0; i < pcRes0->nCubes; i++ )
415 pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
416 for ( i = 0; i < pcRes1->nCubes; i++ )
417 pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
418 for ( i = 0; i < pcRes2->nCubes; i++ )
419 pcRes->pCubes[k++] = pcRes2->pCubes[i];
420 assert( k == pcRes->nCubes );
421 // derive the final truth table
422 uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
423 // assert( (uOn & ~uRes2) == 0 );
424 // assert( (uRes2 & ~uOnDc) == 0 );
425 return uRes2;
426 }
427
428
429 ////////////////////////////////////////////////////////////////////////
430 /// END OF FILE ///
431 ////////////////////////////////////////////////////////////////////////
432
433
434 ABC_NAMESPACE_IMPL_END
435
436