@User Thank you! My email address is nevans@sandia.gov . This is all extremely useful, there’s a strong interest in formal both for hardware and software designs at Sandia. The main thing stopping us has been system verilog support. We’ve gotten around that with Verific but the UHDM work looks extremely promising. Especially if it’s easier to trace counter examples in the generated FSMs.