ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kitDec.c
Go to the documentation of this file.
1
20
21#include "kit.h"
22
24
25
29
30// decomposition manager
33{
34 int nVarsMax; // the max number of variables
35 int nWordsMax; // the max number of words
36 Vec_Ptr_t * vTruthVars; // elementary truth tables
37 Vec_Ptr_t * vTruthNodes; // internal truth tables
38 // current problem
39 int nVarsIn; // the current number of variables
40 Vec_Int_t * vLutsIn; // LUT truth tables
41 Vec_Int_t * vSuppIn; // LUT supports
42 char ATimeIn[64]; // variable arrival times
43 // extracted information
44 unsigned * pTruthIn; // computed truth table
45 unsigned * pTruthOut; // computed truth table
46 int nVarsOut; // the current number of variables
47 int nWordsOut; // the current number of words
48 char Order[32]; // new vars into old vars after supp minimization
49 // computed information
50 Vec_Int_t * vLutsOut; // problem decomposition
51 Vec_Int_t * vSuppOut; // problem decomposition
52 char ATimeOut[64]; // variable arrival times
53};
54
55static inline int Kit_DecOuputArrival( int nVars, Vec_Int_t * vLuts, char ATimes[] ) { return ATimes[nVars + Vec_IntSize(vLuts) - 1]; }
56
60
73{
75 assert( nVarsMax <= 20 );
77 p->nVarsMax = nVarsMax;
78 p->nWordsMax = Kit_TruthWordNum( p->nVarsMax );
79 p->vTruthVars = Vec_PtrAllocTruthTables( p->nVarsMax );
80 p->vTruthNodes = Vec_PtrAllocSimInfo( 64, p->nWordsMax );
81 p->vLutsIn = Vec_IntAlloc( 50 );
82 p->vSuppIn = Vec_IntAlloc( 50 );
83 p->vLutsOut = Vec_IntAlloc( 50 );
84 p->vSuppOut = Vec_IntAlloc( 50 );
85 p->pTruthIn = ABC_ALLOC( unsigned, p->nWordsMax );
86 p->pTruthOut = ABC_ALLOC( unsigned, p->nWordsMax );
87 return p;
88}
89
102{
103 ABC_FREE( p->pTruthIn );
104 ABC_FREE( p->pTruthOut );
105 Vec_IntFreeP( &p->vLutsIn );
106 Vec_IntFreeP( &p->vSuppIn );
107 Vec_IntFreeP( &p->vLutsOut );
108 Vec_IntFreeP( &p->vSuppOut );
109 Vec_PtrFreeP( &p->vTruthVars );
110 Vec_PtrFreeP( &p->vTruthNodes );
111 ABC_FREE( p );
112}
113
114
126int Kit_DecComputeOuputArrival( int nVars, Vec_Int_t * vSupps, int LutSize, char ATimesIn[], char ATimesOut[] )
127{
128 int i, v, iVar, nLuts, Delay;
129 nLuts = Vec_IntSize(vSupps) / LutSize;
130 assert( nLuts > 0 );
131 assert( Vec_IntSize(vSupps) % LutSize == 0 );
132 for ( v = 0; v < nVars; v++ )
133 ATimesOut[v] = ATimesIn[v];
134 for ( v = 0; v < nLuts; v++ )
135 {
136 Delay = 0;
137 for ( i = 0; i < LutSize; i++ )
138 {
139 iVar = Vec_IntEntry( vSupps, v * LutSize + i );
140 assert( iVar < nVars + v );
141 Delay = Abc_MaxInt( Delay, ATimesOut[iVar] );
142 }
143 ATimesOut[nVars + v] = Delay + 1;
144 }
145 return ATimesOut[nVars + nLuts - 1];
146}
147
159void Kit_DecComputeTruthOne( int LutSize, unsigned * pTruthLut, int nVars, unsigned * pTruths[], unsigned * pTemp, unsigned * pRes )
160{
161 int i, v;
162 Kit_TruthClear( pRes, nVars );
163 for ( i = 0; i < (1<<LutSize); i++ )
164 {
165 if ( !Kit_TruthHasBit( pTruthLut, i ) )
166 continue;
167 Kit_TruthFill( pTemp, nVars );
168 for ( v = 0; v < LutSize; v++ )
169 if ( i & (1<<v) )
170 Kit_TruthAnd( pTemp, pTemp, pTruths[v], nVars );
171 else
172 Kit_TruthSharp( pTemp, pTemp, pTruths[v], nVars );
173 Kit_TruthOr( pRes, pRes, pTemp, nVars );
174 }
175}
176
188void Kit_DecComputeTruth( Kit_ManDec_t * p, int nVars, Vec_Int_t * vSupps, int LutSize, Vec_Int_t * vLuts, unsigned * pRes )
189{
190 unsigned * pResult, * pTruthLuts, * pTruths[17];
191 int nTruthLutWords, i, v, iVar, nLuts;
192 nLuts = Vec_IntSize(vSupps) / LutSize;
193 pTruthLuts = (unsigned *)Vec_IntArray( vLuts );
194 nTruthLutWords = Kit_TruthWordNum( LutSize );
195 assert( nLuts > 0 );
196 assert( Vec_IntSize(vSupps) % LutSize == 0 );
197 assert( nLuts * nTruthLutWords == Vec_IntSize(vLuts) );
198 for ( v = 0; v < nLuts; v++ )
199 {
200 for ( i = 0; i < LutSize; i++ )
201 {
202 iVar = Vec_IntEntry( vSupps, v * LutSize + i );
203 assert( iVar < nVars + v );
204 pTruths[i] = (iVar < nVars)? (unsigned *)Vec_PtrEntry(p->vTruthVars, iVar) : (unsigned *)Vec_PtrEntry(p->vTruthNodes, iVar-nVars);
205 }
206 pResult = (v == nLuts - 1) ? pRes : (unsigned *)Vec_PtrEntry(p->vTruthNodes, v);
207 Kit_DecComputeTruthOne( LutSize, pTruthLuts, nVars, pTruths, (unsigned *)Vec_PtrEntry(p->vTruthNodes, v+1), pResult );
208 pTruthLuts += nTruthLutWords;
209 }
210}
211
223int Kit_DecComputePattern( int nVars, unsigned * pTruth, int LutSize, int Pattern[] )
224{
225 int nCofs = (1 << LutSize);
226 int i, k, nMyu = 0;
227 assert( LutSize <= 6 );
228 assert( LutSize < nVars );
229 if ( nVars - LutSize <= 5 )
230 {
231 unsigned uCofs[64];
232 int nBits = (1 << (nVars - LutSize));
233 for ( i = 0; i < nCofs; i++ )
234 uCofs[i] = (pTruth[(i*nBits)/32] >> ((i*nBits)%32)) & ((1<<nBits)-1);
235 for ( i = 0; i < nCofs; i++ )
236 {
237 for ( k = 0; k < nMyu; k++ )
238 if ( uCofs[i] == uCofs[k] )
239 {
240 Pattern[i] = k;
241 break;
242 }
243 if ( k == i )
244 Pattern[nMyu++] = i;
245 }
246 }
247 else
248 {
249 unsigned * puCofs[64];
250 int nWords = (1 << (nVars - LutSize - 5));
251 for ( i = 0; i < nCofs; i++ )
252 puCofs[i] = pTruth + nWords;
253 for ( i = 0; i < nCofs; i++ )
254 {
255 for ( k = 0; k < nMyu; k++ )
256 if ( Kit_TruthIsEqual( puCofs[i], puCofs[k], nVars - LutSize - 5 ) )
257 {
258 Pattern[i] = k;
259 break;
260 }
261 if ( k == i )
262 Pattern[nMyu++] = i;
263 }
264 }
265 return nMyu;
266}
267
279int Kit_DecComputeShared_rec( int Pattern[], int Vars[], int nVars, int Shared[], int iVarTry )
280{
281 int Pat0[32], Pat1[32], Shared0[5], Shared1[5], VarsNext[5];
282 int v, u, iVarsNext, iPat0, iPat1, m, nMints = (1 << nVars);
283 int nShared0, nShared1, nShared = 0;
284 for ( v = iVarTry; v < nVars; v++ )
285 {
286 iVarsNext = 0;
287 for ( u = 0; u < nVars; u++ )
288 if ( u == v )
289 VarsNext[iVarsNext++] = Vars[u];
290 iPat0 = iPat1 = 0;
291 for ( m = 0; m < nMints; m++ )
292 if ( m & (1 << v) )
293 Pat1[iPat1++] = m;
294 else
295 Pat0[iPat0++] = m;
296 assert( iPat0 == nMints / 2 );
297 assert( iPat1 == nMints / 2 );
298 nShared0 = Kit_DecComputeShared_rec( Pat0, VarsNext, nVars-1, Shared0, v + 1 );
299 if ( nShared0 == 0 )
300 continue;
301 nShared1 = Kit_DecComputeShared_rec( Pat1, VarsNext, nVars-1, Shared1, v + 1 );
302 if ( nShared1 == 0 )
303 continue;
304 Shared[nShared++] = v;
305 for ( u = 0; u < nShared0; u++ )
306 for ( m = 0; m < nShared1; m++ )
307 if ( Shared0[u] >= 0 && Shared1[m] >= 0 && Shared0[u] == Shared1[m] )
308 {
309 Shared[nShared++] = Shared0[u];
310 Shared0[u] = Shared1[m] = -1;
311 }
312 return nShared;
313 }
314 return 0;
315}
316
328int Kit_DecComputeShared( int Pattern[], int LutSize, int Shared[] )
329{
330 int i, Vars[6];
331 assert( LutSize <= 6 );
332 for ( i = 0; i < LutSize; i++ )
333 Vars[i] = i;
334 return Kit_DecComputeShared_rec( Pattern, Vars, LutSize, Shared, 0 );
335}
336
340
341
343
int nWords
Definition abcNpn.c:127
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
int Kit_DecComputeShared(int Pattern[], int LutSize, int Shared[])
Definition kitDec.c:328
int Kit_DecComputePattern(int nVars, unsigned *pTruth, int LutSize, int Pattern[])
Definition kitDec.c:223
void Kit_DecComputeTruth(Kit_ManDec_t *p, int nVars, Vec_Int_t *vSupps, int LutSize, Vec_Int_t *vLuts, unsigned *pRes)
Definition kitDec.c:188
int Kit_DecComputeOuputArrival(int nVars, Vec_Int_t *vSupps, int LutSize, char ATimesIn[], char ATimesOut[])
Definition kitDec.c:126
void Kit_ManDecStop(Kit_ManDec_t *p)
Definition kitDec.c:101
Kit_ManDec_t * Kit_ManDecStart(int nVarsMax)
FUNCTION DEFINITIONS ///.
Definition kitDec.c:72
void Kit_DecComputeTruthOne(int LutSize, unsigned *pTruthLut, int nVars, unsigned *pTruths[], unsigned *pTemp, unsigned *pRes)
Definition kitDec.c:159
int Kit_DecComputeShared_rec(int Pattern[], int Vars[], int nVars, int Shared[], int iVarTry)
Definition kitDec.c:279
typedefABC_NAMESPACE_IMPL_START struct Kit_ManDec_t_ Kit_ManDec_t
DECLARATIONS ///.
Definition kitDec.c:31
Vec_Int_t * vLutsIn
Definition kitDec.c:40
Vec_Int_t * vLutsOut
Definition kitDec.c:50
char ATimeIn[64]
Definition kitDec.c:42
int nVarsIn
Definition kitDec.c:39
unsigned * pTruthIn
Definition kitDec.c:44
char ATimeOut[64]
Definition kitDec.c:52
int nVarsMax
Definition kitDec.c:34
int nVarsOut
Definition kitDec.c:46
Vec_Ptr_t * vTruthNodes
Definition kitDec.c:37
int nWordsMax
Definition kitDec.c:35
char Order[32]
Definition kitDec.c:48
Vec_Int_t * vSuppOut
Definition kitDec.c:51
Vec_Ptr_t * vTruthVars
Definition kitDec.c:36
Vec_Int_t * vSuppIn
Definition kitDec.c:41
int nWordsOut
Definition kitDec.c:47
unsigned * pTruthOut
Definition kitDec.c:45
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42