#include "abc.h"
#include "dec.h"
#include "ivy.h"
#include "fraig.h"
Go to the source code of this file.
typedef int Abc_Edge_t |
static Abc_Edge_t Abc_EdgeCreate | ( | int | Id, | |
int | fCompl | |||
) | [inline, static] |
static Abc_Edge_t Abc_EdgeFromNode | ( | Abc_Obj_t * | pNode | ) | [inline, static] |
Definition at line 48 of file abcIvy.c.
00048 { return Abc_EdgeCreate( Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ); }
static int Abc_EdgeId | ( | Abc_Edge_t | Edge | ) | [inline, static] |
static int Abc_EdgeIsComplement | ( | Abc_Edge_t | Edge | ) | [inline, static] |
static Abc_Edge_t Abc_EdgeNot | ( | Abc_Edge_t | Edge | ) | [inline, static] |
static Abc_Edge_t Abc_EdgeNotCond | ( | Abc_Edge_t | Edge, | |
int | fCond | |||
) | [inline, static] |
static Abc_Edge_t Abc_EdgeRegular | ( | Abc_Edge_t | Edge | ) | [inline, static] |
static Abc_Obj_t* Abc_EdgeToNode | ( | Abc_Ntk_t * | p, | |
Abc_Edge_t | Edge | |||
) | [inline, static] |
Definition at line 49 of file abcIvy.c.
00049 { return Abc_ObjNotCond( Abc_NtkObj(p, Abc_EdgeId(Edge)), Abc_EdgeIsComplement(Edge) ); }
Function*************************************************************
Synopsis [Strashes one logic node.]
Description []
SideEffects []
SeeAlso []
Definition at line 916 of file abcIvy.c.
00917 { 00918 int fUseFactor = 1; 00919 char * pSop; 00920 Ivy_Obj_t * pFanin0, * pFanin1; 00921 00922 assert( Abc_ObjIsNode(pNode) ); 00923 00924 // consider the case when the graph is an AIG 00925 if ( Abc_NtkIsStrash(pNode->pNtk) ) 00926 { 00927 if ( Abc_AigNodeIsConst(pNode) ) 00928 return Ivy_ManConst1(pMan); 00929 pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy; 00930 pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); 00931 pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy; 00932 pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) ); 00933 return Ivy_And( pMan, pFanin0, pFanin1 ); 00934 } 00935 00936 // get the SOP of the node 00937 if ( Abc_NtkHasMapping(pNode->pNtk) ) 00938 pSop = Mio_GateReadSop(pNode->pData); 00939 else 00940 pSop = pNode->pData; 00941 00942 // consider the constant node 00943 if ( Abc_NodeIsConst(pNode) ) 00944 return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) ); 00945 00946 // consider the special case of EXOR function 00947 if ( Abc_SopIsExorType(pSop) ) 00948 return Abc_NodeStrashAigExorAig( pMan, pNode, pSop ); 00949 00950 // decide when to use factoring 00951 if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) 00952 return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop ); 00953 return Abc_NodeStrashAigSopAig( pMan, pNode, pSop ); 00954 }
Function*************************************************************
Synopsis [Strashed n-input XOR function.]
Description []
SideEffects []
SeeAlso []
Definition at line 1010 of file abcIvy.c.
01011 { 01012 Abc_Obj_t * pFanin; 01013 Ivy_Obj_t * pSum; 01014 int i, nFanins; 01015 // get the number of node's fanins 01016 nFanins = Abc_ObjFaninNum( pNode ); 01017 assert( nFanins == Abc_SopGetVarNum(pSop) ); 01018 // go through the cubes of the node's SOP 01019 pSum = Ivy_Not( Ivy_ManConst1(pMan) ); 01020 for ( i = 0; i < nFanins; i++ ) 01021 { 01022 pFanin = Abc_ObjFanin( pNode, i ); 01023 pSum = Ivy_Exor( pMan, pSum, (Ivy_Obj_t *)pFanin->pCopy ); 01024 } 01025 if ( Abc_SopIsComplement(pSop) ) 01026 pSum = Ivy_Not(pSum); 01027 return pSum; 01028 }
Ivy_Obj_t * Abc_NodeStrashAigFactorAig | ( | Ivy_Man_t * | pMan, | |
Abc_Obj_t * | pRoot, | |||
char * | pSop | |||
) | [static] |
Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
Definition at line 1041 of file abcIvy.c.
01042 { 01043 Dec_Graph_t * pFForm; 01044 Dec_Node_t * pNode; 01045 Ivy_Obj_t * pAnd; 01046 int i; 01047 01048 // extern Ivy_Obj_t * Dec_GraphToNetworkAig( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ); 01049 extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ); 01050 01051 // assert( 0 ); 01052 01053 // perform factoring 01054 pFForm = Dec_Factor( pSop ); 01055 // collect the fanins 01056 Dec_GraphForEachLeaf( pFForm, pNode, i ) 01057 pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; 01058 // perform strashing 01059 // pAnd = Dec_GraphToNetworkAig( pMan, pFForm ); 01060 pAnd = Dec_GraphToNetworkIvy( pMan, pFForm ); 01061 // pAnd = NULL; 01062 01063 Dec_GraphFree( pFForm ); 01064 return pAnd; 01065 }
Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
Definition at line 967 of file abcIvy.c.
00968 { 00969 Abc_Obj_t * pFanin; 00970 Ivy_Obj_t * pAnd, * pSum; 00971 char * pCube; 00972 int i, nFanins; 00973 00974 // get the number of node's fanins 00975 nFanins = Abc_ObjFaninNum( pNode ); 00976 assert( nFanins == Abc_SopGetVarNum(pSop) ); 00977 // go through the cubes of the node's SOP 00978 pSum = Ivy_Not( Ivy_ManConst1(pMan) ); 00979 Abc_SopForEachCube( pSop, nFanins, pCube ) 00980 { 00981 // create the AND of literals 00982 pAnd = Ivy_ManConst1(pMan); 00983 Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net 00984 { 00985 if ( pCube[i] == '1' ) 00986 pAnd = Ivy_And( pMan, pAnd, (Ivy_Obj_t *)pFanin->pCopy ); 00987 else if ( pCube[i] == '0' ) 00988 pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) ); 00989 } 00990 // add to the sum of cubes 00991 pSum = Ivy_Or( pMan, pSum, pAnd ); 00992 } 00993 // decide whether to complement the result 00994 if ( Abc_SopIsComplement(pSop) ) 00995 pSum = Ivy_Not(pSum); 00996 return pSum; 00997 }
Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
Definition at line 1078 of file abcIvy.c.
01079 { 01080 Abc_Obj_t * pLatch; 01081 Vec_Int_t * vArray; 01082 int i; 01083 vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); 01084 Abc_NtkForEachLatch( pNtk, pLatch, i ) 01085 { 01086 if ( fUseDcs || Abc_LatchIsInitDc(pLatch) ) 01087 Vec_IntPush( vArray, IVY_INIT_DC ); 01088 else if ( Abc_LatchIsInit1(pLatch) ) 01089 Vec_IntPush( vArray, IVY_INIT_1 ); 01090 else if ( Abc_LatchIsInit0(pLatch) ) 01091 Vec_IntPush( vArray, IVY_INIT_0 ); 01092 else assert( 0 ); 01093 } 01094 return vArray; 01095 }
CFile****************************************************************
FileName [abcIvy.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Strashing of the current network.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [
] DECLARATIONS ///
Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
Definition at line 696 of file abcIvy.c.
00697 { 00698 Vec_Int_t * vNodes; 00699 Abc_Ntk_t * pNtk; 00700 Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; 00701 Ivy_Obj_t * pNode; 00702 int i; 00703 // perform strashing 00704 pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); 00705 // transfer the pointers to the basic nodes 00706 Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); 00707 Abc_NtkForEachCi( pNtkOld, pObj, i ) 00708 Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); 00709 // rebuild the AIG 00710 vNodes = Ivy_ManDfs( pMan ); 00711 Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) 00712 { 00713 // add the first fanin 00714 pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode ); 00715 if ( Ivy_ObjIsBuf(pNode) ) 00716 { 00717 pNode->TravId = Abc_EdgeFromNode( pFaninNew0 ); 00718 continue; 00719 } 00720 // add the second fanin 00721 pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode ); 00722 // create the new node 00723 if ( Ivy_ObjIsExor(pNode) ) 00724 pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); 00725 else 00726 pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); 00727 pNode->TravId = Abc_EdgeFromNode( pObjNew ); 00728 } 00729 // connect the PO nodes 00730 Abc_NtkForEachCo( pNtkOld, pObj, i ) 00731 { 00732 pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) ); 00733 Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); 00734 } 00735 Vec_IntFree( vNodes ); 00736 if ( !Abc_NtkCheck( pNtk ) ) 00737 fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" ); 00738 return pNtk; 00739 }
Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
Definition at line 752 of file abcIvy.c.
00753 { 00754 Vec_Int_t * vNodes, * vLatches; 00755 Abc_Ntk_t * pNtk; 00756 Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; 00757 Ivy_Obj_t * pNode, * pTemp; 00758 int i; 00759 // assert( Ivy_ManLatchNum(pMan) > 0 ); 00760 // perform strashing 00761 pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); 00762 // transfer the pointers to the basic nodes 00763 Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); 00764 Abc_NtkForEachPi( pNtkOld, pObj, i ) 00765 Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); 00766 // create latches of the new network 00767 vNodes = Ivy_ManDfsSeq( pMan, &vLatches ); 00768 Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) 00769 { 00770 pObjNew = Abc_NtkCreateLatch( pNtk ); 00771 pFaninNew0 = Abc_NtkCreateBi( pNtk ); 00772 pFaninNew1 = Abc_NtkCreateBo( pNtk ); 00773 Abc_ObjAddFanin( pObjNew, pFaninNew0 ); 00774 Abc_ObjAddFanin( pFaninNew1, pObjNew ); 00775 if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC ) 00776 Abc_LatchSetInitDc( pObjNew ); 00777 else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 ) 00778 Abc_LatchSetInit1( pObjNew ); 00779 else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 ) 00780 Abc_LatchSetInit0( pObjNew ); 00781 else assert( 0 ); 00782 pNode->TravId = Abc_EdgeFromNode( pFaninNew1 ); 00783 } 00784 Abc_NtkAddDummyBoxNames( pNtk ); 00785 // rebuild the AIG 00786 Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) 00787 { 00788 // add the first fanin 00789 pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode ); 00790 if ( Ivy_ObjIsBuf(pNode) ) 00791 { 00792 pNode->TravId = Abc_EdgeFromNode( pFaninNew0 ); 00793 continue; 00794 } 00795 // add the second fanin 00796 pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode ); 00797 // create the new node 00798 if ( Ivy_ObjIsExor(pNode) ) 00799 pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); 00800 else 00801 pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); 00802 pNode->TravId = Abc_EdgeFromNode( pObjNew ); 00803 // process the choice nodes 00804 if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 ) 00805 { 00806 pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId ); 00807 // pFaninNew->fPhase = 0; 00808 assert( !Ivy_IsComplement(pNode->pEquiv) ); 00809 for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) ) 00810 { 00811 pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId ); 00812 // pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv ); 00813 pFaninNew->pData = pFaninNew1; 00814 pFaninNew = pFaninNew1; 00815 } 00816 pFaninNew->pData = NULL; 00817 // printf( "Writing choice node %d.\n", pNode->Id ); 00818 } 00819 } 00820 // connect the PO nodes 00821 Abc_NtkForEachPo( pNtkOld, pObj, i ) 00822 { 00823 pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) ); 00824 Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); 00825 } 00826 // connect the latches 00827 Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) 00828 { 00829 pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode ); 00830 Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew ); 00831 } 00832 Vec_IntFree( vLatches ); 00833 Vec_IntFree( vNodes ); 00834 if ( !Abc_NtkCheck( pNtk ) ) 00835 fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); 00836 return pNtk; 00837 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 583 of file abcIvy.c.
00584 { 00585 // Abc_Ntk_t * pNtkAig; 00586 Ivy_Man_t * pMan;//, * pTemp; 00587 int fCleanup = 1; 00588 // int nNodes; 00589 int nLatches = Abc_NtkLatchNum(pNtk); 00590 Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 ); 00591 00592 assert( !Abc_NtkIsNetlist(pNtk) ); 00593 if ( Abc_NtkIsBddLogic(pNtk) ) 00594 { 00595 if ( !Abc_NtkBddToSop(pNtk, 0) ) 00596 { 00597 Vec_IntFree( vInit ); 00598 printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" ); 00599 return NULL; 00600 } 00601 } 00602 if ( Abc_NtkCountSelfFeedLatches(pNtk) ) 00603 { 00604 printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); 00605 return NULL; 00606 } 00607 00608 // print warning about choice nodes 00609 if ( Abc_NtkGetChoiceNum( pNtk ) ) 00610 printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); 00611 00612 // convert to the AIG manager 00613 pMan = Abc_NtkToIvy( pNtk ); 00614 if ( !Ivy_ManCheck( pMan ) ) 00615 { 00616 Vec_IntFree( vInit ); 00617 printf( "AIG check has failed.\n" ); 00618 Ivy_ManStop( pMan ); 00619 return NULL; 00620 } 00621 00622 // Ivy_MffcTest( pMan ); 00623 // Ivy_ManPrintStats( pMan ); 00624 00625 // pMan = Ivy_ManBalance( pTemp = pMan, 1 ); 00626 // Ivy_ManStop( pTemp ); 00627 00628 // Ivy_ManSeqRewrite( pMan, 0, 0 ); 00629 // Ivy_ManTestCutsAlg( pMan ); 00630 // Ivy_ManTestCutsBool( pMan ); 00631 // Ivy_ManRewriteAlg( pMan, 1, 1 ); 00632 00633 // pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 ); 00634 // Ivy_ManStop( pTemp ); 00635 00636 // Ivy_ManTestCutsAll( pMan ); 00637 // Ivy_ManTestCutsTravAll( pMan ); 00638 00639 // Ivy_ManPrintStats( pMan ); 00640 00641 // Ivy_ManPrintStats( pMan ); 00642 // Ivy_ManRewritePre( pMan, 1, 0, 0 ); 00643 // Ivy_ManPrintStats( pMan ); 00644 // printf( "\n" ); 00645 00646 // Ivy_ManPrintStats( pMan ); 00647 // Ivy_ManMakeSeq( pMan, nLatches, pInit ); 00648 // Ivy_ManPrintStats( pMan ); 00649 00650 // Ivy_ManRequiredLevels( pMan ); 00651 00652 // Ivy_FastMapPerform( pMan, 8 ); 00653 Ivy_ManStop( pMan ); 00654 return NULL; 00655 00656 00657 /* 00658 // convert from the AIG manager 00659 pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); 00660 // pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan ); 00661 Ivy_ManStop( pMan ); 00662 00663 // report the cleanup results 00664 if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 00665 printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); 00666 // duplicate EXDC 00667 if ( pNtk->pExdc ) 00668 pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); 00669 // make sure everything is okay 00670 if ( !Abc_NtkCheck( pNtkAig ) ) 00671 { 00672 FREE( pInit ); 00673 printf( "Abc_NtkStrash: The network check has failed.\n" ); 00674 Abc_NtkDelete( pNtkAig ); 00675 return NULL; 00676 } 00677 00678 FREE( pInit ); 00679 return pNtkAig; 00680 */ 00681 }
Function*************************************************************
Synopsis [Prepares the IVY package.]
Description []
SideEffects []
SeeAlso []
Definition at line 127 of file abcIvy.c.
00128 { 00129 Abc_Ntk_t * pNtkAig; 00130 int nNodes, fCleanup = 1; 00131 // convert from the AIG manager 00132 if ( fSeq ) 00133 pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig ); 00134 else 00135 pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); 00136 // report the cleanup results 00137 if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 00138 printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); 00139 // duplicate EXDC 00140 if ( pNtk->pExdc ) 00141 pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); 00142 // make sure everything is okay 00143 if ( !Abc_NtkCheck( pNtkAig ) ) 00144 { 00145 printf( "Abc_NtkStrash: The network check has failed.\n" ); 00146 Abc_NtkDelete( pNtkAig ); 00147 return NULL; 00148 } 00149 return pNtkAig; 00150 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Prepares the IVY package.]
Description []
SideEffects []
SeeAlso []
Definition at line 73 of file abcIvy.c.
00074 { 00075 Ivy_Man_t * pMan; 00076 int fCleanup = 1; 00077 //timeRetime = clock(); 00078 assert( !Abc_NtkIsNetlist(pNtk) ); 00079 if ( Abc_NtkIsBddLogic(pNtk) ) 00080 { 00081 if ( !Abc_NtkBddToSop(pNtk, 0) ) 00082 { 00083 printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" ); 00084 return NULL; 00085 } 00086 } 00087 if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) ) 00088 { 00089 printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); 00090 // return NULL; 00091 } 00092 // print warning about choice nodes 00093 if ( Abc_NtkGetChoiceNum( pNtk ) ) 00094 printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); 00095 // convert to the AIG manager 00096 pMan = Abc_NtkToIvy( pNtk ); 00097 if ( !Ivy_ManCheck( pMan ) ) 00098 { 00099 printf( "AIG check has failed.\n" ); 00100 Ivy_ManStop( pMan ); 00101 return NULL; 00102 } 00103 // Ivy_ManPrintStats( pMan ); 00104 if ( fSeq ) 00105 { 00106 int nLatches = Abc_NtkLatchNum(pNtk); 00107 Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc ); 00108 Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray ); 00109 Vec_IntFree( vInit ); 00110 // Ivy_ManPrintStats( pMan ); 00111 } 00112 //timeRetime = clock() - timeRetime; 00113 return pMan; 00114 }
void Abc_NtkIvyCuts | ( | Abc_Ntk_t * | pNtk, | |
int | nInputs | |||
) |
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 254 of file abcIvy.c.
00255 { 00256 extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs ); 00257 Ivy_Man_t * pMan; 00258 pMan = Abc_NtkIvyBefore( pNtk, 1, 0 ); 00259 if ( pMan == NULL ) 00260 return; 00261 Ivy_CutComputeAll( pMan, nInputs ); 00262 Ivy_ManStop( pMan ); 00263 }
Abc_Ntk_t* Abc_NtkIvyFraig | ( | Abc_Ntk_t * | pNtk, | |
int | nConfLimit, | |||
int | fDoSparse, | |||
int | fProve, | |||
int | fTransfer, | |||
int | fVerbose | |||
) |
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 447 of file abcIvy.c.
00448 { 00449 Ivy_FraigParams_t Params, * pParams = &Params; 00450 Abc_Ntk_t * pNtkAig; 00451 Ivy_Man_t * pMan, * pTemp; 00452 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00453 if ( pMan == NULL ) 00454 return NULL; 00455 Ivy_FraigParamsDefault( pParams ); 00456 pParams->nBTLimitNode = nConfLimit; 00457 pParams->fVerbose = fVerbose; 00458 pParams->fProve = fProve; 00459 pParams->fDoSparse = fDoSparse; 00460 pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); 00461 // transfer the pointers 00462 if ( fTransfer == 1 ) 00463 { 00464 Vec_Ptr_t * vCopies; 00465 vCopies = Abc_NtkSaveCopy( pNtk ); 00466 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00467 Abc_NtkLoadCopy( pNtk, vCopies ); 00468 Vec_PtrFree( vCopies ); 00469 Abc_NtkTransferPointers( pNtk, pNtkAig ); 00470 } 00471 else 00472 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00473 Ivy_ManStop( pTemp ); 00474 Ivy_ManStop( pMan ); 00475 return pNtkAig; 00476 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 186 of file abcIvy.c.
00187 { 00188 Abc_Ntk_t * pNtkAig; 00189 Ivy_Man_t * pMan; 00190 int clk; 00191 // int i; 00192 /* 00193 extern int nMoves; 00194 extern int nMovesS; 00195 extern int nClauses; 00196 extern int timeInv; 00197 00198 nMoves = 0; 00199 nMovesS = 0; 00200 nClauses = 0; 00201 timeInv = 0; 00202 */ 00203 pMan = Abc_NtkIvyBefore( pNtk, 1, 1 ); 00204 if ( pMan == NULL ) 00205 return NULL; 00206 //timeRetime = clock(); 00207 00208 clk = clock(); 00209 Ivy_ManHaigStart( pMan, fVerbose ); 00210 // Ivy_ManRewriteSeq( pMan, 0, 0 ); 00211 // for ( i = 0; i < nIters; i++ ) 00212 // Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 ); 00213 00214 //printf( "%d ", Ivy_ManNodeNum(pMan) ); 00215 Ivy_ManRewriteSeq( pMan, 0, 0 ); 00216 Ivy_ManRewriteSeq( pMan, 0, 0 ); 00217 Ivy_ManRewriteSeq( pMan, 1, 0 ); 00218 //printf( "%d ", Ivy_ManNodeNum(pMan) ); 00219 //printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) ); 00220 //PRT( " ", clock() - clk ); 00221 //printf( "\n" ); 00222 /* 00223 printf( "Moves = %d. ", nMoves ); 00224 printf( "MovesS = %d. ", nMovesS ); 00225 printf( "Clauses = %d. ", nClauses ); 00226 PRT( "Time", timeInv ); 00227 */ 00228 // Ivy_ManRewriteSeq( pMan, 1, 0 ); 00229 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) ); 00230 // Ivy_ManHaigPostprocess( pMan, fVerbose ); 00231 //timeRetime = clock() - timeRetime; 00232 00233 // write working AIG into the current network 00234 // pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 00235 // write HAIG into the current network 00236 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 ); 00237 00238 Ivy_ManHaigStop( pMan ); 00239 Ivy_ManStop( pMan ); 00240 return pNtkAig; 00241 }
int Abc_NtkIvyProve | ( | Abc_Ntk_t ** | ppNtk, | |
void * | pPars | |||
) |
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 489 of file abcIvy.c.
00490 { 00491 Prove_Params_t * pParams = pPars; 00492 Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp; 00493 Abc_Obj_t * pObj, * pFanin; 00494 Ivy_Man_t * pMan; 00495 int RetValue; 00496 assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) ); 00497 // experiment with various parameters settings 00498 // pParams->fUseBdds = 1; 00499 // pParams->fBddReorder = 1; 00500 // pParams->nTotalBacktrackLimit = 10000; 00501 00502 // strash the network if it is not strashed already 00503 if ( !Abc_NtkIsStrash(pNtk) ) 00504 { 00505 pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 ); 00506 Abc_NtkDelete( pNtkTemp ); 00507 } 00508 00509 // check the case when the 0000 simulation pattern detect the bug 00510 pObj = Abc_NtkPo(pNtk,0); 00511 pFanin = Abc_ObjFanin0(pObj); 00512 if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) ) 00513 { 00514 pNtk->pModel = ALLOC( int, Abc_NtkPiNum(pNtk) ); 00515 memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) ); 00516 return 0; 00517 } 00518 00519 // if SAT only, solve without iteration 00520 RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL ); 00521 if ( RetValue >= 0 ) 00522 return RetValue; 00523 00524 // apply AIG rewriting 00525 if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 ) 00526 { 00527 pParams->fUseRewriting = 0; 00528 pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); 00529 Abc_NtkDelete( pNtkTemp ); 00530 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); 00531 pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); 00532 Abc_NtkDelete( pNtkTemp ); 00533 Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); 00534 Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); 00535 } 00536 00537 // convert ABC network into IVY network 00538 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00539 00540 // solve the CEC problem 00541 RetValue = Ivy_FraigProve( &pMan, pParams ); 00542 // convert IVY network into ABC network 00543 pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 ); 00544 Abc_NtkDelete( pNtkTemp ); 00545 // transfer model if given 00546 pNtk->pModel = pMan->pData; pMan->pData = NULL; 00547 Ivy_ManStop( pMan ); 00548 00549 // try to prove it using brute force SAT 00550 if ( RetValue < 0 && pParams->fUseBdds ) 00551 { 00552 if ( pParams->fVerbose ) 00553 { 00554 printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit ); 00555 fflush( stdout ); 00556 } 00557 pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 ); 00558 if ( pNtk ) 00559 { 00560 Abc_NtkDelete( pNtkTemp ); 00561 RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) ); 00562 } 00563 else 00564 pNtk = pNtkTemp; 00565 } 00566 00567 // return the result 00568 *ppNtk = pNtk; 00569 return RetValue; 00570 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 355 of file abcIvy.c.
00356 { 00357 Abc_Ntk_t * pNtkAig; 00358 Ivy_Man_t * pMan, * pTemp; 00359 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00360 if ( pMan == NULL ) 00361 return NULL; 00362 pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose ); 00363 Ivy_ManStop( pTemp ); 00364 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00365 Ivy_ManStop( pMan ); 00366 return pNtkAig; 00367 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 330 of file abcIvy.c.
00331 { 00332 Abc_Ntk_t * pNtkAig; 00333 Ivy_Man_t * pMan, * pTemp; 00334 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00335 if ( pMan == NULL ) 00336 return NULL; 00337 pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose ); 00338 Ivy_ManStop( pTemp ); 00339 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00340 Ivy_ManStop( pMan ); 00341 return pNtkAig; 00342 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 276 of file abcIvy.c.
00277 { 00278 Abc_Ntk_t * pNtkAig; 00279 Ivy_Man_t * pMan; 00280 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00281 if ( pMan == NULL ) 00282 return NULL; 00283 //timeRetime = clock(); 00284 Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose ); 00285 //timeRetime = clock() - timeRetime; 00286 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00287 Ivy_ManStop( pMan ); 00288 return pNtkAig; 00289 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 302 of file abcIvy.c.
00303 { 00304 Abc_Ntk_t * pNtkAig; 00305 Ivy_Man_t * pMan; 00306 pMan = Abc_NtkIvyBefore( pNtk, 1, 1 ); 00307 if ( pMan == NULL ) 00308 return NULL; 00309 //timeRetime = clock(); 00310 Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose ); 00311 //timeRetime = clock() - timeRetime; 00312 // Ivy_ManRewriteSeq( pMan, 1, 0 ); 00313 // Ivy_ManRewriteSeq( pMan, 1, 0 ); 00314 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 00315 Ivy_ManStop( pMan ); 00316 return pNtkAig; 00317 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 380 of file abcIvy.c.
00381 { 00382 Ivy_FraigParams_t Params, * pParams = &Params; 00383 Abc_Ntk_t * pNtkAig; 00384 Ivy_Man_t * pMan, * pTemp; 00385 pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); 00386 if ( pMan == NULL ) 00387 return NULL; 00388 Ivy_FraigParamsDefault( pParams ); 00389 pParams->nBTLimitMiter = nConfLimit; 00390 pParams->fVerbose = fVerbose; 00391 // pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); 00392 pMan = Ivy_FraigMiter( pTemp = pMan, pParams ); 00393 Ivy_ManStop( pTemp ); 00394 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); 00395 Ivy_ManStop( pMan ); 00396 return pNtkAig; 00397 }
Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
Definition at line 163 of file abcIvy.c.
00164 { 00165 Abc_Ntk_t * pNtkAig; 00166 Ivy_Man_t * pMan; 00167 pMan = Abc_NtkIvyBefore( pNtk, 1, 0 ); 00168 if ( pMan == NULL ) 00169 return NULL; 00170 pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 00171 Ivy_ManStop( pMan ); 00172 return pNtkAig; 00173 }
Function*************************************************************
Synopsis [Prepares the network for strashing.]
Description []
SideEffects []
SeeAlso []
Definition at line 888 of file abcIvy.c.
00889 { 00890 // ProgressBar * pProgress; 00891 Vec_Ptr_t * vNodes; 00892 Abc_Obj_t * pNode; 00893 int i; 00894 vNodes = Abc_NtkDfs( pNtk, 0 ); 00895 // pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); 00896 Vec_PtrForEachEntry( vNodes, pNode, i ) 00897 { 00898 // Extra_ProgressBarUpdate( pProgress, i, NULL ); 00899 pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode ); 00900 } 00901 // Extra_ProgressBarStop( pProgress ); 00902 Vec_PtrFree( vNodes ); 00903 }
Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description []
SideEffects []
SeeAlso []
Definition at line 850 of file abcIvy.c.
00851 { 00852 Ivy_Man_t * pMan; 00853 Abc_Obj_t * pObj; 00854 Ivy_Obj_t * pFanin; 00855 int i; 00856 // create the manager 00857 assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkIsStrash(pNtkOld) ); 00858 pMan = Ivy_ManStart(); 00859 // create the PIs 00860 if ( Abc_NtkIsStrash(pNtkOld) ) 00861 Abc_AigConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); 00862 Abc_NtkForEachCi( pNtkOld, pObj, i ) 00863 pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan); 00864 // perform the conversion of the internal nodes 00865 Abc_NtkStrashPerformAig( pNtkOld, pMan ); 00866 // create the POs 00867 Abc_NtkForEachCo( pNtkOld, pObj, i ) 00868 { 00869 pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy; 00870 pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); 00871 Ivy_ObjCreatePo( pMan, pFanin ); 00872 } 00873 Ivy_ManCleanup( pMan ); 00874 return pMan; 00875 }
Function*************************************************************
Synopsis [Sets the final nodes to point to the original nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 410 of file abcIvy.c.
00411 { 00412 Abc_Obj_t * pObj; 00413 Ivy_Obj_t * pObjIvy, * pObjFraig; 00414 int i; 00415 pObj = Abc_AigConst1(pNtk); 00416 pObj->pCopy = Abc_AigConst1(pNtkAig); 00417 Abc_NtkForEachCi( pNtk, pObj, i ) 00418 pObj->pCopy = Abc_NtkCi(pNtkAig, i); 00419 Abc_NtkForEachCo( pNtk, pObj, i ) 00420 pObj->pCopy = Abc_NtkCo(pNtkAig, i); 00421 Abc_NtkForEachLatch( pNtk, pObj, i ) 00422 pObj->pCopy = Abc_NtkBox(pNtkAig, i); 00423 Abc_NtkForEachNode( pNtk, pObj, i ) 00424 { 00425 pObjIvy = (Ivy_Obj_t *)pObj->pCopy; 00426 if ( pObjIvy == NULL ) 00427 continue; 00428 pObjFraig = Ivy_ObjEquiv( pObjIvy ); 00429 if ( pObjFraig == NULL ) 00430 continue; 00431 pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId ); 00432 pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) ); 00433 } 00434 }
Definition at line 51 of file abcIvy.c.
00051 { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
Definition at line 52 of file abcIvy.c.
00052 { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
char* Mio_GateReadSop | ( | void * | pGate | ) |
int timeRetime |
CFile****************************************************************
FileName [retCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Retiming package.]
Synopsis [The core retiming procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Oct 31, 2006.]
Revision [
] DECLARATIONS ///