Integration Help

[CLappin]

Hi Clifford,

I'm attempting to integrate a rocket chip core to riscv-formal.
I've run "python3 ../../checks/genchecks.py" successfully.
When I run "make -C checks -j2", the initial test runs for about 2 minutes, console output below.
Any help with the errors below would be greatly appreciated.

Kind Regards,
Ciaran

Console Output
SBY [causal_ch0] engine_0: ## 115 0:01:55 Warmup failed!
SBY [causal_ch0] engine_0: ## 115 0:01:55 Status: FAILED (!)
SBY [causal_ch0] engine_0: finished (returncode=1)
SBY [causal_ch0] engine_0: Status returned by engine: FAIL
SBY [causal_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:03 (123)
SBY [causal_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:08 (128)
SBY [causal_ch0] summary: engine_0 (smtbmc --presat boolector) returned FAIL
SBY [causal_ch0] summary: counterexample trace: causal_ch0/engine_0/trace.vcd
SBY [causal_ch0] DONE (FAIL, rc=2)
make: *** [causal_ch0/PASS] Error 2
make: *** Waiting for unfinished jobs....
SBY [causal_ch1] engine_0: ## 117 0:01:57 Checking assumptions in step 36..
SBY [causal_ch1] engine_0: ## 117 0:01:57 Warmup failed!
SBY [causal_ch1] engine_0: ## 117 0:01:57 Status: FAILED (!)
SBY [causal_ch1] engine_0: finished (returncode=1)
SBY [causal_ch1] engine_0: Status returned by engine: FAIL
SBY [causal_ch1] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:05 (125)
SBY [causal_ch1] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:09 (129)
SBY [causal_ch1] summary: engine_0 (smtbmc --presat boolector) returned FAIL
SBY [causal_ch1] summary: counterexample trace: causal_ch1/engine_0/trace.vcd
SBY [causal_ch1] DONE (FAIL, rc=2)
make: *** [causal_ch1/PASS] Error 2
make: Leaving directory `/home/user/riscv-formal/cores/MV/checks'
user@user:~/riscv-formal/cores/MV$ make -C checks -j2
SBY [causal_ch0] engine_0: ## 115 0:01:55 Warmup failed!
SBY [causal_ch0] engine_0: ## 115 0:01:55 Status: FAILED (!)
SBY [causal_ch0] engine_0: finished (returncode=1)
SBY [causal_ch0] engine_0: Status returned by engine: FAIL
SBY [causal_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:03 (123)
SBY [causal_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:08 (128)
SBY [causal_ch0] summary: engine_0 (smtbmc --presat boolector) returned FAIL
SBY [causal_ch0] summary: counterexample trace: causal_ch0/engine_0/trace.vcd
SBY [causal_ch0] DONE (FAIL, rc=2)
make: *** [causal_ch0/PASS] Error 2
make: *** Waiting for unfinished jobs....
SBY [causal_ch1] engine_0: ## 117 0:01:57 Checking assumptions in step 36..
SBY [causal_ch1] engine_0: ## 117 0:01:57 Warmup failed!
SBY [causal_ch1] engine_0: ## 117 0:01:57 Status: FAILED (!)
SBY [causal_ch1] engine_0: finished (returncode=1)
SBY [causal_ch1] engine_0: Status returned by engine: FAIL
SBY [causal_ch1] summary: Elapsed clock time [H:MM:SS (secs)]: 0:02:05 (125)
SBY [causal_ch1] summary: Elapsed process time [H:MM:SS (secs)]: 0:02:09 (129)
SBY [causal_ch1] summary: engine_0 (smtbmc --presat boolector) returned FAIL
SBY [causal_ch1] summary: counterexample trace: causal_ch1/engine_0/trace.vcd
SBY [causal_ch1] DONE (FAIL, rc=2)
make: *** [causal_ch1/PASS] Error 2

[cliffordwolf]

The causality check assumes that in the check step (step 35+1 in the default checks.cfg configuration for rocket) the core retires an instruction that writes to a nonzero register. The "Warmup failed" message means that no such trace exists, i.e. it is impossible for the core to retire such an instruction at this time.

Usually in such cases the problem isn't the nonzero destination register but that the core simply isn't capable to retire any instructions in that cycle, for example because it is still busy with its reset sequence. Impossible to tell anything beyond that without the information necessary to reproduce the issue.

[CLappin]

Thank Clifford, I'll keep working on it and get back to you. I think it has to do with the set up of my rocket core vs your example rocket core.

[CLappin]

I'll close this for now 👍