PREUNSAT error issues

[shushruthholla]

Hey,
I am working on trying to integrate the riscv-formal interface to the noelv processor. I have started running the formal verification tests and encountered an error mentioning PREUNSAT, Assumptions are unsatisfiable. So I looked through previous issues and added the nopresat flag which solved the issues. I am having a dilemma if my approach is right. Any opinion would be appreciable.

[jix]

Adding the nopresat option is most likely only hiding, not solving the issue. The "PREUNSAT" status means that you have conflicting assumptions in your design. Since an assumption excludes all possible traces that would violate that assumption, having mutually conflicting assumptions excludes all traces, leaving no traces to actually verify. If you add the nopresat option without changing the assumptions, you would still exclude all traces and only tell smtbmc to not check for that. In that case smtbmc would then tell you that your assertions hold on all non-excluded traces, but since you excluded all traces, that is vacuously true and does not actually verify anything about your design.

Note that the presat check is only able to detect when you excluded all possible traces. It is still possible to have assumptions exclude more scenarios than intended and it's always a good idea to run separate cover checks using the same set of assumptions.

[shushruthholla]

Sorry for the late reply. Ok what I am trying to do in the processor that I am using is that, because it is designed in vhdl I use ghdl to get the verilog netlist and from this design created the wrapper and used it for riscv-formal test.
Here is the design, config and the wrapper file that I used:
config_file.txt
noelv_verilog.txt
wrapper_noel.txt

The commands that I used to create the ghdl verilog netlist is as shown below:
1)ghdl -m -fexplicit --ieee=synopsys --mb-comments --warn-no-binding -O2 --workdir=gnu/gaisler --work=gaisler cat ghdl.path wrap_noelvcpu
2)ghdl --synth --out=verilog -fexplicit --ieee=synopsys --mb-comments --warn-no-binding --workdir=gnu/work --work=work -Pgnu/grlib -Pgnu/synplify -Pgnu/techmap -Pgnu/wizl -Pgnu/eth -Pgnu/opencores -Pgnu/gaisler -Pgnu/work gaisler.wrap_noelvcpu > noelv.v

If you want to recreate the ghdl netlist it can be done from the zip file for the vhdl design provided below:
grlib-com-nv.tar.gz

The generic design can be found in /designs/noelv-generic and the core design can be found in /lib/gaisler/noelv/core.The top file for the design is named wrap_noelvcpu and can be found in
Use this command to import the file in noelv-generic:make ghdl-import and after that use the above commands.

Since the design is too large I am using only one check from the checks folder in ridcv-formal. The problem that I am facing as you mentioned is that I am unable to find the conflicting assumption that is causing the PREUNSAT ERROR

[jix]

Which versions of yosys, sby and riscv-formal are you using? The noelv_verilog.txt file seems to use $fatal in a way which is not supported by yosys verilog frontend. Can you provide a .tar.gz of the full noel subdirectory of your riscv-formal setup? Including the checks directory after getting the PREUNSAT error? That would help with reproducing the exact setup and would also include all logfiles of your run that resulted in PREUNSAT.

[shushruthholla]

Sorry for not informing earlier I am using the tabby cad suite with yosys version being Yosys 0.25 (git sha1 e02b7f64b, clang 10.0.0-4ubuntu1 -fPIC -Os).
Here is the noelv file of riscv-formal:
noelv.tar.gz

Since the design file is too large and each test takes long time to get an outcome I just executed one of the checks from the checks folder here .i.e. insn_add_ch0.sby. Since the generated output is large I compressed it inside the noelv risc-formal file.

[shushruthholla]

Sorry for not informing earlier I am using the tabby cad suite with yosys version being Yosys 0.25 (git sha1 e02b7f64b, clang 10.0.0-4ubuntu1 -fPIC -Os). Here is the noelv file of riscv-formal: noelv.tar.gz

Since the design file is too large and each test takes long time to get an outcome I just executed one of the checks from the checks folder here .i.e. insn_add_ch0.sby. Since the generated output is large I compressed it inside the noelv risc-formal file.

Do you need anything or did I miss anything? @jix

[jix]

wrapper.sv:70: actual bit length 2 differs from formal bit length 3 for port 'rvvi_valid'
wrapper.sv:71: actual bit length 128 differs from formal bit length 192 for port 'rvvi_order'
wrapper.sv:72: actual bit length 64 differs from formal bit length 96 for port 'rvvi_insn'
wrapper.sv:73: actual bit length 2 differs from formal bit length 3 for port 'rvvi_trap'
wrapper.sv:74: actual bit length 2 differs from formal bit length 3 for port 'rvvi_halt'
wrapper.sv:75: actual bit length 2 differs from formal bit length 3 for port 'rvvi_intr'
wrapper.sv:76: actual bit length 4 differs from formal bit length 6 for port 'rvvi_mode'
wrapper.sv:77: actual bit length 4 differs from formal bit length 6 for port 'rvvi_ixl'
wrapper.sv:78: actual bit length 10 differs from formal bit length 15 for port 'rvvi_rs1_addr'
wrapper.sv:79: actual bit length 10 differs from formal bit length 15 for port 'rvvi_rs2_addr'
wrapper.sv:80: actual bit length 10 differs from formal bit length 15 for port 'rvvi_rd_addr'
wrapper.sv:81: actual bit length 128 differs from formal bit length 192 for port 'rvvi_x_wdata'
wrapper.sv:82: actual bit length 128 differs from formal bit length 192 for port 'rvvi_pc_rdata'
wrapper.sv:83: actual bit length 128 differs from formal bit length 192 for port 'rvvi_pc_wdata'
wrapper.sv:84: actual bit length 128 differs from formal bit length 192 for port 'rvvi_addr'
wrapper.sv:85: actual bit length 16 differs from formal bit length 24 for port 'rvvi_rmask'
wrapper.sv:86: actual bit length 16 differs from formal bit length 24 for port 'rvvi_wmask'
wrapper.sv:87: actual bit length 128 differs from formal bit length 192 for port 'rvvi_rdata'
wrapper.sv:88: actual bit length 128 differs from formal bit length 192 for port 'rvvi_wdata'
wrapper.sv:89: actual bit length 128 differs from formal bit length 192 for port 'rvvi_rs1_rdata'
wrapper.sv:90: actual bit length 128 differs from formal bit length 192 for port 'rvvi_rs2_rdata'

These warnings indicate that checks.cfg has nret 2 but should have nret 3, which seems to be the cause of the PREUNSAT error.

Note that the version of Tabby CAD you're using is missing around a year of updates, so I'd also recommend updating to make sure you have all the latest fixes.

[shushruthholla]

Hey @jix, as mentioned above I changed the noelv.v file to suit for nret 2. But still the PREUNSAT ERROR persists. I just want to know weather you were able to solve the issue. And for reference here is the noelv.v that is altered to work for nret 2:
noelv.txt
Once again thank you for response.

[jix]

I did not get a PREUNSAT when running the design from the .tar.gz with the riscv-formal configuration changed to nret 3, I did not try anything else that nor did I try to verify whether the riscv-formal setup is working correctly besides avoiding the PREUNSAT error (for either nret 2 or nret 3).

[shushruthholla]

Hey @jix, do you mind uploading your log files also can I know the version of Yosys and Tabby CAD suite you're using?

[shushruthholla]

Hey @jix, do you mind uploading your log files also can I know the version of Yosys and Tabby CAD suite you're using?

Would you mind letting me know of this?

[jix]

Sorry, I didn't make a copy of the log file before trying other configurations overwriting the passing logfile, I've now tried reproducing it with the latest tabby CAD release and am now also getting a PREUNSAT even with nret 3 and your initial version.

I might have inadvertently been running the passing run using my then current development version, where assumptions were not working as I was in the middle of making changes to code related to the assumption handling.

I've now started a run with your updated nret 2 version and intend to check the result with a new debugging feature for unsatisfiable assumptions we just released. I'll report back when I have the results of that.

[jix]

In the latest Tabby CAD, re-running smtbmc with the --track-assumes option after SBY failed produces a set of assumptions that are in conflict (there also is the --minimize-assumes option that tells --track-assumes to produce a minimal set of conflicting assumptions, which can involve a significant amount of further solving). It's possible to include that option directly with the smtbmc engine in the SBY configuration file, like this smtbmc yices -- --track-assumes.

Instead of including it in the SBY file I reran just smtbmc manually after SBY failed with PREUNSAT for your updated verilog sources and nret 2 by running the following commands:

cd checks/insn_add_ch0
yosys-smtbmc -s yices --presat --unroll --noprogress -t 20:21 --track-assumes  model/design_smt2.smt2

This ultimately resulted in:

##   0:00:56  Skipping step 19..
##   0:00:58  Checking assumptions in step 20..
##   0:01:58  Assumptions are unsatisfiable!
##   0:01:58  Conficting assumptions:
##   0:01:58    In rvfi_testbench: rvfi_insn_check.sv:139.5-139.24 (_witness_.assume_flatten_checker_inst__auto_verificsva_cc_1731_import_4100)
##   0:01:58    In rvfi_testbench: rvfi_testbench.sv:30.14-30.43 (_witness_.assume_auto_verificsva_cc_1731_import_2625)
##   0:02:02  Status: PREUNSAT

Telling us that assume(spec_valid); in rvfi_insn_check.sv:139 and assume (reset == $initstate); in rvfi_testbench.sv:30 together exclude all possible paths.

The first assumption is only active in the check cycle (step 20) and restricts the FV to paths where the core is reporting that it has retired the target instruction (add).

The second assumption enforces that all considered paths start with the core being reset during step 0.

A PREUNSAT in that case thus means it's not possible for the core to report the retiring of an add on rvfi channel 0 in step 20 starting from a reset state, in turn meaning the check cannot actually check anything thus reporting a PREUNSAT.

Why that is the case is specific to the core in question, and thus not something I can directly help you with. If the core is entirely unable to retire certain instructions on certain rvfi channels that would be expected. In that and only that specific case it would be correct to ignore that expected PREUNSAT error for those specific checks.