Name of Encoding Constraint Annotation

[Jozott00]

encoding definitions will have an optional annotation used by the decode tree generator to resolve conflicting encodings. We’re searching for a good name for such annotation.

Consider the following example

format F: Bits<15> = 
{ a: Bits<5>
, b: Bits<5>
, c: Bits<5>
}

// instruction definition A: F
encoding A = { a = 0b10101 }

// instruction definition B: F
encoding B = { a = 0b10101, b = 0b01001 }

A and B are conflicting, because an instruction with { a = 0b10101, b = 0b01001 } would match both of them. However, we want that A is matched for every field b that is not 0b01001. With this constraint, the conflict is resolved.

[ <name> : b = 0b01001 ]
encoding A = { a = 0b10101 }

encoding B = { a = 0b10101, b = 0b01001 }

@rascmatt and I think that it is in general easier to specify the condition the encoding mustn’t fulfill, than the condition it must fulfill. So we prefer to write [ <name> : b = 0b01001 ] instead of [ ensure : b != 0b01001 ].

We thought of several names for this annotation that should reflect what the annotation does.
If you have other suggestions please let us know.

There are only 8 options allowed, but we have other names like:
require, ensure, assert, constraint, legal, illegal, defined, undefined, reserved, forbid, allow, forbidden, allowed, valid, invalid, include, exclude.

[AndreasKrall]

I am not sure if it is really easier to specify and understand the forbidden constraint, I am a friend of positive specifications. And in reality it will be necessary to specify both constraint expressions as two instructions will be defined with the opposite constraints if we have encoding subsumptions. We further should discuss if encoding constraints and group constraints can be specified similarly. In the following there are some examples:

[assert : imm  = 0]
encoding ImmNull = {}    // also possible: encoding ImmNull = {imm = 0}
[assert : imm != 0]
encoding NonNull = {}    // imm is not listed
[assert : imm3(2)  = 0 || imm3(1..0)  = 0]  // instruction is valid only if imm3 of type Bits<3> <= 4
encoding SmallScale = {}
[illegal: imm3(2) != 0 && imm3(1..0) != 0] // instruction is illegal if imm3 of type Bits<3> > 4
encoding SmallScale = {}

You just have to understand De Morgan's laws.

We also should discuss if we need two annotations, one on the encoding and one on the instruction. The annotation on the encoding guarantees that this instruction is matched, if the constraint is fulfilled. Then an additional constraint can be added to the instruction like:

[raise Undefined: imm3(2) = 1 && imm3(1..0) != 0]

[AndreasKrall]

In the meeting today we decided to use a positive annotation. We came not to a clear decision with the name. I suggest to start with [select when : Expr] or [selected when : Expr] or [select : Expr]. The expression is restricted to (partial) field accesses with (non)equality comparisons against constant expressions connected by the logical operators !, && and ||.