firrtl-spec icon indicating copy to clipboard operation
firrtl-spec copied to clipboard

Published 20 hours ago • verified publisher icon chipsalliance

Introduce LTL as a part of firrtl specification

Open sequencer opened this issue 1 year ago • 2 comments
trafficstars

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.

sequencer avatar Dec 01 '23 19:12 sequencer

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?

seldridge avatar Dec 01 '23 20:12 seldridge

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

mmaloney-sf avatar Dec 02 '23 19:12 mmaloney-sf