Add Value.match(...), an operator with the same semantics as Case(...)

[RobertBaruch]

I'd very much like to use the standard ? for don't-care bits:

  with m.If(x == "0b111???00_01101???"):
    ...

  ...
  with m.Case("0b111???00_01101???"):
    ...

Apparently Verilog supports this directly in casez, but not in equality comparisons -- at least not in a compatible way. There's inside, but I doubt yosys supports that. Such an equality statement could just be translated to something like:

  with m.If( (x & 0b1110000001101000) == 0b1110000001101000):
    ...

[whitequark]

You can use this in Case:

with m.Case("111???0001101???"):

I don't think adding support for don't cares to == is pulling its weight in added complexity. I certainly would like to see some very good justification for why this should be a language feature--even the don't cares in Case were added on a tentative basis, although by now they've seen enough use that they're here to stay. One significant problem with adding don't cares for == is sign extension rules, which does not come up for Case because specifying a bit string literal for Case requires that the width of this literal be exactly identical to the width of the matched signal.

[RobertBaruch]

I used don't-cares in equality extensively in my formal verification for instructions. For example:

wire [1:0] ss          = z80fi_insn[13:12];
wire       iy          = z80fi_insn[5];

assign spec_valid = z80fi_valid &&
    z80fi_insn_len == 2 &&
    z80fi_insn[15:0] == 16'b00??1001_11?11101;

This is a fragment in a module which yields expected results for the instruction matching this pattern. It's possible that this is only supported by yosys. I know that it is not supported by Icarus Verilog (not even in case).

[whitequark]

Yes, but that's a single use case and it's in (nonstandard) Verilog. In my CPU, I took advantage of Python's abstraction features to avoid tying together the semantics of an instruction pattern (which bits are set) and the implementation of it (which nMigen code matches it). This is why I'm asking "why should don't cares in == be an nMigen language feature specifically?": it is not even clear that this is a good solution for the specific problem you're facing.

Let me explain why I am so hesitant to add it. Right now, nMigen uses pure 2-value logic: every bit is either 0 or 1. This has the advantage of being very simple: not only are all language features fully deterministic, but also any literal and any computed value are representable with Python int.

With your suggestion, I would have to add, at the minimum, two language aspects.

First, it would be necessary to make Python str coerce to nMigen Value. This certainly adds opportunity for programmer error, and makes the behavior much less orthogonal; for example, right now, Value.wrap(1) + Value.wrap(1), 1 + 1, and Value.wrap(1) + 1 all have the same semantics, but with this change, Value.wrap("1") + 1 would not work the same way as "1" + 1, for obvious reasons. Similarly, the semantics of Value.wrap("?") + 1 differs from Value.wrap("1") + 1, with the former being an error but the latter not. The complexity here is considerable, and testing every permutation is hard.

Second, everything in the language would now have to understand 3-valued logic, 0, 1 and ?, mostly to reject it, but in case of == and !=, to process it in a custom way. Again, the complexity is considerable.

Here's my proposal: instead of this, add a separate method Value.match, which explicitly uses the same semantics as Case. It would work something like... z80fi_insn.match("00??100111?11101").

[RobertBaruch]

+1, I'm a fan of Value.match.

[whitequark]

Right. So now the question becomes, can this translate nicely to Verilog? Can Yosys' write_verilog generate inside and if yes, how?

[RobertBaruch]

Oh, I would just translate to '(x&p)==p' where 'p' is the pattern with '0' for '?'.

[whitequark]

Sure, that works. Can you implement it? Make sure to reproduce all the errors and warnings from Case, since the semantics should be completely identical. I think it makes sense to accept multiple patterns, also similar to Case.

[RobertBaruch]

Can do.

[RobertBaruch]

Interesting, it seems that

module z80fi_insn_spec_ld_reg_n(
    input logic [7:0] z80fi_insn,
    output logic spec_valid
);

assign spec_valid = z80fi_insn[7:0] == 8'b00???110;

endmodule

Is translated by write_verilog to:

/* Generated by Yosys 0.9+36 (git sha1 4aa505d1, clang 6.0.0-1ubuntu2 -fPIC -Os) */

(* cells_not_processed =  1  *)
(* src = "tmp.sv:1" *)
module z80fi_insn_spec_ld_reg_n(z80fi_insn, spec_valid);
  (* src = "tmp.sv:6" *)
  wire _0_;
  (* src = "tmp.sv:3" *)
  output spec_valid;
  (* src = "tmp.sv:2" *)
  input [7:0] z80fi_insn;
  assign _0_ = z80fi_insn == (* src = "tmp.sv:6" *) 8'b00???110;
  assign spec_valid = _0_;
endmodule

And to ilang as:

# Generated by Yosys 0.9+36 (git sha1 4aa505d1, clang 6.0.0-1ubuntu2 -fPIC -Os)
autoidx 2
attribute \cells_not_processed 1
attribute \src "tmp.sv:1"
module \z80fi_insn_spec_ld_reg_n
  attribute \src "tmp.sv:6"
  wire $eq$tmp.sv:6$1_Y
  attribute \src "tmp.sv:3"
  wire output 2 \spec_valid
  attribute \src "tmp.sv:2"
  wire width 8 input 1 \z80fi_insn
  attribute \src "tmp.sv:6"
  cell $eq $eq$tmp.sv:6$1
    parameter \A_SIGNED 0
    parameter \A_WIDTH 8
    parameter \B_SIGNED 0
    parameter \B_WIDTH 8
    parameter \Y_WIDTH 1
    connect \A \z80fi_insn
    connect \B 8'00---110
    connect \Y $eq$tmp.sv:6$1_Y
  end
  connect \spec_valid $eq$tmp.sv:6$1_Y
end

So it seems there is support (at least in Yosys) for don't care values in equality comparison...

[RobertBaruch]

Pre-work: accept '?' in Case.

[whitequark]

@RobertBaruch I don't understand why #203 is necessary for this feature.

[whitequark]

So it seems there is support (at least in Yosys) for don't care values in equality comparison...

In Verilog, ? used in a number is exactly equivalent to z:

As far as I can tell, the standard provides no way to use == or === to emulate casez, which is what we are trying to achieve here.

In particular, if my reading of the standard is correct, using something like x == 1'b? should always produce 1'bx, not what you're expecting here. So it looks like Yosys might not be compliant here.

[RobertBaruch]

@RobertBaruch I don't understand why #203 is necessary for this feature.

That's the Verilog way of representing don't-cares in case. Or, as you point out, it translates to z, and in casez that is a don't-care. The reason I added it is that people who write Verilog will naturally use ? in a with Case, and be surprised when it fails.

However, I agree that it's wrong to use ? as a don't-care value in == unless you want to exactly compare z. ==?, on the other hand, does use z, and therefore ? as a don't-care. There is also the corresponding inequality !=?. I don't think yosys implements either. I'll check in with Clifford on that.

[RobertBaruch]

In the meantime, I can just add the matches function and use - as the don't care character.

[whitequark]

==? is a SystemVerilog feature, right? I don't think base nMigen language (without assertions) should emit any SystemVerilog features in the Verilog backend. That said, it would be nice to have those in Yosys.

The reason I added it is that people who write Verilog will naturally use ? in a with Case, and be surprised when it fails.

I think adding a syntactic feature requires more motivation than "that's how it's done in Verilog". One specific reason I don't like adding ? is because in Verilog it is an alias for z (i.e. it is not inherently a wildcard) and nMigen does not have z.

In the meantime, I can just add the matches function and use - as the don't care character.

Sounds good.

[RobertBaruch]

I agree -- it would be confusing to add ?, because of its ties to z.