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

Posted 2023-03-28

【中文标题】如何将c代码转换为布尔表达式？

【英文标题】：How to convert c code to boolean expressions?

【发布时间】：2022-01-23 00:49:48

【问题描述】：

我想以等效的布尔方程/表达式导出一个简单的 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 中的示例 - 二进制形式）。

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

【问题讨论】：

boolean, CNF 好的，一些带有真/假值和逻辑运算符的公式...b=2 什么是“2”？

我希望 b 用二进制“表达”。所以，b=(10)_2 = (b1,b0) = (1,0) = (b1 2^1 + b0)。可能是 8 位或 16 位数字格式。你有软件能够做到这一点吗？我认为这种转换必须在 FPGA 软件中......

我想了解您首先要实现的目标。 CNF 中的布尔公式将有一些输入和一个真/假输出。您的程序...没有输入并且总是返回零。不，不明白。也许您应该手动进行示例转换并展示您想要得到的东西。

【参考方案1】：

您可以使用 SMT 求解器的位爆破策略来实现您想要做的一些事情。请注意，结果既不容易阅读，也不容易通过进一步的程序进行剖析。请参阅此问题/答案以获取指示：https://***.com/a/56819837/936310