		Search-engine friendly clone of the ACL2 documentation.

Cblock

Cblock-expression-building

Convert a combinational always block into assignments.

Basic examples of what we're trying to do here:

always @(*)            ---->   assign lhs = condition1 ? {expr1}
   if (condition1)                        : condition2 ? {expr2}
      lhs = expr1;                        : {expr3}
   else if (condition2)
      lhs = expr2;
   else
      lhs = expr3;

always @(*)            ---->   assign lhs = condition ? {expr2} : {expr1}
   lhs = expr1;
   if (condition)
      lhs = expr2;

Note that this conversion isn't quite right if the widths of the exprs above can differ. For instance, in the merged expressions like condition ? expr2 : expr1, suppose the width of expr1 and lhs are 5, but the width of expr2 is 7. Now the width of the new, combined expression is also 7, and (because of the sizing rules) the new expression would be wider than expr1.

To avoid this, we locally use the stmttemps transform before trying to carry out this expression building. This should ensure that all lhses/rhses are well-typed and have compatible widths. The excessive use of concatenations above ensures that everything is unsigned, to avoid creating badly typed ?: expressions.

Slight twist. If we know that this is supposed to be a combinational always block because it's written with always_comb, then we allow the lhs to not be written in every branch. In this case a Verilog simulator may not trigger any update of the variable, essentially treating it like a latch. However, it seems quite likely that a synthesis tool will not infer a latch. To try to avoid making mistakes here, we want to make sure to drive the variable to Xes in this case.

To drive the variable to Xes, a simple thing to do is, e.g.,

always_comb           --->  always_comb
   if (condition)              lhs = XXXX
      lhs = expr;              if (condition)
   if (condition2)                lhs = expr;
      lhs = expr2;             if (condition2)
                                  lhs = expr2;

This is safe even if all the branches are covered (in which case we're simply setting the variable to X and then to its real value).