Skip to content

[feat] parameterized roundrobin arbiter#17

Open
Sparsa wants to merge 1 commit intoVerilean:mainfrom
Sparsa:main
Open

[feat] parameterized roundrobin arbiter#17
Sparsa wants to merge 1 commit intoVerilean:mainfrom
Sparsa:main

Conversation

@Sparsa
Copy link
Copy Markdown

@Sparsa Sparsa commented Mar 27, 2026

Hi, I am really interested in this project of yours. I am just starting up Lean, and I believe there is a huge potential of its use in the hardware verification domain. Currently, I am working as a verification engineer, where I am trying to create a testbench where I will write specs in lean, prove it there, and then use it as a golden model for bisimulation with the RTL. I got to know about this repo yesterday, and was playing around it. The easiest entry point was the arbiter. I tried to implement the arbiter for any parameterized number of clients.

But, I guess I have used some constructs that is not supported yet, so that we can get a Verilog code as output.

Another thing that I noticed that the Simulation test is not actually testing the implementation with the spec. It just running the spec. So I tried to tweak it a bit so that I can compare these two. But due to my limited knowledge its not working.

So I thought of creating this pull request. I am learning here, so any help would be appreciated.

Thanks,
Sparsa

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant