ntkiverify.c

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

        ppMddsExdc1 = Ntk_NetworkGlobalMddEmpty( dd, pValuesOut, nOuts );

    ppMdds2 = Ntk_NetworkGlobalMddCompute( dd, pNet2, psLeavesByName, nLeaves, psRootsByName, nRoots, pVmx );
    if ( pNet2->pNetExdc )
    {
        ppMddsExdc2 = Ntk_NetworkGlobalMddCompute( dd, pNet2->pNetExdc, psLeavesByName, nLeaves, psRootsByName, nRoots, pVmx );
        // convert the EXDC MDDs into the standard format
        ppMddsExdc2 = Ntk_NetworkGlobalMddConvertExdc( dd, pValuesOut, nOuts, ppMddsExdc2 );
    }
    else
        ppMddsExdc2 = Ntk_NetworkGlobalMddEmpty( dd, pValuesOut, nOuts );

    // check the non-determinism
    clk = clock();
    fpNet1ND = Ntk_NetworkGlobalMddCheckND( dd, pValuesOut, nOuts, ppMdds1 );
    fpNet2ND = Ntk_NetworkGlobalMddCheckND( dd, pValuesOut, nOuts, ppMdds2 );

    // report the EXDC status
    fprintf( Ntk_NetworkReadMvsisOut(pNet1), "The current  network (CUR) is %s and has%s exdc.\n", 
       (fpNet1ND?"non-deterministic":"completely specified"), (pNet1->pNetExdc?"":" no")  );
    fprintf( Ntk_NetworkReadMvsisOut(pNet1), "The external network (EXT) is %s and has%s exdc.\n", 
       (fpNet2ND?"non-deterministic":"completely specified"), (pNet2->pNetExdc?"":" no")  );

    if ( Ntk_NetworkGlobalMddCheckEquality( dd, pValuesOut, nOuts, ppMdds1, ppMdds2 ) )
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Equivalence:   CUR w/o exdc = EXT w/o exdc.\n" );
    else if ( pNet1->pNetExdc == NULL && pNet2->pNetExdc == NULL )
    {
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Non-equival:   CUR w/o exdc != EXT w/o exdc.\n" );
        if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMdds1, ppMdds2 ) )
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   CUR w/o exdc < EXT w/o exdc.\n" );
        else //if ( envi->trace )
        {
            bTrace = Ntk_NetworkGlobalMddErrorTrace( dd, pValuesOut, nOuts, ppMdds1, ppMdds2, &iOutput, &nValue );
            Cudd_Ref( bTrace );

            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Error trace:   CUR " );
            Ntk_NetworkGlobalMddPrintErrorTrace( Ntk_NetworkReadMvsisOut(pNet1), dd, pVmx, bTrace, iOutput, psRootsByName[iOutput], nValue, psLeavesByName );
            if ( !fMadeupExdc )
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in EXT" );
            else
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in EXT" );
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), ".\n" );

            Cudd_RecursiveDeref( dd, bTrace );
            fErrorTrace = 1;
        }

        if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMdds2, ppMdds1 ) )
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   EXT w/o exdc < CUR w/o exdc.\n" );
        else //if ( envi->trace )
        {
            bTrace = Ntk_NetworkGlobalMddErrorTrace( dd, pValuesOut, nOuts, ppMdds2, ppMdds1, &iOutput, &nValue );
            Cudd_Ref( bTrace );

            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Error trace:   EXT " );
            Ntk_NetworkGlobalMddPrintErrorTrace( Ntk_NetworkReadMvsisOut(pNet1), dd, pVmx, bTrace, iOutput, psRootsByName[iOutput], nValue, psLeavesByName );
            if ( !fMadeupExdc )
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in CUR" );
            else
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in CUR" );
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), ".\n" );

            Cudd_RecursiveDeref( dd, bTrace );
            fErrorTrace = 1;
        }
    }
    else
    {
        int fAnswer = 0;
        DdNode *** ppMddsSum;

        /////////////////////////////////////////////////////////////////////////////////////////////////
        // in case the first network has EXDC and the second one has no EXDC, copy it from the first network
        if ( pNet1->pNetExdc && !pNet2->pNetExdc )
        {
            ppMddsExdc2 = Ntk_NetworkGlobalMddDup( dd, pValuesOut, nOuts, ppMddsExdc1 );
            fMadeupExdc = 1;
        }
        /////////////////////////////////////////////////////////////////////////////////////////////////

        if ( pNet2->pNetExdc || fMadeupExdc )
        {
            ppMddsSum = Ntk_NetworkGlobalMddOr( dd, pValuesOut, nOuts, ppMdds2, ppMddsExdc2 );
            if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMdds1, ppMddsSum ) )
            {
                if ( !fMadeupExdc )
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   CUR w/o exdc < EXT + exdc(EXT).\n" );
                else
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   CUR w/o exdc < EXT + exdc(CUR).\n" );
                fAnswer = 1;
            }
            else //if ( envi->trace )
            {
                bTrace = Ntk_NetworkGlobalMddErrorTrace( dd, pValuesOut, nOuts, ppMdds1, ppMddsSum, &iOutput, &nValue );
                Cudd_Ref( bTrace );

                fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Error trace:   CUR " );
                Ntk_NetworkGlobalMddPrintErrorTrace( Ntk_NetworkReadMvsisOut(pNet1), dd, pVmx, bTrace, iOutput, psRootsByName[iOutput], nValue, psLeavesByName );
                if ( !fMadeupExdc )
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in EXT + exdc(EXT)" );
                else
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in EXT + exdc(CUR)" );
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), ".\n" );

                Cudd_RecursiveDeref( dd, bTrace );
                fErrorTrace = 1;
            }

            Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMddsSum );  
        }

        if ( pNet1->pNetExdc )
        {
            ppMddsSum = Ntk_NetworkGlobalMddOr( dd, pValuesOut, nOuts, ppMdds1, ppMddsExdc1 );
            if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMdds2, ppMddsSum ) )
            {
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   EXT w/o exdc < CUR + exdc(CUR).\n" );
                fAnswer = 1;
            }
            else //if ( envi->trace )
            {
                bTrace = Ntk_NetworkGlobalMddErrorTrace( dd, pValuesOut, nOuts, ppMdds2, ppMddsSum, &iOutput, &nValue );
                Cudd_Ref( bTrace );

                fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Error trace:   EXT " );
                Ntk_NetworkGlobalMddPrintErrorTrace( Ntk_NetworkReadMvsisOut(pNet1), dd, pVmx, bTrace, iOutput, psRootsByName[iOutput], nValue, psLeavesByName );
                if ( !fMadeupExdc )
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in CUR + exdc(CUR)" );
                else
                    fprintf( Ntk_NetworkReadMvsisOut(pNet1), " is not in CUR + exdc(CUR)" );
                fprintf( Ntk_NetworkReadMvsisOut(pNet1), ".\n" );

                Cudd_RecursiveDeref( dd, bTrace );
                fErrorTrace = 1;
            }

            Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMddsSum );          
        }

        if ( !fAnswer )
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Conclusion:    There is no containment between CUR and EXT.\n" );
    }

    if ( pNet1->pNetExdc && pNet2->pNetExdc && !fMadeupExdc )
    {
        if ( Ntk_NetworkGlobalMddCheckEquality( dd, pValuesOut, nOuts, ppMddsExdc1, ppMddsExdc2 ) )         
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Equivalence:   exdc(CUR) = exdc(EXT).\n" );
        else if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMddsExdc1, ppMddsExdc2 ) ) 
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   exdc(CUR) < exdc(EXT).\n" );
        else if ( Ntk_NetworkGlobalMddCheckContainment( dd, pValuesOut, nOuts, ppMddsExdc2, ppMddsExdc1 ) ) 
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Containment:   exdc(EXT) < exdc(CUR).\n" );
        else
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), "Non-equival:   exdc(CUR) != exdc(EXT).\n" );
    }
    if ( fVerbose )
    {
        PRT( "Total", clock() - clk );
    }

    // print the variable names if necessary
    if ( fErrorTrace )
    {
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "The ordering of inputs is {" );
        for ( i = 0; i < Vm_VarMapReadVarsInNum( pVm ); i++ )
            fprintf( Ntk_NetworkReadMvsisOut(pNet1), " %s", psLeavesByName[i] );
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), " }" );
        fprintf( Ntk_NetworkReadMvsisOut(pNet1), "\n" );
    }

    // dereference the global functions
    Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMdds1 );            
    Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMdds2 );            
    Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMddsExdc1 );            
    Ntk_NetworkGlobalMddDeref( dd, pValuesOut, nOuts, ppMddsExdc2 );    
    
    // remove the temporary manager
    Extra_StopManager( dd );
    // undo the names and values
    FREE( psLeavesByName );
    FREE( psRootsByName );
    FREE( pValuesOut );
}


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