ntkiverify.c

主要进行大规模的电路综合

/**CFile****************************************************************

  FileName    [ntkiVerify.c]

  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

  Synopsis    [Network verification procedures.]

  Author      [MVSIS Group]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: ntkiVerify.c,v 1.3 2003/05/27 23:14:35 alanmi Exp $]

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

#include "ntkiInt.h"

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

static int  Ntk_NetworkVerifyVariables( Ntk_Network_t * pNet1, Ntk_Network_t * pNet2, int fVerbose );
static void Ntk_NetworkVerifyFunctions( Ntk_Network_t * pNet1, Ntk_Network_t * pNet2, int fVerbose );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFITIONS                           ///
////////////////////////////////////////////////////////////////////////
    
/**Function*************************************************************

  Synopsis    [The top level verification procedure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NetworkVerify( Ntk_Network_t * pNet1, Ntk_Network_t * pNet2, int fVerbose )
{
    // verify the identity of network CI/COs
    if ( !Ntk_NetworkVerifyVariables( pNet1, pNet2, fVerbose ) )
        return;

    // verify the functionality
    Ntk_NetworkVerifyFunctions( pNet1, pNet2, fVerbose );
}


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

  Synopsis    [Verifies the CIs/COs of the network.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ntk_NetworkVerifyVariables( Ntk_Network_t * pNet1, Ntk_Network_t * pNet2, int fVerbose )
{
    Ntk_Node_t * pNode1, * pNode2;

    // make sure that networks have the same number of inputs/outputs/latches
    if ( Ntk_NetworkReadCiNum(pNet1) != Ntk_NetworkReadCiNum(pNet2) )
    {
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Networks have different number of PIs. Verification is not performed.\n" );
        return 0;
    }
    if ( Ntk_NetworkReadCoNum(pNet1) != Ntk_NetworkReadCoNum(pNet2) )
    {
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Networks have different number of POs. Verification is not performed.\n" );
        return 0;
    }
    if ( Ntk_NetworkReadLatchNum(pNet1) != Ntk_NetworkReadLatchNum(pNet2) )
    {
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Networks have different number of latches. Verification is not performed.\n" );
        return 0;
    }

    // make sure that the names of the inputs/outputs/latches are matching
    Ntk_NetworkForEachCi( pNet1, pNode1 )
    {
        pNode2 = Ntk_NetworkFindNodeByName( pNet2, pNode1->pName );
        if ( pNode2 == NULL )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "<%s> is a CI of the first network but not of the second. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
        if ( pNode1->nValues != pNode2->nValues )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "CI <%s> has different number of values in the networks. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
    }
    Ntk_NetworkForEachCo( pNet1, pNode1 )
    {
        pNode2 = Ntk_NetworkFindNodeByName( pNet2, pNode1->pName );
        if ( pNode2 == NULL )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "<%s> is a CO of the first network but not of the second. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
        if ( pNode1->nValues != pNode2->nValues )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "CO <%s> has different number of values in the networks. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
    }

    Ntk_NetworkForEachCi( pNet2, pNode1 )
    {
        if ( Ntk_NetworkFindNodeByName( pNet1, pNode1->pName ) == NULL )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "<%s> is a PI of the second network but not of the first. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
    }
    Ntk_NetworkForEachCo( pNet2, pNode1 )
    {
        if ( Ntk_NetworkFindNodeByName( pNet1, pNode1->pName ) == NULL )
        {
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "<%s> is a PO of the second network but not of the first. Verification is not performed.\n", pNode1->pName );
            return 0;
        }
    }
    return 1;
}

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

  Synopsis    [Verifies the functionality of the networks.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ntk_NetworkVerifyFunctions( Ntk_Network_t * pNet1, Ntk_Network_t * pNet2, int fVerbose )
{
    DdManager * dd;
    char ** psLeavesByName, ** psRootsByName;
    Vmx_VarMap_t * pVmx;
    Vm_VarMap_t * pVm;
    DdNode *** ppMdds1, *** ppMddsExdc1;
    DdNode *** ppMdds2, *** ppMddsExdc2;
    int nLeaves, nRoots;
    int * pValuesOut;
    int fpNet1ND, fpNet2ND;
    int fMadeupExdc = 0;
    int nOuts, clk, i;
    DdNode * bTrace;
    int iOutput, nValue;
    bool fErrorTrace = 0;

    // get the CI variable order
    psLeavesByName = Ntk_NetworkOrderArrayByName( pNet1, 0 );
    // collect the output names and values
    psRootsByName = Ntk_NetworkGlobalGetOutputsAndValues( pNet1, &pValuesOut );
    // get the variable map
    pVmx = Ntk_NetworkGlobalGetVmx( pNet1, psLeavesByName );
    pVm  = Vmx_VarMapReadVm( pVmx );
    // get the number of outputs 
    nOuts = Ntk_NetworkReadCoNum( pNet1 );
    // collect the output values

    // start the manager, in which the global MDDs will be stored
    dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );

    // compute the MDDs of both networks
    nLeaves = Ntk_NetworkReadCiNum(pNet1);
    nRoots  = Ntk_NetworkReadCoNum(pNet1);
    ppMdds1 = Ntk_NetworkGlobalMddCompute( dd, pNet1, psLeavesByName, nLeaves, psRootsByName, nRoots, pVmx );
    if ( pNet1->pNetExdc )
    {
        ppMddsExdc1 = Ntk_NetworkGlobalMddCompute( dd, pNet1->pNetExdc, psLeavesByName, nLeaves, psRootsByName, nRoots, pVmx );
        // convert the EXDC MDDs into the standard format
        ppMddsExdc1 = Ntk_NetworkGlobalMddConvertExdc( dd, pValuesOut, nOuts, ppMddsExdc1 );
    }
    else