ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
dch.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Dch_Pars_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
 INCLUDES ///.
 

Functions

Aig_Man_t * Dch_DeriveTotalAig (Vec_Ptr_t *vAigs)
 MACRO DEFINITIONS ///.
 
void Dch_ManSetDefaultParams (Dch_Pars_t *p)
 DECLARATIONS ///.
 
int Dch_ManReadVerbose (Dch_Pars_t *p)
 
Aig_Man_t * Dch_ComputeChoices (Aig_Man_t *pAig, Dch_Pars_t *pPars)
 
void Dch_ComputeEquivalences (Aig_Man_t *pAig, Dch_Pars_t *pPars)
 
Aig_Man_t * Dar_ManChoiceNew (Aig_Man_t *pAig, Dch_Pars_t *pPars)
 

Typedef Documentation

◆ Dch_Pars_t

typedef typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t

INCLUDES ///.

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

FileName [dch.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id
dch.h,v 1.00 2008/07/29 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 43 of file dch.h.

Function Documentation

◆ Dar_ManChoiceNew()

Aig_Man_t * Dar_ManChoiceNew ( Aig_Man_t * pAig,
Dch_Pars_t * pPars )
extern

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

Synopsis [Reproduces script "compress2".]

Description [Consumes the input AIG to reduce memory usage.]

SideEffects []

SeeAlso []

Definition at line 849 of file darScript.c.

850{
851 extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
852 extern Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose );
853 extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
854// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
855 extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
856// int fVerbose = pPars->fVerbose;
857 Aig_Man_t * pMan, * pTemp;
858 Gia_Man_t * pGia;
859 Vec_Ptr_t * vPios;
860 void * pManTime;
861 char * pName, * pSpec;
862 abctime clk;
863
864 // save useful things
865 pManTime = pAig->pManTime; pAig->pManTime = NULL;
866 pName = Abc_UtilStrsav( pAig->pName );
867 pSpec = Abc_UtilStrsav( pAig->pSpec );
868
869 // perform synthesis
870clk = Abc_Clock();
871 pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
872pPars->timeSynth = Abc_Clock() - clk;
873
874 // perform choice computation
875 if ( pPars->fUseNew )
876 pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
877 else if ( pPars->fUseNew2 )
878 pMan = Cec_ComputeChoicesNew2( pGia, pPars->nBTLimit, pPars->fVerbose );
879 else if ( pPars->fUseGia )
880 pMan = Cec_ComputeChoices( pGia, pPars );
881 else
882 {
883 pMan = Gia_ManToAigSkip( pGia, 3 );
884 pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
885 Aig_ManStop( pTemp );
886 }
887 Gia_ManStop( pGia );
888
889 // create guidence
890 vPios = Aig_ManOrderPios( pMan, pAig );
891 Aig_ManStop( pAig );
892
893 // reconstruct the network
894 pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
895 Aig_ManStop( pTemp );
896 Vec_PtrFree( vPios );
897
898 // reset levels
899 pMan->pManTime = pManTime;
900 Aig_ManChoiceLevel( pMan );
901
902 // copy names
903 ABC_FREE( pMan->pName );
904 ABC_FREE( pMan->pSpec );
905 pMan->pName = pName;
906 pMan->pSpec = pSpec;
907 return pMan;
908}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_ManOrderPios
Vec_Ptr_t * Aig_ManOrderPios(Aig_Man_t *p, Aig_Man_t *pOrder)
Definition aigDup.c:626
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition aigDup.c:563
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManDupDfsGuided
Aig_Man_t * Aig_ManDupDfsGuided(Aig_Man_t *p, Vec_Ptr_t *vPios)
Definition aigDup.c:694
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManChoiceLevel
int Aig_ManChoiceLevel(Aig_Man_t *p)
Definition aigDfs.c:595
Cec_ComputeChoicesNew
Aig_Man_t * Cec_ComputeChoicesNew(Gia_Man_t *pGia, int nConfs, int fVerbose)
Definition cecChoice.c:415
Cec_ComputeChoices
Aig_Man_t * Cec_ComputeChoices(Gia_Man_t *pGia, Dch_Pars_t *pPars)
Definition cecChoice.c:385
Cec_ComputeChoicesNew2
Aig_Man_t * Cec_ComputeChoicesNew2(Gia_Man_t *pGia, int nConfs, int fVerbose)
Definition cecChoice.c:425
Dar_NewChoiceSynthesis
Gia_Man_t * Dar_NewChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
Definition darScript.c:632
Dch_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition dch.h:43
Dch_ComputeChoices
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition dchCore.c:89
Gia_ManToAigSkip
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
Definition giaAig.c:365
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Vec_Ptr_t
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:

◆ Dch_ComputeChoices()

Aig_Man_t * Dch_ComputeChoices ( Aig_Man_t * pAig,
Dch_Pars_t * pPars )
extern

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 89 of file dchCore.c.

90{
91 Dch_Man_t * p;
92 Aig_Man_t * pResult;
93 abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock();
94 // reset random numbers
95 Aig_ManRandom(1);
96 // start the choicing manager
97 p = Dch_ManCreate( pAig, pPars );
98 // compute candidate equivalence classes
99clk = Abc_Clock();
100 p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
101p->timeSimInit = Abc_Clock() - clk;
102// Dch_ClassesPrint( p->ppClasses, 0 );
103 p->nLits = Dch_ClassesLitNum( p->ppClasses );
104 // perform SAT sweeping
105 Dch_ManSweep( p );
106 // free memory ahead of time
107p->timeTotal = Abc_Clock() - clkTotal;
108 Dch_ManStop( p );
109 if ( pPars->fVerbose )
110 Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 );
111 // create choices
112 ABC_FREE( pAig->pTable );
113 pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
114 // count the number of representatives
115 if ( pPars->fVerbose )
116 Abc_Print( 1, "STATS: Ands:%8d ->%8d. Reprs:%7d ->%7d. Choices =%7d.\n",
117 Aig_ManNodeNum(pAig),
118 Aig_ManNodeNum(pResult),
119 Dch_DeriveChoiceCountReprs( pAig ),
120 Dch_DeriveChoiceCountEquivs( pResult ),
121 Aig_ManChoiceNum( pResult ) );
122 return pResult;
123}
Aig_ManChoiceNum
int Aig_ManChoiceNum(Aig_Man_t *p)
Definition aigUtil.c:1020
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition aigUtil.c:1170
Dch_DeriveChoiceAig
Aig_Man_t * Dch_DeriveChoiceAig(Aig_Man_t *pAig, int fSkipRedSupps)
Definition dchChoice.c:524
Dch_DeriveChoiceCountEquivs
int Dch_DeriveChoiceCountEquivs(Aig_Man_t *pAig)
Definition dchChoice.c:89
Dch_DeriveChoiceCountReprs
int Dch_DeriveChoiceCountReprs(Aig_Man_t *pAig)
FUNCTION DECLARATIONS ///.
Definition dchChoice.c:75
Dch_ClassesLitNum
int Dch_ClassesLitNum(Dch_Cla_t *p)
Definition dchClass.c:206
Dch_ManCreate
Dch_Man_t * Dch_ManCreate(Aig_Man_t *pAig, Dch_Pars_t *pPars)
DECLARATIONS ///.
Definition dchMan.c:45
Dch_Man_t
struct Dch_Man_t_ Dch_Man_t
Definition dchInt.h:50
Dch_ManStop
void Dch_ManStop(Dch_Man_t *p)
Definition dchMan.c:122
Dch_ManSweep
void Dch_ManSweep(Dch_Man_t *p)
Definition dchSweep.c:106
Dch_CreateCandEquivClasses
Dch_Cla_t * Dch_CreateCandEquivClasses(Aig_Man_t *pAig, int nWords, int fVerbose)
Definition dchSim.c:264
p
Cube * p
Definition exorList.c:222
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dch_ComputeEquivalences()

void Dch_ComputeEquivalences ( Aig_Man_t * pAig,
Dch_Pars_t * pPars )
extern

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 136 of file dchCore.c.

137{
138 Dch_Man_t * p;
139 abctime clk, clkTotal = Abc_Clock();
140 // reset random numbers
141 Aig_ManRandom(1);
142 // start the choicing manager
143 p = Dch_ManCreate( pAig, pPars );
144 // compute candidate equivalence classes
145clk = Abc_Clock();
146 p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
147p->timeSimInit = Abc_Clock() - clk;
148// Dch_ClassesPrint( p->ppClasses, 0 );
149 p->nLits = Dch_ClassesLitNum( p->ppClasses );
150 // perform SAT sweeping
151 Dch_ManSweep( p );
152 // free memory ahead of time
153p->timeTotal = Abc_Clock() - clkTotal;
154 Dch_ManStop( p );
155}

◆ Dch_DeriveTotalAig()

Aig_Man_t * Dch_DeriveTotalAig ( Vec_Ptr_t * vAigs)
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Derives the cumulative AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file dchAig.c.

66{
67 Aig_Man_t * pAig, * pAig2, * pAigTotal;
68 Aig_Obj_t * pObj, * pObjPi, * pObjPo;
69 int i, k, nNodes;
70 assert( Vec_PtrSize(vAigs) > 0 );
71 // make sure they have the same number of PIs/POs
72 nNodes = 0;
73 pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
74 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
75 {
76 assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) );
77 assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) );
78 nNodes += Aig_ManNodeNum(pAig2);
79 Aig_ManCleanData( pAig2 );
80 }
81 // map constant nodes
82 pAigTotal = Aig_ManStart( nNodes );
83 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
84 Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal);
85 // map primary inputs
86 Aig_ManForEachCi( pAig, pObj, i )
87 {
88 pObjPi = Aig_ObjCreateCi( pAigTotal );
89 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
90 Aig_ManCi( pAig2, i )->pData = pObjPi;
91 }
92 // construct the AIG in the order of POs
93 Aig_ManForEachCo( pAig, pObj, i )
94 {
95 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
96 {
97 pObjPo = Aig_ManCo( pAig2, i );
98 Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
99 }
100 Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
101 }
102/*
103 // mark the cone of the first AIG
104 Aig_ManIncrementTravId( pAigTotal );
105 Aig_ManForEachObj( pAig, pObj, i )
106 if ( pObj->pData )
107 Aig_ObjSetTravIdCurrent( pAigTotal, pObj->pData );
108*/
109 // cleanup should not be done
110 return pAigTotal;
111}
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Dch_DeriveTotalAig_rec
ABC_NAMESPACE_IMPL_START void Dch_DeriveTotalAig_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
DECLARATIONS ///.
Definition dchAig.c:45
assert
#define assert(ex)
Definition util_old.h:213
Vec_PtrForEachEntry
#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:

◆ Dch_ManReadVerbose()

int Dch_ManReadVerbose ( Dch_Pars_t * p)
extern

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

Synopsis [Returns verbose parameter.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file dchCore.c.

74{
75 return p->fVerbose;
76}

◆ Dch_ManSetDefaultParams()

void Dch_ManSetDefaultParams ( Dch_Pars_t * p)
extern

DECLARATIONS ///.

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

FileName [dchCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [The core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id
dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchCore.c.

46{
47 memset( p, 0, sizeof(Dch_Pars_t) );
48 p->nWords = 8; // the number of simulation words
49 p->nBTLimit = 1000; // conflict limit at a node
50 p->nSatVarMax = 5000; // the max number of SAT variables
51 p->fSynthesis = 1; // derives three snapshots
52 p->fPolarFlip = 1; // uses polarity adjustment
53 p->fSimulateTfo = 1; // simulate TFO
54 p->fPower = 0; // power-aware rewriting
55 p->fLightSynth = 0; // uses lighter version of synthesis
56 p->fSkipRedSupp = 0; // skips choices with redundant structural support
57 p->fVerbose = 0; // verbose stats
58 p->nNodesAhead = 1000; // the lookahead in terms of nodes
59 p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
60}
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function: