Add unique, unique0, and priority keywords

[nblei]

Consider

module test (
	input [2:0] onehot,
	output logic [1:0] idx
);
always_comb begin
	case (onehot)
		3'b001: idx = 2'b01;
		3'b010: idx = 2'b10;
		3'b100: idx = 2'b11;
	endcase
end
endmodule : test

Synthesizing this with dc_shell results in inferred latches (ignore for a moment the fact that DC doesn't error out when latches are inferred in an always_comb block) because only three out of eight possible mux selects are handled in the switch statement.
This can be fixed by adding a default case, or by adding a default assignment prior to the switch statement. However, this infers unnecessary logic when we are guaranteed the external controllability constraint that onehot is, in fact, one-hot.

However, adding the unique keyword solves this problem optimally:

	unique case (onehot)
		3'b001: idx = 2'b01;
		3'b010: idx = 2'b10;
		3'b100: idx = 2'b11;
	endcase

The unique case is a mechanism for the RTL designer to encode controllability constraints. It encodes the designer's guarantee to the synthesis tool / simulator / model checker that for each evaluation of the switch control signal, exactly one case in the switch statement will match. Similarly, unique can be used to qualify if-else if*-else statements.

Other SV2009 keywords unique0 and priority also modify the semantics of control statements.

[taichi-ishitani]

Switch statement can also have these modifiers.

---

A synthesis tool can make very aggressive optimization for a case/if statement with unique modifier and this optimization may cause simulation/synthesis result mismatch when multiple conditions are matched.To prevent mismatch, our company has a lint rule to prohibit using unique modifier.
Therefore, I think we need to add a build option to remove these modifires during emitting SV RTL.

[dalance]

At the point of view of syntax complexity, adding #[cond_type] attribute instead of adding keywords may be better.

#[cond_type(unique)]
case a {
}

#[cond_type(priority)]
case a {
}

#[cond_type(unique0)]
if a {
} else if b {
} else {
}

About condition overlapping, mismatch between simulation and synthsis can be avoided if these modifiers are allowed when all conditions can be checked by Veryl compiler statilcally.

param X: u32 = 1;
const Y: u32 = 1;

// OK
#[cond_type(unique0)]
case a {
    0: x = 1;
    Y: x = 2;
}

// NG because X may be overridden
#[cond_type(unique0)]
case a {
    X: x = 1;
}

[taichi-ishitani]

About condition overlapping, mismatch between simulation and synthsis can be avoided if these modifiers are allowed when all conditions can be checked by Veryl compiler statilcally.

I think Veryl also needs to check that all possible values for the case condition expression are listed as case items.

[nblei]

There should not be a mismatch between synthesis and simulation in the sense that simulation will emit an error (or perhaps warning, I forget) in the case that no cases match, or more than a single case matches.

I do like the idea of a compiler switch which automatically removes the non-priority cond_type qualifiers.

I do not see how Veryl can possibly be expected to check condition overlapping.

Consider a microprocessor design which purposely does not check for illegal instructions (e.g., a microcontroller executing firmware embedded in an SoC). A mux may only need to handle valid opcodes, but how is Veryl to know this? In the presence of external controllability don't cares, I think static analysis in Veryl is insufficient.

[dalance]

I do not see how Veryl can possibly be expected to check condition overlapping.

Yes. Veryl can't check overlapping in all cases.
So at the most safe side, there is an idea that these attribute can be used only when Veryl can check overlapping.
For example, if all case condition are numeric literal or const value refering literal, Veryl can check it.
I think these limitation may be acceptable.

[nblei]

So at the most safe side, there is an idea that these attribute can be used only when Veryl can check overlapping.

I think this is exactly the wrong approach.

If Veryl can check these conditions, then any logic synthesis tool will, also.

These modifiers exist explicitly to enable encoding of external controlability don't cares. That is, they exist to be used precisely when logic synthesis tools (and thus Veryl) cannot check condition overlapping, condition uniqueness, etc.

It would be like only allowing restrict keyword in C when gcc can determine at compile time when two pointers will not alias.

[dalance]

I understood like below. Is this right?

• When condition is static and overlapping check can be done by tools, synthesizer can optimize enough without these keywords.
• When these checking can't be done, designer notify the condition uniqueness to synthesizer through these keywords. This enables additional optimization which is impossible without these keywords.
• If there is any overlapping contrary to the keyword, mismatch between simulation and synthesis occurs. Designer is responsible for the condition ensurance.
• If these keywords are removed by compiler switch, mismatch doesn't occur, but some optimizations may be disabled.

[nblei]

Yes on points 1, 2, 4. Point 3, I disagree with the statement that there is mismatch between simulation and synthesis. In simulation, if `unique` is used and zero or more than 1 case match (or, if zero or more than one if condition evaluates to true), then an error/warning is emitted. In simulation, if `unique0` is used and more than 1 case match (or, if more than one if condition evaluates to true), then an error/warning is emitted.

…

On Mon, Sep 9, 2024 at 8:18 PM Naoya Hatta ***@***.***> wrote: I understood like below. Is this right? - When condition is static and overlapping check can be done by tools, synthesizer can optimize enough without these keywords. - When these checking can't be done, designer notify the condition uniqueness to synthesizer through these keywords. This enables additional optimization which is impossible without these keywords. - If there is any overlapping contrary to the keyword, mismatch between simulation and synthesis occurs. Designer is responsible for the condition ensurance. - If these keywords are removed by compiler switch, mismatch doesn't occur, but some optimizations may be disabled. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/veryl-lang/veryl/issues/937*issuecomment-2339372052__;Iw!!DZ3fjg!_L9gTQH4KHQ0YLuIiyDeBhsJhV3QcX_9fJZaCwNpMWdPSHXtq9tXNC16DNLkwxzXBYCcbFEXydIgcSHw4qcGw315P8lV$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AFAMUBETCSMFOWTYTHZXMXDZVY3EFAVCNFSM6AAAAABNURDUSSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMZZGM3TEMBVGI__;!!DZ3fjg!_L9gTQH4KHQ0YLuIiyDeBhsJhV3QcX_9fJZaCwNpMWdPSHXtq9tXNC16DNLkwxzXBYCcbFEXydIgcSHw4qcGw87ueaW5$> . You are receiving this because you authored the thread.Message ID: ***@***.***>

-- Very Respectfully, Nathaniel Bleier ***@***.*** 773-531-8229 (Cell)

[dalance]

I agree wrong usage of these keywords emits warning, but in many cases simulator works fine with warning messages.
(Of course, we can configure to promote some warnings to hard errors, but it is not default behavior.)
So if we miss these messages, I think mismatch occurs.

[taichi-ishitani]

I think we need to add a build option to remove these modifires during emitting SV RTL

Regarding this idea, we cannot remove these quarifiers automatically if no default item is specified.
If we remove unique keyword from nblei's exmaple below,

always_comb begin
	case (onehot)
		3'b001: idx = 2'b01;
		3'b010: idx = 2'b10;
		3'b100: idx = 2'b11;
	endcase
end

synthesis tools will infer latch logic.
Therefore, I think we need to tell Veryl which case item is default item to make possible to remove qualifiers automatically and safely.

always_comb {  
  #[cond_type(unique)]
  case onehot {
    3'b001: idx = 1;
    3'b010: idx = 2;
    #[default]
    3'b100: idx = 3;
  }
}

If the build option to remove qualifiers is set false then Veryl will emmit SV RTL like below.

always_comb begin
  unique case (onehot)
    3'b001: idx = 1;
    3'b010: idx = 2;
    3'b100: idx = 3;
  endcase
end

If the option is set true then Veryl will emmit SV RTL like below.

always_comb begin
  case (onehot)
    3'b001: idx = 1;
    3'b010: idx = 2;
    default: idx = 3;
  endcase
end

[taichi-ishitani]

We have to trust designer if RTL code including case/if statements with these quialifiers works correctly.
Therefore, I think Veryl should report information message when quialifiers are used.

[dalance]

We have to trust designer if RTL code including case/if statements with these quialifiers works correctly.
Therefore, I think Veryl should report information message when quialifiers are used.

I think clean RTL should have no message because messages shown at all time will be ignored.
So how about the following designs?

• By default, case_type is ignored. If emit_case_type = true in Veryl.toml, it is emitted.
  emit_case_type = true means that we understand risk of case_type, so the additional message is not required.

• By default, case_type is emitted and the additional message is shown.
  After confirming safety of case_type, we set suppress_case_type_message = true in Veryl.toml, and the messages are suppressed.

[taichi-ishitani]

I agree with this idea.
By the way, should Veryl support adding these quialifier to if statement?

[nblei]

By the way, should Veryl support adding these quialifier to if statement?

Yes.

[taichi-ishitani]

By the way, should Veryl support adding these quialifier to if statement?

Yes.

For if statement, how should we add default attribute?

[nblei]

The trailing `else` branch can be the default automatically.

…

On Thu, Sep 12, 2024 at 9:09 AM Taichi Ishitani ***@***.***> wrote: By the way, should Veryl support adding these quialifier to if statement? Yes. For if statement, how should we add default attribute? — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/veryl-lang/veryl/issues/937*issuecomment-2346240855__;Iw!!DZ3fjg!_SMz3XJZJXmDoQSpia42P5agKV86jvFdw6eAliigVbGhZ2gtEmvd2DIisxyVxyEiMuMv4zqF3AWsnI3QvvZh2UC21s3H$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AFAMUBEZCCL7NMSAE2I5NGDZWGHALAVCNFSM6AAAAABNURDUSSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBWGI2DAOBVGU__;!!DZ3fjg!_SMz3XJZJXmDoQSpia42P5agKV86jvFdw6eAliigVbGhZ2gtEmvd2DIisxyVxyEiMuMv4zqF3AWsnI3QvvZh2R5DZTPR$> . You are receiving this because you authored the thread.Message ID: ***@***.***>

-- Very Respectfully, Nathaniel Bleier ***@***.*** 773-531-8229 (Cell)

[taichi-ishitani]

How about if statement without else branch like this?

if onehot[0] {
  idx = 1;
} else if onehot[1] {
  idx = 2;
} else if onethot[2] {
  idx = 3;
}

[nblei]

With unique it is semantically equivalent to the version where the last block is unconditional. Without unique, we can just default the last block to be unconditional.

…

On Thu, Sep 12, 2024, 6:38 PM Taichi Ishitani ***@***.***> wrote: How about if statement without else branch like this? if onehot[0] { idx = 1;} else if onehot[1] { idx = 2;} else if onethot[2] { idx = 3;} — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/veryl-lang/veryl/issues/937*issuecomment-2347359892__;Iw!!DZ3fjg!_6C6rKVp5nhuhXiWnZuBNaq9BeupyB02odp7h_VrzaPs1QCsFnERSARZi7Inu215lXTIpwE_wM3OE3fQOYaVUkSA7vyt$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AFAMUBGUDXN6DHMKN6332ITZWIJUPAVCNFSM6AAAAABNURDUSSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBXGM2TSOBZGI__;!!DZ3fjg!_6C6rKVp5nhuhXiWnZuBNaq9BeupyB02odp7h_VrzaPs1QCsFnERSARZi7Inu215lXTIpwE_wM3OE3fQOYaVUva7eCzY$> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[taichi-ishitani]

OK, I agree.
I think the following SVA should be inserted to the default item for ease to report the designer that no case conditions are matched.

case (onehot)
  3'b001: idx = 1;
  3'b010: idx = 2;
  default: begin
    assume (onhot == 3'b100)
    else $error("unexpected condtion is matched");
    idx = 3;
  end
endcase

if (onehot[0]) begin
  idx = 1;
end else if (onehot[1]) begin
  idx = 2;
end else begin
  assume (onehot[2])
  else $error("unexpected condtion is matched");
  idx = 3;
end

[nblei]

That works with the caveat that it does not produce error on uniqueness violation. So if more than one case or branch evaluates to true, no error or warning is emitted. Perhaps this is fine, though.