diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-26 16:00:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-26 16:00:19 +0100 |
commit | 08af8ab3c28b61af546be6848ff971373d757ad5 (patch) | |
tree | 2a6ee9cccbc3e578ea12b622a26fd7dcbbdc681c /verilog_notes.tex | |
parent | 2b4120e11a290a71861147fd92d877253955a152 (diff) | |
download | oopsla21_fvhls-08af8ab3c28b61af546be6848ff971373d757ad5.tar.gz oopsla21_fvhls-08af8ab3c28b61af546be6848ff971373d757ad5.zip |
Add minted code block
Diffstat (limited to 'verilog_notes.tex')
-rw-r--r-- | verilog_notes.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/verilog_notes.tex b/verilog_notes.tex new file mode 100644 index 0000000..99f7e24 --- /dev/null +++ b/verilog_notes.tex @@ -0,0 +1,8 @@ +\JW{stmtntrun has four parameters, and if I read the rules correctly, it looks like the fourth parameter is uniquely determined by the first three. So, you could consider presenting stmntrun simply as a recursive definition, e.g. `stmntrun f s Vskip = s', `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2', and so on. That might (\emph{might}) be easier to read than the inference rule format.} + +\YH{It works well for Seq and Skip, but I think that CaseMatch and CaseNoMatch, or even if statements will be a bit clunky? We would have to use case statements in the function to do different things +based on what they evaluate to. For case I think that would end up being a three way choice. I'll try it out though and see how nice it is.} + +\JP{I suppose this would essentially be an ``interpreter'' style semantics but we can prove equivalence pretty easily.} + +\YH{To add to that, I used to have both in the Coq code, but commented the recursive definition out, and now only have the inductive definition, which is basically what I copy pasted here.} \JW{Fair enough. Whatever you think ends up being the easiest to read and understand, really. There's something to be said for staying close to the Coq definitions anyway.} \YH{I have added more rules, we can always switch from one to the other now. One more thing I noticed though is that recursive definitions will need an \texttt{option} type.} \JW{Oh, then my suggestion of `stmntrun f s0 (Vseq st1 st2) = stmntrun f (stmntrun f s0 st1) st2' is a bit ill-typed then, unless the second parameter becomes option-typed too. Maybe the inference rules are better overall then.} \YH{Ah yes, I actually didn't even notice that, it would need the do notation, just like the implementation in Coq, so it may be easier to just use the inference rules.} |