translation to SMV

This is based on `murphi2uclid`. But unlike Uclid5 translation, this is much
more rough. The semantics and structure of SMV are sufficiently different that
an automatic translation would be more like a compiler than the AST-walking
strategy employed by the `murphi2*` tools. It does not seem worth undertaking
something this ambitious until we get some experience in whether this
translation is useful.

The translation gives up in numerous scenarios. But it should be more usable
once we implement the ability to ingest partial Murphi models.