abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
simSupp.c File Reference
#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "sim.h"

Go to the source code of this file.

Functions

static ABC_NAMESPACE_IMPL_START int Sim_ComputeSuppRound (Sim_Man_t *p, int fUseTargets)
 DECLARATIONS ///. More...
 
static int Sim_ComputeSuppRoundNode (Sim_Man_t *p, int iNumCi, int fUseTargets)
 
static void Sim_ComputeSuppSetTargets (Sim_Man_t *p)
 
static void Sim_UtilAssignRandom (Sim_Man_t *p)
 
static void Sim_UtilAssignFromFifo (Sim_Man_t *p)
 
static void Sim_SolveTargetsUsingSat (Sim_Man_t *p, int nCounters)
 
static int Sim_SolveSuppModelVerify (Abc_Ntk_t *pNtk, int *pModel, int Input, int Output)
 
Vec_Ptr_tSim_ComputeStrSupp (Abc_Ntk_t *pNtk)
 FUNCTION DEFINITIONS ///. More...
 
Vec_Ptr_tSim_ComputeFunSupp (Abc_Ntk_t *pNtk, int fVerbose)
 
int Sim_NtkSimTwoPats_rec (Abc_Obj_t *pNode)
 

Function Documentation

Vec_Ptr_t* Sim_ComputeFunSupp ( Abc_Ntk_t pNtk,
int  fVerbose 
)

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

Synopsis [Compute functional supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 103 of file simSupp.c.

104 {
105  Sim_Man_t * p;
106  Vec_Ptr_t * vResult;
107  int nSolved, i;
108  abctime clk = Abc_Clock();
109 
110  srand( 0xABC );
111 
112  // start the simulation manager
113  p = Sim_ManStart( pNtk, 0 );
114 
115  // compute functional support using one round of random simulation
117  Sim_ComputeSuppRound( p, 0 );
118 
119  // set the support targets
121 if ( fVerbose )
122  printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
123  if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
124  goto exit;
125 
126  for ( i = 0; i < 1; i++ )
127  {
128  // compute patterns using one round of random simulation
130  nSolved = Sim_ComputeSuppRound( p, 1 );
131  if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
132  goto exit;
133 
134 if ( fVerbose )
135  printf( "Targets = %5d. Solved = %5d. Fifo = %5d.\n",
136  Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
137  }
138 
139  // try to solve the support targets
140  while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
141  {
142  // solve targets until the first disproved one (which gives counter-example)
144  // compute additional functional support
146  nSolved = Sim_ComputeSuppRound( p, 1 );
147 
148 if ( fVerbose )
149  printf( "Targets = %5d. Solved = %5d. Fifo = %5d. SAT runs = %3d.\n",
150  Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
151  }
152 
153 exit:
154 p->timeTotal = Abc_Clock() - clk;
155  vResult = p->vSuppFun;
156  // p->vSuppFun = NULL;
157  Sim_ManStop( p );
158  return vResult;
159 }
Vec_Ptr_t * vFifo
Definition: sim.h:123
VOID_HACK exit()
int nSuppWords
Definition: sim.h:115
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static void Sim_UtilAssignFromFifo(Sim_Man_t *p)
Definition: simSupp.c:366
Vec_Ptr_t * vSuppFun
Definition: sim.h:117
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int nSimWords
Definition: sim.h:110
int nSatRuns
Definition: sim.h:125
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
abctime timeTotal
Definition: sim.h:133
static void Sim_ComputeSuppSetTargets(Sim_Man_t *p)
Definition: simSupp.c:314
void Sim_ManStop(Sim_Man_t *p)
Definition: simMan.c:208
static void Sim_UtilAssignRandom(Sim_Man_t *p)
Definition: simSupp.c:341
static int Vec_VecSizeSize(Vec_Vec_t *p)
Definition: vecVec.h:417
Vec_Vec_t * vSuppTargs
Definition: sim.h:119
static ABC_NAMESPACE_IMPL_START int Sim_ComputeSuppRound(Sim_Man_t *p, int fUseTargets)
DECLARATIONS ///.
Definition: simSupp.c:172
Sim_Man_t * Sim_ManStart(Abc_Ntk_t *pNtk, int fLightweight)
Definition: simMan.c:166
ABC_INT64_T abctime
Definition: abc_global.h:278
static void Sim_SolveTargetsUsingSat(Sim_Man_t *p, int nCounters)
Definition: simSupp.c:449
Vec_Ptr_t* Sim_ComputeStrSupp ( Abc_Ntk_t pNtk)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes structural supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 57 of file simSupp.c.

58 {
59  Vec_Ptr_t * vSuppStr;
60  Abc_Obj_t * pNode;
61  unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
62  int nSuppWords, i, k;
63  // allocate room for structural supports
64  nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
65  vSuppStr = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
66  // assign the structural support to the PIs
67  Abc_NtkForEachCi( pNtk, pNode, i )
68  Sim_SuppStrSetVar( vSuppStr, pNode, i );
69  // derive the structural supports of the internal nodes
70  Abc_NtkForEachNode( pNtk, pNode, i )
71  {
72 // if ( Abc_NodeIsConst(pNode) )
73 // continue;
74  pSimmNode = (unsigned *)vSuppStr->pArray[ pNode->Id ];
75  pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
76  pSimmNode2 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
77  for ( k = 0; k < nSuppWords; k++ )
78  pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
79  }
80  // set the structural supports of the PO nodes
81  Abc_NtkForEachCo( pNtk, pNode, i )
82  {
83  pSimmNode = (unsigned *)vSuppStr->pArray[ pNode->Id ];
84  pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
85  for ( k = 0; k < nSuppWords; k++ )
86  pSimmNode[k] = pSimmNode1[k];
87  }
88  return vSuppStr;
89 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static int Abc_NtkObjNumMax(Abc_Ntk_t *pNtk)
Definition: abc.h:284
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
static int Abc_ObjFaninId0(Abc_Obj_t *pObj)
Definition: abc.h:367
Vec_Ptr_t * Sim_UtilInfoAlloc(int nSize, int nWords, int fClean)
FUNCTION DEFINITIONS ///.
Definition: simUtils.c:57
#define SIM_NUM_WORDS(n)
MACRO DEFINITIONS ///.
Definition: sim.h:148
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition: abc.h:461
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
static int Abc_ObjFaninId1(Abc_Obj_t *pObj)
Definition: abc.h:368
#define Sim_SuppStrSetVar(vSupps, pNode, v)
Definition: sim.h:166
int Sim_ComputeSuppRound ( Sim_Man_t p,
int  fUseTargets 
)
static

DECLARATIONS ///.

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

FileName [simSupp.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Simulation to determine functional support.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

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

Synopsis [Computes functional support using one round of simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 172 of file simSupp.c.

173 {
174  Vec_Int_t * vTargets;
175  int i, Counter = 0;
176  abctime clk;
177  // perform one round of random simulation
178 clk = Abc_Clock();
179  Sim_UtilSimulate( p, 0 );
180 p->timeSim += Abc_Clock() - clk;
181  // iterate through the CIs and detect COs that depend on them
182  for ( i = p->iInput; i < p->nInputs; i++ )
183  {
184  vTargets = (Vec_Int_t *)p->vSuppTargs->pArray[i];
185  if ( fUseTargets && vTargets->nSize == 0 )
186  continue;
187  Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
188  }
189  return Counter;
190 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static abctime Abc_Clock()
Definition: abc_global.h:279
int iInput
Definition: sim.h:120
static int Sim_ComputeSuppRoundNode(Sim_Man_t *p, int iNumCi, int fUseTargets)
Definition: simSupp.c:203
abctime timeSim
Definition: sim.h:129
void Sim_UtilSimulate(Sim_Man_t *p, int fFirst)
Definition: simUtils.c:208
if(last==0)
Definition: sparse_int.h:34
static int Counter
Vec_Vec_t * vSuppTargs
Definition: sim.h:119
ABC_INT64_T abctime
Definition: abc_global.h:278
int Sim_ComputeSuppRoundNode ( Sim_Man_t p,
int  iNumCi,
int  fUseTargets 
)
static

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

Synopsis [Computes functional support for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file simSupp.c.

204 {
205  int fVerbose = 0;
206  Sim_Pat_t * pPat;
207  Vec_Int_t * vTargets;
208  Vec_Vec_t * vNodesByLevel;
209  Abc_Obj_t * pNodeCi, * pNode;
210  int i, k, v, Output, LuckyPat, fType0, fType1;
211  int Counter = 0;
212  int fFirst = 1;
213  abctime clk;
214  // collect nodes by level in the TFO of the CI
215  // this proceduredoes not collect the CIs and COs
216  // but it increments TravId of the collected nodes and CIs/COs
217 clk = Abc_Clock();
218  pNodeCi = Abc_NtkCi( p->pNtk, iNumCi );
219  vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
220 p->timeTrav += Abc_Clock() - clk;
221  // complement the simulation info of the selected CI
222  Sim_UtilInfoFlip( p, pNodeCi );
223  // simulate the levelized structure of nodes
224  Vec_VecForEachEntry( Abc_Obj_t *, vNodesByLevel, pNode, i, k )
225  {
226  fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
227  fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
228 clk = Abc_Clock();
229  Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
230 p->timeSim += Abc_Clock() - clk;
231  }
232  // set the simulation info of the affected COs
233  if ( fUseTargets )
234  {
235  vTargets = (Vec_Int_t *)p->vSuppTargs->pArray[iNumCi];
236  for ( i = vTargets->nSize - 1; i >= 0; i-- )
237  {
238  // get the target output
239  Output = vTargets->pArray[i];
240  // get the target node
241  pNode = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
242  // the output should be in the cone
244 
245  // skip if the simulation info is equal
246  if ( Sim_UtilInfoCompare( p, pNode ) )
247  continue;
248 
249  // otherwise, we solved a new target
250  Vec_IntRemove( vTargets, Output );
251 if ( fVerbose )
252  printf( "(%d,%d) ", iNumCi, Output );
253  Counter++;
254  // make sure this variable is not yet detected
255  assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) );
256  // set this variable
257  Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
258 
259  // detect the differences in the simulation info
260  Sim_UtilInfoDetectDiffs( (unsigned *)p->vSim0->pArray[pNode->Id], (unsigned *)p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
261  // create new patterns
262  if ( !fFirst && p->vFifo->nSize > 1000 )
263  continue;
264 
265  Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
266  {
267  // set the new pattern
268  pPat = Sim_ManPatAlloc( p );
269  pPat->Input = iNumCi;
270  pPat->Output = Output;
271  Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
272  if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) )
273  Sim_SetBit( pPat->pData, v );
274  Vec_PtrPush( p->vFifo, pPat );
275 
276  fFirst = 0;
277  break;
278  }
279  }
280 if ( fVerbose && Counter )
281 printf( "\n" );
282  }
283  else
284  {
285  Abc_NtkForEachCo( p->pNtk, pNode, Output )
286  {
287  if ( !Abc_NodeIsTravIdCurrent( pNode ) )
288  continue;
289  if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
290  {
291  if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
292  {
293  Counter++;
294  Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
295  }
296  }
297  }
298  }
299  Vec_VecFree( vNodesByLevel );
300  return Counter;
301 }
Vec_Ptr_t * vFifo
Definition: sim.h:123
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
#define Sim_SuppFunSetVar(vSupps, Output, v)
Definition: sim.h:168
Vec_Ptr_t * vSuppFun
Definition: sim.h:117
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition: vecVec.h:42
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define Vec_VecForEachEntry(Type, vGlob, pEntry, i, k)
Definition: vecVec.h:87
int nSimWords
Definition: sim.h:110
Vec_Int_t * vDiffs
Definition: sim.h:124
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
static abctime Abc_Clock()
Definition: abc_global.h:279
abctime timeTrav
Definition: sim.h:130
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
for(p=first;p->value< newval;p=p->next)
int Output
Definition: sim.h:140
static Abc_Obj_t * Abc_NtkCo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:318
void Sim_UtilSimulateNode(Sim_Man_t *p, Abc_Obj_t *pNode, int fType, int fType1, int fType2)
Definition: simUtils.c:231
#define Sim_SimInfoHasVar(vSupps, pNode, v)
Definition: sim.h:171
void Sim_UtilInfoFlip(Sim_Man_t *p, Abc_Obj_t *pNode)
Definition: simUtils.c:164
abctime timeSim
Definition: sim.h:129
void Sim_UtilInfoDetectDiffs(unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
Definition: simUtils.c:118
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
int Input
Definition: sim.h:139
static int Counter
Vec_Ptr_t * vSim1
Definition: sim.h:112
static int Vec_IntRemove(Vec_Int_t *p, int Entry)
Definition: vecInt.h:915
#define Sim_SetBit(p, i)
Definition: sim.h:161
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
Vec_Ptr_t * vSim0
Definition: sim.h:111
ABC_DLL Vec_Vec_t * Abc_DfsLevelized(Abc_Obj_t *pNode, int fTfi)
Definition: abcDfs.c:1129
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
int Id
Definition: abc.h:132
Vec_Vec_t * vSuppTargs
Definition: sim.h:119
Abc_Ntk_t * pNtk
Definition: sim.h:104
#define assert(ex)
Definition: util_old.h:213
int Sim_UtilInfoCompare(Sim_Man_t *p, Abc_Obj_t *pNode)
Definition: simUtils.c:185
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
#define Sim_SuppFunHasVar(vSupps, Output, v)
Definition: sim.h:169
Sim_Pat_t * Sim_ManPatAlloc(Sim_Man_t *p)
Definition: simMan.c:261
void Sim_ComputeSuppSetTargets ( Sim_Man_t p)
static

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

Synopsis [Sets the simulation targets.]

Description []

SideEffects []

SeeAlso []

Definition at line 314 of file simSupp.c.

315 {
316  Abc_Obj_t * pNode;
317  unsigned * pSuppStr, * pSuppFun;
318  int i, k, Num;
319  Abc_NtkForEachCo( p->pNtk, pNode, i )
320  {
321  pSuppStr = (unsigned *)p->vSuppStr->pArray[pNode->Id];
322  pSuppFun = (unsigned *)p->vSuppFun->pArray[i];
323  // find vars in the structural support that are not in the functional support
324  Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
325  Vec_IntForEachEntry( p->vDiffs, Num, k )
326  Vec_VecPush( p->vSuppTargs, Num, (void *)(ABC_PTRUINT_T)i );
327  }
328 }
int nSuppWords
Definition: sim.h:115
static void Vec_VecPush(Vec_Vec_t *p, int Level, void *Entry)
Definition: vecVec.h:456
Vec_Ptr_t * vSuppFun
Definition: sim.h:117
Vec_Int_t * vDiffs
Definition: sim.h:124
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Vec_Ptr_t * vSuppStr
Definition: sim.h:116
int Id
Definition: abc.h:132
Abc_Ntk_t * pNtk
Definition: sim.h:104
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Sim_UtilInfoDetectNews(unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
Definition: simUtils.c:141
int Sim_NtkSimTwoPats_rec ( Abc_Obj_t pNode)

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

Synopsis [Saves the counter example.]

Description []

SideEffects []

SeeAlso []

Definition at line 548 of file simSupp.c.

549 {
550  int Value0, Value1;
551  if ( Abc_NodeIsTravIdCurrent( pNode ) )
552  return (int)(ABC_PTRUINT_T)pNode->pCopy;
553  Abc_NodeSetTravIdCurrent( pNode );
554  Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
555  Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
556  if ( Abc_ObjFaninC0(pNode) )
557  Value0 = ~Value0;
558  if ( Abc_ObjFaninC1(pNode) )
559  Value1 = ~Value1;
560  pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(Value0 & Value1);
561  return Value0 & Value1;
562 }
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
int Sim_NtkSimTwoPats_rec(Abc_Obj_t *pNode)
Definition: simSupp.c:548
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Abc_Obj_t * pCopy
Definition: abc.h:148
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
static void Abc_NodeSetTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:409
int Sim_SolveSuppModelVerify ( Abc_Ntk_t pNtk,
int *  pModel,
int  Input,
int  Output 
)
static

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

Synopsis [Verifies that pModel proves the presence of Input in the support of Output.]

Description []

SideEffects []

SeeAlso []

Definition at line 575 of file simSupp.c.

576 {
577  Abc_Obj_t * pNode;
578  int RetValue, i;
579  // set the PI values
580  Abc_NtkIncrementTravId( pNtk );
581  Abc_NtkForEachCi( pNtk, pNode, i )
582  {
583  Abc_NodeSetTravIdCurrent( pNode );
584  if ( pNode == Abc_NtkCi(pNtk,Input) )
585  pNode->pCopy = (Abc_Obj_t *)1;
586  else if ( pModel[i] == 1 )
587  pNode->pCopy = (Abc_Obj_t *)3;
588  else
589  pNode->pCopy = NULL;
590  }
591  // perform the traversal
592  RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
593 // assert( RetValue == 1 || RetValue == 2 );
594  return RetValue == 1 || RetValue == 2;
595 }
int Sim_NtkSimTwoPats_rec(Abc_Obj_t *pNode)
Definition: simSupp.c:548
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
static Abc_Obj_t * Abc_NtkCo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:318
Abc_Obj_t * pCopy
Definition: abc.h:148
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
static void Abc_NtkIncrementTravId(Abc_Ntk_t *p)
Definition: abc.h:406
static void Abc_NodeSetTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:409
void Sim_SolveTargetsUsingSat ( Sim_Man_t p,
int  Limit 
)
static

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

Synopsis [Get the given number of counter-examples using SAT.]

Description []

SideEffects []

SeeAlso []

Definition at line 449 of file simSupp.c.

450 {
451  Fraig_Params_t Params;
452  Fraig_Man_t * pMan;
453  Abc_Obj_t * pNodeCi;
454  Abc_Ntk_t * pMiter;
455  Sim_Pat_t * pPat;
456  void * pEntry;
457  int * pModel;
458  int RetValue, Output, Input, k, v;
459  int Counter = 0;
460  abctime clk;
461 
462  p->nSatRuns = 0;
463  // put targets into one array
464  Vec_VecForEachEntryReverse( void *, p->vSuppTargs, pEntry, Input, k )
465  {
466  p->nSatRuns++;
467  Output = (int)(ABC_PTRUINT_T)pEntry;
468 
469  // set up the miter for the two cofactors of this output w.r.t. this input
470  pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
471 
472  // transform the miter into a fraig
473  Fraig_ParamsSetDefault( &Params );
474  Params.nSeconds = ABC_INFINITY;
475  Params.fInternal = 1;
476 clk = Abc_Clock();
477  pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 );
478 p->timeFraig += Abc_Clock() - clk;
479 clk = Abc_Clock();
480  Fraig_ManProveMiter( pMan );
481 p->timeSat += Abc_Clock() - clk;
482 
483  // analyze the result
484  RetValue = Fraig_ManCheckMiter( pMan );
485  assert( RetValue >= 0 );
486  if ( RetValue == 1 ) // unsat
487  {
488  p->nSatRunsUnsat++;
489  pModel = NULL;
490  Vec_PtrRemove( (Vec_Ptr_t *)p->vSuppTargs->pArray[Input], pEntry );
491  }
492  else // sat
493  {
494  p->nSatRunsSat++;
495  pModel = Fraig_ManReadModel( pMan );
496  assert( pModel != NULL );
497  assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) );
498 
499 //printf( "Solved by SAT (%d,%d).\n", Input, Output );
500  // set the new pattern
501  pPat = Sim_ManPatAlloc( p );
502  pPat->Input = Input;
503  pPat->Output = Output;
504  Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
505  if ( pModel[v] )
506  Sim_SetBit( pPat->pData, v );
507  Vec_PtrPush( p->vFifo, pPat );
508 /*
509  // set the new pattern
510  pPat = Sim_ManPatAlloc( p );
511  pPat->Input = Input;
512  pPat->Output = Output;
513  Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
514  if ( pModel[v] )
515  Sim_SetBit( pPat->pData, v );
516  Sim_XorBit( pPat->pData, Input ); // add this bit in the opposite polarity
517  Vec_PtrPush( p->vFifo, pPat );
518 */
519  Counter++;
520  }
521  // delete the fraig manager
522  Fraig_ManFree( pMan );
523  // delete the miter
524  Abc_NtkDelete( pMiter );
525 
526  // makr the input, which we are processing
527  p->iInput = Input;
528 
529  // stop when we found enough patterns
530 // if ( Counter == Limit )
531  if ( Counter == 1 )
532  return;
533  }
534 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition: fraig.h:40
abctime timeSat
Definition: sim.h:132
void Fraig_ManFree(Fraig_Man_t *pMan)
Definition: fraigMan.c:262
ABC_DLL Abc_Ntk_t * Abc_NtkMiterForCofactors(Abc_Ntk_t *pNtk, int Out, int In1, int In2)
Definition: abcMiter.c:514
int nSatRuns
Definition: sim.h:125
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
int nSatRunsUnsat
Definition: sim.h:127
static abctime Abc_Clock()
Definition: abc_global.h:279
int Output
Definition: sim.h:140
static void Vec_PtrRemove(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:714
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
abctime timeFraig
Definition: sim.h:131
#define Vec_VecForEachEntryReverse(Type, vGlob, pEntry, i, k)
Definition: vecVec.h:98
if(last==0)
Definition: sparse_int.h:34
void Fraig_ParamsSetDefault(Fraig_Params_t *pParams)
Definition: fraigMan.c:122
int Input
Definition: sim.h:139
static int Counter
static int Sim_SolveSuppModelVerify(Abc_Ntk_t *pNtk, int *pModel, int Input, int Output)
Definition: simSupp.c:575
#define Sim_SetBit(p, i)
Definition: sim.h:161
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
int nSatRunsSat
Definition: sim.h:126
Vec_Vec_t * vSuppTargs
Definition: sim.h:119
Abc_Ntk_t * pNtk
Definition: sim.h:104
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition: abc_global.h:216
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
int * Fraig_ManReadModel(Fraig_Man_t *p)
Definition: fraigApi.c:63
int Fraig_ManCheckMiter(Fraig_Man_t *p)
Definition: fraigSat.c:130
ABC_DLL void * Abc_NtkToFraig(Abc_Ntk_t *pNtk, void *pParams, int fAllNodes, int fExdc)
Definition: abcFraig.c:103
Sim_Pat_t * Sim_ManPatAlloc(Sim_Man_t *p)
Definition: simMan.c:261
void Fraig_ManProveMiter(Fraig_Man_t *p)
Definition: fraigSat.c:85
void Sim_UtilAssignFromFifo ( Sim_Man_t p)
static

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

Synopsis [Sets the new patterns from fifo.]

Description []

SideEffects []

SeeAlso []

Definition at line 366 of file simSupp.c.

367 {
368  int fUseOneWord = 0;
369  Abc_Obj_t * pNode;
370  Sim_Pat_t * pPat;
371  unsigned * pSimInfo;
372  int nWordsNew, iWord, iWordLim, i, w;
373  int iBeg, iEnd;
374  int Counter = 0;
375  // go through the patterns and fill in the dist-1 minterms for each
376  for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim )
377  {
378  ++Counter;
379  // get the pattern
380  pPat = (Sim_Pat_t *)Vec_PtrPop( p->vFifo );
381  if ( fUseOneWord )
382  {
383  // get the first word of the next series
384  iWordLim = iWord + 1;
385  // set the pattern for all PIs from iBit to iWord + p->nInputs
386  iBeg = p->iInput;
387  iEnd = Abc_MinInt( iBeg + 32, p->nInputs );
388 // for ( i = iBeg; i < iEnd; i++ )
389  Abc_NtkForEachCi( p->pNtk, pNode, i )
390  {
391  pNode = Abc_NtkCi(p->pNtk,i);
392  pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
393  if ( Sim_HasBit(pPat->pData, i) )
394  pSimInfo[iWord] = SIM_MASK_FULL;
395  else
396  pSimInfo[iWord] = 0;
397  // flip one bit
398  if ( i >= iBeg && i < iEnd )
399  Sim_XorBit( pSimInfo + iWord, i-iBeg );
400  }
401  }
402  else
403  {
404  // get the number of words for the remaining inputs
405  nWordsNew = p->nSuppWords;
406 // nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
407  // get the first word of the next series
408  iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords;
409  // set the pattern for all CIs from iWord to iWord + nWordsNew
410  Abc_NtkForEachCi( p->pNtk, pNode, i )
411  {
412  pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
413  if ( Sim_HasBit(pPat->pData, i) )
414  {
415  for ( w = iWord; w < iWordLim; w++ )
416  pSimInfo[w] = SIM_MASK_FULL;
417  }
418  else
419  {
420  for ( w = iWord; w < iWordLim; w++ )
421  pSimInfo[w] = 0;
422  }
423  Sim_XorBit( pSimInfo + iWord, i );
424  // flip one bit
425 // if ( i >= p->iInput )
426 // Sim_XorBit( pSimInfo + iWord, i-p->iInput );
427  }
428  }
429  Sim_ManPatFree( p, pPat );
430  // stop if we ran out of room for patterns
431  if ( iWordLim == p->nSimWords )
432  break;
433 // if ( Counter == 1 )
434 // break;
435  }
436 }
Vec_Ptr_t * vFifo
Definition: sim.h:123
int nSuppWords
Definition: sim.h:115
#define SIM_MASK_FULL
Definition: sim.h:151
int nSimWords
Definition: sim.h:110
static Abc_Obj_t * Abc_NtkCi(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:317
int iInput
Definition: sim.h:120
static void * Vec_PtrPop(Vec_Ptr_t *p)
Definition: vecPtr.h:677
unsigned * pData
Definition: sim.h:141
void Sim_ManPatFree(Sim_Man_t *p, Sim_Pat_t *pPat)
Definition: simMan.c:282
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
#define Sim_HasBit(p, i)
Definition: sim.h:163
if(last==0)
Definition: sparse_int.h:34
static int Counter
Vec_Ptr_t * vSim0
Definition: sim.h:111
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
int Id
Definition: abc.h:132
#define Sim_XorBit(p, i)
Definition: sim.h:162
Abc_Ntk_t * pNtk
Definition: sim.h:104
int nInputs
Definition: sim.h:105
void Sim_UtilAssignRandom ( Sim_Man_t p)
static

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

Synopsis [Assigns random simulation info to the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 341 of file simSupp.c.

342 {
343  Abc_Obj_t * pNode;
344  unsigned * pSimInfo;
345  int i, k;
346  // assign the random/systematic simulation info to the PIs
347  Abc_NtkForEachCi( p->pNtk, pNode, i )
348  {
349  pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
350  for ( k = 0; k < p->nSimWords; k++ )
351  pSimInfo[k] = SIM_RANDOM_UNSIGNED;
352  }
353 }
#define SIM_RANDOM_UNSIGNED
Definition: sim.h:158
int nSimWords
Definition: sim.h:110
for(p=first;p->value< newval;p=p->next)
Vec_Ptr_t * vSim0
Definition: sim.h:111
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
int Id
Definition: abc.h:132
Abc_Ntk_t * pNtk
Definition: sim.h:104