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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
/**CFile****************************************************************
FileName [cswInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswInt.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CSW_INT_H__
#define __CSW_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "aig.h"
#include "dar.h"
#include "kit.h"
#include "csw.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Csw_Man_t_ Csw_Man_t;
typedef struct Csw_Cut_t_ Csw_Cut_t;
// the cut used to represent node in the AIG
struct Csw_Cut_t_
{
Csw_Cut_t * pNext; // the next cut in the table
int Cost; // the cost of the cut
// float Cost; // the cost of the cut
unsigned uSign; // cut signature
int iNode; // the node, for which it is the cut
short nCutSize; // the number of bytes in the cut
char nLeafMax; // the maximum number of fanins
char nFanins; // the current number of fanins
int pFanins[0]; // the fanins (followed by the truth table)
};
// the CNF computation manager
struct Csw_Man_t_
{
// AIG manager
Aig_Man_t * pManAig; // the input AIG manager
Aig_Man_t * pManRes; // the output AIG manager
Aig_Obj_t ** pEquiv; // the equivalent nodes in the resulting manager
Csw_Cut_t ** pCuts; // the cuts for each node in the output manager
int * pnRefs; // the number of references of each new node
// hash table for cuts
Csw_Cut_t ** pTable; // the table composed of cuts
int nTableSize; // the size of hash table
// parameters
int nCutsMax; // the max number of cuts at the node
int nLeafMax; // the max number of leaves of a cut
int fVerbose; // enables verbose output
// internal variables
int nCutSize; // the number of bytes needed to store one cut
int nTruthWords; // the number of truth table words
Aig_MmFixed_t * pMemCuts; // memory manager for cuts
unsigned * puTemp[4]; // used for the truth table computation
// statistics
int nNodesTriv0; // the number of trivial nodes
int nNodesTriv1; // the number of trivial nodes
int nNodesTriv2; // the number of trivial nodes
int nNodesCuts; // the number of rewritten nodes
int nNodesTried; // the number of nodes tried
int timeCuts; // time to compute the cut and its truth table
int timeHash; // time for hashing cuts
int timeOther; // other time
int timeTotal; // total time
};
static inline int Csw_CutLeaveNum( Csw_Cut_t * pCut ) { return pCut->nFanins; }
static inline int * Csw_CutLeaves( Csw_Cut_t * pCut ) { return pCut->pFanins; }
static inline unsigned * Csw_CutTruth( Csw_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); }
static inline Csw_Cut_t * Csw_CutNext( Csw_Cut_t * pCut ) { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize); }
static inline int Csw_ObjRefs( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pnRefs[pObj->Id]; }
static inline void Csw_ObjAddRefs( Csw_Man_t * p, Aig_Obj_t * pObj, int nRefs ) { p->pnRefs[pObj->Id] += nRefs; }
static inline Csw_Cut_t * Csw_ObjCuts( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; }
static inline void Csw_ObjSetCuts( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; }
static inline Aig_Obj_t * Csw_ObjEquiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquiv[pObj->Id]; }
static inline void Csw_ObjSetEquiv( Csw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
static inline Aig_Obj_t * Csw_ObjChild0Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Csw_ObjChild1Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over cuts of the node
#define Csw_ObjForEachCut( p, pObj, pCut, i ) \
for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) )
// iterator over leaves of the cut
#define Csw_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCut.c ========================================================*/
extern Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
extern Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
/*=== cnfMan.c ========================================================*/
extern Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
extern void Csw_ManStop( Csw_Man_t * p );
/*=== cnfTable.c ========================================================*/
extern int Csw_TableCountCuts( Csw_Man_t * p );
extern void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut );
extern Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
