#include "bmc.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"

Include dependency graph for bmcFx.c:

Classes
struct	Tab_Obj_t_

struct	Tab_Tab_t_

Macros
#define	TAB_UNUSED 0x7FFF
	DECLARATIONS ///.

Typedefs
typedef struct Tab_Tab_t_	Tab_Tab_t

Enumerations
enum	Div_Type_t { DIV_CST = 0 , DIV_AND , DIV_XOR , DIV_MUX , DIV_NONE }

Functions
int	Div_FindDiv (Vec_Int_t vA, Vec_Int_t vB, int pLitsA[2], int pLitsB[2])

void	Div_CubePrintOne (Vec_Int_t vCube, Vec_Str_t vStr, int nVars)

void	Div_CubePrint (Vec_Wec_t *p, int nVars)

Vec_Int_t *	Div_CubePairs (Vec_Wec_t *p, int nVars, int nDivs)

int	Bmc_FxSolve (sat_solver pSat, int iOut, int iAuxVar, Vec_Int_t vVars, int fDumpPla, int fVerbose, int pCounter, Vec_Wec_t vCubes)

int	Bmc_FxCompute (Gia_Man_t *p)

void	Bmc_FxAddClauses (sat_solver pSat, Vec_Int_t vDivs, int iCiVarBeg, int iVarStart)

int	Bmc_FxComputeOne (Gia_Man_t *p, int nIterMax, int nDiv2Add)

Macro Definition Documentation

◆ TAB_UNUSED

#define TAB_UNUSED 0x7FFF

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcFx.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [INT-FX: Interpolation-based logic sharing extraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id: bmcFx.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Create hash table to hash divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file bmcFx.c.

Typedef Documentation

◆ Tab_Tab_t

typedef struct Tab_Tab_t_ Tab_Tab_t

Definition at line 60 of file bmcFx.c.

Enumeration Type Documentation

◆ Div_Type_t

enum Div_Type_t

Function*************************************************************

Synopsis [Input is four literals. Output is type, polarity and fanins.]

Description []

SideEffects []

SeeAlso []

Enumerator
DIV_CST
DIV_AND
DIV_XOR
DIV_MUX
DIV_NONE

Definition at line 167 of file bmcFx.c.

             { 
    DIV_CST = 0,   // 0: constant 1
    DIV_AND,       // 1: and (ordered fanins)
    DIV_XOR,       // 2: xor (ordered fanins)
    DIV_MUX,       // 3: mux (c, d1, d0)
    DIV_NONE       // 4: not used
} Div_Type_t; 

Function Documentation

◆ Bmc_FxAddClauses()

void Bmc_FxAddClauses	(	sat_solver *	pSat,
		Vec_Int_t *	vDivs,
		int	iCiVarBeg,
		int	iVarStart )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 645 of file bmcFx.c.

{
    int i, Func, pLits[3], nDivs = Vec_IntSize(vDivs)/4;
    assert( Vec_IntSize(vDivs) % 4 == 0 );
    // create new var for each divisor
    for ( i = 0; i < nDivs; i++ )
    {
        Func     = Vec_IntEntry(vDivs, 4*i+0);
        pLits[0] = Vec_IntEntry(vDivs, 4*i+1);
        pLits[1] = Vec_IntEntry(vDivs, 4*i+2);
        pLits[2] = Vec_IntEntry(vDivs, 4*i+3);
        //printf( "Adding clause with vars %d %d -> %d\n", iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iVarStart + nDivs - 1 - i );
        if ( Func == DIV_AND )
            sat_solver_add_and( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 
                Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), 0 );
        else if ( Func == DIV_XOR )
            sat_solver_add_xor( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), 0 );
        else if ( Func == DIV_MUX )
            sat_solver_add_mux( pSat, 
                iVarStart + nDivs - 1 - i, iCiVarBeg + Abc_Lit2Var(pLits[0]), iCiVarBeg + Abc_Lit2Var(pLits[1]), iCiVarBeg + Abc_Lit2Var(pLits[2]), 
                Abc_LitIsCompl(pLits[0]), Abc_LitIsCompl(pLits[1]), Abc_LitIsCompl(pLits[2]), 0 );
        else assert( 0 );
    }
}

Here is the caller graph for this function:

◆ Bmc_FxCompute()

int Bmc_FxCompute ( Gia_Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 593 of file bmcFx.c.

{
    // create dual-output circuit with on-set/off-set
    extern Gia_Man_t * Gia_ManDupOnsetOffset( Gia_Man_t * p );
    Gia_Man_t * p2 = Gia_ManDupOnsetOffset( p );
    // create SAT solver
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p2, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // compute parameters
    int nOuts = Gia_ManCoNum(p);
    int nCiVars = Gia_ManCiNum(p), iCiVarBeg = pCnf->nVars - nCiVars;// - 1;
    int o, i, n, RetValue, nCounter, iAuxVarStart = sat_solver_nvars( pSat );
    int nCubes[2][2] = {{0}};
    // create variables
    Vec_Int_t * vVars = Vec_IntAlloc( nCiVars );
    for ( n = 0; n < nCiVars; n++ )
        Vec_IntPush( vVars, iCiVarBeg + n );
    sat_solver_setnvars( pSat, iAuxVarStart + 4*nOuts );
    // iterate through outputs
    for ( o = 0; o < nOuts; o++ )
    for ( i = 0; i < 2; i++ )
    for ( n = 0; n < 2; n++ ) // 0=onset, 1=offset
//    for ( n = 1; n >= 0; n-- ) // 0=onset, 1=offset
    {
        printf( "Out %3d %sset ", o, n ? "off" : " on" );
        RetValue = Bmc_FxSolve( pSat, Abc_Var2Lit(o, n), iAuxVarStart + 2*i*nOuts + Abc_Var2Lit(o, n), vVars, 0, 0, &nCounter, NULL );
        if ( RetValue == 0 )
            printf( "Mismatch\n" );
        if ( RetValue == -1 )
            printf( "Timeout\n" );
        nCubes[i][n] += nCounter;
    }
    // cleanup
    Vec_IntFree( vVars );
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Gia_ManStop( p2 );
    printf( "Onset = %5d.   Offset = %5d.      Onset = %5d.   Offset = %5d.\n", nCubes[0][0], nCubes[0][1], nCubes[1][0], nCubes[1][1] );
    return 1;
}

Here is the call graph for this function:

◆ Bmc_FxComputeOne()

int Bmc_FxComputeOne	(	Gia_Man_t *	p,
		int	nIterMax,
		int	nDiv2Add )

Definition at line 671 of file bmcFx.c.

{
    int Extra    = 1000;
    // create SAT solver
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // compute parameters
    int nCiVars   = Gia_ManCiNum(p);             // PI count
    int iCiVarBeg = pCnf->nVars - nCiVars;//- 1;   // first PI var
    int iCiVarCur = iCiVarBeg + nCiVars;         // current unused PI var
    int n, Iter, RetValue;
    // create variables
    int iAuxVarStart = sat_solver_nvars(pSat) + Extra; // the aux var
    sat_solver_setnvars( pSat, iAuxVarStart + 1 + nIterMax );
    for ( Iter = 0; Iter < nIterMax; Iter++ )
    {
        Vec_Wec_t * vCubes = Vec_WecAlloc( 1000 );
        // collect variables
        Vec_Int_t * vVar2Sat = Vec_IntAlloc( iCiVarCur-iCiVarBeg ), * vDivs;
//        for ( n = iCiVarCur - 1; n >= iCiVarBeg; n-- )
        for ( n = iCiVarBeg; n < iCiVarCur; n++ )
            Vec_IntPush( vVar2Sat, n );
        // iterate through outputs
        printf( "\nIteration %d (Aux = %d)\n", Iter, iAuxVarStart + Iter );
        RetValue = Bmc_FxSolve( pSat, 0, iAuxVarStart + Iter, vVar2Sat, 1, 1, NULL, vCubes );
        if ( RetValue == 0 )
            printf( "Mismatch\n" );
        if ( RetValue == -1 )
            printf( "Timeout\n" );
        // print cubes
        //Div_CubePrint( vCubes, nCiVars );
        vDivs = Div_CubePairs( vCubes, nCiVars, nDiv2Add );
        Vec_WecFree( vCubes );
        // add clauses and update variables
        Bmc_FxAddClauses( pSat, vDivs, iCiVarBeg, iCiVarCur );
        iCiVarCur += Vec_IntSize(vDivs)/4;
        Vec_IntFree( vDivs );
        // cleanup
        assert( Vec_IntSize(vVar2Sat) <= nCiVars + Extra );
        Vec_IntFree( vVar2Sat );
    }
    // cleanup
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    return 1;
}

Here is the call graph for this function:

◆ Bmc_FxSolve()

int Bmc_FxSolve	(	sat_solver *	pSat,
		int	iOut,
		int	iAuxVar,
		Vec_Int_t *	vVars,
		int	fDumpPla,
		int	fVerbose,
		int *	pCounter,
		Vec_Wec_t *	vCubes )

Function*************************************************************

Synopsis [Solve the enumeration problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 389 of file bmcFx.c.

{
    int nBTLimit = 1000000;
    int fUseOrder = 1;
    Vec_Int_t * vLevel  = NULL;
    Vec_Int_t * vLits   = Vec_IntAlloc( Vec_IntSize(vVars) );
    Vec_Int_t * vLits2  = Vec_IntAlloc( Vec_IntSize(vVars) );
    Vec_Str_t * vCube   = Vec_StrStart( Vec_IntSize(vVars)+1 );
    int status, i, k, n, Lit, Lit2, iVar, nFinal, * pFinal, pLits[2], nIter = 0, RetValue = 0;
    int Before, After, Total = 0, nLits = 0;
    pLits[0] = Abc_Var2Lit( iOut + 1, 0 ); // F = 1
    pLits[1] = Abc_Var2Lit( iAuxVar, 0 );  // iNewLit
    if ( vCubes )
        Vec_WecClear( vCubes );
    if ( fDumpPla )
    printf( ".i %d\n", Vec_IntSize(vVars) );
    if ( fDumpPla )
    printf( ".o %d\n", 1 );
    while ( 1 ) 
    {
        // find onset minterm
        status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
        if ( status == l_Undef )
            { RetValue = -1; break; }
        if ( status == l_False )
            { RetValue = 1; break; }
        assert( status == l_True );
        // collect divisor literals
        Vec_IntClear( vLits );
        Vec_IntPush( vLits, Abc_LitNot(pLits[0]) ); // F = 0
//        Vec_IntForEachEntryReverse( vVars, iVar, i )
        Vec_IntForEachEntry( vVars, iVar, i )
            Vec_IntPush( vLits, sat_solver_var_literal(pSat, iVar) );
 
        if ( fUseOrder )
        {
            // save these literals
            Vec_IntClear( vLits2 );
            Vec_IntAppend( vLits2, vLits );
            Before = Vec_IntSize(vLits2);
 
            // try removing literals from the cube
            Vec_IntForEachEntry( vLits2, Lit2, k )
            {
                if ( Lit2 == Abc_LitNot(pLits[0]) )
                    continue;
                Vec_IntClear( vLits );
                Vec_IntForEachEntry( vLits2, Lit, n )
                    if ( Lit != -1 && Lit != Lit2 )
                        Vec_IntPush( vLits, Lit );
                // call sat
                status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
                if ( status == l_Undef )
                    assert( 0 );
                if ( status == l_True ) // SAT
                    continue;
                // Lit2 can be removed
                Vec_IntWriteEntry( vLits2, k, -1 );
            }
 
            // make one final run
            Vec_IntClear( vLits );
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    Vec_IntPush( vLits, Lit2 );
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );
 
            // get subset of literals
            nFinal = sat_solver_final( pSat, &pFinal );
        }
        else
        {
            // check against offset
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            if ( status == l_Undef )
                { RetValue = -1; break; }
            if ( status == l_True )
                break;
            assert( status == l_False );
            // get subset of literals
            nFinal = sat_solver_final( pSat, &pFinal );
            Before = nFinal;
            //printf( "Before %d. ", nFinal );
 
/*
            // save these literals
            Vec_IntClear( vLits );
            for ( i = 0; i < nFinal; i++ )
                Vec_IntPush( vLits, Abc_LitNot(pFinal[i]) );
            Vec_IntReverseOrder( vLits );
 
            // make one final run
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );
            nFinal = sat_solver_final( pSat, &pFinal );
*/
 
            // save these literals
            Vec_IntClear( vLits2 );
            for ( i = 0; i < nFinal; i++ )
                Vec_IntPush( vLits2, Abc_LitNot(pFinal[i]) );
            Vec_IntSort( vLits2, 1 );
 
            // try removing literals from the cube
            Vec_IntForEachEntry( vLits2, Lit2, k )
            {
                if ( Lit2 == Abc_LitNot(pLits[0]) )
                    continue;
                Vec_IntClear( vLits );
                Vec_IntForEachEntry( vLits2, Lit, n )
                    if ( Lit != -1 && Lit != Lit2 )
                        Vec_IntPush( vLits, Lit );
                // call sat
                status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
                if ( status == l_Undef )
                    assert( 0 );
                if ( status == l_True ) // SAT
                    continue;
                // Lit2 can be removed
                Vec_IntWriteEntry( vLits2, k, -1 );
            }
 
            // make one final run
            Vec_IntClear( vLits );
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    Vec_IntPush( vLits, Lit2 );
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
            assert( status == l_False );
 
            // put them back
            nFinal = 0;
            Vec_IntForEachEntry( vLits2, Lit2, k )
                if ( Lit2 != -1 )
                    pFinal[nFinal++] = Abc_LitNot(Lit2);        
        }
 
 
        //printf( "After %d. \n", nFinal );
        After  = nFinal;
        Total += Before - After;
 
        // get subset of literals
        //nFinal = sat_solver_final( pSat, &pFinal );
        // compute cube and add clause
        Vec_IntClear( vLits );
        Vec_IntPush( vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
        if ( fDumpPla )
            Vec_StrFill( vCube, Vec_IntSize(vVars), '-' );
        if ( vCubes )
            vLevel = Vec_WecPushLevel( vCubes );
        for ( i = 0; i < nFinal; i++ )
        {
            if ( pFinal[i] == pLits[0] )
                continue;
            Vec_IntPush( vLits, pFinal[i] );
            iVar = Vec_IntFind( vVars, Abc_Lit2Var(pFinal[i]) );   
            assert( iVar >= 0 && iVar < Vec_IntSize(vVars) );
            //printf( "%s%d ", Abc_LitIsCompl(pFinal[i]) ? "+":"-", iVar );
            if ( fDumpPla )
                Vec_StrWriteEntry( vCube, iVar, (char)(!Abc_LitIsCompl(pFinal[i]) ? '0' : '1') );
            if ( vLevel )
                Vec_IntPush( vLevel, Abc_Var2Lit(iVar, !Abc_LitIsCompl(pFinal[i])) );
        }
        if ( vCubes )
            Vec_IntSort( vLevel, 0 );
        if ( fDumpPla )
            printf( "%s 1\n", Vec_StrArray(vCube) );
        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
        assert( status );
        nLits += Vec_IntSize(vLevel);
        nIter++;
    }
    if ( fDumpPla )
    printf( ".e\n" );
    if ( fDumpPla )
    printf( ".p %d\n\n", nIter );
    if ( fVerbose )
    printf( "Cubes = %d.  Reduced = %d.  Lits = %d\n", nIter, Total, nLits );
    if ( pCounter )
        *pCounter = nIter;
//    assert( status == l_True );
    Vec_IntFree( vLits );
    Vec_IntFree( vLits2 );
    Vec_StrFree( vCube );
    return RetValue;
}

Here is the caller graph for this function:

◆ Div_CubePairs()

Vec_Int_t * Div_CubePairs	(	Vec_Wec_t *	p,
		int	nVars,
		int	nDivs )

Definition at line 325 of file bmcFx.c.

{
    int fVerbose = 0;
    char * pNames[5] = {"const1", "and", "xor", "mux", "none"};
    Vec_Int_t * vCube1, * vCube2, * vDivs; 
    int i1, i2, i, k, pLitsA[2], pLitsB[2], pLits[4], Type, Phase, nBase, Count = 0;
    Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
    Tab_Tab_t * pTab = Tab_TabAlloc( 5 );
    Vec_WecForEachLevel( p, vCube1, i )
    {
        // add lit pairs
        pLits[2] = TAB_UNUSED;
        Vec_IntForEachEntry( vCube1, pLits[0], i1 )
        Vec_IntForEachEntryStart( vCube1, pLits[1], i2, i1+1 )
        {
            Tab_TabHashAdd( pTab, pLits, DIV_AND, 1 );
        }
 
        Vec_WecForEachLevelStart( p, vCube2, k, i+1 )
        {
            nBase = Div_FindDiv( vCube1, vCube2, pLitsA, pLitsB );
            if ( nBase == -1 )
                continue;
            Type = Div_FindType(pLitsA, pLitsB, pLits, &Phase);
            if ( Type >= DIV_AND && Type <= DIV_MUX )
                Tab_TabHashAdd( pTab, pLits, Type, nBase );
 
            if ( fVerbose )
            {
                printf( "Pair %d:\n", Count++ );
                Div_CubePrintOne( vCube1, vStr, nVars );
                Div_CubePrintOne( vCube2, vStr, nVars );
                printf( "Result = %d   ", nBase );
                assert( nBase > 0 );
 
                printf( "Type = %s  ", pNames[Type] );
                printf( "LitA = %d ",  pLits[0] );
                printf( "LitB = %d ",  pLits[1] );
                printf( "LitC = %d ",  pLits[2] );
                printf( "Phase = %d ", Phase );
                printf( "\n" );
            }
        }
    }
    // print the table
    printf( "Divisors = %d.\n", pTab->nBins );
    vDivs = Tab_TabFindBest( pTab, nDivs );
    // cleanup
    Vec_StrFree( vStr );
    Tab_TabFree( pTab );
    return vDivs;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Div_CubePrint()

void Div_CubePrint	(	Vec_Wec_t *	p,
		int	nVars )

Definition at line 316 of file bmcFx.c.

{
    Vec_Int_t * vCube; int i;
    Vec_Str_t * vStr = Vec_StrStart( nVars + 1 );
    Vec_WecForEachLevel( p, vCube, i )
        Div_CubePrintOne( vCube, vStr, nVars );
    Vec_StrFree( vStr );
}

Here is the call graph for this function:

◆ Div_CubePrintOne()

void Div_CubePrintOne	(	Vec_Int_t *	vCube,
		Vec_Str_t *	vStr,
		int	nVars )

Definition at line 308 of file bmcFx.c.

{
    int i, Lit;
    Vec_StrFill( vStr, nVars, '-' );
    Vec_IntForEachEntry( vCube, Lit, i )
        Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') );
    printf( "%s\n", Vec_StrArray(vStr) );
}

Here is the caller graph for this function:

◆ Div_FindDiv()

int Div_FindDiv	(	Vec_Int_t *	vA,
		Vec_Int_t *	vB,
		int	pLitsA[2],
		int	pLitsB[2] )

Definition at line 278 of file bmcFx.c.

{
    int Counter = 0;
    int * pBegA = vA->pArray, * pEndA = vA->pArray + vA->nSize;
    int * pBegB = vB->pArray, * pEndB = vB->pArray + vB->nSize; 
    pLitsA[0] = pLitsA[1] = pLitsB[0] = pLitsB[1] = -1;
    while ( pBegA < pEndA && pBegB < pEndB )
    {
        if ( *pBegA == *pBegB )
            pBegA++, pBegB++, Counter++;
        else if ( *pBegA < *pBegB )
        {
            if ( Div_AddLit( *pBegA++, pLitsA ) )
                return -1;
        }
        else  
        {
            if ( Div_AddLit( *pBegB++, pLitsB ) )
                return -1;
        }
    }
    while ( pBegA < pEndA )
        if ( Div_AddLit( *pBegA++, pLitsA ) )
            return -1;
    while ( pBegB < pEndB )
        if ( Div_AddLit( *pBegB++, pLitsB ) )
            return -1;
    return Counter;
}

Here is the caller graph for this function:

Classes

Macros

Typedefs

Enumerations

Functions

Macro Definition Documentation

◆ TAB_UNUSED

Typedef Documentation

◆ Tab_Tab_t

Enumeration Type Documentation

◆ Div_Type_t

Function Documentation

◆ Bmc_FxAddClauses()

◆ Bmc_FxCompute()

◆ Bmc_FxComputeOne()

◆ Bmc_FxSolve()

◆ Div_CubePairs()

◆ Div_CubePrint()

◆ Div_CubePrintOne()

◆ Div_FindDiv()