Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce LTL as a part of firrtl specification #157

Open
sequencer opened this issue Dec 1, 2023 · 2 comments
Open

Introduce LTL as a part of firrtl specification #157

sequencer opened this issue Dec 1, 2023 · 2 comments

Comments

@sequencer
Copy link
Member

Since Chisel has supported LTL via intmodule, I think it might be a good idea to upstream LTL as a part of firrtl spec. This cleans up the fir file generation, and makes LTL->SVA flow more clean and elegant.

@seldridge
Copy link
Member

Possibly or possibly this becomes the "verification" section of the spec. @mmaloney-sf had already identified that many of the "commands" (https://github.com/chipsalliance/firrtl-spec/blob/dcd63187d99a923b67caec597e374b8e400f070b/spec.md#commands) are all really verification-only operations. Extending this to support LTL may make sense.

@mmaloney-sf and @fabianschuiki, thoughts?

@mmaloney-sf
Copy link
Collaborator

Currently, all commands and the read statement are part of a (yet-unspecified) Verification superset of FIRRTL. I'm working to formalize this in the spec.

I wouldn't mind a proposal on how to include LTL into FIRRTL. I believe this is more a new kind of verification-only declaration than a set of LTL commands. (Although we probably still consider them statements in the grammar).

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

No branches or pull requests

3 participants