RVProbe

[Clo91eaf]

modified and refactored from #42

[Copilot]

Pull Request Overview

This PR adds comprehensive SMT-based constraint solving and test generation infrastructure for RISC-V instruction verification. The changes include:

• SMT parser enhancements for negative integers and model representation changes
• New SMT operators (smtAnd, smtOr) and API improvements (variadic parameters)
• Auto-generated constraint definitions for RISC-V instructions and extensions
• Test infrastructure with MLIR and SMTLIB output verification
• Sample application for RV32I instruction generation

Reviewed Changes

Copilot reviewed 17 out of 19 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
smtlib/src/SMTParser.scala	Adds negative integer parsing and changes model from Seq to Map
smtlib/src/Api.scala	Adds smtAnd, smtOr operators and changes parameters to variadic
smtlib/src/DefaultOperators.scala	Implements new operators and adds smtValue overload with explicit naming
smtlib/tests/src/ParseSpec.scala	Updates tests to use Map instead of Seq for Z3Result model
smtlib/tests/src/CoreSpec.scala	Adds comprehensive tests for smtAnd and smtOr operators
rvprobe/src/constraints/RVConstraints.scala	Auto-generated constraint definitions (1440 lines)
rvprobe/src/RVDecoderdbApi.scala	Helper functions for instruction and extension retrieval
rvprobe/src/scripts/*.scala	Code generators for constraints from instruction databases
rvprobe/tests/src/*.scala	Test infrastructure and comprehensive recipe tests
rvprobe/src/apps/RV32I.scala	Sample application demonstrating instruction generation
flake.nix	Increases JVM stack size for compilation

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.