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
134
135
136
137
138
139
140
141
|
/**CFile****************************************************************
FileName [resInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __RES_INT_H__
#define __RES_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "res.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Res_Win_t_ Res_Win_t;
struct Res_Win_t_
{
// windowing parameters
Abc_Obj_t * pNode; // the node in the center
int nWinTfiMax; // the fanin levels
int nWinTfoMax; // the fanout levels
int nLevDivMax; // the maximum divisor level
// internal windowing parameters
int nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root)
int nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves
// derived windowing parameters
int nLevLeafMin; // the minimum level of a leaf
int nLevTravMin; // the minimum level to search from TFO
int nDivsPlus; // the number of additional divisors
// the window data
Vec_Ptr_t * vRoots; // outputs of the window
Vec_Ptr_t * vLeaves; // inputs of the window
Vec_Ptr_t * vBranches; // side nodes of the window
Vec_Ptr_t * vNodes; // internal nodes of the window
Vec_Ptr_t * vDivs; // candidate divisors of the node
// temporary data
Vec_Vec_t * vMatrix; // TFI nodes below the given node
};
typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
int nTruePis; // the number of true PIs of the window
int fConst0; // the node can be replaced by constant 0
int fConst1; // the node can be replaced by constant 0
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsIn; // the number of simulation words in the input patterns
int nPatsIn; // the number of patterns in the input patterns
int nBytesIn; // the number of bytes in the input patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
Vec_Ptr_t * vPats; // input simulation patterns
Vec_Ptr_t * vPats0; // input simulation patterns
Vec_Ptr_t * vPats1; // input simulation patterns
Vec_Ptr_t * vOuts; // output simulation info
int nPats0; // the number of 0-patterns accumulated
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
// statistics
int timeSat;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
extern int Res_WinVisitMffc( Abc_Obj_t * pNode );
/*=== resFilter.c ==========================================================*/
extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax, int fArea );
extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW, int nFaninsMax );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
/*=== resWnd.c ==========================================================*/
extern Res_Win_t * Res_WinAlloc();
extern void Res_WinFree( Res_Win_t * p );
extern int Res_WinIsTrivial( Res_Win_t * p );
extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
