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