abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb1Hint.c File Reference
#include "llbInt.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Llb_ManMaxFanoutCi (Aig_Man_t *pAig)
 DECLARATIONS ///. More...
 
Aig_Man_tLlb_ManPerformHints (Aig_Man_t *pAig, int nHintDepth)
 
Vec_Int_tLlb_ManCollectHighFanoutObjects (Aig_Man_t *pAig, int nCandMax, int fCisOnly)
 
int Llb_ManModelCheckAigWithHints (Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars)
 

Function Documentation

Vec_Int_t* Llb_ManCollectHighFanoutObjects ( Aig_Man_t pAig,
int  nCandMax,
int  fCisOnly 
)

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

Synopsis [Returns CI index with the largest number of fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file llb1Hint.c.

97 {
98  Vec_Int_t * vFanouts, * vResult;
99  Aig_Obj_t * pObj;
100  int i, fChanges, PivotValue;
101 // int Entry;
102  // collect fanout counts
103  vFanouts = Vec_IntAlloc( 100 );
104  Aig_ManForEachObj( pAig, pObj, i )
105  {
106 // if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
107  if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
108  continue;
109  Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) );
110  }
111  Vec_IntSort( vFanouts, 1 );
112  // pick the separator
113  nCandMax = Abc_MinInt( nCandMax, Vec_IntSize(vFanouts) - 1 );
114  PivotValue = Vec_IntEntry( vFanouts, nCandMax );
115  Vec_IntFree( vFanouts );
116  // collect obj satisfying the constraints
117  vResult = Vec_IntAlloc( 100 );
118  Aig_ManForEachObj( pAig, pObj, i )
119  {
120 // if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
121  if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
122  continue;
123  if ( Aig_ObjRefs(pObj) < PivotValue )
124  continue;
125  Vec_IntPush( vResult, Aig_ObjId(pObj) );
126  }
127  assert( Vec_IntSize(vResult) >= nCandMax );
128  // order in the decreasing order of fanouts
129  do
130  {
131  fChanges = 0;
132  for ( i = 0; i < Vec_IntSize(vResult) - 1; i++ )
133  if ( Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i))) <
134  Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i+1))) )
135  {
136  int Temp = Vec_IntEntry( vResult, i );
137  Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vResult, i+1) );
138  Vec_IntWriteEntry( vResult, i+1, Temp );
139  fChanges = 1;
140  }
141  }
142  while ( fChanges );
143 /*
144  Vec_IntForEachEntry( vResult, Entry, i )
145  printf( "%d ", Aig_ObjRefs(Aig_ManObj(pAig, Entry)) );
146 printf( "\n" );
147 */
148  return vResult;
149 }
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_NAMESPACE_IMPL_START int Llb_ManMaxFanoutCi ( Aig_Man_t pAig)

DECLARATIONS ///.

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

FileName [llb1Hint.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Cofactors the circuit w.r.t. the high-fanout variables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Returns CI index with the largest number of fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file llb1Hint.c.

46 {
47  Aig_Obj_t * pObj;
48  int i, WeightMax = -ABC_INFINITY, iInput = -1;
49  Aig_ManForEachCi( pAig, pObj, i )
50  if ( WeightMax < Aig_ObjRefs(pObj) )
51  {
52  WeightMax = Aig_ObjRefs(pObj);
53  iInput = i;
54  }
55  assert( iInput >= 0 );
56  return iInput;
57 }
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
int Llb_ManModelCheckAigWithHints ( Aig_Man_t pAigGlo,
Gia_ParLlb_t pPars 
)

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

Synopsis [Derives AIG whose PI is substituted by a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file llb1Hint.c.

163 {
164  DdManager * ddGlo = NULL;
165  Vec_Int_t * vHints;
166  Vec_Int_t * vHFCands;
167  int i, Entry, RetValue = -1;
168  abctime clk = Abc_Clock();
169  assert( pPars->nHintDepth > 0 );
170 /*
171  // perform reachability without hints
172  RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL );
173  if ( RetValue >= 0 )
174  return RetValue;
175 */
176  // create hints representation
177  vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 );
178  vHints = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) );
179  // add one hint at a time till the problem is solved
180  Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst )
181  {
182  Vec_IntWriteEntry( vHints, Entry, 1 ); // change to 1 to start from zero cof!!!
183  // solve under hints
184  RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
185  if ( RetValue == 0 )
186  goto Finish;
187  if ( RetValue == 1 )
188  break;
189  }
190  if ( RetValue == -1 )
191  goto Finish;
192  // undo the hints one at a time
193  for ( ; i >= pPars->HintFirst; i-- )
194  {
195  Entry = Vec_IntEntry( vHFCands, i );
196  Vec_IntWriteEntry( vHints, Entry, -1 );
197  // solve under relaxed hints
198  RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
199  if ( RetValue == 0 )
200  goto Finish;
201  if ( RetValue == 1 )
202  continue;
203  break;
204  }
205 Finish:
206  if ( ddGlo )
207  {
208  if ( ddGlo->bFunc )
209  Cudd_RecursiveDeref( ddGlo, ddGlo->bFunc );
210  Extra_StopManager( ddGlo );
211  }
212  Vec_IntFreeP( &vHFCands );
213  Vec_IntFreeP( &vHints );
214  if ( pPars->fVerbose )
215  Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk );
216  return RetValue;
217 }
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
DdNode * bFunc
Definition: cuddInt.h:487
static abctime Abc_Clock()
Definition: abc_global.h:279
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_Int_t * Llb_ManCollectHighFanoutObjects(Aig_Man_t *pAig, int nCandMax, int fCisOnly)
Definition: llb1Hint.c:96
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int Llb_ManModelCheckAig(Aig_Man_t *pAigGlo, Gia_ParLlb_t *pPars, Vec_Int_t *vHints, DdManager **pddGlo)
Definition: llb1Core.c:112
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
Aig_Man_t* Llb_ManPerformHints ( Aig_Man_t pAig,
int  nHintDepth 
)

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

Synopsis [Derives AIG whose PI is substituted by a constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file llb1Hint.c.

71 {
72  Aig_Man_t * pNew, * pTemp;
73  int i, iInput;
74  pNew = Aig_ManDupDfs( pAig );
75  for ( i = 0; i < nHintDepth; i++ )
76  {
77  iInput = Llb_ManMaxFanoutCi( pNew );
78  Abc_Print( 1, "%d %3d\n", i, iInput );
79  pNew = Aig_ManDupCof( pTemp = pNew, iInput, 1 );
80  Aig_ManStop( pTemp );
81  }
82  return pNew;
83 }
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition: aigDup.c:563
ABC_NAMESPACE_IMPL_START int Llb_ManMaxFanoutCi(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: llb1Hint.c:45
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Aig_Man_t * Aig_ManDupCof(Aig_Man_t *p, int iInput, int Value)
Definition: aigDup.c:345