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

Go to the source code of this file.

Functions

static ABC_NAMESPACE_IMPL_START int Fra_RegToLit (int n, int c)
 DECLARATIONS ///. More...
 
static int Fra_LitReg (int n)
 
static int Fra_LitSign (int n)
 
int Fra_OneHotNodeIsConst (Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
 FUNCTION DEFINITIONS ///. More...
 
int Fra_OneHotNodesAreEqual (Fra_Sml_t *pSeq, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
int Fra_OneHotNodesAreClause (Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2, int fCompl1, int fCompl2)
 
Vec_Int_t * Fra_OneHotCompute (Fra_Man_t *p, Fra_Sml_t *pSim)
 
void Fra_OneHotAssume (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
void Fra_OneHotCheck (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
int Fra_OneHotRefineUsingCex (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
int Fra_OneHotCount (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
void Fra_OneHotEstimateCoverage (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
Aig_Man_t * Fra_OneHotCreateExdc (Fra_Man_t *p, Vec_Int_t *vOneHots)
 
void Fra_OneHotAddKnownConstraint (Fra_Man_t *p, Vec_Ptr_t *vOnehots)
 

Function Documentation

static int Fra_LitReg ( int  n)
inlinestatic

Definition at line 31 of file fraHot.c.

31 { return (n>0)? n-1 : -n-1; }
static int Fra_LitSign ( int  n)
inlinestatic

Definition at line 32 of file fraHot.c.

32 { return (n<0); }
void Fra_OneHotAddKnownConstraint ( Fra_Man_t *  p,
Vec_Ptr_t *  vOnehots 
)

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file fraHot.c.

440 {
441  Vec_Int_t * vGroup;
442  Aig_Obj_t * pObj1, * pObj2;
443  int k, i, j, Out1, Out2, pLits[2];
444  //
445  // these constrants should be added to different timeframes!
446  // (also note that PIs follow first - then registers)
447  //
448  Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, k )
449  {
450  Vec_IntForEachEntry( vGroup, Out1, i )
451  Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
452  {
453  pObj1 = Aig_ManCi( p->pManFraig, Out1 );
454  pObj2 = Aig_ManCi( p->pManFraig, Out2 );
455  pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
456  pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
457  // add constraint to solver
458  if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
459  {
460  printf( "Fra_OneHotAddKnownConstraint(): Adding clause makes SAT solver unsat.\n" );
461  sat_solver_delete( p->pSat );
462  p->pSat = NULL;
463  return;
464  }
465  }
466  }
467 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Aig_Obj_t_
Definition: aig.h:69
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Fra_OneHotAssume ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Assumes one-hot implications in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fraHot.c.

192 {
193  Aig_Obj_t * pObj1, * pObj2;
194  int i, Out1, Out2, pLits[2];
195  int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
196  assert( p->pPars->nFramesK == 1 ); // add to only one frame
197  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
198  {
199  Out1 = Vec_IntEntry( vOneHots, i );
200  Out2 = Vec_IntEntry( vOneHots, i+1 );
201  if ( Out1 == 0 && Out2 == 0 )
202  continue;
203  pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
204  pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
205  pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
206  pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
207  // add constraint to solver
208  if ( !sat_solver_addclause( p->pSat, pLits, pLits + 2 ) )
209  {
210  printf( "Fra_OneHotAssume(): Adding clause makes SAT solver unsat.\n" );
211  sat_solver_delete( p->pSat );
212  p->pSat = NULL;
213  return;
214  }
215  }
216 }
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Fra_Man_t_::pPars
Fra_Par_t * pPars
Definition: fra.h:189
Fra_Man_t_::pSat
sat_solver * pSat
Definition: fra.h:210
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Fra_ObjSatNum
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
assert
#define assert(ex)
Definition: util_old.h:213
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
void Fra_OneHotCheck ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Checks one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file fraHot.c.

230 {
231  Aig_Obj_t * pObj1, * pObj2;
232  int RetValue, i, Out1, Out2;
233  int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
234  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
235  {
236  Out1 = Vec_IntEntry( vOneHots, i );
237  Out2 = Vec_IntEntry( vOneHots, i+1 );
238  if ( Out1 == 0 && Out2 == 0 )
239  continue;
240  pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
241  pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
242  RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
243  if ( RetValue != 1 )
244  {
245  p->pCla->fRefinement = 1;
246  if ( RetValue == 0 )
247  Fra_SmlResimulate( p );
248  if ( Vec_IntEntry(vOneHots, i) != 0 )
249  printf( "Fra_OneHotCheck(): Clause is not refined!\n" );
250  assert( Vec_IntEntry(vOneHots, i) == 0 );
251  }
252  }
253 }
Fra_Cla_t_::fRefinement
int fRefinement
Definition: fra.h:162
Fra_Man_t_::pCla
Fra_Cla_t * pCla
Definition: fra.h:198
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Fra_Man_t_::pManFraig
Aig_Man_t * pManFraig
Definition: fra.h:192
Fra_NodesAreClause
int Fra_NodesAreClause(Fra_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew, int fComplL, int fComplR)
Definition: fraSat.c:317
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Aig_Obj_t_
Definition: aig.h:69
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Fra_SmlResimulate
void Fra_SmlResimulate(Fra_Man_t *p)
Definition: fraSim.c:703
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
Vec_Int_t* Fra_OneHotCompute ( Fra_Man_t *  p,
Fra_Sml_t *  pSim 
)

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

Synopsis [Computes one-hot implications.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fraHot.c.

135 {
136  int fSkipConstEqu = 1;
137  Vec_Int_t * vOneHots;
138  Aig_Obj_t * pObj1, * pObj2;
139  int i, k;
140  int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
141  assert( pSim->pAig == p->pManAig );
142  vOneHots = Vec_IntAlloc( 100 );
143  Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
144  {
145  if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj1) )
146  continue;
147  assert( i-nTruePis >= 0 );
148 // Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
149 // Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
150  Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
151  {
152  if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
153  continue;
154  if ( fSkipConstEqu && Fra_OneHotNodesAreEqual( pSim, pObj1, pObj2 ) )
155  continue;
156  assert( k-nTruePis >= 0 );
157  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 1 ) )
158  {
159  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
160  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
161  continue;
162  }
163  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 0, 1 ) )
164  {
165  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 0) );
166  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 1) );
167  continue;
168  }
169  if ( Fra_OneHotNodesAreClause( pSim, pObj1, pObj2, 1, 0 ) )
170  {
171  Vec_IntPush( vOneHots, Fra_RegToLit(i-nTruePis, 1) );
172  Vec_IntPush( vOneHots, Fra_RegToLit(k-nTruePis, 0) );
173  continue;
174  }
175  }
176  }
177  return vOneHots;
178 }
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
Fra_Sml_t_::pAig
Aig_Man_t * pAig
Definition: fra.h:173
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Fra_OneHotNodesAreClause
int Fra_OneHotNodesAreClause(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2, int fCompl1, int fCompl2)
Definition: fraHot.c:94
Fra_RegToLit
static ABC_NAMESPACE_IMPL_START int Fra_RegToLit(int n, int c)
DECLARATIONS ///.
Definition: fraHot.c:30
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Fra_OneHotNodesAreEqual
int Fra_OneHotNodesAreEqual(Fra_Sml_t *pSeq, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition: fraHot.c:71
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_ManForEachLoSeq
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
assert
#define assert(ex)
Definition: util_old.h:213
Fra_OneHotNodeIsConst
int Fra_OneHotNodeIsConst(Fra_Sml_t *pSeq, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: fraHot.c:49
int Fra_OneHotCount ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 303 of file fraHot.c.

304 {
305  int i, Out1, Out2, Counter = 0;
306  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
307  {
308  Out1 = Vec_IntEntry( vOneHots, i );
309  Out2 = Vec_IntEntry( vOneHots, i+1 );
310  if ( Out1 == 0 && Out2 == 0 )
311  continue;
312  Counter++;
313  }
314  return Counter;
315 }
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Man_t* Fra_OneHotCreateExdc ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Creates one-hotness EXDC.]

Description []

SideEffects []

SeeAlso []

Definition at line 398 of file fraHot.c.

399 {
400  Aig_Man_t * pNew;
401  Aig_Obj_t * pObj1, * pObj2, * pObj;
402  int i, Out1, Out2, nTruePis;
403  pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
404 // for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
405 // Aig_ObjCreateCi(pNew);
406  Aig_ManForEachCi( p->pManAig, pObj, i )
407  Aig_ObjCreateCi(pNew);
408  nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
409  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
410  {
411  Out1 = Vec_IntEntry( vOneHots, i );
412  Out2 = Vec_IntEntry( vOneHots, i+1 );
413  if ( Out1 == 0 && Out2 == 0 )
414  continue;
415  pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
416  pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
417  pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
418  pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
419  pObj = Aig_Or( pNew, pObj1, pObj2 );
420  Aig_ObjCreateCo( pNew, pObj );
421  }
422  Aig_ManCleanup(pNew);
423 // printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
424  return pNew;
425 }
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
for
for(p=first;p->value< newval;p=p->next)
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Aig_Obj_t_
Definition: aig.h:69
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_NotCond
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
void Fra_OneHotEstimateCoverage ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Estimates the coverage of state space by clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file fraHot.c.

329 {
330  int nSimWords = (1<<14);
331  int nRegs = Aig_ManRegNum(p->pManAig);
332  Vec_Ptr_t * vSimInfo;
333  unsigned * pSim1, * pSim2, * pSimTot;
334  int i, w, Out1, Out2, nCovered, Counter = 0;
335  abctime clk = Abc_Clock();
336 
337  // generate random sim-info at register outputs
338  vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
339 // srand( 0xAABBAABB );
340  Aig_ManRandom(1);
341  for ( i = 0; i < nRegs; i++ )
342  {
343  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, i );
344  for ( w = 0; w < nSimWords; w++ )
345  pSim1[w] = Fra_ObjRandomSim();
346  }
347  pSimTot = (unsigned *)Vec_PtrEntry( vSimInfo, nRegs );
348 
349  // collect simulation info
350  memset( pSimTot, 0, sizeof(unsigned) * nSimWords );
351  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
352  {
353  Out1 = Vec_IntEntry( vOneHots, i );
354  Out2 = Vec_IntEntry( vOneHots, i+1 );
355  if ( Out1 == 0 && Out2 == 0 )
356  continue;
357 //printf( "(%c%d,%c%d) ",
358 //Fra_LitSign(Out1)? '-': '+', Fra_LitReg(Out1),
359 //Fra_LitSign(Out2)? '-': '+', Fra_LitReg(Out2) );
360  Counter++;
361  pSim1 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out1) );
362  pSim2 = (unsigned *)Vec_PtrEntry( vSimInfo, Fra_LitReg(Out2) );
363  if ( Fra_LitSign(Out1) && Fra_LitSign(Out2) )
364  for ( w = 0; w < nSimWords; w++ )
365  pSimTot[w] |= pSim1[w] & pSim2[w];
366  else if ( Fra_LitSign(Out1) )
367  for ( w = 0; w < nSimWords; w++ )
368  pSimTot[w] |= pSim1[w] & ~pSim2[w];
369  else if ( Fra_LitSign(Out2) )
370  for ( w = 0; w < nSimWords; w++ )
371  pSimTot[w] |= ~pSim1[w] & pSim2[w];
372  else
373  assert( 0 );
374  }
375 //printf( "\n" );
376  // count the total number of patterns contained in the don't-care
377  nCovered = 0;
378  for ( w = 0; w < nSimWords; w++ )
379  nCovered += Aig_WordCountOnes( pSimTot[w] );
380  Vec_PtrFree( vSimInfo );
381  // print the result
382  printf( "Care states ratio = %f. ", 1.0 * (nSimWords * 32 - nCovered) / (nSimWords * 32) );
383  printf( "(%d out of %d patterns) ", nSimWords * 32 - nCovered, nSimWords * 32 );
384  ABC_PRT( "Time", Abc_Clock() - clk );
385 }
memset
char * memset()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Fra_ObjRandomSim
static unsigned Fra_ObjRandomSim()
Definition: fra.h:258
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
assert
#define assert(ex)
Definition: util_old.h:213
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Fra_OneHotNodeIsConst ( Fra_Sml_t *  pSeq,
Aig_Obj_t *  pObj 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file fraHot.c.

50 {
51  unsigned * pSims;
52  int i;
53  pSims = Fra_ObjSim(pSeq, pObj->Id);
54  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
55  if ( pSims[i] )
56  return 0;
57  return 1;
58 }
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Fra_OneHotNodesAreClause ( Fra_Sml_t *  pSeq,
Aig_Obj_t *  pObj1,
Aig_Obj_t *  pObj2,
int  fCompl1,
int  fCompl2 
)

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

Synopsis [Returns 1 if implications holds.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file fraHot.c.

95 {
96  unsigned * pSim1, * pSim2;
97  int k;
98  pSim1 = Fra_ObjSim(pSeq, pObj1->Id);
99  pSim2 = Fra_ObjSim(pSeq, pObj2->Id);
100  if ( fCompl1 && fCompl2 )
101  {
102  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
103  if ( pSim1[k] & pSim2[k] )
104  return 0;
105  }
106  else if ( fCompl1 )
107  {
108  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
109  if ( pSim1[k] & ~pSim2[k] )
110  return 0;
111  }
112  else if ( fCompl2 )
113  {
114  for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
115  if ( ~pSim1[k] & pSim2[k] )
116  return 0;
117  }
118  else
119  assert( 0 );
120  return 1;
121 }
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
assert
#define assert(ex)
Definition: util_old.h:213
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Fra_OneHotNodesAreEqual ( Fra_Sml_t *  pSeq,
Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file fraHot.c.

72 {
73  unsigned * pSims0, * pSims1;
74  int i;
75  pSims0 = Fra_ObjSim(pSeq, pObj0->Id);
76  pSims1 = Fra_ObjSim(pSeq, pObj1->Id);
77  for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
78  if ( pSims0[i] != pSims1[i] )
79  return 0;
80  return 1;
81 }
Fra_ObjSim
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Fra_Sml_t_::nWordsPref
int nWordsPref
Definition: fra.h:178
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Fra_OneHotRefineUsingCex ( Fra_Man_t *  p,
Vec_Int_t *  vOneHots 
)

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

Synopsis [Removes those implications that no longer hold.]

Description [Returns 1 if refinement has happened.]

SideEffects []

SeeAlso []

Definition at line 266 of file fraHot.c.

267 {
268  Aig_Obj_t * pObj1, * pObj2;
269  int i, Out1, Out2, RetValue = 0;
270  int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
271  assert( p->pSml->pAig == p->pManAig );
272  for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
273  {
274  Out1 = Vec_IntEntry( vOneHots, i );
275  Out2 = Vec_IntEntry( vOneHots, i+1 );
276  if ( Out1 == 0 && Out2 == 0 )
277  continue;
278  // get the corresponding nodes
279  pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
280  pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
281  // check if implication holds using this simulation info
282  if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
283  {
284  Vec_IntWriteEntry( vOneHots, i, 0 );
285  Vec_IntWriteEntry( vOneHots, i+1, 0 );
286  RetValue = 1;
287  }
288  }
289  return RetValue;
290 }
Fra_Man_t_::pManAig
Aig_Man_t * pManAig
Definition: fra.h:191
Fra_Sml_t_::pAig
Aig_Man_t * pAig
Definition: fra.h:173
Fra_Man_t_::pSml
Fra_Sml_t * pSml
Definition: fra.h:200
Fra_OneHotNodesAreClause
int Fra_OneHotNodesAreClause(Fra_Sml_t *pSeq, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2, int fCompl1, int fCompl2)
Definition: fraHot.c:94
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Fra_LitReg
static int Fra_LitReg(int n)
Definition: fraHot.c:31
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Fra_LitSign
static int Fra_LitSign(int n)
Definition: fraHot.c:32
static ABC_NAMESPACE_IMPL_START int Fra_RegToLit ( int  n,
int  c 
)
inlinestatic

DECLARATIONS ///.

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

FileName [fraHot.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Computing and using one-hotness conditions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraHot.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]

Definition at line 30 of file fraHot.c.

30 { return c? -n-1 : n+1; }