SPIN verification (PoC)#4452
Draft
rw1nkler wants to merge 15 commits into
Draft
Conversation
Applies a patch to SPIN adding JSON channel-event trace output (-Q flag). Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
Adds TraceChannelProto to EvaluatorResultsProto; bytecode emitter and interpreter record channel send/receive events. Adds --trace_channels and --output_results_proto flags to interpreter_main. Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
PromelaGenerator (DfsVisitorWithDefault) translates XLS IR to Promela. TraceCompare verifies per-channel event sequences between SPIN and DSLX. Includes public and private Bazel rules and testdata golden fixtures. Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
promela_main: IR -> Promela dslx_trace_filter: EvaluatorResultsProto -> JSON channel events promela_trace_compare: SPIN vs DSLX trace diff Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
Adds entry point for invoking spin for guided and exhaustive simulation Guided simulation generates Promela, drives SPIN along the DSLX interpreter trace and compares per-channel events. Exhaustive simulation runs SPIN -search for exhausitve search of the state space. Adds --spin_guided/--spin_exhaustive to interpreter_main and xls_dslx_test. Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
Signed-off-by: Robert Winkler <rwinkler@antmicro.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds experimental SPIN model checker integration for XLS DSLX designs.
The core of the implementation consists of:
promela_generator, which converts XLS IR into a Promela model,spin_runner, which serves as the entry point for running SPIN verification from theinterpreter_maintrace_compare, which compares execution traces produced by SPIN and the DSLX interpreter.The integration supports two modes:
This PR also includes Bazel rules for integrating and experimenting with SPIN verification directly in build targets.
More information about the general implementation can be found in the README.
There are also example designs in the
examples/directory, which include demonstration of SPIN integration and show how to enable and run both guided and exhaustive verification modes.The last step before marking this as ready for review is updating the
trace_comparemechanism to correctly handle hierarchical designs and to include trace dumping along channel instantiation paths, ensuring comparisons remain accurate in more complex module structures.