sswAig.c 8.51 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    [sswAig.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [AIG manipulation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

Alan Mishchenko committed
36 37 38 39 40 41 42 43 44 45 46 47
  Synopsis    [Starts the SAT manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig )
{
    Ssw_Frm_t * p;
48
    p = ABC_ALLOC( Ssw_Frm_t, 1 );
Alan Mishchenko committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
    memset( p, 0, sizeof(Ssw_Frm_t) );
    p->pAig          = pAig;
    p->nObjs         = Aig_ManObjNumMax( pAig );
    p->nFrames       = 0;
    p->pFrames       = NULL;
    p->vAig2Frm      = Vec_PtrAlloc( 0 );
    Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
    return p;
}

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

  Synopsis    [Starts the SAT manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_FrmStop( Ssw_Frm_t * p )
{
    if ( p->pFrames )
        Aig_ManStop( p->pFrames );
    Vec_PtrFree( p->vAig2Frm );
Alan Mishchenko committed
75
    ABC_FREE( p );
Alan Mishchenko committed
76 77 78 79
}

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

Alan Mishchenko committed
80 81 82
  Synopsis    [Performs speculative reduction for one node.]

  Description []
83

Alan Mishchenko committed
84 85 86 87 88
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
89
static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame, int fTwoPos )
Alan Mishchenko committed
90
{
Alan Mishchenko committed
91
    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
Alan Mishchenko committed
92
    // skip nodes without representative
Alan Mishchenko committed
93 94
    pObjRepr = Aig_ObjRepr(pAig, pObj);
    if ( pObjRepr == NULL )
Alan Mishchenko committed
95 96 97
        return;
    p->nConstrTotal++;
    assert( pObjRepr->Id < pObj->Id );
98
    // get the new node
Alan Mishchenko committed
99
    pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
Alan Mishchenko committed
100
    // get the new node of the representative
Alan Mishchenko committed
101
    pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
Alan Mishchenko committed
102
    // if this is the same node, no need to add constraints
Alan Mishchenko committed
103 104 105 106 107 108 109 110 111 112 113 114
    if ( pObj->fPhase == pObjRepr->fPhase )
    {
        assert( pObjNew != Aig_Not(pObjReprNew) );
        if ( pObjNew == pObjReprNew )
            return;
    }
    else
    {
        assert( pObjNew != pObjReprNew );
        if ( pObjNew == Aig_Not(pObjReprNew) )
            return;
    }
Alan Mishchenko committed
115 116 117 118
    p->nConstrReduced++;
    // these are different nodes - perform speculative reduction
    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
    // set the new node
Alan Mishchenko committed
119
    Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
Alan Mishchenko committed
120
    // add the constraint
Alan Mishchenko committed
121 122
    if ( fTwoPos )
    {
123 124
        Aig_ObjCreateCo( pFrames, pObjNew2 );
        Aig_ObjCreateCo( pFrames, pObjNew );
Alan Mishchenko committed
125 126 127 128
    }
    else
    {
        pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
129
        Aig_ObjCreateCo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
Alan Mishchenko committed
130
    }
Alan Mishchenko committed
131 132 133 134 135 136 137
}

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

  Synopsis    [Prepares the inductive case with speculative reduction.]

  Description []
138

Alan Mishchenko committed
139 140 141 142 143 144 145 146 147
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
148
    int i, f, iLits;
Alan Mishchenko committed
149 150
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
151
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
Alan Mishchenko committed
152
    p->nConstrTotal = p->nConstrReduced = 0;
Alan Mishchenko committed
153 154 155 156 157

    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
158
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
Alan Mishchenko committed
159
    // add timeframes
160
    iLits = 0;
Alan Mishchenko committed
161 162
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
Alan Mishchenko committed
163
        // map constants and PIs
Alan Mishchenko committed
164
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Alan Mishchenko committed
165
        Saig_ManForEachPi( p->pAig, pObj, i )
166
        {
167
            pObjNew = Aig_ObjCreateCi(pFrames);
168 169 170
            pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
Alan Mishchenko committed
171
        // set the constraints on the latch outputs
Alan Mishchenko committed
172 173
        Saig_ManForEachLo( p->pAig, pObj, i )
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
Alan Mishchenko committed
174 175 176 177
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Alan Mishchenko committed
178
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Alan Mishchenko committed
179
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
Alan Mishchenko committed
180
        }
181
        // transfer to the primary outputs
182
        Aig_ManForEachCo( p->pAig, pObj, i )
183
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
184
        // transfer latch input to the latch outputs
Alan Mishchenko committed
185
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
186
            Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
Alan Mishchenko committed
187
    }
188
    assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
Alan Mishchenko committed
189 190
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLo( p->pAig, pObj, i )
191
        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
Alan Mishchenko committed
192 193 194 195 196

    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    // make sure the satisfying assignment is node assigned
    assert( pFrames->pData == NULL );
Alan Mishchenko committed
197
//Aig_ManShow( pFrames, 0, NULL );
Alan Mishchenko committed
198 199 200
    return pFrames;
}

Alan Mishchenko committed
201 202 203 204 205
/**Function*************************************************************

  Synopsis    [Prepares the inductive case with speculative reduction.]

  Description []
206

Alan Mishchenko committed
207 208 209 210 211 212 213 214 215 216 217 218
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
219
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
Alan Mishchenko committed
220
    p->nConstrTotal = p->nConstrReduced = 0;
221

Alan Mishchenko committed
222 223
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
224
    pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
Alan Mishchenko committed
225 226 227
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
228
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
Alan Mishchenko committed
229 230
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
231
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
Alan Mishchenko committed
232 233 234 235 236 237 238 239 240 241 242 243
    // set the constraints on the latch outputs
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    // add internal nodes of this frame
    Aig_ManForEachNode( p->pAig, pObj, i )
    {
        pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    }
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLi( p->pAig, pObj, i )
244
        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
Alan Mishchenko committed
245 246 247
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
248
//    Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", 
Alan Mishchenko committed
249
//        p->nConstrTotal, p->nConstrReduced );
Alan Mishchenko committed
250 251 252
    return pFrames;
}

Alan Mishchenko committed
253 254 255 256 257
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


258
ABC_NAMESPACE_IMPL_END