Introduce LTL as a part of firrtl specification

chipsalliance / firrtl-spec

The specification for the FIRRTL language

38 stars 27 forks source link

Introduce LTL as a part of firrtl specification #157

Open sequencer opened 9 months ago

sequencer commented 9 months ago

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 commented 9 months ago

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 commented 9 months ago

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).