summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw/sswSim.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw/sswSim.c')
-rw-r--r--src/proof/ssw/sswSim.c139
1 files changed, 69 insertions, 70 deletions
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index bb4a55d2..469af654 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -62,19 +62,19 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa
***********************************************************************/
unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
- static int s_SPrimes[128] = {
- 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
- 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
- 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
- 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
- 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
- 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
- 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
- 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
- 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
- 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
- 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
- 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ static int s_SPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
@@ -93,7 +93,7 @@ unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -115,7 +115,7 @@ int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation infos are equal.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -138,7 +138,7 @@ int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1
Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -154,7 +154,7 @@ int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if the nodes appear equal.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -171,7 +171,7 @@ int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Synopsis [Counts the number of 1s in the XOR of simulation data.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -193,7 +193,7 @@ int Ssw_SmlNodeNotEquWeight( Ssw_Sml_t * p, int Left, int Right )
Synopsis [Checks implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -228,7 +228,7 @@ int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -261,7 +261,7 @@ int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
Synopsis [Counts the number of 1s in the implication.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -285,7 +285,7 @@ int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -307,7 +307,7 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -324,7 +324,7 @@ int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
Synopsis [Counts the number of one's in the patten the object.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -353,7 +353,7 @@ int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Counts the number of one's in the patten the object.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -389,7 +389,7 @@ int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
Synopsis [Generated const 0 pattern.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -405,7 +405,7 @@ void Ssw_SmlSavePattern0( Ssw_Man_t * p, int fInit )
Synopsis [[Generated const 1 pattern.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -431,14 +431,14 @@ void Ssw_SmlSavePattern1( Ssw_Man_t * p, int fInit )
Synopsis [Creates the counter-example from the successful pattern.]
Description []
-
+
SideEffects []
SeeAlso []
***********************************************************************/
int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
-{
+{
Aig_Obj_t * pFanin, * pObjPi;
unsigned * pSims;
int i, k, BestPat, * pModel;
@@ -461,10 +461,10 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
Aig_ManForEachCi( p->pAig, pObjPi, i )
{
pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
-// printf( "%d", pModel[i] );
+// Abc_Print( 1, "%d", pModel[i] );
}
pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
-// printf( "\n" );
+// Abc_Print( 1, "\n" );
return pModel;
}
@@ -485,7 +485,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Aig_ManCo( p->pAig, 0 );
- assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
+ assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
Aig_ManForEachCo( p->pAig, pObj, i )
{
if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
@@ -504,7 +504,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
Synopsis [Assigns random patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -529,7 +529,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Assigns random patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -551,7 +551,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -566,14 +566,14 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
for ( i = 0; i < p->nWordsFrame; i++ )
pSims[i] = fConst1? ~(unsigned)0 : 0;
-}
+}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -587,14 +587,14 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = fConst1? ~(unsigned)0 : 0;
-}
+}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -607,14 +607,14 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
assert( Aig_ObjIsCi(pObj) );
pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
pSims[iWord] = Word;
-}
+}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -627,7 +627,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
assert( p->nFrames > 0 );
if ( p->nFrames == 1 )
{
- // copy the PI info
+ // copy the PI info
Aig_ManForEachCi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
// flip one bit
@@ -644,7 +644,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
for ( f = 0; f < p->nFrames; f++ )
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
- // copy the latch info
+ // copy the latch info
k = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
@@ -665,7 +665,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -697,7 +697,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -763,7 +763,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -794,7 +794,7 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -828,7 +828,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -857,7 +857,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
Synopsis [Simulates one node.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -886,7 +886,7 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -919,7 +919,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -946,7 +946,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
Synopsis [Assings random simulation info for the PIs.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -971,7 +971,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p )
Synopsis [Check if any of the POs becomes non-constant.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -996,7 +996,7 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1035,7 +1035,7 @@ p->nSimRounds++;
Synopsis [Converts simulation information to be not normallized.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1067,7 +1067,7 @@ void Ssw_SmlUnnormalize( Ssw_Sml_t * p )
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1108,7 +1108,7 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
-
+
SideEffects []
SeeAlso []
@@ -1139,7 +1139,7 @@ p->nSimRounds++;
Synopsis [Allocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1164,7 +1164,7 @@ Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr
Synopsis [Allocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1180,7 +1180,7 @@ void Ssw_SmlClean( Ssw_Sml_t * p )
Synopsis [Get simulation data.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1202,7 +1202,7 @@ Vec_Ptr_t * Ssw_SmlSimDataPointers( Ssw_Sml_t * p )
Synopsis [Deallocates simulation manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1219,7 +1219,7 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
Synopsis [Performs simulation of the uninitialized circuit.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1239,7 +1239,7 @@ Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
Synopsis [Performs simulation of the initialized circuit.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1260,7 +1260,7 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
Synopsis [Performs next round of sequential simulation.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1279,7 +1279,7 @@ void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
Synopsis [Returns the number of frames simulated in the manager.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1295,7 +1295,7 @@ int Ssw_SmlNumFrames( Ssw_Sml_t * p )
Synopsis [Returns the total number of simulation words.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1312,7 +1312,7 @@ int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p )
Description [The simulation info is normalized unless procedure
Ssw_SmlUnnormalize() is called in advance.]
-
+
SideEffects []
SeeAlso []
@@ -1329,7 +1329,7 @@ unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
Synopsis [Creates sequential counter-example from the simulation info.]
Description []
-
+
SideEffects []
SeeAlso []
@@ -1391,7 +1391,7 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
- printf( "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
+ Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
@@ -1404,4 +1404,3 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p )
ABC_NAMESPACE_IMPL_END
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-27 14:20:54 +0000