ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
dsc.c File Reference
#include "dsc.h"
#include <assert.h>
#include "misc/util/utilTruth.h"
Include dependency graph for dsc.c:

Go to the source code of this file.

Classes

struct  Dsc_node_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Dsc_node_t_ Dsc_node_t
 DECLARATIONS ///.
 

Functions

void dsc_and_group (Dsc_node_t *pOut, Dsc_node_t *ni, int niPolarity, Dsc_node_t *nj, int njPolarity, int nVars, const int TRUTH_WORDS)
 
void dsc_xor_group (Dsc_node_t *pOut, Dsc_node_t *ni, Dsc_node_t *nj, int nVars, const int TRUTH_WORDS)
 
word * Dsc_alloc_pool (int nVars)
 BASIC TYPES ///.
 
void Dsc_free_pool (word *pool)
 
int Dsc_Decompose (word *pTruth, const int nVarsInit, char *const pRes, word *pool)
 
int * Dsc_ComputeMatches (char *p)
 
int Dsc_CountAnds_rec (char *pStr, char **p, int *pMatches)
 
int Dsc_CountAnds (char *pDsd)
 

Typedef Documentation

◆ Dsc_node_t

typedef typedefABC_NAMESPACE_IMPL_START struct Dsc_node_t_ Dsc_node_t

DECLARATIONS ///.

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

FileName [dsc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Disjoint support decomposition - ICCD'15]

Synopsis [Disjoint-support decomposition with cofactoring and boolean difference analysis from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis, "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]

Author [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]

Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]

Date [Ver. 1.0. Started - October 24, 2014.]

Revision [

Id
dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp

]

Definition at line 39 of file dsc.c.

Function Documentation

◆ Dsc_alloc_pool()

word * Dsc_alloc_pool ( int nVars)
extern

BASIC TYPES ///.

memory allocator with a capacity of storing 3*nVars truth-tables for negative and positive cofactors and the boolean difference for each input variable

Definition at line 290 of file dsc.c.

290 {
291 return ABC_ALLOC(word, 3 * Abc_TtWordNum(nVars) * nVars);
292}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Here is the caller graph for this function:

◆ dsc_and_group()

void dsc_and_group ( Dsc_node_t * pOut,
Dsc_node_t * ni,
int niPolarity,
Dsc_node_t * nj,
int njPolarity,
int nVars,
const int TRUTH_WORDS )

Definition at line 129 of file dsc.c.

129 {
130 unsigned int* xiOFF, * xiON, * xjOFF, * xjON;
131 // expression
132 concat(pOut->exp, '(', ')', ni->exp, niPolarity, nj->exp, njPolarity);
133 // ON-OFF
134 if (niPolarity) {
135 xiOFF = ni->off;
136 xiON = ni->on;
137 } else {
138 xiOFF = ni->on;
139 xiON = ni->off;
140 }
141 if (njPolarity) {
142 xjOFF = nj->off;
143 xjON = nj->on;
144 } else {
145 xjOFF = nj->on;
146 xjON = nj->off;
147 }
148 // creating both the new OFF specification and negative cofactor of the new group
149 {
150 // first element of the array represents the size of the cube-cofactor
151 int xiOFFSize = xiOFF[0];
152 int xjOFFSize = xjOFF[0];
153 if (xiOFFSize <= xjOFFSize) {
154 int i;
155 pOut->off[0] = xiOFFSize; // set the number of elements
156 for (i = 1; i <= xiOFFSize; i++) {
157 pOut->off[i] = xiOFF[i];
158 }
159 } else {
160 int i;
161 pOut->off[0] = xjOFFSize; // set the number of elements
162 for (i = 1; i <= xjOFFSize; i++) {
163 pOut->off[i] = xjOFF[i];
164 }
165 }
166 // set the negative cofactor of the new group
167 pOut->pNegCof = niPolarity ? ni->pNegCof : ni->pPosCof;
168 }
169 // creating both new ON specification and positive cofactor of the new group
170 {
171 int i;
172 int j;
173 unsigned int xiONSize = xiON[0];
174 unsigned int xjONSize = xjON[0];
175 pOut->on[0] = xiONSize + xjONSize;
176 for (i = 1; i <= (int)xiONSize; i++) {
177 pOut->on[i] = xiON[i];
178 }
179 for (j = 1; j <= (int)xjONSize; j++) {
180 pOut->on[i++] = xjON[j];
181 }
182 // set the positive cofactor of the new group
183 if (xiONSize >= xjONSize) {
184 pOut->pPosCof = niPolarity ? ni->pPosCof : ni->pNegCof;
185 cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
186 } else {
187 pOut->pPosCof = njPolarity ? nj->pPosCof : nj->pNegCof;
188 cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
189 }
190 }
191 // set the boolean difference of the new group
192 pOut->pBoolDiff = njPolarity ? nj->pNegCof : nj->pPosCof;
193 xorInPlace(pOut->pBoolDiff, pOut->pPosCof, TRUTH_WORDS);
194}
Here is the caller graph for this function:

◆ Dsc_ComputeMatches()

int * Dsc_ComputeMatches ( char * p)

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 450 of file dsc.c.

451{
452 static int pMatches[DSC_MAX_VAR];
453 int pNested[DSC_MAX_VAR];
454 int v, nNested = 0;
455 for ( v = 0; p[v]; v++ )
456 {
457 pMatches[v] = 0;
458 if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
459 pNested[nNested++] = v;
460 else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
461 pMatches[pNested[--nNested]] = v;
462 assert( nNested < DSC_MAX_VAR );
463 }
464 assert( nNested == 0 );
465 return pMatches;
466}
DSC_MAX_VAR
#define DSC_MAX_VAR
INCLUDES ///.
Definition dsc.h:40
p
Cube * p
Definition exorList.c:222
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Dsc_CountAnds()

int Dsc_CountAnds ( char * pDsd)
extern

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 513 of file dsc.c.

514{
515 if ( pDsd[1] == 0 )
516 return 0;
517 return Dsc_CountAnds_rec( pDsd, &pDsd, Dsc_ComputeMatches(pDsd) );
518}
Dsc_ComputeMatches
int * Dsc_ComputeMatches(char *p)
Definition dsc.c:450
Dsc_CountAnds_rec
int Dsc_CountAnds_rec(char *pStr, char **p, int *pMatches)
Definition dsc.c:472
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dsc_CountAnds_rec()

int Dsc_CountAnds_rec ( char * pStr,
char ** p,
int * pMatches )

Function************************************************************* Synopsis [DSD formula manipulation.] Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]

Definition at line 472 of file dsc.c.

473{
474 if ( **p == '!' )
475 (*p)++;
476 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
477 (*p)++;
478 if ( **p == '<' )
479 {
480 char * q = pStr + pMatches[*p - pStr];
481 if ( *(q+1) == '{' )
482 *p = q+1;
483 }
484 if ( **p >= 'a' && **p <= 'z' ) // var
485 return 0;
486 if ( **p == '(' || **p == '[' ) // and/or/xor
487 {
488 int Counter = 0, AddOn = (**p == '(')? 1 : 3;
489 char * q = pStr + pMatches[ *p - pStr ];
490 assert( *q == **p + 1 + (**p != '(') );
491 for ( (*p)++; *p < q; (*p)++ )
492 Counter += AddOn + Dsc_CountAnds_rec( pStr, p, pMatches );
493 assert( *p == q );
494 return Counter - AddOn;
495 }
496 if ( **p == '<' || **p == '{' ) // mux
497 {
498 int Counter = 3;
499 char * q = pStr + pMatches[ *p - pStr ];
500 assert( *q == **p + 1 + (**p != '(') );
501 for ( (*p)++; *p < q; (*p)++ )
502 Counter += Dsc_CountAnds_rec( pStr, p, pMatches );
503 assert( *p == q );
504 return Counter;
505 }
506 assert( 0 );
507 return 0;
508}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dsc_Decompose()

int Dsc_Decompose ( word * pTruth,
const int nVarsInit,
char *const pRes,
word * pool )
extern

This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis, entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015. pTruth: pointer for the truth table representing the target function. nVarsInit: the number of variables of the truth table of the target function. pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found. pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call. (the results presented on ICCD paper are running this method with NULL for the memory pool). The method returns 0 if a full decomposition was found and a negative value otherwise.

Definition at line 311 of file dsc.c.

311 {
312 const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
313 const int NEED_POOL_ALLOC = (pool == NULL);
314
315 Dsc_node_t nodes[DSC_MAX_VAR];
316 Dsc_node_t *newNodes[DSC_MAX_VAR];
317 Dsc_node_t *oldNodes[DSC_MAX_VAR];
318
319 Dsc_node_t freeNodes[DSC_MAX_VAR]; // N is the maximum number of possible groups.
320 int f = 0; // f represent the next free position in the freeNodes array
321 int o = 0; // o stands for the number of already tested nodes
322 int n = 0; // n will represent the number of current nodes (i.e. support)
323
324 pRes[0] = '\0';
325 pRes[1] = '\0';
326
327 if (NEED_POOL_ALLOC)
328 pool = ABC_ALLOC(word, 3 * TRUTH_WORDS * nVarsInit);
329
330 // block for the node data allocation
331 {
332 // pointer for the next free truth word
333 word *pNextTruth = pool;
334 int iVar;
335 for (iVar = 0; iVar < nVarsInit; iVar++) {
336 // negative cofactor
337 Abc_TtCofactor0p(pNextTruth, pTruth, TRUTH_WORDS, iVar);
338 // dont care test
339 if (!Abc_TtEqual(pNextTruth, pTruth, TRUTH_WORDS)) {
340 Dsc_node_t *node = &nodes[iVar];
341 node->pNegCof = pNextTruth;
342 // increment next truth pointer
343 pNextTruth += TRUTH_WORDS;
344 // positive cofactor
345 node->pPosCof = pNextTruth;
346 Abc_TtCofactor1p(node->pPosCof, pTruth, TRUTH_WORDS, iVar);
347 // increment next truth pointer
348 pNextTruth += TRUTH_WORDS;
349 // boolean difference
350 node->pBoolDiff = pNextTruth;
351 Abc_TtXor(node->pBoolDiff, node->pNegCof, node->pPosCof, TRUTH_WORDS, 0);
352 // increment next truth pointer
353 pNextTruth += TRUTH_WORDS;
354 // define on spec -
355 node->on[0] = 1; node->on[1] = (iVar << 1) | 1u; // lit = i*2+1, when polarity=true
356 // define off spec
357 node->off[0] = 1; node->off[1] = iVar << 1;// lit=i*2 otherwise
358 // store the node expression
359 node->exp[0] = 'a'+iVar; // TODO fix the variable names
360 node->exp[1] = '\0';
361 // add the node to the newNodes array
362 newNodes[n++] = node;
363 }
364 }
365 }
366 //const int initialSupport = n;
367 if (n == 0) {
368 if (NEED_POOL_ALLOC)
369 ABC_FREE(pool);
370 if (Abc_TtIsConst0(pTruth, TRUTH_WORDS)) {
371 { if ( pRes ) pRes[0] = '0', pRes[1] = '\0'; }
372 return 0;
373 } else if (Abc_TtIsConst1(pTruth, TRUTH_WORDS)) {
374 { if ( pRes ) pRes[0] = '1', pRes[1] = '\0'; }
375 return 0;
376 } else {
377 Abc_Print(-1, "ERROR. No variable in the support of f, but f isn't constant!\n");
378 return -1;
379 }
380 }
381 while (n > 0) {
382 int tempN = 0;
383 int i, j, iPolarity, jPolarity;
384 Dsc_node_t *ni, *nj, *newNode = NULL;
385 for (i = 0; i < n; i++) {
386 ni = newNodes[i];
387 newNode = NULL;
388 j = 0;
389 while (j < o) {
390 nj = oldNodes[j];
391 if (dsc_and_test(ni, nj, TRUTH_WORDS, &iPolarity, &jPolarity)) {
392 newNode = &freeNodes[f++];
393 dsc_and_group(newNode, ni, iPolarity, nj, jPolarity, nVarsInit, TRUTH_WORDS);
394 }
395 // XOR test
396 if ((newNode == NULL) && (dsc_xor_test(ni, nj, TRUTH_WORDS))) {
397 newNode = &freeNodes[f++];
398 dsc_xor_group(newNode, ni, nj, nVarsInit, TRUTH_WORDS);
399 }
400 if (newNode != NULL) {
401 oldNodes[j] = oldNodes[--o];
402 break;
403 } else {
404 j++;
405 }
406 }
407 if (newNode != NULL) {
408 newNodes[tempN++] = newNode;
409 } else {
410 oldNodes[o++] = ni;
411 }
412 }
413 n = tempN;
414 }
415 if (o == 1) {
416 Dsc_node_t * solution = oldNodes[0];
417 if (Abc_TtIsConst0(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst1(solution->pPosCof, TRUTH_WORDS)) {
418 // Direct solution found
419 if ( pRes )
420 strcpy( pRes, solution->exp);
421 if (NEED_POOL_ALLOC)
422 ABC_FREE(pool);
423 return 0;
424 } else if (Abc_TtIsConst1(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst0(solution->pPosCof, TRUTH_WORDS)) {
425 // Complementary solution found
426 if ( pRes ) {
427 pRes[0] = '!';
428 strcpy( &pRes[1], solution->exp);
429 }
430 if (NEED_POOL_ALLOC)
431 ABC_FREE(pool);
432 return 0;
433 } else {
434 printf("DSC ERROR: Final DSC node found, but differs from target function.\n");
435 if (NEED_POOL_ALLOC)
436 ABC_FREE(pool);
437 return -1;
438 }
439 }
440 if (NEED_POOL_ALLOC)
441 ABC_FREE(pool);
442 return -1;
443}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
dsc_xor_group
void dsc_xor_group(Dsc_node_t *pOut, Dsc_node_t *ni, Dsc_node_t *nj, int nVars, const int TRUTH_WORDS)
Definition dsc.c:196
Dsc_node_t
typedefABC_NAMESPACE_IMPL_START struct Dsc_node_t_ Dsc_node_t
DECLARATIONS ///.
Definition dsc.c:39
dsc_and_group
void dsc_and_group(Dsc_node_t *pOut, Dsc_node_t *ni, int niPolarity, Dsc_node_t *nj, int njPolarity, int nVars, const int TRUTH_WORDS)
Definition dsc.c:129
strcpy
char * strcpy()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dsc_free_pool()

void Dsc_free_pool ( word * pool)
extern

just free the memory pool

Definition at line 297 of file dsc.c.

297 {
298 ABC_FREE(pool);
299}
Here is the caller graph for this function:

◆ dsc_xor_group()

void dsc_xor_group ( Dsc_node_t * pOut,
Dsc_node_t * ni,
Dsc_node_t * nj,
int nVars,
const int TRUTH_WORDS )

Definition at line 196 of file dsc.c.

196 {
197 //
198 const unsigned int * xiOFF = ni->off;
199 const unsigned int * xiON = ni->on;
200 const unsigned int * xjOFF = nj->off;
201 const unsigned int * xjON = nj->on;
202 //
203 const int xiOFFSize = xiOFF[0];
204 const int xiONSize = xiON[0];
205 const int xjOFFSize = xjOFF[0];
206 const int xjONSize = xjON[0];
207 // minCubeCofs
208 int minCCSize = xiOFFSize;
209 int minCCPolarity = 0;
210 Dsc_node_t * minCCNode = ni;
211 // expression
212 concat(pOut->exp, '[', ']', ni->exp, 1, nj->exp, 1);
213 if (minCCSize > xiONSize) {
214 minCCSize = xiONSize;
215 minCCPolarity = 1;
216 //minCCNode = ni;
217 }
218 if (minCCSize > xjOFFSize) {
219 minCCSize = xjOFFSize;
220 minCCPolarity = 0;
221 minCCNode = nj;
222 }
223 if (minCCSize > xjONSize) {
224 minCCSize = xjONSize;
225 minCCPolarity = 1;
226 minCCNode = nj;
227 }
228 //
229 if (minCCNode == ni) {
230 if (minCCPolarity) {
231 // gOFF = xiON, xjON
232 pOut->pNegCof = nj->pPosCof;
233 cubeCofactor(pOut->pNegCof, xiON, TRUTH_WORDS);
234 // gON = xiON, xjOFF
235 pOut->pPosCof = nj->pNegCof;
236 cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
237 } else {
238 // gOFF = xiOFF, xjOFF
239 pOut->pNegCof = nj->pNegCof;
240 cubeCofactor(pOut->pNegCof, xiOFF, TRUTH_WORDS);
241 // gON = xiOFF, xjON
242 pOut->pPosCof = nj->pPosCof;
243 cubeCofactor(pOut->pPosCof, xiOFF, TRUTH_WORDS);
244 }
245 }else {
246 if (minCCPolarity) {
247 // gOFF = xjON, xiON
248 pOut->pNegCof = ni->pPosCof;
249 cubeCofactor(pOut->pNegCof, xjON, TRUTH_WORDS);
250 // gON = xjON, xiOFF
251 pOut->pPosCof = ni->pNegCof;
252 cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
253 } else {
254 // gOFF = xjOFF, xiOFF
255 pOut->pNegCof = ni->pNegCof;
256 cubeCofactor(pOut->pNegCof, xjOFF, TRUTH_WORDS);
257 // gON = xjOFF, xiON
258 pOut->pPosCof = ni->pPosCof;
259 cubeCofactor(pOut->pPosCof, xjOFF, TRUTH_WORDS);
260 }
261 }
262 // bool diff
263 pOut->pBoolDiff = ni->pBoolDiff;
264 // evaluating specs
265 // off spec
266 pOut->off[0] = 0;
267 if ((xiOFFSize+xjOFFSize) <= (xiONSize+xjONSize)) {
268 merge(pOut->off, xiOFF);
269 merge(pOut->off, xjOFF);
270 } else {
271 merge(pOut->off, xiON);
272 merge(pOut->off, xjON);
273 }
274 // on spec
275 pOut->on[0] = 0;
276 if ((xiOFFSize+xjONSize) <= (xiONSize+xjOFFSize)) {
277 merge(pOut->on, xiOFF);
278 merge(pOut->on, xjON);
279 } else {
280 merge(pOut->on, xiON);
281 merge(pOut->on, xjOFF);
282 }
283}
Here is the caller graph for this function: