ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fxu.c File Reference
#include "fxuInt.h"
#include "fxu.h"
Include dependency graph for fxu.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Fxu_MatrixFxu_CreateMatrix (Fxu_Data_t *pData)
 DECLARATIONS ///.
 
void Fxu_CreateCovers (Fxu_Matrix *p, Fxu_Data_t *pData)
 
int Fxu_FastExtract (Fxu_Data_t *pData)
 FUNCTION DEFINITIONS ///.
 
void Fxu_MatrixRingCubesUnmark (Fxu_Matrix *p)
 
void Fxu_MatrixRingVarsUnmark (Fxu_Matrix *p)
 
char * Fxu_MemFetch (Fxu_Matrix *p, int nBytes)
 FUNCTION DEFINITIONS ///.
 
void Fxu_MemRecycle (Fxu_Matrix *p, char *pItem, int nBytes)
 

Function Documentation

◆ Fxu_CreateCovers()

void Fxu_CreateCovers ( Fxu_Matrix * p,
Fxu_Data_t * pData )
extern

Function*************************************************************

Synopsis [Creates the new array of Sop covers from the sparse matrix.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file fxuCreate.c.

279{
280 Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
281 char * pSopCover;
282 int iNode, n;
283
284 // get the first cube of the first internal node
285 pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
286
287 // go through the internal nodes
288 for ( n = 0; n < pData->nNodesOld; n++ )
289 if ( (pSopCover = (char *)pData->vSops->pArray[n]) )
290 {
291 // get the number of this node
292 iNode = n;
293 // get the next first cube
294 pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
295 // check if there any new variables in these cubes
296 for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
297 if ( pCube->lLits.pTail && pCube->lLits.pTail->iVar >= 2 * pData->nNodesOld )
298 break;
299 if ( pCube != pCubeNext )
300 Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
301 // update the first cube
302 pCubeFirst = pCubeNext;
303 }
304
305 // add the covers for the extracted nodes
306 for ( n = 0; n < pData->nNodesNew; n++ )
307 {
308 // get the number of this node
309 iNode = pData->nNodesOld + n;
310 // get the next first cube
311 pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
312 // the node should be added
313 Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
314 // update the first cube
315 pCubeFirst = pCubeNext;
316 }
317}
Cube * p
Definition exorList.c:222
struct FxuCube Fxu_Cube
Definition fxuInt.h:66
Fxu_ListLit lLits
Definition fxuInt.h:206
Fxu_Cube * pNext
Definition fxuInt.h:208
Fxu_Lit * pTail
Definition fxuInt.h:110
int iVar
Definition fxuInt.h:228
Here is the caller graph for this function:

◆ Fxu_CreateMatrix()

ABC_NAMESPACE_IMPL_START Fxu_Matrix * Fxu_CreateMatrix ( Fxu_Data_t * pData)
extern

DECLARATIONS ///.

CFile****************************************************************

FileName [fxu.c]

PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

Synopsis [The entrance into the fast extract module.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id
fxu.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

]

DECLARATIONS ///.

Function*************************************************************

Synopsis [Creates the sparse matrix from the array of SOPs.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file fxuCreate.c.

53{
54 Fxu_Matrix * p;
55 Fxu_Var * pVar;
56 Fxu_Cube * pCubeFirst, * pCubeNew;
57 Fxu_Cube * pCube1, * pCube2;
58 Vec_Int_t * vFanins;
59 char * pSopCover;
60 char * pSopCube;
61 int * pOrder, nBitsMax;
62 int i, v, c;
63 int nCubesTotal;
64 int nPairsTotal;
65 int nPairsStore;
66 int nCubes;
67 int iCube, iPair;
68 int nFanins;
69
70 // collect all sorts of statistics
71 nCubesTotal = 0;
72 nPairsTotal = 0;
73 nPairsStore = 0;
74 nBitsMax = -1;
75 for ( i = 0; i < pData->nNodesOld; i++ )
76 if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
77 {
78 nCubes = Abc_SopGetCubeNum( pSopCover );
79 nFanins = Abc_SopGetVarNum( pSopCover );
80 assert( nFanins > 1 && nCubes > 0 );
81
82 nCubesTotal += nCubes;
83 nPairsTotal += nCubes * (nCubes - 1) / 2;
84 nPairsStore += nCubes * nCubes;
85 if ( nBitsMax < nFanins )
86 nBitsMax = nFanins;
87 }
88 if ( nBitsMax <= 0 )
89 {
90 printf( "The current network does not have SOPs to perform extraction.\n" );
91 return NULL;
92 }
93
94 if ( nPairsStore > 50000000 )
95 {
96 printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
97 return NULL;
98 }
99
100 // start the matrix
102 // create the column labels
103 p->ppVars = ABC_ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
104 for ( i = 0; i < 2 * pData->nNodesOld; i++ )
105 p->ppVars[i] = Fxu_MatrixAddVar( p );
106
107 // allocate storage for all cube pairs at once
108 p->pppPairs = ABC_ALLOC( Fxu_Pair **, nCubesTotal + 100 );
109 p->ppPairs = ABC_ALLOC( Fxu_Pair *, nPairsStore + 100 );
110 memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
111 iCube = 0;
112 iPair = 0;
113 for ( i = 0; i < pData->nNodesOld; i++ )
114 if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
115 {
116 // get the number of cubes
117 nCubes = Abc_SopGetCubeNum( pSopCover );
118 // get the new var in the matrix
119 pVar = p->ppVars[2*i+1];
120 // assign the pair storage
121 pVar->nCubes = nCubes;
122 if ( nCubes > 0 )
123 {
124 pVar->ppPairs = p->pppPairs + iCube;
125 pVar->ppPairs[0] = p->ppPairs + iPair;
126 for ( v = 1; v < nCubes; v++ )
127 pVar->ppPairs[v] = pVar->ppPairs[v-1] + nCubes;
128 }
129 // update
130 iCube += nCubes;
131 iPair += nCubes * nCubes;
132 }
133 assert( iCube == nCubesTotal );
134 assert( iPair == nPairsStore );
135
136
137 // allocate room for the reordered literals
138 pOrder = ABC_ALLOC( int, nBitsMax );
139 // create the rows
140 for ( i = 0; i < pData->nNodesOld; i++ )
141 if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
142 {
143 // get the new var in the matrix
144 pVar = p->ppVars[2*i+1];
145 // here we sort the literals of the cover
146 // in the increasing order of the numbers of the corresponding nodes
147 // because literals should be added to the matrix in this order
148 vFanins = (Vec_Int_t *)pData->vFanins->pArray[i];
149 s_pLits = vFanins->pArray;
150 // start the variable order
151 nFanins = Abc_SopGetVarNum( pSopCover );
152 for ( v = 0; v < nFanins; v++ )
153 pOrder[v] = v;
154 // reorder the fanins
155 qsort( (void *)pOrder, (size_t)nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
156 assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
157 // create the corresponding cubes in the matrix
158 pCubeFirst = NULL;
159 c = 0;
160 Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
161 {
162 // create the cube
163 pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
164 Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
165 if ( pCubeFirst == NULL )
166 pCubeFirst = pCubeNew;
167 pCubeNew->pFirst = pCubeFirst;
168 }
169 // set the first cube of this var
170 pVar->pFirst = pCubeFirst;
171 // create the divisors without preprocessing
172 if ( nPairsTotal <= pData->nPairsMax )
173 {
174 for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->pNext )
175 for ( pCube2 = pCube1? pCube1->pNext: NULL; pCube2; pCube2 = pCube2->pNext )
176 Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
177 }
178 }
179 ABC_FREE( pOrder );
180
181 // consider the case when cube pairs should be preprocessed
182 // before adding them to the set of divisors
183// if ( pData->fVerbose )
184// printf( "The total number of cube pairs is %d.\n", nPairsTotal );
185 if ( nPairsTotal > 10000000 )
186 {
187 printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
188 printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
189 printf( "that the user changes the network by reducing the size of logic node and\n" );
190 printf( "consequently the number of cube pairs to be processed by this command.\n" );
191 printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
192 printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
193 return NULL;
194 }
195 if ( nPairsTotal > pData->nPairsMax )
196 if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
197 return NULL;
198// if ( pData->fVerbose )
199// printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
200
201 if ( p->lVars.nItems > 1000000 )
202 {
203 printf( "The total number of variables is more than 1,000,000.\n" );
204 printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
205 printf( "that the user changes the network by reducing the size of logic node and\n" );
206 printf( "consequently the number of cube pairs to be processed by this command.\n" );
207 printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
208 printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
209 return NULL;
210 }
211
212
213 // add the var pairs to the heap
214 Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
215
216 // print stats
217 if ( pData->fVerbose )
218 {
219 double Density;
220 Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
221 fprintf( stdout, "Matrix: [vars x cubes] = [%d x %d] ",
222 p->lVars.nItems, p->lCubes.nItems );
223 fprintf( stdout, "Lits = %d Density = %.5f%%\n",
224 p->nEntries, Density );
225 fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal );
226 fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal );
227 fprintf( stdout, "\n" );
228 }
229// Fxu_MatrixPrint( stdout, p );
230 return p;
231}
#define Abc_SopForEachCube(pSop, nFanins, pCube)
Definition abc.h:538
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition abcSop.c:584
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
Definition abcSop.c:537
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
int Fxu_PreprocessCubePairs(Fxu_Matrix *p, Vec_Ptr_t *vCovers, int nPairsTotal, int nPairsMax)
FUNCTION DEFINITIONS ///.
Definition fxuReduce.c:53
Fxu_Var * Fxu_MatrixAddVar(Fxu_Matrix *p)
Definition fxuMatrix.c:161
struct FxuVar Fxu_Var
Definition fxuInt.h:67
Fxu_Matrix * Fxu_MatrixAllocate()
DECLARATIONS ///.
Definition fxuMatrix.c:43
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Definition fxuInt.h:63
struct FxuPair Fxu_Pair
Definition fxuInt.h:71
void Fxu_MatrixComputeSingles(Fxu_Matrix *p, int fUse0, int nSingleMax)
FUNCTION DEFINITIONS ///.
Definition fxuSingle.c:47
void Fxu_MatrixAddDivisor(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition fxuMatrix.c:301
Fxu_Cube * Fxu_MatrixAddCube(Fxu_Matrix *p, Fxu_Var *pVar, int iCube)
Definition fxuMatrix.c:183
Fxu_Cube * pFirst
Definition fxuInt.h:204
int nCubes
Definition fxuInt.h:216
Fxu_Pair *** ppPairs
Definition fxuInt.h:218
Fxu_Cube * pFirst
Definition fxuInt.h:217
#define assert(ex)
Definition util_old.h:213
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_FastExtract()

int Fxu_FastExtract ( Fxu_Data_t * pData)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs fast_extract on a set of covers.]

Description [All the covers are given in the array p->vSops. The resulting covers are returned in the array p->vSopsNew. The entries in these arrays correspond to objects in the network. The entries corresponding to the PI and objects with trivial covers are NULL. The number of extracted covers (not exceeding p->nNodesExt) is returned. Two other things are important for the correct operation of this procedure: (1) The input covers do not have duplicated fanins and are SCC-free. (2) The fanins array contains the numbers of the fanin objects.]

SideEffects []

SeeAlso []

Definition at line 58 of file fxu.c.

59{
60 int fScrollLines = 0;
61 Fxu_Matrix * p;
62 Fxu_Single * pSingle;
63 Fxu_Double * pDouble;
64 int Weight1, Weight2, Weight3;
65 int Counter = 0;
66
67 s_MemoryTotal = 0;
68 s_MemoryPeak = 0;
69
70 // create the matrix
71 p = Fxu_CreateMatrix( pData );
72 if ( p == NULL )
73 return -1;
74// if ( pData->fVerbose )
75// printf( "Memory usage after construction: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
76//Fxu_MatrixPrint( NULL, p );
77
78 if ( pData->fOnlyS )
79 {
80 pData->nNodesNew = 0;
81 do
82 {
83 Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
84 if ( pData->fVerbose )
85 printf( "Div %5d : Best single = %5d.%s", Counter++, Weight1, fScrollLines?"\n":"\r" );
86 if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) )
88 else
89 break;
90 }
91 while ( ++pData->nNodesNew < pData->nNodesExt );
92 }
93 else if ( pData->fOnlyD )
94 {
95 pData->nNodesNew = 0;
96 do
97 {
98 Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
99 if ( pData->fVerbose )
100 printf( "Div %5d : Best double = %5d.%s", Counter++, Weight2, fScrollLines?"\n":"\r" );
101 if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) )
103 else
104 break;
105 }
106 while ( ++pData->nNodesNew < pData->nNodesExt );
107 }
108 else if ( !pData->fUseCompl )
109 {
110 pData->nNodesNew = 0;
111 do
112 {
113 Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
114 Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
115
116 if ( pData->fVerbose )
117 printf( "Div %5d : Best double = %5d. Best single = %5d.%s", Counter++, Weight2, Weight1, fScrollLines?"\n":"\r" );
118//Fxu_Select( p, &pSingle, &pDouble );
119
120 if ( Weight1 >= Weight2 )
121 {
122 if ( Weight1 > pData->WeightMin || (Weight1 == 0 && pData->fUse0) )
124 else
125 break;
126 }
127 else
128 {
129 if ( Weight2 > pData->WeightMin || (Weight2 == 0 && pData->fUse0) )
131 else
132 break;
133 }
134 }
135 while ( ++pData->nNodesNew < pData->nNodesExt );
136 }
137 else
138 { // use the complement
139 pData->nNodesNew = 0;
140 do
141 {
142 Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
143 Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
144
145 // select the best single and double
146 Weight3 = Fxu_Select( p, &pSingle, &pDouble );
147 if ( pData->fVerbose )
148 printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.%s",
149 Counter++, Weight2, Weight1, Weight3, fScrollLines?"\n":"\r" );
150
151 if ( Weight3 > pData->WeightMin || (Weight3 == 0 && pData->fUse0) )
152 Fxu_Update( p, pSingle, pDouble );
153 else
154 break;
155 }
156 while ( ++pData->nNodesNew < pData->nNodesExt );
157 }
158
159 if ( pData->fVerbose )
160 printf( "Total single = %3d. Total double = %3d. Total compl = %3d. \n",
161 p->nDivs1, p->nDivs2, p->nDivs3 );
162
163 // create the new covers
164 if ( pData->nNodesNew )
165 Fxu_CreateCovers( p, pData );
167// printf( "Memory usage after deallocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
168 if ( pData->nNodesNew == pData->nNodesExt )
169 printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
170 return pData->nNodesNew;
171}
int Fxu_HeapDoubleReadMaxWeight(Fxu_HeapDouble *p)
Definition fxuHeapD.c:319
int Fxu_HeapSingleReadMaxWeight(Fxu_HeapSingle *p)
Definition fxuHeapS.c:321
void Fxu_UpdateDouble(Fxu_Matrix *p)
Definition fxuUpdate.c:219
void Fxu_UpdateSingle(Fxu_Matrix *p)
Definition fxuUpdate.c:149
struct FxuSingle Fxu_Single
Definition fxuInt.h:73
void Fxu_MatrixDelete(Fxu_Matrix *p)
Definition fxuMatrix.c:96
struct FxuDouble Fxu_Double
Definition fxuInt.h:72
int Fxu_Select(Fxu_Matrix *p, Fxu_Single **ppSingle, Fxu_Double **ppDouble)
FUNCTION DEFINITIONS ///.
Definition fxuSelect.c:57
void Fxu_Update(Fxu_Matrix *p, Fxu_Single *pSingle, Fxu_Double *pDouble)
FUNCTION DEFINITIONS ///.
Definition fxuUpdate.c:57
void Fxu_CreateCovers(Fxu_Matrix *p, Fxu_Data_t *pData)
Definition fxuCreate.c:278
ABC_NAMESPACE_IMPL_START Fxu_Matrix * Fxu_CreateMatrix(Fxu_Data_t *pData)
DECLARATIONS ///.
Definition fxuCreate.c:52
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Fxu_MatrixRingCubesUnmark()

void Fxu_MatrixRingCubesUnmark ( Fxu_Matrix * p)

Function*************************************************************

Synopsis [Unmarks the cubes in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file fxu.c.

186{
187 Fxu_Cube * pCube, * pCube2;
188 // unmark the cubes
189 Fxu_MatrixForEachCubeInRingSafe( p, pCube, pCube2 )
190 pCube->pOrder = NULL;
192}
#define Fxu_MatrixForEachCubeInRingSafe(Matrix, Cube, Cube2)
Definition fxuInt.h:402
#define Fxu_MatrixRingCubesReset(Matrix)
Definition fxuInt.h:391
Fxu_Cube * pOrder
Definition fxuInt.h:209
Here is the caller graph for this function:

◆ Fxu_MatrixRingVarsUnmark()

void Fxu_MatrixRingVarsUnmark ( Fxu_Matrix * p)

Function*************************************************************

Synopsis [Unmarks the vars in the ring.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file fxu.c.

207{
208 Fxu_Var * pVar, * pVar2;
209 // unmark the vars
210 Fxu_MatrixForEachVarInRingSafe( p, pVar, pVar2 )
211 pVar->pOrder = NULL;
213}
#define Fxu_MatrixForEachVarInRingSafe(Matrix, Var, Var2)
Definition fxuInt.h:412
#define Fxu_MatrixRingVarsReset( Matrix)
Definition fxuInt.h:392
Fxu_Var * pOrder
Definition fxuInt.h:222
Here is the caller graph for this function:

◆ Fxu_MemFetch()

char * Fxu_MemFetch ( Fxu_Matrix * p,
int nBytes )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file fxu.c.

228{
229 s_MemoryTotal += nBytes;
230 if ( s_MemoryPeak < s_MemoryTotal )
231 s_MemoryPeak = s_MemoryTotal;
232// return ABC_ALLOC( char, nBytes );
233 return Extra_MmFixedEntryFetch( p->pMemMan );
234}
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Here is the call graph for this function:

◆ Fxu_MemRecycle()

void Fxu_MemRecycle ( Fxu_Matrix * p,
char * pItem,
int nBytes )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file fxu.c.

248{
249 s_MemoryTotal -= nBytes;
250// ABC_FREE( pItem );
251 Extra_MmFixedEntryRecycle( p->pMemMan, pItem );
252}
void Extra_MmFixedEntryRecycle(Extra_MmFixed_t *p, char *pEntry)
Here is the call graph for this function: