From b556c2591e8dc6e35d523971aa467bce4ad6200e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 27 Feb 2014 21:11:05 -0800 Subject: Changes to LUT mappers. --- src/map/if/ifSat.c | 199 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 199 insertions(+) create mode 100644 src/map/if/ifSat.c (limited to 'src/map/if/ifSat.c') diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c new file mode 100644 index 00000000..0afe7ea5 --- /dev/null +++ b/src/map/if/ifSat.c @@ -0,0 +1,199 @@ +/**CFile**************************************************************** + + FileName [ifSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [SAT-based evaluation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" +#include "sat/bsat/satSolver.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Builds SAT instance for the given structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * If_ManSatBuildXY( int nLutSize ) +{ + int nMintsL = (1 << nLutSize); + int nMintsF = (1 << (2 * nLutSize - 1)); + int nVars = 2 * nMintsL + nMintsF; + int iVarP0 = 0; // LUT0 parameters (total nMintsL) + int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL) + int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF) + sat_solver * p = sat_solver_new(); + sat_solver_setnvars( p, nVars ); + for ( m = 0; m < nMintsF; m++ ) + sat_solver_add_mux( p, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), iVarM + m ); + return p; +} + +/**Function************************************************************* + + Synopsis [Returns config string for the given truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ) +{ + int iBSet, nBSet = 0; + int iSSet, nSSet = 0; + int iFSet, nFSet = 0; + int nMintsL = (1 << nLutSize); + int nMintsF = (1 << (2 * nLutSize - 1)); + int v, Value, m, mNew, nMintsFNew, nMintsLNew; + // collect variable sets + Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet ); + assert( nBSet + nSSet + nFSet == nVars ); + // check variable bounds + assert( nSSet + nBSet <= nLutSize ); + assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 ); + nMintsFNew = (1 << (nLutSize + nSSet + nFSet)); + // remap minterms + Vec_IntFill( vLits, nMintsF, -1 ); + for ( m = 0; m < (1 << nVars); m++ ) + { + mNew = iBSet = iSSet = iFSet = 0; + for ( v = 0; v < nVars; v++ ) + { + Value = ((uSet >> (v << 1)) & 3); + if ( Value == 0 ) // FS + { + if ( ((m >> v) & 1) ) + mNew |= 1 << (nLutSize + nSSet + iFSet); + iFSet++; + } + else if ( Value == 1 ) // BS + { + if ( ((m >> v) & 1) ) + mNew |= 1 << (nSSet + iBSet); + iBSet++; + } + else if ( Value == 3 ) // SS + { + if ( ((m >> v) & 1) ) + { + mNew |= 1 << iSSet; + mNew |= 1 << (nLutSize + iSSet); + } + iSSet++; + } + else assert( Value == 0 ); + } + assert( iBSet == nBSet && iFSet == nFSet ); + assert( Vec_IntEntry(vLits, mNew) == -1 ); + Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) ); + } + // find assumptions + v = 0; + Vec_IntForEachEntry( vLits, Value, m ) + { + printf( "%d", (Value >= 0) ? Value : 2 ); + if ( Value >= 0 ) + Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) ); + } + Vec_IntShrink( vLits, v ); + printf( " %d\n", Vec_IntSize(vLits) ); + // run SAT solver + Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + if ( Value != l_True ) + return 0; + // collect config + assert( nSSet + nBSet <= nLutSize ); + *pTBound = 0; + nMintsLNew = (1 << (nSSet + nBSet)); + for ( m = 0; m < nMintsLNew; m++ ) + if ( sat_solver_var_value(p, m) ) + Abc_TtSetBit( pTBound, m ); + *pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet ); + // collect configs + assert( nSSet + nFSet + 1 <= nLutSize ); + *pTFree = 0; + nMintsLNew = (1 << (nSSet + nFSet + 1)); + for ( m = 0; m < nMintsLNew; m++ ) + if ( sat_solver_var_value(p, nMintsL+m) ) + Abc_TtSetBit( pTFree, m ); + *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Test procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManSatTest() +{ + int nVars = 6; + int nLutSize = 4; + sat_solver * p = If_ManSatBuildXY( nLutSize ); +// char * pDsd = "(abcdefg)"; +// char * pDsd = "([a!bc]d!e)"; + char * pDsd = "0123456789ABCDEF{abcdef}"; + word * pTruth = Dau_DsdToTruth( pDsd, nVars ); + word uBound, uFree; + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); +// unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6); +// unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4); + unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6); + int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); + assert( RetValue ); + +// Abc_TtPrintBinary( pTruth, nVars ); +// Abc_TtPrintBinary( &uBound, nLutSize ); +// Abc_TtPrintBinary( &uFree, nLutSize ); + + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &uBound, nLutSize ); + Dau_DsdPrintFromTruth( &uFree, nLutSize ); + sat_solver_delete(p); + Vec_IntFree( vLits ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3