---
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.
```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 );
```
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 );
```
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.
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
Sign in with Wallet
Connect another wallet