It should be quite possible to validate this way, although I would need to implement more ISA specific fences and features.
As mentioned in a sibling comment, I've moved away from the idea of building a model in Clojure and implementing separately, to a system in Rust where the model is the program with a compile time switch.
There were too many ways to introduce careless errors when doing a port. Although the opposite approach would have been to ingest compiled programs directly, or move to something higher level like WASM (once it gets more than SeqCst atomics).
As mentioned in a sibling comment, I've moved away from the idea of building a model in Clojure and implementing separately, to a system in Rust where the model is the program with a compile time switch.
There were too many ways to introduce careless errors when doing a port. Although the opposite approach would have been to ingest compiled programs directly, or move to something higher level like WASM (once it gets more than SeqCst atomics).