如何将c代码转换为布尔表达式？

问：

我想在等效的布尔公式/表达式中导出一个简单的 c 代码。 举个例子：

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

   a=1; b=2;
   c=a+b; %ADD operator
   c=c*b;

   c=c>>1; %RSHIFT operator

   r=10;
   for(i=0;i<5;i++) { //... need to unwind the loop
      r=r+1; //r++;
   }

   return 0; 
}

第 1 阶段：循序渐进和展开循环

int main(void) {
   int I0, A0, B0, C0, R0;

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

   C2 = C1 >> 1; %RSHIFT operator

   R0=10;
   //for(i=0;i<5;i++) { //... need to unwind the loop
   //   r=r+1; //r++;
   //}
   R1=R0+1;
   R2=R1+1;
   R3=R2+1;
   R4=R3+1;
   R5=R4+1;

   return 0; 
}

第 2 阶段：“二元等价”

%int I0, A0, B0, C0, R0; //suppose int=8bits in this case (simplification)

I = [i7 i6 i5 ... i0]; %binary register
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; %ADD operator  
C0 = binADD(A0,B0); %use only logic function (example: multiple full adder XOR(XOR(...),...))

%C1 = C0 * B0;
C1 = binMULTIPLY(C0, B0); %use only logic function

%C2 = C1 >> 1; %RSHIFT operator
=> C2 = SHIFTR(C1,1);
C2_0 = C1_1;
C2_1 = C1_2;
C2_2 = C1_3;
C2_3 = C1_4;
C2_4 = C1_5;
C2_5 = C1_6;
C2_6 = C1_7;
C2_7 = 0;

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

...

最后，我想得到一个变量的表达式。

以 C 为例： C = f（A，B） = f（a7，a6,...A0，B7，B6,...b0）

假设 a 或 b 可以是介于 0 和 255 之间的值 （a=k1; b=k2;）

我看到了很多软件：CMBC、NuSMV 等。但是我找不到如何导出等效的布尔表达式（以 CNF - 二进制形式为例）。

注意：我的目标是在逻辑电路中转换这些表达式。