ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Typedefs | Functions
aigJust.c File Reference
#include "aig.h"
Include dependency graph for aigJust.c:

Go to the source code of this file.

Macros

#define AIG_VAL0   1
 DECLARATIONS ///.
 
#define AIG_VAL1   2
 
#define AIG_VALX   3
 

Typedefs

typedef struct Aig_ManPack_t_ Aig_ManPack_t
 

Functions

int Aig_NtkFindSatAssign_rec (Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits, int Heur)
 
int Aig_ObjFindSatAssign (Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits)
 
int Aig_ObjTerSimulate_rec (Aig_Man_t *pAig, Aig_Obj_t *pNode)
 
int Aig_ObjTerSimulate (Aig_Man_t *pAig, Aig_Obj_t *pNode, Vec_Int_t *vSuppLits)
 
Aig_ManPack_t * Aig_ManPackStart (Aig_Man_t *pAig)
 
void Aig_ManPackStop (Aig_ManPack_t *p)
 
void Aig_ManPackAddPattern (Aig_ManPack_t *p, Vec_Int_t *vLits)
 
Vec_Int_t * Aig_ManPackConstNodes (Aig_ManPack_t *p)
 
void Aig_ManJustExperiment (Aig_Man_t *pAig)
 

Macro Definition Documentation

◆ AIG_VAL0

#define AIG_VAL0   1

DECLARATIONS ///.

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

FileName [aigJust.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Justification of node values.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
aigJust.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 30 of file aigJust.c.

◆ AIG_VAL1

#define AIG_VAL1   2

Definition at line 31 of file aigJust.c.

◆ AIG_VALX

#define AIG_VALX   3

Definition at line 32 of file aigJust.c.

Typedef Documentation

◆ Aig_ManPack_t

typedef struct Aig_ManPack_t_ Aig_ManPack_t

Definition at line 234 of file aigJust.c.

Function Documentation

◆ Aig_ManJustExperiment()

void Aig_ManJustExperiment ( Aig_Man_t * pAig)

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

Synopsis [Testing of the framework.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file aigJust.c.

252{
253 Aig_ManPack_t * pPack;
254 Vec_Int_t * vSuppLits, * vNodes;
255 Aig_Obj_t * pObj;
256 int i;
257 abctime clk = Abc_Clock();
258 int Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
259 int nTotalLits = 0;
260 vSuppLits = Vec_IntAlloc( 100 );
261 pPack = Aig_ManPackStart( pAig );
262 vNodes = Aig_ManPackConstNodes( pPack );
263// Aig_ManForEachCo( pAig, pObj, i )
264 Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
265 {
266 if ( pObj->fPhase ) // const 1
267 {
268 if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) )
269 {
270// assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 );
271// if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
272// printf( "Justification error!\n" );
273 Count0++;
274 nTotalLits += Vec_IntSize(vSuppLits);
275 Aig_ManPackAddPattern( pPack, vSuppLits );
276 }
277 else
278 Count0f++;
279 }
280 else
281 {
282 if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) )
283 {
284// assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 );
285// if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
286// printf( "Justification error!\n" );
287 Count1++;
288 nTotalLits += Vec_IntSize(vSuppLits);
289 Aig_ManPackAddPattern( pPack, vSuppLits );
290 }
291 else
292 Count1f++;
293 }
294 }
295 Vec_IntFree( vSuppLits );
296 printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ",
297 Aig_ManCoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManCoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
298 Abc_PrintTime( 1, "T", Abc_Clock() - clk );
299 Aig_ManCleanMarkAB( pAig );
300 Aig_ManPackStop( pPack );
301 Vec_IntFree( vNodes );
302}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Aig_ObjFindSatAssign
int Aig_ObjFindSatAssign(Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits)
Definition aigJust.c:162
Aig_ManPack_t
struct Aig_ManPack_t_ Aig_ManPack_t
Definition aigJust.c:234
Aig_ManPackConstNodes
Vec_Int_t * Aig_ManPackConstNodes(Aig_ManPack_t *p)
Definition aigPack.c:264
Aig_ManPackStop
void Aig_ManPackStop(Aig_ManPack_t *p)
Definition aigPack.c:391
Aig_ManPackStart
Aig_ManPack_t * Aig_ManPackStart(Aig_Man_t *pAig)
Definition aigPack.c:370
Aig_ManPackAddPattern
void Aig_ManPackAddPattern(Aig_ManPack_t *p, Vec_Int_t *vLits)
Definition aigPack.c:326
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
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
Here is the call graph for this function:

◆ Aig_ManPackAddPattern()

void Aig_ManPackAddPattern ( Aig_ManPack_t * p,
Vec_Int_t * vLits )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file aigPack.c.

327{
328 int k;
329 for ( k = 1; k < 64; k++ )
330 if ( Aig_ManPackAddPatternTry( p, k, vLits ) )
331 break;
332 if ( k == 64 )
333 {
334/*
335 word * pInfo, * pPres;
336 int i, Lit;
337 Vec_IntForEachEntry( vLits, Lit, i )
338 printf( "%d", Abc_LitIsCompl(Lit) );
339 printf( "\n\n" );
340 for ( k = 1; k < 64; k++ )
341 {
342 Vec_IntForEachEntry( vLits, Lit, i )
343 {
344 pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
345 pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
346 if ( Abc_InfoHasBit( (unsigned *)pPres, k ) )
347 printf( "%d", Abc_InfoHasBit( (unsigned *)pInfo, k ) );
348 else
349 printf( "-" );
350 }
351 printf( "\n" );
352 }
353*/
354 p->nPatSkip++;
355 }
356 p->nPatTotal++;
357}
Aig_ManPackAddPatternTry
int Aig_ManPackAddPatternTry(Aig_ManPack_t *p, int iBit, Vec_Int_t *vLits)
Definition aigPack.c:292
p
Cube * p
Definition exorList.c:222
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_ManPackConstNodes()

Vec_Int_t * Aig_ManPackConstNodes ( Aig_ManPack_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file aigPack.c.

265{
266 Vec_Int_t * vNodes;
267 Aig_Obj_t * pObj;
268 word Sign;
269 int i;
270 vNodes = Vec_IntAlloc( 1000 );
271 Aig_ManForEachNode( p->pAig, pObj, i )
272 {
273 Sign = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) );
274 if ( Sign == 0 || ~Sign == 0 || Aig_Word6HasOneBit(Sign) || Aig_Word6HasOneBit(~Sign) )
275 Vec_IntPush( vNodes, Aig_ObjId(pObj) );
276 }
277 return vNodes;
278}
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Here is the caller graph for this function:

◆ Aig_ManPackStart()

Aig_ManPack_t * Aig_ManPackStart ( Aig_Man_t * pAig)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file aigPack.c.

371{
372 Aig_ManPack_t * p;
373 p = Aig_ManPackAlloc( pAig );
374 Aig_ManPackSetRandom( p );
375 Aig_ManPackSimulate( p );
376 Aig_ManPackPrintStats( p );
377 return p;
378}
Aig_ManPackAlloc
Aig_ManPack_t * Aig_ManPackAlloc(Aig_Man_t *pAig)
FUNCTION DEFINITIONS ///.
Definition aigPack.c:65
Aig_ManPackSetRandom
void Aig_ManPackSetRandom(Aig_ManPack_t *p)
Definition aigPack.c:159
Aig_ManPackPrintStats
void Aig_ManPackPrintStats(Aig_ManPack_t *p)
Definition aigPack.c:227
Aig_ManPackSimulate
void Aig_ManPackSimulate(Aig_ManPack_t *p)
Definition aigPack.c:182
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_ManPackStop()

void Aig_ManPackStop ( Aig_ManPack_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 391 of file aigPack.c.

392{
393 Aig_ManPackSimulate( p );
394 Aig_ManPackPrintStats( p );
395 Aig_ManPackFree( p );
396}
Aig_ManPackFree
void Aig_ManPackFree(Aig_ManPack_t *p)
Definition aigPack.c:134
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_NtkFindSatAssign_rec()

int Aig_NtkFindSatAssign_rec ( Aig_Man_t * pAig,
Aig_Obj_t * pNode,
int Value,
Vec_Int_t * vSuppLits,
int Heur )

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

Synopsis [Recursively searched for a satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file aigJust.c.

103{
104 int Value0, Value1;
105// ++Heur;
106 if ( Aig_ObjIsConst1(pNode) )
107 return 1;
108 if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
109 return ((int)pNode->fMarkA == Value);
110 Aig_ObjSetTravIdCurrent(pAig, pNode);
111 pNode->fMarkA = Value;
112 if ( Aig_ObjIsCi(pNode) )
113 {
114// if ( Aig_ObjId(pNode) % 1000 == 0 )
115// Value ^= 1;
116 if ( vSuppLits )
117 Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
118 return 1;
119 }
120 assert( Aig_ObjIsNode(pNode) );
121 // propagation
122 if ( Value )
123 {
124 if ( !Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), vSuppLits, Heur) )
125 return 0;
126 return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), vSuppLits, Heur);
127 }
128 // justification
129 Value0 = Aig_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
130 if ( Value0 == AIG_VAL0 )
131 return 1;
132 Value1 = Aig_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
133 if ( Value1 == AIG_VAL0 )
134 return 1;
135 if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
136 return 0;
137 if ( Value0 == AIG_VAL1 )
138 return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
139 if ( Value1 == AIG_VAL1 )
140 return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
141 assert( Value0 == AIG_VALX && Value1 == AIG_VALX );
142 // decision making
143// if ( rand() % 10 == Heur )
144// if ( Aig_ObjId(pNode) % 8 == Heur )
145 if ( ++Heur % 8 == 0 )
146 return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
147 else
148 return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
149}
Aig_NtkFindSatAssign_rec
int Aig_NtkFindSatAssign_rec(Aig_Man_t *pAig, Aig_Obj_t *pNode, int Value, Vec_Int_t *vSuppLits, int Heur)
Definition aigJust.c:102
AIG_VALX
#define AIG_VALX
Definition aigJust.c:32
AIG_VAL1
#define AIG_VAL1
Definition aigJust.c:31
AIG_VAL0
#define AIG_VAL0
DECLARATIONS ///.
Definition aigJust.c:30
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
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:

◆ Aig_ObjFindSatAssign()

int Aig_ObjFindSatAssign ( Aig_Man_t * pAig,
Aig_Obj_t * pNode,
int Value,
Vec_Int_t * vSuppLits )

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

Synopsis [Returns 1 if SAT assignment is found; 0 otherwise.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file aigJust.c.

163{
164 int i;
165 if ( Aig_ObjIsCo(pNode) )
166 return Aig_ObjFindSatAssign( pAig, Aig_ObjFanin0(pNode), Value ^ Aig_ObjFaninC0(pNode), vSuppLits );
167 for ( i = 0; i < 8; i++ )
168 {
169 Vec_IntClear( vSuppLits );
170 Aig_ManIncrementTravId( pAig );
171 if ( Aig_NtkFindSatAssign_rec( pAig, pNode, Value, vSuppLits, i ) )
172 return 1;
173 }
174 return 0;
175}
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Aig_ObjTerSimulate()

int Aig_ObjTerSimulate ( Aig_Man_t * pAig,
Aig_Obj_t * pNode,
Vec_Int_t * vSuppLits )

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

Synopsis [Returns value of the object under input assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 217 of file aigJust.c.

218{
219 Aig_Obj_t * pObj;
220 int i, Entry;
221 Aig_ManIncrementTravId( pAig );
222 Vec_IntForEachEntry( vSuppLits, Entry, i )
223 {
224 pObj = Aig_ManCi( pAig, Abc_Lit2Var(Entry) );
225 Aig_ObjSetTerValue( pObj, Abc_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
226 Aig_ObjSetTravIdCurrent( pAig, pObj );
227//printf( "%d ", Entry );
228 }
229//printf( "\n" );
230 return Aig_ObjTerSimulate_rec( pAig, pNode );
231}
Aig_ObjTerSimulate_rec
int Aig_ObjTerSimulate_rec(Aig_Man_t *pAig, Aig_Obj_t *pNode)
Definition aigJust.c:188
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:

◆ Aig_ObjTerSimulate_rec()

int Aig_ObjTerSimulate_rec ( Aig_Man_t * pAig,
Aig_Obj_t * pNode )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file aigJust.c.

189{
190 int Value0, Value1;
191 if ( Aig_ObjIsConst1(pNode) )
192 return AIG_VAL1;
193 if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
194 return Aig_ObjGetTerValue( pNode );
195 Aig_ObjSetTravIdCurrent( pAig, pNode );
196 if ( Aig_ObjIsCi(pNode) )
197 return Aig_ObjSetTerValue( pNode, AIG_VALX );
198 Value0 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin0(pNode)), Aig_ObjFaninC0(pNode) );
199 if ( Aig_ObjIsCo(pNode) || Value0 == AIG_VAL0 )
200 return Aig_ObjSetTerValue( pNode, Value0 );
201 assert( Aig_ObjIsNode(pNode) );
202 Value1 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin1(pNode)), Aig_ObjFaninC1(pNode) );
203 return Aig_ObjSetTerValue( pNode, Aig_ObjAndTerValue(Value0, Value1) );
204}
Here is the call graph for this function:
Here is the caller graph for this function: