bbrCex.c 5.72 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [bbrCex.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD-based reachability analysis.]

  Synopsis    [Procedures to derive a satisfiable counter-example.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: bbrCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "bbr.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
30 31
extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );

Alan Mishchenko committed
32 33 34 35 36 37
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

Alan Mishchenko committed
38
  Synopsis    [Derives the counter-example using the set of reached states.]
Alan Mishchenko committed
39 40 41 42 43 44 45 46

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
47
Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
Alan Mishchenko committed
48 49
    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
    int iOutput, int fVerbose, int fSilent )
Alan Mishchenko committed
50
{
51
    Abc_Cex_t * pCex;
Alan Mishchenko committed
52
    Aig_Obj_t * pObj;
Alan Mishchenko committed
53 54 55 56
    Bbr_ImageTree_t * pTree;
    DdNode * bCubeNs, * bState, * bImage;
    DdNode * bTemp, * bVar, * bRing;
    int i, v, RetValue, nPiOffset;
Alan Mishchenko committed
57
    char * pValues;
58
    abctime clk = Abc_Clock();
Alan Mishchenko committed
59
//printf( "\nDeriving counter-example.\n" );
Alan Mishchenko committed
60 61

    // allocate room for the counter-example
62
    pCex = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
Alan Mishchenko committed
63 64 65 66 67 68
    pCex->iFrame = Vec_PtrSize(vOnionRings);
    pCex->iPo = iOutput;
    nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);

    // create the cube of NS variables
    bCubeNs  = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) );    Cudd_Ref( bCubeNs );
Alan Mishchenko committed
69
    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose );
Alan Mishchenko committed
70 71 72 73 74 75 76
    Cudd_RecursiveDeref( dd, bCubeNs );
    if ( pTree == NULL )
    {
        if ( !fSilent )
            printf( "BDDs blew up during qualitification scheduling.  " );
        return NULL;
    }
Alan Mishchenko committed
77 78

    // allocate room for the cube
Alan Mishchenko committed
79
    pValues = ABC_ALLOC( char, dd->size );
Alan Mishchenko committed
80

Alan Mishchenko committed
81 82 83
    // get the last cube
    RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues );
    assert( RetValue );
Alan Mishchenko committed
84

Alan Mishchenko committed
85 86 87
    // write PIs of counter-example
    Saig_ManForEachPi( p, pObj, i )
        if ( pValues[i] == 1 )
88
            Abc_InfoSetBit( pCex->pData, nPiOffset + i );
Alan Mishchenko committed
89
    nPiOffset -= Saig_ManPiNum(p);
Alan Mishchenko committed
90

Alan Mishchenko committed
91 92 93
    // write state in terms of NS variables
    bState = (dd)->one; Cudd_Ref( bState );
    Saig_ManForEachLo( p, pObj, i )
Alan Mishchenko committed
94
    {
Alan Mishchenko committed
95 96 97
        bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
        bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
        Cudd_RecursiveDeref( dd, bTemp ); 
Alan Mishchenko committed
98 99
    }

Alan Mishchenko committed
100
    // perform backward analysis
101
    Vec_PtrForEachEntryReverse( DdNode *, vOnionRings, bRing, v )
Alan Mishchenko committed
102 103
    { 
        // compute the next states
Alan Mishchenko committed
104
        bImage = Bbr_bddImageCompute( pTree, bState );           
Alan Mishchenko committed
105 106
        if ( bImage == NULL )
        {
Alan Mishchenko committed
107
            Cudd_RecursiveDeref( dd, bState );
Alan Mishchenko committed
108 109 110
            if ( !fSilent )
                printf( "BDDs blew up during image computation.  " );
            Bbr_bddImageTreeDelete( pTree );
Alan Mishchenko committed
111
            ABC_FREE( pValues );
Alan Mishchenko committed
112
            return NULL;
Alan Mishchenko committed
113 114
        }
        Cudd_Ref( bImage );
Alan Mishchenko committed
115
        Cudd_RecursiveDeref( dd, bState );
Alan Mishchenko committed
116 117

        // intersect with the previous set
Alan Mishchenko committed
118 119
        bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing );  Cudd_Ref( bImage );
        Cudd_RecursiveDeref( dd, bTemp );
Alan Mishchenko committed
120 121 122

        // find any assignment of the BDD
        RetValue = Cudd_bddPickOneCube( dd, bImage, pValues );
Alan Mishchenko committed
123 124
        assert( RetValue );
        Cudd_RecursiveDeref( dd, bImage );
Alan Mishchenko committed
125

Alan Mishchenko committed
126 127 128
        // write PIs of counter-example
        Saig_ManForEachPi( p, pObj, i )
            if ( pValues[i] == 1 )
129
                Abc_InfoSetBit( pCex->pData, nPiOffset + i );
Alan Mishchenko committed
130
        nPiOffset -= Saig_ManPiNum(p);
Alan Mishchenko committed
131

Alan Mishchenko committed
132 133 134 135 136
        // check that we get the init state
        if ( v == 0 )
        {
            Saig_ManForEachLo( p, pObj, i )
                assert( pValues[Saig_ManPiNum(p)+i] == 0 );
Alan Mishchenko committed
137
            break;
Alan Mishchenko committed
138 139 140 141 142
        }

        // write state in terms of NS variables
        bState = (dd)->one; Cudd_Ref( bState );
        Saig_ManForEachLo( p, pObj, i )
Alan Mishchenko committed
143
        {
Alan Mishchenko committed
144 145 146
            bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
            bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
            Cudd_RecursiveDeref( dd, bTemp ); 
Alan Mishchenko committed
147
        }
Alan Mishchenko committed
148 149 150
    }
    // cleanup
    Bbr_bddImageTreeDelete( pTree );
Alan Mishchenko committed
151
    ABC_FREE( pValues );
Alan Mishchenko committed
152 153 154
    // verify the counter example
    if ( Vec_PtrSize(vOnionRings) < 1000 )
    {
155
    RetValue = Saig_ManVerifyCex( p, pCex );
Alan Mishchenko committed
156 157 158 159 160
    if ( RetValue == 0 && !fSilent )
        printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
    }
    if ( fVerbose && !fSilent )
    {
161
    ABC_PRT( "Counter-example generation time", Abc_Clock() - clk );
Alan Mishchenko committed
162 163
    }
    return pCex;
Alan Mishchenko committed
164 165 166 167 168 169 170
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


171 172
ABC_NAMESPACE_IMPL_END