Constrains on specific bits in integer

Question

I want to gen b (uint) with the following constrain: If a has zero in specific bit I want be to have zero in the same bit.

I tried this:

!a , !b : uint(bits:4);
gen a; gen b;
for i from 0 to 3 {
  keep read_only(a[i:i] == 0) => b[i:i] == 0;
}:

I got this error:gen action "Constraint does not contain any generative element"

Answer 1

are a and b really generated on the fly, in different "gen" action? if they are generated together, you can try something like this -

   a  : uint(bits:4);
b  : uint(bits:4);

all_bits : list of int;
keep all_bits == {0; 1; 2; 3};
keep for each (i) in all_bits  {
    read_only(a[i:i] == 0) => b[i:i] == 0;
};