ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
kitSop.c File Reference
#include "kit.h"
Include dependency graph for kitSop.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Kit_SopCreate (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
 DECLARATIONS ///.
 
void Kit_SopCreateInverse (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nLits, Vec_Int_t *vMemory)
 
void Kit_SopDup (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
 
void Kit_SopDivideByLiteralQuo (Kit_Sop_t *cSop, int iLit)
 
void Kit_SopDivideByCube (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
 
void Kit_SopDivideInternal (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
 
void Kit_SopMakeCubeFree (Kit_Sop_t *cSop)
 
int Kit_SopIsCubeFree (Kit_Sop_t *cSop)
 
void Kit_SopCommonCubeCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
 
int Kit_SopAnyLiteral (Kit_Sop_t *cSop, int nLits)
 
int Kit_SopWorstLiteral (Kit_Sop_t *cSop, int nLits)
 
int Kit_SopBestLiteral (Kit_Sop_t *cSop, int nLits, unsigned uMask)
 
void Kit_SopDivisorZeroKernel_rec (Kit_Sop_t *cSop, int nLits)
 
int Kit_SopDivisor (Kit_Sop_t *cResult, Kit_Sop_t *cSop, int nLits, Vec_Int_t *vMemory)
 
void Kit_SopBestLiteralCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, unsigned uCube, int nLits, Vec_Int_t *vMemory)
 

Function Documentation

◆ Kit_SopAnyLiteral()

int Kit_SopAnyLiteral ( Kit_Sop_t * cSop,
int nLits )

Function*************************************************************

Synopsis [Find any literal that occurs more than once.]

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file kitSop.c.

371{
372 unsigned uCube;
373 int i, k, nLitsCur;
374 // go through each literal
375 for ( i = 0; i < nLits; i++ )
376 {
377 // go through all the cubes
378 nLitsCur = 0;
379 Kit_SopForEachCube( cSop, uCube, k )
380 if ( Kit_CubeHasLit(uCube, i) )
381 nLitsCur++;
382 if ( nLitsCur > 1 )
383 return i;
384 }
385 return -1;
386}
Kit_SopForEachCube
#define Kit_SopForEachCube(cSop, uCube, i)
ITERATORS ///.
Definition kit.h:500
Here is the caller graph for this function:

◆ Kit_SopBestLiteral()

int Kit_SopBestLiteral ( Kit_Sop_t * cSop,
int nLits,
unsigned uMask )

Function*************************************************************

Synopsis [Find the least often occurring literal.]

Description [Find the least often occurring literal among those that occur more than once.]

SideEffects []

SeeAlso []

Definition at line 454 of file kitSop.c.

455{
456 unsigned uCube;
457 int i, k, iMax, nLitsMax, nLitsCur;
458 int fUseFirst = 1;
459
460 // go through each literal
461 iMax = -1;
462 nLitsMax = -1;
463 for ( i = 0; i < nLits; i++ )
464 {
465 if ( !Kit_CubeHasLit(uMask, i) )
466 continue;
467 // go through all the cubes
468 nLitsCur = 0;
469 Kit_SopForEachCube( cSop, uCube, k )
470 if ( Kit_CubeHasLit(uCube, i) )
471 nLitsCur++;
472 // skip the literal that does not occur or occurs once
473 if ( nLitsCur < 2 )
474 continue;
475 // check if this is the best literal
476 if ( fUseFirst )
477 {
478 if ( nLitsMax < nLitsCur )
479 {
480 nLitsMax = nLitsCur;
481 iMax = i;
482 }
483 }
484 else
485 {
486 if ( nLitsMax <= nLitsCur )
487 {
488 nLitsMax = nLitsCur;
489 iMax = i;
490 }
491 }
492 }
493 if ( nLitsMax >= 0 )
494 return iMax;
495 return -1;
496}
Here is the caller graph for this function:

◆ Kit_SopBestLiteralCover()

void Kit_SopBestLiteralCover ( Kit_Sop_t * cResult,
Kit_Sop_t * cSop,
unsigned uCube,
int nLits,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Create the one-literal cover with the best literal from cSop.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file kitSop.c.

561{
562 int iLitBest;
563 // get the best literal
564 iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
565 // start the cover
566 cResult->nCubes = 0;
567 cResult->pCubes = Vec_IntFetch( vMemory, 1 );
568 // set the cube
569 Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
570}
Kit_SopBestLiteral
int Kit_SopBestLiteral(Kit_Sop_t *cSop, int nLits, unsigned uMask)
Definition kitSop.c:454
Here is the call graph for this function:

◆ Kit_SopCommonCubeCover()

void Kit_SopCommonCubeCover ( Kit_Sop_t * cResult,
Kit_Sop_t * cSop,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Creates SOP composes of the common cube of the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file kitSop.c.

351{
352 assert( Kit_SopCubeNum(cSop) > 0 );
353 cResult->nCubes = 0;
354 cResult->pCubes = Vec_IntFetch( vMemory, 1 );
355 Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
356}
assert
#define assert(ex)
Definition util_old.h:213

◆ Kit_SopCreate()

ABC_NAMESPACE_IMPL_START void Kit_SopCreate ( Kit_Sop_t * cResult,
Vec_Int_t * vInput,
int nVars,
Vec_Int_t * vMemory )

DECLARATIONS ///.

CFile****************************************************************

FileName [kitSop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving SOPs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id
kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitSop.c.

46{
47 unsigned uCube;
48 int i;
49 // start the cover
50 cResult->nCubes = 0;
51 cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
52 // add the cubes
53 Vec_IntForEachEntry( vInput, uCube, i )
54 Kit_SopPushCube( cResult, uCube );
55}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54

◆ Kit_SopCreateInverse()

void Kit_SopCreateInverse ( Kit_Sop_t * cResult,
Vec_Int_t * vInput,
int nLits,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file kitSop.c.

69{
70 unsigned uCube, uMask = 0;
71 int i, nCubes = Vec_IntSize(vInput);
72 // start the cover
73 cResult->nCubes = 0;
74 cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
75 // add the cubes
76// Vec_IntForEachEntry( vInput, uCube, i )
77 for ( i = 0; i < nCubes; i++ )
78 {
79 uCube = Vec_IntEntry( vInput, i );
80 uMask = ((uCube | (uCube >> 1)) & 0x55555555);
81 uMask |= (uMask << 1);
82 Kit_SopPushCube( cResult, uCube ^ uMask );
83 }
84}
Here is the caller graph for this function:

◆ Kit_SopDivideByCube()

void Kit_SopDivideByCube ( Kit_Sop_t * cSop,
Kit_Sop_t * cDiv,
Kit_Sop_t * vQuo,
Kit_Sop_t * vRem,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file kitSop.c.

146{
147 unsigned uCube, uDiv;
148 int i;
149 // get the only cube
150 assert( Kit_SopCubeNum(cDiv) == 1 );
151 uDiv = Kit_SopCube(cDiv, 0);
152 // allocate covers
153 vQuo->nCubes = 0;
154 vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
155 vRem->nCubes = 0;
156 vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
157 // sort the cubes
158 Kit_SopForEachCube( cSop, uCube, i )
159 {
160 if ( Kit_CubeContains( uCube, uDiv ) )
161 Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
162 else
163 Kit_SopPushCube( vRem, uCube );
164 }
165}
Here is the caller graph for this function:

◆ Kit_SopDivideByLiteralQuo()

void Kit_SopDivideByLiteralQuo ( Kit_Sop_t * cSop,
int iLit )

Function*************************************************************

Synopsis [Derives the quotient of division by literal.]

Description [Reduces the cover to be equal to the result of division of the given cover by the literal.]

SideEffects []

SeeAlso []

Definition at line 121 of file kitSop.c.

122{
123 unsigned uCube;
124 int i, k = 0;
125 Kit_SopForEachCube( cSop, uCube, i )
126 {
127 if ( Kit_CubeHasLit(uCube, iLit) )
128 Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
129 }
130 Kit_SopShrink( cSop, k );
131}
Here is the caller graph for this function:

◆ Kit_SopDivideInternal()

void Kit_SopDivideInternal ( Kit_Sop_t * cSop,
Kit_Sop_t * cDiv,
Kit_Sop_t * vQuo,
Kit_Sop_t * vRem,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file kitSop.c.

179{
180 unsigned uCube, uDiv;
181 unsigned uCube2 = 0; // Suppress "might be used uninitialized"
182 unsigned uDiv2, uQuo;
183 int i, i2, k, k2, nCubesRem;
184 assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
185 // consider special case
186 if ( Kit_SopCubeNum(cDiv) == 1 )
187 {
188 Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
189 return;
190 }
191 // allocate quotient
192 vQuo->nCubes = 0;
193 vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
194 // for each cube of the cover
195 // it either belongs to the quotient or to the remainder
196 Kit_SopForEachCube( cSop, uCube, i )
197 {
198 // skip taken cubes
199 if ( Kit_CubeIsMarked(uCube) )
200 continue;
201 // find a matching cube in the divisor
202 uDiv = ~0;
203 Kit_SopForEachCube( cDiv, uDiv, k )
204 if ( Kit_CubeContains( uCube, uDiv ) )
205 break;
206 // the cube is not found
207 if ( k == Kit_SopCubeNum(cDiv) )
208 continue;
209 // the quotient cube exists
210 uQuo = Kit_CubeSharp( uCube, uDiv );
211 // find corresponding cubes for other cubes of the divisor
212 uDiv2 = ~0;
213 Kit_SopForEachCube( cDiv, uDiv2, k2 )
214 {
215 if ( k2 == k )
216 continue;
217 // find a matching cube
218 Kit_SopForEachCube( cSop, uCube2, i2 )
219 {
220 // skip taken cubes
221 if ( Kit_CubeIsMarked(uCube2) )
222 continue;
223 // check if the cube can be used
224 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
225 break;
226 }
227 // the case when the cube is not found
228 if ( i2 == Kit_SopCubeNum(cSop) )
229 break;
230 }
231 // we did not find some cubes - continue looking at other cubes
232 if ( k2 != Kit_SopCubeNum(cDiv) )
233 continue;
234 // we found all cubes - add the quotient cube
235 Kit_SopPushCube( vQuo, uQuo );
236
237 // mark the first cube
238 Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
239 // mark other cubes that have this quotient
240 Kit_SopForEachCube( cDiv, uDiv2, k2 )
241 {
242 if ( k2 == k )
243 continue;
244 // find a matching cube
245 Kit_SopForEachCube( cSop, uCube2, i2 )
246 {
247 // skip taken cubes
248 if ( Kit_CubeIsMarked(uCube2) )
249 continue;
250 // check if the cube can be used
251 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
252 break;
253 }
254 assert( i2 < Kit_SopCubeNum(cSop) );
255 // the cube is found, mark it
256 // (later we will add all unmarked cubes to the remainder)
257 Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
258 }
259 }
260 // determine the number of cubes in the remainder
261 nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
262 // allocate remainder
263 vRem->nCubes = 0;
264 vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
265 // finally add the remaining unmarked cubes to the remainder
266 // and clean the marked cubes in the cover
267 Kit_SopForEachCube( cSop, uCube, i )
268 {
269 if ( !Kit_CubeIsMarked(uCube) )
270 {
271 Kit_SopPushCube( vRem, uCube );
272 continue;
273 }
274 Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
275 }
276 assert( nCubesRem == Kit_SopCubeNum(vRem) );
277}
Kit_SopDivideByCube
void Kit_SopDivideByCube(Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
Definition kitSop.c:145
Here is the call graph for this function:

◆ Kit_SopDivisor()

int Kit_SopDivisor ( Kit_Sop_t * cResult,
Kit_Sop_t * cSop,
int nLits,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Computes the quick divisor of the cover.]

Description [Returns 0, if there is no divisor other than trivial.]

SideEffects []

SeeAlso []

Definition at line 534 of file kitSop.c.

535{
536 if ( Kit_SopCubeNum(cSop) <= 1 )
537 return 0;
538 if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
539 return 0;
540 // duplicate the cover
541 Kit_SopDup( cResult, cSop, vMemory );
542 // perform the kerneling
543 Kit_SopDivisorZeroKernel_rec( cResult, nLits );
544 assert( Kit_SopCubeNum(cResult) > 0 );
545 return 1;
546}
Kit_SopAnyLiteral
int Kit_SopAnyLiteral(Kit_Sop_t *cSop, int nLits)
Definition kitSop.c:370
Kit_SopDup
void Kit_SopDup(Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
Definition kitSop.c:97
Kit_SopDivisorZeroKernel_rec
void Kit_SopDivisorZeroKernel_rec(Kit_Sop_t *cSop, int nLits)
Definition kitSop.c:509
Here is the call graph for this function:

◆ Kit_SopDivisorZeroKernel_rec()

void Kit_SopDivisorZeroKernel_rec ( Kit_Sop_t * cSop,
int nLits )

Function*************************************************************

Synopsis [Computes a level-zero kernel.]

Description [Modifies the cover to contain one level-zero kernel.]

SideEffects []

SeeAlso []

Definition at line 509 of file kitSop.c.

510{
511 int iLit;
512 // find any literal that occurs at least two times
513 iLit = Kit_SopWorstLiteral( cSop, nLits );
514 if ( iLit == -1 )
515 return;
516 // derive the cube-free quotient
517 Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
518 Kit_SopMakeCubeFree( cSop ); // the same cover
519 // call recursively
520 Kit_SopDivisorZeroKernel_rec( cSop, nLits ); // the same cover
521}
Kit_SopDivideByLiteralQuo
void Kit_SopDivideByLiteralQuo(Kit_Sop_t *cSop, int iLit)
Definition kitSop.c:121
Kit_SopMakeCubeFree
void Kit_SopMakeCubeFree(Kit_Sop_t *cSop)
Definition kitSop.c:311
Kit_SopWorstLiteral
int Kit_SopWorstLiteral(Kit_Sop_t *cSop, int nLits)
Definition kitSop.c:400
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_SopDup()

void Kit_SopDup ( Kit_Sop_t * cResult,
Kit_Sop_t * cSop,
Vec_Int_t * vMemory )

Function*************************************************************

Synopsis [Duplicates SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file kitSop.c.

98{
99 unsigned uCube;
100 int i;
101 // start the cover
102 cResult->nCubes = 0;
103 cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
104 // add the cubes
105 Kit_SopForEachCube( cSop, uCube, i )
106 Kit_SopPushCube( cResult, uCube );
107}
Here is the caller graph for this function:

◆ Kit_SopIsCubeFree()

int Kit_SopIsCubeFree ( Kit_Sop_t * cSop)

Function*************************************************************

Synopsis [Checks if the cover is cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 334 of file kitSop.c.

335{
336 return Kit_SopCommonCube( cSop ) == 0;
337}

◆ Kit_SopMakeCubeFree()

void Kit_SopMakeCubeFree ( Kit_Sop_t * cSop)

Function*************************************************************

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file kitSop.c.

312{
313 unsigned uMask, uCube;
314 int i;
315 uMask = Kit_SopCommonCube( cSop );
316 if ( uMask == 0 )
317 return;
318 // remove the common cube
319 Kit_SopForEachCube( cSop, uCube, i )
320 Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
321}
Here is the caller graph for this function:

◆ Kit_SopWorstLiteral()

int Kit_SopWorstLiteral ( Kit_Sop_t * cSop,
int nLits )

Function*************************************************************

Synopsis [Find the least often occurring literal.]

Description [Find the least often occurring literal among those that occur more than once.]

SideEffects []

SeeAlso []

Definition at line 400 of file kitSop.c.

401{
402 unsigned uCube;
403 int i, k, iMin, nLitsMin, nLitsCur;
404 int fUseFirst = 1;
405
406 // go through each literal
407 iMin = -1;
408 nLitsMin = 1000000;
409 for ( i = 0; i < nLits; i++ )
410 {
411 // go through all the cubes
412 nLitsCur = 0;
413 Kit_SopForEachCube( cSop, uCube, k )
414 if ( Kit_CubeHasLit(uCube, i) )
415 nLitsCur++;
416 // skip the literal that does not occur or occurs once
417 if ( nLitsCur < 2 )
418 continue;
419 // check if this is the best literal
420 if ( fUseFirst )
421 {
422 if ( nLitsMin > nLitsCur )
423 {
424 nLitsMin = nLitsCur;
425 iMin = i;
426 }
427 }
428 else
429 {
430 if ( nLitsMin >= nLitsCur )
431 {
432 nLitsMin = nLitsCur;
433 iMin = i;
434 }
435 }
436 }
437 if ( nLitsMin < 1000000 )
438 return iMin;
439 return -1;
440}
Here is the caller graph for this function: