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
68c79ee8
Commit
68c79ee8
authored
Jun 15, 2011
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added command &filter to filter equiv classes.
parent
dcd95cac
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
471 additions
and
138 deletions
+471
-138
src/aig/gia/gia.h
+3
-0
src/aig/gia/giaEquiv.c
+388
-137
src/base/abci/abc.c
+80
-1
No files found.
src/aig/gia/gia.h
View file @
68c79ee8
...
@@ -675,6 +675,9 @@ extern void Gia_ManEquivImprove( Gia_Man_t * p );
...
@@ -675,6 +675,9 @@ extern void Gia_ManEquivImprove( Gia_Man_t * p );
extern
Gia_Man_t
*
Gia_ManEquivToChoices
(
Gia_Man_t
*
p
,
int
nSnapshots
);
extern
Gia_Man_t
*
Gia_ManEquivToChoices
(
Gia_Man_t
*
p
,
int
nSnapshots
);
extern
int
Gia_ManCountChoiceNodes
(
Gia_Man_t
*
p
);
extern
int
Gia_ManCountChoiceNodes
(
Gia_Man_t
*
p
);
extern
int
Gia_ManCountChoices
(
Gia_Man_t
*
p
);
extern
int
Gia_ManCountChoices
(
Gia_Man_t
*
p
);
extern
int
Gia_ManFilterEquivsForSpeculation
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
,
int
fLatchA
,
int
fLatchB
);
extern
int
Gia_ManFilterEquivsUsingParts
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
);
extern
void
Gia_ManFilterEquivsUsingLatches
(
Gia_Man_t
*
pGia
,
int
fFlopsOnly
,
int
fFlopsWith
);
/*=== giaFanout.c =========================================================*/
/*=== giaFanout.c =========================================================*/
extern
void
Gia_ObjAddFanout
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
Gia_Obj_t
*
pFanout
);
extern
void
Gia_ObjAddFanout
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
Gia_Obj_t
*
pFanout
);
extern
void
Gia_ObjRemoveFanout
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
Gia_Obj_t
*
pFanout
);
extern
void
Gia_ObjRemoveFanout
(
Gia_Man_t
*
p
,
Gia_Obj_t
*
pObj
,
Gia_Obj_t
*
pFanout
);
...
...
src/aig/gia/giaEquiv.c
View file @
68c79ee8
...
@@ -875,143 +875,6 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
...
@@ -875,143 +875,6 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
return
pNew
;
return
pNew
;
}
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Gia_ManFilterEquivsForSpeculation
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
,
int
fLatchA
,
int
fLatchB
)
{
Gia_Man_t
*
pGia1
,
*
pGia2
,
*
pMiter
;
Gia_Obj_t
*
pObj1
,
*
pObj2
,
*
pObjM
,
*
pObj
;
int
i
,
iObj
,
iNext
,
Counter
=
0
;
if
(
pGia
->
pReprs
==
NULL
||
pGia
->
pNexts
==
NULL
)
{
printf
(
"Equivalences are not defined.
\n
"
);
return
0
;
}
pGia1
=
Gia_ReadAiger
(
pName1
,
0
);
if
(
pGia1
==
NULL
)
{
printf
(
"Cannot read first file %s.
\n
"
,
pName1
);
return
0
;
}
pGia2
=
Gia_ReadAiger
(
pName2
,
0
);
if
(
pGia2
==
NULL
)
{
Gia_ManStop
(
pGia2
);
printf
(
"Cannot read second file %s.
\n
"
,
pName2
);
return
0
;
}
pMiter
=
Gia_ManMiter
(
pGia1
,
pGia2
,
0
,
1
,
0
);
if
(
pMiter
==
NULL
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
printf
(
"Cannot create sequential miter.
\n
"
);
return
0
;
}
// make sure the miter is isomorphic
if
(
Gia_ManObjNum
(
pGia
)
!=
Gia_ManObjNum
(
pMiter
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The number of objects in different.
\n
"
);
return
0
;
}
if
(
memcmp
(
pGia
->
pObjs
,
pMiter
->
pObjs
,
sizeof
(
Gia_Obj_t
)
*
Gia_ManObjNum
(
pGia
)
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The AIG structure of the miter does not match.
\n
"
);
return
0
;
}
// transfer copies
Gia_ManCleanMark0
(
pGia
);
Gia_ManForEachObj
(
pGia1
,
pObj1
,
i
)
{
if
(
pObj1
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj1
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark0
=
1
;
}
Gia_ManCleanMark1
(
pGia
);
Gia_ManForEachObj
(
pGia2
,
pObj2
,
i
)
{
if
(
pObj2
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj2
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark1
=
1
;
}
// filter equivalences
Gia_ManForEachConst
(
pGia
,
i
)
{
Gia_ObjUnsetRepr
(
pGia
,
i
);
assert
(
pGia
->
pNexts
[
i
]
==
0
);
}
Gia_ManForEachClass
(
pGia
,
i
)
{
// find the first colorA and colorB
int
ClassA
=
-
1
,
ClassB
=
-
1
;
Gia_ClassForEachObj
(
pGia
,
i
,
iObj
)
{
pObj
=
Gia_ManObj
(
pGia
,
iObj
);
if
(
ClassA
==
-
1
&&
pObj
->
fMark0
&&
!
pObj
->
fMark1
)
{
if
(
fLatchA
&&
!
Gia_ObjIsRo
(
pGia
,
pObj
)
)
continue
;
ClassA
=
iObj
;
}
if
(
ClassB
==
-
1
&&
pObj
->
fMark1
&&
!
pObj
->
fMark0
)
{
if
(
fLatchB
&&
!
Gia_ObjIsRo
(
pGia
,
pObj
)
)
continue
;
ClassB
=
iObj
;
}
}
// undo equivalence classes
for
(
iObj
=
i
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
);
iObj
;
iObj
=
iNext
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
)
)
{
Gia_ObjUnsetRepr
(
pGia
,
iObj
);
Gia_ObjSetNext
(
pGia
,
iObj
,
0
);
}
assert
(
!
Gia_ObjIsHead
(
pGia
,
i
)
);
if
(
ClassA
>
0
&&
ClassB
>
0
)
{
if
(
ClassA
>
ClassB
)
{
ClassA
^=
ClassB
;
ClassB
^=
ClassA
;
ClassA
^=
ClassB
;
}
assert
(
ClassA
<
ClassB
);
Gia_ObjSetNext
(
pGia
,
ClassA
,
ClassB
);
Gia_ObjSetRepr
(
pGia
,
ClassB
,
ClassA
);
Counter
++
;
assert
(
Gia_ObjIsHead
(
pGia
,
ClassA
)
);
}
}
printf
(
"The number of two-node classes after filtering = %d.
\n
"
,
Counter
);
//Gia_ManEquivPrintClasses( pGia, 1, 0 );
Gia_ManCleanMark0
(
pGia
);
Gia_ManCleanMark1
(
pGia
);
return
1
;
}
/**Function*************************************************************
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Synopsis [Reduces AIG using equivalence classes.]
...
@@ -1895,6 +1758,394 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
...
@@ -1895,6 +1758,394 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
return
1
;
return
1
;
}
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Gia_ManFilterEquivsForSpeculation
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
,
int
fLatchA
,
int
fLatchB
)
{
Gia_Man_t
*
pGia1
,
*
pGia2
,
*
pMiter
;
Gia_Obj_t
*
pObj1
,
*
pObj2
,
*
pObjM
,
*
pObj
;
int
i
,
iObj
,
iNext
,
Counter
=
0
;
if
(
pGia
->
pReprs
==
NULL
||
pGia
->
pNexts
==
NULL
)
{
printf
(
"Equivalences are not defined.
\n
"
);
return
0
;
}
pGia1
=
Gia_ReadAiger
(
pName1
,
0
);
if
(
pGia1
==
NULL
)
{
printf
(
"Cannot read first file %s.
\n
"
,
pName1
);
return
0
;
}
pGia2
=
Gia_ReadAiger
(
pName2
,
0
);
if
(
pGia2
==
NULL
)
{
Gia_ManStop
(
pGia2
);
printf
(
"Cannot read second file %s.
\n
"
,
pName2
);
return
0
;
}
pMiter
=
Gia_ManMiter
(
pGia1
,
pGia2
,
0
,
1
,
0
);
if
(
pMiter
==
NULL
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
printf
(
"Cannot create sequential miter.
\n
"
);
return
0
;
}
// make sure the miter is isomorphic
if
(
Gia_ManObjNum
(
pGia
)
!=
Gia_ManObjNum
(
pMiter
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The number of objects in different.
\n
"
);
return
0
;
}
if
(
memcmp
(
pGia
->
pObjs
,
pMiter
->
pObjs
,
sizeof
(
Gia_Obj_t
)
*
Gia_ManObjNum
(
pGia
)
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The AIG structure of the miter does not match.
\n
"
);
return
0
;
}
// transfer copies
Gia_ManCleanMark0
(
pGia
);
Gia_ManForEachObj
(
pGia1
,
pObj1
,
i
)
{
if
(
pObj1
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj1
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark0
=
1
;
}
Gia_ManCleanMark1
(
pGia
);
Gia_ManForEachObj
(
pGia2
,
pObj2
,
i
)
{
if
(
pObj2
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj2
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark1
=
1
;
}
// filter equivalences
Gia_ManForEachConst
(
pGia
,
i
)
{
Gia_ObjUnsetRepr
(
pGia
,
i
);
assert
(
pGia
->
pNexts
[
i
]
==
0
);
}
Gia_ManForEachClass
(
pGia
,
i
)
{
// find the first colorA and colorB
int
ClassA
=
-
1
,
ClassB
=
-
1
;
Gia_ClassForEachObj
(
pGia
,
i
,
iObj
)
{
pObj
=
Gia_ManObj
(
pGia
,
iObj
);
if
(
ClassA
==
-
1
&&
pObj
->
fMark0
&&
!
pObj
->
fMark1
)
{
if
(
fLatchA
&&
!
Gia_ObjIsRo
(
pGia
,
pObj
)
)
continue
;
ClassA
=
iObj
;
}
if
(
ClassB
==
-
1
&&
pObj
->
fMark1
&&
!
pObj
->
fMark0
)
{
if
(
fLatchB
&&
!
Gia_ObjIsRo
(
pGia
,
pObj
)
)
continue
;
ClassB
=
iObj
;
}
}
// undo equivalence classes
for
(
iObj
=
i
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
);
iObj
;
iObj
=
iNext
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
)
)
{
Gia_ObjUnsetRepr
(
pGia
,
iObj
);
Gia_ObjSetNext
(
pGia
,
iObj
,
0
);
}
assert
(
!
Gia_ObjIsHead
(
pGia
,
i
)
);
if
(
ClassA
>
0
&&
ClassB
>
0
)
{
if
(
ClassA
>
ClassB
)
{
ClassA
^=
ClassB
;
ClassB
^=
ClassA
;
ClassA
^=
ClassB
;
}
assert
(
ClassA
<
ClassB
);
Gia_ObjSetNext
(
pGia
,
ClassA
,
ClassB
);
Gia_ObjSetRepr
(
pGia
,
ClassB
,
ClassA
);
Counter
++
;
assert
(
Gia_ObjIsHead
(
pGia
,
ClassA
)
);
}
}
printf
(
"The number of two-node classes after filtering = %d.
\n
"
,
Counter
);
//Gia_ManEquivPrintClasses( pGia, 1, 0 );
Gia_ManCleanMark0
(
pGia
);
Gia_ManCleanMark1
(
pGia
);
return
1
;
}
/**Function*************************************************************
Synopsis [Reduces AIG using equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Gia_ManFilterEquivsUsingParts
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
)
{
Vec_Int_t
*
vNodes
;
Gia_Man_t
*
pGia1
,
*
pGia2
,
*
pMiter
;
Gia_Obj_t
*
pObj1
,
*
pObj2
,
*
pObjM
,
*
pObj
;
int
i
,
k
,
iObj
,
iNext
,
iPrev
,
iRepr
;
int
iLitsOld
,
iLitsNew
;
if
(
pGia
->
pReprs
==
NULL
||
pGia
->
pNexts
==
NULL
)
{
printf
(
"Equivalences are not defined.
\n
"
);
return
0
;
}
pGia1
=
Gia_ReadAiger
(
pName1
,
0
);
if
(
pGia1
==
NULL
)
{
printf
(
"Cannot read first file %s.
\n
"
,
pName1
);
return
0
;
}
pGia2
=
Gia_ReadAiger
(
pName2
,
0
);
if
(
pGia2
==
NULL
)
{
Gia_ManStop
(
pGia2
);
printf
(
"Cannot read second file %s.
\n
"
,
pName2
);
return
0
;
}
pMiter
=
Gia_ManMiter
(
pGia1
,
pGia2
,
0
,
1
,
0
);
if
(
pMiter
==
NULL
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
printf
(
"Cannot create sequential miter.
\n
"
);
return
0
;
}
// make sure the miter is isomorphic
if
(
Gia_ManObjNum
(
pGia
)
!=
Gia_ManObjNum
(
pMiter
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The number of objects in different.
\n
"
);
return
0
;
}
if
(
memcmp
(
pGia
->
pObjs
,
pMiter
->
pObjs
,
sizeof
(
Gia_Obj_t
)
*
Gia_ManObjNum
(
pGia
)
)
)
{
Gia_ManStop
(
pGia1
);
Gia_ManStop
(
pGia2
);
Gia_ManStop
(
pMiter
);
printf
(
"The AIG structure of the miter does not match.
\n
"
);
return
0
;
}
// transfer copies
Gia_ManCleanMark0
(
pGia
);
Gia_ManForEachObj
(
pGia1
,
pObj1
,
i
)
{
if
(
pObj1
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj1
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark0
=
1
;
}
Gia_ManCleanMark1
(
pGia
);
Gia_ManForEachObj
(
pGia2
,
pObj2
,
i
)
{
if
(
pObj2
->
Value
==
~
0
)
continue
;
pObjM
=
Gia_ManObj
(
pMiter
,
Gia_Lit2Var
(
pObj2
->
Value
)
);
pObj
=
Gia_ManObj
(
pGia
,
Gia_ObjId
(
pMiter
,
pObjM
)
);
pObj
->
fMark1
=
1
;
}
// filter equivalences
iLitsOld
=
iLitsNew
=
0
;
Gia_ManForEachConst
(
pGia
,
i
)
{
iLitsOld
++
;
pObj
=
Gia_ManObj
(
pGia
,
i
);
assert
(
pGia
->
pNexts
[
i
]
==
0
);
assert
(
pObj
->
fMark0
||
pObj
->
fMark1
);
if
(
pObj
->
fMark0
&&
pObj
->
fMark1
)
// belongs to both A and B
Gia_ObjUnsetRepr
(
pGia
,
i
);
else
iLitsNew
++
;
}
// filter equivalences
vNodes
=
Vec_IntAlloc
(
100
);
Gia_ManForEachClass
(
pGia
,
i
)
{
int
fSeenA
=
0
,
fSeenB
=
0
;
assert
(
pObj
->
fMark0
||
pObj
->
fMark1
);
Vec_IntClear
(
vNodes
);
Gia_ClassForEachObj
(
pGia
,
i
,
iObj
)
{
pObj
=
Gia_ManObj
(
pGia
,
iObj
);
if
(
pObj
->
fMark0
&&
!
pObj
->
fMark1
)
{
fSeenA
=
1
;
Vec_IntPush
(
vNodes
,
iObj
);
}
if
(
!
pObj
->
fMark0
&&
pObj
->
fMark1
)
{
fSeenB
=
1
;
Vec_IntPush
(
vNodes
,
iObj
);
}
iLitsOld
++
;
}
iLitsOld
--
;
// undo equivalence classes
for
(
iObj
=
i
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
);
iObj
;
iObj
=
iNext
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
)
)
{
Gia_ObjUnsetRepr
(
pGia
,
iObj
);
Gia_ObjSetNext
(
pGia
,
iObj
,
0
);
}
assert
(
!
Gia_ObjIsHead
(
pGia
,
i
)
);
if
(
fSeenA
&&
fSeenB
&&
Vec_IntSize
(
vNodes
)
>
1
)
{
// create new class
iPrev
=
iRepr
=
Vec_IntEntry
(
vNodes
,
0
);
Vec_IntForEachEntryStart
(
vNodes
,
iObj
,
k
,
1
)
{
Gia_ObjSetRepr
(
pGia
,
iObj
,
iRepr
);
Gia_ObjSetNext
(
pGia
,
iPrev
,
iObj
);
iPrev
=
iObj
;
iLitsNew
++
;
}
assert
(
Gia_ObjNext
(
pGia
,
iPrev
)
==
0
);
}
}
Vec_IntFree
(
vNodes
);
printf
(
"The number of literals: Before = %d. After = %d.
\n
"
,
iLitsOld
,
iLitsNew
);
//Gia_ManEquivPrintClasses( pGia, 1, 0 );
Gia_ManCleanMark0
(
pGia
);
Gia_ManCleanMark1
(
pGia
);
return
1
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Gia_ManFilterEquivsUsingLatches
(
Gia_Man_t
*
pGia
,
int
fFlopsOnly
,
int
fFlopsWith
)
{
Vec_Int_t
*
vNodes
;
Gia_Obj_t
*
pObj
;
int
i
,
k
,
iObj
,
iNext
,
iPrev
,
iRepr
;
int
iLitsOld
=
0
,
iLitsNew
=
0
;
assert
(
fFlopsOnly
^
fFlopsWith
);
vNodes
=
Vec_IntAlloc
(
100
);
// remove all noo-flop constants
Gia_ManForEachConst
(
pGia
,
i
)
{
iLitsOld
++
;
pObj
=
Gia_ManObj
(
pGia
,
i
);
assert
(
pGia
->
pNexts
[
i
]
==
0
);
if
(
!
Gia_ObjIsRo
(
pGia
,
pObj
)
)
Gia_ObjUnsetRepr
(
pGia
,
i
);
else
iLitsNew
++
;
}
// clear the classes
if
(
fFlopsOnly
)
{
Gia_ManForEachClass
(
pGia
,
i
)
{
Vec_IntClear
(
vNodes
);
Gia_ClassForEachObj
(
pGia
,
i
,
iObj
)
{
pObj
=
Gia_ManObj
(
pGia
,
iObj
);
if
(
Gia_ObjIsRo
(
pGia
,
pObj
)
)
Vec_IntPush
(
vNodes
,
iObj
);
iLitsOld
++
;
}
iLitsOld
--
;
// undo equivalence classes
for
(
iObj
=
i
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
);
iObj
;
iObj
=
iNext
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
)
)
{
Gia_ObjUnsetRepr
(
pGia
,
iObj
);
Gia_ObjSetNext
(
pGia
,
iObj
,
0
);
}
assert
(
!
Gia_ObjIsHead
(
pGia
,
i
)
);
if
(
Vec_IntSize
(
vNodes
)
>
1
)
{
// create new class
iPrev
=
iRepr
=
Vec_IntEntry
(
vNodes
,
0
);
Vec_IntForEachEntryStart
(
vNodes
,
iObj
,
k
,
1
)
{
Gia_ObjSetRepr
(
pGia
,
iObj
,
iRepr
);
Gia_ObjSetNext
(
pGia
,
iPrev
,
iObj
);
iPrev
=
iObj
;
iLitsNew
++
;
}
assert
(
Gia_ObjNext
(
pGia
,
iPrev
)
==
0
);
}
}
}
else
{
Gia_ManForEachClass
(
pGia
,
i
)
{
int
fSeenFlop
=
0
;
Gia_ClassForEachObj
(
pGia
,
i
,
iObj
)
{
pObj
=
Gia_ManObj
(
pGia
,
iObj
);
if
(
Gia_ObjIsRo
(
pGia
,
pObj
)
)
fSeenFlop
=
1
;
iLitsOld
++
;
iLitsNew
++
;
}
iLitsOld
--
;
iLitsNew
--
;
if
(
fSeenFlop
)
continue
;
// undo equivalence classes
for
(
iObj
=
i
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
);
iObj
;
iObj
=
iNext
,
iNext
=
Gia_ObjNext
(
pGia
,
iObj
)
)
{
Gia_ObjUnsetRepr
(
pGia
,
iObj
);
Gia_ObjSetNext
(
pGia
,
iObj
,
0
);
iLitsNew
--
;
}
iLitsNew
++
;
assert
(
!
Gia_ObjIsHead
(
pGia
,
i
)
);
}
}
Vec_IntFree
(
vNodes
);
printf
(
"The number of literals: Before = %d. After = %d.
\n
"
,
iLitsOld
,
iLitsNew
);
}
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
...
...
src/base/abci/abc.c
View file @
68c79ee8
...
@@ -357,6 +357,7 @@ static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, cha
...
@@ -357,6 +357,7 @@ static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, cha
static
int
Abc_CommandAbc9Fraig
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Fraig
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Srm
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Srm
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Srm2
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Srm2
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Filter
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Reduce
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Reduce
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9EquivMark
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9EquivMark
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Cec
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
static
int
Abc_CommandAbc9Cec
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
...
@@ -773,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
...
@@ -773,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&fraig"
,
Abc_CommandAbc9Fraig
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&fraig"
,
Abc_CommandAbc9Fraig
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&srm"
,
Abc_CommandAbc9Srm
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&srm"
,
Abc_CommandAbc9Srm
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&srm2"
,
Abc_CommandAbc9Srm2
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&srm2"
,
Abc_CommandAbc9Srm2
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&filter"
,
Abc_CommandAbc9Filter
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&reduce"
,
Abc_CommandAbc9Reduce
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&reduce"
,
Abc_CommandAbc9Reduce
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&equiv_mark"
,
Abc_CommandAbc9EquivMark
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&equiv_mark"
,
Abc_CommandAbc9EquivMark
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&cec"
,
Abc_CommandAbc9Cec
,
0
);
Cmd_CommandAdd
(
pAbc
,
"ABC9"
,
"&cec"
,
Abc_CommandAbc9Cec
,
0
);
...
@@ -26279,7 +26281,6 @@ usage:
...
@@ -26279,7 +26281,6 @@ usage:
***********************************************************************/
***********************************************************************/
int
Abc_CommandAbc9Srm2
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
int
Abc_CommandAbc9Srm2
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
{
extern
int
Gia_ManFilterEquivsForSpeculation
(
Gia_Man_t
*
pGia
,
char
*
pName1
,
char
*
pName2
,
int
fLatchA
,
int
fLatchB
);
char
pFileName
[
10
],
*
pFileName1
,
*
pFileName2
;
char
pFileName
[
10
],
*
pFileName1
,
*
pFileName2
;
Gia_Man_t
*
pTemp
,
*
pAux
;
Gia_Man_t
*
pTemp
,
*
pAux
;
int
fLatchA
=
0
,
fLatchB
=
0
;
int
fLatchA
=
0
,
fLatchB
=
0
;
...
@@ -26375,6 +26376,84 @@ usage:
...
@@ -26375,6 +26376,84 @@ usage:
SeeAlso []
SeeAlso []
***********************************************************************/
***********************************************************************/
int
Abc_CommandAbc9Filter
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
char
*
pFileName1
=
NULL
,
*
pFileName2
=
NULL
;
int
fFlopsOnly
=
0
,
fFlopsWith
=
0
;
int
c
,
fVerbose
=
0
;
Extra_UtilGetoptReset
();
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"fgvh"
)
)
!=
EOF
)
{
switch
(
c
)
{
case
'f'
:
fFlopsOnly
^=
1
;
break
;
case
'g'
:
fFlopsWith
^=
1
;
break
;
case
'v'
:
fVerbose
^=
1
;
break
;
case
'h'
:
goto
usage
;
default:
goto
usage
;
}
}
if
(
pAbc
->
pGia
==
NULL
)
{
Abc_Print
(
-
1
,
"Abc_CommandAbc9Srm2(): There is no AIG.
\n
"
);
return
1
;
}
if
(
pAbc
->
pGia
->
pReprs
==
NULL
||
pAbc
->
pGia
->
pNexts
==
NULL
)
{
Abc_Print
(
-
1
,
"Equivalences are not defined.
\n
"
);
return
0
;
}
if
(
argc
!=
globalUtilOptind
&&
argc
!=
globalUtilOptind
+
2
)
{
Abc_Print
(
-
1
,
"Abc_CommandAbc9Srm2(): Expecting two file names on the command line.
\n
"
);
return
1
;
}
// filter using one of the choices
if
(
fFlopsOnly
^
fFlopsWith
)
Gia_ManFilterEquivsUsingLatches
(
pAbc
->
pGia
,
fFlopsOnly
,
fFlopsWith
);
// get the input file name
if
(
argc
==
globalUtilOptind
+
2
)
{
pFileName1
=
argv
[
globalUtilOptind
];
pFileName2
=
argv
[
globalUtilOptind
+
1
];
if
(
!
Gia_ManFilterEquivsUsingParts
(
pAbc
->
pGia
,
pFileName1
,
pFileName2
)
)
{
Abc_Print
(
-
1
,
"Filtering equivalences using PartA and PartB has failed.
\n
"
);
return
1
;
}
}
return
0
;
usage:
Abc_Print
(
-
2
,
"usage: &filter [-fgvh] <PartA_FileName> <PartB_FileName>
\n
"
);
Abc_Print
(
-
2
,
"
\t
performs filtering of equivalence classes
\n
"
);
Abc_Print
(
-
2
,
"
\t
(if Parts A/B are given, removes classes composed of one part)
\n
"
);
Abc_Print
(
-
2
,
"
\t
-f : toggle removing all elements except flops [default = %s]
\n
"
,
fFlopsOnly
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-g : toggle removing removing classes without flops [default = %s]
\n
"
,
fFlopsWith
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-v : toggle printing verbose information [default = %s]
\n
"
,
fVerbose
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-h : print the command usage
\n
"
);
return
1
;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int
Abc_CommandAbc9Reduce
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
int
Abc_CommandAbc9Reduce
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
{
Gia_Man_t
*
pTemp
,
*
pTemp2
;
Gia_Man_t
*
pTemp
,
*
pTemp2
;
...
...
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