ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
cecSynth.c File Reference
#include "cecInt.h"
#include "aig/gia/giaAig.h"
Include dependency graph for cecSynth.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Cec_SeqSynthesisSetDefaultParams (Cec_ParSeq_t *p)
 DECLARATIONS ///.
 
int Cec_SeqReadMinDomSize (Cec_ParSeq_t *p)
 
int Cec_SeqReadVerbose (Cec_ParSeq_t *p)
 
Gia_Man_t * Gia_ManRegCreatePart (Gia_Man_t *p, Vec_Int_t *vPart, int *pnCountPis, int *pnCountRegs, int **ppMapBack)
 
int Gia_TransferMappedClasses (Gia_Man_t *pPart, int *pMapBack, int *pReprs)
 
int Gia_ManFindRepr_rec (int *pReprs, int Id)
 
void Gia_ManNormalizeEquivalences (Gia_Man_t *p, int *pReprs)
 
int Cec_SequentialSynthesisPart (Gia_Man_t *p, Cec_ParSeq_t *pPars)
 
int Gia_ManTestOnePair (Gia_Man_t *p, int iObj1, int iObj2, int fPhase)
 

Function Documentation

◆ Cec_SeqReadMinDomSize()

int Cec_SeqReadMinDomSize ( Cec_ParSeq_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file cecSynth.c.

74{
75 return p->nMinDomSize;
76}
p
Cube * p
Definition exorList.c:222

◆ Cec_SeqReadVerbose()

int Cec_SeqReadVerbose ( Cec_ParSeq_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file cecSynth.c.

90{
91 return p->fVerbose;
92}

◆ Cec_SeqSynthesisSetDefaultParams()

ABC_NAMESPACE_IMPL_START void Cec_SeqSynthesisSetDefaultParams ( Cec_ParSeq_t * p)

DECLARATIONS ///.

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

FileName [cecSynth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Partitioned sequential synthesis.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
cecSynth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Populate sequential synthesis parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cecSynth.c.

47{
48 memset( p, 0, sizeof(Cec_ParSeq_t) );
49 p->fUseLcorr = 0; // enables latch correspondence
50 p->fUseScorr = 0; // enables signal correspondence
51 p->nBTLimit = 1000; // (scorr/lcorr) conflict limit at a node
52 p->nFrames = 1; // (scorr only) the number of timeframes
53 p->nLevelMax = -1; // (scorr only) the max number of levels
54 p->fConsts = 1; // (scl only) merging constants
55 p->fEquivs = 1; // (scl only) merging equivalences
56 p->fUseMiniSat = 0; // enables MiniSat in lcorr/scorr
57 p->nMinDomSize = 100; // the size of minimum clock domain
58 p->fVeryVerbose = 0; // verbose stats
59 p->fVerbose = 0; // verbose stats
60}
Cec_ParSeq_t
struct Cec_ParSeq_t_ Cec_ParSeq_t
Definition cec.h:188
memset
char * memset()
Here is the call graph for this function:

◆ Cec_SequentialSynthesisPart()

int Cec_SequentialSynthesisPart ( Gia_Man_t * p,
Cec_ParSeq_t * pPars )

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

Synopsis [Partitioned sequential synthesis.]

Description [Returns AIG annotated with equivalence classes.]

SideEffects []

SeeAlso []

Definition at line 291 of file cecSynth.c.

292{
293 int fPrintParts = 0;
294 char Buffer[100];
295 Gia_Man_t * pTemp;
296 Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms;
297 Vec_Int_t * vPart;
298 int * pMapBack, * pReprs;
299 int i, nCountPis, nCountRegs;
300 int nClasses;
301 abctime clk = Abc_Clock();
302
303 // save parameters
304 if ( fPrintParts )
305 {
306 // print partitions
307 Abc_Print( 1, "The following clock domains are used:\n" );
308 Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
309 {
310 pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
311 sprintf( Buffer, "part%03d.aig", i );
312 Gia_AigerWrite( pTemp, Buffer, 0, 0, 0 );
313 Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
314 i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
315 Gia_ManStop( pTemp );
316 }
317 }
318
319 // perform sequential synthesis for clock domains
320 pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
321 Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
322 {
323 pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack );
324 if ( nCountPis > 0 )
325 {
326 if ( pPars->fUseScorr )
327 {
328 Cec_ParCor_t CorPars, * pCorPars = &CorPars;
329 Cec_ManCorSetDefaultParams( pCorPars );
330 pCorPars->nBTLimit = pPars->nBTLimit;
331 pCorPars->nLevelMax = pPars->nLevelMax;
332 pCorPars->fVerbose = pPars->fVeryVerbose;
333 pCorPars->fUseCSat = 1;
334 Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
335 }
336 else if ( pPars->fUseLcorr )
337 {
338 Cec_ParCor_t CorPars, * pCorPars = &CorPars;
339 Cec_ManCorSetDefaultParams( pCorPars );
340 pCorPars->fLatchCorr = 1;
341 pCorPars->nBTLimit = pPars->nBTLimit;
342 pCorPars->fVerbose = pPars->fVeryVerbose;
343 pCorPars->fUseCSat = 1;
344 Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
345 }
346 else
347 {
348// pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
349// Gia_ManStop( pNew );
350 Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
351 }
352//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) );
353 nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs );
354 if ( pPars->fVerbose )
355 {
356 Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n",
357 i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses );
358 }
359 }
360 Gia_ManStop( pTemp );
361 ABC_FREE( pMapBack );
362 }
363
364 // generate resulting equivalences
365 Gia_ManNormalizeEquivalences( p, pReprs );
366//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) );
367 ABC_FREE( pReprs );
368 if ( pPars->fVerbose )
369 {
370 Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
371 }
372 return 1;
373}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Gia_ManNormalizeEquivalences
void Gia_ManNormalizeEquivalences(Gia_Man_t *p, int *pReprs)
Definition cecSynth.c:262
Gia_ManRegCreatePart
Gia_Man_t * Gia_ManRegCreatePart(Gia_Man_t *p, Vec_Int_t *vPart, int *pnCountPis, int *pnCountRegs, int **ppMapBack)
Definition cecSynth.c:105
Gia_TransferMappedClasses
int Gia_TransferMappedClasses(Gia_Man_t *pPart, int *pMapBack, int *pReprs)
Definition cecSynth.c:204
Cec_ManCorSetDefaultParams
void Cec_ManCorSetDefaultParams(Cec_ParCor_t *p)
Definition cecCore.c:183
Cec_ManLSCorrespondenceClasses
int Cec_ManLSCorrespondenceClasses(Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Definition cecCorr.c:924
Cec_ParCor_t
struct Cec_ParCor_t_ Cec_ParCor_t
Definition cec.h:145
Gia_ManSeqCleanupClasses
void Gia_ManSeqCleanupClasses(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition giaAig.c:676
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
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Cec_ParCor_t_::nLevelMax
int nLevelMax
Definition cec.h:155
Cec_ParCor_t_::fUseCSat
int fUseCSat
Definition cec.h:162
Cec_ParCor_t_::fLatchCorr
int fLatchCorr
Definition cec.h:158
Cec_ParCor_t_::nBTLimit
int nBTLimit
Definition cec.h:152
Cec_ParCor_t_::fVerbose
int fVerbose
Definition cec.h:168
Cec_ParSeq_t_::nLevelMax
int nLevelMax
Definition cec.h:195
Cec_ParSeq_t_::fUseScorr
int fUseScorr
Definition cec.h:192
Cec_ParSeq_t_::nBTLimit
int nBTLimit
Definition cec.h:193
Cec_ParSeq_t_::fVeryVerbose
int fVeryVerbose
Definition cec.h:200
Cec_ParSeq_t_::fUseLcorr
int fUseLcorr
Definition cec.h:191
Cec_ParSeq_t_::fVerbose
int fVerbose
Definition cec.h:201
Cec_ParSeq_t_::fEquivs
int fEquivs
Definition cec.h:197
Cec_ParSeq_t_::fConsts
int fConsts
Definition cec.h:196
sprintf
char * sprintf()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:

◆ Gia_ManFindRepr_rec()

int Gia_ManFindRepr_rec ( int * pReprs,
int Id )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file cecSynth.c.

243{
244 if ( pReprs[Id] == 0 )
245 return 0;
246 if ( pReprs[Id] == ~0 )
247 return Id;
248 return Gia_ManFindRepr_rec( pReprs, pReprs[Id] );
249}
Gia_ManFindRepr_rec
int Gia_ManFindRepr_rec(int *pReprs, int Id)
Definition cecSynth.c:242
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManNormalizeEquivalences()

void Gia_ManNormalizeEquivalences ( Gia_Man_t * p,
int * pReprs )

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

Synopsis [Normalizes equivalences.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file cecSynth.c.

263{
264 int i, iRepr;
265 assert( p->pReprs == NULL );
266 assert( p->pNexts == NULL );
267 p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
268 for ( i = 0; i < Gia_ManObjNum(p); i++ )
269 Gia_ObjSetRepr( p, i, GIA_VOID );
270 for ( i = 0; i < Gia_ManObjNum(p); i++ )
271 {
272 if ( pReprs[i] == ~0 )
273 continue;
274 iRepr = Gia_ManFindRepr_rec( pReprs, i );
275 Gia_ObjSetRepr( p, i, iRepr );
276 }
277 p->pNexts = Gia_ManDeriveNexts( p );
278}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Gia_Rpr_t
struct Gia_Rpr_t_ Gia_Rpr_t
Definition gia.h:57
Gia_ManDeriveNexts
int * Gia_ManDeriveNexts(Gia_Man_t *p)
Definition giaEquiv.c:260
GIA_VOID
#define GIA_VOID
Definition gia.h:46
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManRegCreatePart()

Gia_Man_t * Gia_ManRegCreatePart ( Gia_Man_t * p,
Vec_Int_t * vPart,
int * pnCountPis,
int * pnCountRegs,
int ** ppMapBack )

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

Synopsis [Computes partitioning of registers.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file cecSynth.c.

106{
107 Gia_Man_t * pNew;
108 Gia_Obj_t * pObj;
109 Vec_Int_t * vNodes, * vRoots;
110 int i, iOut, nCountPis, nCountRegs;
111 int * pMapBack;
112 // collect/mark nodes/PIs in the DFS order from the roots
113 Gia_ManIncrementTravId( p );
114 vRoots = Vec_IntAlloc( Vec_IntSize(vPart) );
115 Vec_IntForEachEntry( vPart, iOut, i )
116 Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) );
117 vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) );
118 Vec_IntFree( vRoots );
119 // unmark register outputs
120 Vec_IntForEachEntry( vPart, iOut, i )
121 Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) );
122 // count pure PIs
123 nCountPis = nCountRegs = 0;
124 Gia_ManForEachPi( p, pObj, i )
125 nCountPis += Gia_ObjIsTravIdCurrent(p, pObj);
126 // count outputs of other registers
127 Gia_ManForEachRo( p, pObj, i )
128 nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ???
129 if ( pnCountPis )
130 *pnCountPis = nCountPis;
131 if ( pnCountRegs )
132 *pnCountRegs = nCountRegs;
133 // clean old manager
134 Gia_ManFillValue(p);
135 Gia_ManConst0(p)->Value = 0;
136 // create the new manager
137 pNew = Gia_ManStart( Vec_IntSize(vNodes) );
138 // create the PIs
139 Gia_ManForEachCi( p, pObj, i )
140 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
141 pObj->Value = Gia_ManAppendCi(pNew);
142 // add variables for the register outputs
143 // create fake POs to hold the register outputs
144 Vec_IntForEachEntry( vPart, iOut, i )
145 {
146 pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
147 pObj->Value = Gia_ManAppendCi(pNew);
148 Gia_ManAppendCo( pNew, pObj->Value );
149 Gia_ObjSetTravIdCurrent( p, pObj ); // added
150 }
151 // create the nodes
152 Gia_ManForEachObjVec( vNodes, p, pObj, i )
153 if ( Gia_ObjIsAnd(pObj) )
154 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
155 // add real POs for the registers
156 Vec_IntForEachEntry( vPart, iOut, i )
157 {
158 pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut );
159 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
160 }
161 Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) );
162 // create map
163 if ( ppMapBack )
164 {
165 pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
166 // map constant nodes
167 pMapBack[0] = 0;
168 // logic cones of register outputs
169 Gia_ManForEachObjVec( vNodes, p, pObj, i )
170 {
171// pObjNew = Aig_Regular(pObj->pData);
172// pMapBack[pObjNew->Id] = pObj->Id;
173 assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
174 assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
175 pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
176 }
177 // map register outputs
178 Vec_IntForEachEntry( vPart, iOut, i )
179 {
180 pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
181// pObjNew = pObj->pData;
182// pMapBack[pObjNew->Id] = pObj->Id;
183 assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
184 assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
185 pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
186 }
187 *ppMapBack = pMapBack;
188 }
189 Vec_IntFree( vNodes );
190 return pNew;
191}
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
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_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManCollectNodesCis
Vec_Int_t * Gia_ManCollectNodesCis(Gia_Man_t *p, int *pNodes, int nNodes)
Definition giaDfs.c:202
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManTestOnePair()

int Gia_ManTestOnePair ( Gia_Man_t * p,
int iObj1,
int iObj2,
int fPhase )

Definition at line 403 of file cecSynth.c.

404{
405 int Lits[2] = {1}, status;
406 sat_solver * pSat = sat_solver_new();
407 Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) );
408 Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) );
409 sat_solver_addclause( pSat, Lits, Lits + 1 );
410 Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar );
411 Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar );
412 Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 );
413 Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase );
414 status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
415 if ( status == l_False )
416 {
417 Lits[0] = Abc_LitNot( Lits[0] );
418 Lits[1] = Abc_LitNot( Lits[1] );
419 status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 );
420 }
421 Vec_IntFree( vSatVar );
422 sat_solver_delete( pSat );
423 return status;
424}
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_addvar
#define sat_solver_addvar
Definition cecSatG2.c:40
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Here is the call graph for this function:

◆ Gia_TransferMappedClasses()

int Gia_TransferMappedClasses ( Gia_Man_t * pPart,
int * pMapBack,
int * pReprs )

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

Synopsis [Transfers the classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file cecSynth.c.

205{
206 Gia_Obj_t * pObj;
207 int i, Id1, Id2, nClasses;
208 if ( pPart->pReprs == NULL )
209 return 0;
210 nClasses = 0;
211 Gia_ManForEachObj( pPart, pObj, i )
212 {
213 if ( Gia_ObjRepr(pPart, i) == GIA_VOID )
214 continue;
215 assert( i < Gia_ManObjNum(pPart) );
216 assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) );
217 Id1 = pMapBack[ i ];
218 Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ];
219 if ( Id1 == Id2 )
220 continue;
221 if ( Id1 < Id2 )
222 pReprs[Id2] = Id1;
223 else
224 pReprs[Id1] = Id2;
225 nClasses++;
226 }
227 return nClasses;
228}
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition gia.h:126
Here is the caller graph for this function: