search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
407 stars 148 forks source link

How to generate a reference ISA model in SystemVerilog? #503

Closed SeddonShen closed 8 hours ago

SeddonShen commented 2 days ago

Can this project generating a reference ISA model in SystemVerilog now? In the Readme it says that this work is in progress, are there any milestones? Thanks!

Timmmm commented 1 day ago

There's some support but it's incomplete. For example loops aren't implemented. I believe it has been used for some formal equivalence checking but I'm not sure of the details.

Alasdair commented 1 day ago

It's available on the current development branch of Sail. It's in a bit of a transitional state right now as we implement support for generating systemverilog using modules as an alternative to a more procedural style, as well as refactoring the translator to improve its capabilities.

A previous version prior to this refactoring was able to generate a complete translation of this model (prior to the addition of the vector extension, which complicates things greatly). We also had a complete CHERI translation we used for verification. Hopefully soon I will be able to polish the new implementation and get it tested on the current model (But probably not before the POPL deadline this month...). Loops were handled by unrolling.

SeddonShen commented 8 hours ago

Ok, thx!!!