3 ms·
State machines can be metaprogrammed: https://github.com/mratsim/Synthesis https://github.com/mratsim/Synthesis You describe the events, transitions and even i
by mratsim 6y ago
State machines can be metaprogrammed: https://github.com/mratsim/Synthesis https://github.com/mratsim/Synthesis
You describe the events, transitions and even interrupts and this compiles to optimized goto statements with no allocation, no indirect function calls, no switch statement.
There are compile-time checks to make sure you don't have state with no transition from and it also produce a visual graph of your state and transitions.
It's been tuned to be used as the core of my high performance multithreading runtime so zero overhead compared to handwritten.
It is suitable for any state machine with zero alloc constraint and state machines can be composed (they are just a function).
I hope in the future to be able to add model checking using Nim Z3 integration so that we can reach Ada/Sparks formal verification prowess: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222
- mhh__ 6y agoI've seen people do similar things in D (although the "D way" of doing it would probably be to parse some kind of textual description and turn it into code at compile time). The cost/benefit of making a metaprogramming library just to write a lexer is fairly bad, however. wrt to the SMT integration, it's something that I would very much like to try in D, but it's quite difficult to work out exactly where to start (and means bolting a fairly big dependency on the compiler). There also seems to be a big gap in the literature between "practical" verification done "in" the widget being verified (e.g. SystemVerilog code) and more academic work where, effectively, a parallel structure is built which represents the semantics of the widget.
- mratsim 6y agoFor a lexer/parser you should use a coroutine / suspendable function abstraction. Or a parser generator.