test generation via Sail spec

[eistar]

I am tring to find out if there's a backend of Sail can generate tests based on specifications in Sail. From the homepage, it seems that test generation is already supported:

support automated instruction-sequence test generation from the specification in ways that get good specification coverage, using the Isla SMT-based symbolic evaluation engine for Sail

But I cannot find any further information about the options for this purpose. Could you please point me to the related information?

Thanks!

[bacam]

The project is at https://github.com/rems-project/isla-testgen and was used for testing of our Morello and x86-64-from-acl2 specifications. It's very much research-grade software and is likely to need updated for use with current versions of the Sail and Isla tools, although it should be possible to get it running with the exact versions in the README file.

I'd be happy to answer any questions you have about it, although I'm going to be away until the 11th September so it might be a while before I'm able to answer.

[eistar]

Many thanks for the information!
I will try it. Before you return, I'll also work on understanding the underlying principles of the project.