Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
c7b331ef
Commit
c7b331ef
authored
Jul 06, 2008
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Version abc80706
parent
7b734f23
Show whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
1241 additions
and
626 deletions
+1241
-626
abc.dsp
+8
-0
src/aig/nwk/module.make
+1
-0
src/aig/nwk/nwk.h
+14
-0
src/aig/nwk/nwkMerge.c
+763
-0
src/aig/nwk/nwkUtil_old.c
+0
-615
src/base/abci/abc.c
+246
-0
src/base/abci/abcSense.c
+208
-0
src/base/abci/module.make
+1
-0
todo.txt
+0
-11
No files found.
abc.dsp
View file @
c7b331ef
...
...
@@ -386,6 +386,10 @@ SOURCE=.\src\base\abci\abcSat.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcSense.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcStrash.c
# End Source File
# Begin Source File
...
...
@@ -3314,6 +3318,10 @@ SOURCE=.\src\aig\nwk\nwkMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nwk\nwkMerge.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\nwk\nwkObj.c
# End Source File
# Begin Source File
...
...
src/aig/nwk/module.make
View file @
c7b331ef
...
...
@@ -6,6 +6,7 @@ SRC += src/aig/nwk/nwkAig.c \
src/aig/nwk/nwkFlow.c
\
src/aig/nwk/nwkMan.c
\
src/aig/nwk/nwkMap.c
\
src/aig/nwk/nwkMerge.c
\
src/aig/nwk/nwkObj.c
\
src/aig/nwk/nwkSpeedup.c
\
src/aig/nwk/nwkStrash.c
\
...
...
src/aig/nwk/nwk.h
View file @
c7b331ef
...
...
@@ -109,6 +109,20 @@ struct Nwk_Obj_t_
};
// the LUT merging parameters
typedef
struct
Nwk_LMPars_t_
Nwk_LMPars_t
;
struct
Nwk_LMPars_t_
{
int
nMaxLutSize
;
// the max LUT size for merging (N=5)
int
nMaxSuppSize
;
// the max total support size after merging (S=5)
int
nMaxDistance
;
// the max number of nodes separating LUTs
int
nMaxLevelDiff
;
// the max difference in levels
int
nMaxFanout
;
// the max number of fanouts to traverse
int
fUseTfiTfo
;
// enables the use of TFO/TFO nodes as candidates
int
fVeryVerbose
;
// enables additional verbose output
int
fVerbose
;
// enables verbose output
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
...
...
src/aig/nwk/nwkMerge.c
0 → 100644
View file @
c7b331ef
/**CFile****************************************************************
FileName [nwkMerge.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [LUT merging algorithm.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: nwkMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "nwk.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Marks the fanins of the node with the current trav ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManMarkFanins_rec
(
Nwk_Obj_t
*
pLut
,
int
nLevMin
)
{
Nwk_Obj_t
*
pNext
;
int
i
;
if
(
!
Nwk_ObjIsNode
(
pLut
)
)
return
;
if
(
Nwk_ObjIsTravIdCurrent
(
pLut
)
)
return
;
Nwk_ObjSetTravIdCurrent
(
pLut
);
if
(
Nwk_ObjLevel
(
pLut
)
<
nLevMin
)
return
;
Nwk_ObjForEachFanin
(
pLut
,
pNext
,
i
)
Nwk_ManMarkFanins_rec
(
pNext
,
nLevMin
);
}
/**Function*************************************************************
Synopsis [Marks the fanouts of the node with the current trav ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManMarkFanouts_rec
(
Nwk_Obj_t
*
pLut
,
int
nLevMax
,
int
nFanMax
)
{
Nwk_Obj_t
*
pNext
;
int
i
;
if
(
!
Nwk_ObjIsNode
(
pLut
)
)
return
;
if
(
Nwk_ObjIsTravIdCurrent
(
pLut
)
)
return
;
Nwk_ObjSetTravIdCurrent
(
pLut
);
if
(
Nwk_ObjLevel
(
pLut
)
>
nLevMax
)
return
;
if
(
Nwk_ObjFanoutNum
(
pLut
)
>
nFanMax
)
return
;
Nwk_ObjForEachFanout
(
pLut
,
pNext
,
i
)
Nwk_ManMarkFanouts_rec
(
pNext
,
nLevMax
,
nFanMax
);
}
/**Function*************************************************************
Synopsis [Collects the circle of nodes around the given set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManCollectCircle
(
Vec_Ptr_t
*
vStart
,
Vec_Ptr_t
*
vNext
,
int
nFanMax
)
{
Nwk_Obj_t
*
pObj
,
*
pNext
;
int
i
,
k
;
Vec_PtrClear
(
vNext
);
Vec_PtrForEachEntry
(
vStart
,
pObj
,
i
)
{
Nwk_ObjForEachFanin
(
pObj
,
pNext
,
k
)
{
if
(
!
Nwk_ObjIsNode
(
pNext
)
)
continue
;
if
(
Nwk_ObjIsTravIdCurrent
(
pNext
)
)
continue
;
Nwk_ObjSetTravIdCurrent
(
pNext
);
Vec_PtrPush
(
vNext
,
pNext
);
}
Nwk_ObjForEachFanout
(
pObj
,
pNext
,
k
)
{
if
(
!
Nwk_ObjIsNode
(
pNext
)
)
continue
;
if
(
Nwk_ObjIsTravIdCurrent
(
pNext
)
)
continue
;
Nwk_ObjSetTravIdCurrent
(
pNext
);
if
(
Nwk_ObjFanoutNum
(
pNext
)
>
nFanMax
)
continue
;
Vec_PtrPush
(
vNext
,
pNext
);
}
}
}
/**Function*************************************************************
Synopsis [Collects the circle of nodes removes from the given one.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManCollectNonOverlapCands
(
Nwk_Obj_t
*
pLut
,
Vec_Ptr_t
*
vStart
,
Vec_Ptr_t
*
vNext
,
Vec_Ptr_t
*
vCands
,
Nwk_LMPars_t
*
pPars
)
{
Vec_Ptr_t
*
vTemp
;
Nwk_Obj_t
*
pObj
;
int
i
,
k
;
Vec_PtrClear
(
vCands
);
if
(
pPars
->
nMaxSuppSize
-
Nwk_ObjFaninNum
(
pLut
)
<=
1
)
return
;
// collect nodes removed by this distance
assert
(
pPars
->
nMaxDistance
>
0
);
Vec_PtrClear
(
vStart
);
Vec_PtrPush
(
vStart
,
pLut
);
Nwk_ManIncrementTravId
(
pLut
->
pMan
);
Nwk_ObjSetTravIdCurrent
(
pLut
);
for
(
i
=
1
;
i
<
pPars
->
nMaxDistance
;
i
++
)
{
Nwk_ManCollectCircle
(
vStart
,
vNext
,
pPars
->
nMaxFanout
);
vTemp
=
vStart
;
vStart
=
vNext
;
vNext
=
vTemp
;
// collect the nodes in vStart
Vec_PtrForEachEntry
(
vStart
,
pObj
,
k
)
Vec_PtrPush
(
vCands
,
pObj
);
}
// mark the TFI/TFO nodes
Nwk_ManIncrementTravId
(
pLut
->
pMan
);
if
(
pPars
->
fUseTfiTfo
)
Nwk_ObjSetTravIdCurrent
(
pLut
);
else
{
Nwk_ObjSetTravIdPrevious
(
pLut
);
Nwk_ManMarkFanins_rec
(
pLut
,
Nwk_ObjLevel
(
pLut
)
-
pPars
->
nMaxDistance
);
Nwk_ObjSetTravIdPrevious
(
pLut
);
Nwk_ManMarkFanouts_rec
(
pLut
,
Nwk_ObjLevel
(
pLut
)
+
pPars
->
nMaxDistance
,
pPars
->
nMaxFanout
);
}
// collect nodes satisfying the following conditions:
// - they are close enough in terms of distance
// - they are not in the TFI/TFO of the LUT
// - they have no more than the given number of fanins
// - they have no more than the given diff in delay
k
=
0
;
Vec_PtrForEachEntry
(
vCands
,
pObj
,
i
)
{
if
(
Nwk_ObjIsTravIdCurrent
(
pObj
)
)
continue
;
if
(
Nwk_ObjFaninNum
(
pLut
)
+
Nwk_ObjFaninNum
(
pObj
)
>
pPars
->
nMaxSuppSize
)
continue
;
if
(
Nwk_ObjLevel
(
pLut
)
-
Nwk_ObjLevel
(
pObj
)
>
pPars
->
nMaxLevelDiff
||
Nwk_ObjLevel
(
pObj
)
-
Nwk_ObjLevel
(
pLut
)
>
pPars
->
nMaxLevelDiff
)
continue
;
Vec_PtrWriteEntry
(
vCands
,
k
++
,
pObj
);
}
Vec_PtrShrink
(
vCands
,
k
);
}
/**Function*************************************************************
Synopsis [Count the total number of fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManCountTotalFanins
(
Nwk_Obj_t
*
pLut
,
Nwk_Obj_t
*
pCand
)
{
Nwk_Obj_t
*
pFanin
;
int
i
,
nCounter
=
Nwk_ObjFaninNum
(
pLut
);
Nwk_ObjForEachFanin
(
pCand
,
pFanin
,
i
)
nCounter
+=
!
pFanin
->
MarkC
;
return
nCounter
;
}
/**Function*************************************************************
Synopsis [Collects overlapping candidates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwl_ManCollectOverlapCands
(
Nwk_Obj_t
*
pLut
,
Vec_Ptr_t
*
vCands
,
Nwk_LMPars_t
*
pPars
)
{
Nwk_Obj_t
*
pFanin
,
*
pObj
;
int
i
,
k
;
// mark fanins of pLut
Nwk_ObjForEachFanin
(
pLut
,
pFanin
,
i
)
pFanin
->
MarkC
=
1
;
// collect the matching fanouts of each fanin of the node
Vec_PtrClear
(
vCands
);
Nwk_ManIncrementTravId
(
pLut
->
pMan
);
Nwk_ObjSetTravIdCurrent
(
pLut
);
Nwk_ObjForEachFanin
(
pLut
,
pFanin
,
i
)
{
if
(
!
Nwk_ObjIsNode
(
pFanin
)
)
continue
;
if
(
Nwk_ObjFanoutNum
(
pFanin
)
>
pPars
->
nMaxFanout
)
continue
;
Nwk_ObjForEachFanout
(
pFanin
,
pObj
,
k
)
{
if
(
!
Nwk_ObjIsNode
(
pObj
)
)
continue
;
if
(
Nwk_ObjIsTravIdCurrent
(
pObj
)
)
continue
;
Nwk_ObjSetTravIdCurrent
(
pObj
);
// check the difference in delay
if
(
Nwk_ObjLevel
(
pLut
)
-
Nwk_ObjLevel
(
pObj
)
>
pPars
->
nMaxLevelDiff
||
Nwk_ObjLevel
(
pObj
)
-
Nwk_ObjLevel
(
pLut
)
>
pPars
->
nMaxLevelDiff
)
continue
;
// check the total number of fanins of the node
if
(
Nwk_ManCountTotalFanins
(
pLut
,
pObj
)
>
pPars
->
nMaxSuppSize
)
continue
;
Vec_PtrPush
(
vCands
,
pObj
);
}
}
// unmark fanins of pLut
Nwk_ObjForEachFanin
(
pLut
,
pFanin
,
i
)
pFanin
->
MarkC
=
0
;
}
#define MAX_LIST 16
// edge of the graph
typedef
struct
Nwk_Edg_t_
Nwk_Edg_t
;
struct
Nwk_Edg_t_
{
int
iNode1
;
// the first node
int
iNode2
;
// the second node
Nwk_Edg_t
*
pNext
;
// the next edge
};
// vertex of the graph
typedef
struct
Nwk_Vrt_t_
Nwk_Vrt_t
;
struct
Nwk_Vrt_t_
{
int
Id
;
// the vertex number
int
iPrev
;
// the previous vertex in the list
int
iNext
;
// the next vertex in the list
int
nEdges
;
// the number of edges
int
pEdges
[
0
];
// the array of edges
};
// the connectivity graph
typedef
struct
Nwk_Grf_t_
Nwk_Grf_t
;
struct
Nwk_Grf_t_
{
// preliminary graph representation
int
nObjs
;
// the number of objects
int
nVertsPre
;
// the upper bound on the number of vertices
int
nEdgeHash
;
// approximate number of edges
Nwk_Edg_t
**
pEdgeHash
;
// hash table for edges
Aig_MmFixed_t
*
pMemEdges
;
// memory for edges
// graph representation
int
nEdges
;
// the number of edges
int
nVerts
;
// the number of vertices
Nwk_Vrt_t
**
pVerts
;
// the array of vertices
Aig_MmFlex_t
*
pMemVerts
;
// memory for vertices
// intermediate data
int
pLists1
[
MAX_LIST
+
1
];
int
pLists2
[
MAX_LIST
+
1
];
// the results of matching
Vec_Int_t
*
vPairs
;
// mappings graph into LUTs and back
int
*
pMapLut2Id
;
int
*
pMapId2Lut
;
};
/**Function*************************************************************
Synopsis [Deallocates the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManGraphFree
(
Nwk_Grf_t
*
p
)
{
if
(
p
->
vPairs
)
Vec_IntFree
(
p
->
vPairs
);
if
(
p
->
pMemEdges
)
Aig_MmFixedStop
(
p
->
pMemEdges
,
0
);
if
(
p
->
pMemVerts
)
Aig_MmFlexStop
(
p
->
pMemVerts
,
0
);
FREE
(
p
->
pEdgeHash
);
FREE
(
p
->
pVerts
);
FREE
(
p
->
pMapLut2Id
);
FREE
(
p
->
pMapId2Lut
);
free
(
p
);
}
/**Function*************************************************************
Synopsis [Allocates the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Nwk_Grf_t
*
Nwk_ManGraphAlloc
(
int
nObjs
,
int
nVertsPre
)
{
Nwk_Grf_t
*
p
;
p
=
ALLOC
(
Nwk_Grf_t
,
1
);
memset
(
p
,
0
,
sizeof
(
Nwk_Grf_t
)
);
p
->
nObjs
=
nObjs
;
p
->
nVertsPre
=
nVertsPre
;
p
->
nEdgeHash
=
Aig_PrimeCudd
(
10
*
nVertsPre
);
p
->
pEdgeHash
=
CALLOC
(
Nwk_Edg_t
*
,
p
->
nEdgeHash
);
p
->
pMemEdges
=
Aig_MmFixedStart
(
sizeof
(
Nwk_Edg_t
),
p
->
nEdgeHash
);
p
->
pMapLut2Id
=
ALLOC
(
int
,
nObjs
);
p
->
pMapId2Lut
=
ALLOC
(
int
,
nVertsPre
);
p
->
vPairs
=
Vec_IntAlloc
(
1000
);
memset
(
p
->
pMapLut2Id
,
0xff
,
sizeof
(
int
)
*
nObjs
);
memset
(
p
->
pMapId2Lut
,
0xff
,
sizeof
(
int
)
*
nVertsPre
);
return
p
;
}
/**Function*************************************************************
Synopsis [Finds or adds the edge to the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphSetMapping
(
Nwk_Grf_t
*
p
,
int
iLut
)
{
p
->
nVerts
++
;
p
->
pMapId2Lut
[
p
->
nVerts
]
=
iLut
;
p
->
pMapLut2Id
[
iLut
]
=
p
->
nVerts
;
}
/**Function*************************************************************
Synopsis [Finds or adds the edge to the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphHashEdge
(
Nwk_Grf_t
*
p
,
int
iLut1
,
int
iLut2
)
{
Nwk_Edg_t
*
pEntry
;
int
Key
;
if
(
iLut1
==
iLut2
)
return
;
if
(
iLut1
>
iLut2
)
{
Key
=
iLut1
;
iLut1
=
iLut2
;
iLut2
=
Key
;
}
assert
(
iLut1
<
iLut2
);
Key
=
(
741457
*
iLut1
+
4256249
*
iLut2
)
%
p
->
nEdgeHash
;
for
(
pEntry
=
p
->
pEdgeHash
[
Key
];
pEntry
;
pEntry
=
pEntry
->
pNext
)
if
(
pEntry
->
iNode1
==
iLut1
&&
pEntry
->
iNode2
==
iLut2
)
return
;
pEntry
=
(
Nwk_Edg_t
*
)
Aig_MmFixedEntryFetch
(
p
->
pMemEdges
);
pEntry
->
iNode1
=
iLut1
;
pEntry
->
iNode2
=
iLut2
;
pEntry
->
pNext
=
p
->
pEdgeHash
[
Key
];
p
->
pEdgeHash
[
Key
]
=
pEntry
;
p
->
nEdges
++
;
}
/**Function*************************************************************
Synopsis [Prepares the graph for solving the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphListAdd
(
Nwk_Grf_t
*
p
,
int
*
pList
,
Nwk_Vrt_t
*
pVertex
)
{
if
(
*
pList
)
{
Nwk_Vrt_t
*
pHead
;
pHead
=
p
->
pVerts
[
*
pList
];
pVertex
->
iPrev
=
0
;
pVertex
->
iNext
=
pHead
->
Id
;
pHead
->
iPrev
=
pVertex
->
Id
;
}
*
pList
=
pVertex
->
Id
;
}
/**Function*************************************************************
Synopsis [Prepares the graph for solving the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphListDelete
(
Nwk_Grf_t
*
p
,
int
*
pList
,
Nwk_Vrt_t
*
pVertex
)
{
assert
(
*
pList
);
if
(
pVertex
->
iPrev
)
p
->
pVerts
[
pVertex
->
iPrev
]
->
iNext
=
pVertex
->
iNext
;
if
(
pVertex
->
iNext
)
p
->
pVerts
[
pVertex
->
iNext
]
->
iNext
=
pVertex
->
iPrev
;
if
(
*
pList
==
pVertex
->
Id
)
*
pList
=
pVertex
->
iNext
;
pVertex
->
iPrev
=
pVertex
->
iNext
=
0
;
}
/**Function*************************************************************
Synopsis [Inserts the edge into one of the linked lists.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphListInsert
(
Nwk_Grf_t
*
p
,
Nwk_Vrt_t
*
pVertex
)
{
Nwk_Vrt_t
*
pNext
;
assert
(
pVertex
->
nEdges
>
0
);
if
(
pVertex
->
nEdges
==
1
)
{
pNext
=
p
->
pVerts
[
pVertex
->
pEdges
[
0
]
];
if
(
pNext
->
nEdges
>=
MAX_LIST
)
Nwk_ManGraphListAdd
(
p
,
p
->
pLists1
+
MAX_LIST
,
pVertex
);
else
Nwk_ManGraphListAdd
(
p
,
p
->
pLists1
+
pNext
->
nEdges
,
pVertex
);
}
else
{
if
(
pVertex
->
nEdges
>=
MAX_LIST
)
Nwk_ManGraphListAdd
(
p
,
p
->
pLists1
+
MAX_LIST
,
pVertex
);
else
Nwk_ManGraphListAdd
(
p
,
p
->
pLists1
+
pVertex
->
nEdges
,
pVertex
);
}
}
/**Function*************************************************************
Synopsis [Extracts the edge from one of the linked lists.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Nwk_ManGraphListExtract
(
Nwk_Grf_t
*
p
,
Nwk_Vrt_t
*
pVertex
)
{
Nwk_Vrt_t
*
pNext
;
assert
(
pVertex
->
nEdges
>
0
);
if
(
pVertex
->
nEdges
==
1
)
{
pNext
=
p
->
pVerts
[
pVertex
->
pEdges
[
0
]
];
if
(
pNext
->
nEdges
>=
MAX_LIST
)
Nwk_ManGraphListDelete
(
p
,
p
->
pLists1
+
MAX_LIST
,
pVertex
);
else
Nwk_ManGraphListDelete
(
p
,
p
->
pLists1
+
pNext
->
nEdges
,
pVertex
);
}
else
{
if
(
pVertex
->
nEdges
>=
MAX_LIST
)
Nwk_ManGraphListDelete
(
p
,
p
->
pLists1
+
MAX_LIST
,
pVertex
);
else
Nwk_ManGraphListDelete
(
p
,
p
->
pLists1
+
pVertex
->
nEdges
,
pVertex
);
}
}
/**Function*************************************************************
Synopsis [Prepares the graph for solving the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManGraphPrepare
(
Nwk_Grf_t
*
p
)
{
Nwk_Edg_t
*
pEntry
;
Nwk_Vrt_t
*
pVertex
;
int
*
pnEdges
,
Key
,
nBytes
,
i
;
// count the edges
pnEdges
=
CALLOC
(
int
,
p
->
nVerts
);
for
(
Key
=
0
;
Key
<
p
->
nEdgeHash
;
Key
++
)
for
(
pEntry
=
p
->
pEdgeHash
[
Key
];
pEntry
;
pEntry
=
pEntry
->
pNext
)
{
// translate into vertices
assert
(
pEntry
->
iNode1
<
p
->
nObjs
);
assert
(
pEntry
->
iNode2
<
p
->
nObjs
);
pEntry
->
iNode1
=
p
->
pMapLut2Id
[
pEntry
->
iNode1
];
pEntry
->
iNode2
=
p
->
pMapLut2Id
[
pEntry
->
iNode2
];
// count the edges
assert
(
pEntry
->
iNode1
<
p
->
nVerts
);
assert
(
pEntry
->
iNode2
<
p
->
nVerts
);
pnEdges
[
pEntry
->
iNode1
]
++
;
pnEdges
[
pEntry
->
iNode2
]
++
;
}
// allocate the real graph
p
->
pMemVerts
=
Aig_MmFlexStart
();
p
->
pVerts
=
ALLOC
(
Nwk_Vrt_t
*
,
p
->
nVerts
+
1
);
p
->
pVerts
[
0
]
=
NULL
;
for
(
i
=
1
;
i
<=
p
->
nVerts
;
i
++
)
{
assert
(
pnEdges
[
i
]
>
0
);
nBytes
=
sizeof
(
Nwk_Vrt_t
)
+
sizeof
(
int
)
*
pnEdges
[
i
];
p
->
pVerts
[
i
]
=
(
Nwk_Vrt_t
*
)
Aig_MmFlexEntryFetch
(
p
->
pMemVerts
,
nBytes
);
memset
(
p
->
pVerts
[
i
],
0
,
nBytes
);
p
->
pVerts
[
i
]
->
Id
=
i
;
}
// add edges to the real graph
for
(
Key
=
0
;
Key
<
p
->
nEdgeHash
;
Key
++
)
for
(
pEntry
=
p
->
pEdgeHash
[
Key
];
pEntry
;
pEntry
=
pEntry
->
pNext
)
{
pVertex
=
p
->
pVerts
[
pEntry
->
iNode1
];
pVertex
->
pEdges
[
pVertex
->
nEdges
++
]
=
pEntry
->
iNode2
;
pVertex
=
p
->
pVerts
[
pEntry
->
iNode2
];
pVertex
->
pEdges
[
pVertex
->
nEdges
++
]
=
pEntry
->
iNode1
;
}
// put vertices into the data structure
for
(
i
=
1
;
i
<=
p
->
nVerts
;
i
++
)
{
assert
(
p
->
pVerts
[
i
]
->
nEdges
==
pnEdges
[
i
]
);
Nwk_ManGraphListInsert
(
p
,
p
->
pVerts
[
i
]
);
}
// clean up
Aig_MmFixedStop
(
p
->
pMemEdges
,
0
);
p
->
pMemEdges
=
NULL
;
FREE
(
p
->
pEdgeHash
);
p
->
nEdgeHash
=
0
;
free
(
pnEdges
);
}
/**Function*************************************************************
Synopsis [Updates the problem after pulling out one edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManGraphUpdate
(
Nwk_Grf_t
*
p
,
Nwk_Vrt_t
*
pVertex
,
Nwk_Vrt_t
*
pNext
)
{
Nwk_Vrt_t
*
pChanged
;
int
i
,
k
;
// update neibors of pVertex
for
(
i
=
0
;
i
<
pVertex
->
nEdges
;
i
++
)
{
pChanged
=
p
->
pVerts
[
pVertex
->
pEdges
[
i
]
];
Nwk_ManGraphListExtract
(
p
,
pChanged
);
for
(
k
=
0
;
k
<
pChanged
->
nEdges
;
k
++
)
if
(
pChanged
->
pEdges
[
k
]
==
pVertex
->
Id
)
break
;
assert
(
k
<
pChanged
->
nEdges
);
pChanged
->
nEdges
--
;
for
(
;
k
<
pChanged
->
nEdges
;
k
++
)
pChanged
->
pEdges
[
k
]
=
pChanged
->
pEdges
[
k
+
1
];
if
(
pChanged
->
nEdges
>
0
)
Nwk_ManGraphListInsert
(
p
,
pChanged
);
}
// update neibors of pNext
for
(
i
=
0
;
i
<
pNext
->
nEdges
;
i
++
)
{
pChanged
=
p
->
pVerts
[
pNext
->
pEdges
[
i
]
];
Nwk_ManGraphListExtract
(
p
,
pChanged
);
for
(
k
=
0
;
k
<
pChanged
->
nEdges
;
k
++
)
if
(
pChanged
->
pEdges
[
k
]
==
pNext
->
Id
)
break
;
assert
(
k
<
pChanged
->
nEdges
);
pChanged
->
nEdges
--
;
for
(
;
k
<
pChanged
->
nEdges
;
k
++
)
pChanged
->
pEdges
[
k
]
=
pChanged
->
pEdges
[
k
+
1
];
if
(
pChanged
->
nEdges
>
0
)
Nwk_ManGraphListInsert
(
p
,
pChanged
);
}
// add to the result
if
(
pVertex
->
Id
<
pNext
->
Id
)
{
Vec_IntPush
(
p
->
vPairs
,
p
->
pMapId2Lut
[
pVertex
->
Id
]
);
Vec_IntPush
(
p
->
vPairs
,
p
->
pMapId2Lut
[
pNext
->
Id
]
);
}
else
{
Vec_IntPush
(
p
->
vPairs
,
p
->
pMapId2Lut
[
pNext
->
Id
]
);
Vec_IntPush
(
p
->
vPairs
,
p
->
pMapId2Lut
[
pVertex
->
Id
]
);
}
}
/**Function*************************************************************
Synopsis [Solves the problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManGraphSolve
(
Nwk_Grf_t
*
p
)
{
Nwk_Vrt_t
*
pVertex
,
*
pNext
;
int
i
,
j
;
while
(
1
)
{
// find the next vertext to extract
for
(
i
=
1
;
i
<=
MAX_LIST
;
i
++
)
if
(
p
->
pLists1
[
i
]
)
{
pVertex
=
p
->
pVerts
[
p
->
pLists1
[
i
]
];
assert
(
pVertex
->
nEdges
==
1
);
pNext
=
p
->
pVerts
[
pVertex
->
pEdges
[
0
]
];
// update the data-structures
Nwk_ManGraphUpdate
(
p
,
pVertex
,
pNext
);
break
;
}
// find the next vertext to extract
for
(
j
=
2
;
j
<=
MAX_LIST
;
j
++
)
if
(
p
->
pLists2
[
j
]
)
{
pVertex
=
p
->
pVerts
[
p
->
pLists2
[
j
]
];
assert
(
pVertex
->
nEdges
==
j
||
j
==
MAX_LIST
);
// update the data-structures
Nwk_ManGraphUpdate
(
p
,
pVertex
,
pNext
);
break
;
}
if
(
i
==
MAX_LIST
+
1
&&
j
==
MAX_LIST
+
1
)
break
;
}
}
/**Function*************************************************************
Synopsis [Performs LUT merging with parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t
*
Nwk_ManLutMerge
(
Nwk_Man_t
*
pNtk
,
Nwk_LMPars_t
*
pPars
)
{
Nwk_Grf_t
*
p
;
Vec_Int_t
*
vResult
;
Vec_Ptr_t
*
vStart
,
*
vNext
,
*
vCands1
,
*
vCands2
;
Nwk_Obj_t
*
pLut
,
*
pCand
;
int
i
,
k
,
nVertsPre
;
// count the number of vertices
nVertsPre
=
0
;
Nwk_ManForEachNode
(
pNtk
,
pLut
,
i
)
nVertsPre
+=
(
int
)(
Nwk_ObjFaninNum
(
pLut
)
<=
pPars
->
nMaxLutSize
);
p
=
Nwk_ManGraphAlloc
(
Nwk_ManObjNumMax
(
pNtk
),
nVertsPre
);
// create graph
vStart
=
Vec_PtrAlloc
(
1000
);
vNext
=
Vec_PtrAlloc
(
1000
);
vCands1
=
Vec_PtrAlloc
(
1000
);
vCands2
=
Vec_PtrAlloc
(
1000
);
Nwk_ManForEachNode
(
pNtk
,
pLut
,
i
)
{
if
(
Nwk_ObjFaninNum
(
pLut
)
>
pPars
->
nMaxLutSize
)
continue
;
Nwl_ManCollectOverlapCands
(
pLut
,
vCands1
,
pPars
);
Nwk_ManCollectNonOverlapCands
(
pLut
,
vStart
,
vNext
,
vCands2
,
pPars
);
if
(
Vec_PtrSize
(
vCands1
)
==
0
&&
Vec_PtrSize
(
vCands2
)
==
0
)
continue
;
// save candidates
Nwk_ManGraphSetMapping
(
p
,
Nwk_ObjId
(
pLut
)
);
Vec_PtrForEachEntry
(
vCands1
,
pCand
,
k
)
Nwk_ManGraphHashEdge
(
p
,
Nwk_ObjId
(
pLut
),
Nwk_ObjId
(
pCand
)
);
Vec_PtrForEachEntry
(
vCands2
,
pCand
,
k
)
Nwk_ManGraphHashEdge
(
p
,
Nwk_ObjId
(
pLut
),
Nwk_ObjId
(
pCand
)
);
// print statistics about this node
printf
(
"Node %6d : Fanins = %d. Fanouts = %3d. Cand1 = %3d. Cand2 = %3d.
\n
"
,
Nwk_ObjId
(
pLut
),
Nwk_ObjFaninNum
(
pLut
),
Nwk_ObjFaninNum
(
pLut
),
Vec_PtrSize
(
vCands1
),
Vec_PtrSize
(
vCands2
)
);
}
Vec_PtrFree
(
vStart
);
Vec_PtrFree
(
vNext
);
Vec_PtrFree
(
vCands1
);
Vec_PtrFree
(
vCands2
);
// solve the graph problem
Nwk_ManGraphPrepare
(
p
);
Nwk_ManGraphSolve
(
p
);
vResult
=
p
->
vPairs
;
p
->
vPairs
=
NULL
;
Nwk_ManGraphFree
(
p
);
return
vResult
;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/nwk/nwkUtil_old.c
deleted
100644 → 0
View file @
7b734f23
/**CFile****************************************************************
FileName [nwkUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Logic network representation.]
Synopsis [Various utilities.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "nwk.h"
#include "kit.h"
#include <math.h>
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Increments the current traversal ID of the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManIncrementTravId
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pObj
;
int
i
;
if
(
pNtk
->
nTravIds
>=
(
1
<<
26
)
-
1
)
{
pNtk
->
nTravIds
=
0
;
Nwk_ManForEachObj
(
pNtk
,
pObj
,
i
)
pObj
->
TravId
=
0
;
}
pNtk
->
nTravIds
++
;
}
/**Function*************************************************************
Synopsis [Reads the maximum number of fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManGetFaninMax
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pNode
;
int
i
,
nFaninsMax
=
0
;
Nwk_ManForEachNode
(
pNtk
,
pNode
,
i
)
{
if
(
nFaninsMax
<
Nwk_ObjFaninNum
(
pNode
)
)
nFaninsMax
=
Nwk_ObjFaninNum
(
pNode
);
}
return
nFaninsMax
;
}
/**Function*************************************************************
Synopsis [Reads the total number of all fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManGetTotalFanins
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pNode
;
int
i
,
nFanins
=
0
;
Nwk_ManForEachNode
(
pNtk
,
pNode
,
i
)
nFanins
+=
Nwk_ObjFaninNum
(
pNode
);
return
nFanins
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManPiNum
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pNode
;
int
i
,
Counter
=
0
;
Nwk_ManForEachCi
(
pNtk
,
pNode
,
i
)
Counter
+=
Nwk_ObjIsPi
(
pNode
);
return
Counter
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManPoNum
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pNode
;
int
i
,
Counter
=
0
;
Nwk_ManForEachCo
(
pNtk
,
pNode
,
i
)
Counter
+=
Nwk_ObjIsPo
(
pNode
);
return
Counter
;
}
/**Function*************************************************************
Synopsis [Reads the number of BDD nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManGetAigNodeNum
(
Nwk_Man_t
*
pNtk
)
{
Nwk_Obj_t
*
pNode
;
int
i
,
nNodes
=
0
;
Nwk_ManForEachNode
(
pNtk
,
pNode
,
i
)
{
if
(
pNode
->
pFunc
==
NULL
)
{
printf
(
"Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.
\n
"
,
pNode
->
Id
);
continue
;
}
if
(
Nwk_ObjFaninNum
(
pNode
)
<
2
)
continue
;
nNodes
+=
Hop_DagSize
(
pNode
->
pFunc
);
}
return
nNodes
;
}
/**Function*************************************************************
Synopsis [Procedure used for sorting the nodes in increasing order of levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_NodeCompareLevelsIncrease
(
Nwk_Obj_t
**
pp1
,
Nwk_Obj_t
**
pp2
)
{
int
Diff
=
(
*
pp1
)
->
Level
-
(
*
pp2
)
->
Level
;
if
(
Diff
<
0
)
return
-
1
;
if
(
Diff
>
0
)
return
1
;
return
0
;
}
/**Function*************************************************************
Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_NodeCompareLevelsDecrease
(
Nwk_Obj_t
**
pp1
,
Nwk_Obj_t
**
pp2
)
{
int
Diff
=
(
*
pp1
)
->
Level
-
(
*
pp2
)
->
Level
;
if
(
Diff
>
0
)
return
-
1
;
if
(
Diff
<
0
)
return
1
;
return
0
;
}
/**Function*************************************************************
Synopsis [Deletes the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ObjPrint
(
Nwk_Obj_t
*
pObj
)
{
Nwk_Obj_t
*
pNext
;
int
i
;
printf
(
"ObjId = %5d. "
,
pObj
->
Id
);
if
(
Nwk_ObjIsPi
(
pObj
)
)
printf
(
"PI"
);
if
(
Nwk_ObjIsPo
(
pObj
)
)
printf
(
"PO"
);
if
(
Nwk_ObjIsNode
(
pObj
)
)
printf
(
"Node"
);
printf
(
" Fanins = "
);
Nwk_ObjForEachFanin
(
pObj
,
pNext
,
i
)
printf
(
"%d "
,
pNext
->
Id
);
printf
(
" Fanouts = "
);
Nwk_ObjForEachFanout
(
pObj
,
pNext
,
i
)
printf
(
"%d "
,
pNext
->
Id
);
printf
(
"
\n
"
);
}
/**Function*************************************************************
Synopsis [Deletes the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManDumpBlif
(
Nwk_Man_t
*
pNtk
,
char
*
pFileName
,
Vec_Ptr_t
*
vPiNames
,
Vec_Ptr_t
*
vPoNames
)
{
FILE
*
pFile
;
Vec_Ptr_t
*
vNodes
;
Vec_Int_t
*
vTruth
;
Vec_Int_t
*
vCover
;
Nwk_Obj_t
*
pObj
,
*
pFanin
;
Aig_MmFlex_t
*
pMem
;
char
*
pSop
=
NULL
;
unsigned
*
pTruth
;
int
i
,
k
,
nDigits
,
Counter
=
0
;
if
(
Nwk_ManPoNum
(
pNtk
)
==
0
)
{
printf
(
"Nwk_ManDumpBlif(): Network does not have POs.
\n
"
);
return
;
}
// collect nodes in the DFS order
nDigits
=
Aig_Base10Log
(
Nwk_ManObjNumMax
(
pNtk
)
);
// write the file
pFile
=
fopen
(
pFileName
,
"w"
);
fprintf
(
pFile
,
"# BLIF file written by procedure Nwk_ManDumpBlif()
\n
"
);
// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
fprintf
(
pFile
,
".model %s
\n
"
,
pNtk
->
pName
);
// write PIs
fprintf
(
pFile
,
".inputs"
);
Nwk_ManForEachCi
(
pNtk
,
pObj
,
i
)
if
(
vPiNames
)
fprintf
(
pFile
,
" %s"
,
Vec_PtrEntry
(
vPiNames
,
i
)
);
else
fprintf
(
pFile
,
" n%0*d"
,
nDigits
,
pObj
->
Id
);
fprintf
(
pFile
,
"
\n
"
);
// write POs
fprintf
(
pFile
,
".outputs"
);
Nwk_ManForEachCo
(
pNtk
,
pObj
,
i
)
if
(
vPoNames
)
fprintf
(
pFile
,
" %s"
,
Vec_PtrEntry
(
vPoNames
,
i
)
);
else
fprintf
(
pFile
,
" n%0*d"
,
nDigits
,
pObj
->
Id
);
fprintf
(
pFile
,
"
\n
"
);
// write nodes
pMem
=
Aig_MmFlexStart
();
vTruth
=
Vec_IntAlloc
(
1
<<
16
);
vCover
=
Vec_IntAlloc
(
1
<<
16
);
vNodes
=
Nwk_ManDfs
(
pNtk
);
Vec_PtrForEachEntry
(
vNodes
,
pObj
,
i
)
{
if
(
!
Nwk_ObjIsNode
(
pObj
)
)
continue
;
// derive SOP for the AIG
pTruth
=
Hop_ManConvertAigToTruth
(
pNtk
->
pManHop
,
Hop_Regular
(
pObj
->
pFunc
),
Nwk_ObjFaninNum
(
pObj
),
vTruth
,
0
);
if
(
Hop_IsComplement
(
pObj
->
pFunc
)
)
Kit_TruthNot
(
pTruth
,
pTruth
,
Nwk_ObjFaninNum
(
pObj
)
);
pSop
=
Kit_PlaFromTruth
(
pMem
,
pTruth
,
Nwk_ObjFaninNum
(
pObj
),
vCover
);
// write the node
fprintf
(
pFile
,
".names"
);
if
(
!
Kit_TruthIsConst0
(
pTruth
,
Nwk_ObjFaninNum
(
pObj
))
&&
!
Kit_TruthIsConst1
(
pTruth
,
Nwk_ObjFaninNum
(
pObj
))
)
{
Nwk_ObjForEachFanin
(
pObj
,
pFanin
,
k
)
if
(
vPiNames
&&
Nwk_ObjIsPi
(
pFanin
)
)
fprintf
(
pFile
,
" %s"
,
Vec_PtrEntry
(
vPiNames
,
Nwk_ObjPioNum
(
pFanin
))
);
else
fprintf
(
pFile
,
" n%0*d"
,
nDigits
,
pFanin
->
Id
);
}
fprintf
(
pFile
,
" n%0*d
\n
"
,
nDigits
,
pObj
->
Id
);
// write the function
fprintf
(
pFile
,
"%s"
,
pSop
);
}
Vec_IntFree
(
vCover
);
Vec_IntFree
(
vTruth
);
Vec_PtrFree
(
vNodes
);
Aig_MmFlexStop
(
pMem
,
0
);
// write POs
Nwk_ManForEachCo
(
pNtk
,
pObj
,
i
)
{
fprintf
(
pFile
,
".names"
);
if
(
vPiNames
&&
Nwk_ObjIsPi
(
Nwk_ObjFanin0
(
pObj
))
)
fprintf
(
pFile
,
" %s"
,
Vec_PtrEntry
(
vPiNames
,
Nwk_ObjPioNum
(
Nwk_ObjFanin0
(
pObj
)))
);
else
fprintf
(
pFile
,
" n%0*d"
,
nDigits
,
Nwk_ObjFanin0
(
pObj
)
->
Id
);
if
(
vPoNames
)
fprintf
(
pFile
,
" %s
\n
"
,
Vec_PtrEntry
(
vPoNames
,
Nwk_ObjPioNum
(
pObj
))
);
else
fprintf
(
pFile
,
" n%0*d
\n
"
,
nDigits
,
pObj
->
Id
);
fprintf
(
pFile
,
"%d 1
\n
"
,
!
pObj
->
fInvert
);
}
fprintf
(
pFile
,
".end
\n\n
"
);
fclose
(
pFile
);
}
/**Function*************************************************************
Synopsis [Prints the distribution of fanins/fanouts in the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManPrintFanioNew
(
Nwk_Man_t
*
pNtk
)
{
char
Buffer
[
100
];
Nwk_Obj_t
*
pNode
;
Vec_Int_t
*
vFanins
,
*
vFanouts
;
int
nFanins
,
nFanouts
,
nFaninsMax
,
nFanoutsMax
,
nFaninsAll
,
nFanoutsAll
;
int
i
,
k
,
nSizeMax
;
// determine the largest fanin and fanout
nFaninsMax
=
nFanoutsMax
=
0
;
nFaninsAll
=
nFanoutsAll
=
0
;
Nwk_ManForEachNode
(
pNtk
,
pNode
,
i
)
{
nFanins
=
Nwk_ObjFaninNum
(
pNode
);
nFanouts
=
Nwk_ObjFanoutNum
(
pNode
);
nFaninsAll
+=
nFanins
;
nFanoutsAll
+=
nFanouts
;
nFaninsMax
=
AIG_MAX
(
nFaninsMax
,
nFanins
);
nFanoutsMax
=
AIG_MAX
(
nFanoutsMax
,
nFanouts
);
}
// allocate storage for fanin/fanout numbers
nSizeMax
=
AIG_MAX
(
10
*
(
Aig_Base10Log
(
nFaninsMax
)
+
1
),
10
*
(
Aig_Base10Log
(
nFanoutsMax
)
+
1
)
);
vFanins
=
Vec_IntStart
(
nSizeMax
);
vFanouts
=
Vec_IntStart
(
nSizeMax
);
// count the number of fanins and fanouts
Nwk_ManForEachNode
(
pNtk
,
pNode
,
i
)
{
nFanins
=
Nwk_ObjFaninNum
(
pNode
);
nFanouts
=
Nwk_ObjFanoutNum
(
pNode
);
// nFanouts = Nwk_NodeMffcSize(pNode);
if
(
nFanins
<
10
)
Vec_IntAddToEntry
(
vFanins
,
nFanins
,
1
);
else
if
(
nFanins
<
100
)
Vec_IntAddToEntry
(
vFanins
,
10
+
nFanins
/
10
,
1
);
else
if
(
nFanins
<
1000
)
Vec_IntAddToEntry
(
vFanins
,
20
+
nFanins
/
100
,
1
);
else
if
(
nFanins
<
10000
)
Vec_IntAddToEntry
(
vFanins
,
30
+
nFanins
/
1000
,
1
);
else
if
(
nFanins
<
100000
)
Vec_IntAddToEntry
(
vFanins
,
40
+
nFanins
/
10000
,
1
);
else
if
(
nFanins
<
1000000
)
Vec_IntAddToEntry
(
vFanins
,
50
+
nFanins
/
100000
,
1
);
else
if
(
nFanins
<
10000000
)
Vec_IntAddToEntry
(
vFanins
,
60
+
nFanins
/
1000000
,
1
);
if
(
nFanouts
<
10
)
Vec_IntAddToEntry
(
vFanouts
,
nFanouts
,
1
);
else
if
(
nFanouts
<
100
)
Vec_IntAddToEntry
(
vFanouts
,
10
+
nFanouts
/
10
,
1
);
else
if
(
nFanouts
<
1000
)
Vec_IntAddToEntry
(
vFanouts
,
20
+
nFanouts
/
100
,
1
);
else
if
(
nFanouts
<
10000
)
Vec_IntAddToEntry
(
vFanouts
,
30
+
nFanouts
/
1000
,
1
);
else
if
(
nFanouts
<
100000
)
Vec_IntAddToEntry
(
vFanouts
,
40
+
nFanouts
/
10000
,
1
);
else
if
(
nFanouts
<
1000000
)
Vec_IntAddToEntry
(
vFanouts
,
50
+
nFanouts
/
100000
,
1
);
else
if
(
nFanouts
<
10000000
)
Vec_IntAddToEntry
(
vFanouts
,
60
+
nFanouts
/
1000000
,
1
);
}
printf
(
"The distribution of fanins and fanouts in the network:
\n
"
);
printf
(
" Number Nodes with fanin Nodes with fanout
\n
"
);
for
(
k
=
0
;
k
<
nSizeMax
;
k
++
)
{
if
(
vFanins
->
pArray
[
k
]
==
0
&&
vFanouts
->
pArray
[
k
]
==
0
)
continue
;
if
(
k
<
10
)
printf
(
"%15d : "
,
k
);
else
{
sprintf
(
Buffer
,
"%d - %d"
,
(
int
)
pow
(
10
,
k
/
10
)
*
(
k
%
10
),
(
int
)
pow
(
10
,
k
/
10
)
*
(
k
%
10
+
1
)
-
1
);
printf
(
"%15s : "
,
Buffer
);
}
if
(
vFanins
->
pArray
[
k
]
==
0
)
printf
(
" "
);
else
printf
(
"%12d "
,
vFanins
->
pArray
[
k
]
);
printf
(
" "
);
if
(
vFanouts
->
pArray
[
k
]
==
0
)
printf
(
" "
);
else
printf
(
"%12d "
,
vFanouts
->
pArray
[
k
]
);
printf
(
"
\n
"
);
}
Vec_IntFree
(
vFanins
);
Vec_IntFree
(
vFanouts
);
printf
(
"Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.
\n
"
,
nFaninsMax
,
1
.
0
*
nFaninsAll
/
Nwk_ManNodeNum
(
pNtk
),
nFanoutsMax
,
1
.
0
*
nFanoutsAll
/
Nwk_ManNodeNum
(
pNtk
)
);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManCleanMarks
(
Nwk_Man_t
*
pMan
)
{
Nwk_Obj_t
*
pObj
;
int
i
;
Nwk_ManForEachObj
(
pMan
,
pObj
,
i
)
pObj
->
MarkA
=
pObj
->
MarkB
=
0
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManMarkCone_rec
(
Nwk_Obj_t
*
pObj
)
{
Nwk_Obj_t
*
pNext
;
int
i
;
if
(
pObj
->
MarkA
)
return
;
pObj
->
MarkA
=
1
;
Nwk_ObjForEachFanin
(
pObj
,
pNext
,
i
)
Nwk_ManMarkCone_rec
(
pNext
);
}
/**Function*************************************************************
Synopsis [Returns 1 if the flow can be pushed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Nwk_ManPushFlow_rec
(
Nwk_Obj_t
*
pObj
)
{
Nwk_Obj_t
*
pNext
;
int
i
;
if
(
Nwk_ObjIsTravIdCurrent
(
pObj
)
)
return
0
;
Nwk_ObjSetTravIdCurrent
(
pObj
);
// check the case when there is no flow
if
(
!
pObj
->
MarkB
)
{
if
(
pObj
->
MarkA
)
return
pObj
->
MarkB
=
1
;
Nwk_ObjForEachFanin
(
pObj
,
pNext
,
i
)
if
(
Nwk_ManPushFlow_rec
(
pNext
)
)
return
pObj
->
MarkB
=
1
;
}
// check the case when there is no flow or we could not push the flow
Nwk_ObjForEachFanout
(
pObj
,
pNext
,
i
)
if
(
Nwk_ManPushFlow_rec
(
pNext
)
)
return
1
;
return
0
;
}
/**Function*************************************************************
Synopsis [Computes min-cut using max-flow.]
Description [MarkA means the sink. MarkB means the flow is present.]
SideEffects []
SeeAlso []
***********************************************************************/
void
Nwk_ManComputeCut
(
Nwk_Man_t
*
pMan
,
int
nLatches
)
{
Vec_Ptr_t
*
vNodes
;
Nwk_Obj_t
*
pObj
,
*
pNext
;
int
i
,
k
,
RetValue
,
Counter
=
0
;
// set the sequential parameters
pMan
->
nLatches
=
nLatches
;
pMan
->
nTruePis
=
Nwk_ManCiNum
(
pMan
)
-
nLatches
;
pMan
->
nTruePos
=
Nwk_ManCoNum
(
pMan
)
-
nLatches
;
// mark the CIs
Nwk_ManForEachCi
(
pMan
,
pObj
,
i
)
pObj
->
MarkA
=
1
;
// mark the TFI of the POs
Nwk_ManForEachPoSeq
(
pMan
,
pObj
,
i
)
Nwk_ManMarkCone_rec
(
pObj
);
// start flow computation from each LI
// Nwk_ManIncrementTravId( pMan );
Nwk_ManForEachLiSeq
(
pMan
,
pObj
,
i
)
{
Nwk_ManIncrementTravId
(
pMan
);
if
(
!
Nwk_ManPushFlow_rec
(
pObj
)
)
continue
;
// Nwk_ManIncrementTravId( pMan );
Counter
++
;
}
// mark the nodes reachable from the LIs
Nwk_ManIncrementTravId
(
pMan
);
Nwk_ManForEachLiSeq
(
pMan
,
pObj
,
i
)
{
RetValue
=
Nwk_ManPushFlow_rec
(
pObj
);
assert
(
RetValue
==
0
);
}
// collect labeled nodes whose all fanins are labeled
vNodes
=
Vec_PtrAlloc
(
Counter
);
Nwk_ManForEachObj
(
pMan
,
pObj
,
i
)
{
// skip unlabeled
if
(
!
Nwk_ObjIsTravIdCurrent
(
pObj
)
)
continue
;
// visit the fanins
Nwk_ObjForEachFanin
(
pObj
,
pNext
,
k
)
if
(
!
Nwk_ObjIsTravIdCurrent
(
pNext
)
)
break
;
if
(
k
==
Nwk_ObjFaninNum
(
pObj
)
)
Vec_PtrPush
(
vNodes
,
pObj
);
}
// unlabel these nodes
Nwk_ManIncrementTravId
(
pMan
);
Vec_PtrForEachEntry
(
vNodes
,
pObj
,
i
)
Nwk_ObjSetTravIdCurrent
(
pObj
);
// collect labeled nodes having unlabeled fanouts
Vec_PtrClear
(
vNodes
);
Nwk_ManForEachObj
(
pMan
,
pObj
,
i
)
{
// skip unreachable nodes
if
(
!
Nwk_ObjIsTravIdPrevious
(
pObj
)
)
continue
;
if
(
Nwk_ObjIsCo
(
pObj
)
)
{
Vec_PtrPush
(
vNodes
,
pObj
);
continue
;
}
Nwk_ObjForEachFanout
(
pObj
,
pNext
,
k
)
if
(
Nwk_ObjIsTravIdCurrent
(
pNext
)
)
break
;
if
(
k
<
Nwk_ObjFanoutNum
(
pObj
)
)
Vec_PtrPush
(
vNodes
,
pObj
);
}
// clean the marks
Nwk_ManCleanMarks
(
pMan
);
printf
(
"Flow = %5d. Cut = %5d.
\n
"
,
Counter
,
Vec_PtrSize
(
vNodes
)
);
Vec_PtrFree
(
vNodes
);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abc.c
View file @
c7b331ef
...
...
@@ -123,6 +123,7 @@ static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** arg
static
int
Abc_CommandQuaVar
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandQuaRel
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandQuaReach
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandSenseInput
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandIStrash
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandICut
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
...
...
@@ -228,6 +229,7 @@ static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** arg
static
int
Abc_CommandAbc8Lutpack
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc8Balance
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc8Speedup
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc8Merge
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc8Fraig
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc8Scl
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
...
...
@@ -380,6 +382,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd
(
pAbc
,
"Various"
,
"qvar"
,
Abc_CommandQuaVar
,
1
);
Cmd_CommandAdd
(
pAbc
,
"Various"
,
"qrel"
,
Abc_CommandQuaRel
,
1
);
Cmd_CommandAdd
(
pAbc
,
"Various"
,
"qreach"
,
Abc_CommandQuaReach
,
1
);
Cmd_CommandAdd
(
pAbc
,
"Various"
,
"senseinput"
,
Abc_CommandSenseInput
,
1
);
Cmd_CommandAdd
(
pAbc
,
"New AIG"
,
"istrash"
,
Abc_CommandIStrash
,
1
);
Cmd_CommandAdd
(
pAbc
,
"New AIG"
,
"icut"
,
Abc_CommandICut
,
0
);
...
...
@@ -480,6 +483,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*lp"
,
Abc_CommandAbc8Lutpack
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*b"
,
Abc_CommandAbc8Balance
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*speedup"
,
Abc_CommandAbc8Speedup
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*merge"
,
Abc_CommandAbc8Merge
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*fraig"
,
Abc_CommandAbc8Fraig
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC8"
,
"*scl"
,
Abc_CommandAbc8Scl
,
0
);
...
...
@@ -8096,6 +8100,98 @@ usage:
return
1
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Abc_CommandSenseInput
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
FILE
*
pOut
,
*
pErr
;
Abc_Ntk_t
*
pNtk
;
Vec_Int_t
*
vResult
;
int
c
,
nConfLim
,
fVerbose
;
extern
Vec_Int_t
*
Abc_NtkSensitivity
(
Abc_Ntk_t
*
pNtk
,
int
nConfLim
,
int
fVerbose
);
pNtk
=
Abc_FrameReadNtk
(
pAbc
);
pOut
=
Abc_FrameReadOut
(
pAbc
);
pErr
=
Abc_FrameReadErr
(
pAbc
);
// set defaults
nConfLim
=
1000
;
fVerbose
=
1
;
Extra_UtilGetoptReset
();
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"Cvh"
)
)
!=
EOF
)
{
switch
(
c
)
{
case
'C'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
pErr
,
"Command line switch
\"
-C
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
nConfLim
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
nConfLim
<
0
)
goto
usage
;
break
;
case
'v'
:
fVerbose
^=
1
;
break
;
case
'h'
:
goto
usage
;
default:
goto
usage
;
}
}
if
(
pNtk
==
NULL
)
{
fprintf
(
pErr
,
"Empty network.
\n
"
);
return
1
;
}
if
(
Abc_NtkGetChoiceNum
(
pNtk
)
)
{
fprintf
(
pErr
,
"This command cannot be applied to an AIG with choice nodes.
\n
"
);
return
1
;
}
if
(
!
Abc_NtkIsComb
(
pNtk
)
)
{
fprintf
(
pErr
,
"This command works only for combinational transition relations.
\n
"
);
return
1
;
}
if
(
!
Abc_NtkIsStrash
(
pNtk
)
)
{
fprintf
(
pErr
,
"This command works only for strashed networks.
\n
"
);
return
1
;
}
if
(
Abc_NtkPoNum
(
pNtk
)
<
2
)
{
fprintf
(
pErr
,
"The network should have at least two outputs.
\n
"
);
return
1
;
}
vResult
=
Abc_NtkSensitivity
(
pNtk
,
nConfLim
,
fVerbose
);
Vec_IntFree
(
vResult
);
return
0
;
usage:
fprintf
(
pErr
,
"usage: senseinput [-C num] [-vh]
\n
"
);
fprintf
(
pErr
,
"
\t
computes sensitivity of POs to PIs under constaint
\n
"
);
fprintf
(
pErr
,
"
\t
constraint should be represented as the last PO"
);
fprintf
(
pErr
,
"
\t
-C num : the max number of conflicts at a node [default = %d]
\n
"
,
nConfLim
);
fprintf
(
pErr
,
"
\t
-v : toggle printing verbose information [default = %s]
\n
"
,
fVerbose
?
"yes"
:
"no"
);
fprintf
(
pErr
,
"
\t
-h : print the command usage
\n
"
);
return
1
;
}
/**Function*************************************************************
...
...
@@ -17224,6 +17320,156 @@ usage:
return
1
;
}
//#include "nwk.h"
// the LUT merging parameters
typedef
struct
Nwk_LMPars_t_
Nwk_LMPars_t
;
struct
Nwk_LMPars_t_
{
int
nMaxLutSize
;
// the max LUT size for merging (N=5)
int
nMaxSuppSize
;
// the max total support size after merging (S=5)
int
nMaxDistance
;
// the max number of nodes separating LUTs
int
nMaxLevelDiff
;
// the max difference in levels
int
nMaxFanout
;
// the max number of fanouts to traverse
int
fUseTfiTfo
;
// enables the use of TFO/TFO nodes as candidates
int
fVeryVerbose
;
// enables additional verbose output
int
fVerbose
;
// enables verbose output
};
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Abc_CommandAbc8Merge
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
Nwk_LMPars_t
Pars
,
*
pPars
=
&
Pars
;
Vec_Int_t
*
vResult
;
int
c
;
int
fUseLutLib
=
0
;
int
Percentage
=
100
;
int
Degree
=
5
;
int
fVerbose
=
0
;
int
fVeryVerbose
=
0
;
extern
Vec_Int_t
*
Nwk_ManLutMerge
(
void
*
pNtk
,
Nwk_LMPars_t
*
pPars
);
// set defaults
memset
(
pPars
,
0
,
sizeof
(
Nwk_LMPars_t
)
);
pPars
->
nMaxLutSize
=
5
;
// the max LUT size for merging (N=5)
pPars
->
nMaxSuppSize
=
5
;
// the max total support size after merging (S=5)
pPars
->
nMaxDistance
=
3
;
// the max number of nodes separating LUTs
pPars
->
nMaxLevelDiff
=
2
;
// the max difference in levels
pPars
->
nMaxFanout
=
100
;
// the max number of fanouts to traverse
pPars
->
fUseTfiTfo
=
0
;
// enables the use of TFO/TFO nodes as candidates
pPars
->
fVeryVerbose
=
0
;
// enables additional verbose output
pPars
->
fVerbose
=
1
;
// enables verbose output
Extra_UtilGetoptReset
();
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"NSDLFcvwh"
)
)
!=
EOF
)
{
switch
(
c
)
{
case
'N'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
stdout
,
"Command line switch
\"
-N
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
pPars
->
nMaxLutSize
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
pPars
->
nMaxLutSize
<
2
)
goto
usage
;
break
;
case
'S'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
stdout
,
"Command line switch
\"
-S
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
pPars
->
nMaxSuppSize
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
pPars
->
nMaxSuppSize
<
2
)
goto
usage
;
break
;
case
'D'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
stdout
,
"Command line switch
\"
-D
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
pPars
->
nMaxDistance
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
pPars
->
nMaxDistance
<
2
)
goto
usage
;
break
;
case
'L'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
stdout
,
"Command line switch
\"
-L
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
pPars
->
nMaxLevelDiff
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
pPars
->
nMaxLevelDiff
<
2
)
goto
usage
;
break
;
case
'F'
:
if
(
globalUtilOptind
>=
argc
)
{
fprintf
(
stdout
,
"Command line switch
\"
-F
\"
should be followed by an integer.
\n
"
);
goto
usage
;
}
pPars
->
nMaxFanout
=
atoi
(
argv
[
globalUtilOptind
]);
globalUtilOptind
++
;
if
(
pPars
->
nMaxFanout
<
2
)
goto
usage
;
break
;
case
'c'
:
pPars
->
fUseTfiTfo
^=
1
;
break
;
case
'w'
:
pPars
->
fVeryVerbose
^=
1
;
break
;
case
'v'
:
pPars
->
fVerbose
^=
1
;
break
;
case
'h'
:
goto
usage
;
default:
goto
usage
;
}
}
if
(
pAbc
->
pAbc8Nwk
==
NULL
)
{
printf
(
"Abc_CommandAbc8Speedup(): There is no mapped network to merge LUTs.
\n
"
);
return
1
;
}
vResult
=
Nwk_ManLutMerge
(
pAbc
->
pAbc8Nwk
,
pPars
);
Vec_IntFree
(
vResult
);
return
0
;
usage:
fprintf
(
stdout
,
"usage: *merge [-NSDLF num] [-cwvh]
\n
"
);
fprintf
(
stdout
,
"
\t
creates pairs of topologically-related LUTs
\n
"
);
fprintf
(
stdout
,
"
\t
-N <num> : the max LUT size for merging (1 < num) [default = %d]
\n
"
,
pPars
->
nMaxLutSize
);
fprintf
(
stdout
,
"
\t
-S <num> : the max total support size after merging (1 < num) [default = %d]
\n
"
,
pPars
->
nMaxSuppSize
);
fprintf
(
stdout
,
"
\t
-D <num> : the max distance in terms of LUTs (0 < num) [default = %d]
\n
"
,
pPars
->
nMaxDistance
);
fprintf
(
stdout
,
"
\t
-L <num> : the max difference in levels (0 <= num) [default = %d]
\n
"
,
pPars
->
nMaxLevelDiff
);
fprintf
(
stdout
,
"
\t
-F <num> : the max number of fanouts to stop traversal (0 < num) [default = %d]
\n
"
,
pPars
->
nMaxFanout
);
fprintf
(
stdout
,
"
\t
-c : toggle the use of TFI/TFO nodes as candidates [default = %s]
\n
"
,
pPars
->
fUseTfiTfo
?
"yes"
:
"no"
);
fprintf
(
stdout
,
"
\t
-w : toggle printing detailed stats for each node [default = %s]
\n
"
,
pPars
->
fVeryVerbose
?
"yes"
:
"no"
);
fprintf
(
stdout
,
"
\t
-v : toggle printing optimization summary [default = %s]
\n
"
,
pPars
->
fVerbose
?
"yes"
:
"no"
);
fprintf
(
stdout
,
"
\t
-h : print the command usage
\n
"
);
return
1
;
}
/**Function*************************************************************
Synopsis []
...
...
src/base/abci/abcSense.c
0 → 100644
View file @
c7b331ef
/**CFile****************************************************************
FileName [abcSense.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "fraig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Copies the topmost levels of the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t
*
Abc_NtkSensitivityMiter_rec
(
Abc_Ntk_t
*
pNtkNew
,
Abc_Obj_t
*
pNode
)
{
assert
(
!
Abc_ObjIsComplement
(
pNode
)
);
if
(
pNode
->
pCopy
)
return
pNode
->
pCopy
;
Abc_NtkSensitivityMiter_rec
(
pNtkNew
,
Abc_ObjFanin0
(
pNode
)
);
Abc_NtkSensitivityMiter_rec
(
pNtkNew
,
Abc_ObjFanin1
(
pNode
)
);
return
pNode
->
pCopy
=
Abc_AigAnd
(
pNtkNew
->
pManFunc
,
Abc_ObjChild0Copy
(
pNode
),
Abc_ObjChild1Copy
(
pNode
)
);
}
/**Function*************************************************************
Synopsis [Creates miter for the sensitivity analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t
*
Abc_NtkSensitivityMiter
(
Abc_Ntk_t
*
pNtk
,
int
iVar
)
{
Abc_Ntk_t
*
pMiter
;
Vec_Ptr_t
*
vNodes
;
Abc_Obj_t
*
pObj
,
*
pNext
,
*
pFanin
,
*
pOutput
,
*
pObjNew
;
int
i
;
assert
(
Abc_NtkIsStrash
(
pNtk
)
);
assert
(
iVar
<
Abc_NtkCiNum
(
pNtk
)
);
// duplicate the network
pMiter
=
Abc_NtkAlloc
(
ABC_NTK_STRASH
,
ABC_FUNC_AIG
,
1
);
pMiter
->
pName
=
Extra_UtilStrsav
(
pNtk
->
pName
);
pMiter
->
pSpec
=
Extra_UtilStrsav
(
pNtk
->
pSpec
);
// assign the PIs
Abc_NtkCleanCopy
(
pNtk
);
Abc_AigConst1
(
pNtk
)
->
pCopy
=
Abc_AigConst1
(
pMiter
);
Abc_AigConst1
(
pNtk
)
->
pData
=
Abc_AigConst1
(
pMiter
);
Abc_NtkForEachCi
(
pNtk
,
pObj
,
i
)
pObj
->
pCopy
=
pObj
->
pData
=
Abc_NtkCreatePi
(
pMiter
);
Abc_NtkAddDummyPiNames
(
pMiter
);
// assign the cofactors of the CI node to be constants
pObj
=
Abc_NtkCi
(
pNtk
,
iVar
);
pObj
->
pCopy
=
Abc_ObjNot
(
Abc_AigConst1
(
pMiter
)
);
pObj
->
pData
=
Abc_AigConst1
(
pMiter
);
// collect the internal nodes
vNodes
=
Abc_NtkDfsReverseNodes
(
pNtk
,
&
pObj
,
1
);
Vec_PtrForEachEntry
(
vNodes
,
pObj
,
i
)
{
for
(
pNext
=
pObj
?
pObj
->
pCopy
:
pObj
;
pObj
;
pObj
=
pNext
,
pNext
=
pObj
?
pObj
->
pCopy
:
pObj
)
{
pFanin
=
Abc_ObjFanin0
(
pObj
);
if
(
!
Abc_NodeIsTravIdCurrent
(
pFanin
)
)
pFanin
->
pData
=
Abc_NtkSensitivityMiter_rec
(
pMiter
,
pFanin
);
pFanin
=
Abc_ObjFanin1
(
pObj
);
if
(
!
Abc_NodeIsTravIdCurrent
(
pFanin
)
)
pFanin
->
pData
=
Abc_NtkSensitivityMiter_rec
(
pMiter
,
pFanin
);
pObj
->
pCopy
=
Abc_AigAnd
(
pMiter
->
pManFunc
,
Abc_ObjChild0Copy
(
pObj
),
Abc_ObjChild1Copy
(
pObj
)
);
pObj
->
pData
=
Abc_AigAnd
(
pMiter
->
pManFunc
,
Abc_ObjChild0Data
(
pObj
),
Abc_ObjChild1Data
(
pObj
)
);
}
}
Vec_PtrFree
(
vNodes
);
// update the affected COs
pOutput
=
Abc_ObjNot
(
Abc_AigConst1
(
pMiter
)
);
Abc_NtkForEachCo
(
pNtk
,
pObj
,
i
)
{
if
(
!
Abc_NodeIsTravIdCurrent
(
pObj
)
)
continue
;
// get the result of quantification
if
(
i
==
Abc_NtkCoNum
(
pNtk
)
-
1
)
{
pOutput
=
Abc_AigAnd
(
pMiter
->
pManFunc
,
pOutput
,
Abc_ObjChild0Data
(
pObj
)
);
pOutput
=
Abc_AigAnd
(
pMiter
->
pManFunc
,
pOutput
,
Abc_ObjChild0Copy
(
pObj
)
);
}
else
{
pNext
=
Abc_AigXor
(
pMiter
->
pManFunc
,
Abc_ObjChild0Copy
(
pObj
),
Abc_ObjChild0Data
(
pObj
)
);
pOutput
=
Abc_AigOr
(
pMiter
->
pManFunc
,
pOutput
,
pNext
);
}
}
// add the PO node and name
pObjNew
=
Abc_NtkCreatePo
(
pMiter
);
Abc_ObjAddFanin
(
pObjNew
,
pOutput
);
Abc_ObjAssignName
(
pObjNew
,
"miter"
,
NULL
);
// make sure everything is okay
if
(
!
Abc_NtkCheck
(
pMiter
)
)
{
printf
(
"Abc_NtkSensitivityMiter: The network check has failed.
\n
"
);
Abc_NtkDelete
(
pMiter
);
return
NULL
;
}
return
pMiter
;
}
/**Function*************************************************************
Synopsis [Computing sensitivity of POs to POs under constaints.]
Description [The input network is a combinatonal AIG. The last output
is a constraint. The procedure returns the list of number of PIs,
such that at least one PO depends on this PI, under the constraint.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t
*
Abc_NtkSensitivity
(
Abc_Ntk_t
*
pNtk
,
int
nConfLim
,
int
fVerbose
)
{
ProgressBar
*
pProgress
;
Prove_Params_t
Params
,
*
pParams
=
&
Params
;
Vec_Int_t
*
vResult
=
NULL
;
Abc_Ntk_t
*
pMiter
;
Abc_Obj_t
*
pObj
;
int
RetValue
,
i
;
assert
(
Abc_NtkIsStrash
(
pNtk
)
);
assert
(
Abc_NtkLatchNum
(
pNtk
)
==
0
);
// set up solving parameters
Prove_ParamsSetDefault
(
pParams
);
pParams
->
nItersMax
=
3
;
pParams
->
nMiteringLimitLast
=
nConfLim
;
// iterate through the PIs
vResult
=
Vec_IntAlloc
(
100
);
pProgress
=
Extra_ProgressBarStart
(
stdout
,
Abc_NtkCiNum
(
pNtk
)
);
Abc_NtkForEachCi
(
pNtk
,
pObj
,
i
)
{
Extra_ProgressBarUpdate
(
pProgress
,
i
,
NULL
);
// generate the sensitivity miter
pMiter
=
Abc_NtkSensitivityMiter
(
pNtk
,
i
);
// solve the miter using CEC engine
RetValue
=
Abc_NtkIvyProve
(
&
pMiter
,
pParams
);
if
(
RetValue
==
-
1
)
// undecided
Vec_IntPush
(
vResult
,
i
);
else
if
(
RetValue
==
0
)
{
int
*
pSimInfo
=
Abc_NtkVerifySimulatePattern
(
pMiter
,
pMiter
->
pModel
);
if
(
pSimInfo
[
0
]
!=
1
)
printf
(
"ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.
\n
"
);
// else
// printf( "Networks are NOT EQUIVALENT.\n" );
free
(
pSimInfo
);
Vec_IntPush
(
vResult
,
i
);
}
Abc_NtkDelete
(
pMiter
);
}
Extra_ProgressBarStop
(
pProgress
);
if
(
fVerbose
)
{
printf
(
"The outputs are sensitive to %d (out of %d) inputs:
\n
"
,
Vec_IntSize
(
vResult
),
Abc_NtkCiNum
(
pNtk
)
);
Vec_IntForEachEntry
(
vResult
,
RetValue
,
i
)
printf
(
"%d "
,
RetValue
);
printf
(
"
\n
"
);
}
return
vResult
;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/module.make
View file @
c7b331ef
...
...
@@ -48,6 +48,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcRewrite.c
\
src/base/abci/abcRr.c
\
src/base/abci/abcSat.c
\
src/base/abci/abcSense.c
\
src/base/abci/abcStrash.c
\
src/base/abci/abcSweep.c
\
src/base/abci/abcSymm.c
\
...
...
todo.txt
View file @
c7b331ef
- required time support
- printing ABC version/platform in the output files
- fix gcc compiler warnings
- port "mfs" from MVSIS
- improve AIG rewriting package
- unify functional representation of local functions
- additional rewriting options for delay optimization
- experiment with yield-aware standard-cell mapping
- improving area recovery in integrated sequential synthesis
- high-effort logic synthesis for hard miters (cofactoring, Boolean division)
- mapping into MV cells
- SAT solver with linear constraints
- specialized synthesis for EXORs and large MUXes
- sequential AIG rewriting initial state computation
- placement-aware mapping
- sequential equivalence checking
- parser for Verilog netlists
- hierarchy manager (hierarchical BLIF/BLIF-MV parser)
- required time based on all cuts
- comparing tts of differently derived the same cut
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment