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
f53e56e8
Commit
f53e56e8
authored
Sep 05, 2013
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Improved unrolling manager.
parent
6570fe14
Show whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
130 additions
and
81 deletions
+130
-81
src/aig/gia/giaAiger.c
+2
-2
src/base/abci/abc.c
+7
-7
src/sat/bmc/bmcUnroll.c
+121
-72
No files found.
src/aig/gia/giaAiger.c
View file @
f53e56e8
...
...
@@ -672,7 +672,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
if
(
fVerbose
)
printf
(
"Finished reading extension
\"
q
\"
.
\n
"
);
}
// read switching activity
else
if
(
*
pCur
==
'
s
'
)
else
if
(
*
pCur
==
'
u
'
)
{
unsigned
char
*
pSwitching
;
pCur
++
;
...
...
@@ -1258,7 +1258,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
// write switching activity
if
(
p
->
pSwitching
)
{
fprintf
(
pFile
,
"
s
"
);
fprintf
(
pFile
,
"
u
"
);
Gia_FileWriteBufferSize
(
pFile
,
Gia_ManObjNum
(
p
)
);
fwrite
(
p
->
pSwitching
,
1
,
Gia_ManObjNum
(
p
),
pFile
);
}
...
...
src/base/abci/abc.c
View file @
f53e56e8
...
...
@@ -19644,7 +19644,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if
(
pNtk
->
vPhases
!=
NULL
)
if
(
pNtk
&&
pNtk
->
vPhases
!=
NULL
)
{
Abc_Print
(
-
1
,
"Cannot compare networks with phases defined.
\n
"
);
return
1
;
...
...
@@ -32958,7 +32958,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t
*
pTemp
=
NULL
;
int
c
,
fVerbose
=
0
;
int
nFrames
=
3
;
int
nFrames
=
10
;
int
fSwitch
=
0
;
// extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
// extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
...
...
@@ -32967,7 +32967,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Ga2_ManComputeTest( Gia_Man_t * p );
// extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
// extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
// extern void Unr_ManTest( Gia_Man_t * pGia
);
extern
void
Unr_ManTest
(
Gia_Man_t
*
pGia
,
int
nFrames
);
// extern int Gia_ManVerify( Gia_Man_t * pGia );
// extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p );
// extern void Gia_ManCollectSeqTest( Gia_Man_t * p );
...
...
@@ -32976,7 +32976,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames );
// extern void Gia_ManMuxProfiling( Gia_Man_t * p );
// extern Gia_Man_t * Mig_ManTest( Gia_Man_t * pGia );
extern
Gia_Man_t
*
Gia_ManInterTest
(
Gia_Man_t
*
p
);
//
extern Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p );
Extra_UtilGetoptReset
();
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"Fsvh"
)
)
!=
EOF
)
...
...
@@ -33036,7 +33036,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Ga2_ManComputeTest( pAbc->pGia );
// Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose );
// Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 );
// Unr_ManTest( pAbc->pGia
);
Unr_ManTest
(
pAbc
->
pGia
,
nFrames
);
// Gia_ManVerifyWithBoxes( pAbc->pGia );
// Gia_ManCollectSeqTest( pAbc->pGia );
// pTemp = Gia_ManOptimizeRing( pAbc->pGia );
...
...
@@ -33048,8 +33048,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManMuxProfiling( pAbc->pGia );
// pTemp = Mig_ManTest( pAbc->pGia );
// Abc_FrameUpdateGia( pAbc, pTemp );
pTemp
=
Gia_ManInterTest
(
pAbc
->
pGia
);
Abc_FrameUpdateGia
(
pAbc
,
pTemp
);
//
pTemp = Gia_ManInterTest( pAbc->pGia );
//
Abc_FrameUpdateGia( pAbc, pTemp );
return
0
;
usage:
Abc_Print
(
-
2
,
"usage: &test [-F num] [-svh]
\n
"
);
src/sat/bmc/bmcUnroll.c
View file @
f53e56e8
...
...
@@ -48,7 +48,7 @@ struct Unr_Man_t_
{
// input data
Gia_Man_t
*
pGia
;
// the user's AIG manager
Gia_Man_t
*
pNew
;
// unrolling manager
//
Gia_Man_t * pNew; // unrolling manager
int
nObjs
;
// the number of objects
// intermediate data
Vec_Int_t
*
vOrder
;
// ordering of GIA objects
...
...
@@ -61,30 +61,36 @@ struct Unr_Man_t_
Vec_Int_t
*
vObjLim
;
// handle of the first object in each frame
Vec_Int_t
*
vResLits
;
// resulting literals
Vec_Int_t
*
vCiMap
;
// mapping of GIA CIs into unrolling objects
Vec_Int_t
*
v
P
oMap
;
// mapping of GIA POs into unrolling objects
Vec_Int_t
*
v
C
oMap
;
// mapping of GIA POs into unrolling objects
};
static
inline
Unr_Obj_t
*
Unr_ManObj
(
Unr_Man_t
*
p
,
int
h
)
{
assert
(
h
>=
0
&&
h
<
p
->
pEnd
-
p
->
pObjs
);
return
(
Unr_Obj_t
*
)(
p
->
pObjs
+
h
);
}
static
inline
int
Unr_ObjSize
(
Unr_Obj_t
*
pObj
)
{
return
0x7FFFFFFE
&
(
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
)
+
pObj
->
RankMax
);
}
static
inline
int
Unr_ManFanin0Value
(
Unr_Man_t
*
p
,
Unr_Obj_t
*
pObj
)
{
Unr_Obj_t
*
pFanin
=
Unr_ManObj
(
p
,
pObj
->
hFan0
);
int
Index
=
(
pFanin
->
RankCur
+
pFanin
->
RankMax
-
pObj
->
uRDiff0
)
%
pFanin
->
RankMax
;
assert
(
pFanin
->
RankCur
<
=
pFanin
->
RankMax
);
assert
(
pObj
->
uRDiff0
<
=
pFanin
->
RankMax
);
assert
(
pFanin
->
RankCur
<
pFanin
->
RankMax
);
assert
(
pObj
->
uRDiff0
<
pFanin
->
RankMax
);
return
Abc_LitNotCond
(
pFanin
->
Res
[
Index
],
pObj
->
fCompl0
);
}
static
inline
int
Unr_ManFanin1Value
(
Unr_Man_t
*
p
,
Unr_Obj_t
*
pObj
)
{
Unr_Obj_t
*
pFanin
=
Unr_ManObj
(
p
,
pObj
->
hFan1
);
int
Index
=
(
pFanin
->
RankCur
+
pFanin
->
RankMax
-
pObj
->
uRDiff1
)
%
pFanin
->
RankMax
;
assert
(
pFanin
->
RankCur
<
=
pFanin
->
RankMax
);
assert
(
pObj
->
uRDiff1
<
=
pFanin
->
RankMax
);
assert
(
pFanin
->
RankCur
<
pFanin
->
RankMax
);
assert
(
pObj
->
uRDiff1
<
pFanin
->
RankMax
);
return
Abc_LitNotCond
(
pFanin
->
Res
[
Index
],
pObj
->
fCompl1
);
}
static
inline
void
Unr_ManObjSetValue
(
Unr_Man_t
*
p
,
Unr_Obj_t
*
pObj
,
int
Value
)
static
inline
int
Unr_ManObjReadValue
(
Unr_Obj_t
*
pObj
)
{
assert
(
pObj
->
RankCur
>=
0
&&
pObj
->
RankCur
<
pObj
->
RankMax
);
return
pObj
->
Res
[
pObj
->
RankCur
];
}
static
inline
void
Unr_ManObjSetValue
(
Unr_Obj_t
*
pObj
,
int
Value
)
{
pObj
->
RankCur
=
(
0xFFFF
&
(
pObj
->
RankCur
+
1
))
%
pObj
->
RankMax
;
pObj
->
Res
[
pObj
->
RankCur
]
=
Value
;
pObj
->
RankCur
=
(
pObj
->
RankCur
+
1
)
%
pObj
->
RankMax
;
}
////////////////////////////////////////////////////////////////////////
...
...
@@ -157,26 +163,26 @@ void Unr_ManSetup_rec( Unr_Man_t * p, int iObj, int iTent, Vec_Int_t * vRoots )
if
(
Gia_ObjIsAnd
(
pObj
)
||
Gia_ObjIsCo
(
pObj
)
)
{
Unr_ManSetup_rec
(
p
,
(
iFanin
=
Gia_ObjFaninId0
(
pObj
,
iObj
)),
iTent
,
vRoots
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
iTent
-
Vec_IntEntry
(
p
->
vTents
,
iFanin
)
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
Abc_MaxInt
(
0
,
iTent
-
Vec_IntEntry
(
p
->
vTents
,
iFanin
)
-
1
)
);
}
if
(
Gia_ObjIsAnd
(
pObj
)
)
{
Unr_ManSetup_rec
(
p
,
(
iFanin
=
Gia_ObjFaninId1
(
pObj
,
iObj
)),
iTent
,
vRoots
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
iTent
-
Vec_IntEntry
(
p
->
vTents
,
iFanin
)
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
Abc_MaxInt
(
0
,
iTent
-
Vec_IntEntry
(
p
->
vTents
,
iFanin
)
-
1
)
);
}
else
if
(
Gia_ObjIsRo
(
p
->
pGia
,
pObj
)
)
{
Vec_IntPush
(
vRoots
,
(
iFanin
=
Gia_ObjId
(
p
->
pGia
,
Gia_ObjRoToRi
(
p
->
pGia
,
pObj
)))
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
1
);
Vec_IntWriteMaxEntry
(
p
->
vRanks
,
iFanin
,
0
);
}
Vec_IntPush
(
p
->
vOrder
,
iObj
);
}
void
Unr_ManSetup
(
Unr_Man_t
*
p
)
{
Vec_Int_t
*
vRoots
,
*
vRoots2
,
*
vMap
;
Gia_Obj_t
*
pObj
,
*
pObjRi
;
Unr_Obj_t
*
pUnrObj
;
int
i
,
k
,
t
,
iObj
,
nInts
,
*
pInts
;
Gia_Obj_t
*
pObj
;
int
i
,
k
,
t
,
iObj
,
Rank
,
nInts
,
*
pInts
;
abctime
clk
=
Abc_Clock
();
vRoots
=
Vec_IntAlloc
(
100
);
vRoots2
=
Vec_IntAlloc
(
100
);
...
...
@@ -199,72 +205,85 @@ void Unr_ManSetup( Unr_Man_t * p )
ABC_SWAP
(
Vec_Int_t
*
,
vRoots
,
vRoots2
);
}
Vec_IntPush
(
p
->
vOrderLim
,
Vec_IntSize
(
p
->
vOrder
)
);
Vec_IntWriteEntry
(
p
->
vRanks
,
0
,
0
);
Vec_IntFree
(
vRoots
);
Vec_IntFree
(
vRoots2
);
// allocate memory
nInts
=
Vec_IntSize
(
p
->
vOrder
)
*
(
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
))
+
Vec_IntSum
(
p
->
vRanks
);
nInts
=
Vec_IntSize
(
p
->
vOrder
)
*
(
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
));
Vec_IntForEachEntry
(
p
->
vRanks
,
Rank
,
i
)
nInts
+=
0x7FFFFFFE
&
(
Rank
+
1
);
p
->
pObjs
=
pInts
=
ABC_CALLOC
(
int
,
nInts
);
p
->
pEnd
=
p
->
pObjs
+
nInts
;
vMap
=
Vec_IntStartFull
(
p
->
nObjs
);
// create const0 node
pUnrObj
=
Unr_ManObj
(
p
,
pInts
-
p
->
pObjs
);
pUnrObj
->
RankMax
=
1
;
pUnrObj
->
uRDiff0
=
pUnrObj
->
uRDiff1
=
UNR_DIFF_NULL
;
pUnrObj
->
Res
[
0
]
=
0
;
// const0
pInts
+=
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
);
// map the objects
vMap
=
Vec_IntStartFull
(
p
->
nObjs
);
Vec_IntWriteEntry
(
vMap
,
0
,
pInts
-
p
->
pObjs
);
pInts
+=
Unr_ObjSize
(
pUnrObj
);
// mark up the entries
assert
(
Vec_IntSize
(
p
->
vObjLim
)
==
0
);
Vec_IntPush
(
p
->
vObjLim
,
pInts
-
p
->
pObjs
);
for
(
t
=
Vec_IntSize
(
p
->
vOrderLim
)
-
2
;
t
>=
0
;
t
--
)
{
int
Beg
=
Vec_IntEntry
(
p
->
vOrderLim
,
t
);
int
End
=
Vec_IntEntry
(
p
->
vOrderLim
,
t
+
1
);
Vec_IntPush
(
p
->
vObjLim
,
pInts
-
p
->
pObjs
);
Vec_IntForEachEntryStartStop
(
p
->
vOrder
,
iObj
,
i
,
Beg
,
End
)
{
pObj
=
Gia_ManObj
(
p
->
pGia
,
iObj
);
pUnrObj
=
Unr_ManObj
(
p
,
pInts
-
p
->
pObjs
);
pUnrObj
->
uRDiff0
=
pUnrObj
->
uRDiff1
=
UNR_DIFF_NULL
;
if
(
Gia_ObjIsAnd
(
pObj
)
||
Gia_ObjIsCo
(
pObj
)
)
{
pUnrObj
->
hFan0
=
Vec_IntEntry
(
vMap
,
Gia_ObjFaninId0
(
pObj
,
iObj
)
);
pUnrObj
->
fCompl0
=
Gia_ObjFaninC0
(
pObj
);
pUnrObj
->
uRDiff0
=
Vec_IntEntry
(
p
->
vTents
,
iObj
)
-
Vec_IntEntry
(
p
->
vTents
,
Gia_ObjFaninId0
(
pObj
,
iObj
));
}
pUnrObj
->
uRDiff0
=
Abc_MaxInt
(
0
,
Vec_IntEntry
(
p
->
vTents
,
iObj
)
-
Vec_IntEntry
(
p
->
vTents
,
Gia_ObjFaninId0
(
pObj
,
iObj
))
-
1
);
if
(
Gia_ObjIsAnd
(
pObj
)
)
{
pUnrObj
->
hFan1
=
Vec_IntEntry
(
vMap
,
Gia_ObjFaninId1
(
pObj
,
iObj
)
);
pUnrObj
->
fCompl1
=
Gia_ObjFaninC1
(
pObj
);
pUnrObj
->
uRDiff1
=
Vec_IntEntry
(
p
->
vTents
,
iObj
)
-
Vec_IntEntry
(
p
->
vTents
,
Gia_ObjFaninId1
(
pObj
,
iObj
));
}
pUnrObj
->
uRDiff1
=
Abc_MaxInt
(
0
,
Vec_IntEntry
(
p
->
vTents
,
iObj
)
-
Vec_IntEntry
(
p
->
vTents
,
Gia_ObjFaninId1
(
pObj
,
iObj
))
-
1
);
else
if
(
Gia_ObjIsRo
(
p
->
pGia
,
pObj
)
)
{
pObjRi
=
Gia_ObjRoToRi
(
p
->
pGia
,
pObj
);
pUnrObj
->
hFan0
=
Vec_IntEntry
(
vMap
,
Gia_ObjId
(
p
->
pGia
,
pObjRi
)
);
pUnrObj
->
fCompl0
=
0
;
pUnrObj
->
uRDiff0
=
1
;
}
pUnrObj
->
uRDiff0
=
0
;
pUnrObj
->
RankMax
=
Vec_IntEntry
(
p
->
vRanks
,
iObj
)
+
1
;
pUnrObj
->
RankCur
=
0
;
pUnrObj
->
RankCur
=
0
xFFFF
;
pUnrObj
->
OrigId
=
iObj
;
for
(
k
=
0
;
k
<
(
int
)
pUnrObj
->
RankMax
;
k
++
)
pUnrObj
->
Res
[
k
]
=
-
1
;
Vec_IntWriteEntry
(
vMap
,
iObj
,
pInts
-
p
->
pObjs
);
pInts
+=
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
)
+
pUnrObj
->
RankMax
-
1
;
pInts
+=
Unr_ObjSize
(
pUnrObj
)
;
}
Vec_IntPush
(
p
->
vObjLim
,
pInts
-
p
->
pObjs
);
}
assert
(
pInts
-
p
->
pObjs
==
nInts
);
assert
(
pInts
-
p
->
pObjs
<=
nInts
);
Unr_ManProfileRanks
(
p
->
vRanks
);
Vec_IntFreeP
(
&
p
->
vOrder
);
Vec_IntFreeP
(
&
p
->
vOrderLim
);
Vec_IntFreeP
(
&
p
->
vTents
);
Unr_ManProfileRanks
(
p
->
vRanks
);
Vec_IntFreeP
(
&
p
->
vRanks
);
// Vec_IntFreeP( &p->vTents );
// label the objects
Gia_ManForEachObj
(
p
->
pGia
,
pObj
,
i
)
{
if
(
Vec_IntEntry
(
vMap
,
i
)
==
-
1
)
continue
;
pUnrObj
=
Unr_ManObj
(
p
,
Vec_IntEntry
(
vMap
,
i
)
);
if
(
Gia_ObjIsAnd
(
pObj
)
||
Gia_ObjIsCo
(
pObj
)
)
{
pUnrObj
->
hFan0
=
Vec_IntEntry
(
vMap
,
Gia_ObjFaninId0
(
pObj
,
i
)
);
pUnrObj
->
fCompl0
=
Gia_ObjFaninC0
(
pObj
);
assert
(
pUnrObj
->
hFan0
!=
~
0
);
}
if
(
Gia_ObjIsAnd
(
pObj
)
)
{
pUnrObj
->
hFan1
=
Vec_IntEntry
(
vMap
,
Gia_ObjFaninId1
(
pObj
,
i
)
);
pUnrObj
->
fCompl1
=
Gia_ObjFaninC1
(
pObj
);
assert
(
pUnrObj
->
hFan1
!=
~
0
);
}
else
if
(
Gia_ObjIsRo
(
p
->
pGia
,
pObj
)
)
{
pUnrObj
->
hFan0
=
Vec_IntEntry
(
vMap
,
Gia_ObjId
(
p
->
pGia
,
Gia_ObjRoToRi
(
p
->
pGia
,
pObj
))
);
pUnrObj
->
fCompl0
=
0
;
}
}
// store CI/PO objects;
Gia_ManForEachCi
(
p
->
pGia
,
pObj
,
i
)
Vec_IntPush
(
p
->
vCiMap
,
Vec_IntEntry
(
vMap
,
Gia_ObjId
(
p
->
pGia
,
pObj
))
);
Gia_ManForEach
P
o
(
p
->
pGia
,
pObj
,
i
)
Vec_IntPush
(
p
->
v
P
oMap
,
Vec_IntEntry
(
vMap
,
Gia_ObjId
(
p
->
pGia
,
pObj
))
);
Gia_ManForEach
C
o
(
p
->
pGia
,
pObj
,
i
)
Vec_IntPush
(
p
->
v
C
oMap
,
Vec_IntEntry
(
vMap
,
Gia_ObjId
(
p
->
pGia
,
pObj
))
);
Vec_IntFreeP
(
&
vMap
);
printf
(
"Memory usage = %6.2f MB
\n
"
,
4
.
0
*
nInts
/
(
1
<<
20
)
);
...
...
@@ -290,7 +309,7 @@ Unr_Man_t * Unr_ManAlloc( Gia_Man_t * pGia )
p
=
ABC_CALLOC
(
Unr_Man_t
,
1
);
p
->
pGia
=
pGia
;
p
->
nObjs
=
Gia_ManObjNum
(
pGia
);
p
->
pNew
=
Gia_ManStart
(
10000
);
//
p->pNew = Gia_ManStart( 10000 );
p
->
vOrder
=
Vec_IntAlloc
(
p
->
nObjs
);
p
->
vOrderLim
=
Vec_IntAlloc
(
100
);
p
->
vTents
=
Vec_IntStartFull
(
p
->
nObjs
);
...
...
@@ -298,12 +317,13 @@ Unr_Man_t * Unr_ManAlloc( Gia_Man_t * pGia )
p
->
vObjLim
=
Vec_IntAlloc
(
100
);
p
->
vResLits
=
Vec_IntAlloc
(
Gia_ManPoNum
(
pGia
)
);
p
->
vCiMap
=
Vec_IntAlloc
(
Gia_ManCiNum
(
pGia
)
);
p
->
v
PoMap
=
Vec_IntAlloc
(
Gia_ManP
oNum
(
pGia
)
);
p
->
v
CoMap
=
Vec_IntAlloc
(
Gia_ManC
oNum
(
pGia
)
);
return
p
;
}
void
Unr_ManFree
(
Unr_Man_t
*
p
)
{
Gia_ManStop
(
p
->
pNew
);
// Gia_ManStop( p->pNew );
Vec_IntFreeP
(
&
p
->
vTents
);
// intermediate data
Vec_IntFreeP
(
&
p
->
vOrder
);
Vec_IntFreeP
(
&
p
->
vOrderLim
);
...
...
@@ -313,7 +333,7 @@ void Unr_ManFree( Unr_Man_t * p )
Vec_IntFreeP
(
&
p
->
vObjLim
);
Vec_IntFreeP
(
&
p
->
vResLits
);
Vec_IntFreeP
(
&
p
->
vCiMap
);
Vec_IntFreeP
(
&
p
->
v
P
oMap
);
Vec_IntFreeP
(
&
p
->
v
C
oMap
);
ABC_FREE
(
p
->
pObjs
);
ABC_FREE
(
p
);
}
...
...
@@ -331,8 +351,9 @@ void Unr_ManFree( Unr_Man_t * p )
***********************************************************************/
Gia_Man_t
*
Unr_ManUnroll
(
Unr_Man_t
*
p
,
int
nFrames
)
{
Gia_Man_t
*
p
Gia
,
*
pFrames
;
Gia_Man_t
*
p
Temp
,
*
pFrames
;
Unr_Obj_t
*
pUnrObj
;
Vec_Int_t
*
vPiLits
;
int
f
,
i
,
iLit
,
iLit0
,
iLit1
,
hStart
;
pFrames
=
Gia_ManStart
(
10000
);
pFrames
->
pName
=
Abc_UtilStrsav
(
p
->
pGia
->
pName
);
...
...
@@ -340,17 +361,17 @@ Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames )
// create flop values
for
(
i
=
0
;
i
<
Gia_ManRegNum
(
p
->
pGia
);
i
++
)
{
pUnrObj
=
Unr_ManObj
(
p
,
Vec_IntEntry
(
p
->
vCiMap
,
Gia_ManPiNum
(
p
->
pGia
)
+
i
));
Unr_ManObjSetValue
(
p
,
pUnrObj
,
0
);
if
(
Vec_IntEntry
(
p
->
vCoMap
,
Gia_ManPoNum
(
p
->
pGia
)
+
i
)
==
-
1
)
continue
;
pUnrObj
=
Unr_ManObj
(
p
,
Vec_IntEntry
(
p
->
vCoMap
,
Gia_ManPoNum
(
p
->
pGia
)
+
i
)
);
Unr_ManObjSetValue
(
pUnrObj
,
0
);
}
vPiLits
=
Vec_IntAlloc
(
nFrames
*
Gia_ManPiNum
(
p
->
pGia
)
);
for
(
f
=
0
;
f
<
nFrames
;
f
++
)
{
for
(
i
=
0
;
i
<
Gia_ManPiNum
(
p
->
pGia
);
i
++
)
{
pUnrObj
=
Unr_ManObj
(
p
,
Vec_IntEntry
(
p
->
vCiMap
,
Gia_ManPiNum
(
p
->
pGia
)
+
i
));
Unr_ManObjSetValue
(
p
,
pUnrObj
,
Gia_ManAppendCi
(
pFrames
)
);
}
hStart
=
f
<
Vec_IntSize
(
p
->
vObjLim
)
-
1
?
Vec_IntEntry
(
p
->
vObjLim
,
Vec_IntSize
(
p
->
vObjLim
)
-
2
-
f
)
:
0
;
Vec_IntPush
(
vPiLits
,
Gia_ManAppendCi
(
pFrames
)
);
hStart
=
Vec_IntEntry
(
p
->
vObjLim
,
Abc_MaxInt
(
0
,
Vec_IntSize
(
p
->
vObjLim
)
-
1
-
f
)
);
while
(
p
->
pObjs
+
hStart
<
p
->
pEnd
)
{
pUnrObj
=
Unr_ManObj
(
p
,
hStart
);
...
...
@@ -358,22 +379,38 @@ Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames )
{
iLit0
=
Unr_ManFanin0Value
(
p
,
pUnrObj
);
iLit1
=
Unr_ManFanin1Value
(
p
,
pUnrObj
);
iLit
=
Gia_ManAppendAnd
(
pFrames
,
iLit0
,
iLit1
);
Unr_ManObjSetValue
(
p
,
pUnrObj
,
iLit
);
iLit
=
Gia_ManHashAnd
(
pFrames
,
iLit0
,
iLit1
);
assert
(
iLit
>=
0
);
Unr_ManObjSetValue
(
pUnrObj
,
iLit
);
}
else
if
(
pUnrObj
->
uRDiff1
==
UNR_DIFF_NULL
)
else
if
(
pUnrObj
->
uRDiff
0
!=
UNR_DIFF_NULL
&&
pUnrObj
->
uRDiff
1
==
UNR_DIFF_NULL
)
{
iLit
=
Unr_ManFanin0Value
(
p
,
pUnrObj
);
Unr_ManObjSetValue
(
p
,
pUnrObj
,
iLit
);
assert
(
iLit
>=
0
);
Unr_ManObjSetValue
(
pUnrObj
,
iLit
);
}
hStart
+=
sizeof
(
Unr_Obj_t
)
/
sizeof
(
int
)
+
pUnrObj
->
RankMax
-
1
;
else
{
Gia_Obj_t
*
pObj
=
Gia_ManObj
(
p
->
pGia
,
pUnrObj
->
OrigId
);
assert
(
Gia_ObjIsPi
(
p
->
pGia
,
pObj
)
);
assert
(
f
>=
Vec_IntEntry
(
p
->
vTents
,
pUnrObj
->
OrigId
)
);
iLit
=
Vec_IntEntry
(
vPiLits
,
Gia_ManPiNum
(
p
->
pGia
)
*
(
f
-
Vec_IntEntry
(
p
->
vTents
,
pUnrObj
->
OrigId
))
+
Gia_ObjCioId
(
pObj
)
);
Unr_ManObjSetValue
(
pUnrObj
,
iLit
);
}
hStart
+=
Unr_ObjSize
(
pUnrObj
);
}
assert
(
p
->
pObjs
+
hStart
==
p
->
pEnd
);
for
(
i
=
0
;
i
<
Gia_ManPoNum
(
p
->
pGia
);
i
++
)
{
pUnrObj
=
Unr_ManObj
(
p
,
Vec_IntEntry
(
p
->
vCoMap
,
i
));
Gia_ManAppendCo
(
pFrames
,
Unr_ManObjReadValue
(
pUnrObj
)
);
}
}
Vec_IntFree
(
vPiLits
);
Gia_ManHashStop
(
pFrames
);
Gia_ManSetRegNum
(
pFrames
,
0
);
pFrames
=
Gia_ManCleanup
(
p
Gia
=
pFrames
);
Gia_ManStop
(
p
Gia
);
pFrames
=
Gia_ManCleanup
(
p
Temp
=
pFrames
);
Gia_ManStop
(
p
Temp
);
return
pFrames
;
}
...
...
@@ -393,7 +430,7 @@ Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames )
Gia_Man_t
*
pFrames
;
Gia_Obj_t
*
pObj
,
*
pObjRi
;
int
f
,
i
;
pFrames
=
Gia_ManStart
(
Gia_ManObjNum
(
pGia
)
*
nFrames
);
pFrames
=
Gia_ManStart
(
10000
);
pFrames
->
pName
=
Abc_UtilStrsav
(
pGia
->
pName
);
Gia_ManHashAlloc
(
pFrames
);
Gia_ManConst0
(
pGia
)
->
Value
=
0
;
...
...
@@ -406,7 +443,7 @@ Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames )
Gia_ManForEachRiRo
(
pGia
,
pObjRi
,
pObj
,
i
)
pObj
->
Value
=
pObjRi
->
Value
;
Gia_ManForEachAnd
(
pGia
,
pObj
,
i
)
pObj
->
Value
=
Gia_Man
Append
And
(
pFrames
,
Gia_ObjFanin0Copy
(
pObj
),
Gia_ObjFanin1Copy
(
pObj
)
);
pObj
->
Value
=
Gia_Man
Hash
And
(
pFrames
,
Gia_ObjFanin0Copy
(
pObj
),
Gia_ObjFanin1Copy
(
pObj
)
);
Gia_ManForEachCo
(
pGia
,
pObj
,
i
)
pObj
->
Value
=
Gia_ObjFanin0Copy
(
pObj
);
Gia_ManForEachPo
(
pGia
,
pObj
,
i
)
...
...
@@ -430,20 +467,32 @@ Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames )
SeeAlso []
***********************************************************************/
void
Unr_ManTest
(
Gia_Man_t
*
pGia
)
void
Unr_ManTest
(
Gia_Man_t
*
pGia
,
int
nFrames
)
{
// Gia_Man_t * pFrames0, * pFrames1;
// int nFrames = 10;
Gia_Man_t
*
pFrames0
,
*
pFrames1
;
Unr_Man_t
*
p
;
abctime
clk
=
Abc_Clock
();
p
=
Unr_ManAlloc
(
pGia
);
Unr_ManSetup
(
p
);
// pFrames0 = Unr_ManUnroll( p, nFrames );
Abc_PrintTime
(
1
,
"Prepare"
,
Abc_Clock
()
-
clk
);
clk
=
Abc_Clock
();
pFrames0
=
Unr_ManUnroll
(
p
,
nFrames
);
Abc_PrintTime
(
1
,
"Unroll "
,
Abc_Clock
()
-
clk
);
Unr_ManFree
(
p
);
// pFrames1 = Unr_ManUnrollSimple( pGia, nFrames );
//Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
//Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );
// Gia_ManStop( pFrames0 );
// Gia_ManStop( pFrames1 );
clk
=
Abc_Clock
();
pFrames1
=
Unr_ManUnrollSimple
(
pGia
,
nFrames
);
Abc_PrintTime
(
1
,
"UnrollS"
,
Abc_Clock
()
-
clk
);
Gia_ManPrintStats
(
pFrames0
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pFrames1
,
0
,
0
,
0
);
Gia_AigerWrite
(
pFrames0
,
"frames0.aig"
,
0
,
0
);
Gia_AigerWrite
(
pFrames1
,
"frames1.aig"
,
0
,
0
);
Gia_ManStop
(
pFrames0
);
Gia_ManStop
(
pFrames1
);
}
////////////////////////////////////////////////////////////////////////
...
...
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