Formality LEC Failure Elaboration 116: Unique case but some items may overlap.

[nstewart-amd]

LEC Formality Error code errors reported in csrng_reg_top.sv

Warning: You are using the unique case but some items may overlap. (Signal: addr_hit[0] Block: /csrng_reg_top File: RTL/csrng_reg_top.sv Line: 1951) (Formality Error code) Changed from unique case to case

LEC Formality Error code errors reported in entropy_src_reg_top.sv

Warning: You are using the unique case but some items may overlap. (Signal: addr_hit[0] Block: /entropy_src_reg_top File: RTL/entropy_src_reg_top.sv Line: 3592) (Formality Error code) Changed from unique case to case

caliptra_fm_errors.tar.gz

[calebofearth]

@howardtr can you take a look at this since these files are imported from OT?

[howardtr]

Completely missed this, will take a look, thanks @calebofearth!

[howardtr]

Hey @nstewart-amd -

Following up on this. Trying to understand the error so hopefully you can tell me where my gap in understanding is

so we have addr_hit vector defined here, which should make this onehot0

https://github.com/chipsalliance/caliptra-rtl/blob/main/src/csrng/rtl/csrng_reg_top.sv#L1808-L1827

  always_comb begin
    addr_hit = '0;
    addr_hit[ 0] = (reg_addr == CSRNG_INTR_STATE_OFFSET);
    addr_hit[ 1] = (reg_addr == CSRNG_INTR_ENABLE_OFFSET);
....
    addr_hit[16] = (reg_addr == CSRNG_MAIN_SM_STATE_OFFSET);
  end

https://github.com/chipsalliance/caliptra-rtl/blob/main/src/csrng/rtl/csrng_reg_top.sv#L1948-L2067

  always_comb begin
    reg_rdata_next = '0;
    unique case (1'b1)
      addr_hit[0]: begin
      end
....
      addr_hit[16]: begin
      end

      default: begin
        reg_rdata_next = '1;
      end
    endcase
  end

1. Do you have further context on why the error message is saying that the items may overlap? I'm wondering if there's a special pragma / waiver that I need to include since I believe this should be unique. (I double checked the constant values to make sure that there wasn't an overlap)

2. I saw that the caliptra_fm_errors.tar.gz contained a change going from unique case -> case. Does case by itself pass in the tool?

[nstewart-amd]

Howard - I expect the issue is with respect to "default" and pre-assignment. The default would contain (non-one-hot) encodings that overlap with prior one-hot cases.

I do not recommend priority encoding (case only), since this will be treated as a 16-bit binary encoded value and turn into a massive priority decoder.

` always_comb begin reg_rdata_next = '0; unique case (1'b1) addr_hit[0]: begin end .... addr_hit[16]: begin end

endcase

end `

[bharatpillilli]

What's the action on this? @howardtr

We fixing or waiving? If this is OT code that has been under use for a while, we may want to leave it as is than causing an entire val to happen because of this change

[howardtr]

Thanks for the context @nstewart-amd

I agree that we shouldn't change this to case over unique for the reasons that was listed

I'd like to push for a waiver in this case in regards to the default statement. Our internal linting tools will complain if the default state is not defined for the reasons given in https://github.com/lowRISC/style-guides/blob/master/VerilogCodingStyle.md#case-statements

[nstewart-amd]

Bharat, If it's meant to be strictly unique one hot coding, then I suggest a cleaner coding style of AND/OR structure if the LINT tool doesn't like "unique_case without default". It's kind of the point of unique_case. I'm not convinced this results in the intended circuit as coded (i.e. do you end up with all of other cases also as a result of the default?). I wouldn't be surprised if the synthesis tools implement a 16bit wide case once they detect non-overlapping conditions in the unique case.

Alternately, I think the correct coding for this would have been:

unique case (addr_hit) 16'h0001: 16'b0002: 16'b0004: ... 16'h8000: endcase

[nstewart-amd]

Anecdotally... we modifed the code to "case" and re-ran Formality against netlist synthesized with "unique case + overlaps". It passes.

Interpretation - Synthesis tools identified overlapping cases, ignored the unique qualifier, and proceeded to build a 16deep priority decoder with a default catchall at the end.

[howardtr]

I've put the change into https://github.com/chipsalliance/caliptra-rtl/pull/208

@bharatpillilli @calebofearth - ptal and let me know what the team's experience has been with unique case + default, thanks!

[Nitsirks]

I'm not convinced removing the default will actually remove the warning. @nstewart-amd have you tried this and confirmed it works? Default with unique just adds a catch for when nothing matches, simulation would still fail if multiple matches were detected. Synthesis just doesn't know that the addr_hit signal is going to be one-hot, so it dumps the unique qualifier.

unique case (addr_hit) will work, but likely doesn't synthesizes into 1 hot mux select.

Switching to case from unique case makes sense, that's what the warning is telling us synthesis is doing. This should result in a priority decode rather than the intended parallel decode.

Like Norman said - converting to AND/OR guarantees we get the intended optimized logic.

[nstewart-amd]

There's a misunderstanding on one-hot coding and use of case/default here. It might be good to review this: https://www.sutherland-hdl.com/papers/2005-SNUG-paper_SystemVerilog_unique_and_priority.pdf

What is a "default" for a case(1'b1)?

For the case(1'b1) coding style, we would typically have:

Verilog2k: //synopsys parallel_case case(1'b1) foo[0]: ... foo[n-1] default: endcase

or

//synopsys parallel_case full_case case(1'b1) foo[0]: ... foo[n-1] endcase

To defeat the evil twins, I think it should be this. SystemVerilog: unique case(1'b1) foo[0] .... foo[n-1] endcase

[nstewart-amd]

We have trials running. We had previously just changed it to "case" to resolve the LINT issue. Will advise regarding outcome of unqiue case trials.

[Nitsirks]

The default for reverse-case catches the situation where none of the branches are entered (if the one hot value is all 0, we would fall into the default).

Initializing the output also works to handle the "no match" situation deterministically, but I think simulation would balk either way if you have a unique case that doesn't match anything without a default to catch it.

From the Sutherland paper:

The semantic rules of unique have assured (assuming that run-time simulation
warnings are not ignored) that all case items used by the design have been specified. The unique
modifier has also assured (assuming run-time simulation warnings are not ignored) that there will
never be two case items that are true at the same time. Thus, synthesis can safely fully optimize a
unique case statement, removing any latched logic that might have been caused by a case
statement that is not fully specified, and removing any priority encoded logic.

It seems your synthesis tools are deciding to ignore this and drop the unique modifier.

[nstewart-amd]

the unique case does not require the default. the initial assignment already gets reg_rdata_next = '0;

the addition of "default" implies an "else", which shouldn't be there for the 2 stage AND-OR implied by unique one-hot.

[Nitsirks]

I understand that it's not required to have a default - but I believe simulation will throw an error if there is no default and the case does not match anything. Since the addr_hit vector is assigned to 0 when the address doesn't match anything, we would likely see that error during simulation.

Even the assertion checks that addr_hit is some one hot value OR zero. So either default the addr_hit to a one hot value (add an extra bit to catch a miss?) or explicitly code it as an AND/OR mux and let the addr miss case fall out that way with zeroes.

[nstewart-amd]

Michael - Simulation won't care about default/no-default. What do you mean "simulation will throw an error"? It will throw and error because of expected data mismatch elsewhere?
Synthesis and LINT will care about latch inferences. Simulation just does what it's told.

The current code is foobar. It assigns rdata=0x0000000, falls into case to pick 1-of-n rdatas, else assigns rdata=0xFFFFFFFF;

The default contradicts the initial blocking assignment.

always_comb begin
    reg_rdata_next = '0;   //initial blocking assignment to all 0's
    unique case (1'b1)
      addr_hit[0]: begin
      end
....
      addr_hit[16]: begin
      end

      default: begin
        reg_rdata_next = '1;  //default catch-all assignment to all 1's.
      end
    endcase
  end

[Nitsirks]

I guess it only throws a warning, not an error. Unique directive is powerful because it is a directive to both simulation AND synthesis.

Warning-[RT-NCMUCS] No condition matches in statement csrng_reg_top.sv, 1950 No condition matches in 'unique case' statement. 'default' specification is missing, inside caliptra_top_tb.caliptra_top_dut.csrng.u_reg, at time 0ps.

reg_rdata_next is initialized to 0 so that it can be partially assigned inside each case branch. The default case seems to be intentionally assigning '1 when the address misses any valid address.

I think we're spending a lot of effort optimizing a single mux in the design. I'll let Howard decide how to proceed with this, these are the options I see to resolve the Formality error.

Remove the unique directive - we'll get a priority mux. Remove the default - hopefully synthesizes optimally as a 1hot AND/OR chain. Warnings during simulation might create noise - some companies may flag this as errors (I know we used to). Need to confirm this resolves formality error. Explicitly code it as an AND/OR chain.

[nstewart-amd]

Feedback from design team:

1. unique case (1'b1) w/o default coding. SPG-LINT Happy Formality Unhappy - FMR_ELAB-116 warning It looks like it has strong feelings about (1'b1) decoding redundantly.

2. unique case (addr_hit) w/o default coding, SPG-LINT Happy Formality "looks" happy since addr_hit decoding can be unique. We haven't generated a netlist to compare, but have no reason to expect issue with netlist generation.

[bharatpillilli]

@howardtr - can we find a way to close this off?

Options: 1) If this code is working in a silicon for google as is (eg. titan chip), you can use this that as a waiver with the silicon proof. 2) Fix it as long as it is not going to open a wide set of new test corner cases (since this block's goal is to use as is and we aren't doing a FEV on it). If needed pull in the google author of the code into this discussion with @nstewart-amd

[howardtr]

@bharatpillilli - I was OOO - will find a way to close this out

@nstewart-amd - Can we add a formal warning waiver since we're re-using this block as-is from OpenTitan. I'd prefer we stick with the reverse unique case statement (1'b1) and take advantage of the onehot since we'd end up with a large comparator by doing the unique case(addr_hit).

I've already pushed in the changes to remove the default case into main since that's a relatively small change. We can certainly start a discussion on the OpenTitan side and make sure that the open source community benefits from this discussion. wdyt?

[bharatpillilli]

Hi @howardtr - can you have a side call with @nstewart-amd and @Nitsirks so that its faster?

[nstewart-amd]

[AMD Official Use Only - General]

Howard, re: take advantage of onehot; This is what "unique case" buys us. It avoids that clunky (1'b1) with full_case, parallel_case pragmas that would have been needed in legacy verilog.

FMR_ELAB_116 is a fatal in our flow setup currently and we don't have path to waive 1-of-N violations. Accordingly, I expect we'll need to modify locally if published code violates.

Norman

---

From: Howard T @.> Sent: Tuesday, October 3, 2023 2:26 PM To: chipsalliance/caliptra-rtl @.> Cc: Stewart, Norman @.>; Mention @.> Subject: Re: [chipsalliance/caliptra-rtl] Formality LEC Failure Elaboration 116: Unique case but some items may overlap. (Issue #187)

Caution: This message originated from an External Source. Use proper caution when opening attachments, clicking links, or responding.

@bharatpillillihttps://github.com/bharatpillilli - I was OOO - will find a way to close this out

@nstewart-amdhttps://github.com/nstewart-amd - Can we add a formal warning waiver since we're re-using this block as-is from OpenTitan. I'd prefer we stick with the reverse unique case statement (1'b1) and take advantage of the onehot since we'd end up with a large comparator by doing the unique case(addr_hit).

I've already pushed in the changes to remove the default case into main since that's a relatively small change. We can certainly start a discussion on the OpenTitan side and make sure that the open source community benefits from this discussion. wdyt?

— Reply to this email directly, view it on GitHubhttps://github.com/chipsalliance/caliptra-rtl/issues/187#issuecomment-1745502579, or unsubscribehttps://github.com/notifications/unsubscribe-auth/A2RWN2W7YLVMYYM4LZU23XDX5RKFZAVCNFSM6AAAAAA3RORZHWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONBVGUYDENJXHE. You are receiving this because you were mentioned.Message ID: @.***>

[nstewart-amd]

@howardtr I've run formal LEC for case(1'b1) version against case(addr_hit) version (both with default removed). case(1'b1) throws FMR_ELAB_116 violations. case(addr_hit) is clean.

Formal LEC is PASS. Reference code and summary of LEC run attached. csrng_reg_top_formal_lec.tar.gz

[bharatpillilli]

@howardtr ?

[howardtr]

@nstewart-amd - I've updated https://github.com/chipsalliance/caliptra-rtl/pull/247 with the changes, ptal

[calebofearth]

247 has been merged to main via #255. Can we close this issue?

[nstewart-amd]

I believe this issue is resolved.

[amullick007]

@nstewart-amd, did you get FMR_ELAB-131 warnings in your formality runs with unique case(addr_hit) w/o default?

[nstewart-amd]

We see the FMR_ELAB-131, but these are reported as warning severity and not promoted to error in our flows.