Stopping to prevent exponential design size explosion

Users
1

Hello,

I was trying to compile a SystemVerilog design with Verific (with Tabby CAD license). This design works with Synopsys VCS.

While compiling the design, I get the following error.

Importing module cache_controller.
ERROR: SVA DFSM state ctrl signal has 18 (>16) bits. Stopping to prevent exponential design size explosion

A few warnings were generated, namely some assertion features not being supported.

My minimum compile script (cc.ys) to reproduce looks like this:

echo on

# Compile main file list
verific -f -sv2012 -formal run_dir/flist

# Set hierarchy
hierarchy -top cache_controller

I compile it with $ yosys cc.ys

My question is, how should I debug this? i.e. obtain more information from yosys about state explosion. Is there something I can control here? Identify the origin/line number where this begins to happen.

Compilation works fine, setting the hierarchy causes the problem.

Happy to provide more information. Trying to explain it minimally first.

Thanks!

2

verific -vv or something should raise the verbosity to tell you the signal. This seems a bit silly… It’s in SvaFsm::create_dnode if you want to make it behave more nicely in a PR. I created an issue.

To change this width limit, there’s a setting for the verific -import command. From its help:

  -L <int>
    Maximum number of ctrl bits for SVA checker FSMs (default=16).

Learn more here

2 Likes
3

Thanks for this! With -vv, I was able to identify the assertion that caused the problem.