General Kenobi
Greetings.
My name is Bo Purtell, and I’m an aspiring senior at the University of Florida.
Wanted to share a little project I’ve been working on over the course of the last year being a small networking stack for the hardcaml ecosystem for hardware development with OCaml! The project is still in it’s infancy stages right now, but I’ve validated out a 10/100Mb duplex interface with very loose IPv4 and UDP support, and I’m currently wrapping up a PCS layer for 64/66b BASE-R encodings for 10G applications. A tad limited with my servers getting moved all the way back to Florida (from Cali) though, and I lost one of my regression machines in the move so going to have to go dive into docker stuff again - bleh.
It’s All Math
I fear that I cannot go back to writing SystemVerilog the same way anymore given the wonderful levels of abstraction that I was able to get away with in OCaml. I firmly believe that my thinking of how “state” is represented, and the fact that I could reach for mathematical terminology when I went to describe an OCaml construct helped me immensely in being able to reason about some of these systems as I was constructing them. Helps with verification to an extent too.
Challenges
The biggest challenge I faced was the structuring of my verification suites and testing. There are a few floating hardcaml projects around, but trying to integrate around the expect test framework was a tad difficult since said examples are quite poor in demonstrating re-usable architecture or integration testing. I had thoughts that Alcotest might be used for larger integration suites, but I feel it’s philosophy goes against what a standard expect test is even shooting at doing. Ultimately, expect tests pushed me to Emacs (from Neovim), as expect tests and tuareg fit nicely together - if I had to go pasting s-expressions again from the terminal I probably would’ve imploded. The change is definitely interesting, but well worth it in terms of configurability and OCaml support.
Quickcheck tests were quite nifty as well, but I was flying completely blind on using those, as there are seldom examples for any properly-sized projects release. It was nice to see that alot of my own UVM-based idioms that I am familiar with translated somewhat well with the Observation.t and Snapshot.t formations, but it would still be nice to see what actual production-grade hardcaml verification looks like. Wish there were formal verif examples as well as I have been firmly grasped by the formal-verif-bug, but only a few dronings in dead branches were all I could muster.
In Space!
Truly a bummer that no functional languages will ever see industry use. With that in mind, after wrapping up a double-internship stint Spring & Summer I can finally claim that some nonzero amount of Hardcaml is flying in Space!
If anyone has any questions feel free to shoot me a message here or on LinkedIn!
PS : if anyone is familiar with proper hardcaml-based verification, could I beg for a quick chat on how integration tests would even work with expect systems? Do I just chuck a gigantic 300-line s-expression into the expected field? Surely not. Does Alcotest even enter the vocabulary for such things then?