1 /**CFile****************************************************************
2 
3   FileName    [mioSop.c]
4 
5   PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
6 
7   Synopsis    [Derives SOP from Boolean expression.]
8 
9   Author      [MVSIS Group]
10 
11   Affiliation [UC Berkeley]
12 
13   Date        [Ver. 1.0. Started - September 8, 2003.]
14 
15   Revision    [$Id: mioSop.c,v 1.4 2004/06/28 14:20:25 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "mioInt.h"
20 #include "exp.h"
21 
22 ABC_NAMESPACE_IMPL_START
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 ///                        DECLARATIONS                              ///
27 ////////////////////////////////////////////////////////////////////////
28 
Mio_CubeVar0(int v)29 static inline unsigned Mio_CubeVar0( int v )                       { return (1<< (v<<1)   );                   }
Mio_CubeVar1(int v)30 static inline unsigned Mio_CubeVar1( int v )                       { return (1<<((v<<1)+1));                   }
Mio_CubeHasVar0(unsigned x,int v)31 static inline int      Mio_CubeHasVar0( unsigned x, int v )        { return (x & Mio_CubeVar0(v)) > 0;         }
Mio_CubeHasVar1(unsigned x,int v)32 static inline int      Mio_CubeHasVar1( unsigned x, int v )        { return (x & Mio_CubeVar1(v)) > 0;         }
Mio_CubeEmpty(unsigned x)33 static inline int      Mio_CubeEmpty( unsigned x )                 { return (x & (x>>1) & 0x55555555) != 0;    }
Mio_CubeAnd(unsigned x,unsigned y)34 static inline unsigned Mio_CubeAnd( unsigned x, unsigned y )       { return x | y;                             }
Mio_CubeContains(unsigned x,unsigned y)35 static inline int      Mio_CubeContains( unsigned x, unsigned y )  { return (x | y) == y;                      } // x contains y
36 
37 ////////////////////////////////////////////////////////////////////////
38 ///                     FUNCTION DEFINITIONS                         ///
39 ////////////////////////////////////////////////////////////////////////
40 
41 /**Function*************************************************************
42 
43   Synopsis    [Push while performing SCC.]
44 
45   Description []
46 
47   SideEffects []
48 
49   SeeAlso     []
50 
51 ***********************************************************************/
Mio_SopPushSCC(Vec_Int_t * p,unsigned c)52 void Mio_SopPushSCC( Vec_Int_t * p, unsigned c )
53 {
54     unsigned Entry;
55     int i, k = 0;
56     Vec_IntForEachEntry( p, Entry, i )
57     {
58         if ( Mio_CubeContains( Entry, c ) ) // Entry contains c
59         {
60             assert( i == k );
61             return;
62         }
63         if ( Mio_CubeContains( c, Entry ) ) // c contains Entry
64             continue;
65         Vec_IntWriteEntry( p, k++, Entry );
66     }
67     Vec_IntShrink( p, k );
68     Vec_IntPush( p, c );
69 }
70 
71 /**Function*************************************************************
72 
73   Synopsis    [Make the OR of two covers.]
74 
75   Description []
76 
77   SideEffects []
78 
79   SeeAlso     []
80 
81 ***********************************************************************/
Mio_SopCoverOr(Vec_Int_t * p,Vec_Int_t * q)82 Vec_Int_t * Mio_SopCoverOr( Vec_Int_t * p, Vec_Int_t * q )
83 {
84     Vec_Int_t * r;
85     unsigned Entry;
86     int i;
87     r = Vec_IntAlloc( Vec_IntSize(p) + Vec_IntSize(q) );
88     Vec_IntForEachEntry( p, Entry, i )
89         Vec_IntPush( r, Entry );
90     Vec_IntForEachEntry( q, Entry, i )
91         Mio_SopPushSCC( r, Entry );
92     return r;
93 }
94 
95 /**Function*************************************************************
96 
97   Synopsis    [Make the AND of two covers.]
98 
99   Description []
100 
101   SideEffects []
102 
103   SeeAlso     []
104 
105 ***********************************************************************/
Mio_SopCoverAnd(Vec_Int_t * p,Vec_Int_t * q)106 Vec_Int_t * Mio_SopCoverAnd( Vec_Int_t * p, Vec_Int_t * q )
107 {
108     Vec_Int_t * r;
109     unsigned EntryP, EntryQ;
110     int i, k;
111     r = Vec_IntAlloc( Vec_IntSize(p) * Vec_IntSize(q) );
112     Vec_IntForEachEntry( p, EntryP, i )
113         Vec_IntForEachEntry( q, EntryQ, k )
114             if ( !Mio_CubeEmpty( Mio_CubeAnd(EntryP, EntryQ) ) )
115                 Mio_SopPushSCC( r, Mio_CubeAnd(EntryP, EntryQ) );
116     return r;
117 }
118 
119 /**Function*************************************************************
120 
121   Synopsis    [Create negative literal.]
122 
123   Description []
124 
125   SideEffects []
126 
127   SeeAlso     []
128 
129 ***********************************************************************/
Mio_SopVar0(int i)130 Vec_Int_t * Mio_SopVar0( int i )
131 {
132     Vec_Int_t * vSop;
133     vSop = Vec_IntAlloc( 1 );
134     Vec_IntPush( vSop, Mio_CubeVar0(i) );
135     return vSop;
136 }
137 
138 /**Function*************************************************************
139 
140   Synopsis    [Create positive literal.]
141 
142   Description []
143 
144   SideEffects []
145 
146   SeeAlso     []
147 
148 ***********************************************************************/
Mio_SopVar1(int i)149 Vec_Int_t * Mio_SopVar1( int i )
150 {
151     Vec_Int_t * vSop;
152     vSop = Vec_IntAlloc( 1 );
153     Vec_IntPush( vSop, Mio_CubeVar1(i) );
154     return vSop;
155 }
156 
157 /**Function*************************************************************
158 
159   Synopsis    [Create constant 0 literal.]
160 
161   Description []
162 
163   SideEffects []
164 
165   SeeAlso     []
166 
167 ***********************************************************************/
Mio_SopConst0()168 Vec_Int_t * Mio_SopConst0()
169 {
170     Vec_Int_t * vSop;
171     vSop = Vec_IntAlloc( 1 );
172     return vSop;
173 }
174 
175 /**Function*************************************************************
176 
177   Synopsis    [Create constant 1 literal.]
178 
179   Description []
180 
181   SideEffects []
182 
183   SeeAlso     []
184 
185 ***********************************************************************/
Mio_SopConst1()186 Vec_Int_t * Mio_SopConst1()
187 {
188     Vec_Int_t * vSop;
189     vSop = Vec_IntAlloc( 1 );
190     Vec_IntPush( vSop, 0 );
191     return vSop;
192 }
193 
194 /**Function*************************************************************
195 
196   Synopsis    [Derives SOP representation as the char string.]
197 
198   Description []
199 
200   SideEffects []
201 
202   SeeAlso     []
203 
204 ***********************************************************************/
Mio_SopDeriveFromArray(Vec_Int_t * vSop,int nVars,Vec_Str_t * vStr,int fPolarity)205 char * Mio_SopDeriveFromArray( Vec_Int_t * vSop, int nVars, Vec_Str_t * vStr, int fPolarity )
206 {
207     unsigned Entry;
208     int i, k;
209     Vec_StrClear( vStr );
210     if ( Vec_IntSize(vSop) == 0 )
211     {
212         Vec_StrPush( vStr, ' ' );
213         Vec_StrPush( vStr, (char)('1'-fPolarity) );
214         Vec_StrPush( vStr, '\n' );
215         Vec_StrPush( vStr, '\0' );
216         return Vec_StrArray( vStr );
217     }
218     if ( Vec_IntSize(vSop) == 1 && Vec_IntEntry(vSop, 0) == 0 )
219     {
220         Vec_StrPush( vStr, ' ' );
221         Vec_StrPush( vStr, (char)('0'+fPolarity) );
222         Vec_StrPush( vStr, '\n' );
223         Vec_StrPush( vStr, '\0' );
224         return Vec_StrArray( vStr );
225     }
226     // create cubes
227     Vec_IntForEachEntry( vSop, Entry, i )
228     {
229         for ( k = 0; k < nVars; k++ )
230         {
231             if ( Mio_CubeHasVar0( Entry, k ) )
232                 Vec_StrPush( vStr, '0' );
233             else if ( Mio_CubeHasVar1( Entry, k ) )
234                 Vec_StrPush( vStr, '1' );
235             else
236                 Vec_StrPush( vStr, '-' );
237         }
238         Vec_StrPush( vStr, ' ' );
239         Vec_StrPush( vStr, (char)('0'+fPolarity) );
240         Vec_StrPush( vStr, '\n' );
241     }
242     Vec_StrPush( vStr, '\0' );
243     return Vec_StrArray( vStr );
244 }
245 
246 /**Function*************************************************************
247 
248   Synopsis    [Derives SOP representation.]
249 
250   Description [The SOP is guaranteed to be SCC-free but not minimal.]
251 
252   SideEffects []
253 
254   SeeAlso     []
255 
256 ***********************************************************************/
Mio_LibDeriveSop(int nVars,Vec_Int_t * vExpr,Vec_Str_t * vStr)257 char * Mio_LibDeriveSop( int nVars, Vec_Int_t * vExpr, Vec_Str_t * vStr )
258 {
259     Vec_Int_t * vSop;
260     Vec_Ptr_t * vSops0, * vSops1, * vTemp;
261     int i, Index0, Index1, fCompl0, fCompl1;
262     Vec_StrClear( vStr );
263     if ( Exp_IsConst0(vExpr) )
264     {
265         Vec_StrPrintStr( vStr, " 0\n" );
266         Vec_StrPush( vStr, '\0' );
267         return Vec_StrArray( vStr );
268     }
269     if ( Exp_IsConst1(vExpr) )
270     {
271         Vec_StrPrintStr( vStr, " 1\n" );
272         Vec_StrPush( vStr, '\0' );
273         return Vec_StrArray( vStr );
274     }
275     if ( Exp_IsLit(vExpr) )
276     {
277         for ( i = 0; i < nVars; i++ )
278             Vec_StrPush( vStr, '-' );
279         Vec_StrPrintStr( vStr, " 1\n" );
280         Vec_StrPush( vStr, '\0' );
281         assert( (Vec_IntEntry(vExpr,0) >> 1) < nVars );
282         Vec_StrWriteEntry( vStr, Vec_IntEntry(vExpr,0) >> 1, (char)('1' - (Vec_IntEntry(vExpr,0) & 1)) );
283         return Vec_StrArray( vStr );
284     }
285     vSops0 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
286     vSops1 = Vec_PtrAlloc( nVars + Exp_NodeNum(vExpr) );
287     for ( i = 0; i < nVars; i++ )
288     {
289         Vec_PtrPush( vSops0, Mio_SopVar0(i) );
290         Vec_PtrPush( vSops1, Mio_SopVar1(i) );
291     }
292     for ( i = 0; i < Exp_NodeNum(vExpr); i++ )
293     {
294         Index0  = Vec_IntEntry( vExpr, 2*i+0 ) >> 1;
295         Index1  = Vec_IntEntry( vExpr, 2*i+1 ) >> 1;
296         fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1;
297         fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1;
298         // positive polarity
299         vSop = Mio_SopCoverAnd( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0),
300                                 fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) );
301         Vec_PtrPush( vSops1, vSop );
302         // negative polarity
303         vSop = Mio_SopCoverOr( fCompl0 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index0) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index0),
304                                fCompl1 ? (Vec_Int_t *)Vec_PtrEntry(vSops1, Index1) : (Vec_Int_t *)Vec_PtrEntry(vSops0, Index1) );
305         Vec_PtrPush( vSops0, vSop );
306     }
307     // complement
308     if ( Vec_IntEntryLast(vExpr) & 1 )
309     {
310         vTemp  = vSops0;
311         vSops0 = vSops1;
312         vSops1 = vTemp;
313     }
314     // select the best polarity
315     if ( Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops0) ) < Vec_IntSize( (Vec_Int_t *)Vec_PtrEntryLast(vSops1) ) )
316         vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops0);
317     else
318         vSop = (Vec_Int_t *)Vec_PtrEntryLast(vSops1);
319     // convert positive polarity into SOP
320     Mio_SopDeriveFromArray( vSop, nVars, vStr, (vSop == Vec_PtrEntryLast(vSops1)) );
321     Vec_VecFree( (Vec_Vec_t *)vSops0 );
322     Vec_VecFree( (Vec_Vec_t *)vSops1 );
323     return Vec_StrArray( vStr );
324 }
325 
326 
327 ////////////////////////////////////////////////////////////////////////
328 ///                       END OF FILE                                ///
329 ////////////////////////////////////////////////////////////////////////
330 
331 
332 ABC_NAMESPACE_IMPL_END
333 
334