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
e6e6a3cf
Commit
e6e6a3cf
authored
Oct 01, 2011
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Changes to the matching procedure.
parent
ff4c674d
Show whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
624 additions
and
167 deletions
+624
-167
src/base/abci/abc.c
+15
-5
src/map/if/if.h
+9
-5
src/map/if/ifCut.c
+1
-1
src/map/if/ifDec07.c
+5
-4
src/map/if/ifDec08.c
+1
-1
src/map/if/ifDec10.c
+1
-1
src/map/if/ifDec16.c
+569
-139
src/map/if/ifMan.c
+9
-2
src/map/if/ifMap.c
+14
-9
No files found.
src/base/abci/abc.c
View file @
e6e6a3cf
...
...
@@ -903,8 +903,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
}
*/
{
//
extern void If_CluTest();
//
If_CluTest();
extern
void
If_CluTest
();
If_CluTest
();
}
}
...
...
@@ -13252,7 +13252,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars
->
fCutMin
=
1
;
}
if
(
pPars
->
fEnableCheck07
+
pPars
->
fEnableCheck08
+
pPars
->
fEnableCheck10
>
1
)
if
(
pPars
->
fEnableCheck07
+
pPars
->
fEnableCheck08
+
pPars
->
fEnableCheck10
+
(
pPars
->
pLutStruct
!=
NULL
)
>
1
)
{
Abc_Print
(
-
1
,
"Only one additional check can be performed at the same time.
\n
"
);
return
1
;
...
...
@@ -13287,6 +13287,16 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars
->
pFuncCell
=
If_CutPerformCheck10
;
pPars
->
fCutMin
=
1
;
}
if
(
pPars
->
pLutStruct
)
{
if
(
pPars
->
nLutSize
<
6
||
pPars
->
nLutSize
>
11
)
{
Abc_Print
(
-
1
,
"This feature only works for {6,7,8,9,10,11}-LUTs.
\n
"
);
return
1
;
}
pPars
->
pFuncCell
=
If_CutPerformCheck16
;
pPars
->
fCutMin
=
1
;
}
// enable truth table computation if cut minimization is selected
if
(
pPars
->
fCutMin
)
...
...
@@ -13303,7 +13313,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars
->
fUsePerm
=
1
;
pPars
->
pLutLib
=
NULL
;
}
/*
// modify for LUT structures
if ( pPars->pLutStruct )
{
...
...
@@ -13317,7 +13327,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fUsePerm = 1;
pPars->pLutLib = NULL;
}
*/
// complain if truth tables are requested but the cut size is too large
if
(
pPars
->
fTruth
&&
pPars
->
nLutSize
>
IF_MAX_FUNC_LUTSIZE
)
{
...
...
src/map/if/if.h
View file @
e6e6a3cf
...
...
@@ -121,7 +121,7 @@ struct If_Par_t_
float
*
pTimesReq
;
// required times
int
(
*
pFuncCost
)
(
If_Cut_t
*
);
// procedure to compute the user's cost of a cut
int
(
*
pFuncUser
)
(
If_Man_t
*
,
If_Obj_t
*
,
If_Cut_t
*
);
// procedure called for each cut when cut computation is finished
int
(
*
pFuncCell
)
(
unsigned
*
,
int
,
int
);
// procedure called for cut functions
int
(
*
pFuncCell
)
(
unsigned
*
,
int
,
int
,
char
*
);
// procedure called for cut functions
void
*
pReoMan
;
// reordering manager
};
...
...
@@ -184,7 +184,10 @@ struct If_Man_t_
If_Set_t
*
pFreeList
;
// the list of free cutsets
int
nSmallSupp
;
// the small support
int
nCutsTotal
;
int
nCutsUseless
;
int
nCutsUseless
[
32
];
int
nCutsCount
[
32
];
int
nCutsCountAll
;
int
nCutsUselessAll
;
// timing manager
Tim_Man_t
*
pManTim
;
Vec_Int_t
*
vCoAttrs
;
// CO attributes 0=optimize; 1=keep; 2=relax
...
...
@@ -413,9 +416,10 @@ extern float If_CutPowerRef( If_Man_t * p, If_Cut_t * pCut, If_Obj_t *
extern
float
If_CutPowerDerefed
(
If_Man_t
*
p
,
If_Cut_t
*
pCut
,
If_Obj_t
*
pRoot
);
extern
float
If_CutPowerRefed
(
If_Man_t
*
p
,
If_Cut_t
*
pCut
,
If_Obj_t
*
pRoot
);
/*=== ifDec.c =============================================================*/
extern
int
If_CutPerformCheck07
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
);
extern
int
If_CutPerformCheck08
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
);
extern
int
If_CutPerformCheck10
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
);
extern
int
If_CutPerformCheck07
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
);
extern
int
If_CutPerformCheck08
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
);
extern
int
If_CutPerformCheck10
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
);
extern
int
If_CutPerformCheck16
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
);
extern
float
If_CutDelayLutStruct
(
If_Man_t
*
p
,
If_Cut_t
*
pCut
,
char
*
pStr
,
float
WireDelay
);
/*=== ifLib.c =============================================================*/
extern
If_Lib_t
*
If_LutLibRead
(
char
*
FileName
);
...
...
src/map/if/ifCut.c
View file @
e6e6a3cf
...
...
@@ -685,7 +685,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
return
;
}
if
(
(
p
->
pPars
->
fUseBat
||
p
->
pPars
->
fEnableCheck07
||
p
->
pPars
->
fEnableCheck08
||
p
->
pPars
->
fEnableCheck10
)
&&
!
pCut
->
fUseless
)
if
(
(
p
->
pPars
->
fUseBat
||
p
->
pPars
->
fEnableCheck07
||
p
->
pPars
->
fEnableCheck08
||
p
->
pPars
->
fEnableCheck10
||
p
->
pPars
->
pLutStruct
)
&&
!
pCut
->
fUseless
)
{
If_Cut_t
*
pFirst
=
pCutSet
->
ppCuts
[
0
];
if
(
pFirst
->
fUseless
||
If_ManSortCompare
(
p
,
pFirst
,
pCut
)
==
1
)
...
...
src/map/if/ifDec07.c
View file @
e6e6a3cf
...
...
@@ -673,9 +673,9 @@ int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
SeeAlso []
***********************************************************************/
int
If_CutPerformCheck07
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
)
int
If_CutPerformCheck07
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
)
{
int
fDerive
=
1
;
int
fDerive
=
0
;
if
(
nLeaves
<
6
)
return
1
;
if
(
nLeaves
==
6
)
...
...
@@ -685,7 +685,10 @@ int If_CutPerformCheck07( unsigned * pTruth, int nVars, int nLeaves )
return
1
;
z
=
If_Dec6Perform
(
t
,
fDerive
);
if
(
fDerive
&&
z
)
{
// If_DecPrintConfig( z );
If_Dec6Verify
(
t
,
z
);
}
return
z
!=
0
;
}
if
(
nLeaves
==
7
)
...
...
@@ -698,8 +701,6 @@ int If_CutPerformCheck07( unsigned * pTruth, int nVars, int nLeaves )
z
=
If_Dec7Perform
(
t
,
fDerive
);
if
(
fDerive
&&
z
)
If_Dec7Verify
(
t
,
z
);
return
z
!=
0
;
}
assert
(
0
);
...
...
src/map/if/ifDec08.c
View file @
e6e6a3cf
...
...
@@ -478,7 +478,7 @@ printf( "\n" );
SeeAlso []
***********************************************************************/
int
If_CutPerformCheck08
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
)
int
If_CutPerformCheck08
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
)
{
int
nSupp
,
fDerive
=
0
;
word
z
[
2
]
=
{
0
},
pF
[
16
];
...
...
src/map/if/ifDec10.c
View file @
e6e6a3cf
...
...
@@ -477,7 +477,7 @@ printf( "\n" );
SeeAlso []
***********************************************************************/
int
If_CutPerformCheck10
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
)
int
If_CutPerformCheck10
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
)
{
int
nSupp
,
fDerive
=
0
;
word
z
[
2
]
=
{
0
},
pF
[
16
];
...
...
src/map/if/ifDec16.c
View file @
e6e6a3cf
/**CFile****************************************************************
FileName [ifDec1
0f
.c]
FileName [ifDec1
6
.c]
SystemName [ABC: Logic synthesis and verification system.]
...
...
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifDec1
0f
.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
Revision [$Id: ifDec1
6
.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
...
...
@@ -36,7 +36,7 @@ struct If_Grp_t_
{
char
nVars
;
char
nMyu
;
char
pVars
[
6
];
char
pVars
[
CLU_VAR_MAX
];
};
// the bit count for the first 256 integer numbers
...
...
@@ -67,36 +67,33 @@ static word Truth6[6] = {
0xFFFF0000FFFF0000
,
0xFFFFFFFF00000000
};
static
word
TruthAll
[
CLU_VAR_MAX
][
CLU_WRD_MAX
];
static
word
TruthAll
[
CLU_VAR_MAX
][
CLU_WRD_MAX
]
=
{{
0
}}
;
extern
void
Kit_DsdPrintFromTruth
(
unsigned
*
pTruth
,
int
nVars
);
extern
void
Extra_PrintBinary
(
FILE
*
pFile
,
unsigned
Sign
[],
int
nBits
);
// group representation (MSB <-> LSB)
// nVars | nMyu | v5 | v4 | v3 | v2 | v1 | v0
// if nCofs > 2, v0 is the shared variable
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
void
If_CluInitTruthTables
()
{
int
i
,
k
;
assert
(
CLU_VAR_MAX
<=
16
);
for
(
i
=
0
;
i
<
6
;
i
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
TruthAll
[
i
][
k
]
=
Truth6
[
i
];
for
(
i
=
6
;
i
<
CLU_VAR_MAX
;
i
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
TruthAll
[
i
][
k
]
=
((
k
>>
i
)
&
1
)
?
~
0
:
0
;
}
// variable permutation for large functions
static
inline
int
If_CluWordNum
(
int
nVars
)
{
return
nVars
<=
6
?
1
:
1
<<
(
nVars
-
6
);
}
static
inline
void
If_CluClear
(
word
*
pIn
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pIn
[
w
]
=
0
;
}
static
inline
void
If_CluFill
(
word
*
pIn
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pIn
[
w
]
=
~
0
;
}
static
inline
void
If_CluCopy
(
word
*
pOut
,
word
*
pIn
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
...
...
@@ -111,6 +108,42 @@ static inline int If_CluEqual( word * pOut, word * pIn, int nVars )
return
0
;
return
1
;
}
static
inline
void
If_CluAnd
(
word
*
pRes
,
word
*
pIn1
,
word
*
pIn2
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pRes
[
w
]
=
pIn1
[
w
]
&
pIn2
[
w
];
}
static
inline
void
If_CluSharp
(
word
*
pRes
,
word
*
pIn1
,
word
*
pIn2
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pRes
[
w
]
=
pIn1
[
w
]
&
~
pIn2
[
w
];
}
static
inline
void
If_CluOr
(
word
*
pRes
,
word
*
pIn1
,
word
*
pIn2
,
int
nVars
)
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pRes
[
w
]
=
pIn1
[
w
]
|
pIn2
[
w
];
}
static
inline
word
If_CluAdjust
(
word
t
,
int
nVars
)
{
assert
(
nVars
>=
0
&&
nVars
<
6
);
t
&=
(
1
<<
(
1
<<
nVars
))
-
1
;
if
(
nVars
==
0
)
t
|=
t
<<
(
1
<<
nVars
++
);
if
(
nVars
==
1
)
t
|=
t
<<
(
1
<<
nVars
++
);
if
(
nVars
==
2
)
t
|=
t
<<
(
1
<<
nVars
++
);
if
(
nVars
==
3
)
t
|=
t
<<
(
1
<<
nVars
++
);
if
(
nVars
==
4
)
t
|=
t
<<
(
1
<<
nVars
++
);
if
(
nVars
==
5
)
t
|=
t
<<
(
1
<<
nVars
++
);
return
t
;
}
static
inline
void
If_CluSwapAdjacent
(
word
*
pOut
,
word
*
pIn
,
int
iVar
,
int
nVars
)
{
int
i
,
k
,
nWords
=
If_CluWordNum
(
nVars
);
...
...
@@ -148,14 +181,107 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV
}
}
void
If_CluPrintGroup
(
If_Grp_t
*
g
)
{
int
i
;
printf
(
"Vars = %d "
,
g
->
nVars
);
printf
(
"Myu = %d "
,
g
->
nMyu
);
for
(
i
=
0
;
i
<
g
->
nVars
;
i
++
)
printf
(
"%d "
,
g
->
pVars
[
i
]
);
printf
(
"
\n
"
);
}
void
If_CluPrintConfig
(
int
nVars
,
If_Grp_t
*
g
,
If_Grp_t
*
r
,
word
BStruth
,
word
*
pFStruth
)
{
assert
(
r
->
nVars
==
nVars
-
g
->
nVars
+
1
+
(
g
->
nMyu
>
2
)
);
If_CluPrintGroup
(
g
);
if
(
g
->
nVars
<
6
)
BStruth
=
If_CluAdjust
(
BStruth
,
g
->
nVars
);
Kit_DsdPrintFromTruth
(
(
unsigned
*
)
&
BStruth
,
g
->
nVars
);
printf
(
"
\n
"
);
If_CluPrintGroup
(
r
);
if
(
r
->
nVars
<
6
)
pFStruth
[
0
]
=
If_CluAdjust
(
pFStruth
[
0
],
r
->
nVars
);
Kit_DsdPrintFromTruth
(
(
unsigned
*
)
pFStruth
,
r
->
nVars
);
printf
(
"
\n
"
);
}
void
If_CluInitTruthTables
()
{
int
i
,
k
;
assert
(
CLU_VAR_MAX
<=
16
);
for
(
i
=
0
;
i
<
6
;
i
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
TruthAll
[
i
][
k
]
=
Truth6
[
i
];
for
(
i
=
6
;
i
<
CLU_VAR_MAX
;
i
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
TruthAll
[
i
][
k
]
=
((
k
>>
(
i
-
6
))
&
1
)
?
~
0
:
0
;
// Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" );
// Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" );
}
// verification
static
void
If_CluComposeLut
(
int
nVars
,
If_Grp_t
*
g
,
word
*
t
,
word
f
[
6
][
CLU_WRD_MAX
],
word
*
r
)
{
word
c
[
CLU_WRD_MAX
];
int
m
,
v
;
If_CluClear
(
r
,
nVars
);
for
(
m
=
0
;
m
<
(
1
<<
g
->
nVars
);
m
++
)
{
if
(
!
((
t
[
m
>>
6
]
>>
(
m
&
63
))
&
1
)
)
continue
;
If_CluFill
(
c
,
nVars
);
for
(
v
=
0
;
v
<
g
->
nVars
;
v
++
)
if
(
(
m
>>
v
)
&
1
)
If_CluAnd
(
c
,
c
,
f
[
v
],
nVars
);
else
If_CluSharp
(
c
,
c
,
f
[
v
],
nVars
);
If_CluOr
(
r
,
r
,
c
,
nVars
);
}
}
void
If_CluVerify
(
word
*
pF
,
int
nVars
,
If_Grp_t
*
g
,
If_Grp_t
*
r
,
word
BStruth
,
word
*
pFStruth
)
{
word
pTTFans
[
6
][
CLU_WRD_MAX
],
pTTWire
[
CLU_WRD_MAX
],
pTTRes
[
CLU_WRD_MAX
];
int
i
;
assert
(
g
->
nVars
<=
6
&&
r
->
nVars
<=
6
);
if
(
TruthAll
[
0
][
0
]
==
0
)
If_CluInitTruthTables
();
for
(
i
=
0
;
i
<
g
->
nVars
;
i
++
)
If_CluCopy
(
pTTFans
[
i
],
TruthAll
[
g
->
pVars
[
i
]],
nVars
);
If_CluComposeLut
(
nVars
,
g
,
&
BStruth
,
pTTFans
,
pTTWire
);
for
(
i
=
0
;
i
<
r
->
nVars
;
i
++
)
if
(
r
->
pVars
[
i
]
==
nVars
)
If_CluCopy
(
pTTFans
[
i
],
pTTWire
,
nVars
);
else
If_CluCopy
(
pTTFans
[
i
],
TruthAll
[
r
->
pVars
[
i
]],
nVars
);
If_CluComposeLut
(
nVars
,
r
,
pFStruth
,
pTTFans
,
pTTRes
);
if
(
!
If_CluEqual
(
pTTRes
,
pF
,
nVars
)
)
{
printf
(
"
\n
"
);
If_CluPrintConfig
(
nVars
,
g
,
r
,
BStruth
,
pFStruth
);
Kit_DsdPrintFromTruth
(
(
unsigned
*
)
pTTRes
,
nVars
);
printf
(
"
\n
"
);
Kit_DsdPrintFromTruth
(
(
unsigned
*
)
pF
,
nVars
);
printf
(
"
\n
"
);
// Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( "\n" );
printf
(
"Verification FAILED!
\n
"
);
}
// else
// printf( "Verification succeed!\n" );
}
// moves one var (v) to the given position (p)
void
If_CluMoveVar
(
word
*
pF
,
int
nVars
,
int
*
Var2Pla
,
int
*
Pla2Var
,
int
v
,
int
p
)
{
word
pG
[
CLU_WRD_MAX
],
*
pIn
=
pF
,
*
pOut
=
pG
,
*
pTemp
;
int
iPlace0
,
iPlace1
,
Count
=
0
;
assert
(
v
>=
0
&&
v
<
nVars
);
if
(
Var2Pla
[
v
]
<=
p
)
{
while
(
Var2Pla
[
v
]
<
p
)
{
iPlace0
=
Var2Pla
[
v
];
...
...
@@ -169,9 +295,6 @@ void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, i
Pla2Var
[
iPlace0
]
^=
Pla2Var
[
iPlace1
];
Count
++
;
}
}
else
{
while
(
Var2Pla
[
v
]
>
p
)
{
iPlace0
=
Var2Pla
[
v
]
-
1
;
...
...
@@ -185,7 +308,6 @@ void If_CluMoveVar( word * pF, int nVars, int * Var2Pla, int * Pla2Var, int v, i
Pla2Var
[
iPlace0
]
^=
Pla2Var
[
iPlace1
];
Count
++
;
}
}
if
(
Count
&
1
)
If_CluCopy
(
pF
,
pIn
,
nVars
);
assert
(
Pla2Var
[
p
]
==
v
);
...
...
@@ -199,64 +321,86 @@ void If_CluMoveGroupToMsb( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t
If_CluMoveVar
(
pF
,
nVars
,
V2P
,
P2V
,
g
->
pVars
[
g
->
nVars
-
1
-
v
],
nVars
-
1
-
v
);
}
// re
turn the number of cofactors w.r.t. the topmost vars (nBSsize)
int
If_CluCountCofs
(
word
*
pF
,
int
nVars
,
int
nBSsize
,
int
iShift
,
word
*
pCofs
[
2
]
)
// re
verses the variable order
void
If_CluReverseOrder
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
)
{
word
iCofs
[
64
],
iCof
;
int
i
,
c
,
w
,
nMints
=
(
1
<<
nBSsize
),
nCofs
;
assert
(
nBSsize
<
nVars
);
assert
(
nBSsize
>=
3
&&
nBSsize
<=
6
);
int
v
;
for
(
v
=
0
;
v
<
nVars
;
v
++
)
If_CluMoveVar
(
pF
,
nVars
,
V2P
,
P2V
,
P2V
[
0
],
nVars
-
1
-
v
);
}
if
(
nVars
-
nBSsize
>=
6
)
{
// return the number of cofactors w.r.t. the topmost vars (nBSsize)
int
If_CluCountCofs
(
word
*
pF
,
int
nVars
,
int
nBSsize
,
int
iShift
,
word
pCofs
[
3
][
CLU_WRD_MAX
/
4
]
)
{
word
iCofs
[
128
],
iCof
,
Result
=
0
;
word
*
pCofA
,
*
pCofB
;
int
nWords
=
(
1
<<
(
nVars
-
nBSsize
-
6
));
assert
(
nWords
*
nMints
==
If_CluWordNum
(
nVars
)
);
int
nMints
=
(
1
<<
nBSsize
);
int
i
,
c
,
w
,
nCofs
;
assert
(
nBSsize
>=
2
&&
nBSsize
<=
7
&&
nBSsize
<
nVars
);
if
(
nVars
-
nBSsize
<
6
)
{
int
nShift
=
(
1
<<
(
nVars
-
nBSsize
));
word
Mask
=
((((
word
)
1
)
<<
nShift
)
-
1
);
for
(
nCofs
=
i
=
0
;
i
<
nMints
;
i
++
)
{
iCof
=
(
pF
[(
iShift
+
i
*
nShift
)
/
64
]
>>
((
iShift
+
i
*
nShift
)
&
63
))
&
Mask
;
for
(
c
=
0
;
c
<
nCofs
;
c
++
)
{
pCofA
=
pF
+
i
*
nWords
;
pCofB
=
pF
+
iCofs
[
c
]
*
nWords
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
pCofA
[
w
]
!=
pCofB
[
w
]
)
break
;
if
(
w
==
nWords
)
if
(
iCof
==
iCofs
[
c
]
)
break
;
}
if
(
c
==
nCofs
)
iCofs
[
nCofs
++
]
=
i
;
iCofs
[
nCofs
++
]
=
iCof
;
if
(
pCofs
&&
iCof
!=
iCofs
[
0
]
)
Result
|=
(((
word
)
1
)
<<
i
);
if
(
nCofs
==
5
)
break
;
}
if
(
nCofs
==
2
&&
pCofs
)
{
for
(
c
=
0
;
c
<
nCofs
;
c
++
)
if
(
nCofs
<=
2
&&
pCofs
)
{
word
*
pCofA
=
pF
+
iCofs
[
c
]
*
nWords
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pCofs
[
c
][
w
]
=
pCofA
[
w
];
}
assert
(
nBSsize
<=
6
)
;
pCofs
[
0
][
0
]
=
iCofs
[
0
];
pCofs
[
1
][
0
]
=
(
nCofs
==
2
)
?
iCofs
[
1
]
:
iCofs
[
0
];
pCofs
[
2
][
0
]
=
Result
;
}
}
else
{
int
n
Shift
=
(
1
<<
(
nVars
-
nBSsize
)
);
word
Mask
=
((((
word
)
1
)
<<
nShift
)
-
1
);
int
n
Words
=
If_CluWordNum
(
nVars
-
nBSsize
);
assert
(
nWords
*
nMints
==
If_CluWordNum
(
nVars
)
);
for
(
nCofs
=
i
=
0
;
i
<
nMints
;
i
++
)
{
iCof
=
(
pF
[(
iShift
+
i
*
nShift
)
/
64
]
>>
((
iShift
+
i
*
nShift
)
&
63
))
&
Mask
;
pCofA
=
pF
+
i
*
nWords
;
for
(
c
=
0
;
c
<
nCofs
;
c
++
)
if
(
iCof
==
iCofs
[
c
]
)
{
pCofB
=
pF
+
iCofs
[
c
]
*
nWords
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
pCofA
[
w
]
!=
pCofB
[
w
]
)
break
;
if
(
w
==
nWords
)
break
;
}
if
(
c
==
nCofs
)
iCofs
[
nCofs
++
]
=
iCof
;
iCofs
[
nCofs
++
]
=
i
;
if
(
pCofs
)
{
assert
(
nBSsize
<=
6
);
pCofB
=
pF
+
iCofs
[
0
]
*
nWords
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
pCofA
[
w
]
!=
pCofB
[
w
]
)
break
;
if
(
w
!=
nWords
)
Result
|=
(((
word
)
1
)
<<
i
);
}
if
(
nCofs
==
5
)
break
;
}
if
(
nCofs
<=
2
&&
pCofs
)
{
If_CluCopy
(
pCofs
[
0
],
pF
+
iCofs
[
0
]
*
nWords
,
nVars
-
nBSsize
);
If_CluCopy
(
pCofs
[
1
],
pF
+
((
nCofs
==
2
)
?
iCofs
[
1
]
:
iCofs
[
0
])
*
nWords
,
nVars
-
nBSsize
);
pCofs
[
2
][
0
]
=
Result
;
}
assert
(
nCofs
>=
2
&&
nCofs
<=
5
);
}
assert
(
nCofs
>=
1
&&
nCofs
<=
5
);
return
nCofs
;
}
...
...
@@ -272,7 +416,6 @@ void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1
pCof0
[
i
]
=
(
pF
[
i
]
&
~
Truth6
[
iVar
])
|
((
pF
[
i
]
&
~
Truth6
[
iVar
])
<<
Shift
);
pCof1
[
i
]
=
(
pF
[
i
]
&
Truth6
[
iVar
])
|
((
pF
[
i
]
&
Truth6
[
iVar
])
>>
Shift
);
}
return
;
}
else
{
...
...
@@ -288,70 +431,227 @@ void If_CluCofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1
pCof0
+=
2
*
Step
;
pCof1
+=
2
*
Step
;
}
return
;
}
}
//
derives non-disjoint decomposition (assumes the shared var in pG->pVars[pG->nVars-1]
word
If_CluDeriveNonDisjoint
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
,
If_Grp_t
*
g
,
If_Grp_t
*
pG
)
//
returns 1 if we have special case of cofactors; otherwise, returns 0
int
If_CluDetectSpecialCaseCofs
(
word
*
pF
,
int
nVars
,
int
iVar
)
{
/*
word Truth, Truth0, Truth1;
word Cof[2][CLU_WRD_MAX], Cof0[2][CLU_WRD_MAX], Cof1[2][CLU_WRD_MAX];
int i, nFSvars, nFSHalfBits, nBSHalfBits;
assert( pG->nVars >= 3 && pG->nVar <= 6 );
assert( pG->nMyu == 3 || pG->nMyu == 4 );
If_CluMoveGroupToMsb( pF, nVars, V2P, P2V, pG );
If_CluCofactors( pF, nVars, nVars - 1, Cof[0], Cof[1] );
assert( 2 >= If_Dec6CofCount2(c0) );
assert( 2 >= If_Dec6CofCount2(c1) );
assert( 2 >= If_CluCountCofs( Cof[0], nVars - 1, pG->nVars - 1, 0 ) );
assert( 2 >= If_CluCountCofs( Cof[1], nVars - 1, pG->nVars - 1, 0 ) );
word
Cof0
,
Cof1
;
int
State
[
6
]
=
{
0
};
int
i
,
nWords
=
If_CluWordNum
(
nVars
);
assert
(
iVar
<
nVars
);
if
(
iVar
<
6
)
{
int
Shift
=
(
1
<<
iVar
);
for
(
i
=
0
;
i
<
nWords
;
i
++
)
{
Cof0
=
(
pF
[
i
]
&
~
Truth6
[
iVar
]);
Cof1
=
((
pF
[
i
]
&
Truth6
[
iVar
])
>>
Shift
);
if
(
Cof0
==
0
)
State
[
0
]
++
;
else
if
(
Cof0
==
~
Truth6
[
iVar
]
)
State
[
1
]
++
;
else
if
(
Cof1
==
0
)
State
[
2
]
++
;
else
if
(
Cof1
==
~
Truth6
[
iVar
]
)
State
[
3
]
++
;
else
if
(
Cof0
==
~
Cof1
)
State
[
4
]
++
;
else
if
(
Cof0
==
Cof1
)
State
[
5
]
++
;
}
}
else
{
int
k
,
Step
=
(
1
<<
(
iVar
-
6
));
for
(
k
=
0
;
k
<
nWords
;
k
+=
2
*
Step
)
{
for
(
i
=
0
;
i
<
Step
;
i
++
)
{
Cof0
=
pF
[
i
];
Cof1
=
pF
[
Step
+
i
];
if
(
Cof0
==
0
)
State
[
0
]
++
;
else
if
(
Cof0
==
~
Truth6
[
iVar
]
)
State
[
1
]
++
;
else
if
(
Cof1
==
0
)
State
[
2
]
++
;
else
if
(
Cof1
==
~
Truth6
[
iVar
]
)
State
[
3
]
++
;
else
if
(
Cof0
==
~
Cof1
)
State
[
4
]
++
;
else
if
(
Cof0
==
Cof1
)
State
[
5
]
++
;
}
pF
+=
2
*
Step
;
}
nWords
/=
2
;
}
assert
(
State
[
5
]
!=
nWords
);
for
(
i
=
0
;
i
<
5
;
i
++
)
{
assert
(
State
[
i
]
<=
nWords
);
if
(
State
[
i
]
==
nWords
)
return
i
;
}
return
-
1
;
}
Truth0 = If_CluExtract2Cofs( Cof[0], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] );
Truth1 = If_CluExtract2Cofs( Cof[1], nVars - 1, pG->nVars - 1, &Cof0[0], &Cof0[1] );
// returns 1 if we have special case of cofactors; otherwise, returns 0
If_Grp_t
If_CluDecUsingCofs
(
word
*
pTruth
,
int
nVars
,
int
nLutLeaf
)
{
If_Grp_t
G
=
{
0
};
word
pF2
[
CLU_WRD_MAX
],
*
pF
=
pF2
;
int
Var2Pla
[
CLU_VAR_MAX
+
2
],
Pla2Var
[
CLU_VAR_MAX
+
2
];
int
V2P
[
CLU_VAR_MAX
+
2
],
P2V
[
CLU_VAR_MAX
+
2
];
int
nVarsNeeded
=
nVars
-
nLutLeaf
;
int
v
,
i
,
k
,
iVar
,
State
;
//Kit_DsdPrintFromTruth( (unsigned*)pTruth, nVars ); printf( "\n" );
// create local copy
If_CluCopy
(
pF
,
pTruth
,
nVars
);
for
(
k
=
0
;
k
<
nVars
;
k
++
)
Var2Pla
[
k
]
=
Pla2Var
[
k
]
=
k
;
// find decomposable vars
for
(
i
=
0
;
i
<
nVarsNeeded
;
i
++
)
{
for
(
v
=
nVars
-
1
;
v
>=
0
;
v
--
)
{
State
=
If_CluDetectSpecialCaseCofs
(
pF
,
nVars
,
v
);
if
(
State
==
-
1
)
continue
;
// update the variable place
iVar
=
Pla2Var
[
v
];
while
(
Var2Pla
[
iVar
]
<
nVars
-
1
)
{
int
iPlace0
=
Var2Pla
[
iVar
];
int
iPlace1
=
Var2Pla
[
iVar
]
+
1
;
Var2Pla
[
Pla2Var
[
iPlace0
]]
++
;
Var2Pla
[
Pla2Var
[
iPlace1
]]
--
;
Pla2Var
[
iPlace0
]
^=
Pla2Var
[
iPlace1
];
Pla2Var
[
iPlace1
]
^=
Pla2Var
[
iPlace0
];
Pla2Var
[
iPlace0
]
^=
Pla2Var
[
iPlace1
];
}
// move this variable to the top
for
(
k
=
0
;
k
<
nVars
;
k
++
)
V2P
[
k
]
=
P2V
[
k
]
=
k
;
//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
If_CluMoveVar
(
pF
,
nVars
,
V2P
,
P2V
,
v
,
nVars
-
1
);
//Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
// choose cofactor to follow
iVar
=
nVars
-
1
;
if
(
State
==
0
||
State
==
1
)
// need cof1
{
if
(
iVar
<
6
)
pF
[
0
]
=
(
pF
[
0
]
&
Truth6
[
iVar
])
|
((
pF
[
0
]
&
Truth6
[
iVar
])
>>
(
1
<<
iVar
));
else
pF
+=
If_CluWordNum
(
nVars
)
/
2
;
}
else
// need cof0
{
if
(
iVar
<
6
)
pF
[
0
]
=
(
pF
[
0
]
&
~
Truth6
[
iVar
])
|
((
pF
[
0
]
&
~
Truth6
[
iVar
])
<<
(
1
<<
iVar
));
}
// update the variable count
nVars
--
;
break
;
}
if
(
v
==
-
1
)
return
G
;
}
// create the resulting group
G
.
nVars
=
nLutLeaf
;
G
.
nMyu
=
2
;
for
(
v
=
0
;
v
<
G
.
nVars
;
v
++
)
G
.
pVars
[
v
]
=
Pla2Var
[
v
];
return
G
;
}
nFSHalfBits = (1 << (nVars - pG->nVars - 1));
nBSHalfBits = (1 << (pG->nVars - 1))
Truth = ((Truth0 && ((1 << nBSHalfBits) - 1)) << nBSHalfBits) | (Truth0 && ((1 << nBSHalfBits) - 1))
// deriving decomposition
word
If_CluDeriveDisjoint
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
,
If_Grp_t
*
g
,
If_Grp_t
*
r
)
{
word
pCofs
[
3
][
CLU_WRD_MAX
/
4
];
int
i
,
RetValue
,
nFSset
=
nVars
-
g
->
nVars
;
RetValue
=
If_CluCountCofs
(
pF
,
nVars
,
g
->
nVars
,
0
,
pCofs
);
// assert( RetValue == 2 );
for ( i = 0; i < 4; i++ )
z |= (((word)Pla2Var[i+2]) << (16 + 4*i));
z |= ((word)((Cof0[1] << 4) | Cof0[0]) << 32);
z |= ((word)((Cof1[1] << 4) | Cof1[0]) << 40);
for ( i = 0; i < 2; i++ )
z |= (((word)Pla2Var[i]) << (48 + 4*i));
z |= (((word)7) << (48 + 4*i++));
z |= (((word)Pla2Var[5]) << (48 + 4*i++));
assert( i == 4 );
return z;
*/
return
0
;
if
(
nFSset
<
6
)
pF
[
0
]
=
(
pCofs
[
1
][
0
]
<<
(
1
<<
nFSset
))
|
pCofs
[
0
][
0
];
else
{
If_CluCopy
(
pF
,
pCofs
[
0
],
nFSset
);
If_CluCopy
(
pF
+
If_CluWordNum
(
nFSset
),
pCofs
[
1
],
nFSset
);
}
// create the resulting group
if
(
r
)
{
r
->
nVars
=
nFSset
+
1
;
r
->
nMyu
=
0
;
for
(
i
=
0
;
i
<
nFSset
;
i
++
)
r
->
pVars
[
i
]
=
P2V
[
i
];
r
->
pVars
[
nFSset
]
=
nVars
;
}
return
pCofs
[
2
][
0
];
}
word
If_CluDeriveNonDisjoint
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
,
If_Grp_t
*
g
,
If_Grp_t
*
r
)
{
word
pCofs
[
2
][
CLU_WRD_MAX
];
word
Truth0
,
Truth1
,
Truth
;
int
i
,
nFSset
=
nVars
-
g
->
nVars
,
nFSset1
=
nFSset
+
1
;
If_CluCofactors
(
pF
,
nVars
,
nVars
-
1
,
pCofs
[
0
],
pCofs
[
1
]
);
// Extra_PrintHex( stdout, (unsigned *)pCofs[0], nVars ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)pCofs[1], nVars ); printf( "\n" );
g
->
nVars
--
;
Truth0
=
If_CluDeriveDisjoint
(
pCofs
[
0
],
nVars
-
1
,
V2P
,
P2V
,
g
,
NULL
);
Truth1
=
If_CluDeriveDisjoint
(
pCofs
[
1
],
nVars
-
1
,
V2P
,
P2V
,
g
,
NULL
);
Truth
=
(
Truth1
<<
(
1
<<
g
->
nVars
))
|
Truth0
;
g
->
nVars
++
;
if
(
nFSset1
<
6
)
pF
[
0
]
=
(
pCofs
[
1
][
0
]
<<
(
1
<<
nFSset1
))
|
pCofs
[
0
][
0
];
else
{
If_CluCopy
(
pF
,
pCofs
[
0
],
nFSset1
);
If_CluCopy
(
pF
+
If_CluWordNum
(
nFSset1
),
pCofs
[
1
],
nFSset1
);
}
// Extra_PrintHex( stdout, (unsigned *)&Truth0, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&Truth1, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pCofs[0][0], 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pCofs[1][0], 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&Truth, 6 ); printf( "\n" );
// Extra_PrintHex( stdout, (unsigned *)&pF[0], 6 ); printf( "\n" );
// create the resulting group
r
->
nVars
=
nFSset
+
2
;
r
->
nMyu
=
0
;
for
(
i
=
0
;
i
<
nFSset
;
i
++
)
r
->
pVars
[
i
]
=
P2V
[
i
];
r
->
pVars
[
nFSset
]
=
nVars
;
r
->
pVars
[
nFSset
+
1
]
=
g
->
pVars
[
g
->
nVars
-
1
];
return
Truth
;
}
// check non-disjoint decomposition
int
If_CluCheckNonDisjoint
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
,
If_Grp_t
*
g
)
int
If_CluCheckNonDisjoint
Group
(
word
*
pF
,
int
nVars
,
int
*
V2P
,
int
*
P2V
,
If_Grp_t
*
g
)
{
int
v
,
i
,
nCofsBest2
;
if
(
(
g
->
nMyu
==
3
||
g
->
nMyu
==
4
)
)
{
word
pCof0
[
CLU_WRD_MAX
];
word
pCof1
[
CLU_WRD_MAX
];
word
pCofs
[
2
][
CLU_WRD_MAX
];
// try cofactoring w.r.t. each variable
for
(
v
=
0
;
v
<
g
->
nVars
;
v
++
)
{
If_CluCofactors
(
pF
,
nVars
,
V2P
[
g
->
pVars
[
v
]],
pCof
0
,
pCof1
);
nCofsBest2
=
If_CluCountCofs
(
pCof
0
,
nVars
,
g
->
nVars
,
0
,
NULL
);
If_CluCofactors
(
pF
,
nVars
,
V2P
[
g
->
pVars
[
v
]],
pCof
s
[
0
],
pCofs
[
1
]
);
nCofsBest2
=
If_CluCountCofs
(
pCof
s
[
0
]
,
nVars
,
g
->
nVars
,
0
,
NULL
);
if
(
nCofsBest2
>
2
)
continue
;
nCofsBest2
=
If_CluCountCofs
(
pCof
1
,
nVars
,
g
->
nVars
,
0
,
NULL
);
nCofsBest2
=
If_CluCountCofs
(
pCof
s
[
1
]
,
nVars
,
g
->
nVars
,
0
,
NULL
);
if
(
nCofsBest2
>
2
)
continue
;
// found good shared variable - move to the end
...
...
@@ -364,25 +664,15 @@ int If_CluCheckNonDisjoint( word * pF, int nVars, int * V2P, int * P2V, If_Grp_t
return
0
;
}
void
If_CluPrintGroup
(
If_Grp_t
*
g
)
{
int
i
;
for
(
i
=
0
;
i
<
g
->
nVars
;
i
++
)
printf
(
"%d "
,
g
->
pVars
[
i
]
);
printf
(
"
\n
"
);
printf
(
"Cofs = %d"
,
g
->
nMyu
);
printf
(
"
\n
"
);
printf
(
"Vars = %d"
,
g
->
nVars
);
printf
(
"
\n
"
);
}
// finds a good var group (cof count < 6; vars are MSBs)
If_Grp_t
If_CluFindGroup
(
word
*
pF
,
int
nVars
,
int
iVarStart
,
int
*
V2P
,
int
*
P2V
,
int
nBSsize
,
int
fDisjoint
)
{
int
fVerbose
=
0
;
int
nRounds
=
2
;
//nBSsize;
If_Grp_t
G
=
{
0
},
*
g
=
&
G
;
int
i
,
r
,
v
,
nCofs
,
VarBest
,
nCofsBest2
;
assert
(
nVars
>=
nBSsize
+
iVarStart
&&
nVars
<=
CLU_VAR_MAX
);
assert
(
nVars
>
nBSsize
&&
nVars
>
=
nBSsize
+
iVarStart
&&
nVars
<=
CLU_VAR_MAX
);
assert
(
nBSsize
>=
3
&&
nBSsize
<=
6
);
// start with the default group
g
->
nVars
=
nBSsize
;
...
...
@@ -392,14 +682,19 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int *
// check if good enough
if
(
g
->
nMyu
==
2
)
return
G
;
if
(
If_CluCheckNonDisjoint
(
pF
,
nVars
,
V2P
,
P2V
,
g
)
)
if
(
!
fDisjoint
&&
If_CluCheckNonDisjointGroup
(
pF
,
nVars
,
V2P
,
P2V
,
g
)
)
return
G
;
printf
(
"Iter %d "
,
-
1
);
if
(
fVerbose
)
{
printf
(
"Iter %2d "
,
-
1
);
If_CluPrintGroup
(
g
);
}
// try to find better group
for
(
r
=
0
;
r
<
nBSsize
;
r
++
)
for
(
r
=
0
;
r
<
nRounds
;
r
++
)
{
if
(
nBSsize
<
nVars
-
1
)
{
// find the best var to add
VarBest
=
P2V
[
nVars
-
1
-
nBSsize
];
...
...
@@ -419,6 +714,7 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int *
// update best bound set
nCofs
=
If_CluCountCofs
(
pF
,
nVars
,
nBSsize
+
1
,
0
,
NULL
);
assert
(
nCofs
==
nCofsBest2
);
}
// find the best var to remove
VarBest
=
P2V
[
nVars
-
1
-
nBSsize
];
...
...
@@ -447,16 +743,20 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int *
g
->
pVars
[
i
]
=
P2V
[
nVars
-
nBSsize
+
i
];
}
printf
(
"Iter %d "
,
r
);
if
(
fVerbose
)
{
printf
(
"Iter %2d "
,
r
);
If_CluPrintGroup
(
g
);
}
// check if good enough
if
(
g
->
nMyu
==
2
)
return
G
;
if
(
If_CluCheckNonDisjoint
(
pF
,
nVars
,
V2P
,
P2V
,
g
)
)
if
(
!
fDisjoint
&&
If_CluCheckNonDisjointGroup
(
pF
,
nVars
,
V2P
,
P2V
,
g
)
)
return
G
;
}
assert
(
r
==
nBSsize
);
assert
(
r
==
nRounds
);
g
->
nVars
=
0
;
return
G
;
}
...
...
@@ -467,7 +767,7 @@ void If_CluCheckGroup( word * pTruth, int nVars, If_Grp_t * g )
{
word
pF
[
CLU_WRD_MAX
];
int
v
,
nCofs
,
V2P
[
CLU_VAR_MAX
],
P2V
[
CLU_VAR_MAX
];
assert
(
g
->
nVars
>=
3
&&
g
->
nVars
<=
6
);
// vars
assert
(
g
->
nVars
>=
2
&&
g
->
nVars
<=
6
);
// vars
assert
(
g
->
nMyu
>=
2
&&
g
->
nMyu
<=
4
);
// cofs
// create permutation
for
(
v
=
0
;
v
<
nVars
;
v
++
)
...
...
@@ -500,10 +800,10 @@ void If_CluCheckPerm( word * pTruth, word * pF, int nVars, int * V2P, int * P2V
for
(
i
=
0
;
i
<
nVars
;
i
++
)
If_CluMoveVar
(
pF
,
nVars
,
V2P
,
P2V
,
i
,
i
);
if
(
If_CluEqual
(
pTruth
,
pF
,
nVars
)
)
printf
(
"Permutation successful
\n
"
);
else
if
(
!
If_CluEqual
(
pTruth
,
pF
,
nVars
)
)
printf
(
"Permutation FAILED.
\n
"
);
// else
// printf( "Permutation successful\n" );
}
...
...
@@ -550,32 +850,92 @@ static inline int If_CluSupport( word * t, int nVars )
// returns the best group found
If_Grp_t
If_CluCheck
(
word
*
pTruth
,
int
nVars
,
int
nLutLeaf
,
int
nLutRoot
)
{
int
V2P
[
CLU_VAR_MAX
],
P2V
[
CLU_VAR_MAX
]
;
word
pF
[
CLU_WRD_MAX
];
If_Grp_t
G1
=
{
0
}
;
If_Grp_t
G1
=
{
0
},
R
=
{
0
}
;
word
Truth
,
pF
[
CLU_WRD_MAX
];
//, pG
[CLU_WRD_MAX];
int
V2P
[
CLU_VAR_MAX
+
2
],
P2V
[
CLU_VAR_MAX
+
2
]
;
int
i
,
nSupp
;
assert
(
nVars
<=
CLU_VAR_MAX
);
assert
(
nVars
<=
nLutLeaf
+
nLutRoot
-
1
);
/*
{
int pCanonPerm[32];
short pStore[32];
unsigned uCanonPhase;
If_CluCopy( pF, pTruth, nVars );
uCanonPhase = Kit_TruthSemiCanonicize( pF, pG, nVars, pCanonPerm, pStore );
G1.nVars = 1;
return G1;
}
*/
// check minnimum base
If_CluCopy
(
pF
,
pTruth
,
nVars
);
for
(
i
=
0
;
i
<
nVars
;
i
++
)
V2P
[
i
]
=
P2V
[
i
]
=
i
;
// check support
nSupp
=
If_CluSupport
(
pF
,
nVars
);
//Extra_PrintBinary( stdout, &nSupp, 16 ); printf( "\n" );
if
(
!
nSupp
||
!
If_CluSuppIsMinBase
(
nSupp
)
)
return
G1
;
// detect easy cofs
G1
=
If_CluDecUsingCofs
(
pTruth
,
nVars
,
nLutLeaf
);
if
(
G1
.
nVars
==
0
)
{
// perform testing
for
(
i
=
0
;
i
<
nVars
;
i
++
)
V2P
[
i
]
=
P2V
[
i
]
=
i
;
G1
=
If_CluFindGroup
(
pF
,
nVars
,
0
,
V2P
,
P2V
,
nLutLeaf
,
nLutLeaf
+
nLutRoot
==
nVars
+
1
);
// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
if
(
G1
.
nVars
==
0
)
{
// perform testing with a smaller set
if
(
nVars
<
nLutLeaf
+
nLutRoot
-
2
)
{
nLutLeaf
--
;
G1
=
If_CluFindGroup
(
pF
,
nVars
,
0
,
V2P
,
P2V
,
nLutLeaf
,
nLutLeaf
+
nLutRoot
==
nVars
+
1
);
nLutLeaf
++
;
}
if
(
G1
.
nVars
==
0
)
{
// perform testing with a different order
If_CluReverseOrder
(
pF
,
nVars
,
V2P
,
P2V
);
G1
=
If_CluFindGroup
(
pF
,
nVars
,
0
,
V2P
,
P2V
,
nLutLeaf
,
nLutLeaf
+
nLutRoot
==
nVars
+
1
);
// check permutation
If_CluCheckPerm
(
pTruth
,
pF
,
nVars
,
V2P
,
P2V
);
// If_CluCheckPerm( pTruth, pF, nVars, V2P, P2V );
if
(
G1
.
nVars
==
0
)
{
/*
if ( nVars == 6 )
{
Extra_PrintHex( stdout, (unsigned *)pF, nVars ); printf( " " );
Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
if ( !If_CutPerformCheck07( (unsigned *)pF, 6, 6, NULL ) )
printf( "no\n" );
}
*/
return
G1
;
}
}
}
}
// derive
if
(
0
)
{
If_CluMoveGroupToMsb
(
pF
,
nVars
,
V2P
,
P2V
,
&
G1
);
if
(
G1
.
nMyu
==
2
)
Truth
=
If_CluDeriveDisjoint
(
pF
,
nVars
,
V2P
,
P2V
,
&
G1
,
&
R
);
else
Truth
=
If_CluDeriveNonDisjoint
(
pF
,
nVars
,
V2P
,
P2V
,
&
G1
,
&
R
);
// perform checking
if
(
0
)
{
If_CluCheckGroup
(
pTruth
,
nVars
,
&
G1
);
If_CluVerify
(
pTruth
,
nVars
,
&
G1
,
&
R
,
Truth
,
pF
);
}
}
return
G1
;
}
...
...
@@ -600,7 +960,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
int
nLeaves
=
If_CutLeaveNum
(
pCut
);
int
i
,
nLutLeaf
,
nLutRoot
;
// mark the cut as user cut
pCut
->
fUser
=
1
;
//
pCut->fUser = 1;
// quit if parameters are wrong
if
(
strlen
(
pStr
)
!=
2
)
{
...
...
@@ -616,7 +976,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
nLutRoot
=
pStr
[
1
]
-
'0'
;
if
(
nLutRoot
<
3
||
nLutRoot
>
6
)
{
printf
(
"
Leaf
size (%d) should belong to {3,4,5,6}.
\n
"
,
nLutRoot
);
printf
(
"
Root
size (%d) should belong to {3,4,5,6}.
\n
"
,
nLutRoot
);
return
ABC_INFINITY
;
}
if
(
nLeaves
>
nLutLeaf
+
nLutRoot
-
1
)
...
...
@@ -627,7 +987,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
// remember the delays
If_CutForEachLeaf
(
p
,
pCut
,
pLeaf
,
i
)
Delays
[
nLeaves
-
1
-
i
]
=
If_ObjCutBest
(
pLeaf
)
->
Delay
;
Delays
[
i
]
=
If_ObjCutBest
(
pLeaf
)
->
Delay
;
// consider easy case
if
(
nLeaves
<=
Abc_MaxInt
(
nLutLeaf
,
nLutRoot
)
)
...
...
@@ -639,7 +999,6 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
G1
.
pVars
[
i
]
=
i
;
}
G1
.
nVars
=
nLeaves
;
pCut
->
Cost
=
1
;
return
1
.
0
+
If_CluDelayMax
(
&
G1
,
Delays
);
}
...
...
@@ -647,6 +1006,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
G1
=
If_CluCheck
(
(
word
*
)
If_CutTruth
(
pCut
),
nLeaves
,
nLutLeaf
,
nLutRoot
);
if
(
G1
.
nVars
==
0
)
return
ABC_INFINITY
;
// compute the delay
Delays
[
nLeaves
]
=
If_CluDelayMax
(
&
G1
,
Delays
)
+
(
WireDelay
==
0
.
0
)
?
1
.
0
:
WireDelay
;
if
(
G2
.
nVars
)
...
...
@@ -661,7 +1021,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
assert
(
G1
.
nMyu
>=
2
&&
G1
.
nMyu
<=
4
);
if
(
G1
.
nMyu
>
2
)
fUsed
[
G1
.
pVars
[
G1
.
nVars
-
1
]]
=
0
;
assert
(
G2
.
nMyu
>=
2
&&
G2
.
nMyu
<=
4
);
assert
(
!
G2
.
nVars
||
(
G2
.
nMyu
>=
2
&&
G2
.
nMyu
<=
4
)
);
if
(
G2
.
nMyu
>
2
)
fUsed
[
G2
.
pVars
[
G2
.
nVars
-
1
]]
=
0
;
...
...
@@ -681,17 +1041,87 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
return
1
.
0
+
If_CluDelayMax
(
&
G3
,
Delays
);
}
/**Function*************************************************************
Synopsis [Performs additional check.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
If_CutPerformCheck16
(
unsigned
*
pTruth
,
int
nVars
,
int
nLeaves
,
char
*
pStr
)
{
If_Grp_t
G1
=
{
0
},
G2
=
{
0
},
G3
=
{
0
};
int
nLutLeaf
,
nLutRoot
;
// quit if parameters are wrong
if
(
strlen
(
pStr
)
!=
2
)
{
printf
(
"Wrong LUT struct (%s)
\n
"
,
pStr
);
return
0
;
}
nLutLeaf
=
pStr
[
0
]
-
'0'
;
if
(
nLutLeaf
<
3
||
nLutLeaf
>
6
)
{
printf
(
"Leaf size (%d) should belong to {3,4,5,6}.
\n
"
,
nLutLeaf
);
return
0
;
}
nLutRoot
=
pStr
[
1
]
-
'0'
;
if
(
nLutRoot
<
3
||
nLutRoot
>
6
)
{
printf
(
"Root size (%d) should belong to {3,4,5,6}.
\n
"
,
nLutRoot
);
return
0
;
}
if
(
nLeaves
>
nLutLeaf
+
nLutRoot
-
1
)
{
printf
(
"The cut size (%d) is too large for the LUT structure %d%d.
\n
"
,
nLeaves
,
nLutLeaf
,
nLutRoot
);
return
0
;
}
// consider easy case
if
(
nLeaves
<=
Abc_MaxInt
(
nLutLeaf
,
nLutRoot
)
)
return
1
;
// derive the first group
G1
=
If_CluCheck
(
(
word
*
)
pTruth
,
nLeaves
,
nLutLeaf
,
nLutRoot
);
if
(
G1
.
nVars
==
0
)
{
// printf( "-%d ", nLeaves );
return
0
;
}
// printf( "+%d ", nLeaves );
return
1
;
}
// testing procedure
void
If_CluTest
()
{
// word t = 0xff00f0f0ccccaaaa;
word
t
=
0xfedcba9876543210
;
int
nLeaves
=
6
;
// word t = 0xfedcba9876543210;
// word t = 0xec64000000000000;
// word t = 0x0100200000000001;
// word t2[4] = { 0x0000800080008000, 0x8000000000008000, 0x8000000080008000, 0x0000000080008000 };
// word t = 0x07770FFF07770FFF;
// word t = 0x002000D000D00020;
// word t = 0x000F000E000F000F;
word
t
=
0xF7FFF7F7F7F7F7F7
;
int
nVars
=
6
;
int
nLutLeaf
=
4
;
int
nLutRoot
=
4
;
If_Grp_t
G
;
G
=
If_CluCheck
(
&
t
,
nLeaves
,
nLutLeaf
,
nLutRoot
);
return
;
If_CutPerformCheck07
(
(
unsigned
*
)
&
t
,
6
,
6
,
NULL
);
// return;
Kit_DsdPrintFromTruth
(
(
unsigned
*
)
&
t
,
nVars
);
printf
(
"
\n
"
);
G
=
If_CluCheck
(
&
t
,
nVars
,
nLutLeaf
,
nLutRoot
);
If_CluPrintGroup
(
&
G
);
}
...
...
src/map/if/ifMan.c
View file @
e6e6a3cf
...
...
@@ -127,8 +127,15 @@ void If_ManRestart( If_Man_t * p )
***********************************************************************/
void
If_ManStop
(
If_Man_t
*
p
)
{
if
(
p
->
nCutsUseless
&&
p
->
pPars
->
fVerbose
)
Abc_Print
(
1
,
"Useless cuts = %7d (out of %7d) (%6.2f %%)
\n
"
,
p
->
nCutsUseless
,
p
->
nCutsTotal
,
100
.
0
*
p
->
nCutsUseless
/
(
p
->
nCutsTotal
+
1
)
);
// if ( p->nCutsUselessAll && p->pPars->fVerbose )
if
(
p
->
nCutsUselessAll
)
{
int
i
;
for
(
i
=
0
;
i
<=
16
;
i
++
)
if
(
p
->
nCutsUseless
[
i
]
)
Abc_Print
(
1
,
"Useless cuts %2d = %7d (out of %7d) (%6.2f %%)
\n
"
,
i
,
p
->
nCutsUseless
[
i
],
p
->
nCutsCount
[
i
],
100
.
0
*
p
->
nCutsUseless
[
i
]
/
(
p
->
nCutsCount
[
i
]
+
1
)
);
Abc_Print
(
1
,
"Useless cuts all = %7d (out of %7d) (%6.2f %%)
\n
"
,
p
->
nCutsUselessAll
,
p
->
nCutsCountAll
,
100
.
0
*
p
->
nCutsUselessAll
/
(
p
->
nCutsCountAll
+
1
)
);
}
// Abc_PrintTime( 1, "Truth", p->timeTruth );
// Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
Vec_IntFreeP
(
&
p
->
vCoAttrs
);
...
...
src/map/if/ifMap.c
View file @
e6e6a3cf
...
...
@@ -153,9 +153,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if
(
pCut
->
nLeaves
>
0
)
{
// recompute the parameters of the best cut
if
(
p
->
pPars
->
pLutStruct
)
pCut
->
Delay
=
If_CutDelayLutStruct
(
p
,
pCut
,
p
->
pPars
->
pLutStruct
,
p
->
pPars
->
WireDelay
);
else
if
(
p
->
pPars
->
fDelayOpt
)
/// if ( p->pPars->pLutStruct )
/// pCut->Delay = If_CutDelayLutStruct( p, pCut, p->pPars->pLutStruct, p->pPars->WireDelay );
// else if ( p->pPars->fDelayOpt )
if
(
p
->
pPars
->
fDelayOpt
)
pCut
->
Delay
=
If_CutDelaySopCost
(
p
,
pCut
);
else
pCut
->
Delay
=
If_CutDelay
(
p
,
pObj
,
pCut
);
...
...
@@ -205,9 +206,12 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut
->
fUseless
=
0
;
if
(
p
->
pPars
->
pFuncCell
&&
RetValue
<
2
)
{
assert
(
pCut
->
nLimit
>=
4
&&
pCut
->
nLimit
<=
10
);
pCut
->
fUseless
=
!
p
->
pPars
->
pFuncCell
(
If_CutTruth
(
pCut
),
pCut
->
nLimit
,
pCut
->
nLeaves
);
p
->
nCutsUseless
+=
pCut
->
fUseless
;
assert
(
pCut
->
nLimit
>=
4
&&
pCut
->
nLimit
<=
16
);
pCut
->
fUseless
=
!
p
->
pPars
->
pFuncCell
(
If_CutTruth
(
pCut
),
pCut
->
nLimit
,
pCut
->
nLeaves
,
p
->
pPars
->
pLutStruct
);
p
->
nCutsUselessAll
+=
pCut
->
fUseless
;
p
->
nCutsUseless
[
pCut
->
nLeaves
]
+=
pCut
->
fUseless
;
p
->
nCutsCountAll
++
;
p
->
nCutsCount
[
pCut
->
nLeaves
]
++
;
}
}
...
...
@@ -217,9 +221,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if
(
pCut
->
Cost
==
IF_COST_MAX
)
continue
;
// check if the cut satisfies the required times
if
(
p
->
pPars
->
pLutStruct
)
pCut
->
Delay
=
If_CutDelayLutStruct
(
p
,
pCut
,
p
->
pPars
->
pLutStruct
,
p
->
pPars
->
WireDelay
);
else
if
(
p
->
pPars
->
fDelayOpt
)
/// if ( p->pPars->pLutStruct )
/// pCut->Delay = If_CutDelayLutStruct( p, pCut, p->pPars->pLutStruct, p->pPars->WireDelay );
// else if ( p->pPars->fDelayOpt )
if
(
p
->
pPars
->
fDelayOpt
)
pCut
->
Delay
=
If_CutDelaySopCost
(
p
,
pCut
);
else
pCut
->
Delay
=
If_CutDelay
(
p
,
pObj
,
pCut
);
...
...
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