summaryrefslogtreecommitdiffstats
path: root/src/sat/aig/aigCheck.c
blob: a9facef34264a6821a44d49aaae796027c3090b1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
/**CFile****************************************************************

  FileName    [aigCheck.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [And-Inverter Graph package.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "aig.h"

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

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

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

  Synopsis    [Makes sure that every node in the table is in the network and vice versa.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Aig_ManCheck( Aig_Man_t * pMan )
{
    Aig_Node_t * pObj, * pAnd;
    int i;
    Aig_ManForEachNode( pMan, pObj, i )
    {
        if ( pObj == pMan->pConst1 || Aig_NodeIsPi(pObj) )
        {
            if ( pObj->Fans[0].iNode || pObj->Fans[1].iNode || pObj->Level )
            {
                printf( "Aig_ManCheck: The AIG has non-standard constant or PI node \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Aig_NodeIsPo(pObj) )
        {
            if ( pObj->Fans[1].iNode )
            {
                printf( "Aig_ManCheck: The AIG has non-standard PO node \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        // consider the AND node
        if ( !pObj->Fans[0].iNode || !pObj->Fans[1].iNode )
        {
            printf( "Aig_ManCheck: The AIG has node \"%d\" with a constant fanin.\n", pObj->Id );
            return 0;
        }
        if ( pObj->Fans[0].iNode > pObj->Fans[1].iNode )
        {
            printf( "Aig_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
            return 0;
        }
        if ( pObj->Level != 1 + AIG_MAX(Aig_NodeFanin0(pObj)->Level, Aig_NodeFanin1(pObj)->Level) )
            printf( "Aig_ManCheck: Node \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
        pAnd = Aig_TableLookupNode( pMan, Aig_NodeChild0(pObj), Aig_NodeChild1(pObj) );
        if ( pAnd != pObj )
            printf( "Aig_ManCheck: Node \"%d\" is not in the structural hashing table.\n", pObj->Id );
    }
    // count the number of nodes in the table
    if ( Aig_TableNumNodes(pMan->pTable) != Aig_ManAndNum(pMan) )
    {
        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
        return 0;
    }
    return 1;
}

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

  Synopsis    [Check if the node has a combination loop of depth 1 or 2.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot )
{
    Aig_Node_t * pFanin0, * pFanin1;
    Aig_Node_t * pChild00, * pChild01;
    Aig_Node_t * pChild10, * pChild11;
    if ( !Aig_NodeIsAnd(pNode) )
        return 1;
    pFanin0 = Aig_NodeFanin0(pNode);
    pFanin1 = Aig_NodeFanin1(pNode);
    if ( pRoot == pFanin0 || pRoot == pFanin1 )
        return 0;
    if ( Aig_NodeIsPi(pFanin0) )
    {
        pChild00 = NULL;
        pChild01 = NULL;
    }
    else
    {
        pChild00 = Aig_NodeFanin0(pFanin0);
        pChild01 = Aig_NodeFanin1(pFanin0);
        if ( pRoot == pChild00 || pRoot == pChild01 )
            return 0;
    }
    if ( Aig_NodeIsPi(pFanin1) )
    {
        pChild10 = NULL;
        pChild11 = NULL;
    }
    else
    {
        pChild10 = Aig_NodeFanin0(pFanin1);
        pChild11 = Aig_NodeFanin1(pFanin1);
        if ( pRoot == pChild10 || pRoot == pChild11 )
            return 0;
    }
    return 1;
}


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