---
# System prepended metadata

title: Compute sdc and odc by ABC
tags: [Documentation, Templates]

---

---
title: 'Compute sdc and odc by ABC'
disqus: hackmd
---

Compute sdc and odc by ABC
===

## Prerequisite knowledge
### 1. Get cone from current network
Here is a one bit adder. I took this as an original network.
![Screenshot 2024-11-18 at 11.41.21 am](https://hackmd.io/_uploads/BJXdw4_zJx.png)

```cpp=
Abc_NtkCreateCone(*pNtk,*pNode,*pNodeName,fUseAllCis )
```
The API will get specific node as output and exctrac cone from pNtk;

parameter

1. pNtk      => Network that you want to extract from.
2. pNode     => Node in network that you want to extract from.
3. pNodeName => Node name that you assigned. If you want to keep the same name. Just use 
```cpp=
Abc_ObjName(pNodeName)
```
4. fUseAllCis=> If this parameter is 1, all pirmary inputs (e.g. a, b, c in above figure) will be included.



:::danger
When using Abc_NtkCreateCone. The node id will be totally different from original network.
The network will be slightly different.
:::
Here are two examples.
Using the function to get cone from original network.(The variable declareation and some detail are neglect in following code)
:::warning
Set the last parameter to 1 to make all PIs are included.
:::
```cpp=
pObj = Abc_NtkFindNode( pNtk,"n16");
sub_ntk =  Abc_NtkCreateCone( pNtk, pObj, Abc_ObjName(pObj), 1 );
```
![Screenshot 2024-11-18 at 5.18.40 pm](https://hackmd.io/_uploads/HyX6IFdzJe.png)
Cone network structure of node 16 are the same as original network.


---
```cpp=
pObj = Abc_NtkFindNode( pNtk,"n11");
sub_ntk =  Abc_NtkCreateCone( pNtk, pObj, Abc_ObjName(pObj), 1 );
```
![Screenshot 2024-11-18 at 5.18.30 pm](https://hackmd.io/_uploads/BkhOwFOMJe.png)

Cone network structure of node n11 is slightly different but function is equivalent to original network respect to node 11. 

>[!Note]
You can notice that the network consists of of node a, node b, node 6, node 5 in cone network and in original netwotk are different.




### 2. Derive CNF from circuit
#### There are some steps.
*  Convert network to CNF.
* Find relationship bewteen Lit ID and Obj ID(Since these two ID are different).
* Decode literal in clause.

#### Convert network to CNF.
```cpp=
Cnf_Dat_t *pCnf_fanin0 = Cnf_Derive(pAig_man_fanin0, Aig_ManCoNum(pAig_man_fanin0));
```
:::danger
Not all node will be converted into cnf.
:::
####  Find relationship bewteen Lit ID and Obj ID.


Using the function following to get relationship bewteen Obj ID and Literal ID
```cpp=
 Abc_NtkForEachObj(pObj_Ntk, pIteObj, k){
    int lit_id = pCnf_obj->pVarNums[Abc_ObjId(pIteObj)];
    if (Abc_ObjIsPi(pIteObj))
        printf("\tPI  node ID:%d  name:%5s lit id:%d\n", Abc_ObjId(pIteObj), Abc_ObjName(pIteObj),lit_id);
    else if (Abc_ObjIsPo(pIteObj))
        printf("\tPO  node ID:%d  name:%5s lit id:%d\n", Abc_ObjId(pIteObj), Abc_ObjName(pIteObj),lit_id);
    else
        printf("\tABC node ID:%d  name:%5s lit id:%d\n", Abc_ObjId(pIteObj), Abc_ObjName(pIteObj),lit_id);
     
 }
```
:::danger
Please note that the clause id is NOT the same as the node id in aig.
:::
The result will like this. 
```
	ABC node ID:0  name:   n0 lit id:7
	PI  node ID:1  name:    a lit id:4
	PI  node ID:2  name:    b lit id:5
	PI  node ID:3  name:  cin lit id:6
	PO  node ID:4  name:  n11 lit id:-1
	ABC node ID:5  name:   n5 lit id:-1
	ABC node ID:6  name:   n6 lit id:3
	ABC node ID:7  name:   n7 lit id:-1
	ABC node ID:8  name:   n8 lit id:-1
	ABC node ID:9  name:   n9 lit id:2
	ABC node ID:10  name:  n10 lit id:1
```
:::warning
Lit ID is -1 means the node is deprecated in CNF.
:::
Lit is abbrivation of literal. You can obersve that there are some node have -1 lit id. It means this node won't be use in CNF expression.

Red nodes are removing in CNF formular. Green nodes are used nodes of network.
![a11](https://hackmd.io/_uploads/SJxmt3YMJg.png)






For example, the cnf formular of n11 cone network will look like this.
```cpp=
    for (int i = 0; i < pCnf_obj->nClauses; ++i)
    {
      int *pClause = pCnf_obj->pClauses[i];
      while (pClause < pCnf_obj->pClauses[i + 1])
      {
        int lit_id_index = *pClause;
        printf("%d ",lit_id_index);        
        *pClause++;
      }
      printf("\n");
    }
```
```
4 6 10
4 8 10
4 6 8
5 7 9
5 9 11
5 7 11
12
2 5
3 4
```
The literals in clauses were encoded based on the rules.
:::info
A positive literal of a variable is the double of it. A negative literal is a positive literal plus one
e.g. the ID of last clause is (3 4) it means the literal id correspond to clause is (-1 2)
:::
We can insert these code into previous for loop to get decoded literals. 
```cpp=
int lit_id = lit_id_index>>1 ;
printf("%c%3d ",(lit_id_index&1)?'!':' ' ,lit_id);
```


So after decoding we can get intuitive clauses.

```
2 3 5
2 4 5
2 3 4
!2 !3 !4
!2 !4 !5
!2 !3 !5
6
1 !2
!1 2
```
---
### 3. Add clause into CNF formular
> [!IMPORTANT]
> I met a problem here about sat_addclause()

:::spoiler source code of sat_addclause
```cpp=
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
    lit *i,*j;
    int maxvar;
    lit last;
    assert( begin < end );
    if ( s->fPrintClause )
    {
        for ( i = begin; i < end; i++ )
            printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
        printf( "\n" );
    }

    veci_resize( &s->temp_clause, 0 );
    for ( i = begin; i < end; i++ )
        veci_push( &s->temp_clause, *i );
    begin = veci_begin( &s->temp_clause );
    end = begin + veci_size( &s->temp_clause );

    // insertion sort
    maxvar = lit_var(*begin);
    for (i = begin + 1; i < end; i++){
        lit l = *i;
        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
        for (j = i; j > begin && *(j-1) > l; j--)
            *j = *(j-1);
        *j = l;
    }
    sat_solver_setnvars(s,maxvar+1);

    ///////////////////////////////////
    // add clause to internal storage
    if ( s->pStore )
    {
        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
        assert( RetValue );
        (void) RetValue;
    }
    ///////////////////////////////////

    // delete duplicates
    last = lit_Undef;
    for (i = j = begin; i < end; i++){
        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
            return true;   // tautology
        else if (*i != last && var_value(s, lit_var(*i)) == varX)
            last = *j++ = *i;
    }
//    j = i;

    if (j == begin)          // empty clause
        return false;

    if (j - begin == 1) // unit clause
        return sat_solver_enqueue(s,*begin,0);

    // create new clause
    sat_solver_clause_new(s,begin,j,0);
    return true;
}
```
:::

:::danger
When got 0 as return value from sat_addclause(). It means add clause it conflict to original clauses.
:::


>[!Note]
Select and node 
Simulation with random patten
Check which conditions doesn't appear
Construct 





