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
|
/**CFile****************************************************************
FileName [bmcBmcAnd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Memory-efficient BMC engine]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcBmcAnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCountUnmarked_rec( Gia_Obj_t * pObj )
{
if ( !Gia_ObjIsAnd(pObj) || pObj->fMark0 )
return 0;
pObj->fMark0 = 1;
return 1 + Gia_ManCountUnmarked_rec( Gia_ObjFanin0(pObj) ) +
Gia_ManCountUnmarked_rec( Gia_ObjFanin1(pObj) );
}
int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
{
int i, Counter = 0;
for ( i = iStart; i < Gia_ManPoNum(p); i++ )
Counter += Gia_ManCountUnmarked_rec( Gia_ObjFanin0(Gia_ManPo(p, i)) );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Unr_Man_t * p;
Gia_Man_t * pFrames;
abctime clk = Abc_Clock();
int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
int i, f, iStart, status = -1, Counter = 0;
p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
for ( f = 0; f < nFramesMax; f++ )
{
pFrames = Unr_ManUnrollFrame( p, f );
assert( Gia_ManPoNum(pFrames) == (f + 1) * Gia_ManPoNum(pGia) );
iStart = f * Gia_ManPoNum(pGia);
for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
break;
if ( i == Gia_ManPoNum(pFrames) )
{
if ( pPars->fVerbose )
{
printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%6.1f Mb ",
f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
continue;
}
if ( pPars->fVerbose )
{
printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%6.1f Mb ",
f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// if ( ++Counter == 10 )
// break;
}
Unr_ManFree( p );
return status;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
