I'm currently encountering significant difficulties using Verilator to write some integration tests for the Kestrel's SIA (Serial Interface Adapter) core.  Formal verification says everything should work, but Verilator is giving completely different results.

Some external help from ZipCPU suggests that the problem lies in the specific subset of Verilog I'm using to write my core's logic, so I'll be looking to retrofit the cores as time permits.  Unlikely to be this week or next, though, due to holidays.  Hopefully, I can get some time in to fix this before December though, as I'll be busy with a whole new set of holidays!