ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sbdCore.c
Go to the documentation of this file.
1
20
21#include "sbdInt.h"
22#include "opt/dau/dau.h"
23#include "misc/tim/tim.h"
24
25ABC_NAMESPACE_IMPL_START
26
30
31#define SBD_MAX_LUTSIZE 6
32
33typedef struct Sbd_Man_t_ Sbd_Man_t;
34struct Sbd_Man_t_
35{
36 Sbd_Par_t * pPars; // user's parameters
37 Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
38 Vec_Wec_t * vTfos; // TFO for each node (roots are marked) (windowing)
39 Vec_Int_t * vLutLevs; // LUT level for each node after resynthesis
40 Vec_Int_t * vLutCuts; // LUT cut for each nodes after resynthesis
41 Vec_Int_t * vLutCuts2; // LUT cut for each nodes after resynthesis
42 Vec_Int_t * vMirrors; // alternative node
43 Vec_Wrd_t * vSims[4]; // simulation information (main, backup, controlability)
44 Vec_Int_t * vCover; // temporary
45 Vec_Int_t * vLits; // temporary
46 Vec_Int_t * vLits2; // temporary
47 int nLuts[6]; // 0=const, 1=1lut, 2=2lut, 3=3lut
48 int nTried;
49 int nUsed;
50 abctime timeWin;
51 abctime timeCut;
52 abctime timeCov;
53 abctime timeCnf;
54 abctime timeSat;
55 abctime timeQbf;
56 abctime timeNew;
57 abctime timeOther;
58 abctime timeTotal;
59 Sbd_Sto_t * pSto;
60 Sbd_Srv_t * pSrv;
61 // target node
62 int Pivot; // target node
63 int DivCutoff; // the place where D-2 divisors begin
64 Vec_Int_t * vTfo; // TFO (excludes node, includes roots) - precomputed
65 Vec_Int_t * vRoots; // TFO root nodes
66 Vec_Int_t * vWinObjs; // TFI + Pivot + sideTFI + TFO (including roots)
67 Vec_Int_t * vObj2Var; // SAT variables for the window (indexes of objects in vWinObjs)
68 Vec_Int_t * vDivSet; // divisor variables
69 Vec_Int_t * vDivVars; // divisor variables
70 Vec_Int_t * vDivValues; // SAT variables values for the divisor variables
71 Vec_Wec_t * vDivLevels; // divisors collected by levels
72 Vec_Int_t * vCounts[2]; // counters of zeros and ones
73 Vec_Wrd_t * vMatrix; // covering matrix
74 sat_solver * pSat; // SAT solver
75};
76
77static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
78static inline int * Sbd_ObjCut2( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts2, (p->pPars->nLutSize + 1) * i ); }
79
80static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i ); }
81static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i ); }
82static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i ); }
83static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[3], p->pPars->nWords * i ); }
84
88
100void Sbd_ParSetDefault( Sbd_Par_t * pPars )
101{
102 memset( pPars, 0, sizeof(Sbd_Par_t) );
103 pPars->nLutSize = 4; // target LUT size
104 pPars->nLutNum = 3; // target LUT count
105 pPars->nCutSize = (pPars->nLutSize - 1) * pPars->nLutNum + 1; // target cut size
106 pPars->nCutNum = 128; // target cut count
107 pPars->nTfoLevels = 5; // the number of TFO levels (windowing)
108 pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
109 pPars->nWinSizeMax = 2000; // maximum window size (windowing)
110 pPars->nBTLimit = 0; // maximum number of SAT conflicts
111 pPars->nWords = 1; // simulation word count
112 pPars->fMapping = 1; // generate mapping
113 pPars->fMoreCuts = 0; // use several cuts
114 pPars->fFindDivs = 0; // perform divisor search
115 pPars->fUsePath = 0; // optimize only critical path
116 pPars->fArea = 0; // area-oriented optimization
117 pPars->fCover = 0; // use complete cover procedure
118 pPars->fVerbose = 0; // verbose flag
119 pPars->fVeryVerbose = 0; // verbose flag
120}
121
135Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
136{
137 Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked
138 Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage
139 Vec_Int_t * vNodes, * vNodes0, * vNodes1;
140 Vec_Bit_t * vPoDrivers = Vec_BitStart( Gia_ManObjNum(p) );
141 int i, k, k2, Id, Fan;
142 Gia_ManLevelNum( p );
143 Gia_ManCreateRefs( p );
144 Gia_ManCleanMark0( p );
145 Gia_ManForEachCiId( p, Id, i )
146 {
147 vNodes = Vec_WecEntry( vTemp, Id );
148 Vec_IntGrow( vNodes, 1 );
149 Vec_IntPush( vNodes, Id );
150 }
151 Gia_ManForEachCoDriverId( p, Id, i )
152 Vec_BitWriteEntry( vPoDrivers, Id, 1 );
153 Gia_ManForEachAndId( p, Id )
154 {
155 int fAlwaysRoot = Vec_BitEntry(vPoDrivers, Id) || (Gia_ObjRefNumId(p, Id) >= nTfoFanMax);
156 vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) );
157 vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) );
158 vNodes = Vec_WecEntry( vTemp, Id );
159 Vec_IntTwoMerge2( vNodes0, vNodes1, vNodes );
160 k2 = 0;
161 Vec_IntForEachEntry( vNodes, Fan, k )
162 {
163 int fRoot = fAlwaysRoot || (Gia_ObjLevelId(p, Id) - Gia_ObjLevelId(p, Fan) >= nTfoLevels);
164 Vec_WecPush( vTfos, Fan, Abc_Var2Lit(Id, fRoot) );
165 if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan );
166 }
167 Vec_IntShrink( vNodes, k2 );
168 if ( !fAlwaysRoot )
169 Vec_IntPush( vNodes, Id );
170 }
171 Vec_WecFree( vTemp );
172 Vec_BitFree( vPoDrivers );
173
174 // print the results
175 if ( 0 )
176 Vec_WecForEachLevel( vTfos, vNodes, i )
177 {
178 if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
179 continue;
180 printf( "Node %3d : ", i );
181 Vec_IntForEachEntry( vNodes, Fan, k )
182 printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" );
183 printf( "\n" );
184 }
185
186 return vTfos;
187}
188
200Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
201{
202 int i, w, Id;
203 Sbd_Man_t * p = ABC_CALLOC( Sbd_Man_t, 1 );
204 p->timeTotal = Abc_Clock();
205 p->pPars = pPars;
206 p->pGia = pGia;
207 p->vTfos = Sbd_ManWindowRoots( pGia, pPars->nTfoLevels, pPars->nTfoFanMax );
208 p->vLutLevs = Vec_IntStart( Gia_ManObjNum(pGia) );
209 p->vLutCuts = Vec_IntStart( Gia_ManObjNum(pGia) * (p->pPars->nLutSize + 1) );
210 p->vMirrors = Vec_IntStartFull( Gia_ManObjNum(pGia) );
211 for ( i = 0; i < 4; i++ )
212 p->vSims[i] = Vec_WrdStart( Gia_ManObjNum(pGia) * p->pPars->nWords );
213 // target node
214 p->vCover = Vec_IntAlloc( 100 );
215 p->vLits = Vec_IntAlloc( 100 );
216 p->vLits2 = Vec_IntAlloc( 100 );
217 p->vRoots = Vec_IntAlloc( 100 );
218 p->vWinObjs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
219 p->vObj2Var = Vec_IntStart( Gia_ManObjNum(pGia) );
220 p->vDivSet = Vec_IntAlloc( 100 );
221 p->vDivVars = Vec_IntAlloc( 100 );
222 p->vDivValues = Vec_IntAlloc( 100 );
223 p->vDivLevels = Vec_WecAlloc( 100 );
224 p->vCounts[0] = Vec_IntAlloc( 100 );
225 p->vCounts[1] = Vec_IntAlloc( 100 );
226 p->vMatrix = Vec_WrdAlloc( 100 );
227 // start input cuts
228 Gia_ManForEachCiId( pGia, Id, i )
229 {
230 int * pCut = Sbd_ObjCut( p, Id );
231 pCut[0] = 1;
232 pCut[1] = Id;
233 }
234 // generate random input
235 Gia_ManRandom( 1 );
236 Gia_ManForEachCiId( pGia, Id, i )
237 for ( w = 0; w < p->pPars->nWords; w++ )
238 Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
239 // cut enumeration
240 if ( pPars->fMoreCuts )
241 p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, !pPars->fMapping, 1 );
242 else
243 {
244 p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, !pPars->fMapping, 1 );
245 p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
246 }
247 return p;
248}
249void Sbd_ManStop( Sbd_Man_t * p )
250{
251 int i;
252 Vec_WecFree( p->vTfos );
253 Vec_IntFree( p->vLutLevs );
254 Vec_IntFree( p->vLutCuts );
255 Vec_IntFree( p->vMirrors );
256 for ( i = 0; i < 4; i++ )
257 Vec_WrdFree( p->vSims[i] );
258 Vec_IntFree( p->vCover );
259 Vec_IntFree( p->vLits );
260 Vec_IntFree( p->vLits2 );
261 Vec_IntFree( p->vRoots );
262 Vec_IntFree( p->vWinObjs );
263 Vec_IntFree( p->vObj2Var );
264 Vec_IntFree( p->vDivSet );
265 Vec_IntFree( p->vDivVars );
266 Vec_IntFree( p->vDivValues );
267 Vec_WecFree( p->vDivLevels );
268 Vec_IntFree( p->vCounts[0] );
269 Vec_IntFree( p->vCounts[1] );
270 Vec_WrdFree( p->vMatrix );
271 sat_solver_delete_p( &p->pSat );
272 if ( p->pSto ) Sbd_StoFree( p->pSto );
273 if ( p->pSrv ) Sbd_ManCutServerStop( p->pSrv );
274 ABC_FREE( p );
275}
276
277
289void Sbd_ManPropagateControlOne( Sbd_Man_t * p, int Node )
290{
291 Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node); int w;
292 int iObj0 = Gia_ObjFaninId0(pNode, Node);
293 int iObj1 = Gia_ObjFaninId1(pNode, Node);
294
295// word * pSims = Sbd_ObjSim0(p, Node);
296// word * pSims0 = Sbd_ObjSim0(p, iObj0);
297// word * pSims1 = Sbd_ObjSim0(p, iObj1);
298
299 word * pCtrl = Sbd_ObjSim2(p, Node);
300 word * pCtrl0 = Sbd_ObjSim2(p, iObj0);
301 word * pCtrl1 = Sbd_ObjSim2(p, iObj1);
302
303 word * pDtrl = Sbd_ObjSim3(p, Node);
304 word * pDtrl0 = Sbd_ObjSim3(p, iObj0);
305 word * pDtrl1 = Sbd_ObjSim3(p, iObj1);
306
307// Gia_ObjPrint( p->pGia, pNode );
308// printf( "Node %2d : %d %d\n\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
309
310 for ( w = 0; w < p->pPars->nWords; w++ )
311 {
312// word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w];
313// word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w];
314
315 pCtrl0[w] |= pCtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
316 pCtrl1[w] |= pCtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
317
318 pDtrl0[w] |= pDtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
319 pDtrl1[w] |= pDtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
320 }
321}
322void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot )
323{
324 abctime clk = Abc_Clock();
325 int i, Node;
326 Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 );
327 // clean controlability
328 for ( i = 0; i < Vec_IntEntry(p->vObj2Var, Pivot) && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i++ )
329 {
330 Abc_TtClear( Sbd_ObjSim2(p, Node), p->pPars->nWords );
331 Abc_TtClear( Sbd_ObjSim3(p, Node), p->pPars->nWords );
332 //printf( "Clearing node %d.\n", Node );
333 }
334 // propagate controlability to fanins for the TFI nodes starting from the pivot
335 for ( i = Vec_IntEntry(p->vObj2Var, Pivot); i >= 0 && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i-- )
336 if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Node)) )
337 Sbd_ManPropagateControlOne( p, Node );
338 p->timeWin += Abc_Clock() - clk;
339}
340void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
341{
342 int i, k, Node;
343 Vec_Int_t * vLevel;
344 int nTimeValidDivs = 0;
345 // collect divisors by logic level
346 int LevelMax = Vec_IntEntry(p->vLutLevs, Pivot);
347 Vec_WecClear( p->vDivLevels );
348 Vec_WecInit( p->vDivLevels, LevelMax + 1 );
349 Vec_IntForEachEntry( p->vWinObjs, Node, i )
350 Vec_WecPush( p->vDivLevels, Vec_IntEntry(p->vLutLevs, Node), Node );
351 // reload divisors
352 Vec_IntClear( p->vWinObjs );
353 Vec_WecForEachLevel( p->vDivLevels, vLevel, i )
354 {
355 Vec_IntSort( vLevel, 0 );
356 Vec_IntForEachEntry( vLevel, Node, k )
357 {
358 Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
359 Vec_IntPush( p->vWinObjs, Node );
360 }
361 // remember divisor cutoff
362 if ( i == LevelMax - 2 )
363 nTimeValidDivs = Vec_IntSize(p->vWinObjs);
364 }
365 assert( nTimeValidDivs > 0 );
366 Vec_IntClear( p->vDivVars );
367 p->DivCutoff = -1;
368 Vec_IntForEachEntryStartStop( p->vWinObjs, Node, i, Abc_MaxInt(0, nTimeValidDivs-63), nTimeValidDivs )
369 {
370 if ( p->DivCutoff == -1 && Vec_IntEntry(p->vLutLevs, Node) == LevelMax - 2 )
371 p->DivCutoff = Vec_IntSize(p->vDivVars);
372 Vec_IntPush( p->vDivVars, i );
373 }
374 if ( p->DivCutoff == -1 )
375 p->DivCutoff = 0;
376 // verify
377/*
378 assert( Vec_IntSize(p->vDivVars) < 64 );
379 Vec_IntForEachEntryStart( p->vDivVars, Node, i, p->DivCutoff )
380 assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) == LevelMax - 2 );
381 Vec_IntForEachEntryStop( p->vDivVars, Node, i, p->DivCutoff )
382 assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) < LevelMax - 2 );
383*/
384 Vec_IntFill( p->vDivValues, Vec_IntSize(p->vDivVars), 0 );
385 //printf( "%d ", Vec_IntSize(p->vDivVars) );
386// printf( "Node %4d : Win = %5d. Divs = %5d. D1 = %5d. D2 = %5d.\n",
387// Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vDivVars), Vec_IntSize(p->vDivVars)-p->DivCutoff, p->DivCutoff );
388}
389void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
390{
391 Gia_Obj_t * pObj;
392 int Node = NodeInit;
393 if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
394 Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) );
395 if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) )
396 return;
397 Gia_ObjSetTravIdCurrentId(p->pGia, Node);
398 pObj = Gia_ManObj( p->pGia, Node );
399 if ( Gia_ObjIsAnd(pObj) )
400 {
401 Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) );
402 Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
403 }
404 if ( !pObj->fMark0 )
405 {
406 Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
407 Vec_IntPush( p->vWinObjs, Node );
408 }
409 if ( Gia_ObjIsCi(pObj) )
410 return;
411 // simulate
412 assert( Gia_ObjIsAnd(pObj) );
413 if ( Gia_ObjIsXor(pObj) )
414 {
415 Abc_TtXor( Sbd_ObjSim0(p, Node),
416 Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
417 Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
418 p->pPars->nWords,
419 Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
420
421 if ( pObj->fMark0 )
422 Abc_TtXor( Sbd_ObjSim1(p, Node),
423 Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
424 Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
425 p->pPars->nWords,
426 Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
427 }
428 else
429 {
430 Abc_TtAndCompl( Sbd_ObjSim0(p, Node),
431 Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
432 Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
433 p->pPars->nWords );
434
435 if ( pObj->fMark0 )
436 Abc_TtAndCompl( Sbd_ObjSim1(p, Node),
437 Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
438 Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
439 p->pPars->nWords );
440 }
441 if ( Node != NodeInit )
442 Abc_TtCopy( Sbd_ObjSim0(p, NodeInit), Sbd_ObjSim0(p, Node), p->pPars->nWords, Abc_LitIsCompl(Vec_IntEntry(p->vMirrors, NodeInit)) );
443}
444int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
445{
446 abctime clk = Abc_Clock();
447 int i, Node;
448 // assign pivot and TFO (assume siminfo is assigned at the PIs)
449 p->Pivot = Pivot;
450 p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
451 // add constant node
452 Vec_IntClear( p->vWinObjs );
453 Vec_IntWriteEntry( p->vObj2Var, 0, Vec_IntSize(p->vWinObjs) );
454 Vec_IntPush( p->vWinObjs, 0 );
455 // simulate TFI cone
456 Gia_ManIncrementTravId( p->pGia );
457 Gia_ObjSetTravIdCurrentId(p->pGia, 0);
458 Sbd_ManWindowSim_rec( p, Pivot );
459 if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
460 {
461 p->timeWin += Abc_Clock() - clk;
462 return 0;
463 }
464 Sbd_ManUpdateOrder( p, Pivot );
465 assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
466 assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
467 // simulate node
468 Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
469 Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
470 // mark TFO and simulate extended TFI without adding TFO nodes
471 Vec_IntClear( p->vRoots );
472 Vec_IntForEachEntry( p->vTfo, Node, i )
473 {
474 Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1;
475 if ( !Abc_LitIsCompl(Node) )
476 continue;
477 Sbd_ManWindowSim_rec( p, Abc_Lit2Var(Node) );
478 Vec_IntPush( p->vRoots, Abc_Lit2Var(Node) );
479 }
480 // add TFO nodes and remove marks
481 Gia_ManObj(p->pGia, Pivot)->fMark0 = 0;
482 Vec_IntForEachEntry( p->vTfo, Node, i )
483 {
484 Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 0;
485 Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) );
486 Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) );
487 }
488 if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
489 {
490 p->timeWin += Abc_Clock() - clk;
491 return 0;
492 }
493 // compute controlability for node
494 if ( Vec_IntSize(p->vTfo) == 0 )
495 Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
496 else
497 Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
498 Vec_IntForEachEntry( p->vTfo, Node, i )
499 if ( Abc_LitIsCompl(Node) ) // root
500 Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords );
501 p->timeWin += Abc_Clock() - clk;
502 // propagate controlability to fanins for the TFI nodes starting from the pivot
503 Sbd_ManPropagateControl( p, Pivot );
504 assert( Vec_IntSize(p->vDivValues) <= 64 );
505 return (int)(Vec_IntSize(p->vDivValues) <= 64);
506}
507
519int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
520{
521 int nMintCount = 1;
522 Vec_Ptr_t * vSims;
523 word * pSims = Sbd_ObjSim0( p, Pivot );
524 word * pCtrl = Sbd_ObjSim2( p, Pivot );
525 int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
526 int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
527
528 abctime clk = Abc_Clock();
529 p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
530 p->timeCnf += Abc_Clock() - clk;
531 if ( p->pSat == NULL )
532 {
533 //if ( p->pPars->fVerbose )
534 // printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
535 Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
536 p->nLuts[0]++;
537 return 0;
538 }
539 //return -1;
540 //Sbd_ManPrintObj( p, Pivot );
541
542 // count the number of on-set and off-set care-set minterms
543 Vec_IntClear( p->vLits );
544 for ( i = 0; i < 64; i++ )
545 if ( Abc_TtGetBit(pCtrl, i) )
546 nCares[Abc_TtGetBit(pSims, i)]++;
547 else
548 Vec_IntPush( p->vLits, i );
549 fFindOnset = (int)(nCares[0] < nCares[1]);
550 if ( nCares[0] >= nMintCount && nCares[1] >= nMintCount )
551 return -1;
552 // find how many do we need
553 nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
554 nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
555
556 if ( p->pPars->fVeryVerbose )
557 printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot );
558
559 if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] )
560 Vec_IntShrink( p->vLits, nCares[0] + nCares[1] );
561 else
562 {
563 // collect places to insert new minterms
564 for ( i = 0; i < 64 && Vec_IntSize(p->vLits) < nCares[0] + nCares[1]; i++ )
565 if ( fFindOnset == Abc_TtGetBit(pSims, i) )
566 Vec_IntPush( p->vLits, i );
567 }
568 // collect simulation pointers
569 vSims = Vec_PtrAlloc( PivotVar + 1 );
570 Vec_IntForEachEntry( p->vWinObjs, iObj, i )
571 {
572 Vec_PtrPush( vSims, Sbd_ObjSim0(p, iObj) );
573 if ( iObj == Pivot )
574 break;
575 }
576 assert( i == PivotVar );
577 // compute patterns
578 RetValue = Sbd_ManCollectConstants( p->pSat, nCares, PivotVar, (word **)Vec_PtrArray(vSims), p->vLits );
579 // print computed miterms
580 if ( 0 && RetValue < 0 )
581 {
582 Vec_Int_t * vPis = Vec_WecEntry(p->vDivLevels, 0);
583 int i, k, Ind;
584 printf( "Additional minterms:\n" );
585 Vec_IntForEachEntry( p->vLits, Ind, k )
586 {
587 for ( i = 0; i < Vec_IntSize(vPis); i++ )
588 printf( "%d", Abc_TtGetBit( (word *)Vec_PtrEntry(vSims, Vec_IntEntry(p->vWinObjs, i)), Ind ) );
589 printf( "\n" );
590 }
591 }
592 Vec_PtrFree( vSims );
593 if ( RetValue >= 0 )
594 {
595 if ( p->pPars->fVeryVerbose )
596 printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
597 Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
598 p->nLuts[0]++;
599 return RetValue;
600 }
601 // set controlability of these minterms
602 Vec_IntForEachEntry( p->vLits, Ind, i )
603 Abc_TtSetBit( pCtrl, Ind );
604 // propagate controlability to fanins for the TFI nodes starting from the pivot
605 Sbd_ManPropagateControl( p, Pivot );
606 // double check that we now have enough minterms
607 for ( i = 0; i < 64; i++ )
608 if ( Abc_TtGetBit(pCtrl, i) )
609 nCares[Abc_TtGetBit(pSims, i)]++;
610 assert( nCares[0] >= nMintCount && nCares[1] >= nMintCount );
611 return -1;
612}
613
625static inline void Sbd_TransposeMatrix64( word A[64] )
626{
627 int j, k;
628 word t, m = 0x00000000FFFFFFFF;
629 for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
630 {
631 for ( k = 0; k < 64; k = (k + j + 1) & ~j )
632 {
633 t = (A[k] ^ (A[k+j] >> j)) & m;
634 A[k] = A[k] ^ t;
635 A[k+j] = A[k+j] ^ (t << j);
636 }
637 }
638}
639static inline void Sbd_PrintMatrix64( word A[64] )
640{
641 int j, k;
642 for ( j = 0; j < 64; j++, printf("\n") )
643 for ( k = 0; k < 64; k++ )
644 printf( "%d", (int)((A[j] >> k) & 1) );
645 printf( "\n" );
646}
647
659void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
660{
661 int nDivs = Vec_IntEntry(p->vObj2Var, Pivot) + 1;
662 int i, k, k0, k1, Id, Bit0, Bit1;
663
664 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
665 printf( "%3d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" );
666
667 assert( p->Pivot == Pivot );
668 Vec_IntClear( p->vCounts[0] );
669 Vec_IntClear( p->vCounts[1] );
670
671 printf( "Node %d. Useful divisors = %d.\n", Pivot, Vec_IntSize(p->vDivValues) );
672 printf( "Lev : " );
673 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
674 {
675 if ( i == nDivs-1 )
676 printf( " " );
677 printf( "%d", Vec_IntEntry(p->vLutLevs, Id) );
678 }
679 printf( "\n" );
680 printf( "\n" );
681
682 if ( nDivs > 99 )
683 {
684 printf( " : " );
685 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
686 {
687 if ( i == nDivs-1 )
688 printf( " " );
689 printf( "%d", Id / 100 );
690 }
691 printf( "\n" );
692 }
693 if ( nDivs > 9 )
694 {
695 printf( " : " );
696 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
697 {
698 if ( i == nDivs-1 )
699 printf( " " );
700 printf( "%d", (Id % 100) / 10 );
701 }
702 printf( "\n" );
703 }
704 if ( nDivs > 0 )
705 {
706 printf( " : " );
707 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
708 {
709 if ( i == nDivs-1 )
710 printf( " " );
711 printf( "%d", Id % 10 );
712 }
713 printf( "\n" );
714 printf( "\n" );
715 }
716
717 // sampling matrix
718 for ( k = 0; k < p->pPars->nWords * 64; k++ )
719 {
720 if ( !Abc_TtGetBit(Sbd_ObjSim2(p, Pivot), k) )
721 continue;
722
723 printf( "%3d : ", k );
724 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
725 {
726 word * pSims = Sbd_ObjSim0( p, Id );
727 word * pCtrl = Sbd_ObjSim2( p, Id );
728 if ( i == nDivs-1 )
729 {
730 if ( Abc_TtGetBit(pCtrl, k) )
731 Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
732 printf( " " );
733 }
734 printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' );
735 }
736 printf( "\n" );
737
738 printf( "%3d : ", k );
739 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
740 {
741 word * pSims = Sbd_ObjSim0( p, Id );
742 word * pCtrl = Sbd_ObjSim3( p, Id );
743 if ( i == nDivs-1 )
744 {
745 if ( Abc_TtGetBit(pCtrl, k) )
746 Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
747 printf( " " );
748 }
749 printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' );
750 }
751 printf( "\n" );
752
753 printf( "Sims: " );
754 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
755 {
756 word * pSims = Sbd_ObjSim0( p, Id );
757 //word * pCtrl = Sbd_ObjSim2( p, Id );
758 if ( i == nDivs-1 )
759 printf( " " );
760 printf( "%c", '0' + Abc_TtGetBit(pSims, k) );
761 }
762 printf( "\n" );
763
764 printf( "Ctrl: " );
765 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
766 {
767 //word * pSims = Sbd_ObjSim0( p, Id );
768 word * pCtrl = Sbd_ObjSim2( p, Id );
769 if ( i == nDivs-1 )
770 printf( " " );
771 printf( "%c", '0' + Abc_TtGetBit(pCtrl, k) );
772 }
773 printf( "\n" );
774
775
776 printf( "\n" );
777 }
778 // covering table
779 printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) );
780/*
781 Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, Abc_MinInt(Vec_IntSize(p->vCounts[0]), 8) )
782 Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, Abc_MinInt(Vec_IntSize(p->vCounts[1]), 8) )
783 {
784 printf( "%3d %3d : ", Bit0, Bit1 );
785 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
786 {
787 word * pSims = Sbd_ObjSim0( p, Id );
788 word * pCtrl = Sbd_ObjSim2( p, Id );
789 if ( i == nDivs-1 )
790 printf( " " );
791 printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' );
792 }
793 printf( "\n" );
794 }
795*/
796 Vec_WrdClear( p->vMatrix );
797 Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, Abc_MinInt(Vec_IntSize(p->vCounts[0]), 64) )
798 Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, Abc_MinInt(Vec_IntSize(p->vCounts[1]), 64) )
799 {
800 word Row = 0;
801 Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
802 {
803 word * pSims = Sbd_ObjSim0( p, Id );
804 word * pCtrl = Sbd_ObjSim2( p, Id );
805 if ( Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1) )
806 Abc_TtXorBit( &Row, i );
807 }
808 if ( Vec_WrdPushUnique( p->vMatrix, Row ) )
809 continue;
810 for ( i = 0; i < nDivs; i++ )
811 printf( "%d", (int)((Row >> i) & 1) );
812 printf( "\n" );
813 }
814}
815
816void Sbd_ManMatrPrint( Sbd_Man_t * p, word Cover[], int nCol, int nRows )
817{
818 int i, k;
819 for ( i = 0; i <= nCol; i++ )
820 {
821 printf( "%2d : ", i );
822 printf( "%d ", i == nCol ? Vec_IntEntry(p->vLutLevs, p->Pivot) : Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
823 for ( k = 0; k < nRows; k++ )
824 printf( "%d", (int)((Cover[i] >> k) & 1) );
825 printf( "\n");
826 }
827 printf( "\n");
828}
829static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
830{
831 int i;
832 for ( i = 0; i < 32; i++ )
833 {
834 word Cube = Cover[i];
835 Cover[i] = Cover[63-i];
836 Cover[63-i] = Cube;
837 }
838}
839
840static inline int Sbd_ManAddCube1( int nRowLimit, word Cover[], int nRows, word Cube )
841{
842 int n, m;
843 if ( 0 )
844 {
845 printf( "Adding cube: " );
846 for ( n = 0; n < nRowLimit; n++ )
847 printf( "%d", (int)((Cube >> n) & 1) );
848 printf( "\n" );
849 }
850 // do not add contained Cube
851 assert( nRows <= nRowLimit );
852 for ( n = 0; n < nRows; n++ )
853 if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
854 return nRows;
855 // remove rows contained by Cube
856 for ( n = m = 0; n < nRows; n++ )
857 if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained
858 Cover[m++] = Cover[n];
859 if ( m < nRowLimit )
860 Cover[m++] = Cube;
861 for ( n = m; n < nRows; n++ )
862 Cover[n] = 0;
863 nRows = m;
864 return nRows;
865}
866static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
867{
868 int n, m;
869 // do not add contained Cube
870 assert( nRows <= 64 );
871 for ( n = 0; n < nRows; n++ )
872 if ( (Cover[0][n] & Cube[0]) == Cover[0][n] && (Cover[1][n] & Cube[1]) == Cover[1][n] ) // Cube is contained
873 return nRows;
874 // remove rows contained by Cube
875 for ( n = m = 0; n < nRows; n++ )
876 if ( (Cover[0][n] & Cube[0]) != Cube[0] || (Cover[1][n] & Cube[1]) != Cube[1] ) // Cover[n] is not contained
877 {
878 Cover[0][m] = Cover[0][n];
879 Cover[1][m] = Cover[1][n];
880 m++;
881 }
882 if ( m < 64 )
883 {
884 Cover[0][m] = Cube[0];
885 Cover[1][m] = Cube[1];
886 m++;
887 }
888 for ( n = m; n < nRows; n++ )
889 Cover[0][n] = Cover[1][n] = 0;
890 nRows = m;
891 return nRows;
892}
893
894static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[], int nDivs )
895{
896 int c0, c1, c2, c3;
897 word Target = Cover[nDivs];
898 Vec_IntClear( p->vDivSet );
899 for ( c0 = 0; c0 < nDivs; c0++ )
900 if ( Cover[c0] == Target )
901 {
902 Vec_IntPush( p->vDivSet, c0 );
903 return 1;
904 }
905
906 for ( c0 = 0; c0 < nDivs; c0++ )
907 for ( c1 = c0+1; c1 < nDivs; c1++ )
908 if ( (Cover[c0] | Cover[c1]) == Target )
909 {
910 Vec_IntPush( p->vDivSet, c0 );
911 Vec_IntPush( p->vDivSet, c1 );
912 return 1;
913 }
914
915 for ( c0 = 0; c0 < nDivs; c0++ )
916 for ( c1 = c0+1; c1 < nDivs; c1++ )
917 for ( c2 = c1+1; c2 < nDivs; c2++ )
918 if ( (Cover[c0] | Cover[c1] | Cover[c2]) == Target )
919 {
920 Vec_IntPush( p->vDivSet, c0 );
921 Vec_IntPush( p->vDivSet, c1 );
922 Vec_IntPush( p->vDivSet, c2 );
923 return 1;
924 }
925
926 for ( c0 = 0; c0 < nDivs; c0++ )
927 for ( c1 = c0+1; c1 < nDivs; c1++ )
928 for ( c2 = c1+1; c2 < nDivs; c2++ )
929 for ( c3 = c2+1; c3 < nDivs; c3++ )
930 {
931 if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
932 {
933 Vec_IntPush( p->vDivSet, c0 );
934 Vec_IntPush( p->vDivSet, c1 );
935 Vec_IntPush( p->vDivSet, c2 );
936 Vec_IntPush( p->vDivSet, c3 );
937 return 1;
938 }
939 }
940 return 0;
941}
942
943static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
944{
945 int Ones[64], Order[64];
946 int Limits[4] = { nDivs/4+1, nDivs/3+2, nDivs/2+3, nDivs };
947 int c0, c1, c2, c3;
948 word Target = Cover[nDivs];
949
950 if ( nDivs < 8 || p->pPars->fCover )
951 return Sbd_ManFindCandsSimple( p, Cover, nDivs );
952
953 Vec_IntClear( p->vDivSet );
954 for ( c0 = 0; c0 < nDivs; c0++ )
955 if ( Cover[c0] == Target )
956 {
957 Vec_IntPush( p->vDivSet, c0 );
958 return 1;
959 }
960
961 for ( c0 = 0; c0 < nDivs; c0++ )
962 for ( c1 = c0+1; c1 < nDivs; c1++ )
963 if ( (Cover[c0] | Cover[c1]) == Target )
964 {
965 Vec_IntPush( p->vDivSet, c0 );
966 Vec_IntPush( p->vDivSet, c1 );
967 return 1;
968 }
969
970 // count ones
971 for ( c0 = 0; c0 < nDivs; c0++ )
972 Ones[c0] = Abc_TtCountOnes( Cover[c0] );
973
974 // sort by the number of ones
975 for ( c0 = 0; c0 < nDivs; c0++ )
976 Order[c0] = c0;
977 Vec_IntSelectSortCost2Reverse( Order, nDivs, Ones );
978
979 // sort with limits
980 for ( c0 = 0; c0 < Limits[0]; c0++ )
981 for ( c1 = c0+1; c1 < Limits[1]; c1++ )
982 for ( c2 = c1+1; c2 < Limits[2]; c2++ )
983 if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
984 {
985 Vec_IntPush( p->vDivSet, Order[c0] );
986 Vec_IntPush( p->vDivSet, Order[c1] );
987 Vec_IntPush( p->vDivSet, Order[c2] );
988 return 1;
989 }
990
991 for ( c0 = 0; c0 < Limits[0]; c0++ )
992 for ( c1 = c0+1; c1 < Limits[1]; c1++ )
993 for ( c2 = c1+1; c2 < Limits[2]; c2++ )
994 for ( c3 = c2+1; c3 < Limits[3]; c3++ )
995 {
996 if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
997 {
998 Vec_IntPush( p->vDivSet, Order[c0] );
999 Vec_IntPush( p->vDivSet, Order[c1] );
1000 Vec_IntPush( p->vDivSet, Order[c2] );
1001 Vec_IntPush( p->vDivSet, Order[c3] );
1002 return 1;
1003 }
1004 }
1005 return 0;
1006}
1007
1008
1009int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
1010{
1011 int fVerbose = 0;
1012 abctime clk;
1013 int nIters, nItersMax = 32;
1014
1015 word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
1016 int i, k, n, Node, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
1017
1018 int nDivs = Vec_IntSize(p->vDivValues);
1019 int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
1020 int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
1021 int RetValue = 0;
1022
1023 if ( p->pPars->fVerbose )
1024 printf( "Node %d. Useful divisors = %d.\n", Pivot, nDivs );
1025
1026 if ( fVerbose )
1027 Sbd_ManPrintObj( p, Pivot );
1028
1029 // collect bit-matrices
1030 Vec_IntForEachEntry( p->vDivVars, Node, i )
1031 {
1032 MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, Node) );
1033 MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, Node) );
1034 MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, Node) );
1035 }
1036 MatrS[63-i] = *Sbd_ObjSim0( p, Pivot );
1037 MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
1038 MatrC[1][63-i] = *Sbd_ObjSim3( p, Pivot );
1039
1040 //Sbd_PrintMatrix64( MatrS );
1041 Sbd_TransposeMatrix64( MatrS );
1042 Sbd_TransposeMatrix64( MatrC[0] );
1043 Sbd_TransposeMatrix64( MatrC[1] );
1044 //Sbd_PrintMatrix64( MatrS );
1045
1046 // collect cubes
1047 for ( i = 0; i < 64; i++ )
1048 {
1049 assert( Abc_TtGetBit(&MatrC[0][i], nDivs) == Abc_TtGetBit(&MatrC[1][i], nDivs) );
1050 if ( !Abc_TtGetBit(&MatrC[0][i], nDivs) )
1051 continue;
1052 Index = Abc_TtGetBit(&MatrS[i], nDivs); // Index==0 offset; Index==1 onset
1053 for ( n = 0; n < 2; n++ )
1054 {
1055 if ( n && MatrC[0][i] == MatrC[1][i] )
1056 continue;
1057 assert( MatrC[n][i] );
1058 CubeNew[0] = ~MatrS[i] & MatrC[n][i];
1059 CubeNew[1] = MatrS[i] & MatrC[n][i];
1060 assert( CubeNew[0] || CubeNew[1] );
1061 nCubes[Index] = Sbd_ManAddCube2( Cubes[Index], nCubes[Index], CubeNew );
1062 }
1063 }
1064
1065 if ( p->pPars->fVerbose )
1066 printf( "Generated matrix with %d x %d entries.\n", nCubes[0], nCubes[1] );
1067
1068 if ( p->pPars->fVerbose )
1069 for ( n = 0; n < 2; n++ )
1070 {
1071 printf( "%s:\n", n ? "Onset" : "Offset" );
1072 for ( i = 0; i < nCubes[n]; i++, printf( "\n" ) )
1073 for ( k = 0; k < 64; k++ )
1074 if ( Abc_TtGetBit(&Cubes[n][0][i], k) )
1075 printf( "0" );
1076 else if ( Abc_TtGetBit(&Cubes[n][1][i], k) )
1077 printf( "1" );
1078 else
1079 printf( "." );
1080 printf( "\n" );
1081 }
1082
1083 // create covering table
1084 nRows = 0;
1085 for ( i = 0; i < nCubes[0] && nRows < 32; i++ )
1086 for ( k = 0; k < nCubes[1] && nRows < 32; k++ )
1087 {
1088 Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
1089 assert( Cube );
1090 nRows = Sbd_ManAddCube1( 64, Cover, nRows, Cube );
1091 }
1092
1093 Sbd_ManCoverReverseOrder( Cover );
1094
1095 if ( p->pPars->fVerbose )
1096 printf( "Generated cover with %d entries.\n", nRows );
1097
1098 //if ( p->pPars->fVerbose )
1099 //Sbd_PrintMatrix64( Cover );
1100 Sbd_TransposeMatrix64( Cover );
1101 //if ( p->pPars->fVerbose )
1102 //Sbd_PrintMatrix64( Cover );
1103
1104 Sbd_ManCoverReverseOrder( Cover );
1105
1106 nRowsOld = nRows;
1107 for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
1108 {
1109 if ( p->pPars->fVerbose )
1110 Sbd_ManMatrPrint( p, Cover, nDivs, nRows );
1111
1112 clk = Abc_Clock();
1113 if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
1114 {
1115 if ( p->pPars->fVerbose )
1116 printf( "Cannot find a feasible cover.\n" );
1117 p->timeCov += Abc_Clock() - clk;
1118 return RetValue;
1119 }
1120 p->timeCov += Abc_Clock() - clk;
1121
1122 if ( p->pPars->fVerbose )
1123 printf( "Candidate support: " ),
1124 Vec_IntPrint( p->vDivSet );
1125
1126 clk = Abc_Clock();
1127 *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
1128 p->timeSat += Abc_Clock() - clk;
1129
1130 if ( *pTruth == SBD_SAT_UNDEC )
1131 printf( "Node %d: Undecided.\n", Pivot );
1132 else if ( *pTruth == SBD_SAT_SAT )
1133 {
1134 if ( p->pPars->fVerbose )
1135 {
1136 int i;
1137 printf( "Node %d: SAT.\n", Pivot );
1138 for ( i = 0; i < nDivs; i++ )
1139 printf( "%d", i % 10 );
1140 printf( "\n" );
1141 for ( i = 0; i < nDivs; i++ )
1142 printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
1143 printf( "\n" );
1144 for ( i = 0; i < nDivs; i++ )
1145 printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
1146 printf( "\n" );
1147 }
1148 // add row to the covering table
1149 for ( i = 0; i < nDivs; i++ )
1150 if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
1151 Cover[i] |= ((word)1 << nRows);
1152 Cover[nDivs] |= ((word)1 << nRows);
1153 nRows++;
1154 }
1155 else
1156 {
1157 if ( p->pPars->fVerbose )
1158 {
1159 printf( "Node %d: UNSAT.\n", Pivot );
1160 Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
1161 }
1162 RetValue = 1;
1163 break;
1164 }
1165 //break;
1166 }
1167 return RetValue;
1168}
1169
1170int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
1171{
1172 abctime clk;
1173 word Onset[64] = {0}, Offset[64] = {0}, Cube;
1174 word CoverRows[64] = {0}, CoverCols[64] = {0};
1175 int nIters, nItersMax = 32;
1176 int i, k, nRows = 0;
1177
1178 int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
1179 int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
1180 int nDivs = Vec_IntSize( p->vDivVars );
1181 int nConsts = 4;
1182 int RetValue;
1183
1184 clk = Abc_Clock();
1185 //sat_solver_delete_p( &p->pSat );
1186 p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
1187 p->timeCnf += Abc_Clock() - clk;
1188
1189 assert( nConsts <= 8 );
1190 clk = Abc_Clock();
1191 RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
1192 p->timeSat += Abc_Clock() - clk;
1193 if ( RetValue >= 0 )
1194 {
1195 if ( p->pPars->fVeryVerbose )
1196 printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
1197 Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
1198 p->nLuts[0]++;
1199 return RetValue;
1200 }
1201 RetValue = 0;
1202
1203 // create rows of the table
1204 nRows = 0;
1205 for ( i = 0; i < nConsts; i++ )
1206 for ( k = 0; k < nConsts; k++ )
1207 {
1208 Cube = Onset[i] ^ Offset[k];
1209 assert( Cube );
1210 nRows = Sbd_ManAddCube1( 256, CoverRows, nRows, Cube );
1211 }
1212 assert( nRows <= 64 );
1213
1214 // create columns of the table
1215 for ( i = 0; i < nRows; i++ )
1216 for ( k = 0; k <= nDivs; k++ )
1217 if ( (CoverRows[i] >> k) & 1 )
1218 Abc_TtXorBit(&CoverCols[k], i);
1219
1220 // solve the covering problem
1221 for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
1222 {
1223 if ( p->pPars->fVeryVerbose )
1224 Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
1225
1226 clk = Abc_Clock();
1227 if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) )
1228 {
1229 if ( p->pPars->fVeryVerbose )
1230 printf( "Cannot find a feasible cover.\n" );
1231 p->timeCov += Abc_Clock() - clk;
1232 return 0;
1233 }
1234 p->timeCov += Abc_Clock() - clk;
1235
1236 if ( p->pPars->fVeryVerbose )
1237 printf( "Candidate support: " ),
1238 Vec_IntPrint( p->vDivSet );
1239
1240 clk = Abc_Clock();
1241 *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
1242 p->timeSat += Abc_Clock() - clk;
1243
1244 if ( *pTruth == SBD_SAT_UNDEC )
1245 printf( "Node %d: Undecided.\n", Pivot );
1246 else if ( *pTruth == SBD_SAT_SAT )
1247 {
1248 if ( p->pPars->fVeryVerbose )
1249 {
1250 int i;
1251 printf( "Node %d: SAT.\n", Pivot );
1252 for ( i = 0; i < nDivs; i++ )
1253 printf( "%d", Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
1254 printf( "\n" );
1255 for ( i = 0; i < nDivs; i++ )
1256 printf( "%d", i % 10 );
1257 printf( "\n" );
1258 for ( i = 0; i < nDivs; i++ )
1259 printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
1260 printf( "\n" );
1261 for ( i = 0; i < nDivs; i++ )
1262 printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
1263 printf( "\n" );
1264 }
1265 // add row to the covering table
1266 for ( i = 0; i < nDivs; i++ )
1267 if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
1268 CoverCols[i] |= ((word)1 << nRows);
1269 CoverCols[nDivs] |= ((word)1 << nRows);
1270 nRows++;
1271 }
1272 else
1273 {
1274 if ( p->pPars->fVeryVerbose )
1275 {
1276 printf( "Node %d: UNSAT. ", Pivot );
1277 Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
1278 }
1279 p->nLuts[1]++;
1280 RetValue = 1;
1281 break;
1282 }
1283 }
1284 return RetValue;
1285}
1286
1287int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int * pnStrs, Sbd_Str_t * Strs, int * pFreeVar )
1288{
1289 abctime clk = Abc_Clock();
1290 int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
1291 int Delay = Vec_IntEntry( p->vLutLevs, Pivot );
1292 int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodesBot1[SBD_DIV_MAX], pNodesBot2[SBD_DIV_MAX];
1293 int nNodesTop = 0, nNodesBot = 0, nNodesBot1 = 0, nNodesBot2 = 0, nNodesDiff = 0, nNodesDiff1 = 0, nNodesDiff2 = 0;
1294 int i, k, iObj, nIters, RetValue = 0;
1295
1296 // try to remove fanins
1297 for ( nIters = 0; nIters < nLeaves; nIters++ )
1298 {
1299 word Truth;
1300 // try to remove one variable from divisors
1301 Vec_IntClear( p->vDivSet );
1302 for ( i = 0; i < nLeaves; i++ )
1303 if ( i != nLeaves-1-nIters && pLeaves[i] != -1 )
1304 Vec_IntPush( p->vDivSet, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
1305 assert( Vec_IntSize(p->vDivSet) < nLeaves );
1306 // compute truth table
1307 clk = Abc_Clock();
1308 Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
1309 p->timeSat += Abc_Clock() - clk;
1310 if ( Truth == SBD_SAT_UNDEC )
1311 printf( "Node %d: Undecided.\n", Pivot );
1312 else if ( Truth == SBD_SAT_SAT )
1313 {
1314 int DelayDiff = Vec_IntEntry(p->vLutLevs, pLeaves[nLeaves-1-nIters]) - Delay;
1315 if ( DelayDiff > -2 )
1316 return 0;
1317 }
1318 else
1319 pLeaves[nLeaves-1-nIters] = -1;
1320 }
1321 Vec_IntClear( p->vDivSet );
1322 for ( i = 0; i < nLeaves; i++ )
1323 if ( pLeaves[i] != -1 )
1324 Vec_IntPush( p->vDivSet, pLeaves[i] );
1325 //printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
1326 if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
1327 {
1328 word Truth;
1329 *pnStrs = 1;
1330 // remap divisors
1331 Vec_IntForEachEntry( p->vDivSet, iObj, i )
1332 Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
1333 // compute truth table
1334 clk = Abc_Clock();
1335 Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
1336 p->timeSat += Abc_Clock() - clk;
1337 if ( Truth == SBD_SAT_SAT )
1338 {
1339 printf( "The cut at node %d is not topological.\n", p->Pivot );
1340 return 0;
1341 }
1342 assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
1343 // create structure
1344 Strs->fLut = 1;
1345 Strs->nVarIns = Vec_IntSize( p->vDivSet );
1346 for ( i = 0; i < Strs->nVarIns; i++ )
1347 Strs->VarIns[i] = i;
1348 Strs->Res = Truth;
1349 p->nLuts[1]++;
1350 //Extra_PrintBinary( stdout, (unsigned *)&Truth, 1 << Strs->nVarIns ), printf( "\n" );
1351 return 1;
1352 }
1353 assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
1354
1355 // count number of nodes on each level
1356 nNodesTop = nNodesBot = nNodesBot1 = nNodesBot2 = 0;
1357 Vec_IntForEachEntry( p->vDivSet, iObj, i )
1358 {
1359 int DelayDiff = Vec_IntEntry(p->vLutLevs, iObj) - Delay;
1360 if ( DelayDiff > -2 )
1361 break;
1362 if ( DelayDiff == -2 )
1363 pNodesTop[nNodesTop++] = i;
1364 else // if ( DelayDiff < -2 )
1365 {
1366 pNodesBot[nNodesBot++] = i;
1367 if ( DelayDiff == -3 )
1368 pNodesBot1[nNodesBot1++] = i;
1369 else // if ( DelayDiff < -3 )
1370 pNodesBot2[nNodesBot2++] = i;
1371 }
1372 Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
1373 }
1374 assert( nNodesBot == nNodesBot1 + nNodesBot2 );
1375 if ( i < Vec_IntSize(p->vDivSet) )
1376 return 0;
1377 if ( nNodesTop > p->pPars->nLutSize-1 )
1378 return 0;
1379
1380 // try 44
1381 if ( Vec_IntSize(p->vDivSet) <= 2*p->pPars->nLutSize-1 )
1382 {
1383 int nMoved = 0;
1384 if ( nNodesBot > p->pPars->nLutSize ) // need to move bottom left-over to the top
1385 {
1386 while ( nNodesBot > p->pPars->nLutSize )
1387 pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
1388 assert( nNodesBot == p->pPars->nLutSize );
1389 }
1390 assert( nNodesBot <= p->pPars->nLutSize );
1391 assert( nNodesTop <= p->pPars->nLutSize-1 );
1392
1393 Strs[0].fLut = 1;
1394 Strs[0].nVarIns = p->pPars->nLutSize;
1395 for ( i = 0; i < nNodesTop; i++ )
1396 Strs[0].VarIns[i] = pNodesTop[i];
1397 for ( ; i < p->pPars->nLutSize; i++ )
1398 Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
1399 Strs[0].Res = 0;
1400
1401 Strs[1].fLut = 1;
1402 Strs[1].nVarIns = nNodesBot;
1403 for ( i = 0; i < nNodesBot; i++ )
1404 Strs[1].VarIns[i] = pNodesBot[i];
1405 Strs[1].Res = 0;
1406
1407 nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
1408 assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
1409 for ( k = 0; k < nNodesDiff; k++ )
1410 {
1411 Strs[2+k].fLut = 0;
1412 Strs[2+k].nVarIns = nNodesBot;
1413 for ( i = 0; i < nNodesBot; i++ )
1414 Strs[2+k].VarIns[i] = pNodesBot[i];
1415 Strs[2+k].Res = 0;
1416 }
1417
1418 *pnStrs = 2 + nNodesDiff;
1419 clk = Abc_Clock();
1420 RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
1421 p->timeQbf += Abc_Clock() - clk;
1422 if ( RetValue )
1423 p->nLuts[2]++;
1424
1425 while ( nMoved-- )
1426 pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
1427 }
1428
1429 if ( RetValue )
1430 return RetValue;
1431 if ( p->pPars->nLutNum < 3 )
1432 return 0;
1433 if ( Vec_IntSize(p->vDivSet) < 2*p->pPars->nLutSize-1 )
1434 return 0;
1435
1436 // try 444 -- LUT(LUT, LUT)
1437 if ( nNodesTop <= p->pPars->nLutSize-2 )
1438 {
1439 int nMoved = 0;
1440 if ( nNodesBot > 2*p->pPars->nLutSize ) // need to move bottom left-over to the top
1441 {
1442 while ( nNodesBot > 2*p->pPars->nLutSize )
1443 pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
1444 assert( nNodesBot == 2*p->pPars->nLutSize );
1445 }
1446 assert( nNodesBot > p->pPars->nLutSize );
1447 assert( nNodesBot <= 2*p->pPars->nLutSize );
1448 assert( nNodesTop <= p->pPars->nLutSize-2 );
1449
1450 Strs[0].fLut = 1;
1451 Strs[0].nVarIns = p->pPars->nLutSize;
1452 for ( i = 0; i < nNodesTop; i++ )
1453 Strs[0].VarIns[i] = pNodesTop[i];
1454 for ( ; i < p->pPars->nLutSize; i++ )
1455 Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
1456 Strs[0].Res = 0;
1457
1458 Strs[1].fLut = 1;
1459 Strs[1].nVarIns = p->pPars->nLutSize;
1460 for ( i = 0; i < Strs[1].nVarIns; i++ )
1461 Strs[1].VarIns[i] = pNodesBot[i];
1462 Strs[1].Res = 0;
1463
1464 Strs[2].fLut = 1;
1465 Strs[2].nVarIns = p->pPars->nLutSize;
1466 for ( i = 0; i < Strs[2].nVarIns; i++ )
1467 Strs[2].VarIns[i] = pNodesBot[nNodesBot-p->pPars->nLutSize+i];
1468 Strs[2].Res = 0;
1469
1470 nNodesDiff = p->pPars->nLutSize-2 - nNodesTop;
1471 assert( nNodesDiff >= 0 && nNodesDiff <= 2 );
1472 for ( k = 0; k < nNodesDiff; k++ )
1473 {
1474 Strs[3+k].fLut = 0;
1475 Strs[3+k].nVarIns = nNodesBot;
1476 for ( i = 0; i < nNodesBot; i++ )
1477 Strs[3+k].VarIns[i] = pNodesBot[i];
1478 Strs[3+k].Res = 0;
1479 }
1480
1481 *pnStrs = 3 + nNodesDiff;
1482 clk = Abc_Clock();
1483 RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
1484 p->timeQbf += Abc_Clock() - clk;
1485 if ( RetValue )
1486 p->nLuts[3]++;
1487
1488 while ( nMoved-- )
1489 pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
1490 }
1491 if ( RetValue )
1492 return RetValue;
1493
1494 // try 444 -- LUT(LUT(LUT))
1495 if ( nNodesBot1 + nNodesTop <= 2*p->pPars->nLutSize-2 )
1496 {
1497 if ( nNodesBot2 > p->pPars->nLutSize ) // need to move bottom left-over to the top
1498 {
1499 while ( nNodesBot2 > p->pPars->nLutSize )
1500 pNodesBot1[nNodesBot1++] = pNodesBot2[--nNodesBot2];
1501 assert( nNodesBot2 == p->pPars->nLutSize );
1502 }
1503 if ( nNodesBot1 > p->pPars->nLutSize-1 ) // need to move bottom left-over to the top
1504 {
1505 while ( nNodesBot1 > p->pPars->nLutSize-1 )
1506 pNodesTop[nNodesTop++] = pNodesBot1[--nNodesBot1];
1507 assert( nNodesBot1 == p->pPars->nLutSize-1 );
1508 }
1509 assert( nNodesBot2 <= p->pPars->nLutSize );
1510 assert( nNodesBot1 <= p->pPars->nLutSize-1 );
1511 assert( nNodesTop <= p->pPars->nLutSize-1 );
1512
1513 Strs[0].fLut = 1;
1514 Strs[0].nVarIns = p->pPars->nLutSize;
1515 for ( i = 0; i < nNodesTop; i++ )
1516 Strs[0].VarIns[i] = pNodesTop[i];
1517 Strs[0].VarIns[i++] = Vec_IntSize(p->vDivSet)+1;
1518 for ( ; i < p->pPars->nLutSize; i++ )
1519 Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+2 + i-nNodesTop;
1520 Strs[0].Res = 0;
1521 nNodesDiff1 = p->pPars->nLutSize-1 - nNodesTop;
1522
1523 Strs[1].fLut = 1;
1524 Strs[1].nVarIns = p->pPars->nLutSize;
1525 for ( i = 0; i < nNodesBot1; i++ )
1526 Strs[1].VarIns[i] = pNodesBot1[i];
1527 Strs[1].VarIns[i++] = Vec_IntSize(p->vDivSet)+2;
1528 for ( ; i < p->pPars->nLutSize; i++ )
1529 Strs[1].VarIns[i] = Vec_IntSize(p->vDivSet)+2+nNodesDiff1 + i-nNodesBot1;
1530 Strs[1].Res = 0;
1531 nNodesDiff2 = p->pPars->nLutSize-1 - nNodesBot1;
1532
1533 Strs[2].fLut = 1;
1534 Strs[2].nVarIns = nNodesBot2;
1535 for ( i = 0; i < Strs[2].nVarIns; i++ )
1536 Strs[2].VarIns[i] = pNodesBot2[i];
1537 Strs[2].Res = 0;
1538
1539 nNodesDiff = nNodesDiff1 + nNodesDiff2;
1540 assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
1541 for ( k = 0; k < nNodesDiff; k++ )
1542 {
1543 Strs[3+k].fLut = 0;
1544 Strs[3+k].nVarIns = nNodesBot2;
1545 for ( i = 0; i < nNodesBot2; i++ )
1546 Strs[3+k].VarIns[i] = pNodesBot2[i];
1547 Strs[3+k].Res = 0;
1548 if ( k >= nNodesDiff1 )
1549 continue;
1550 Strs[3+k].nVarIns += nNodesBot1;
1551 for ( i = 0; i < nNodesBot1; i++ )
1552 Strs[3+k].VarIns[nNodesBot2 + i] = pNodesBot1[i];
1553 }
1554
1555 *pnStrs = 3 + nNodesDiff;
1556 clk = Abc_Clock();
1557 RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
1558 p->timeQbf += Abc_Clock() - clk;
1559 if ( RetValue )
1560 p->nLuts[4]++;
1561 }
1562 return RetValue;
1563}
1564int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
1565{
1566 int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
1567 int FreeVarStart = FreeVar;
1568 int nSize, nLeaves, pLeaves[SBD_DIV_MAX];
1569 //sat_solver_delete_p( &p->pSat );
1570 abctime clk = Abc_Clock();
1571 p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
1572 p->timeCnf += Abc_Clock() - clk;
1573 // extract one cut
1574 if ( p->pSrv )
1575 {
1576 nLeaves = Sbd_ManCutServerFirst( p->pSrv, Pivot, pLeaves );
1577 if ( nLeaves == -1 )
1578 return 0;
1579 assert( nLeaves <= p->pPars->nCutSize );
1580 if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
1581 return 1;
1582 return 0;
1583 }
1584 // extract one cut
1585 for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ )
1586 {
1587 nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves );
1588 if ( nLeaves == -1 )
1589 continue;
1590 assert( nLeaves == nSize );
1591 if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
1592 return 1;
1593 }
1594 assert( FreeVar - FreeVarStart <= SBD_FVAR_MAX );
1595 return 0;
1596}
1597
1598
1610int Sbd_CutMergeSimple( Sbd_Man_t * p, int * pCut1, int * pCut2, int * pCut )
1611{
1612 int * pBeg = pCut + 1;
1613 int * pBeg1 = pCut1 + 1;
1614 int * pBeg2 = pCut2 + 1;
1615 int * pEnd1 = pCut1 + 1 + pCut1[0];
1616 int * pEnd2 = pCut2 + 1 + pCut2[0];
1617 while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
1618 {
1619 if ( *pBeg1 == *pBeg2 )
1620 *pBeg++ = *pBeg1++, pBeg2++;
1621 else if ( *pBeg1 < *pBeg2 )
1622 *pBeg++ = *pBeg1++;
1623 else
1624 *pBeg++ = *pBeg2++;
1625 }
1626 while ( pBeg1 < pEnd1 )
1627 *pBeg++ = *pBeg1++;
1628 while ( pBeg2 < pEnd2 )
1629 *pBeg++ = *pBeg2++;
1630 return (pCut[0] = pBeg - pCut - 1);
1631}
1632/*
1633int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
1634{
1635 int Result = 1; // no need to resynthesize
1636 int pCut[2*SBD_MAX_LUTSIZE+1];
1637 int iFan0 = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
1638 int iFan1 = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
1639 int Level0 = Vec_IntEntry( p->vLutLevs, iFan0 );
1640 int Level1 = Vec_IntEntry( p->vLutLevs, iFan1 );
1641 int LevMax = (Level0 || Level1) ? Abc_MaxInt(Level0, Level1) : 1;
1642 int * pCut0 = Sbd_ObjCut( p, iFan0 );
1643 int * pCut1 = Sbd_ObjCut( p, iFan1 );
1644 int nSize = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut );
1645 if ( nSize > p->pPars->nLutSize )
1646 {
1647 if ( Level0 != Level1 )
1648 {
1649 int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0;
1650 int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1;
1651 nSize = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut );
1652 }
1653 if ( nSize > p->pPars->nLutSize )
1654 {
1655 pCut[0] = 2;
1656 pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1;
1657 pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0;
1658 Result = LevMax ? 0 : 1;
1659 LevMax++;
1660 }
1661 }
1662 assert( iFan0 != iFan1 );
1663 assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
1664 Vec_IntWriteEntry( p->vLutLevs, Node, LevMax );
1665 memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
1666 //printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result );
1667 return Result;
1668}
1669*/
1670int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
1671{
1672 int pCut11[2*SBD_MAX_LUTSIZE+1];
1673 int pCut01[2*SBD_MAX_LUTSIZE+1];
1674 int pCut10[2*SBD_MAX_LUTSIZE+1];
1675 int pCut00[2*SBD_MAX_LUTSIZE+1];
1676 int iFan0 = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
1677 int iFan1 = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
1678 int Level0 = Vec_IntEntry( p->vLutLevs, iFan0 ) ? Vec_IntEntry( p->vLutLevs, iFan0 ) : 1;
1679 int Level1 = Vec_IntEntry( p->vLutLevs, iFan1 ) ? Vec_IntEntry( p->vLutLevs, iFan1 ) : 1;
1680 int * pCut0 = Sbd_ObjCut( p, iFan0 );
1681 int * pCut1 = Sbd_ObjCut( p, iFan1 );
1682 int Cut0[2] = {1, iFan0};
1683 int Cut1[2] = {1, iFan1};
1684 int nSize11 = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut11 );
1685 int nSize01 = Sbd_CutMergeSimple( p, Cut0, pCut1, pCut01 );
1686 int nSize10 = Sbd_CutMergeSimple( p, pCut0, Cut1, pCut10 );
1687 int nSize00 = Sbd_CutMergeSimple( p, Cut0, Cut1, pCut00 );
1688 int Lev11 = nSize11 <= p->pPars->nLutSize ? Abc_MaxInt(Level0, Level1) : ABC_INFINITY;
1689 int Lev01 = nSize01 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1) : ABC_INFINITY;
1690 int Lev10 = nSize10 <= p->pPars->nLutSize ? Abc_MaxInt(Level0, Level1+1) : ABC_INFINITY;
1691 int Lev00 = nSize00 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1+1) : ABC_INFINITY;
1692 int * pCutRes = pCut11;
1693 int LevCur = Lev11;
1694 if ( Lev01 < LevCur || (Lev01 == LevCur && pCut01[0] < pCutRes[0]) )
1695 {
1696 pCutRes = pCut01;
1697 LevCur = Lev01;
1698 }
1699 if ( Lev10 < LevCur || (Lev10 == LevCur && pCut10[0] < pCutRes[0]) )
1700 {
1701 pCutRes = pCut10;
1702 LevCur = Lev10;
1703 }
1704 if ( Lev00 < LevCur || (Lev00 == LevCur && pCut00[0] < pCutRes[0]) )
1705 {
1706 pCutRes = pCut00;
1707 LevCur = Lev00;
1708 }
1709 assert( iFan0 != iFan1 );
1710 assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
1711 Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
1712 //Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, iFan0), Vec_IntEntry(p->vLevs, iFan1)) );
1713 assert( pCutRes[0] <= p->pPars->nLutSize );
1714 memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
1715//printf( "Setting node %d with delay %d.\n", Node, LevCur );
1716 return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
1717}
1718int Sbd_ManDelay( Sbd_Man_t * p )
1719{
1720 int i, Id, Delay = 0;
1721 Gia_ManForEachCoDriverId( p->pGia, Id, i )
1722 Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vLutLevs, Id) );
1723 return Delay;
1724}
1725void Sbd_ManMergeTest( Sbd_Man_t * p )
1726{
1727 int Node;
1728 Gia_ManForEachAndId( p->pGia, Node )
1729 Sbd_ManMergeCuts( p, Node );
1730 printf( "Delay %d.\n", Sbd_ManDelay(p) );
1731}
1732
1733void Sbd_ManFindCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1734{
1735 if ( pObj->fMark1 )
1736 return;
1737 pObj->fMark1 = 1;
1738 if ( pObj->fMark0 )
1739 return;
1740 assert( Gia_ObjIsAnd(pObj) );
1741 Sbd_ManFindCut_rec( p, Gia_ObjFanin0(pObj) );
1742 Sbd_ManFindCut_rec( p, Gia_ObjFanin1(pObj) );
1743}
1744void Sbd_ManFindCutUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
1745{
1746 if ( !pObj->fMark1 )
1747 return;
1748 pObj->fMark1 = 0;
1749 if ( pObj->fMark0 )
1750 return;
1751 assert( Gia_ObjIsAnd(pObj) );
1752 Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin0(pObj) );
1753 Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin1(pObj) );
1754}
1755void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
1756{
1757 int pCut[SBD_MAX_LUTSIZE+1];
1758 int i, LevelMax = 0;
1759 // label reachable nodes
1760 Gia_Obj_t * pTemp, * pObj = Gia_ManObj(p->pGia, Node);
1761 Sbd_ManFindCut_rec( p->pGia, pObj );
1762 // collect
1763 pCut[0] = 0;
1764 Gia_ManForEachObjVec( vCutLits, p->pGia, pTemp, i )
1765 if ( pTemp->fMark1 )
1766 {
1767 LevelMax = Abc_MaxInt( LevelMax, Vec_IntEntry(p->vLutLevs, Gia_ObjId(p->pGia, pTemp)) );
1768 pCut[1+pCut[0]++] = Gia_ObjId(p->pGia, pTemp);
1769 }
1770 assert( pCut[0] <= p->pPars->nLutSize );
1771 // unlabel reachable nodes
1772 Sbd_ManFindCutUnmark_rec( p->pGia, pObj );
1773 // create cut
1774 assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
1775 Vec_IntWriteEntry( p->vLutLevs, Node, LevelMax+1 );
1776 //Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Node)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Node))) );
1777 memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
1778}
1779
1780int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
1781{
1782 Gia_Obj_t * pObj;
1783 int i, k, w, iLit, Entry, Node;
1784 int iObjLast = Gia_ManObjNum(p->pGia);
1785 int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
1786 int iNewLev;
1787 // collect leaf literals
1788 Vec_IntClear( p->vLits );
1789 Vec_IntForEachEntry( p->vDivSet, Node, i )
1790 {
1791 Node = Vec_IntEntry( p->vWinObjs, Node );
1792 if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
1793 Vec_IntPush( p->vLits, Vec_IntEntry(p->vMirrors, Node) );
1794 else
1795 Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
1796 }
1797 // pretend to have MUXes
1798// assert( p->pGia->pMuxes == NULL );
1799 if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
1800 p->pGia->pMuxes = (unsigned *)p;
1801 // derive new function of the node
1802 iLit = Dsm_ManTruthToGia( p->pGia, &Truth, p->vLits, p->vCover );
1803 if ( p->pGia->pMuxes == (unsigned *)p )
1804 p->pGia->pMuxes = NULL;
1805 // remember this function
1806 assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
1807 Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
1808 if ( p->pPars->fVerbose )
1809 printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
1810 // translate literals into variables
1811 Vec_IntForEachEntry( p->vLits, Entry, i )
1812 Vec_IntWriteEntry( p->vLits, i, Abc_Lit2Var(Entry) );
1813 // label inputs
1814 Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
1815 pObj->fMark0 = 1;
1816 // extend data-structure to accommodate new nodes
1817 assert( Vec_IntSize(p->vLutLevs) == iObjLast );
1818 for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
1819 {
1820 Vec_IntPush( p->vLutLevs, 0 );
1821 Vec_IntPush( p->vObj2Var, 0 );
1822 Vec_IntPush( p->vMirrors, -1 );
1823 Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
1824 Sbd_ManFindCut( p, i, p->vLits );
1825 for ( k = 0; k < 4; k++ )
1826 for ( w = 0; w < p->pPars->nWords; w++ )
1827 Vec_WrdPush( p->vSims[k], 0 );
1828 }
1829 // unlabel inputs
1830 Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
1831 pObj->fMark0 = 0;
1832 // make sure delay reduction is achieved
1833 iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
1834 assert( iNewLev < iCurLev );
1835 // update delay of the initial node
1836 assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
1837 Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
1838 //Vec_IntWriteEntry( p->vLevs, Pivot, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) );
1839 return 0;
1840}
1841
1842int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
1843{
1844 //Gia_Obj_t * pObj = NULL;
1845 int i, k, w, iLit, Node;
1846 int iObjLast = Gia_ManObjNum(p->pGia);
1847 int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
1848 int iNewLev;
1849 // collect leaf literals
1850 Vec_IntClear( p->vLits );
1851 Vec_IntForEachEntry( p->vDivSet, Node, i )
1852 {
1853 Node = Vec_IntEntry( p->vWinObjs, Node );
1854 if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
1855 Vec_IntPush( p->vLits, Vec_IntEntry(p->vMirrors, Node) );
1856 else
1857 Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
1858 }
1859 // collect structure nodes
1860 for ( i = 0; i < nStrs; i++ )
1861 Vec_IntPush( p->vLits, -1 );
1862 // implement structures
1863 for ( i = nStrs-1; i >= 0; i-- )
1864 {
1865 if ( pStrs[i].fLut )
1866 {
1867 // collect local literals
1868 Vec_IntClear( p->vLits2 );
1869 for ( k = 0; k < (int)pStrs[i].nVarIns; k++ )
1870 Vec_IntPush( p->vLits2, Vec_IntEntry(p->vLits, pStrs[i].VarIns[k]) );
1871 // pretend to have MUXes
1872 // assert( p->pGia->pMuxes == NULL );
1873 if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
1874 p->pGia->pMuxes = (unsigned *)p;
1875 // derive new function of the node
1876 iLit = Dsm_ManTruthToGia( p->pGia, &pStrs[i].Res, p->vLits2, p->vCover );
1877 if ( p->pGia->pMuxes == (unsigned *)p )
1878 p->pGia->pMuxes = NULL;
1879 }
1880 else
1881 {
1882 iLit = Vec_IntEntry( p->vLits, (int)pStrs[i].Res );
1883 assert( iLit > 0 );
1884 }
1885 // update literal
1886 assert( Vec_IntEntry(p->vLits, Vec_IntSize(p->vLits)-nStrs+i) == -1 );
1887 Vec_IntWriteEntry( p->vLits, Vec_IntSize(p->vLits)-nStrs+i, iLit );
1888 }
1889 iLit = Vec_IntEntry( p->vLits, Vec_IntSize(p->vDivSet) );
1890 //assert( iObjLast == Gia_ManObjNum(p->pGia) || Abc_Lit2Var(iLit) == Gia_ManObjNum(p->pGia)-1 );
1891 // remember this function
1892 assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
1893 Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
1894 if ( p->pPars->fVeryVerbose )
1895 printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
1896
1897 // extend data-structure to accommodate new nodes
1898 assert( Vec_IntSize(p->vLutLevs) == iObjLast );
1899 for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
1900 {
1901 assert( i == Vec_IntSize(p->vMirrors) );
1902 Vec_IntPush( p->vMirrors, -1 );
1903 Sbd_StoRefObj( p->pSto, i, i == Gia_ManObjNum(p->pGia)-1 ? Pivot : -1 );
1904 }
1905 Sbd_StoDerefObj( p->pSto, Pivot );
1906 for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
1907 {
1908 //Gia_Obj_t * pObjI = Gia_ManObj( p->pGia, i );
1909 abctime clk = Abc_Clock();
1910 int Delay = Sbd_StoComputeCutsNode( p->pSto, i );
1911 p->timeCut += Abc_Clock() - clk;
1912 assert( i == Vec_IntSize(p->vLutLevs) );
1913 Vec_IntPush( p->vLutLevs, Delay );
1914 //Vec_IntPush( p->vLevs, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObjI, i)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObjI, i))) );
1915 Vec_IntPush( p->vObj2Var, 0 );
1916 Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
1917 Sbd_StoSaveBestDelayCut( p->pSto, i, Sbd_ObjCut(p, i) );
1918 //Sbd_ManFindCut( p, i, p->vLits );
1919 for ( k = 0; k < 4; k++ )
1920 for ( w = 0; w < p->pPars->nWords; w++ )
1921 Vec_WrdPush( p->vSims[k], 0 );
1922 }
1923 // make sure delay reduction is achieved
1924 iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
1925 assert( !iNewLev || iNewLev < iCurLev );
1926 // update delay of the initial node
1927 //pObj = Gia_ManObj( p->pGia, Pivot );
1928 assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
1929 Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
1930 //Vec_IntWriteEntry( p->vLevs, Pivot, Pivot ? 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) : 0 );
1931 return 0;
1932}
1933
1945void Sbd_ManDeriveMapping_rec( Sbd_Man_t * p, Gia_Man_t * pNew, int iObj )
1946{
1947 Gia_Obj_t * pObj; int k, * pCut;
1948 if ( !iObj || Gia_ObjIsTravIdCurrentId(pNew, iObj) )
1949 return;
1950 Gia_ObjSetTravIdCurrentId(pNew, iObj);
1951 pObj = Gia_ManObj( pNew, iObj );
1952 if ( Gia_ObjIsCi(pObj) )
1953 return;
1954 assert( Gia_ObjIsAnd(pObj) );
1955 pCut = Sbd_ObjCut2( p, iObj );
1956 for ( k = 1; k <= pCut[0]; k++ )
1957 Sbd_ManDeriveMapping_rec( p, pNew, pCut[k] );
1958 // add mapping
1959 Vec_IntWriteEntry( pNew->vMapping, iObj, Vec_IntSize(pNew->vMapping) );
1960 for ( k = 0; k <= pCut[0]; k++ )
1961 Vec_IntPush( pNew->vMapping, pCut[k] );
1962 Vec_IntPush( pNew->vMapping, iObj );
1963}
1964void Sbd_ManDeriveMapping( Sbd_Man_t * p, Gia_Man_t * pNew )
1965{
1966 Gia_Obj_t * pObj, * pFan;
1967 int i, k, iFan, iObjNew, iFanNew, * pCut, * pCutNew;
1968 Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
1969 // derive cuts for the new manager
1970 p->vLutCuts2 = Vec_IntStart( Gia_ManObjNum(pNew) * (p->pPars->nLutSize + 1) );
1971 Gia_ManForEachAnd( p->pGia, pObj, i )
1972 {
1973 if ( Vec_IntEntry(p->vMirrors, i) >= 0 )
1974 continue;
1975 if ( pObj->Value == ~0 )
1976 continue;
1977 iObjNew = Abc_Lit2Var( pObj->Value );
1978 if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, iObjNew)) )
1979 continue;
1980 pCutNew = Sbd_ObjCut2( p, iObjNew );
1981 pCut = Sbd_ObjCut( p, i );
1982 Vec_IntClear( vLeaves );
1983 for ( k = 1; k <= pCut[0]; k++ )
1984 {
1985 iFan = Vec_IntEntry(p->vMirrors, pCut[k]) >= 0 ? Abc_Lit2Var(Vec_IntEntry(p->vMirrors, pCut[k])) : pCut[k];
1986 pFan = Gia_ManObj( p->pGia, iFan );
1987 if ( pFan->Value == ~0 )
1988 continue;
1989 iFanNew = Abc_Lit2Var( pFan->Value );
1990 if ( iFanNew == 0 || iFanNew == iObjNew )
1991 continue;
1992 Vec_IntPushUniqueOrder( vLeaves, iFanNew );
1993 }
1994 assert( Vec_IntSize(vLeaves) <= p->pPars->nLutSize );
1995 //assert( Vec_IntSize(vLeaves) > 1 );
1996 pCutNew[0] = Vec_IntSize(vLeaves);
1997 memcpy( pCutNew+1, Vec_IntArray(vLeaves), sizeof(int) * Vec_IntSize(vLeaves) );
1998 }
1999 Vec_IntFree( vLeaves );
2000 // create new mapping
2001 Vec_IntFreeP( &pNew->vMapping );
2002 pNew->vMapping = Vec_IntAlloc( (p->pPars->nLutSize + 2) * Gia_ManObjNum(pNew) );
2003 Vec_IntFill( pNew->vMapping, Gia_ManObjNum(pNew), 0 );
2004 Gia_ManIncrementTravId( pNew );
2005 Gia_ManForEachCo( pNew, pObj, i )
2006 Sbd_ManDeriveMapping_rec( p, pNew, Gia_ObjFaninId0p(pNew, pObj) );
2007 Vec_IntFreeP( &p->vLutCuts2 );
2008}
2009void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
2010{
2011 Gia_Obj_t * pObj;
2012 int Obj = Node;
2013 if ( Vec_IntEntry(vMirrors, Node) >= 0 )
2014 Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
2015 pObj = Gia_ManObj( p, Obj );
2016 if ( !~pObj->Value )
2017 {
2018 assert( Gia_ObjIsAnd(pObj) );
2019 Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
2020 Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
2021 if ( Gia_ObjIsXor(pObj) )
2022 pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2023 else
2024 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
2025 }
2026 // set the original node as well
2027 if ( Obj != Node )
2028 Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
2029}
2030Gia_Man_t * Sbd_ManDerive( Sbd_Man_t * pMan, Gia_Man_t * p, Vec_Int_t * vMirrors )
2031{
2032 Gia_Man_t * pNew, * pTemp;
2033 Gia_Obj_t * pObj;
2034 int i;
2035 Gia_ManFillValue( p );
2036 pNew = Gia_ManStart( Gia_ManObjNum(p) );
2037 pNew->pName = Abc_UtilStrsav( p->pName );
2038 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
2039 if ( p->pMuxes )
2040 pNew->pMuxes = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
2041 Gia_ManConst0(p)->Value = 0;
2042 Gia_ManHashAlloc( pNew );
2043 Gia_ManForEachCi( p, pObj, i )
2044 pObj->Value = Gia_ManAppendCi(pNew);
2045 Gia_ManForEachCo( p, pObj, i )
2046 Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0p(p, pObj), vMirrors );
2047 Gia_ManForEachCo( p, pObj, i )
2048 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
2049 Gia_ManHashStop( pNew );
2050 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
2051 Gia_ManTransferTiming( pNew, p );
2052 if ( pMan->pPars->fMapping )
2053 Sbd_ManDeriveMapping( pMan, pNew );
2054 // remove dangling nodes
2055 pNew = Gia_ManCleanup( pTemp = pNew );
2056 Gia_ManTransferTiming( pNew, pTemp );
2057 Gia_ManTransferMapping( pNew, pTemp );
2058 Gia_ManStop( pTemp );
2059 return pNew;
2060}
2061
2073void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
2074{
2075 Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
2076 int RetValue, nStrs = 0;
2077 if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
2078 return;
2079 if ( !Sbd_ManWindow( p, Pivot ) )
2080 return;
2081 //if ( Vec_IntSize(p->vWinObjs) > 100 )
2082 // printf( "Obj %d : Win = %d TFO = %d. Roots = %d.\n", Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vTfo), Vec_IntSize(p->vRoots) );
2083 p->nTried++;
2084 p->nUsed++;
2085 RetValue = Sbd_ManCheckConst( p, Pivot );
2086 if ( RetValue >= 0 )
2087 {
2088 Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
2089 //if ( p->pPars->fVerbose ) printf( "Node %5d: Detected constant %d.\n", Pivot, RetValue );
2090 }
2091 else if ( p->pPars->fFindDivs && p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
2092 {
2093 int i;
2094 Strs->fLut = 1;
2095 Strs->nVarIns = Vec_IntSize( p->vDivSet );
2096 for ( i = 0; i < Strs->nVarIns; i++ )
2097 Strs->VarIns[i] = i;
2098 Strs->Res = Truth;
2099 Sbd_ManImplement2( p, Pivot, 1, Strs );
2100 //if ( p->pPars->fVerbose ) printf( "Node %5d: Detected LUT%d\n", Pivot, p->pPars->nLutSize );
2101 }
2102 else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
2103 {
2104 Sbd_ManImplement2( p, Pivot, nStrs, Strs );
2105 if ( !p->pPars->fVerbose )
2106 return;
2107 //if ( Vec_IntSize(p->vDivSet) <= 4 )
2108 // printf( "Node %5d: Detected %d\n", Pivot, p->pPars->nLutSize );
2109 //else if ( Vec_IntSize(p->vDivSet) <= 6 || (Vec_IntSize(p->vDivSet) == 7 && nStrs == 2) )
2110 // printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
2111 //else
2112 // printf( "Node %5d: Detected %d%d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize, p->pPars->nLutSize );
2113 }
2114 else
2115 p->nUsed--;
2116}
2117Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
2118{
2119 Gia_Man_t * pNew;
2120 Gia_Obj_t * pObj;
2121 Vec_Bit_t * vPath;
2122 Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
2123 int nNodesOld = Gia_ManObjNum(pGia);
2124 int k, Pivot;
2125 assert( pPars->nLutSize <= 6 );
2126 // prepare references
2127 Gia_ManForEachObj( p->pGia, pObj, Pivot )
2128 Sbd_StoRefObj( p->pSto, Pivot, -1 );
2129 //return NULL;
2130 vPath = (pPars->fUsePath && Gia_ManHasMapping(pGia)) ? Sbc_ManCriticalPath(pGia) : NULL;
2131 if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
2132 {
2133 Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
2134 Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
2135 pGia->pManTime = Tim_ManDup( pTimOld, 1 );
2136 //Tim_ManPrint( pGia->pManTime );
2137 Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
2138 Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
2139 {
2140 Pivot = Gia_ObjId( pGia, pObj );
2141 if ( Pivot >= nNodesOld )
2142 break;
2143 if ( Gia_ObjIsAnd(pObj) )
2144 {
2145 abctime clk = Abc_Clock();
2146 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
2147 Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
2148 p->timeCut += Abc_Clock() - clk;
2149 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
2150 if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
2151 Sbd_NtkPerformOne( p, Pivot );
2152 }
2153 else if ( Gia_ObjIsCi(pObj) )
2154 {
2155 int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
2156 Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
2157 Sbd_StoComputeCutsCi( p->pSto, Pivot, arrTime, arrTime );
2158 }
2159 else if ( Gia_ObjIsCo(pObj) )
2160 {
2161 int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
2162 Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
2163 }
2164 else if ( Gia_ObjIsConst0(pObj) )
2165 Sbd_StoComputeCutsConst0( p->pSto, 0 );
2166 else assert( 0 );
2167 }
2168 Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
2169 pGia->pManTime = pTimOld;
2170 Vec_IntFree( vNodes );
2171 }
2172 else
2173 {
2174 Sbd_StoComputeCutsConst0( p->pSto, 0 );
2175 Gia_ManForEachObj( pGia, pObj, Pivot )
2176 {
2177 if ( Pivot >= nNodesOld )
2178 break;
2179 if ( Gia_ObjIsCi(pObj) )
2180 Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
2181 else if ( Gia_ObjIsAnd(pObj) )
2182 {
2183 abctime clk = Abc_Clock();
2184 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
2185 Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
2186 p->timeCut += Abc_Clock() - clk;
2187 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
2188 if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
2189 Sbd_NtkPerformOne( p, Pivot );
2190 }
2191 //if ( nNodesOld != Gia_ManObjNum(pGia) )
2192 // break;
2193 }
2194 }
2195 Vec_BitFreeP( &vPath );
2196 p->timeTotal = Abc_Clock() - p->timeTotal;
2197 if ( p->pPars->fVerbose )
2198 {
2199 printf( "K = %d. S = %d. N = %d. P = %d. ",
2200 p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
2201 printf( "Try = %d. Use = %d. C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d. Lev = %d. ",
2202 p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) );
2203 Abc_PrintTime( 1, "Time", p->timeTotal );
2204 }
2205 pNew = Sbd_ManDerive( p, pGia, p->vMirrors );
2206 // print runtime statistics
2207 p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
2208 if ( p->pPars->fVerbose )
2209 {
2210 ABC_PRTP( "Win", p->timeWin , p->timeTotal );
2211 ABC_PRTP( "Cut", p->timeCut , p->timeTotal );
2212 ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
2213 ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
2214 ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
2215 ABC_PRTP( "Qbf", p->timeQbf , p->timeTotal );
2216 ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
2217 ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
2218 }
2219 Sbd_ManStop( p );
2220 return pNew;
2221}
2222
2226
2227
2228ABC_NAMESPACE_IMPL_END
2229
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
Dsm_ManTruthToGia
int Dsm_ManTruthToGia(void *p, word *pTruth, Vec_Int_t *vLeaves, Vec_Int_t *vCover)
Definition dauGia.c:441
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition giaUtil.c:67
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManForEachCoDriverId
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManTransferTiming
void Gia_ManTransferTiming(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2370
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManHashXorReal
int Gia_ManHashXorReal(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:469
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManOrderWithBoxes
Vec_Int_t * Gia_ManOrderWithBoxes(Gia_Man_t *p)
Definition giaTim.c:286
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
Gia_ManTransferMapping
void Gia_ManTransferMapping(Gia_Man_t *p, Gia_Man_t *pGia)
Definition giaIf.c:2305
Gia_ManForEachAndId
#define Gia_ManForEachAndId(p, i)
Definition gia.h:1216
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition giaUtil.c:49
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Sbd_ManWindow
int Sbd_ManWindow(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:444
Sbd_ManFindCut_rec
void Sbd_ManFindCut_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition sbdCore.c:1733
Sbd_ManPrintObj
void Sbd_ManPrintObj(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:659
Sbd_ManPropagateControl
void Sbd_ManPropagateControl(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:322
Sbd_ManStart
Sbd_Man_t * Sbd_ManStart(Gia_Man_t *pGia, Sbd_Par_t *pPars)
Definition sbdCore.c:200
Sbd_ManDeriveMapping
void Sbd_ManDeriveMapping(Sbd_Man_t *p, Gia_Man_t *pNew)
Definition sbdCore.c:1964
Sbd_ManCheckConst
int Sbd_ManCheckConst(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:519
Sbd_ManExplore2
int Sbd_ManExplore2(Sbd_Man_t *p, int Pivot, word *pTruth)
Definition sbdCore.c:1170
Sbd_ManFindCutUnmark_rec
void Sbd_ManFindCutUnmark_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition sbdCore.c:1744
SBD_MAX_LUTSIZE
#define SBD_MAX_LUTSIZE
DECLARATIONS ///.
Definition sbdCore.c:31
Sbd_ManDeriveMapping_rec
void Sbd_ManDeriveMapping_rec(Sbd_Man_t *p, Gia_Man_t *pNew, int iObj)
Definition sbdCore.c:1945
Sbd_CutMergeSimple
int Sbd_CutMergeSimple(Sbd_Man_t *p, int *pCut1, int *pCut2, int *pCut)
Definition sbdCore.c:1610
Sbd_ManFindCut
void Sbd_ManFindCut(Sbd_Man_t *p, int Node, Vec_Int_t *vCutLits)
Definition sbdCore.c:1755
Sbd_ManExplore
int Sbd_ManExplore(Sbd_Man_t *p, int Pivot, word *pTruth)
Definition sbdCore.c:1009
Sbd_ManDelay
int Sbd_ManDelay(Sbd_Man_t *p)
Definition sbdCore.c:1718
Sbd_ManExplore3
int Sbd_ManExplore3(Sbd_Man_t *p, int Pivot, int *pnStrs, Sbd_Str_t *Strs)
Definition sbdCore.c:1564
Sbd_ManDerive_rec
void Sbd_ManDerive_rec(Gia_Man_t *pNew, Gia_Man_t *p, int Node, Vec_Int_t *vMirrors)
Definition sbdCore.c:2009
Sbd_ManMergeTest
void Sbd_ManMergeTest(Sbd_Man_t *p)
Definition sbdCore.c:1725
Sbd_NtkPerformOne
void Sbd_NtkPerformOne(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:2073
Sbd_ManMergeCuts
int Sbd_ManMergeCuts(Sbd_Man_t *p, int Node)
Definition sbdCore.c:1670
Sbd_ManStop
void Sbd_ManStop(Sbd_Man_t *p)
Definition sbdCore.c:249
Sbd_ManImplement
int Sbd_ManImplement(Sbd_Man_t *p, int Pivot, word Truth)
Definition sbdCore.c:1780
Sbd_ParSetDefault
void Sbd_ParSetDefault(Sbd_Par_t *pPars)
FUNCTION DEFINITIONS ///.
Definition sbdCore.c:100
Sbd_ManUpdateOrder
void Sbd_ManUpdateOrder(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:340
Sbd_ManExploreCut
int Sbd_ManExploreCut(Sbd_Man_t *p, int Pivot, int nLeaves, int *pLeaves, int *pnStrs, Sbd_Str_t *Strs, int *pFreeVar)
Definition sbdCore.c:1287
Sbd_ManWindowSim_rec
void Sbd_ManWindowSim_rec(Sbd_Man_t *p, int NodeInit)
Definition sbdCore.c:389
Sbd_ManWindowRoots
Vec_Wec_t * Sbd_ManWindowRoots(Gia_Man_t *p, int nTfoLevels, int nTfoFanMax)
Definition sbdCore.c:135
Sbd_Man_t
struct Sbd_Man_t_ Sbd_Man_t
Definition sbdCore.c:33
Sbd_ManMatrPrint
void Sbd_ManMatrPrint(Sbd_Man_t *p, word Cover[], int nCol, int nRows)
Definition sbdCore.c:816
Sbd_ManImplement2
int Sbd_ManImplement2(Sbd_Man_t *p, int Pivot, int nStrs, Sbd_Str_t *pStrs)
Definition sbdCore.c:1842
Sbd_ManPropagateControlOne
void Sbd_ManPropagateControlOne(Sbd_Man_t *p, int Node)
Definition sbdCore.c:289
Sbd_ManDerive
Gia_Man_t * Sbd_ManDerive(Sbd_Man_t *pMan, Gia_Man_t *p, Vec_Int_t *vMirrors)
Definition sbdCore.c:2030
Sbd_NtkPerform
Gia_Man_t * Sbd_NtkPerform(Gia_Man_t *pGia, Sbd_Par_t *pPars)
Definition sbdCore.c:2117
Sbd_ManCutServerStop
void Sbd_ManCutServerStop(Sbd_Srv_t *p)
Definition sbdCut2.c:110
Sbd_ManCutServerFirst
int Sbd_ManCutServerFirst(Sbd_Srv_t *p, int iObj, int *pLeaves)
Definition sbdCut2.c:308
Sbd_ManCutServerStart
Sbd_Srv_t * Sbd_ManCutServerStart(Gia_Man_t *pGia, Vec_Int_t *vMirrors, Vec_Int_t *vLutLevs, Vec_Int_t *vLevs, Vec_Int_t *vRefs, int nLutSize, int nCutSize, int nCutNum, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition sbdCut2.c:84
Sbd_StoAlloc
Sbd_Sto_t * Sbd_StoAlloc(Gia_Man_t *pGia, Vec_Int_t *vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose)
MACRO DEFINITIONS ///.
Definition sbdCut.c:667
Sbd_StoFree
void Sbd_StoFree(Sbd_Sto_t *p)
Definition sbdCut.c:690
Sbd_StoComputeCutsNode
int Sbd_StoComputeCutsNode(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:729
Sbd_StoSaveBestDelayCut
void Sbd_StoSaveBestDelayCut(Sbd_Sto_t *p, int iObj, int *pCut)
Definition sbdCut.c:738
Sbd_StoComputeCutsConst0
void Sbd_StoComputeCutsConst0(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:719
Sbd_StoRefObj
void Sbd_StoRefObj(Sbd_Sto_t *p, int iObj, int iMirror)
Definition sbdCut.c:750
Sbd_StoDerefObj
void Sbd_StoDerefObj(Sbd_Sto_t *p, int iObj)
Definition sbdCut.c:778
Sbd_StoObjBestCut
int Sbd_StoObjBestCut(Sbd_Sto_t *p, int iObj, int nSize, int *pLeaves)
Definition sbdCut.c:802
Sbd_StoComputeCutsCi
void Sbd_StoComputeCutsCi(Sbd_Sto_t *p, int iObj, int Delay, int Level)
Definition sbdCut.c:724
SBD_FVAR_MAX
#define SBD_FVAR_MAX
Definition sbdInt.h:58
SBD_SAT_SAT
#define SBD_SAT_SAT
Definition sbdInt.h:53
Sbd_Sto_t
struct Sbd_Sto_t_ Sbd_Sto_t
BASIC TYPES ///.
Definition sbdInt.h:64
Sbd_Srv_t
struct Sbd_Srv_t_ Sbd_Srv_t
Definition sbdInt.h:65
Sbd_ManSolve
word Sbd_ManSolve(sat_solver *pSat, int PivotVar, int FreeVar, Vec_Int_t *vDivSet, Vec_Int_t *vDivVars, Vec_Int_t *vDivValues, Vec_Int_t *vTemp)
Definition sbdWin.c:178
Sbd_ManSatSolver
sat_solver * Sbd_ManSatSolver(sat_solver *pSat, Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots, int fQbf)
DECLARATIONS ///.
Definition sbdWin.c:52
SBD_DIV_MAX
#define SBD_DIV_MAX
Definition sbdInt.h:57
SBD_SAT_UNDEC
#define SBD_SAT_UNDEC
INCLUDES ///.
Definition sbdInt.h:52
Sbd_ManCollectConstants
int Sbd_ManCollectConstants(sat_solver *pSat, int nCareMints[2], int PivotVar, word *pVarSims[], Vec_Int_t *vInds)
Definition sbdWin.c:411
Sbd_ManCollectConstantsNew
int Sbd_ManCollectConstantsNew(sat_solver *pSat, Vec_Int_t *vDivVars, int nConsts, int PivotVar, word *pOnset, word *pOffset)
Definition sbdWin.c:433
Sbd_ProblemSolve
int Sbd_ProblemSolve(Gia_Man_t *p, Vec_Int_t *vMirrors, int Pivot, Vec_Int_t *vWinObjs, Vec_Int_t *vObj2Var, Vec_Int_t *vTfo, Vec_Int_t *vRoots, Vec_Int_t *vDivSet, int nStrs, Sbd_Str_t *pStr0)
Definition sbdLut.c:187
Sbc_ManCriticalPath
Vec_Bit_t * Sbc_ManCriticalPath(Gia_Man_t *p)
Definition sbdPath.c:119
Sbd_Str_t
struct Sbd_Str_t_ Sbd_Str_t
Definition sbdInt.h:67
Sbd_Par_t
typedefABC_NAMESPACE_HEADER_START struct Sbd_Par_t_ Sbd_Par_t
INCLUDES ///.
Definition sbd.h:38
Gia_Man_t_::pMuxes
unsigned * pMuxes
Definition gia.h:106
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::vMapping
Vec_Int_t * vMapping
Definition gia.h:136
Gia_Man_t_::pManTime
void * pManTime
Definition gia.h:194
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Sbd_Man_t_
Definition sbdCore.c:35
Sbd_Man_t_::vCounts
Vec_Int_t * vCounts[2]
Definition sbdCore.c:72
Sbd_Man_t_::vCover
Vec_Int_t * vCover
Definition sbdCore.c:44
Sbd_Man_t_::pGia
Gia_Man_t * pGia
Definition sbdCore.c:37
Sbd_Man_t_::timeQbf
abctime timeQbf
Definition sbdCore.c:55
Sbd_Man_t_::pPars
Sbd_Par_t * pPars
Definition sbdCore.c:36
Sbd_Man_t_::vDivValues
Vec_Int_t * vDivValues
Definition sbdCore.c:70
Sbd_Man_t_::timeNew
abctime timeNew
Definition sbdCore.c:56
Sbd_Man_t_::timeTotal
abctime timeTotal
Definition sbdCore.c:58
Sbd_Man_t_::vLutCuts
Vec_Int_t * vLutCuts
Definition sbdCore.c:40
Sbd_Man_t_::vTfo
Vec_Int_t * vTfo
Definition sbdCore.c:64
Sbd_Man_t_::vRoots
Vec_Int_t * vRoots
Definition sbdCore.c:65
Sbd_Man_t_::vObj2Var
Vec_Int_t * vObj2Var
Definition sbdCore.c:67
Sbd_Man_t_::vLits2
Vec_Int_t * vLits2
Definition sbdCore.c:46
Sbd_Man_t_::vLutLevs
Vec_Int_t * vLutLevs
Definition sbdCore.c:39
Sbd_Man_t_::vDivVars
Vec_Int_t * vDivVars
Definition sbdCore.c:69
Sbd_Man_t_::pSto
Sbd_Sto_t * pSto
Definition sbdCore.c:59
Sbd_Man_t_::timeCov
abctime timeCov
Definition sbdCore.c:52
Sbd_Man_t_::vTfos
Vec_Wec_t * vTfos
Definition sbdCore.c:38
Sbd_Man_t_::vDivSet
Vec_Int_t * vDivSet
Definition sbdCore.c:68
Sbd_Man_t_::vWinObjs
Vec_Int_t * vWinObjs
Definition sbdCore.c:66
Sbd_Man_t_::vDivLevels
Vec_Wec_t * vDivLevels
Definition sbdCore.c:71
Sbd_Man_t_::pSrv
Sbd_Srv_t * pSrv
Definition sbdCore.c:60
Sbd_Man_t_::nTried
int nTried
Definition sbdCore.c:48
Sbd_Man_t_::Pivot
int Pivot
Definition sbdCore.c:62
Sbd_Man_t_::vMirrors
Vec_Int_t * vMirrors
Definition sbdCore.c:42
Sbd_Man_t_::vMatrix
Vec_Wrd_t * vMatrix
Definition sbdCore.c:73
Sbd_Man_t_::timeOther
abctime timeOther
Definition sbdCore.c:57
Sbd_Man_t_::nUsed
int nUsed
Definition sbdCore.c:49
Sbd_Man_t_::timeCut
abctime timeCut
Definition sbdCore.c:51
Sbd_Man_t_::timeWin
abctime timeWin
Definition sbdCore.c:50
Sbd_Man_t_::timeSat
abctime timeSat
Definition sbdCore.c:54
Sbd_Man_t_::timeCnf
abctime timeCnf
Definition sbdCore.c:53
Sbd_Man_t_::nLuts
int nLuts[6]
Definition sbdCore.c:47
Sbd_Man_t_::vLutCuts2
Vec_Int_t * vLutCuts2
Definition sbdCore.c:41
Sbd_Man_t_::DivCutoff
int DivCutoff
Definition sbdCore.c:63
Sbd_Man_t_::vLits
Vec_Int_t * vLits
Definition sbdCore.c:45
Sbd_Man_t_::vSims
Vec_Wrd_t * vSims[4]
Definition sbdCore.c:43
Sbd_Man_t_::pSat
sat_solver * pSat
Definition sbdCore.c:74
Sbd_Str_t_::Res
word Res
Definition sbdInt.h:73
Sbd_Str_t_::nVarIns
int nVarIns
Definition sbdInt.h:71
Sbd_Str_t_::fLut
int fLut
Definition sbdInt.h:70
Sbd_Str_t_::VarIns
int VarIns[SBD_DIV_MAX]
Definition sbdInt.h:72
Tim_ManSetCoArrival
void Tim_ManSetCoArrival(Tim_Man_t *p, int iCo, float Delay)
Definition timTime.c:116
Tim_ManBoxNum
int Tim_ManBoxNum(Tim_Man_t *p)
Definition timMan.c:722
Tim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition tim.h:92
Tim_ManIncrementTravId
void Tim_ManIncrementTravId(Tim_Man_t *p)
DECLARATIONS ///.
Definition timTrav.c:44
Tim_ManStop
void Tim_ManStop(Tim_Man_t *p)
Definition timMan.c:378
Tim_ManDup
Tim_Man_t * Tim_ManDup(Tim_Man_t *p, int fUnitDelay)
Definition timMan.c:86
Tim_ManGetCiArrival
float Tim_ManGetCiArrival(Tim_Man_t *p, int iCi)
Definition timTime.c:174
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
memset
char * memset()
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
Vec_IntForEachEntryStartStop
#define Vec_IntForEachEntryStartStop(vVec, Entry, i, Start, Stop)
Definition vecInt.h:60
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42