1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
/**CFile****************************************************************
FileName [saigAbs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Intergrated abstraction procedure.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Transform flop map into flop list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses )
{
Vec_Int_t * vFlops;
int i, Entry;
vFlops = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vFlopClasses, Entry, i )
if ( Entry )
Vec_IntPush( vFlops, i );
return vFlops;
}
/**Function*************************************************************
Synopsis [Transform flop list into flop map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops )
{
Vec_Int_t * vFlopClasses;
int i, Entry;
vFlopClasses = Vec_IntStart( nRegs );
Vec_IntForEachEntry( vFlops, Entry, i )
Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
return vFlopClasses;
}
/**Function*************************************************************
Synopsis [Derive a new counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, f;
if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
// else
// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" );
// start the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
pCex->iFrame = pCexAbs->iFrame;
pCex->iPo = pCexAbs->iPo;
// copy the bit data
for ( f = 0; f <= pCexAbs->iFrame; f++ )
{
Saig_ManForEachPi( pAbs, pObj, i )
{
if ( i == Saig_ManPiNum(p) )
break;
if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
}
}
// verify the counter example
if ( !Saig_ManVerifyCex( p, pCex ) )
{
printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
else
{
printf( "Counter-example verification is successful.\n" );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
}
return pCex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
