Not that I know, but clash could serve as a starting (play)ground.
-
-
-
Ohhh, excellent reference, thank you!
-
Really interested to see what you find, I guess you already saw Tom Hawkins stuff? Back in the day I played with his confluence thing (a scheme-ish HDL) and I see he also did something called HDCaml. Really seemed like a promising path back then..
-
No, I didn't. Will check it out!
End of conversation
New conversation -
-
-
gallais in Freenode irc ## dependent cited this: https://joaopizani.gitlab.io/piware/
-
Closest to what I am looking for, thank you very much! (Now it needs to generate Verilog instead of VHDL, and it should make use of *some* form of automated proof search, like in F*, but yeah, it exists!)
End of conversation
New conversation -
-
-
I remember some time ago there was some talk about using OCaml as a HDL. I think it was Hardcaml, never looked into it thought... https://www.ujamjar.com/open-source/ocaml/2014/06/17/hardcaml.html …
-
also http://karl-flicker.at/hdcaml/ but presumably no dependent types.
End of conversation
New conversation -
-
-
See https://people.ece.cornell.edu/af433/publication/mut-deptypes/ … and Andrew Myers’ related papers. Dependent (security) types in an HDL
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.