Вот мой Verilog заявление:Присвоить значение конкретного бита BitVecExpr в Z3
reg[2:0] a; // Create register 'a' which is 3 bit.
assign a[1] = 1'b1; // Assigning value to 1st bit of register 'a'.
Я должен реализовать заявление выше в Z3. За 1-й линии Verilog заявления с использованием BitVecExpr:
BitVecExpr a = ctx.mkBVConst("a",3);
Я проблема облицовочный при реализации 2-й линии Verilog заявления. Кто-нибудь знает, как реализовать это в Z3?
С Z3 вы не можете изменять переменные. На самом деле Z3 не называет эту переменную, она является константой.
Вам нужно создать новую константу, связанную со старой константой. Например, если вы хотите сказать, y = x + 1 это будет
var y = ctx.MkBVAdd(x, 1);
Если вы хотите сказать x = x + 1 вам нужно ввести новое имя для старого и нового x:
var x2 = ctx.MkBVAdd(x1, 1);
Я понимаю, что вы хотели сказать, но моя проблема заключается в том, что у меня есть несколько назначений для одной константы. Например: назначить [1] = 1'b1; присвойте [0] = 1'b0; назначьте [3: 2] = 2'b01; и так далее. Я думал, если есть какое-либо прямое решение для этой проблемы, например, я могу напрямую перейти и присвоить значение любому конкретному биту в Z3. Как вы думаете, мы можем это сделать? – Ajit
Назначение значений не имеет смысла. Вы просите Z3 дать вам модель для булевой формулы. Вы не можете «назначить» части формулы. Вероятно, вам нужно что-то вроде 'b = replacebits (ctx, a)' где 'replacebits' означает такие операции, как' MkExtract' или 'MkConcat'. – usr
@ChristophWintersteiger ли вам думаю, что у нас есть прямое решение этой проблемы в Z3. – Ajit