From f8b1be8bbf588fb6e0f6362a79c56283ab11858f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Mar 2020 19:01:45 -0700 Subject: Extending TT-based ISOP to handle ISFs. --- src/bool/kit/kit.h | 2 ++ src/bool/kit/kitGraph.c | 28 ++++++++++++++++++++ src/bool/kit/kitHop.c | 24 +++++++++++++++++ src/bool/kit/kitIsop.c | 70 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 124 insertions(+) diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h index 15b27fad..6889aa32 100644 --- a/src/bool/kit/kit.h +++ b/src/bool/kit/kit.h @@ -566,6 +566,7 @@ extern Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEd extern Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type ); extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ); extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); +extern Kit_Graph_t * Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ); extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf ); /*=== kitHop.c ==========================================================*/ //extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); @@ -574,6 +575,7 @@ extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t //extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory ); /*=== kitIsop.c ==========================================================*/ extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); +extern int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth ); extern void Kit_TruthIsopPrint( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); extern void Kit_TruthIsopPrintCover( Vec_Int_t * vCover, int nVars, int fCompl ); /*=== kitPla.c ==========================================================*/ diff --git a/src/bool/kit/kitGraph.c b/src/bool/kit/kitGraph.c index 08dabc7e..2ee135e2 100644 --- a/src/bool/kit/kitGraph.c +++ b/src/bool/kit/kitGraph.c @@ -369,6 +369,34 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor return pGraph; } +/**Function************************************************************* + + Synopsis [Derives the factored form from the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Kit_Graph_t * Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory ) +{ + Kit_Graph_t * pGraph; + int RetValue; + // derive SOP + RetValue = Kit_TruthIsop2( pTruth0, pTruth1, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode" + if ( RetValue == -1 ) + return NULL; + if ( Vec_IntSize(vMemory) > (1<<16) ) + return NULL; +// printf( "Isop size = %d.\n", Vec_IntSize(vMemory) ); + assert( RetValue == 0 || RetValue == 1 ); + // derive factored form + pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory ); + return pGraph; +} + /**Function************************************************************* Synopsis [Derives the maximum depth from the leaf to the root.] diff --git a/src/bool/kit/kitHop.c b/src/bool/kit/kitHop.c index a159a05a..4ac82ac9 100644 --- a/src/bool/kit/kitHop.c +++ b/src/bool/kit/kitHop.c @@ -100,6 +100,30 @@ int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * Kit_GraphFree( pGraph ); return iLit; } +int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ) +{ + int iLit; + Kit_Graph_t * pGraph; + // transform truth table into the decomposition tree + if ( vMemory == NULL ) + { + vMemory = Vec_IntAlloc( 0 ); + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + Vec_IntFree( vMemory ); + } + else + pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory ); + if ( pGraph == NULL ) + { + printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" ); + Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" ); + Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" ); + } + // derive the AIG for the decomposition tree + iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash ); + Kit_GraphFree( pGraph ); + return iLit; +} /**Function************************************************************* diff --git a/src/bool/kit/kitIsop.c b/src/bool/kit/kitIsop.c index 506da2e5..828ef1de 100644 --- a/src/bool/kit/kitIsop.c +++ b/src/bool/kit/kitIsop.c @@ -38,6 +38,76 @@ static unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, K /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Computes ISOP from TT.] + + Description [Returns the cover in vMemory. Uses the rest of array in vMemory + as an intermediate memory storage. Returns the cover with -1 cubes, if the + the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of + intermediate data).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_TruthIsop2( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth ) +{ + Kit_Sop_t cRes, * pcRes = &cRes; + Kit_Sop_t cRes2, * pcRes2 = &cRes2; + unsigned * pResult; + int RetValue = 0; + assert( nVars >= 0 && nVars <= 16 ); + // prepare memory manager + Vec_IntClear( vMemory ); + Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT ); + // compute ISOP for the direct polarity + Kit_TruthNot( puTruth0, puTruth0, nVars ); + pResult = Kit_TruthIsop_rec( puTruth1, puTruth0, nVars, pcRes, vMemory ); + Kit_TruthNot( puTruth0, puTruth0, nVars ); + if ( pcRes->nCubes == -1 ) + { + vMemory->nSize = -1; + return -1; + } + assert( Kit_TruthIsImply( puTruth1, pResult, nVars ) ); + Kit_TruthNot( puTruth0, puTruth0, nVars ); + assert( Kit_TruthIsImply( pResult, puTruth0, nVars ) ); + Kit_TruthNot( puTruth0, puTruth0, nVars ); + if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) ) + { + vMemory->pArray[0] = 0; + Vec_IntShrink( vMemory, pcRes->nCubes ); + return 0; + } + if ( fTryBoth ) + { + // compute ISOP for the complemented polarity + Kit_TruthNot( puTruth1, puTruth1, nVars ); + pResult = Kit_TruthIsop_rec( puTruth0, puTruth1, nVars, pcRes2, vMemory ); + Kit_TruthNot( puTruth1, puTruth1, nVars ); + if ( pcRes2->nCubes >= 0 ) + { + assert( Kit_TruthIsImply( puTruth0, pResult, nVars ) ); + Kit_TruthNot( puTruth1, puTruth1, nVars ); + assert( Kit_TruthIsImply( pResult, puTruth1, nVars ) ); + Kit_TruthNot( puTruth1, puTruth1, nVars ); + if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) ) + { + RetValue = 1; + pcRes = pcRes2; + } + } + } +// printf( "%d ", vMemory->nSize ); + // move the cover representation to the beginning of the memory buffer + memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) ); + Vec_IntShrink( vMemory, pcRes->nCubes ); + return RetValue; +} + + /**Function************************************************************* Synopsis [Computes ISOP from TT.] -- cgit v1.2.3