ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
rpo.h File Reference
#include "literal.h"
Include dependency graph for rpo.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Rpo_LCI_Edge_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
 INCLUDES ///.
 

Functions

void Rpo_PrintEdge (Rpo_LCI_Edge_t *edge)
 
int Rpo_CheckANDGroup (Literal_t *lit1, Literal_t *lit2, int nVars)
 FUNCTION DEFINITIONS ///.
 
int Rpo_CheckORGroup (Literal_t *lit1, Literal_t *lit2, int nVars)
 
Literal_t * Rpo_Factorize (unsigned *target, int nVars, int nThreshold, int verbose)
 
Literal_t * Rpo_Recursion (unsigned *target, Literal_t **vecLit, int nLit, int nLitCount, int nVars, int *thresholdCount, int thresholdMax, int verbose)
 
Rpo_LCI_Edge_t * Rpo_CreateEdge (Operator_t op, int i, int j, int *vertexDegree)
 
int Rpo_computeMinEdgeCost (Rpo_LCI_Edge_t **edges, int edgeCount, int *vertexDegree)
 

Typedef Documentation

◆ Rpo_LCI_Edge_t

typedef typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t

INCLUDES ///.

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

FileName [rpo.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [RPO]

Synopsis [Rpo Header]

Author [Mayler G. A. Martins / Vinicius Callegaro]

Affiliation [UFRGS]

Date [Ver. 1.0. Started - May 08, 2013.]

Revision [

Id
rpo.h,v 1.00 2013/05/08 00:00:00 mgamartins Exp

] DECLARATIONS ///

Definition at line 36 of file rpo.h.

Function Documentation

◆ Rpo_CheckANDGroup()

int Rpo_CheckANDGroup ( Literal_t * lit1,
Literal_t * lit2,
int nVars )

FUNCTION DEFINITIONS ///.

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

Synopsis [Check if two literals are AND-grouped]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file rpo.c.

71 {
72 unsigned* notLit1Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
73 unsigned* notLit2Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
74 unsigned* and1;
75 unsigned* and2;
76 int isZero;
77
78 Kit_TruthNot(notLit1Func, lit1->function, nVars);
79 Kit_TruthNot(notLit2Func, lit2->function, nVars);
80 and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
81 and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
82 Kit_TruthAnd(and1, lit1->transition, notLit2Func, nVars);
83 isZero = Kit_TruthIsConst0(and1, nVars);
84 if (isZero) {
85 Kit_TruthAnd(and2, lit2->transition, notLit1Func, nVars);
86 isZero = Kit_TruthIsConst0(and2, nVars);
87 }
88 ABC_FREE(notLit1Func);
89 ABC_FREE(notLit2Func);
90 ABC_FREE(and1);
91 ABC_FREE(and2);
92 return isZero;
93}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Literal_t_::function
unsigned * function
Definition literal.h:54
Literal_t_::transition
unsigned * transition
Definition literal.h:53
Here is the caller graph for this function:

◆ Rpo_CheckORGroup()

int Rpo_CheckORGroup ( Literal_t * lit1,
Literal_t * lit2,
int nVars )

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

Synopsis [Check if two literals are AND-grouped]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file rpo.c.

106 {
107 unsigned* and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
108 unsigned* and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
109 int isZero;
110 Kit_TruthAnd(and1, lit1->transition, lit2->function, nVars);
111 isZero = Kit_TruthIsConst0(and1, nVars);
112 if (isZero) {
113 Kit_TruthAnd(and2, lit2->transition, lit1->function, nVars);
114 isZero = Kit_TruthIsConst0(and2, nVars);
115 }
116 ABC_FREE(and1);
117 ABC_FREE(and2);
118 return isZero;
119}
Here is the caller graph for this function:

◆ Rpo_computeMinEdgeCost()

int Rpo_computeMinEdgeCost ( Rpo_LCI_Edge_t ** edges,
int edgeCount,
int * vertexDegree )

Definition at line 132 of file rpo.c.

132 {
133 int minCostIndex = -1;
134 int minVertexIndex = -1;
135 unsigned int minCost = ~0;
136 Rpo_LCI_Edge_t* edge;
137 unsigned int edgeCost;
138 int minVertex;
139 int i;
140 for (i = 0; i < edgeCount; ++i) {
141 edge = edges[i];
142 if (!edge->visited) {
143 edgeCost = vertexDegree[edge->idx1] + vertexDegree[edge->idx2];
144 minVertex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2;
145 if (edgeCost < minCost) {
146 minCost = edgeCost;
147 minCostIndex = i;
148 minVertexIndex = minVertex;
149 } else if ((edgeCost == minCost) && minVertex < minVertexIndex) {
150 minCost = edgeCost;
151 minCostIndex = i;
152 minVertexIndex = minVertex;
153 }
154 }
155 }
156 return minCostIndex;
157}
NewBdd::edge
unsigned edge
Definition giaNewBdd.h:40
Rpo_LCI_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
INCLUDES ///.
Definition rpo.h:36
Here is the caller graph for this function:

◆ Rpo_CreateEdge()

Rpo_LCI_Edge_t * Rpo_CreateEdge ( Operator_t op,
int i,
int j,
int * vertexDegree )

Definition at line 121 of file rpo.c.

121 {
122 Rpo_LCI_Edge_t* edge = ABC_ALLOC(Rpo_LCI_Edge_t, 1);
123 edge->connectionType = op;
124 edge->idx1 = i;
125 edge->idx2 = j;
126 edge->visited = 0;
127 vertexDegree[i]++;
128 vertexDegree[j]++;
129 return edge;
130}
Here is the caller graph for this function:

◆ Rpo_Factorize()

Literal_t * Rpo_Factorize ( unsigned * target,
int nVars,
int nThreshold,
int verbose )

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

Synopsis [Test]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file rpo.c.

174 {
175
176 int nLitCap = nVars * 2;
177 int nLit = 0;
178 int w;
179 Literal_t** vecLit;
180 Literal_t* lit;
181 Literal_t* result;
182 int thresholdCount = 0;
183
184 if (Kit_TruthIsConst0(target, nVars)) {
185 return Lit_CreateLiteralConst(target, nVars, 0);
186 } else if (Kit_TruthIsConst1(target, nVars)) {
187 return Lit_CreateLiteralConst(target, nVars, 1);
188 }
189
190 // if (nThreshold == -1) {
191 // nThreshold = nLitCap + nVars;
192 // }
193 if (verbose) {
194 Abc_Print(-2, "Target: ");
195 Lit_PrintTT(target, nVars);
196 Abc_Print(-2, "\n");
197 }
198 vecLit = ABC_ALLOC(Literal_t*, nLitCap);
199
200 for (w = nVars - 1; w >= 0; w--) {
201 lit = Lit_Alloc(target, nVars, w, '+');
202 if (lit != NULL) {
203 vecLit[nLit] = lit;
204 nLit++;
205 }
206 lit = Lit_Alloc(target, nVars, w, '-');
207 if (lit != NULL) {
208 vecLit[nLit] = lit;
209 nLit++;
210 }
211 }
212 if (verbose) {
213 Abc_Print(-2, "Allocated %d literal clusters\n", nLit);
214 }
215
216 result = Rpo_Recursion(target, vecLit, nLit, nLit, nVars, &thresholdCount, nThreshold, verbose);
217
218 //freeing the memory
219 for (w = 0; w < nLit; ++w) {
220 Lit_Free(vecLit[w]);
221 }
222 ABC_FREE(vecLit);
223
224 return result;
225
226}
Literal_t
struct Literal_t_ Literal_t
Definition literal.h:50
Rpo_Recursion
Literal_t * Rpo_Recursion(unsigned *target, Literal_t **vecLit, int nLit, int nLitCount, int nVars, int *thresholdCount, int thresholdMax, int verbose)
Definition rpo.c:228
lit
int lit
Definition satVec.h:130
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rpo_PrintEdge()

void Rpo_PrintEdge ( Rpo_LCI_Edge_t * edge)

Definition at line 159 of file rpo.c.

159 {
160 Abc_Print(-2, "Edge (%d,%d)/%d\n", edge->idx1, edge->idx2, edge->connectionType);
161}

◆ Rpo_Recursion()

Literal_t * Rpo_Recursion ( unsigned * target,
Literal_t ** vecLit,
int nLit,
int nLitCount,
int nVars,
int * thresholdCount,
int thresholdMax,
int verbose )

Definition at line 228 of file rpo.c.

228 {
229 int i, j, k;
230 Literal_t* copyResult;
231 int* vertexDegree;
232 int v;
233 int edgeSize;
234 Rpo_LCI_Edge_t** edges;
235 int edgeCount = 0;
236 int isAnd;
237 int isOr;
238 Rpo_LCI_Edge_t* edge;
239 Literal_t* result = NULL;
240 int edgeIndex;
241 int minLitIndex;
242 int maxLitIndex;
243 Literal_t* oldLit1;
244 Literal_t* oldLit2;
245 Literal_t* newLit;
246
247 *thresholdCount = *thresholdCount + 1;
248 if (*thresholdCount == thresholdMax) {
249 return NULL;
250 }
251 if (verbose) {
252 Abc_Print(-2, "Entering recursion %d\n", *thresholdCount);
253 }
254 // verify if solution is the target or not
255 if (nLitCount == 1) {
256 if (verbose) {
257 Abc_Print(-2, "Checking solution: ");
258 }
259 for (k = 0; k < nLit; ++k) {
260 if (vecLit[k] != NULL) {
261 if (Kit_TruthIsEqual(target, vecLit[k]->function, nVars)) {
262 copyResult = Lit_Copy(vecLit[k], nVars);
263 if (verbose) {
264 Abc_Print(-2, "FOUND!\n", thresholdCount);
265 }
266 thresholdCount = 0; //??
267 return copyResult;
268 }
269 }
270 }
271 if (verbose) {
272 Abc_Print(-2, "FAILED!\n", thresholdCount);
273 }
274 return NULL;
275 }
276
277 vertexDegree = ABC_ALLOC(int, nLit);
278 // if(verbose) {
279 // Abc_Print(-2,"Allocating vertexDegree...\n");
280 // }
281 for (v = 0; v < nLit; v++) {
282 vertexDegree[v] = 0;
283 }
284 // building edges
285 edgeSize = (nLit * (nLit - 1)) / 2;
286 edges = ABC_ALLOC(Rpo_LCI_Edge_t*, edgeSize);
287 if (verbose) {
288 Abc_Print(-2, "Creating Edges: \n");
289 }
290
291 for (i = 0; i < nLit; ++i) {
292 if (vecLit[i] == NULL) {
293 continue;
294 }
295 for (j = i; j < nLit; ++j) {
296 if (vecLit[j] == NULL) {
297 continue;
298 }
299 isAnd = Rpo_CheckANDGroup(vecLit[i], vecLit[j], nVars);
300 isOr = Rpo_CheckORGroup(vecLit[i], vecLit[j], nVars);
301 if (isAnd) {
302 if (verbose) {
303 Abc_Print(-2, "Grouped: ");
304 Lit_PrintExp(vecLit[j]);
305 Abc_Print(-2, " AND ");
306 Lit_PrintExp(vecLit[i]);
307 Abc_Print(-2, "\n");
308 }
309 // add edge
310 edge = Rpo_CreateEdge(LIT_AND, i, j, vertexDegree);
311 edges[edgeCount++] = edge;
312 }
313 if (isOr) {
314 if (verbose) {
315 Abc_Print(-2, "Grouped: ");
316 Lit_PrintExp(vecLit[j]);
317 Abc_Print(-2, " OR ");
318 Lit_PrintExp(vecLit[i]);
319 Abc_Print(-2, "\n");
320 }
321 // add edge
322 edge = Rpo_CreateEdge(LIT_OR, i, j, vertexDegree);
323 edges[edgeCount++] = edge;
324 }
325 }
326 }
327 if (verbose) {
328 Abc_Print(-2, "%d edges created.\n", edgeCount);
329 }
330
331
332 //traverse the edges, grouping new Literal Clusters
333 do {
334 edgeIndex = Rpo_computeMinEdgeCost(edges, edgeCount, vertexDegree);
335 if (edgeIndex < 0) {
336 if (verbose) {
337 Abc_Print(-2, "There is no edges unvisited... Exiting recursion.\n");
338 //exit(-1);
339 }
340 break;
341 //return NULL; // the graph does not have unvisited edges
342 }
343 edge = edges[edgeIndex];
344 edge->visited = 1;
345 //Rpo_PrintEdge(edge);
346 minLitIndex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2;
347 maxLitIndex = (edge->idx1 > edge->idx2) ? edge->idx1 : edge->idx2;
348 oldLit1 = vecLit[minLitIndex];
349 oldLit2 = vecLit[maxLitIndex];
350 newLit = Lit_GroupLiterals(oldLit1, oldLit2, (Operator_t)edge->connectionType, nVars);
351 vecLit[minLitIndex] = newLit;
352 vecLit[maxLitIndex] = NULL;
353
354 if (verbose) {
355 Abc_Print(-2, "New Literal Cluster found: ");
356 Lit_PrintExp(newLit);
357 Abc_Print(-2, " -> ");
358 Lit_PrintTT(newLit->function, nVars);
359 Abc_Print(-2, "\n");
360 }
361 result = Rpo_Recursion(target, vecLit, nLit, (nLitCount - 1), nVars, thresholdCount, thresholdMax, verbose);
362 //independent of result, free the newLit and restore the vector of Literal Clusters
363 Lit_Free(newLit);
364 vecLit[minLitIndex] = oldLit1;
365 vecLit[maxLitIndex] = oldLit2;
366 if (*thresholdCount == thresholdMax) {
367 break;
368 }
369 } while (result == NULL);
370 //freeing memory
371 // if(verbose) {
372 // Abc_Print(-2,"Freeing vertexDegree...\n");
373 // }
374 ABC_FREE(vertexDegree);
375 for (i = 0; i < edgeCount; ++i) {
376 //Abc_Print(-2, "%p ", edges[i]);
377 ABC_FREE(edges[i]);
378 }
379 ABC_FREE(edges);
380 return result;
381}
Operator_t
Operator_t
INCLUDES ///.
Definition literal.h:42
LIT_OR
@ LIT_OR
Definition literal.h:45
LIT_AND
@ LIT_AND
Definition literal.h:44
Rpo_CheckANDGroup
int Rpo_CheckANDGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
FUNCTION DEFINITIONS ///.
Definition rpo.c:71
Rpo_CreateEdge
Rpo_LCI_Edge_t * Rpo_CreateEdge(Operator_t op, int i, int j, int *vertexDegree)
Definition rpo.c:121
Rpo_CheckORGroup
int Rpo_CheckORGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
Definition rpo.c:106
Rpo_computeMinEdgeCost
int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t **edges, int edgeCount, int *vertexDegree)
Definition rpo.c:132
Here is the call graph for this function:
Here is the caller graph for this function: