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

Go to the source code of this file.

Classes

struct  Sbd_Par_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Sbd_Par_t_ Sbd_Par_t
 INCLUDES ///.
 

Functions

void Sbd_ParSetDefault (Sbd_Par_t *pPars)
 MACRO DEFINITIONS ///.
 
Gia_Man_t * Sbd_NtkPerform (Gia_Man_t *p, Sbd_Par_t *pPars)
 

Typedef Documentation

◆ Sbd_Par_t

typedef typedefABC_NAMESPACE_HEADER_START struct Sbd_Par_t_ Sbd_Par_t

INCLUDES ///.

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

FileName [sbd.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
sbd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 38 of file sbd.h.

Function Documentation

◆ Sbd_NtkPerform()

Gia_Man_t * Sbd_NtkPerform ( Gia_Man_t * p,
Sbd_Par_t * pPars )
extern

Definition at line 2117 of file sbdCore.c.

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}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
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_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManOrderWithBoxes
Vec_Int_t * Gia_ManOrderWithBoxes(Gia_Man_t *p)
Definition giaTim.c:286
Sbd_ManStart
Sbd_Man_t * Sbd_ManStart(Gia_Man_t *pGia, Sbd_Par_t *pPars)
Definition sbdCore.c:200
Sbd_ManDelay
int Sbd_ManDelay(Sbd_Man_t *p)
Definition sbdCore.c:1718
Sbd_NtkPerformOne
void Sbd_NtkPerformOne(Sbd_Man_t *p, int Pivot)
Definition sbdCore.c:2073
Sbd_ManStop
void Sbd_ManStop(Sbd_Man_t *p)
Definition sbdCore.c:249
Sbd_Man_t
struct Sbd_Man_t_ Sbd_Man_t
Definition sbdCore.c:33
Sbd_ManDerive
Gia_Man_t * Sbd_ManDerive(Sbd_Man_t *pMan, Gia_Man_t *p, Vec_Int_t *vMirrors)
Definition sbdCore.c:2030
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_StoComputeCutsCi
void Sbd_StoComputeCutsCi(Sbd_Sto_t *p, int iObj, int Delay, int Level)
Definition sbdCut.c:724
Sbc_ManCriticalPath
Vec_Bit_t * Sbc_ManCriticalPath(Gia_Man_t *p)
Definition sbdPath.c:119
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
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Here is the call graph for this function:

◆ Sbd_ParSetDefault()

void Sbd_ParSetDefault ( Sbd_Par_t * pPars)
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file sbdCore.c.

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}
Sbd_Par_t
typedefABC_NAMESPACE_HEADER_START struct Sbd_Par_t_ Sbd_Par_t
INCLUDES ///.
Definition sbd.h:38
memset
char * memset()
Here is the call graph for this function: