Missing `ifdef guard from assertion in ibex_core.sv

[Kyrhe]

Observed Behavior

Building ibex without INC_ASSERT define fails due to missing guard in ibex_core.sv.

Expected Behavior

Expecting core to elaborate without this define.

Steps to reproduce the issue

This assertion relies on logic only present in ibex_ex_block.sv when it is compiled with this assertion. If ex_block is compiled with the define, elaboration succeeds without issues.

My Environment

RHEL7 / Questa

Compiling source codes based on external filelists and Questa commands in makefile.

Version of the Ibex source code:

The issue is present in current master (53888bc), assertion was introduced by [rtl] Guard... merge.

Edit: Testing more locally

This seems to be more complex issue than I originally figured. Simply inserting guard ifdef does not fix the issue, Module seems to be inheriting the INC_ASSERT define from somewhere (and the ex_block does not). Probably from includes that define the macros, but I did not investigate that too much yet.

Alternative is to use the SYNTHESIS define which of course disables all assertions.

[rswarbrick]

Hmm. I think the problem is that ibex_core.sv has a hierarchical reference to ex_block_i.sva_multdiv_fsm_idle on line 1858 and that signal doesn't exist if INC_ASSERT is not defined.

The weird thing is that the reference is:

  // If the ID stage signals its ready the mult/div FSMs must be idle in the following cycle
  `ASSERT(MultDivFSMIdleOnIdReady, id_in_ready |=> ex_block_i.sva_multdiv_fsm_idle)

and it was a bit surprising to me if this matters when INC_ASSERT is not defined! The INC_ASSERT macro is defined in prim_assert.sv when we aren't in a "dummy" mode.

Given your last note, I guess we don't have SYNTHESIS defined. Does that mean your Questa simulation has VERILATOR defined?(!)

To debug further, I think you'll need to do some "debug printing" by hacking on prim_assert.sv to figure out how things are expanding.

[Kyrhe]

I did not have any defines included originally.

With the VERILATOR in questa defined, core does pass elaboration. So that behavior is the same as SYNTHESIS when considering this particular assertion. This does make sense as they both have the same dummy header defined in prim_assert.sv#L102.

Additionally, the else branch without either one does set INC_ASSERT define for this file. Hence, my intial thought on just having that as same guard define as ex_block does not work.

[rswarbrick]

Ok, that's rather confusing! Since we don't have access to the tool you're working with, I think you'll have to do some debugging. To trace the ifdef chain, you can insert silly lines that won't compile (hello, I am invalid code) and see whether a build error comes out. If so, that line was being included...

If it feels like something hasn't been defined properly, you can also hunt down the order that things are compiled by inserting a syntax error in two places (and seeing which one appears in the log!).

[Kyrhe]

Sorry for the delay in returning to this.

I've looked into the compile some more and it seems to be interaction between ibex_core.sv and the ibex_ex_block.sv. As mentioned earlier, prim_assert.sv defines the used assertion macros and whether INC_ASSERT is defined. This generally acts as guard for the assertions across all of the files. By default as I run the simulation in questa, I hit the branch of including standard macros and addition of INC_ASSERT. This (correctly) adds the verification bits to the ibex_core.sv and due to using normal assertions, it fails the hierarchical check of ibex_core.sv#L1858. I do now believe this is correct and expected behavior for both files.

To synchronize the ibex_ex_block.sv to this behavior, it probably requires that include "prim_assert.sv" be added. I tested the compile on this locally and it seems to now correctly compile and add the verification parts guarded by INC_ASSERT ifdef. Also, this addition combined with SYNTHESIS define to compile, disables assertions and behaves as expected.

My suggestion on fixing this would be on ibex_ex_block.sv to add

ibex_ex_block.sv:

<start removed for brevity>
 * Execution block: Hosts ALU and MUL/DIV unit
 */

`include "prim_assert.sv"

module ibex_ex_block #(
<end removed for brevity>

[rswarbrick]

Ahah, now I see! I think I probably agree. @GregAC: I think the use of INC_ASSERT in that file comes from commit 5977d4e in March. Does the message from @Kyrhe sound right to you?