Translation of 'inside' includes 1'bx

[NilsGraf]

Example (from dmi_jtag.sv):

    if (capture_dr && state_q inside {Read, WaitReadValid}) begin
      error_dmi_busy = 1'b1;
    end

sv2v translates it as follows:

    if (capture_dr && |{((Read ^ Read) !== ((state_q ^ state_q) ^ (Read ^ Read)) ? 1'bx : (Read ^ Read) === (Read ^ state_q)), ((WaitReadValid ^ WaitReadValid) !== ((state_q ^ state_q) ^ (WaitReadValid ^ WaitReadValid)) ? 1'bx : (WaitReadValid ^ WaitReadValid) === (WaitReadValid ^ state_q))})
        error_dmi_busy = 1'b1;

LEC has issues with the 1'bx. Would it be possible to translate above to something simpler such as below? Thanks!

    if (capture_dr && ((state_q == Read) || (state_q == WaitReadValid)))
      error_dmi_busy = 1'b1;

[zachjs]

Could you clarify what issues you're running into? The 1'bx comes from the definition of the wildcard equality operators, which are used in the definition of the the set membership operator. The 1'bx should only be returned here if state_q contains an x or a z.

[NilsGraf]

Conformal LEC has issues with this. I'm not even sure if "===" and "!==" are synthesizable.

[NilsGraf]

Ah, I just noticed your PR #2465.

I had created a similar one here and one for ibex here. Let me look through this. It seems you have now access to Conformal LEC, which is awesome.

[zachjs]

I'm surprised Conformal LEC is giving issues for this, as I successfully verified other modules containing the same logic (for example, dm_csrs). In case it matters, I am using Conformal Version 19.10-s300 (24-Aug-2019) (64 bit executable). I have access to some older versions, too.

[NilsGraf]

I'm using Version 18.10.100. Will try to use the newer version.

I noticed the following: It passes when I run dm_csrs.sv and also dm_mem.sv. But LEC fails when I run rv_dm.sv with all its subblocks (note that dm_csrs.sv and dm_mem.sv are subblocks of rv_dm.sv). If you are running LEC with set undefined cell black_box, then I believe only the toplevel of the module (e.g. rv_dm.sv) is checked and all its submodules are blackboxed and ignored.

[zachjs]

I believe I have found an issue with the conversion of the wildcard equality operators. I will need some time to figure out an alternative solution.

[NilsGraf]

Awesome!

[zachjs]

The conversions for inside and wildcard equality should now be fixed. The end result is even more verbose. There may be a more clever way of implementing the wildcard operators, I suspect involving reductions.

[NilsGraf]

Awesome, I downloaded the latest version of sv2v but LEC still doesn't work without removing the inside lines. I will debug some more.

On a different note, using the latest version v0.0.3 (64f3067) caused a new issue to pop up: For flash_mp.sv, a few parameters are used before they are defined in the generated file flash_mp.v. For example parameters NumBanks and BankW. This issue also exists for other flash_*.sv files. Any ideas?

[zachjs]

This issue with NumBanks was introduced in https://github.com/lowRISC/opentitan/commit/b02859e6879105e905bf3d00fb22e2338751aaef. NumBanks is a parameter in that module and is imported using a wildcard import. While this is legal, sv2v does not currently handle it correctly.

[zachjs]

That import issue should now be fixed.

[NilsGraf]

Thanks for the prompt fix. I downloaded the latest version. Now I see a similar parameter order issue. This time it's parameter DataPart in file flash_ctrl.sv. Any ideas? Thanks!

[zachjs]

That issue should also now be fixed. Unfortunately, most of the tools I interact with don't complain about the ordering of data declarations, so such issues can be easy to miss.

[NilsGraf]

Thanks for fixing, it works now fine on my side.

[zachjs]

I think the cause of this issue has been staring us right in the face:

// Warning: (VLG1.2) Case equality operators are treated as equality operators (occurrence:4)

It doesn't look like Conformal supports the case equality operators, which date back to at least Verilog-2001.

[NilsGraf]

Good catch. I'm not surprised because I wouldn't expect case operators ("===" and "!==") to be synthesizable. I wouldn't use these operators in code that gets synthesized.

Would it make sense to have a mode where sv2v doesn't generate case operators? And also no 1'bx (which I also wouldn't expect in synthesizable code). Note from LEC log file: x-values are treated as 0 in unary/binary expressions.

[zachjs]

I'm generally opposed to adding modes as a way of hiding flaws :)

I was not aware that my conversion strategy for wildcard operators was not synthesizable. I believe in the long run, sv2v will need to resolve the value of the "pattern" and compute the different possible combinations for patterns that have wildcard bits. As of c005e5c6ae91bcab608d86439945d1a14fae0e10, the wildcard conversion does not rely on the case equality operators if the pattern can be trivially resolved and determined to not contain any wildcard bits. I believe OpenTitan most often uses inside for sets of enum values, which are among the "trivially resolvable" patterns.

[NilsGraf]

I'm copying again the original example from this issue. Could the following SystemVerilog be translated to the Verilog code below? Thanks!

    if (capture_dr && state_q inside {Read, WaitReadValid}) begin
      error_dmi_busy = 1'b1;
    end

    if (capture_dr && ((state_q == Read) || (state_q == WaitReadValid)))
      error_dmi_busy = 1'b1;

This is synthesizable and should be fine with Conformal.

[zachjs]

Absolutely! As of that commit, you'll get:

if (capture_dr && |{state_q == Read, state_q == WaitReadValid})

The use of the OR reduction comes from explanation of the set membership operator in the SystemVerilog specification. I'm confident this is equivalent to the logical OR in your example.

[NilsGraf]

Yes, this is equivalent. Thanks! I'll give this a try.

[NilsGraf]

Works fine on my side, thanks!