search

rems-project / sail

Sail architecture definition language
Other
622 stars 116 forks source link

SystemVerilog Generation from Sail-RISC-V Description Hangs or Crashes #728

Closed NicolasVanPhan closed 1 month ago

NicolasVanPhan commented 1 month ago

Description:

I'm encountering an issue when attempting to generate SystemVerilog from the Sail-RISC-V description using the Sail compiler. The process either runs indefinitely (after approximately 45 minutes) or crashes with a stack overflow error (after around 10 minutes).

Steps to Reproduce:

I added the following Makefile target 

riscv.sv_model: $(SAIL_SRCS)
       $(SAIL) -sv $(SAIL_FLAGS) $(SAIL_SRCS) -o riscv

Then ran this target :

make SAIL=~/sail/sail riscv.sv_model

Observed Behavior:

One of the two happen randomly :

System Information:

Logs

In attachment is the output of the make when run with -verbose 100. log.txt

Any help or guidance on how to resolve or further debug this issue would be greatly appreciated.

Alasdair commented 1 month ago

The SystemVerilog generation is very much a work in progress at the moment.

Just applying it directly to the RISC-V model does not work out of the box right now. In particular you need to modify the RISC-V model to annotate loops (among other things), and more work needs to be done to support the vector extension fully. Without those annotations, it'll just get lost in the complexity created by unrolling all the loops naively - this is probably what you are observing.

I think it will still be a few months before the generation will be in a state where you can apply it to the RISC-V model as is and get something that works, and I'll likely have to upstream some changes to the model.

NicolasVanPhan commented 1 month ago

Thanks for your quick response !

Actually I can't manage to generate a C emulator neither, the same problem happens. The generation keeps running after half an hour and nothing gets generated.

It must be an internal problem in my environment setup I guess.

Alasdair commented 1 month ago

That's odd. It might take a little while the first time you generate the C emulator, but it shouldn't be that long - once it's cached all the solver queries it should rebuild quickly with make -B csim or similar. make clean deletes all the caching so I don't recommend doing that too often.

NicolasVanPhan commented 1 month ago

I rebuilt sail after a opam install . to make sure I have packages to the correct version. And I removed the -verbose 100 from the build. With this, I successfully built the C emulator within a minute.

However I still couldn't build the SystemVerilog, it crashed after 10 minutes with the following error message : log.txt I guess it falls into the issue you mentioned above, with the too many loop unrolling.

I saw the following successful attempt at generating SV from Sail
https://github.com/microsoft/cheriot-ibex and was wondering why it couldn't work on the raw RISC-V model. Could you please provide some pointers to better understand what should be done in terms of annotations ?

Alasdair commented 1 month ago

The CHERIoT architecture has a few things that made it quite a bit simpler than the full RISC-V model. Because it's an embedded processor for IoT type devices, it doesn't have address translation (the recursive address translation walk could also be what's hanging it right now, although I did add bounded mutual recursion support recently), and it doesn't have the vector extension. In fact, it didn't have any loops or recursion in any instructions.

We used a much earlier version of the translator, and we got some feedback as to the kind of SystemVerilog we should be producing - that led me to essentially rebuilding the translator with a much more sophisticated approach. This means that while we can now translate a lot more of Sail into SystemVerilog, the 'wrapper/harness' we built around the model for our CHERIoT verification no longer applies - we used to just generate only SystemVerilog functions, but now we generate modules or functions, depending on how the Sail function behaves. Some of the annotations you need right now are to tell Sail how it should link to the SystemVerilog primitives either as modules or functions.

It's all very much up in the air as I am building it though, things are likely to change on a whim for at least a while longer. I plan to write documentation for how to use the SystemVerilog generation when it's in a more stable state, but at this stage I don't have anything to point to.

NicolasVanPhan commented 1 month ago

I see, in the meantime I'll retry without the vector extension and without address translation to see how it goes.

Thank you a lot for your clear and quick help !