[axi ar_len assertion] ARLEN is limited to 0 or 1

[khandelwaltanuj]

Is there an existing CVA6 bug for this?

• [x] I have searched the existing bug issues

Bug Description

Hello @AEzzejjari @ASintzoff

In the following file:

https://github.com/openhwgroup/cva6/blob/8202a7f714d708555021598a7baf3f97eda6b468/verif/tb/uvmt/uvmt_cva6_axi_assert.sv#L95

I have following assertion failing. //Check if all Read transaction performed by CVA6 are equal to 0 or 1 property AXI4_CVA6_ARLEN; @(posedge axi_assert_if.clk && axi_assert_if.axi_assertion_enabled) disable iff (!axi_assert_if.rst_n) axi_assert_if.ar_valid |-> axi_assert_if.ar_len == 0 || axi_assert_if.ar_len == 1; endproperty

For my configuration: https://github.com/openhwgroup/cva6/blob/master/core/include/cv64a60ax_config_pkg.sv

It seems to be doing access of ALREN = 3.

As can be seen in the following capture of waves:

Do you think there is an issue with this assertion ?

Thanks and Regards Tanuj Khandelwal

[khandelwaltanuj]

I see that I have already one issue on this:

https://github.com/openhwgroup/cva6/issues/2754

[khandelwaltanuj]

I am now able to create my 64 bit configuration and spike.yaml file.

[ASintzoff]

Depending on the AXI configuration, ARLEN may be different of 0 or 1. Until now, the AXI agent was used for CVA6 configuration with ARLEN equals to 0 or 1.

Feel free to update the testbench.

It could be useful to establish a link between the assertions and the actual CVA6 configuration. For instance, if according to the configuration, ARLEN shall not be equal to 3, it would be better to stick to existing assertions.