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
edba505d
Commit
edba505d
authored
Aug 02, 2014
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Profiling code for SOP/DSD/LMS balancing.
parent
62bc45d1
Show whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
465 additions
and
0 deletions
+465
-0
src/aig/gia/giaMffc.c
+308
-0
src/base/abci/abcRec3.c
+20
-0
src/map/if/ifDelay.c
+29
-0
src/map/if/ifDsd.c
+21
-0
src/misc/util/utilTruth.h
+87
-0
No files found.
src/aig/gia/giaMffc.c
0 → 100644
View file @
edba505d
/**CFile****************************************************************
FileName [gia.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static
inline
int
Gia_ObjDom
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
)
{
return
Vec_IntEntry
(
p
->
vDoms
,
Gia_ObjId
(
p
,
pObj
));
}
static
inline
void
Gia_ObjSetDom
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
int
d
)
{
Vec_IntWriteEntry
(
p
->
vDoms
,
Gia_ObjId
(
p
,
pObj
),
d
);
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes one-node dominators.]
Description [For each node, computes the closest one-node dominator,
which can be the node itself if the node has no other dominators.]
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
void
Gia_ManAddDom
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
int
iDom0
)
{
int
iDom1
,
iDomNext
;
if
(
Gia_ObjDom
(
p
,
pObj
)
==
-
1
)
{
Gia_ObjSetDom
(
p
,
pObj
,
iDom0
);
return
;
}
iDom1
=
Gia_ObjDom
(
p
,
pObj
);
while
(
1
)
{
if
(
iDom0
>
iDom1
)
{
iDomNext
=
Gia_ObjDom
(
p
,
Gia_ManObj
(
p
,
iDom1
)
);
if
(
iDomNext
==
iDom1
)
break
;
iDom1
=
iDomNext
;
continue
;
}
if
(
iDom1
>
iDom0
)
{
iDomNext
=
Gia_ObjDom
(
p
,
Gia_ManObj
(
p
,
iDom0
)
);
if
(
iDomNext
==
iDom0
)
break
;
iDom0
=
iDomNext
;
continue
;
}
assert
(
iDom0
==
iDom1
);
Gia_ObjSetDom
(
p
,
pObj
,
iDom0
);
return
;
}
Gia_ObjSetDom
(
p
,
pObj
,
Gia_ObjId
(
p
,
pObj
)
);
}
static
inline
void
Gia_ManComputeDoms
(
Gia_Man_t
*
p
)
{
Gia_Obj_t
*
pObj
;
int
i
;
if
(
p
->
vDoms
==
NULL
)
p
->
vDoms
=
Vec_IntAlloc
(
0
);
Vec_IntFill
(
p
->
vDoms
,
Gia_ManObjNum
(
p
),
-
1
);
Gia_ManForEachObjReverse
(
p
,
pObj
,
i
)
{
if
(
i
==
0
||
Gia_ObjIsCi
(
pObj
)
)
continue
;
if
(
Gia_ObjIsCo
(
pObj
)
)
{
Gia_ObjSetDom
(
p
,
pObj
,
i
);
Gia_ManAddDom
(
p
,
Gia_ObjFanin0
(
pObj
),
i
);
continue
;
}
assert
(
Gia_ObjIsAnd
(
pObj
)
);
Gia_ManAddDom
(
p
,
Gia_ObjFanin0
(
pObj
),
i
);
Gia_ManAddDom
(
p
,
Gia_ObjFanin1
(
pObj
),
i
);
}
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes in the MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
int
Gia_NodeDeref_rec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pNode
)
{
Gia_Obj_t
*
pFanin
;
int
Counter
=
0
;
if
(
Gia_ObjIsCi
(
pNode
)
)
return
0
;
assert
(
Gia_ObjIsAnd
(
pNode
)
);
pFanin
=
Gia_ObjFanin0
(
pNode
);
assert
(
Gia_ObjRefNum
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeDeref_rec
(
p
,
pFanin
);
pFanin
=
Gia_ObjFanin1
(
pNode
);
assert
(
Gia_ObjRefNum
(
p
,
pFanin
)
>
0
);
if
(
Gia_ObjRefDec
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeDeref_rec
(
p
,
pFanin
);
return
Counter
+
1
;
}
static
inline
int
Gia_NodeRef_rec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pNode
)
{
Gia_Obj_t
*
pFanin
;
int
Counter
=
0
;
if
(
Gia_ObjIsCi
(
pNode
)
)
return
0
;
assert
(
Gia_ObjIsAnd
(
pNode
)
);
pFanin
=
Gia_ObjFanin0
(
pNode
);
if
(
Gia_ObjRefInc
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeRef_rec
(
p
,
pFanin
);
pFanin
=
Gia_ObjFanin1
(
pNode
);
if
(
Gia_ObjRefInc
(
p
,
pFanin
)
==
0
)
Counter
+=
Gia_NodeRef_rec
(
p
,
pFanin
);
return
Counter
+
1
;
}
static
inline
void
Gia_NodeCollect_rec
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pNode
,
Vec_Int_t
*
vSupp
,
Vec_Int_t
*
vSuppRefs
)
{
if
(
Gia_ObjIsTravIdCurrent
(
p
,
pNode
)
)
return
;
Gia_ObjSetTravIdCurrent
(
p
,
pNode
);
if
(
Gia_ObjRefNum
(
p
,
pNode
)
||
Gia_ObjIsCi
(
pNode
)
)
{
Vec_IntPush
(
vSupp
,
Gia_ObjId
(
p
,
pNode
)
);
Vec_IntPush
(
vSuppRefs
,
Gia_ObjRefNum
(
p
,
pNode
)
);
return
;
}
assert
(
Gia_ObjIsAnd
(
pNode
)
);
Gia_NodeCollect_rec
(
p
,
Gia_ObjFanin0
(
pNode
),
vSupp
,
vSuppRefs
);
Gia_NodeCollect_rec
(
p
,
Gia_ObjFanin1
(
pNode
),
vSupp
,
vSuppRefs
);
}
static
inline
int
Gia_NodeMffcSizeSupp
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pNode
,
Vec_Int_t
*
vSupp
,
Vec_Int_t
*
vSuppRefs
)
{
int
ConeSize1
,
ConeSize2
,
i
,
iObj
;
assert
(
!
Gia_IsComplement
(
pNode
)
);
assert
(
Gia_ObjIsAnd
(
pNode
)
);
Vec_IntClear
(
vSupp
);
Vec_IntClear
(
vSuppRefs
);
Gia_ManIncrementTravId
(
p
);
ConeSize1
=
Gia_NodeDeref_rec
(
p
,
pNode
);
Gia_NodeCollect_rec
(
p
,
Gia_ObjFanin0
(
pNode
),
vSupp
,
vSuppRefs
);
Gia_NodeCollect_rec
(
p
,
Gia_ObjFanin1
(
pNode
),
vSupp
,
vSuppRefs
);
ConeSize2
=
Gia_NodeRef_rec
(
p
,
pNode
);
assert
(
ConeSize1
==
ConeSize2
);
assert
(
ConeSize1
>=
0
);
// record supp refs
Vec_IntForEachEntry
(
vSupp
,
iObj
,
i
)
Vec_IntAddToEntry
(
vSuppRefs
,
i
,
-
Gia_ObjRefNumId
(
p
,
iObj
)
);
return
ConeSize1
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Gia_ManDomDerive_rec
(
Gia_Man_t
*
pNew
,
Gia_Man_t
*
p
,
Gia_Obj_t
*
pNode
)
{
if
(
Gia_ObjIsTravIdCurrent
(
p
,
pNode
)
)
return
pNode
->
Value
;
Gia_ObjSetTravIdCurrent
(
p
,
pNode
);
assert
(
Gia_ObjIsAnd
(
pNode
)
);
Gia_ManDomDerive_rec
(
pNew
,
p
,
Gia_ObjFanin0
(
pNode
)
);
Gia_ManDomDerive_rec
(
pNew
,
p
,
Gia_ObjFanin1
(
pNode
)
);
return
pNode
->
Value
=
Gia_ManHashAnd
(
pNew
,
Gia_ObjFanin0Copy
(
pNode
),
Gia_ObjFanin1Copy
(
pNode
)
);
}
Gia_Man_t
*
Gia_ManDomDerive
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pRoot
,
Vec_Int_t
*
vSupp
,
int
nVars
)
{
Gia_Man_t
*
pNew
,
*
pTemp
;
int
nMints
=
1
<<
nVars
;
int
i
,
m
,
iResLit
;
assert
(
nVars
>
0
&&
nVars
<=
5
);
pNew
=
Gia_ManStart
(
Gia_ManObjNum
(
p
)
);
pNew
->
pName
=
Abc_UtilStrsav
(
p
->
pName
);
pNew
->
pSpec
=
Abc_UtilStrsav
(
p
->
pSpec
);
Gia_ManConst0
(
p
)
->
Value
=
0
;
Gia_ManHashAlloc
(
pNew
);
for
(
i
=
0
;
i
<
Vec_IntSize
(
vSupp
);
i
++
)
Gia_ManAppendCi
(
pNew
);
for
(
m
=
0
;
m
<
nMints
;
m
++
)
{
Gia_Obj_t
*
pObj
;
Gia_ManIncrementTravId
(
p
);
Gia_ManForEachObjVec
(
vSupp
,
p
,
pObj
,
i
)
{
if
(
i
<
nVars
)
pObj
->
Value
=
(
m
>>
i
)
&
1
;
else
pObj
->
Value
=
Gia_ObjToLit
(
pNew
,
Gia_ManCi
(
pNew
,
i
));
Gia_ObjSetTravIdCurrent
(
p
,
pObj
);
}
iResLit
=
Gia_ManDomDerive_rec
(
pNew
,
p
,
pRoot
);
Gia_ManAppendCo
(
pNew
,
iResLit
);
}
Gia_ManHashStop
(
pNew
);
pNew
=
Gia_ManCleanup
(
pTemp
=
pNew
);
Gia_ManStop
(
pTemp
);
return
pNew
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Gia_ManComputeDomsTry
(
Gia_Man_t
*
p
)
{
Vec_Int_t
*
vSupp
,
*
vSuppRefs
;
Gia_Man_t
*
pNew
;
Gia_Obj_t
*
pObj
;
int
i
,
nSize
,
Entry
,
k
;
abctime
clk
=
Abc_Clock
();
ABC_FREE
(
p
->
pRefs
);
Gia_ManLevelNum
(
p
);
Gia_ManCreateRefs
(
p
);
Gia_ManComputeDoms
(
p
);
Abc_PrintTime
(
1
,
"Time"
,
Abc_Clock
()
-
clk
);
vSupp
=
Vec_IntAlloc
(
1000
);
vSuppRefs
=
Vec_IntAlloc
(
1000
);
Gia_ManForEachObj
(
p
,
pObj
,
i
)
{
if
(
!
Gia_ObjIsAnd
(
pObj
)
&&
!
Gia_ObjIsCo
(
pObj
)
)
continue
;
if
(
Gia_ObjDom
(
p
,
pObj
)
!=
i
)
continue
;
if
(
Gia_ObjIsCo
(
pObj
)
)
pObj
=
Gia_ObjFanin0
(
pObj
);
if
(
!
Gia_ObjIsAnd
(
pObj
)
)
continue
;
nSize
=
Gia_NodeMffcSizeSupp
(
p
,
pObj
,
vSupp
,
vSuppRefs
);
if
(
nSize
<
30
||
nSize
>
100
)
continue
;
// sort by cost
Vec_IntSelectSortCost2
(
Vec_IntArray
(
vSupp
),
Vec_IntSize
(
vSupp
),
Vec_IntArray
(
vSuppRefs
)
);
printf
(
"Obj %6d : "
,
i
);
printf
(
"Cone = %4d "
,
nSize
);
printf
(
"Supp = %4d "
,
Vec_IntSize
(
vSupp
)
);
Vec_IntForEachEntry
(
vSuppRefs
,
Entry
,
k
)
printf
(
"%d(%d) "
,
-
Entry
,
Gia_ObjLevelId
(
p
,
Vec_IntEntry
(
vSupp
,
k
))
);
printf
(
"
\n
"
);
// selected k
for
(
k
=
0
;
k
<
Vec_IntSize
(
vSupp
);
k
++
)
if
(
Vec_IntEntry
(
vSuppRefs
,
k
)
==
1
)
break
;
k
=
Abc_MinInt
(
k
,
3
);
// dump
pNew
=
Gia_ManDomDerive
(
p
,
pObj
,
vSupp
,
k
);
Gia_DumpAiger
(
pNew
,
"mffc"
,
i
,
6
);
Gia_ManStop
(
pNew
);
}
Vec_IntFree
(
vSuppRefs
);
Vec_IntFree
(
vSupp
);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/base/abci/abcRec3.c
View file @
edba505d
...
...
@@ -979,6 +979,26 @@ p->timeCanon += Abc_Clock() - clk;
pCut
->
Cost
=
Vec_StrEntry
(
p
->
vAreas
,
iBestPo
);
for
(
i
=
0
;
i
<
nLeaves
;
i
++
)
pPerm
[(
int
)
pCanonPerm
[
i
]]
=
Lms_DelayGet
(
DelayProfile
,
i
);
if
(
0
)
{
int
Max
=
0
,
Two
=
0
,
pTimes
[
16
];
for
(
i
=
0
;
i
<
nLeaves
;
i
++
)
pTimes
[
i
]
=
(
int
)
If_ObjCutBest
(
If_CutLeaf
(
pIfMan
,
pCut
,
i
))
->
Delay
;
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
Max
=
Abc_MaxInt
(
Max
,
pTimes
[
i
]
);
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
if
(
pTimes
[
i
]
!=
Max
)
Two
=
Abc_MaxInt
(
Two
,
pTimes
[
i
]
);
if
(
Two
+
2
<
Max
&&
Max
+
3
<
BestDelay
)
{
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
printf
(
"%3d "
,
pTimes
[
i
]
);
for
(
;
i
<
pIfMan
->
pPars
->
nLutSize
;
i
++
)
printf
(
" "
);
printf
(
"-> %3d "
,
BestDelay
);
Dau_DsdPrintFromTruth
(
If_CutTruthW
(
pIfMan
,
pCut
),
If_CutLeaveNum
(
pCut
)
);
}
}
return
BestDelay
;
}
int
If_CutDelayRecCost3
(
If_Man_t
*
pIfMan
,
If_Cut_t
*
pCut
,
If_Obj_t
*
pObj
)
...
...
src/map/if/ifDelay.c
View file @
edba505d
...
...
@@ -269,6 +269,7 @@ int If_CutSopBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
}
else
{
int
fVerbose
=
0
;
Vec_Int_t
*
vCover
=
Vec_WecEntry
(
p
->
vTtIsops
[
pCut
->
nLeaves
],
Abc_Lit2Var
(
If_CutTruthLit
(
pCut
))
);
int
Delay
,
Area
=
0
;
int
i
,
pTimes
[
IF_MAX_FUNC_LUTSIZE
];
...
...
@@ -279,6 +280,34 @@ int If_CutSopBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
pTimes
[
i
]
=
(
int
)
If_ObjCutBest
(
If_CutLeaf
(
p
,
pCut
,
i
))
->
Delay
;
Delay
=
If_CutSopBalanceEvalIntInt
(
vCover
,
If_CutLeaveNum
(
pCut
),
pTimes
,
vAig
,
Abc_LitIsCompl
(
If_CutTruthLit
(
pCut
))
^
pCut
->
fCompl
,
&
Area
);
pCut
->
Cost
=
Area
;
if
(
fVerbose
)
{
int
Max
=
0
,
Two
=
0
;
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
Max
=
Abc_MaxInt
(
Max
,
pTimes
[
i
]
);
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
if
(
pTimes
[
i
]
!=
Max
)
Two
=
Abc_MaxInt
(
Two
,
pTimes
[
i
]
);
if
(
Two
+
2
<
Max
&&
Max
+
3
<
Delay
)
{
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
printf
(
"%3d "
,
pTimes
[
i
]
);
for
(
;
i
<
p
->
pPars
->
nLutSize
;
i
++
)
printf
(
" "
);
printf
(
"-> %3d "
,
Delay
);
Dau_DsdPrintFromTruth
(
If_CutTruthW
(
p
,
pCut
),
If_CutLeaveNum
(
pCut
)
);
Kit_TruthIsopPrintCover
(
vCover
,
If_CutLeaveNum
(
pCut
),
Abc_LitIsCompl
(
If_CutTruthLit
(
pCut
))
^
pCut
->
fCompl
);
{
Vec_Int_t
vIsop
;
int
pIsop
[
64
];
vIsop
.
nCap
=
vIsop
.
nSize
=
Abc_Tt6Esop
(
*
If_CutTruthW
(
p
,
pCut
),
pCut
->
nLeaves
,
pIsop
);
vIsop
.
pArray
=
pIsop
;
printf
(
"ESOP (%d -> %d)
\n
"
,
Vec_IntSize
(
vCover
),
vIsop
.
nSize
);
Kit_TruthIsopPrintCover
(
&
vIsop
,
If_CutLeaveNum
(
pCut
),
0
);
}
printf
(
"
\n
"
);
}
}
return
Delay
;
}
}
...
...
src/map/if/ifDsd.c
View file @
edba505d
...
...
@@ -2096,12 +2096,33 @@ int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig )
}
else
{
int
fVerbose
=
0
;
int
i
,
pTimes
[
IF_MAX_FUNC_LUTSIZE
];
int
Delay
,
Area
=
0
;
char
*
pPermLits
=
If_CutDsdPerm
(
p
,
pCut
);
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
pTimes
[
i
]
=
(
int
)
If_ObjCutBest
(
If_CutLeaf
(
p
,
pCut
,
i
))
->
Delay
;
Delay
=
If_CutDsdBalanceEvalInt
(
p
->
pIfDsdMan
,
Abc_LitNotCond
(
If_CutDsdLit
(
p
,
pCut
),
pCut
->
fCompl
),
pTimes
,
vAig
,
&
Area
,
If_CutDsdPerm
(
p
,
pCut
)
);
pCut
->
Cost
=
Area
;
if
(
fVerbose
)
{
int
Max
=
0
,
Two
=
0
;
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
Max
=
Abc_MaxInt
(
Max
,
pTimes
[
i
]
);
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
if
(
pTimes
[
i
]
!=
Max
)
Two
=
Abc_MaxInt
(
Two
,
pTimes
[
i
]
);
if
(
Two
+
2
<
Max
&&
Max
+
3
<
Delay
)
{
for
(
i
=
0
;
i
<
If_CutLeaveNum
(
pCut
);
i
++
)
printf
(
"%3d "
,
pTimes
[
Abc_Lit2Var
(
pPermLits
[
i
])]
);
for
(
;
i
<
p
->
pPars
->
nLutSize
;
i
++
)
printf
(
" "
);
printf
(
"-> %3d "
,
Delay
);
If_DsdManPrintOne
(
stdout
,
p
->
pIfDsdMan
,
Abc_Lit2Var
(
If_CutDsdLit
(
p
,
pCut
)),
NULL
,
0
);
printf
(
"
\n
"
);
}
}
return
Delay
;
}
}
...
...
src/misc/util/utilTruth.h
View file @
edba505d
...
...
@@ -1728,6 +1728,93 @@ static inline int Abc_Tt8Cnf( word t[4], int nVars, int * pCover )
/**Function*************************************************************
Synopsis [Computes ISOP for 6 variables or less.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
inline
int
Abc_Tt6Esop
(
word
t
,
int
nVars
,
int
*
pCover
)
{
word
c0
,
c1
;
int
Var
,
r0
,
r1
,
r2
,
Max
,
i
;
assert
(
nVars
<=
6
);
if
(
t
==
0
)
return
0
;
if
(
t
==
~
(
word
)
0
)
{
if
(
pCover
)
*
pCover
=
0
;
return
1
;
}
assert
(
nVars
>
0
);
// find the topmost var
for
(
Var
=
nVars
-
1
;
Var
>=
0
;
Var
--
)
if
(
Abc_Tt6HasVar
(
t
,
Var
)
)
break
;
assert
(
Var
>=
0
);
// cofactor
c0
=
Abc_Tt6Cofactor0
(
t
,
Var
);
c1
=
Abc_Tt6Cofactor1
(
t
,
Var
);
// call recursively
r0
=
Abc_Tt6Esop
(
c0
,
Var
,
pCover
?
pCover
:
NULL
);
r1
=
Abc_Tt6Esop
(
c1
,
Var
,
pCover
?
pCover
+
r0
:
NULL
);
r2
=
Abc_Tt6Esop
(
c0
^
c1
,
Var
,
pCover
?
pCover
+
r0
+
r1
:
NULL
);
Max
=
Abc_MaxInt
(
r0
,
Abc_MaxInt
(
r1
,
r2
)
);
// add literals
if
(
pCover
)
{
if
(
Max
==
r0
)
{
for
(
i
=
0
;
i
<
r1
;
i
++
)
pCover
[
i
]
=
pCover
[
r0
+
i
];
for
(
i
=
0
;
i
<
r2
;
i
++
)
pCover
[
r1
+
i
]
=
pCover
[
r0
+
r1
+
i
]
|
(
1
<<
(
2
*
Var
+
0
));
}
else
if
(
Max
==
r1
)
{
for
(
i
=
0
;
i
<
r2
;
i
++
)
pCover
[
r0
+
i
]
=
pCover
[
r0
+
r1
+
i
]
|
(
1
<<
(
2
*
Var
+
1
));
}
else
{
for
(
i
=
0
;
i
<
r0
;
i
++
)
pCover
[
i
]
|=
(
1
<<
(
2
*
Var
+
0
));
for
(
i
=
0
;
i
<
r1
;
i
++
)
pCover
[
r0
+
i
]
|=
(
1
<<
(
2
*
Var
+
1
));
}
}
return
r0
+
r1
+
r2
-
Max
;
}
static
inline
word
Abc_Tt6EsopBuild
(
int
nVars
,
int
*
pCover
,
int
nCubes
)
{
word
p
,
t
=
0
;
int
c
,
v
;
for
(
c
=
0
;
c
<
nCubes
;
c
++
)
{
p
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
nVars
;
v
++
)
if
(
((
pCover
[
c
]
>>
(
v
<<
1
))
&
3
)
==
1
)
p
&=
~
s_Truths6
[
v
];
else
if
(
((
pCover
[
c
]
>>
(
v
<<
1
))
&
3
)
==
2
)
p
&=
s_Truths6
[
v
];
t
^=
p
;
}
return
t
;
}
static
inline
int
Abc_Tt6EsopVerify
(
word
t
,
int
nVars
)
{
int
pCover
[
64
];
int
nCubes
=
Abc_Tt6Esop
(
t
,
nVars
,
pCover
);
word
t2
=
Abc_Tt6EsopBuild
(
nVars
,
pCover
,
nCubes
);
if
(
t
!=
t2
)
printf
(
"Verification failed.
\n
"
);
return
nCubes
;
}
/**Function*************************************************************
Synopsis [Check if the function is decomposable with the given pair.]
Description []
...
...
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