Cómo convertir código C a expresiones booleanas?

Me gustaría exportar un código C simple en ecuaciones/expresiones booleanas equivalentes.
Por ejemplo:

int main(void) {
   int i, a, b, c, r;

<p>a=1; b=2;
   c=a+b; % operador ADD
   c=c*b;</p>

<p>c=c>>1; % operador RSHIFT</p>

<p>r=10;
   for(i=0;i<5;i++) { //... necesito desenrollar el bucle
      r=r+1; //r++;
   }</p>

<p>return 0;
}
```</p>

Fase 1: paso a paso y desenrollar bucles
````
int main(void) {
   int I0, A0, B0, C0, R0;

A0=1; B0=2;
   C0=A0 + B0; % operador ADD
   C1 = C0 * B0;

C2 = C1 >> 1; % operador RSHIFT

R0=10;
   //for(i=0;i<5;i++) { //... necesito desenrollar el bucle
   //   r=r+1; //r++;
   //}
   R1=R0+1;
   R2=R1+1;
   R3=R2+1;
   R4=R3+1;
   R5=R4+1;

return 0;
}
````
Fase 2: "equivalencia binaria"

````
int I0, A0, B0, C0, R0; //supongamos int=8bits en este caso (simplificación)

I = [i7 i6 i5 ... i0]; //registro binario
A = [a7 a6 a5 ... a0];
B = [b7 b6 b5 ... b0];
C = [c7 c6 c5 ... c0];
R = [r7 r6 r5 ... r0];

%A0=1; B0=2;
A0 = [0 0 0 0 0 0 0 1]; //a0=1 
B0 = [0 0 0 0 0 0 1 0]; //b1=1

%C0=A0 + B0; % operador ADD
C0 = binADD(A0,B0); %usar solo función lógica (por ejemplo: múltiples XOR sumadores completos (XOR(XOR(...),...)))

%C1 = C0 * B0;
C1 = binMULTIPLY(C0, B0); %usar solo función lógica

%C2 = C1 >> 1; % operador RSHIFT
=> C2 = SHIFTR(C1,1);
C20 = C11;
C21 = C12;
C22 = C13;
C23 = C14;
C24 = C15;
C25 = C16;
C26 = C17;
C27 = 0;

%R0=10;
%R1=R0+1;
%R2=R1+1;
%R3=R2+1;
%R4=R3+1;
%R5=R4+1;

...

Al final, me gustaría obtener una expresión para una de mis variables.

Por ejemplo, para C:
C = f(A,B) = f(a7, a6, …, a0, b7, b6, …, b0)

Supongamos que a o b podrían ser un valor entre 0 y 255 (a=k1; b=k2;)

He visto mucho software: CMBC, NuSMV, etc. Pero no puedo encontrar cómo exportar las expresiones booleanas equivalentes (por ejemplo, en forma CNF – binaria).

Nota: mi objetivo es convertir esas expresiones en circuitos lógicos.