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

Go to the source code of this file.

Classes

struct  Ssw_Cla_t_
 

Macros

#define Ssw_ManForEachClass(p, ppClass, i)
 
#define Ssw_ClassForEachNode(p, pRepr, pNode, i)
 

Functions

Ssw_Cla_tSsw_ClassesStart (Aig_Man_t *pAig)
 
void Ssw_ClassesSetData (Ssw_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
 
void Ssw_ClassesStop (Ssw_Cla_t *p)
 
Aig_Man_tSsw_ClassesReadAig (Ssw_Cla_t *p)
 
Vec_Ptr_tSsw_ClassesGetRefined (Ssw_Cla_t *p)
 
void Ssw_ClassesClearRefined (Ssw_Cla_t *p)
 
int Ssw_ClassesCand1Num (Ssw_Cla_t *p)
 
int Ssw_ClassesClassNum (Ssw_Cla_t *p)
 
int Ssw_ClassesLitNum (Ssw_Cla_t *p)
 
Aig_Obj_t ** Ssw_ClassesReadClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
 
void Ssw_ClassesCollectClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vClass)
 
void Ssw_ClassesCheck (Ssw_Cla_t *p)
 
void Ssw_ClassesPrintOne (Ssw_Cla_t *p, Aig_Obj_t *pRepr)
 
void Ssw_ClassesPrint (Ssw_Cla_t *p, int fVeryVerbose)
 
void Ssw_ClassesRemoveNode (Ssw_Cla_t *p, Aig_Obj_t *pObj)
 
int Ssw_ClassesPrepareRehash (Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
 
Ssw_Cla_tSsw_ClassesPrepare (Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
 
Ssw_Cla_tSsw_ClassesPrepareSimple (Aig_Man_t *pAig, int fLatchCorr, int nMaxLevs)
 
Ssw_Cla_tSsw_ClassesPrepareFromReprs (Aig_Man_t *pAig)
 
Ssw_Cla_tSsw_ClassesPrepareTargets (Aig_Man_t *pAig)
 
Ssw_Cla_tSsw_ClassesPreparePairs (Aig_Man_t *pAig, Vec_Int_t **pvClasses)
 
Ssw_Cla_tSsw_ClassesPreparePairsSimple (Aig_Man_t *pMiter, Vec_Int_t *vPairs)
 
int Ssw_ClassesRefineOneClass (Ssw_Cla_t *p, Aig_Obj_t *pReprOld, int fRecursive)
 
int Ssw_ClassesRefine (Ssw_Cla_t *p, int fRecursive)
 
int Ssw_ClassesRefineGroup (Ssw_Cla_t *p, Vec_Ptr_t *vReprs, int fRecursive)
 
int Ssw_ClassesRefineConst1Group (Ssw_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
 
int Ssw_ClassesRefineConst1 (Ssw_Cla_t *p, int fRecursive)
 

Macro Definition Documentation

◆ Ssw_ClassForEachNode

#define Ssw_ClassForEachNode ( p,
pRepr,
pNode,
i )
Value:
for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
Cube * p
Definition exorList.c:222

Definition at line 73 of file sswClass.c.

73#define Ssw_ClassForEachNode( p, pRepr, pNode, i ) \
74 for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ ) \
75 if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else

◆ Ssw_ManForEachClass

#define Ssw_ManForEachClass ( p,
ppClass,
i )
Value:
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else

Definition at line 69 of file sswClass.c.

69#define Ssw_ManForEachClass( p, ppClass, i ) \
70 for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ ) \
71 if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else

Function Documentation

◆ Ssw_ClassesCand1Num()

int Ssw_ClassesCand1Num ( Ssw_Cla_t * p)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file sswClass.c.

260{
261 return p->nCands1;
262}
Here is the caller graph for this function:

◆ Ssw_ClassesCheck()

void Ssw_ClassesCheck ( Ssw_Cla_t * p)

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

Synopsis [Checks candidate equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file sswClass.c.

351{
352 Aig_Obj_t * pObj, * pPrev, ** ppClass;
353 int i, k, nLits, nClasses, nCands1;
354 nClasses = nLits = 0;
355 Ssw_ManForEachClass( p, ppClass, k )
356 {
357 pPrev = NULL;
358 assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
359 Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
360 {
361 if ( i == 0 )
362 assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
363 else
364 {
365 assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
366 assert( pPrev->Id < pObj->Id );
367 nLits++;
368 }
369 pPrev = pObj;
370 }
371 nClasses++;
372 }
373 nCands1 = 0;
374 Aig_ManForEachObj( p->pAig, pObj, i )
375 nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
376 assert( p->nLits == nLits );
377 assert( p->nCands1 == nCands1 );
378 assert( p->nClasses == nClasses );
379}
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
#define Ssw_ManForEachClass(p, ppClass, i)
Definition sswClass.c:69
#define Ssw_ClassForEachNode(p, pRepr, pNode, i)
Definition sswClass.c:73
int Id
Definition aig.h:85
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Ssw_ClassesClassNum()

int Ssw_ClassesClassNum ( Ssw_Cla_t * p)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file sswClass.c.

276{
277 return p->nClasses;
278}
Here is the caller graph for this function:

◆ Ssw_ClassesClearRefined()

void Ssw_ClassesClearRefined ( Ssw_Cla_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file sswClass.c.

244{
245 Vec_PtrClear( p->vRefined );
246}
Here is the caller graph for this function:

◆ Ssw_ClassesCollectClass()

void Ssw_ClassesCollectClass ( Ssw_Cla_t * p,
Aig_Obj_t * pRepr,
Vec_Ptr_t * vClass )

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file sswClass.c.

329{
330 int i;
331 Vec_PtrClear( vClass );
332 if ( p->pId2Class[pRepr->Id] == NULL )
333 return;
334 assert( p->pClassSizes[pRepr->Id] > 1 );
335 for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
336 Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
337}
Here is the caller graph for this function:

◆ Ssw_ClassesGetRefined()

Vec_Ptr_t * Ssw_ClassesGetRefined ( Ssw_Cla_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file sswClass.c.

228{
229 return p->vRefined;
230}

◆ Ssw_ClassesLitNum()

int Ssw_ClassesLitNum ( Ssw_Cla_t * p)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file sswClass.c.

292{
293 return p->nLits;
294}
Here is the caller graph for this function:

◆ Ssw_ClassesPrepare()

Ssw_Cla_t * Ssw_ClassesPrepare ( Aig_Man_t * pAig,
int nFramesK,
int fLatchCorr,
int fConstCorr,
int fOutputCorr,
int nMaxLevs,
int fVerbose )

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 596 of file sswClass.c.

597{
598// int nFrames = 4;
599// int nWords = 1;
600// int nIters = 16;
601
602// int nFrames = 32;
603// int nWords = 4;
604// int nIters = 0;
605
606 int nFrames = Abc_MaxInt( nFramesK, 4 );
607 int nWords = 2;
608 int nIters = 16;
609 Ssw_Cla_t * p;
610 Ssw_Sml_t * pSml;
611 Vec_Ptr_t * vCands;
612 Aig_Obj_t * pObj;
613 int i, k, RetValue;
614 abctime clk;
615
616 // start the classes
617 p = Ssw_ClassesStart( pAig );
618 p->fConstCorr = fConstCorr;
619
620 // perform sequential simulation
621clk = Abc_Clock();
622 pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
623if ( fVerbose )
624{
625 Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
626 1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
627 Abc_Print( 1, "Initial simulation of %d frames with %d words. ", nFrames, nWords );
628 ABC_PRT( "Time", Abc_Clock() - clk );
629}
630
631 // set comparison procedures
632clk = Abc_Clock();
633 Ssw_ClassesSetData( p, pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
634
635 // collect nodes to be considered as candidates
636 vCands = Vec_PtrAlloc( 1000 );
637 Aig_ManForEachObj( p->pAig, pObj, i )
638 {
639 if ( fLatchCorr )
640 {
641 if ( !Saig_ObjIsLo(p->pAig, pObj) )
642 continue;
643 }
644 else
645 {
646 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
647 continue;
648 // skip the node with more that the given number of levels
649 if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
650 continue;
651 }
652 Vec_PtrPush( vCands, pObj );
653 }
654
655 // this change will consider all PO drivers
656 if ( fOutputCorr )
657 {
658 Vec_PtrClear( vCands );
659 Aig_ManForEachObj( p->pAig, pObj, i )
660 pObj->fMarkB = 0;
661 Saig_ManForEachPo( p->pAig, pObj, i )
662 if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
663 Aig_ObjFanin0(pObj)->fMarkB = 1;
664 Aig_ManForEachObj( p->pAig, pObj, i )
665 if ( pObj->fMarkB )
666 Vec_PtrPush( vCands, pObj );
667 Aig_ManForEachObj( p->pAig, pObj, i )
668 pObj->fMarkB = 0;
669 }
670
671 // allocate room for classes
672 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
673 p->pMemClassesFree = p->pMemClasses;
674
675 // now it is time to refine the classes
676 Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
677if ( fVerbose )
678{
679 Abc_Print( 1, "Collecting candidate equivalence classes. " );
680ABC_PRT( "Time", Abc_Clock() - clk );
681}
682
683clk = Abc_Clock();
684 // perform iterative refinement using simulation
685 for ( i = 1; i < nIters; i++ )
686 {
687 // collect const1 candidates
688 Vec_PtrClear( vCands );
689 Aig_ManForEachObj( p->pAig, pObj, k )
690 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
691 Vec_PtrPush( vCands, pObj );
692 assert( Vec_PtrSize(vCands) == p->nCands1 );
693 // perform new round of simulation
694 Ssw_SmlResimulateSeq( pSml );
695 // check equivalence classes
696 RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
697 if ( RetValue == 0 )
698 break;
699 }
700 Ssw_SmlStop( pSml );
701 Vec_PtrFree( vCands );
702if ( fVerbose )
703{
704 Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
705 nFrames, nWords, i-1 );
706 ABC_PRT( "Time", Abc_Clock() - clk );
707}
709// Ssw_ClassesPrint( p, 0 );
710 return p;
711}
int nWords
Definition abcNpn.c:127
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_PRT(a, t)
Definition abc_global.h:255
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
int Ssw_ClassesPrepareRehash(Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
Definition sswClass.c:500
void Ssw_ClassesCheck(Ssw_Cla_t *p)
Definition sswClass.c:350
Ssw_Cla_t * Ssw_ClassesStart(Aig_Man_t *pAig)
Definition sswClass.c:140
void Ssw_ClassesSetData(Ssw_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
Definition sswClass.c:167
struct Ssw_Cla_t_ Ssw_Cla_t
Definition sswInt.h:50
void Ssw_SmlResimulateSeq(Ssw_Sml_t *p)
Definition sswSim.c:1269
unsigned Ssw_SmlObjHashWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition sswSim.c:63
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition sswSim.c:102
struct Ssw_Sml_t_ Ssw_Sml_t
Definition ssw.h:120
int Ssw_SmlObjsAreEqualWord(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition sswSim.c:124
Ssw_Sml_t * Ssw_SmlSimulateSeq(Aig_Man_t *pAig, int nPref, int nFrames, int nWords)
Definition sswSim.c:1248
void Ssw_SmlStop(Ssw_Sml_t *p)
Definition sswSim.c:1211
unsigned int fMarkB
Definition aig.h:80
unsigned Level
Definition aig.h:82
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPrepareFromReprs()

Ssw_Cla_t * Ssw_ClassesPrepareFromReprs ( Aig_Man_t * pAig)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 768 of file sswClass.c.

769{
770 Ssw_Cla_t * p;
771 Aig_Obj_t * pObj, * pRepr;
772 int * pClassSizes, nEntries, i;
773 // start the classes
774 p = Ssw_ClassesStart( pAig );
775 // allocate memory for classes
776 p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
777 // count classes
778 p->nCands1 = 0;
779 Aig_ManForEachObj( pAig, pObj, i )
780 {
781 if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
782 {
783 p->nCands1++;
784 continue;
785 }
786 if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
787 {
788 if ( p->pClassSizes[pRepr->Id]++ == 0 )
789 p->pClassSizes[pRepr->Id]++;
790 }
791 }
792 // add nodes
793 nEntries = 0;
794 p->nClasses = 0;
795 pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
796 Aig_ManForEachObj( pAig, pObj, i )
797 {
798 if ( p->pClassSizes[i] )
799 {
800 p->pId2Class[i] = p->pMemClasses + nEntries;
801 nEntries += p->pClassSizes[i];
802 p->pId2Class[i][pClassSizes[i]++] = pObj;
803 p->nClasses++;
804 continue;
805 }
806 if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
807 continue;
808 if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
809 p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
810 }
811 p->pMemClassesFree = p->pMemClasses + nEntries;
812 p->nLits = nEntries - p->nClasses;
813 assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
814 ABC_FREE( pClassSizes );
815// Abc_Print( 1, "After converting:\n" );
816// Ssw_ClassesPrint( p, 0 );
817 return p;
818}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
int memcmp()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPreparePairs()

Ssw_Cla_t * Ssw_ClassesPreparePairs ( Aig_Man_t * pAig,
Vec_Int_t ** pvClasses )

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 862 of file sswClass.c.

863{
864 Ssw_Cla_t * p;
865 Aig_Obj_t ** ppClassNew;
866 Aig_Obj_t * pObj, * pRepr, * pPrev;
867 int i, k, nTotalObjs, nEntries, Entry;
868 // start the classes
869 p = Ssw_ClassesStart( pAig );
870 // count the number of entries in the classes
871 nTotalObjs = 0;
872 for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
873 nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
874 // allocate memory for classes
875 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
876 // create constant-1 class
877 if ( pvClasses[0] )
878 Vec_IntForEachEntry( pvClasses[0], Entry, i )
879 {
880 assert( (i == 0) == (Entry == 0) );
881 if ( i == 0 )
882 continue;
883 pObj = Aig_ManObj( pAig, Entry );
884 Ssw_ObjSetConst1Cand( pAig, pObj );
885 p->nCands1++;
886 }
887 // create classes
888 nEntries = 0;
889 for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
890 {
891 if ( pvClasses[i] == NULL )
892 continue;
893 // get room for storing the class
894 ppClassNew = p->pMemClasses + nEntries;
895 nEntries += Vec_IntSize( pvClasses[i] );
896 // store the nodes of the class
897 pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
898 ppClassNew[0] = pRepr;
899 Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
900 {
901 pObj = Aig_ManObj( pAig, Entry );
902 assert( pPrev->Id < pObj->Id );
903 pPrev = pObj;
904 ppClassNew[k] = pObj;
905 Aig_ObjSetRepr( pAig, pObj, pRepr );
906 }
907 // create new class
908 Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
909 }
910 // prepare room for new classes
911 p->pMemClassesFree = p->pMemClasses + nEntries;
913// Ssw_ClassesPrint( p, 0 );
914 return p;
915}
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPreparePairsSimple()

Ssw_Cla_t * Ssw_ClassesPreparePairsSimple ( Aig_Man_t * pMiter,
Vec_Int_t * vPairs )

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file sswClass.c.

929{
930 Ssw_Cla_t * p;
931 Aig_Obj_t ** ppClassNew;
932 Aig_Obj_t * pObj, * pRepr;
933 int i;
934 // start the classes
935 p = Ssw_ClassesStart( pMiter );
936 // allocate memory for classes
937 p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
938 // create classes
939 for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
940 {
941 pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
942 pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
943 assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
944 Aig_ObjSetRepr( pMiter, pObj, pRepr );
945 // get room for storing the class
946 ppClassNew = p->pMemClasses + i;
947 ppClassNew[0] = pRepr;
948 ppClassNew[1] = pObj;
949 // create new class
950 Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
951 }
952 // prepare room for new classes
953 p->pMemClassesFree = NULL;
955// Ssw_ClassesPrint( p, 0 );
956 return p;
957}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPrepareRehash()

int Ssw_ClassesPrepareRehash ( Ssw_Cla_t * p,
Vec_Ptr_t * vCands,
int fConstCorr )

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

Synopsis [Takes the set of const1 cands and rehashes them using sim info.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file sswClass.c.

501{
502// Aig_Man_t * pAig = p->pAig;
503 Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
504 Aig_Obj_t * pObj, * pTemp, * pRepr;
505 int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
506
507 // allocate the hash table hashing simulation info into nodes
508 nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
509 ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
510 ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
511
512 // sort through the candidates
513 nEntries = 0;
514 p->nCands1 = 0;
515 Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
516 {
517 assert( p->pClassSizes[pObj->Id] == 0 );
518 Aig_ObjSetRepr( p->pAig, pObj, NULL );
519 // check if the node belongs to the class of constant 1
520 if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
521 {
522 Ssw_ObjSetConst1Cand( p->pAig, pObj );
523 p->nCands1++;
524 continue;
525 }
526 if ( fConstCorr )
527 continue;
528 // hash the node by its simulation info
529 iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
530 // add the node to the class
531 if ( ppTable[iEntry] == NULL )
532 {
533 ppTable[iEntry] = pObj;
534 }
535 else
536 {
537 // set the representative of this node
538 pRepr = ppTable[iEntry];
539 Aig_ObjSetRepr( p->pAig, pObj, pRepr );
540 // add node to the table
541 if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
542 { // this will be the second entry
543 p->pClassSizes[pRepr->Id]++;
544 nEntries++;
545 }
546 // add the entry to the list
547 Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
548 Ssw_ObjSetNext( ppNexts, pRepr, pObj );
549 p->pClassSizes[pRepr->Id]++;
550 nEntries++;
551 }
552 }
553
554 // copy the entries into storage in the topological order
555 nEntries2 = 0;
556 Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
557 {
558 nNodes = p->pClassSizes[pObj->Id];
559 // skip the nodes that are not representatives of non-trivial classes
560 if ( nNodes == 0 )
561 continue;
562 assert( nNodes > 1 );
563 // add the nodes to the class in the topological order
564 ppClassNew = p->pMemClassesFree + nEntries2;
565 ppClassNew[0] = pObj;
566 for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
567 pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
568 {
569 ppClassNew[nNodes-k] = pTemp;
570 }
571 // add the class of nodes
572 p->pClassSizes[pObj->Id] = 0;
573 Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
574 // increment the number of entries
575 nEntries2 += nNodes;
576 }
577 p->pMemClassesFree += nEntries2;
578 assert( nEntries == nEntries2 );
579 ABC_FREE( ppTable );
580 ABC_FREE( ppNexts );
581 // now it is time to refine the classes
582 return Ssw_ClassesRefine( p, 1 );
583}
int Ssw_ClassesRefine(Ssw_Cla_t *p, int fRecursive)
Definition sswClass.c:1034
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPrepareSimple()

Ssw_Cla_t * Ssw_ClassesPrepareSimple ( Aig_Man_t * pAig,
int fLatchCorr,
int nMaxLevs )

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 724 of file sswClass.c.

725{
726 Ssw_Cla_t * p;
727 Aig_Obj_t * pObj;
728 int i;
729 // start the classes
730 p = Ssw_ClassesStart( pAig );
731 // go through the nodes
732 p->nCands1 = 0;
733 Aig_ManForEachObj( pAig, pObj, i )
734 {
735 if ( fLatchCorr )
736 {
737 if ( !Saig_ObjIsLo(pAig, pObj) )
738 continue;
739 }
740 else
741 {
742 if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
743 continue;
744 // skip the node with more that the given number of levels
745 if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
746 continue;
747 }
748 Ssw_ObjSetConst1Cand( pAig, pObj );
749 p->nCands1++;
750 }
751 // allocate room for classes
752 p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
753// Ssw_ClassesPrint( p, 0 );
754 return p;
755}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPrepareTargets()

Ssw_Cla_t * Ssw_ClassesPrepareTargets ( Aig_Man_t * pAig)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 831 of file sswClass.c.

832{
833 Ssw_Cla_t * p;
834 Aig_Obj_t * pObj;
835 int i;
836 // start the classes
837 p = Ssw_ClassesStart( pAig );
838 // go through the nodes
839 p->nCands1 = 0;
840 Saig_ManForEachPo( pAig, pObj, i )
841 {
842 Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
843 p->nCands1++;
844 }
845 // allocate room for classes
846 p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
847// Ssw_ClassesPrint( p, 0 );
848 return p;
849}
Here is the call graph for this function:

◆ Ssw_ClassesPrint()

void Ssw_ClassesPrint ( Ssw_Cla_t * p,
int fVeryVerbose )

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file sswClass.c.

415{
416 Aig_Obj_t ** ppClass;
417 Aig_Obj_t * pObj;
418 int i;
419 Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
420 p->nCands1, p->nClasses, p->nCands1+p->nLits );
421 if ( !fVeryVerbose )
422 return;
423 Abc_Print( 1, "Constants { " );
424 Aig_ManForEachObj( p->pAig, pObj, i )
425 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
426 Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
427 Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
428 Abc_Print( 1, "}\n" );
429 Ssw_ManForEachClass( p, ppClass, i )
430 {
431 Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
432 Ssw_ClassesPrintOne( p, ppClass[0] );
433 }
434 Abc_Print( 1, "\n" );
435}
int Aig_SupportSize(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition aigDfs.c:772
int Aig_NodeMffcSupp(Aig_Man_t *p, Aig_Obj_t *pNode, int LevelMin, Vec_Ptr_t *vSupp)
Definition aigMffc.c:179
void Ssw_ClassesPrintOne(Ssw_Cla_t *p, Aig_Obj_t *pRepr)
Definition sswClass.c:392
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesPrintOne()

void Ssw_ClassesPrintOne ( Ssw_Cla_t * p,
Aig_Obj_t * pRepr )

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 392 of file sswClass.c.

393{
394 Aig_Obj_t * pObj;
395 int i;
396 Abc_Print( 1, "{ " );
397 Ssw_ClassForEachNode( p, pRepr, pObj, i )
398 Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
399 Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
400 Abc_Print( 1, "}\n" );
401}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesReadAig()

Aig_Man_t * Ssw_ClassesReadAig ( Ssw_Cla_t * p)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file sswClass.c.

212{
213 return p->pAig;
214}

◆ Ssw_ClassesReadClass()

Aig_Obj_t ** Ssw_ClassesReadClass ( Ssw_Cla_t * p,
Aig_Obj_t * pRepr,
int * pnSize )

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file sswClass.c.

308{
309 if ( p->pId2Class[pRepr->Id] == NULL )
310 return NULL;
311 assert( p->pId2Class[pRepr->Id] != NULL );
312 assert( p->pClassSizes[pRepr->Id] > 1 );
313 *pnSize = p->pClassSizes[pRepr->Id];
314 return p->pId2Class[pRepr->Id];
315}
Here is the caller graph for this function:

◆ Ssw_ClassesRefine()

int Ssw_ClassesRefine ( Ssw_Cla_t * p,
int fRecursive )

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1034 of file sswClass.c.

1035{
1036 Aig_Obj_t ** ppClass;
1037 int i, nRefis = 0;
1038 Ssw_ManForEachClass( p, ppClass, i )
1039 nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
1040 return nRefis;
1041}
int Ssw_ClassesRefineOneClass(Ssw_Cla_t *p, Aig_Obj_t *pReprOld, int fRecursive)
Definition sswClass.c:970
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesRefineConst1()

int Ssw_ClassesRefineConst1 ( Ssw_Cla_t * p,
int fRecursive )

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1119 of file sswClass.c.

1120{
1121 Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1122 int i;
1123 // collect the nodes to be refined
1124 Vec_PtrClear( p->vClassNew );
1125 for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
1126 if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
1127 {
1128 pObj = Aig_ManObj( p->pAig, i );
1129 if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1130 {
1131 Vec_PtrPush( p->vClassNew, pObj );
1132// Vec_PtrPush( p->vRefined, pObj );
1133 }
1134 }
1135 // check if there is a new class
1136 if ( Vec_PtrSize(p->vClassNew) == 0 )
1137 return 0;
1138 if ( p->fConstCorr )
1139 {
1140 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1141 Aig_ObjSetRepr( p->pAig, pObj, NULL );
1142 return 1;
1143 }
1144 p->nCands1 -= Vec_PtrSize(p->vClassNew);
1145 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1146 Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1147 if ( Vec_PtrSize(p->vClassNew) == 1 )
1148 return 1;
1149 // create a new class composed of these nodes
1150 ppClassNew = p->pMemClassesFree;
1151 p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1152 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1153 {
1154 ppClassNew[i] = pObj;
1155 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1156 }
1157 Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1158 // refine them recursively
1159 if ( fRecursive )
1160 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1161 return 1;
1162}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesRefineConst1Group()

int Ssw_ClassesRefineConst1Group ( Ssw_Cla_t * p,
Vec_Ptr_t * vRoots,
int fRecursive )

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1074 of file sswClass.c.

1075{
1076 Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
1077 int i;
1078 if ( Vec_PtrSize(vRoots) == 0 )
1079 return 0;
1080 // collect the nodes to be refined
1081 Vec_PtrClear( p->vClassNew );
1082 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
1083 if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
1084 Vec_PtrPush( p->vClassNew, pObj );
1085 // check if there is a new class
1086 if ( Vec_PtrSize(p->vClassNew) == 0 )
1087 return 0;
1088 p->nCands1 -= Vec_PtrSize(p->vClassNew);
1089 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
1090 Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
1091 if ( Vec_PtrSize(p->vClassNew) == 1 )
1092 return 1;
1093 // create a new class composed of these nodes
1094 ppClassNew = p->pMemClassesFree;
1095 p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
1096 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1097 {
1098 ppClassNew[i] = pObj;
1099 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1100 }
1101 Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
1102 // refine them recursively
1103 if ( fRecursive )
1104 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1105 return 1;
1106}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesRefineGroup()

int Ssw_ClassesRefineGroup ( Ssw_Cla_t * p,
Vec_Ptr_t * vReprs,
int fRecursive )

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1054 of file sswClass.c.

1055{
1056 Aig_Obj_t * pObj;
1057 int i, nRefis = 0;
1058 Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
1059 nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
1060 return nRefis;
1061}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesRefineOneClass()

int Ssw_ClassesRefineOneClass ( Ssw_Cla_t * p,
Aig_Obj_t * pReprOld,
int fRecursive )

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

Synopsis [Iteratively refines the classes after simulation.]

Description [Returns the number of refinements performed.]

SideEffects []

SeeAlso []

Definition at line 970 of file sswClass.c.

971{
972 Aig_Obj_t ** pClassOld, ** pClassNew;
973 Aig_Obj_t * pObj, * pReprNew;
974 int i;
975
976 // split the class
977 Vec_PtrClear( p->vClassOld );
978 Vec_PtrClear( p->vClassNew );
979 Ssw_ClassForEachNode( p, pReprOld, pObj, i )
980 if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
981 Vec_PtrPush( p->vClassOld, pObj );
982 else
983 Vec_PtrPush( p->vClassNew, pObj );
984 // check if splitting happened
985 if ( Vec_PtrSize(p->vClassNew) == 0 )
986 return 0;
987 // remember that this class is refined
988// Ssw_ClassForEachNode( p, pReprOld, pObj, i )
989// Vec_PtrPush( p->vRefined, pObj );
990
991 // get the new representative
992 pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
993 assert( Vec_PtrSize(p->vClassOld) > 0 );
994 assert( Vec_PtrSize(p->vClassNew) > 0 );
995
996 // create old class
997 pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
998 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
999 {
1000 pClassOld[i] = pObj;
1001 Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
1002 }
1003 // create new class
1004 pClassNew = pClassOld + i;
1005 Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
1006 {
1007 pClassNew[i] = pObj;
1008 Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
1009 }
1010
1011 // put classes back
1012 if ( Vec_PtrSize(p->vClassOld) > 1 )
1013 Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
1014 if ( Vec_PtrSize(p->vClassNew) > 1 )
1015 Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
1016
1017 // check if the class should be recursively refined
1018 if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
1019 return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
1020 return 1;
1021}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesRemoveNode()

void Ssw_ClassesRemoveNode ( Ssw_Cla_t * p,
Aig_Obj_t * pObj )

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file sswClass.c.

449{
450 Aig_Obj_t * pRepr, * pTemp;
451 assert( p->pClassSizes[pObj->Id] == 0 );
452 assert( p->pId2Class[pObj->Id] == NULL );
453 pRepr = Aig_ObjRepr( p->pAig, pObj );
454 assert( pRepr != NULL );
455// Vec_PtrPush( p->vRefined, pObj );
456 if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
457 {
458 assert( p->pClassSizes[pRepr->Id] == 0 );
459 assert( p->pId2Class[pRepr->Id] == NULL );
460 Aig_ObjSetRepr( p->pAig, pObj, NULL );
461 p->nCands1--;
462 return;
463 }
464// Vec_PtrPush( p->vRefined, pRepr );
465 Aig_ObjSetRepr( p->pAig, pObj, NULL );
466 assert( p->pId2Class[pRepr->Id][0] == pRepr );
467 assert( p->pClassSizes[pRepr->Id] >= 2 );
468 if ( p->pClassSizes[pRepr->Id] == 2 )
469 {
470 p->pId2Class[pRepr->Id] = NULL;
471 p->nClasses--;
472 p->pClassSizes[pRepr->Id] = 0;
473 p->nLits--;
474 }
475 else
476 {
477 int i, k = 0;
478 // remove the entry from the class
479 Ssw_ClassForEachNode( p, pRepr, pTemp, i )
480 if ( pTemp != pObj )
481 p->pId2Class[pRepr->Id][k++] = pTemp;
482 assert( k + 1 == p->pClassSizes[pRepr->Id] );
483 // reduce the class
484 p->pClassSizes[pRepr->Id]--;
485 p->nLits--;
486 }
487}
Here is the caller graph for this function:

◆ Ssw_ClassesSetData()

void Ssw_ClassesSetData ( Ssw_Cla_t * p,
void * pManData,
unsigned(* pFuncNodeHash )(void *, Aig_Obj_t *),
int(* pFuncNodeIsConst )(void *, Aig_Obj_t *),
int(* pFuncNodesAreEqual )(void *, Aig_Obj_t *, Aig_Obj_t *) )

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file sswClass.c.

171{
172 p->pManData = pManData;
173 p->pFuncNodeHash = pFuncNodeHash;
174 p->pFuncNodeIsConst = pFuncNodeIsConst;
175 p->pFuncNodesAreEqual = pFuncNodesAreEqual;
176}
Here is the caller graph for this function:

◆ Ssw_ClassesStart()

Ssw_Cla_t * Ssw_ClassesStart ( Aig_Man_t * pAig)

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file sswClass.c.

141{
142 Ssw_Cla_t * p;
143 p = ABC_ALLOC( Ssw_Cla_t, 1 );
144 memset( p, 0, sizeof(Ssw_Cla_t) );
145 p->pAig = pAig;
146 p->pId2Class = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
147 p->pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
148 p->vClassOld = Vec_PtrAlloc( 100 );
149 p->vClassNew = Vec_PtrAlloc( 100 );
150 p->vRefined = Vec_PtrAlloc( 1000 );
151 if ( pAig->pReprs == NULL )
152 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
153 return p;
154}
void Aig_ManReprStart(Aig_Man_t *p, int nIdMax)
DECLARATIONS ///.
Definition aigRepr.c:45
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ClassesStop()

void Ssw_ClassesStop ( Ssw_Cla_t * p)

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswClass.c.

190{
191 if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
192 if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
193 Vec_PtrFree( p->vRefined );
194 ABC_FREE( p->pId2Class );
195 ABC_FREE( p->pClassSizes );
196 ABC_FREE( p->pMemClasses );
197 ABC_FREE( p );
198}
Here is the caller graph for this function: