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
|
/**CFile****************************************************************
FileName [cgtSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Clock gating package.]
Synopsis [Checking implications using SAT.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cgtSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cgtInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description [Both nodes should be regular and different from each other.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cgt_CheckImplication( Cgt_Man_t * p, Aig_Obj_t * pGate, Aig_Obj_t * pMiter )
{
int nBTLimit = p->pPars->nConfMax;
int pLits[2], RetValue;
clock_t clk;
p->nCalls++;
// sanity checks
assert( p->pSat && p->pCnf );
assert( !Aig_IsComplement(pMiter) );
assert( Aig_Regular(pGate) != pMiter );
// solve under assumptions
// G => !M -- true G & M -- false
pLits[0] = toLitCond( p->pCnf->pVarNums[Aig_Regular(pGate)->Id], Aig_IsComplement(pGate) );
pLits[1] = toLitCond( p->pCnf->pVarNums[pMiter->Id], 0 );
clk = clock();
RetValue = sat_solver_solve( p->pSat, pLits, pLits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += clock() - clk;
if ( RetValue == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
sat_solver_compress( p->pSat );
p->nCallsUnsat++;
return 1;
}
else if ( RetValue == l_True )
{
p->timeSatSat += clock() - clk;
p->nCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->nCallsUndec++;
return -1;
}
return -2;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
