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

Go to the source code of this file.

Classes

struct  Dau_Sto_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Dau_Sto_t_ Dau_Sto_t
 DECLARATIONS ///.
 

Functions

int Dau_DsdMergeStatus_rec (char *pStr, char **p, int *pMatches, int nShared, int *pStatus)
 
void Dau_DsdMergeSubstitute_rec (Dau_Sto_t *pS, char *pStr, char **p, int *pMatches, int *pStatus, int fWrite)
 
void Dau_DsdRemoveBraces_rec (char *pStr, char **p, int *pMatches)
 
void Dau_DsdRemoveBraces (char *pDsd, int *pMatches)
 
char * Dau_DsdMerge (char *pDsd0i, int *pPerm0, char *pDsd1i, int *pPerm1, int fCompl0, int fCompl1, int nVars)
 DECLARATIONS ///.
 
void Dau_DsdTest66 ()
 

Variables

abctime s_TimeComp [4] = {0}
 

Typedef Documentation

◆ Dau_Sto_t

typedef typedefABC_NAMESPACE_IMPL_START struct Dau_Sto_t_ Dau_Sto_t

DECLARATIONS ///.

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

FileName [dauMerge.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware unmapping.]

Synopsis [Enumeration of decompositions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
dauMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Substitution storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file dauMerge.c.

Function Documentation

◆ Dau_DsdMerge()

char * Dau_DsdMerge ( char * pDsd0i,
int * pPerm0,
char * pDsd1i,
int * pPerm1,
int fCompl0,
int fCompl1,
int nVars )

DECLARATIONS ///.

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

Synopsis [Performs merging of two DSD formulas.]

Description []

SideEffects []

SeeAlso []

Definition at line 587 of file dauMerge.c.

588{
589 int fVerbose = 0;
590 int fCheck = 0;
591 static int Counter = 0;
592 static char pRes[2*DAU_MAX_STR+10];
593 char pDsd0[DAU_MAX_STR];
594 char pDsd1[DAU_MAX_STR];
595 int pMatches0[DAU_MAX_STR];
596 int pMatches1[DAU_MAX_STR];
597 int pVarPres[DAU_MAX_VAR];
598 int pOld2New[DAU_MAX_VAR];
599 int pNew2Old[DAU_MAX_VAR];
600 int pStatus0[DAU_MAX_STR];
601 int pStatus1[DAU_MAX_STR];
602 int pMatches[DAU_MAX_STR];
603 int nVarsShared, nVarsTotal;
604 Dau_Sto_t S, * pS = &S;
605 word * pTruth, * pt = NULL, * pt0 = NULL, * pt1 = NULL;
606 word pParts[3][DAU_MAX_WORD];
607 int Status;
608 abctime clk = Abc_Clock();
609 Counter++;
610 // create local copies
611 Dau_DsdMergeCopy( pDsd0i, fCompl0, pDsd0 );
612 Dau_DsdMergeCopy( pDsd1i, fCompl1, pDsd1 );
613if ( fVerbose )
614printf( "\nAfter copying:\n" );
615if ( fVerbose )
616printf( "%s\n", pDsd0 );
617if ( fVerbose )
618printf( "%s\n", pDsd1 );
619 // handle constants
620 if ( Dau_DsdIsConst(pDsd0) || Dau_DsdIsConst(pDsd1) )
621 {
622 if ( Dau_DsdIsConst0(pDsd0) )
623 strcpy( pRes, pDsd0 );
624 else if ( Dau_DsdIsConst1(pDsd0) )
625 strcpy( pRes, pDsd1 );
626 else if ( Dau_DsdIsConst0(pDsd1) )
627 strcpy( pRes, pDsd1 );
628 else if ( Dau_DsdIsConst1(pDsd1) )
629 strcpy( pRes, pDsd0 );
630 else assert( 0 );
631 return pRes;
632 }
633
634 // compute matches
635 Dau_DsdMergeMatches( pDsd0, pMatches0 );
636 Dau_DsdMergeMatches( pDsd1, pMatches1 );
637 // implement permutation
638 Dau_DsdMergeReplace( pDsd0, pMatches0, pPerm0 );
639 Dau_DsdMergeReplace( pDsd1, pMatches1, pPerm1 );
640if ( fVerbose )
641printf( "After replacement:\n" );
642if ( fVerbose )
643printf( "%s\n", pDsd0 );
644if ( fVerbose )
645printf( "%s\n", pDsd1 );
646
647
648 if ( fCheck )
649 {
650 pt0 = Dau_DsdToTruth( pDsd0, nVars );
651 Abc_TtCopy( pParts[0], pt0, Abc_TtWordNum(nVars), 0 );
652 }
653 if ( fCheck )
654 {
655 pt1 = Dau_DsdToTruth( pDsd1, nVars );
656 Abc_TtCopy( pParts[1], pt1, Abc_TtWordNum(nVars), 0 );
657 Abc_TtAnd( pParts[2], pParts[0], pParts[1], Abc_TtWordNum(nVars), 0 );
658 }
659
660 // find shared varaiables
661 nVarsShared = Dau_DsdMergeFindShared(pDsd0, pDsd1, pMatches0, pMatches1, pVarPres);
662 if ( nVarsShared == 0 )
663 {
664 sprintf( pRes, "(%s%s)", pDsd0, pDsd1 );
665if ( fVerbose )
666printf( "Disjoint:\n" );
667if ( fVerbose )
668printf( "%s\n", pRes );
669
670 Dau_DsdMergeMatches( pRes, pMatches );
671 Dau_DsdRemoveBraces( pRes, pMatches );
672 Dau_DsdNormalize( pRes );
673if ( fVerbose )
674printf( "Normalized:\n" );
675if ( fVerbose )
676printf( "%s\n", pRes );
677
678 s_TimeComp[0] += Abc_Clock() - clk;
679 return pRes;
680 }
681s_TimeComp[3] += Abc_Clock() - clk;
682 // create variable mapping
683 nVarsTotal = Dau_DsdMergeCreateMaps( pVarPres, nVarsShared, pOld2New, pNew2Old );
684 // perform variable replacement
685 Dau_DsdMergeReplace( pDsd0, pMatches0, pOld2New );
686 Dau_DsdMergeReplace( pDsd1, pMatches1, pOld2New );
687 // find uniqueness status
688 Dau_DsdMergeStatus( pDsd0, pMatches0, nVarsShared, pStatus0 );
689 Dau_DsdMergeStatus( pDsd1, pMatches1, nVarsShared, pStatus1 );
690if ( fVerbose )
691printf( "Individual status:\n" );
692if ( fVerbose )
693Dau_DsdMergePrintWithStatus( pDsd0, pStatus0 );
694if ( fVerbose )
695Dau_DsdMergePrintWithStatus( pDsd1, pStatus1 );
696 // prepare storage
697 Dau_DsdMergeStoreClean( pS, nVarsShared );
698 // perform substitutions
699 Dau_DsdMergeStoreCleanOutput( pS );
700 Dau_DsdMergeSubstitute( pS, pDsd0, pMatches0, pStatus0 );
701 strcpy( pDsd0, pS->pOutput );
702if ( fVerbose )
703printf( "Substitutions:\n" );
704if ( fVerbose )
705printf( "%s\n", pDsd0 );
706
707 // perform substitutions
708 Dau_DsdMergeStoreCleanOutput( pS );
709 Dau_DsdMergeSubstitute( pS, pDsd1, pMatches1, pStatus1 );
710 strcpy( pDsd1, pS->pOutput );
711if ( fVerbose )
712printf( "%s\n", pDsd1 );
713if ( fVerbose )
714Dau_DsdMergeStorePrintDefs( pS );
715
716 // create new function
717// assert( nVarsTotal <= 6 );
718 sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
719 pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
720 Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput );
721//printf( "%d ", Status );
722 if ( Status == -1 ) // did not find 1-step DSD
723 return NULL;
724// if ( Status > 6 ) // non-DSD part is too large
725// return NULL;
726 if ( Dau_DsdIsConst(pS->pOutput) )
727 {
728 strcpy( pRes, pS->pOutput );
729 return pRes;
730 }
731if ( fVerbose )
732printf( "Decomposition:\n" );
733if ( fVerbose )
734printf( "%s\n", pS->pOutput );
735 // substitute definitions
736 Dau_DsdMergeMatches( pS->pOutput, pMatches );
737 Dau_DsdMergeInlineDefinitions( pS->pOutput, pMatches, pS, pRes, nVarsShared );
738if ( fVerbose )
739printf( "Inlining:\n" );
740if ( fVerbose )
741printf( "%s\n", pRes );
742 // perform variable replacement
743 Dau_DsdMergeMatches( pRes, pMatches );
744 Dau_DsdMergeReplace( pRes, pMatches, pNew2Old );
745 Dau_DsdRemoveBraces( pRes, pMatches );
746if ( fVerbose )
747printf( "Replaced:\n" );
748if ( fVerbose )
749printf( "%s\n", pRes );
750 Dau_DsdNormalize( pRes );
751if ( fVerbose )
752printf( "Normalized:\n" );
753if ( fVerbose )
754printf( "%s\n", pRes );
755
756 if ( fCheck )
757 {
758 pt = Dau_DsdToTruth( pRes, nVars );
759 if ( !Abc_TtEqual( pParts[2], pt, Abc_TtWordNum(nVars) ) )
760 printf( "Dau_DsdMerge(): Verification failed!\n" );
761 }
762
763 if ( Status == 0 )
764 s_TimeComp[1] += Abc_Clock() - clk;
765 else
766 s_TimeComp[2] += Abc_Clock() - clk;
767 return pRes;
768}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
s_TimeComp
abctime s_TimeComp[4]
Definition dauMerge.c:574
Dau_Sto_t
typedefABC_NAMESPACE_IMPL_START struct Dau_Sto_t_ Dau_Sto_t
DECLARATIONS ///.
Definition dauMerge.c:47
Dau_DsdRemoveBraces
void Dau_DsdRemoveBraces(char *pDsd, int *pMatches)
Definition dauMerge.c:554
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition dauDsd.c:609
DAU_MAX_WORD
#define DAU_MAX_WORD
Definition dau.h:44
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition dauDsd.c:1912
Dau_DsdNormalize
void Dau_DsdNormalize(char *p)
Definition dauDsd.c:260
DAU_MAX_STR
#define DAU_MAX_STR
Definition dau.h:43
DAU_MAX_VAR
#define DAU_MAX_VAR
INCLUDES ///.
Definition dau.h:42
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
sprintf
char * sprintf()
strcpy
char * strcpy()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dau_DsdMergeStatus_rec()

int Dau_DsdMergeStatus_rec ( char * pStr,
char ** p,
int * pMatches,
int nShared,
int * pStatus )

Definition at line 289 of file dauMerge.c.

290{
291 // none pure
292 // 1 one pure
293 // 2 two or more pure
294 // 3 all pure
295 if ( **p == '!' )
296 {
297 pStatus[*p - pStr] = -1;
298 (*p)++;
299 }
300 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
301 {
302 pStatus[*p - pStr] = -1;
303 (*p)++;
304 }
305 if ( **p == '<' )
306 {
307 char * q = pStr + pMatches[ *p - pStr ];
308 if ( *(q+1) == '{' )
309 {
310 char * pTemp = *p;
311 *p = q+1;
312 for ( ; pTemp < q+1; pTemp++ )
313 pStatus[pTemp - pStr] = -1;
314 }
315 }
316 if ( **p >= 'a' && **p <= 'z' ) // var
317 return pStatus[*p - pStr] = (**p - 'a' < nShared) ? 0 : 3;
318 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
319 {
320 int Status, nPure = 0, nTotal = 0;
321 char * pOld = *p;
322 char * q = pStr + pMatches[ *p - pStr ];
323 assert( *q == **p + 1 + (**p != '(') );
324 for ( (*p)++; *p < q; (*p)++ )
325 {
326 Status = Dau_DsdMergeStatus_rec( pStr, p, pMatches, nShared, pStatus );
327 nPure += (Status == 3);
328 nTotal++;
329 }
330 assert( *p == q );
331 assert( nTotal > 1 );
332 if ( nPure == 0 )
333 Status = 0;
334 else if ( nPure == 1 )
335 Status = 1;
336 else if ( nPure < nTotal )
337 Status = 2;
338 else if ( nPure == nTotal )
339 Status = 3;
340 else assert( 0 );
341 return (pStatus[pOld - pStr] = Status);
342 }
343 assert( 0 );
344 return 0;
345}
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Dau_DsdMergeStatus_rec
int Dau_DsdMergeStatus_rec(char *pStr, char **p, int *pMatches, int nShared, int *pStatus)
Definition dauMerge.c:289
p
Cube * p
Definition exorList.c:222
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dau_DsdMergeSubstitute_rec()

void Dau_DsdMergeSubstitute_rec ( Dau_Sto_t * pS,
char * pStr,
char ** p,
int * pMatches,
int * pStatus,
int fWrite )

Definition at line 376 of file dauMerge.c.

377{
378// assert( **p != '!' );
379
380 if ( **p == '!' )
381 {
382 if ( fWrite )
383 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
384 (*p)++;
385 }
386
387 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
388 {
389 if ( fWrite )
390 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
391 (*p)++;
392 }
393 if ( **p == '<' )
394 {
395 char * q = pStr + pMatches[ *p - pStr ];
396 if ( *(q+1) == '{' )
397 {
398 char * pTemp = *p;
399 *p = q+1;
400 if ( fWrite )
401 for ( ; pTemp < q+1; pTemp++ )
402 Dau_DsdMergeStoreAddToOutputChar( pS, *pTemp );
403 }
404 }
405 if ( **p >= 'a' && **p <= 'z' ) // var
406 {
407 if ( fWrite )
408 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
409 return;
410 }
411 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
412 {
413 int New, StatusFan, Status = pStatus[*p - pStr];
414 char * pBeg, * q = pStr + pMatches[ *p - pStr ];
415 assert( *q == **p + 1 + (**p != '(') );
416 if ( !fWrite )
417 {
418 assert( Status == 3 );
419 *p = q;
420 return;
421 }
422 assert( Status != 3 );
423 if ( Status == 0 ) // none pure
424 {
425 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
426 for ( (*p)++; *p < q; (*p)++ )
427 {
428 if ( **p == '!' )
429 {
430 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
431 (*p)++;
432 }
433 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, 1 );
434 }
435 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
436 assert( *p == q );
437 return;
438 }
439 if ( Status == 1 || **p == '<' || **p == '{' ) // 1 pure
440 {
441 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
442 for ( (*p)++; *p < q; (*p)++ )
443 {
444 if ( **p == '!' )
445 {
446 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
447 (*p)++;
448 }
449 pBeg = *p;
450 StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
451 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
452 if ( StatusFan == 3 )
453 {
454 int New = Dau_DsdMergeStoreCreateDef( pS, pBeg, *p+1 );
455 Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
456 }
457 }
458 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
459 assert( *p == q );
460 return;
461 }
462 if ( Status == 2 )
463 {
464 // add more than one defs
465 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
466 New = Dau_DsdMergeStoreStartDef( pS, **p );
467 for ( (*p)++; *p < q; (*p)++ )
468 {
469 pBeg = *p;
470 StatusFan = Dau_DsdMergeGetStatus( pBeg, pStr, pMatches, pStatus );
471 if ( **p == '!' )
472 {
473 if ( StatusFan != 3 )
474 Dau_DsdMergeStoreAddToOutputChar( pS, '!' );
475 else
476 Dau_DsdMergeStoreAddToDefChar( pS, New, '!' );
477 (*p)++;
478 pBeg++;
479 }
480 Dau_DsdMergeSubstitute_rec( pS, pStr, p, pMatches, pStatus, StatusFan != 3 );
481 if ( StatusFan == 3 )
482 Dau_DsdMergeStoreAddToDef( pS, New, pBeg, *p+1 );
483 }
484 Dau_DsdMergeStoreStopDef( pS, New, *q );
485 Dau_DsdMergeStoreAddToOutputChar( pS, (char)('a' + New) );
486 Dau_DsdMergeStoreAddToOutputChar( pS, **p );
487 return;
488 }
489 assert( 0 );
490 return;
491 }
492 assert( 0 );
493}
Dau_DsdMergeSubstitute_rec
void Dau_DsdMergeSubstitute_rec(Dau_Sto_t *pS, char *pStr, char **p, int *pMatches, int *pStatus, int fWrite)
Definition dauMerge.c:376
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dau_DsdRemoveBraces()

void Dau_DsdRemoveBraces ( char * pDsd,
int * pMatches )

Definition at line 554 of file dauMerge.c.

555{
556 char * q, * p = pDsd;
557 if ( pDsd[1] == 0 )
558 return;
559 Dau_DsdRemoveBraces_rec( pDsd, &pDsd, pMatches );
560 for ( q = p; *p; p++ )
561 if ( *p != ' ' )
562 {
563 if ( *p == '!' && p != q && *(q-1) == '!' )
564 {
565 q--;
566 continue;
567 }
568 *q++ = *p;
569 }
570 *q = 0;
571}
Dau_DsdRemoveBraces_rec
void Dau_DsdRemoveBraces_rec(char *pStr, char **p, int *pMatches)
Definition dauMerge.c:520
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dau_DsdRemoveBraces_rec()

void Dau_DsdRemoveBraces_rec ( char * pStr,
char ** p,
int * pMatches )

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

Synopsis [Removes braces.]

Description []

SideEffects []

SeeAlso []

Definition at line 520 of file dauMerge.c.

521{
522 if ( **p == '!' )
523 (*p)++;
524 while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
525 (*p)++;
526 if ( **p == '<' )
527 {
528 char * q = pStr + pMatches[*p - pStr];
529 if ( *(q+1) == '{' )
530 *p = q+1;
531 }
532 if ( **p >= 'a' && **p <= 'z' ) // var
533 return;
534 if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' )
535 {
536 char * q = pStr + pMatches[ *p - pStr ];
537 assert( *q == **p + 1 + (**p != '(') );
538 for ( (*p)++; *p < q; (*p)++ )
539 {
540 int fCompl = (**p == '!');
541 char * pBeg = fCompl ? *p + 1 : *p;
542 Dau_DsdRemoveBraces_rec( pStr, p, pMatches );
543 if ( (!fCompl && *pBeg == '(' && *q == ')') || (*pBeg == '[' && *q == ']') )
544 {
545 assert( **p == ')' || **p == ']' );
546 *pBeg = **p = ' ';
547 }
548 }
549 assert( *p == q );
550 return;
551 }
552 assert( 0 );
553}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dau_DsdTest66()

void Dau_DsdTest66 ( )

Definition at line 771 of file dauMerge.c.

772{
773 int Perm0[DAU_MAX_VAR] = { 0, 1, 2, 3, 4, 5 };
774// int pMatches[DAU_MAX_STR];
775// int pStatus[DAU_MAX_STR];
776
777// char * pStr = "(!(!a<bcd>)!(!fe))";
778// char * pStr = "([acb]<!edf>)";
779// char * pStr = "!(f!(b!c!(d[ea])))";
780 char * pStr = "[!(a[be])!(c!df)]";
781// char * pStr = "<(e<bca>)fd>";
782// char * pStr = "[d8001{abef}c]";
783// char * pStr1 = "(abc)";
784// char * pStr2 = "[adf]";
785// char * pStr1 = "(!abce)";
786// char * pStr2 = "[adf!b]";
787// char * pStr1 = "(!abc)";
788// char * pStr2 = "[ab]";
789// char * pStr1 = "[d81{abe}c]";
790// char * pStr1 = "[d<a(bc)(!b!c)>{abe}c]";
791// char * pStr1 = "[d81{abe}c]";
792// char * pStr1 = "[d(a[be])c]";
793// char * pStr2 = "(df)";
794// char * pStr1 = "(abf)";
795// char * pStr2 = "(a[(bc)(fde)])";
796// char * pStr1 = "8001{abc[ef]}";
797// char * pStr2 = "(abe)";
798
799 char * pStr1 = "(!(ab)de)";
800 char * pStr2 = "(!(ac)f)";
801
802 char * pRes;
803 word t = Dau_Dsd6ToTruth( pStr );
804 return;
805
806// pStr2 = Dau_DsdDecompose( &t, 6, 0, NULL );
807// Dau_DsdNormalize( pStr2 );
808
809// Dau_DsdMergeMatches( pStr, pMatches );
810// Dau_DsdMergeStatus( pStr, pMatches, 2, pStatus );
811// Dau_DsdMergePrintWithStatus( pStr, pStatus );
812
813 pRes = Dau_DsdMerge( pStr1, Perm0, pStr2, Perm0, 0, 0, 6 );
814
815 t = 0;
816}
Dau_DsdMerge
char * Dau_DsdMerge(char *pDsd0i, int *pPerm0, char *pDsd1i, int *pPerm1, int fCompl0, int fCompl1, int nVars)
DECLARATIONS ///.
Definition dauMerge.c:587
Dau_Dsd6ToTruth
word Dau_Dsd6ToTruth(char *p)
Definition dauDsd.c:445
Here is the call graph for this function:

Variable Documentation

◆ s_TimeComp

abctime s_TimeComp[4] = {0}

Definition at line 574 of file dauMerge.c.

574{0};