1 /**CFile****************************************************************
2
3 FileName [ifTruth.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [FPGA mapping based on priority cuts.]
8
9 Synopsis [Computation of truth tables of the cuts.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 21, 2006.]
16
17 Revision [$Id: ifTruth.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "if.h"
22 #include "bool/kit/kit.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 //#define IF_TRY_NEW
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Sorts the pins in the decreasing order of delays.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
If_CutTruthPermute(word * pTruth,int nLeaves,int nVars,int nWords,float * pDelays,int * pVars)48 void If_CutTruthPermute( word * pTruth, int nLeaves, int nVars, int nWords, float * pDelays, int * pVars )
49 {
50 while ( 1 )
51 {
52 int i, fChange = 0;
53 for ( i = 0; i < nLeaves - 1; i++ )
54 {
55 if ( pDelays[i] >= pDelays[i+1] )
56 continue;
57 ABC_SWAP( float, pDelays[i], pDelays[i+1] );
58 ABC_SWAP( int, pVars[i], pVars[i+1] );
59 if ( pTruth )
60 Abc_TtSwapAdjacent( pTruth, nWords, i );
61 fChange = 1;
62 }
63 if ( !fChange )
64 return;
65 }
66 }
If_CutRotatePins(If_Man_t * p,If_Cut_t * pCut)67 void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
68 {
69 If_Obj_t * pLeaf;
70 float PinDelays[IF_MAX_LUTSIZE];
71 int i, truthId;
72 assert( !p->pPars->fUseTtPerm );
73 If_CutForEachLeaf( p, pCut, pLeaf, i )
74 PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
75 if ( p->vTtMem[pCut->nLeaves] == NULL )
76 {
77 If_CutTruthPermute( NULL, If_CutLeaveNum(pCut), pCut->nLeaves, p->nTruth6Words[pCut->nLeaves], PinDelays, If_CutLeaves(pCut) );
78 return;
79 }
80 Abc_TtCopy( p->puTempW, If_CutTruthWR(p, pCut), p->nTruth6Words[pCut->nLeaves], 0 );
81 If_CutTruthPermute( p->puTempW, If_CutLeaveNum(pCut), pCut->nLeaves, p->nTruth6Words[pCut->nLeaves], PinDelays, If_CutLeaves(pCut) );
82 truthId = Vec_MemHashInsert( p->vTtMem[pCut->nLeaves], p->puTempW );
83 pCut->iCutFunc = Abc_Var2Lit( truthId, If_CutTruthIsCompl(pCut) );
84 assert( (p->puTempW[0] & 1) == 0 );
85 }
86
87 /**Function*************************************************************
88
89 Synopsis [Truth table computation.]
90
91 Description []
92
93 SideEffects []
94
95 SeeAlso []
96
97 ***********************************************************************/
If_CutComputeTruth(If_Man_t * p,If_Cut_t * pCut,If_Cut_t * pCut0,If_Cut_t * pCut1,int fCompl0,int fCompl1)98 int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
99 {
100 int fCompl, truthId, nLeavesNew, PrevSize, RetValue = 0;
101 word * pTruth0s = Vec_MemReadEntry( p->vTtMem[pCut0->nLeaves], Abc_Lit2Var(pCut0->iCutFunc) );
102 word * pTruth1s = Vec_MemReadEntry( p->vTtMem[pCut1->nLeaves], Abc_Lit2Var(pCut1->iCutFunc) );
103 word * pTruth0 = (word *)p->puTemp[0];
104 word * pTruth1 = (word *)p->puTemp[1];
105 word * pTruth = (word *)p->puTemp[2];
106 Abc_TtCopy( pTruth0, pTruth0s, p->nTruth6Words[pCut0->nLeaves], fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iCutFunc) );
107 Abc_TtCopy( pTruth1, pTruth1s, p->nTruth6Words[pCut1->nLeaves], fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iCutFunc) );
108 Abc_TtStretch6( pTruth0, pCut0->nLeaves, pCut->nLeaves );
109 Abc_TtStretch6( pTruth1, pCut1->nLeaves, pCut->nLeaves );
110 Abc_TtExpand( pTruth0, pCut->nLeaves, pCut0->pLeaves, pCut0->nLeaves, pCut->pLeaves, pCut->nLeaves );
111 Abc_TtExpand( pTruth1, pCut->nLeaves, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves );
112 fCompl = (pTruth0[0] & pTruth1[0] & 1);
113 Abc_TtAnd( pTruth, pTruth0, pTruth1, p->nTruth6Words[pCut->nLeaves], fCompl );
114 if ( p->pPars->fCutMin && (pCut0->nLeaves + pCut1->nLeaves > pCut->nLeaves || pCut0->nLeaves == 0 || pCut1->nLeaves == 0) )
115 {
116 nLeavesNew = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves, pCut->nLeaves );
117 if ( nLeavesNew < If_CutLeaveNum(pCut) )
118 {
119 pCut->nLeaves = nLeavesNew;
120 pCut->uSign = If_ObjCutSignCompute( pCut );
121 RetValue = 1;
122 }
123 }
124 PrevSize = Vec_MemEntryNum( p->vTtMem[pCut->nLeaves] );
125 truthId = Vec_MemHashInsert( p->vTtMem[pCut->nLeaves], pTruth );
126 pCut->iCutFunc = Abc_Var2Lit( truthId, fCompl );
127 assert( (pTruth[0] & 1) == 0 );
128 #ifdef IF_TRY_NEW
129 {
130 word pCopy[1024];
131 char pCanonPerm[16];
132 memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * p->nTruth6Words[pCut->nLeaves] );
133 Abc_TtCanonicize( pCopy, pCut->nLeaves, pCanonPerm );
134 }
135 #endif
136 if ( p->vTtIsops[pCut->nLeaves] && PrevSize != Vec_MemEntryNum(p->vTtMem[pCut->nLeaves]) )
137 {
138 Vec_Int_t * vLevel = Vec_WecPushLevel( p->vTtIsops[pCut->nLeaves] );
139 fCompl = Kit_TruthIsop( (unsigned *)pTruth, pCut->nLeaves, p->vCover, 1 );
140 if ( fCompl >= 0 )
141 {
142 Vec_IntGrow( vLevel, Vec_IntSize(p->vCover) );
143 Vec_IntAppend( vLevel, p->vCover );
144 if ( fCompl )
145 vLevel->nCap ^= (1<<16); // hack to remember complemented attribute
146 }
147 assert( Vec_WecSize(p->vTtIsops[pCut->nLeaves]) == Vec_MemEntryNum(p->vTtMem[pCut->nLeaves]) );
148 }
149 return RetValue;
150 }
151
152 /**Function*************************************************************
153
154 Synopsis [Truth table computation.]
155
156 Description []
157
158 SideEffects []
159
160 SeeAlso []
161
162 ***********************************************************************/
If_CutComputeTruthPerm_int(If_Man_t * p,If_Cut_t * pCut,If_Cut_t * pCut0,If_Cut_t * pCut1,int iCutFunc0,int iCutFunc1)163 int If_CutComputeTruthPerm_int( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int iCutFunc0, int iCutFunc1 )
164 {
165 int fVerbose = 0;
166 abctime clk = 0;
167 int pPerm[IF_MAX_LUTSIZE];
168 int v, Place, fCompl, truthId, nLeavesNew, RetValue = 0;
169 word * pTruth0s = Vec_MemReadEntry( p->vTtMem[pCut0->nLeaves], Abc_Lit2Var(iCutFunc0) );
170 word * pTruth1s = Vec_MemReadEntry( p->vTtMem[pCut1->nLeaves], Abc_Lit2Var(iCutFunc1) );
171 word * pTruth0 = (word *)p->puTemp[0];
172 word * pTruth1 = (word *)p->puTemp[1];
173 word * pTruth = (word *)p->puTemp[2];
174 assert( pCut0->uMaskFunc >= 0 );
175 assert( pCut1->uMaskFunc >= 0 );
176 Abc_TtCopy( pTruth0, pTruth0s, p->nTruth6Words[pCut0->nLeaves], Abc_LitIsCompl(iCutFunc0) );
177 Abc_TtCopy( pTruth1, pTruth1s, p->nTruth6Words[pCut1->nLeaves], Abc_LitIsCompl(iCutFunc1) );
178 Abc_TtStretch6( pTruth0, pCut0->nLeaves, pCut->nLeaves );
179 Abc_TtStretch6( pTruth1, pCut1->nLeaves, pCut->nLeaves );
180
181 if ( fVerbose )
182 {
183 //Kit_DsdPrintFromTruth( pTruth0, pCut0->nLeaves ); printf( "\n" );
184 //Kit_DsdPrintFromTruth( pTruth1, pCut1->nLeaves ); printf( "\n" );
185 }
186 // create literals
187 for ( v = 0; v < (int)pCut0->nLeaves; v++ )
188 pCut->pLeaves[v] = Abc_Var2Lit( pCut0->pLeaves[v], If_CutLeafBit(pCut0, v) );
189 for ( v = 0; v < (int)pCut1->nLeaves; v++ )
190 if ( p->pPerm[1][v] >= (int)pCut0->nLeaves )
191 pCut->pLeaves[p->pPerm[1][v]] = Abc_Var2Lit( pCut1->pLeaves[v], If_CutLeafBit(pCut1, v) );
192 else if ( If_CutLeafBit(pCut0, p->pPerm[1][v]) != If_CutLeafBit(pCut1, v) )
193 Abc_TtFlip( pTruth1, p->nTruth6Words[pCut1->nLeaves], v );
194 // permute variables
195 for ( v = (int)pCut1->nLeaves; v < (int)pCut->nLeaves; v++ )
196 p->pPerm[1][v] = -1;
197 for ( v = 0; v < (int)pCut1->nLeaves; v++ )
198 {
199 Place = p->pPerm[1][v];
200 if ( Place == v || Place == -1 )
201 continue;
202 Abc_TtSwapVars( pTruth1, pCut->nLeaves, v, Place );
203 p->pPerm[1][v] = p->pPerm[1][Place];
204 p->pPerm[1][Place] = Place;
205 v--;
206 }
207
208 if ( fVerbose )
209 {
210 //Kit_DsdPrintFromTruth( pTruth0, pCut0->nLeaves ); printf( "\n" );
211 //Kit_DsdPrintFromTruth( pTruth1, pCut->nLeaves ); printf( "\n" );
212 }
213
214 // perform operation
215 Abc_TtAnd( pTruth, pTruth0, pTruth1, p->nTruth6Words[pCut->nLeaves], 0 );
216 // minimize support
217 if ( p->pPars->fCutMin && (pCut0->nLeaves + pCut1->nLeaves > pCut->nLeaves || pCut0->nLeaves == 0 || pCut1->nLeaves == 0) )
218 {
219 nLeavesNew = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves, pCut->nLeaves );
220 if ( nLeavesNew < If_CutLeaveNum(pCut) )
221 {
222 pCut->nLeaves = nLeavesNew;
223 RetValue = 1;
224 }
225 }
226 // compute canonical form
227 if ( p->pPars->fVerbose )
228 clk = Abc_Clock();
229 p->uCanonPhase = Abc_TtCanonicize( pTruth, pCut->nLeaves, p->pCanonPerm );
230 if ( p->pPars->fVerbose )
231 p->timeCache[3] += Abc_Clock() - clk;
232 for ( v = 0; v < (int)pCut->nLeaves; v++ )
233 pPerm[v] = Abc_LitNotCond( pCut->pLeaves[(int)p->pCanonPerm[v]], ((p->uCanonPhase>>v)&1) );
234 pCut->uMaskFunc = 0;
235 for ( v = 0; v < (int)pCut->nLeaves; v++ )
236 {
237 pCut->pLeaves[v] = Abc_Lit2Var(pPerm[v]);
238 if ( Abc_LitIsCompl(pPerm[v]) )
239 pCut->uMaskFunc |= (1 << v);
240 }
241 // create signature after lowering literals
242 if ( RetValue )
243 pCut->uSign = If_ObjCutSignCompute( pCut );
244 else
245 assert( pCut->uSign == If_ObjCutSignCompute( pCut ) );
246
247 assert( Vec_IntSize(p->vTtOccurs[pCut->nLeaves]) == Vec_MemEntryNum(p->vTtMem[pCut->nLeaves]) );
248 // hash function
249 fCompl = ((p->uCanonPhase >> pCut->nLeaves) & 1);
250 truthId = Vec_MemHashInsert( p->vTtMem[pCut->nLeaves], pTruth );
251 pCut->iCutFunc = Abc_Var2Lit( truthId, fCompl );
252 // count how many time this truth table is used
253 if ( Vec_IntSize(p->vTtOccurs[pCut->nLeaves]) < Vec_MemEntryNum(p->vTtMem[pCut->nLeaves]) )
254 Vec_IntPush( p->vTtOccurs[pCut->nLeaves], 0 );
255 Vec_IntAddToEntry( p->vTtOccurs[pCut->nLeaves], truthId, 1 );
256
257 if ( fVerbose )
258 {
259 //Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); printf( "\n" );
260 //If_CutPrint( pCut0 );
261 //If_CutPrint( pCut1 );
262 //If_CutPrint( pCut );
263 //printf( "%d\n\n", pCut->iCutFunc );
264 }
265
266 return RetValue;
267 }
If_CutComputeTruthPerm(If_Man_t * p,If_Cut_t * pCut,If_Cut_t * pCut0,If_Cut_t * pCut1,int iCutFunc0,int iCutFunc1)268 int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int iCutFunc0, int iCutFunc1 )
269 {
270 abctime clk = 0;
271 int i, Num, nEntriesOld, RetValue;
272 if ( pCut0->nLeaves + pCut1->nLeaves > pCut->nLeaves || iCutFunc0 < 2 || iCutFunc1 < 2 )
273 {
274 if ( p->pPars->fVerbose )
275 clk = Abc_Clock();
276 RetValue = If_CutComputeTruthPerm_int( p, pCut, pCut0, pCut1, iCutFunc0, iCutFunc1 );
277 if ( p->pPars->fVerbose )
278 p->timeCache[0] += Abc_Clock() - clk;
279 return RetValue;
280 }
281 assert( pCut0->nLeaves + pCut1->nLeaves == pCut->nLeaves );
282 nEntriesOld = Hash_IntManEntryNum(p->vPairHash);
283 Num = Hash_Int2ManInsert( p->vPairHash, (iCutFunc0 << 5)|pCut0->nLeaves, (iCutFunc1 << 5)|pCut1->nLeaves, -1 );
284 assert( Num > 0 );
285 if ( nEntriesOld == Hash_IntManEntryNum(p->vPairHash) )
286 {
287 char * pCanonPerm;
288 int v, pPerm[IF_MAX_LUTSIZE];
289 pCut->iCutFunc = Vec_IntEntry( p->vPairRes, Num );
290 // move complements from the fanin cuts
291 for ( v = 0; v < (int)pCut->nLeaves; v++ )
292 if ( v < (int)pCut0->nLeaves )
293 pCut->pLeaves[v] = Abc_Var2Lit( pCut->pLeaves[v], If_CutLeafBit(pCut0, v) );
294 else
295 pCut->pLeaves[v] = Abc_Var2Lit( pCut->pLeaves[v], If_CutLeafBit(pCut1, v-(int)pCut0->nLeaves) );
296 // reorder the cut
297 pCanonPerm = Vec_StrEntryP( p->vPairPerms, Num * pCut->nLimit );
298 for ( v = 0; v < (int)pCut->nLeaves; v++ )
299 pPerm[v] = Abc_LitNotCond( pCut->pLeaves[Abc_Lit2Var((int)pCanonPerm[v])], Abc_LitIsCompl((int)pCanonPerm[v]) );
300 // generate the result
301 pCut->uMaskFunc = 0;
302 for ( v = 0; v < (int)pCut->nLeaves; v++ )
303 {
304 pCut->pLeaves[v] = Abc_Lit2Var(pPerm[v]);
305 if ( Abc_LitIsCompl(pPerm[v]) )
306 pCut->uMaskFunc |= (1 << v);
307 }
308 // printf( "Found: %d(%d) %d(%d) -> %d(%d)\n", iCutFunc0, pCut0->nLeaves, iCutFunc1, pCut0->nLeaves, pCut->iCutFunc, pCut->nLeaves );
309 p->nCacheHits++;
310 //p->timeCache[1] += Abc_Clock() - clk;
311 return 0;
312 }
313 if ( p->pPars->fVerbose )
314 clk = Abc_Clock();
315 p->nCacheMisses++;
316 RetValue = If_CutComputeTruthPerm_int( p, pCut, pCut0, pCut1, iCutFunc0, iCutFunc1 );
317 assert( RetValue == 0 );
318 // printf( "Added: %d(%d) %d(%d) -> %d(%d)\n", iCutFunc0, pCut0->nLeaves, iCutFunc1, pCut0->nLeaves, pCut->iCutFunc, pCut->nLeaves );
319 // save the result
320 assert( Num == Vec_IntSize(p->vPairRes) );
321 Vec_IntPush( p->vPairRes, pCut->iCutFunc );
322 // save the permutation
323 assert( Num * (int)pCut->nLimit == Vec_StrSize(p->vPairPerms) );
324 for ( i = 0; i < (int)pCut->nLeaves; i++ )
325 Vec_StrPush( p->vPairPerms, (char)Abc_Var2Lit((int)p->pCanonPerm[i], ((p->uCanonPhase>>i)&1)) );
326 for ( i = (int)pCut0->nLeaves + (int)pCut1->nLeaves; i < (int)pCut->nLimit; i++ )
327 Vec_StrPush( p->vPairPerms, (char)-1 );
328 if ( p->pPars->fVerbose )
329 p->timeCache[2] += Abc_Clock() - clk;
330 return 0;
331 }
332
333 /**Function*************************************************************
334
335 Synopsis [Check the function of 6-input LUT.]
336
337 Description []
338
339 SideEffects []
340
341 SeeAlso []
342
343 ***********************************************************************/
If_DeriveHashTable6(int nVars,word uTruth)344 Vec_Mem_t * If_DeriveHashTable6( int nVars, word uTruth )
345 {
346 int fVerbose = 0;
347 int nMints = (1 << nVars);
348 int nPerms = Extra_Factorial( nVars );
349 int * pComp = Extra_GreyCodeSchedule( nVars );
350 int * pPerm = Extra_PermSchedule( nVars );
351 word Canon = ABC_CONST(0xFFFFFFFFFFFFFFFF);
352 word tCur, tTemp1, tTemp2;
353 Vec_Mem_t * vTtMem6 = Vec_MemAllocForTTSimple( nVars );
354 int i, p, c;
355 for ( i = 0; i < 2; i++ )
356 {
357 tCur = i ? ~uTruth : uTruth;
358 tTemp1 = tCur;
359 for ( p = 0; p < nPerms; p++ )
360 {
361 tTemp2 = tCur;
362 for ( c = 0; c < nMints; c++ )
363 {
364 if ( Canon > tCur )
365 Canon = tCur;
366 Vec_MemHashInsert( vTtMem6, &tCur );
367 tCur = Abc_Tt6Flip( tCur, pComp[c] );
368 }
369 assert( tTemp2 == tCur );
370 tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[p] );
371 }
372 assert( tTemp1 == tCur );
373 }
374 ABC_FREE( pComp );
375 ABC_FREE( pPerm );
376 if ( fVerbose )
377 {
378 /*
379 word * pEntry;
380 Vec_MemForEachEntry( vTtMem6, pEntry, i )
381 {
382 Extra_PrintHex( stdout, (unsigned*)pEntry, nVars );
383 printf( ", " );
384 if ( i % 4 == 3 )
385 printf( "\n" );
386 }
387 */
388 Extra_PrintHex( stdout, (unsigned*)&uTruth, nVars ); printf( "\n" );
389 Extra_PrintHex( stdout, (unsigned*)&Canon, nVars ); printf( "\n" );
390 printf( "Members = %d.\n", Vec_MemEntryNum(vTtMem6) );
391 }
392 return vTtMem6;
393 }
394
If_CutCheckTruth6(If_Man_t * p,If_Cut_t * pCut)395 int If_CutCheckTruth6( If_Man_t * p, If_Cut_t * pCut )
396 {
397 if ( pCut->nLeaves != 6 )
398 return 0;
399 if ( p->vTtMem6 == NULL )
400 p->vTtMem6 = If_DeriveHashTable6( 6, ABC_CONST(0xfedcba9876543210) );
401 if ( *Vec_MemHashLookup( p->vTtMem6, If_CutTruthWR(p, pCut) ) == -1 )
402 return 0;
403 return 1;
404 }
405
406 ////////////////////////////////////////////////////////////////////////
407 /// END OF FILE ///
408 ////////////////////////////////////////////////////////////////////////
409
410
411 ABC_NAMESPACE_IMPL_END
412
413