bmcMaj2.c File Reference

#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"

Include dependency graph for bmcMaj2.c:

Go to the source code of this file.

Classes
struct	Maj_Man_t_
struct	Exa_Man_t_
struct	Exa3_Man_t_

Macros
#define	MAJ_NOBJS   32
	DECLARATIONS ///.

Functions
int	Maj_ManExactSynthesis2 (int nVars, int nNodes, int fUseConst, int fUseLine, int fUseRand, int nRands, int fVerbose)
int	Maj_ManExactSynthesisTest ()
void	Exa_ManExactSynthesis2 (Bmc_EsPar_t *pPars)
void	Exa3_ManExactSynthesis2 (Bmc_EsPar_t *pPars)

Macro Definition Documentation

MAJ_NOBJS

#define MAJ_NOBJS   32

DECLARATIONS ///.

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

FileName [bmcMaj2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Exact synthesis with majority gates.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 1, 2017.]

Revision [

Id

bmcMaj.c,v 1.00 2017/10/01 00:00:00 alanmi Exp

]

Definition at line 33 of file bmcMaj2.c.

Function Documentation

Exa3_ManExactSynthesis2()

void Exa3_ManExactSynthesis2

(

Bmc_EsPar_t *

pPars

)

Definition at line 1385 of file bmcMaj2.c.

{
    int i, status, iMint = 1;
    abctime clkTotal = Abc_Clock();
    Exa3_Man_t * p; int fCompl = 0;
    word pTruth[16];
    if ( pPars->pSymStr ) {
        word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
        pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
        Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
        printf( "Generated symmetric function: %s\n", pPars->pTtStr );
        ABC_FREE( pFun );
    }    
    if ( pPars->pTtStr )
        Abc_TtReadHex( pTruth, pPars->pTtStr );
    else assert( 0 );    
    assert( pPars->nVars <= 10 );
    assert( pPars->nLutSize <= 6 );
    p = Exa3_ManAlloc( pPars, pTruth );
    if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
    status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
    assert( status );
    printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
    for ( i = 0; iMint != -1; i++ )
    {
        abctime clk = Abc_Clock();
        if ( !Exa3_ManAddCnf( p, iMint ) )
            break;
        status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
        if ( pPars->fVerbose )
        {
            printf( "Iter %3d : ", i );
            Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
            printf( "  Var =%5d  ", p->iVar );
            printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
            printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
        if ( status == l_False )
        {
            printf( "The problem has no solution.\n" );
            break;
        }
        iMint = Exa3_ManEval( p );
    }
    if ( iMint == -1 )
        Exa3_ManPrintSolution( p, fCompl );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
    if ( iMint == -1 )
        Exa3_ManDumpBlif( p, fCompl );
    if ( pPars->pSymStr ) 
        ABC_FREE( pPars->pTtStr );
    Exa3_ManFree( p );
}

Here is the call graph for this function:

Exa_ManExactSynthesis2()

void Exa_ManExactSynthesis2

(

Bmc_EsPar_t *

pPars

)

Definition at line 852 of file bmcMaj2.c.

{
    int i, status, iMint = 1;
    abctime clkTotal = Abc_Clock();
    Exa_Man_t * p; int fCompl = 0;
    word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
    assert( pPars->nVars <= 10 );
    p = Exa_ManAlloc( pPars, pTruth );
    if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
    status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd );
    assert( status );
    printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes );
    for ( i = 0; iMint != -1; i++ )
    {
        abctime clk = Abc_Clock();
        if ( !Exa_ManAddCnf( p, iMint ) )
            break;
        status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
        if ( pPars->fVerbose )
        {
            printf( "Iter %3d : ", i );
            Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
            printf( "  Var =%5d  ", p->iVar );
            printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
            printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
        if ( status == l_False )
        {
            printf( "The problem has no solution.\n" );
            break;
        }
        iMint = Exa_ManEval( p );
    }
    if ( iMint == -1 )
        Exa_ManPrintSolution( p, fCompl );
    Exa_ManFree( p );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
}

Here is the call graph for this function:

Maj_ManExactSynthesis2()

int Maj_ManExactSynthesis2	(	int	nVars,
		int	nNodes,
		int	fUseConst,
		int	fUseLine,
		int	fUseRand,
		int	nRands,
		int	fVerbose )

Definition at line 462 of file bmcMaj2.c.

{
    int i, iMint = 0;
    abctime clkTotal = Abc_Clock();
    Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine, fUseRand, nRands, fVerbose );
    int status = Maj_ManAddCnfStart( p );
    assert( status );
    if ( fVerbose )
    printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
    for ( i = 0; iMint != -1; i++ )
    {
        abctime clk = Abc_Clock();
        if ( !Maj_ManAddCnf( p, iMint ) )
        {
            printf( "The problem has no solution after %2d iterations.  ", i+1 );
            break;
        }
        status = sat_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
        if ( fVerbose )
        {
            printf( "Iter %3d : ", i );
            Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
            printf( "  Var =%5d  ", p->iVar );
            printf( "Cla =%6d  ", sat_solver_nclauses(p->pSat) );
            printf( "Conf =%9d  ", sat_solver_nconflicts(p->pSat) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
        if ( status == l_False )
        {
            printf( "The problem has no solution after %2d iterations.  ", i+1 );
            break;
        }
        iMint = Maj_ManEval( p );
    }
    if ( iMint == -1 )
        Maj_ManPrintSolution( p );
    Maj_ManFree( p );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
    return iMint == -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj_ManExactSynthesisTest()

int Maj_ManExactSynthesisTest

(

)

Definition at line 503 of file bmcMaj2.c.

{
//    while ( !Maj_ManExactSynthesis2( 5, 4, 0, 0, 1, 1, 0 ) );
//    while ( !Maj_ManExactSynthesis2( 7, 7, 0, 0, 1, 2, 0 ) );
    while ( !Maj_ManExactSynthesis2( 9, 10, 0, 0, 1, 3, 0 ) );
    return 1;
}

Here is the call graph for this function: