search

SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
572 stars 94 forks source link

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

Open weedmank opened 4 years ago

weedmank commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

Thanks! I'll look at this tomorrow

On Jan 8, 2020, 11:07 PM, at 11:07 PM, Tobias Woelfel notifications@github.com 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: https://github.com/SymbioticEDA/riscv-formal/issues/34#issuecomment-572422402

weedmank commented 4 years ago

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 https://github.com/SymbioticEDA/riscv-formal/issues/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 commented 4 years ago

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.