Hello everyone,
I have started to think of the formalization of the virtIO specification. Roughly speaking, I could use a formal language to "code" the virtIO spec. As far as I can think, this has three benefits:Â
1. You can validate any implementation.
2. You can generate the implementation for a given target. For example, you could be able to generate the implementation of a virtIO device in VHDL.Â
3. You can provide simulation and verification before any implementation. In automotive, this is interesting because you ease the certification so formalization pays off.Â
Do you think this may be interesting work to do to become the virtIO specification more robust?Â
Regards, Matias.   Â