Formal methods and MyHDL


Is anyone using formal methods to verify their models written in MyHDL? Care to share your tools and workflow?


I am not aware of anyone using formal methods with myhdl (or python software development in general).

In general, although not a formal verification technique - more of direct testing, I would use coverage and make sure you are fully testing, and possibly look into hypothesis.

I would look to the Python software world (not the HDL world) for formal methods and how to apply these to myhdl.


Thanks for the link to Hypothesis. I had not heard of it before, but I can see immediate uses for it in any Python code, not just MyHDL. A while back I tried to search for use of formal methods in Python, but came away empty-handed. Thus I started to wonder whether someone had tried combining MyHDL with, for example, SymbiYosys.