[ExportVerilog] Add LTL and Verif dialect support #5256
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
238451a to
82d7590
Compare
717a63c to
845b24d
Compare
82d7590 to
580a15a
Compare
dtzSiFive
reviewed
May 25, 2023
Yes this would be great 👍 . |
dtzSiFive
reviewed
May 25, 2023
c1dad90 to
1f22d7e
Compare
845b24d to
3e7ed1d
Compare
darthscsi
approved these changes
May 25, 2023
|
Looks awesome, great work! Maybe in the future we might want to introduce a variable declaration into LTL and spill multiply used expressions. Since currently all the expressions are expanded, it's easy to construct exponential example. Though I guess it's a bit artificial but it could be a problem when we started using LTL heavily, e.g: hw.module @Sequences(%a: i1) {
%0 = ltl.concat %a, %a : i1, i1
%1 = ltl.concat %0, %0 : !ltl.sequence, !ltl.sequence
%2 = ltl.concat %1, %1 : !ltl.sequence, !ltl.sequence
%3 = ltl.concat %2, %2 : !ltl.sequence, !ltl.sequence
%4 = ltl.concat %3, %3 : !ltl.sequence, !ltl.sequence
%5 = ltl.concat %4, %4 : !ltl.sequence, !ltl.sequence
verif.assert %5 : !ltl.sequence
hw.output
}current output: assert property (a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0
a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0
a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0
a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0
a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0 a ##0
a ##0 a ##0 a ##0 a); |
3e7ed1d to
e62a2b3
Compare
1f22d7e to
3b0036e
Compare
|
Haha nice one @uenoku! I hadn't thought of passing the same value multiple times to concat to create an exponential blow-up in the output. You're totally right, we should introduce a property and sequence declaration op that can be used to move the definitions behind a name. Then Added #5286 to track this. |
Add support for emitting the assert, assume, and cover ops from the `verif` dialect, and property and sequence expressions from the `ltl` dialect directly in ExportVerilog. In the future we may want to build up AST-like ops in the SV dialect for this, simplify ExportVerilog, and add a lowering from Verif/LTL to SV separately. Doing so would allow us to do more involved conversions and leverage more syntactic sugar upon emission, and would declutter ExportVerilog. In their current form the LTL and Verif dialects are simple enough to emit directly though, so this is what this commit does for now. The new `verif` assert-like ops can be used either in a procedural region, where they will emit as immediate `assert(x)` when possible, or a graph region like a module, where they will emit as `assert property`. We'll be able to add lowering options later to have more control over which flavor of assertions we want. The properties and sequences in Verilog form a separate kind of expression tree that doesn't really mix with boolean expressions all that much. Therefore, this commit introduces a new `PropertyEmitter` inspired by the `ExprEmitter` which handles property and sequence expression trees.
3b0036e to
fe3224d
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add support for emitting the assert, assume, and cover ops from the
verifdialect, and property and sequence expressions from theltldialect directly in ExportVerilog. In the future we may want to build up AST-like ops in the SV dialect for this, simplify ExportVerilog, and add a lowering from Verif/LTL to SV separately. Doing so would allow us to do more involved conversions and leverage more syntactic sugar upon emission, and would declutter ExportVerilog. In their current form the LTL and Verif dialects are simple enough to emit directly though, so this is what this commit does for now.The new
verifassert-like ops can be used either in a procedural region, where they will emit as immediateassert(x)when possible, or a graph region like a module, where they will emit asassert property. We'll be able to add lowering options later to have more control over which flavor of assertions we want.The properties and sequences in Verilog form a separate kind of expression tree that doesn't really mix with boolean expressions all that much. Therefore, this commit introduces a new
PropertyEmitterinspired by theExprEmitterwhich handles property and sequence expression trees.