summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-05-11 17:01:13 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-05-11 17:01:13 -0700
commitf2abd6b8a9b59e28769662bfc6e6e6670de20faa (patch)
tree4866c5b6203ca928657adf3f4cb154816260dfa9 /src/base/abci
parentcac32a32c720af661e5f30ef62a2dfc75d13da92 (diff)
downloadabc-f2abd6b8a9b59e28769662bfc6e6e6670de20faa.tar.gz
abc-f2abd6b8a9b59e28769662bfc6e6e6670de20faa.tar.bz2
abc-f2abd6b8a9b59e28769662bfc6e6e6670de20faa.zip
Preprocessing SOPs given to 'fx' to be D1C-free and SCC-free. Handling the case of non-prime SOPs.
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/abci/abcFx.c18
2 files changed, 17 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6de6a637..bd18200c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9625,8 +9625,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
if ( pNtk )
{
- extern void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose );
- Abc_NtkTestTim( pNtk, fVerbose );
+ extern void Abc_NtkMakeLegit( Abc_Ntk_t * pNtk );
+ Abc_NtkMakeLegit( pNtk );
}
return 0;
usage:
diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c
index c515afb1..953f87f3 100644
--- a/src/base/abci/abcFx.c
+++ b/src/base/abci/abcFx.c
@@ -134,12 +134,14 @@ static inline int Fx_ManGetFirstVarCube( Fx_Man_t * p, Vec_Int_t * vCube ) { ret
***********************************************************************/
Vec_Wec_t * Abc_NtkFxRetrieve( Abc_Ntk_t * pNtk )
{
+ extern int Abc_NtkMakeLegit( Abc_Ntk_t * pNtk );
Vec_Wec_t * vCubes;
Vec_Int_t * vCube;
Abc_Obj_t * pNode;
char * pCube, * pSop;
int nVars, i, v, Lit;
assert( Abc_NtkIsSopLogic(pNtk) );
+ Abc_NtkMakeLegit( pNtk );
vCubes = Vec_WecAlloc( 1000 );
Abc_NtkForEachNode( pNtk, pNode, i )
{
@@ -597,7 +599,7 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
pBeg1++, pBeg2++, Counter++;
else if ( *pBeg1 < *pBeg2 )
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
- else
+ else
{
if ( Vec_IntSize(vCubeFree) == 0 )
fAttr0 = 1, fAttr1 = 0;
@@ -608,7 +610,12 @@ int Fx_ManDivFindCubeFree( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vCu
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) );
while ( pBeg2 < pEnd2 )
Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) );
- assert( Vec_IntSize(vCubeFree) > 1 ); // the cover is not SCC-free
+ if ( Vec_IntSize(vCubeFree) == 0 )
+ printf( "The SOP has duplicated cubes.\n" );
+ else if ( Vec_IntSize(vCubeFree) == 1 )
+ printf( "The SOP has contained cubes.\n" );
+ else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) )
+ printf( "The SOP has distance-1 cubes or it is not a prime cover. Please make sure the result verifies.\n" );
assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) );
return Counter;
}
@@ -807,7 +814,7 @@ void Fx_ManCubeDoubleCubeDivisors( Fx_Man_t * p, int iFirst, Vec_Int_t * vPivot,
else if ( !fRemove )
Vec_QuePush( p->vPrio, iDiv );
}
- }
+ }
}
void Fx_ManCreateDivisors( Fx_Man_t * p )
{
@@ -936,6 +943,11 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv )
Fx_ManDivFindPivots( vDiv, &Lit0, &Lit1 );
assert( Lit0 >= 0 && Lit1 >= 0 );
+ // if the input cover is not prime, it may happen that we are extracting divisor (x + !x)
+ // although it is not strictly correct, it seems to be fine to just skip such divisors
+ if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) )
+ return;
+
// collect single-cube-divisor cubes
Vec_IntClear( p->vCubesS );
if ( Vec_IntSize(vDiv) == 2 )