Adding support for a newRISC-V processor to riscv-formal

[weedmank]

On https://github.com/SymbioticEDA/riscv-formal there's a Table of Contents that gives good information, but I have a new RISC-V CPU I want to try to test and need to know the procedure to create a folder and whatever else to be able to test it. This would be a good webpage addition to have for those of us wanting to test new CPUs. I finally found some info on page 15 of http://www.clifford.at/papers/2017/riscv-formal/slides.pdf. It gives a little info and says "Write a genchecks.cfg config file for the new core–See cores/picorv32/ and cores/rocket/ for examples" Problem is, I can't find the genchecks.cfg file in either folder. More info on what should go in genchecks.cfg would be appreciated.

[towoe]

Hi @weedmank, I do not have a description but I worked on integrating Ibex and in my fork there is a branch https://github.com/towoe/riscv-formal/tree/ibex with all the latest commits related to adding the core. Maybe this is helpful to you.
And I guess the genchecks.cfg is now checks.cfg.

[weedmank]

Thanks! I'll look at this tomorrow

…

On Jan 8, 2020, 11:07 PM, at 11:07 PM, Tobias Woelfel ***@***.***> wrote: Hi @weedmank, I do not have a description but I worked on integrating Ibex and in my fork there is a branch https://github.com/towoe/riscv-formal/tree/ibex with all the latest commits related to adding the core. Maybe this is helpful to you. And I guess the `genchecks.cfg` is now `checks.cfg`. -- You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: #34 (comment)

[weedmank]

OK. I looked. In your wrapper.sv, what are you going to do with all the instr_xxxx and data_xxxx signals. I too have similar signals but they’re tailored to connect to L1 instruction and data caches I’ve created. Is memory supposed to be instantiated inside the wrapper for this setup??? Or is it ignored? If ignored, what to do with signal that go into the cpu core? This is where I’m stuck with this project as to what to do. Thanks Kirk From: Tobias Woelfel [mailto:notifications@github.com] Sent: Wednesday, January 8, 2020 11:07 PM To: SymbioticEDA/riscv-formal Cc: Kirk Weedman; Mention Subject: Re: [SymbioticEDA/riscv-formal] Adding support for a newRISC-V processor to riscv-formal (#34) Hi @weedmank <https://github.com/weedmank> , I do not have a description but I worked on integrating Ibex and in my fork there is a branch https://github.com/towoe/riscv-formal/tree/ibex with all the latest commits related to adding the core. Maybe this is helpful to you. And I guess the genchecks.cfg is now checks.cfg. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#34?email_source=notifications&email_token=ALJF6PUIHIZ4A6FJWGGR7ILQ43EKNA5CNFSM4KCGHGVKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEIPHSAQ#issuecomment-572422402> , or unsubscribe <https://github.com/notifications/unsubscribe-auth/ALJF6PX3J5S4ADKEVRQ6M6LQ43EKNANCNFSM4KCGHGVA> . <https://github.com/notifications/beacon/ALJF6PRIE6WQGHR7FKIHTULQ43EKNA5CNFSM4KCGHGVKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEIPHSAQ.gif>

[towoe]

OK. I looked. In your wrapper.sv, what are you going to do with all the instr_xxxx and data_xxxx signals. I too have similar signals but they’re tailored to connect to L1 instruction and data caches I’ve created. Is memory supposed to be instantiated inside the wrapper for this setup??? Or is it ignored? If ignored, what to do with signal that go into the cpu core? This is where I’m stuck with this project as to what to do. Thanks Kirk

Those instr_* and data_* signals are connect in order to get data into the core. This is the same as in picorv32 where, with the define, the input signals are marked with rand.
As this riscv-formal is checking the core itself, the memory details can be omitted.
So: only instantiate your core and connect the input signals with signals created with rand in your wrapper.