I just wrote and posted this article on ZipCPU.com about how to formally verify an AXI-lite peripheral using SymbiYosys. The example peripheral was the demo IP created by Vivado 2016.3. The property set works with the freely downloadable version of SymbiYosys. I'm posting here because I believe this community may be one of the most interested in it.
Feel free to share any comments below if you would like.