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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Ssw_Man_t * Ssw_ManCreate (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
 DECLARATIONS ///.
 
int Ssw_ManCountEquivs (Ssw_Man_t *p)
 
void Ssw_ManPrintStats (Ssw_Man_t *p)
 
void Ssw_ManCleanup (Ssw_Man_t *p)
 
void Ssw_ManStop (Ssw_Man_t *p)
 

Function Documentation

◆ Ssw_ManCleanup()

void Ssw_ManCleanup ( Ssw_Man_t * p)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file sswMan.c.

159{
160// Aig_ManCleanMarkAB( p->pAig );
161 assert( p->pMSat == NULL );
162 if ( p->pFrames )
163 {
164 Aig_ManCleanMarkAB( p->pFrames );
165 Aig_ManStop( p->pFrames );
166 p->pFrames = NULL;
167 memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
168 }
169 if ( p->vSimInfo )
170 {
171 Vec_PtrFree( p->vSimInfo );
172 p->vSimInfo = NULL;
173 }
174 p->nConstrTotal = 0;
175 p->nConstrReduced = 0;
176}
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
p
Cube * p
Definition exorList.c:222
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ManCountEquivs()

int Ssw_ManCountEquivs ( Ssw_Man_t * p)

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

Synopsis [Prints stats of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file sswMan.c.

85{
86 Aig_Obj_t * pObj;
87 int i, nEquivs = 0;
88 Aig_ManForEachObj( p->pAig, pObj, i )
89 nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL );
90 return nEquivs;
91}
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Here is the caller graph for this function:

◆ Ssw_ManCreate()

ABC_NAMESPACE_IMPL_START Ssw_Man_t * Ssw_ManCreate ( Aig_Man_t * pAig,
Ssw_Pars_t * pPars )

DECLARATIONS ///.

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

FileName [sswMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id
sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Creates the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswMan.c.

46{
47 Ssw_Man_t * p;
48 // prepare the sequential AIG
49 assert( Saig_ManRegNum(pAig) > 0 );
50 Aig_ManFanoutStart( pAig );
51 Aig_ManSetCioIds( pAig );
52 // create interpolation manager
53 p = ABC_ALLOC( Ssw_Man_t, 1 );
54 memset( p, 0, sizeof(Ssw_Man_t) );
55 p->pPars = pPars;
56 p->pAig = pAig;
57 p->nFrames = pPars->nFramesK + 1;
58 p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
59 p->vCommon = Vec_PtrAlloc( 100 );
60 p->iOutputLit = -1;
61 // allocate storage for sim pattern
62 p->nPatWords = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
63 p->pPatWords = ABC_CALLOC( unsigned, p->nPatWords );
64 // other
65 p->vNewLos = Vec_PtrAlloc( 100 );
66 p->vNewPos = Vec_IntAlloc( 100 );
67 p->vResimConsts = Vec_PtrAlloc( 100 );
68 p->vResimClasses = Vec_PtrAlloc( 100 );
69// p->pPars->fVerbose = 1;
70 return p;
71}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition aigFanout.c:56
Aig_ManSetCioIds
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition aigUtil.c:978
Ssw_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition sswInt.h:47
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ManPrintStats()

void Ssw_ManPrintStats ( Ssw_Man_t * p)

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

Synopsis [Prints stats of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file sswMan.c.

105{
106 double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
107
108 Abc_Print( 1, "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f MB.\n",
109 p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, Saig_ManConstrNum(p->pAig), p->pPars->nMaxLevs, nMemory );
110 Abc_Print( 1, "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
111 Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
112 0/(p->pPars->nIters+1) );
113 Abc_Print( 1, "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n",
114 p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
115 Abc_Print( 1, "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n",
116 p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
117 Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
118 p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
119 p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
120
121 p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
122 ABC_PRTP( "BMC ", p->timeBmc, p->timeTotal );
123 ABC_PRTP( "Spec reduce", p->timeReduce, p->timeTotal );
124 ABC_PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
125 ABC_PRTP( "Sim SAT ", p->timeSimSat, p->timeTotal );
126 ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal );
127 ABC_PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
128 ABC_PRTP( " sat ", p->timeSatSat, p->timeTotal );
129 ABC_PRTP( " undecided", p->timeSatUndec, p->timeTotal );
130 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
131 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
132
133 // report the reductions
134 if ( p->pAig->nConstrs )
135 {
136 Abc_Print( 1, "Statistics reflecting the use of constraints:\n" );
137 Abc_Print( 1, "Total cones = %6d. Constraint cones = %6d. (%6.2f %%)\n",
138 p->nConesTotal, p->nConesConstr, 100.0*p->nConesConstr/p->nConesTotal );
139 Abc_Print( 1, "Total equivs = %6d. Removed equivs = %6d. (%6.2f %%)\n",
140 p->nEquivsTotal, p->nEquivsConstr, 100.0*p->nEquivsConstr/p->nEquivsTotal );
141 Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
142 p->nNodesBegC, p->nNodesEndC, 100.0*(p->nNodesBegC-p->nNodesEndC)/(p->nNodesBegC?p->nNodesBegC:1),
143 p->nRegsBegC, p->nRegsEndC, 100.0*(p->nRegsBegC-p->nRegsEndC)/(p->nRegsBegC?p->nRegsBegC:1) );
144 }
145}
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Ssw_ManCountEquivs
int Ssw_ManCountEquivs(Ssw_Man_t *p)
Definition sswMan.c:84
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_ManStop()

void Ssw_ManStop ( Ssw_Man_t * p)

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswMan.c.

190{
191 ABC_FREE( p->pVisited );
192 if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 )
193 Ssw_ManPrintStats( p );
194 if ( p->ppClasses )
195 Ssw_ClassesStop( p->ppClasses );
196 if ( p->pSml )
197 Ssw_SmlStop( p->pSml );
198 if ( p->vDiffPairs )
199 Vec_IntFree( p->vDiffPairs );
200 if ( p->vInits )
201 Vec_IntFree( p->vInits );
202 Vec_PtrFree( p->vResimConsts );
203 Vec_PtrFree( p->vResimClasses );
204 Vec_PtrFree( p->vNewLos );
205 Vec_IntFree( p->vNewPos );
206 Vec_PtrFree( p->vCommon );
207 ABC_FREE( p->pNodeToFrames );
208 ABC_FREE( p->pPatWords );
209 ABC_FREE( p );
210}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Ssw_ClassesStop
void Ssw_ClassesStop(Ssw_Cla_t *p)
Definition sswClass.c:189
Ssw_ManPrintStats
void Ssw_ManPrintStats(Ssw_Man_t *p)
Definition sswMan.c:104
Ssw_SmlStop
void Ssw_SmlStop(Ssw_Sml_t *p)
Definition sswSim.c:1211
Here is the call graph for this function:
Here is the caller graph for this function: