From 50e30b2eeee1e8f710c850b62e73dcca7bff61ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 22 Sep 2026 15:50:38 -0400 Subject: [PATCH 01/15] wip functional models --- functional-models/README.md | 0 functional-models/fun.py | 36 ++++++++++++++++++++++++++++++++ functional-models/main.py | 33 +++++++++++++++++++++++++++++ functional-models/pyproject.toml | 7 +++++++ pyproject.toml | 5 +++++ uv.lock | 11 ++++++++++ 6 files changed, 92 insertions(+) create mode 100644 functional-models/README.md create mode 100644 functional-models/fun.py create mode 100644 functional-models/main.py create mode 100644 functional-models/pyproject.toml diff --git a/functional-models/README.md b/functional-models/README.md new file mode 100644 index 00000000..e69de29b diff --git a/functional-models/fun.py b/functional-models/fun.py new file mode 100644 index 00000000..7b0fd071 --- /dev/null +++ b/functional-models/fun.py @@ -0,0 +1,36 @@ +from dataclasses import dataclass, field +from pypatronus import TransitionSystem, BitVec + +@dataclass +class FunctionalModel: + name: str + transactions: list = field(default_factory=list) + states: list = field(default_factory=list) + +@dataclass +class Transaction: + name: str + inputs: list = field(default_factory=list) + outputs: list = field(default_factory=list) + state_updates: list = field(default_factory=list) + + +def verify_model(m :FunctionalModel): + for transaction in m.transactions: + assert len(transaction.state_updates) == len(m.states) + for output in transaction.outputs: + # TODO: check symbols + pass + +def serialize(m :FunctionalModel): + verify_model(m) + + inputs = [] + enables = [] + for t in m.transactions: + inputs.append(BitVec(f"{t.name}_enable", 1)) + enables.append(inputs[-1]) + for inp in t.inputs: + inputs.append(BitVec(f"{t.name}_in_{inp.name}", 1)) + + sys = TransitionSystem(name=m.name) \ No newline at end of file diff --git a/functional-models/main.py b/functional-models/main.py new file mode 100644 index 00000000..0a4ba0c9 --- /dev/null +++ b/functional-models/main.py @@ -0,0 +1,33 @@ +# Copyright 2026 Cornell University +# released under MIT License +# author: Kevin Laeufer + +from pypatronus import BitVec, SignExt, ZeroExt, Slice +from fun import FunctionalModel, Transaction, serialize + + +def picorv32_pcpi_mul(): + """ + https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/picorv32/PicoRV32Spec.scala#L8 + """ + m = FunctionalModel(name="picorv32_pcpi_mul") + rs1, rs2 = BitVec('rs1_data', 32),BitVec('rs2_data', 32) + m.transactions = [ + Transaction("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]), + Transaction("pcpi_mulh", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))]), + Transaction("pcpi_mulhu", [rs1, rs2], [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))]), + Transaction("pcpi_mulhsu", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))]), + ] + return m + + + +def main(): + m = picorv32_pcpi_mul() + print(m) + serialize(m) + + + +if __name__ == "__main__": + main() diff --git a/functional-models/pyproject.toml b/functional-models/pyproject.toml new file mode 100644 index 00000000..ac87f047 --- /dev/null +++ b/functional-models/pyproject.toml @@ -0,0 +1,7 @@ +[project] +name = "functional-models" +version = "0.1.0" +description = "Add your description here" +readme = "README.md" +requires-python = ">=3.12" +dependencies = [] diff --git a/pyproject.toml b/pyproject.toml index 83fd56f5..c7b57668 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -11,3 +11,8 @@ dev = [ "ruff>=0.15.1", "ty>=0.0.17", ] + +[tool.uv.workspace] +members = [ + "functional-models", +] diff --git a/uv.lock b/uv.lock index f1f647a9..6d40e155 100644 --- a/uv.lock +++ b/uv.lock @@ -2,6 +2,17 @@ version = 1 revision = 3 requires-python = ">=3.12" +[manifest] +members = [ + "functional-models", + "protocols", +] + +[[package]] +name = "functional-models" +version = "0.1.0" +source = { virtual = "functional-models" } + [[package]] name = "protocols" version = "0.1.0" From e64d60e46577e2c7c7d0df0d7120e3c271e28b9f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 23 Sep 2026 12:05:20 -0400 Subject: [PATCH 02/15] functional model for multiplier --- .gitignore | 4 ++- functional-models/README.md | 4 +++ functional-models/fun.py | 47 ++++++++++++++++++++++++-------- functional-models/main.py | 24 +++++++++++----- functional-models/pyproject.toml | 4 ++- uv.lock | 30 ++++++++++++++++++++ 6 files changed, 92 insertions(+), 21 deletions(-) diff --git a/.gitignore b/.gitignore index 3b1ae089..679459d0 100644 --- a/.gitignore +++ b/.gitignore @@ -31,7 +31,9 @@ run_dir/ # Archived catalog-generation logic (kept locally, not checked in) scripts/_catalog_gen.py -scripts/__pycache__/ + +# Python +__pycache__ # Include images of waveforms in Brave New World bug readme !tests/fpga-debugging/axis-async-fifo-c4/*.png diff --git a/functional-models/README.md b/functional-models/README.md index e69de29b..d3317f10 100644 --- a/functional-models/README.md +++ b/functional-models/README.md @@ -0,0 +1,4 @@ +# Functional Models + +Define your functional model in `main.py`, export to JSON and +then load it using the rust library. diff --git a/functional-models/fun.py b/functional-models/fun.py index 7b0fd071..8755b954 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -1,12 +1,15 @@ +import json from dataclasses import dataclass, field from pypatronus import TransitionSystem, BitVec + @dataclass class FunctionalModel: name: str transactions: list = field(default_factory=list) states: list = field(default_factory=list) + @dataclass class Transaction: name: str @@ -15,22 +18,42 @@ class Transaction: state_updates: list = field(default_factory=list) -def verify_model(m :FunctionalModel): +def verify_model(m: FunctionalModel): + assert len(m.states) == 0, "TODO: deal with states" for transaction in m.transactions: assert len(transaction.state_updates) == len(m.states) - for output in transaction.outputs: - # TODO: check symbols - pass + allowed_symbols = set(m.states) | set(transaction.inputs) -def serialize(m :FunctionalModel): - verify_model(m) + for out_name, out_expr in transaction.outputs: + unallowed = out_expr.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"Output {out_name} uses symbols that are neither inputs nor state: {unallowed}" + ) - inputs = [] - enables = [] + +def serialize(m: FunctionalModel, filename): + assert len(m.states) == 0, "TODO: deal with states" + verify_model(m) + sys = TransitionSystem(name=m.name) for t in m.transactions: - inputs.append(BitVec(f"{t.name}_enable", 1)) - enables.append(inputs[-1]) + commit_signal = BitVec(f"{t.name}_commit", 1) + sys.add_input(commit_signal) + input_map = {} for inp in t.inputs: - inputs.append(BitVec(f"{t.name}_in_{inp.name}", 1)) + renamed = BitVec(f"{t.name}_in_{inp.name()}", inp.width()) + input_map[inp] = renamed + sys.add_input(renamed) + for out_name, out_expr in t.outputs: + out_expr = out_expr.replace(input_map) + sys.add_output(f"{t.name}_out_{out_name}", out_expr) + + transactions = [{"name": t.name} for t in m.transactions] + info = { + "name": m.name, + "transactions": transactions, + "states": [s.name for s in m.states], + "sys": sys.to_btor2_str(), + } - sys = TransitionSystem(name=m.name) \ No newline at end of file + with open(filename, "w") as f: + json.dump(info, f) diff --git a/functional-models/main.py b/functional-models/main.py index 0a4ba0c9..0071c53d 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -11,22 +11,32 @@ def picorv32_pcpi_mul(): https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/picorv32/PicoRV32Spec.scala#L8 """ m = FunctionalModel(name="picorv32_pcpi_mul") - rs1, rs2 = BitVec('rs1_data', 32),BitVec('rs2_data', 32) + rs1, rs2 = BitVec("rs1_data", 32), BitVec("rs2_data", 32) m.transactions = [ Transaction("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]), - Transaction("pcpi_mulh", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))]), - Transaction("pcpi_mulhu", [rs1, rs2], [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))]), - Transaction("pcpi_mulhsu", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))]), + Transaction( + "pcpi_mulh", + [rs1, rs2], + [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))], + ), + Transaction( + "pcpi_mulhu", + [rs1, rs2], + [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))], + ), + Transaction( + "pcpi_mulhsu", + [rs1, rs2], + [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))], + ), ] return m - def main(): m = picorv32_pcpi_mul() print(m) - serialize(m) - + serialize(m, "picorv32_pcpi_mul.json") if __name__ == "__main__": diff --git a/functional-models/pyproject.toml b/functional-models/pyproject.toml index ac87f047..8c1a7d59 100644 --- a/functional-models/pyproject.toml +++ b/functional-models/pyproject.toml @@ -4,4 +4,6 @@ version = "0.1.0" description = "Add your description here" readme = "README.md" requires-python = ">=3.12" -dependencies = [] +dependencies = [ + "pypatronus==0.39.4", +] diff --git a/uv.lock b/uv.lock index 6d40e155..d54dc550 100644 --- a/uv.lock +++ b/uv.lock @@ -12,6 +12,12 @@ members = [ name = "functional-models" version = "0.1.0" source = { virtual = "functional-models" } +dependencies = [ + { name = "pypatronus" }, +] + +[package.metadata] +requires-dist = [{ name = "pypatronus", specifier = "==0.39.4" }] [[package]] name = "protocols" @@ -32,6 +38,30 @@ dev = [ { name = "ty", specifier = ">=0.0.17" }, ] +[[package]] +name = "pypatronus" +version = "0.39.4" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/31/48/247a70b9ea7b07862c31ec169fd6f3ab23521e407a765bc99939f091aa7d/pypatronus-0.39.4.tar.gz", hash = "sha256:774da01f8af5b3b4447054d4b719a4cdd3dd0c8b06541aa38fbf31de4d371015", size = 164797, upload-time = "2026-09-23T15:27:28.082Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/49/c5/3e9953ed91870eda4387113bb8ecd040ebede477483b8801ff8658f2cbb2/pypatronus-0.39.4-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:9335a6fb15cb0a53b5f29d5e55bb090a0fc1cfc4187b7a85c9e7e3cbb01b787f", size = 1353907, upload-time = "2026-09-23T15:27:23.659Z" }, + { url = "https://files.pythonhosted.org/packages/94/8f/24e37b42f7a3580e995550ab23c6e92b28f782845a17dcada1743a321576/pypatronus-0.39.4-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:7e8fd40d25f6d1773a67108401942536230c8751ea56f977617bd1030b4fb288", size = 1304486, upload-time = "2026-09-23T15:27:15.639Z" }, + { url = "https://files.pythonhosted.org/packages/f2/67/ad4f33c1c1d7a41e9ca5ce55a77e01df954ae702cd5fa2cd52f1ef8760e2/pypatronus-0.39.4-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:26c5f4f1f9504f0f1994028d538df2352fc1065c597116a725e89260d0876cfe", size = 11389009, upload-time = "2026-09-23T15:26:33.901Z" }, + { url = "https://files.pythonhosted.org/packages/2c/3a/efa7c4956ed08a5e8adf37d71f0a86ad36c8b69a2e99046f9be5665ae0b5/pypatronus-0.39.4-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:73c20828fc045278c230c3efb531467036cb1eee8699fb51feadf1531c609823", size = 12820150, upload-time = "2026-09-23T15:26:52.236Z" }, + { url = "https://files.pythonhosted.org/packages/ab/55/b6da29d5e5854d418bbaa3a81380718831fa0b683ff0c6d997eb68410e79/pypatronus-0.39.4-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:1b0bffd469615b28d8748d65022c60f826a49fa5cd95198b2c048a13a485768a", size = 1355081, upload-time = "2026-09-23T15:27:25.268Z" }, + { url = "https://files.pythonhosted.org/packages/07/7c/9213a3c4b8a1e84069e3d3c54a1041178c934fb1c0df5a6ab5f0b380f6be/pypatronus-0.39.4-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:829b9bfacb8116c1428ce50cf4ec381fef541d3f6da6bee2a2dfec26f0e7a39a", size = 1304210, upload-time = "2026-09-23T15:27:17.167Z" }, + { url = "https://files.pythonhosted.org/packages/5f/61/a86235251796315a15998c946ccddb6407dc32f3d43a42fa409f55296cc0/pypatronus-0.39.4-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e4ae9ec45854d57a3e9e28565bf2322b6955c1498daf95ceee2367b0b061df58", size = 11375383, upload-time = "2026-09-23T15:26:36.641Z" }, + { url = "https://files.pythonhosted.org/packages/c1/e5/ab2e88dbc8356905eff42693ef56ab765fa7acee45219d4dd57a6fd8b32f/pypatronus-0.39.4-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c71a95c261506f7b1c8c633da1d0c98b0ef5f3f59a85238d9c6792862f9c3c0d", size = 12804551, upload-time = "2026-09-23T15:26:54.943Z" }, + { url = "https://files.pythonhosted.org/packages/41/58/074783e08da59192c778f2306fe1b4c02206bb71276243964e4a2c24dd0f/pypatronus-0.39.4-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:0908bae1784a557c6988212b5069a70b002f5229ec823f56e6533abba243e7ae", size = 1356758, upload-time = "2026-09-23T15:27:26.723Z" }, + { url = "https://files.pythonhosted.org/packages/50/cf/5efdd697772bbf1dee3aef2d326765b00029a908b4189e74b0c61995ecff/pypatronus-0.39.4-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:935ef51c47fd9cb3447c9da3aafbe9cf13baf5a7bfaa09b7cdcde0a1cbb09d6b", size = 1304542, upload-time = "2026-09-23T15:27:18.803Z" }, + { url = "https://files.pythonhosted.org/packages/d6/c9/f5305c838e2ff8df951937f7e3e13b0a730c39b1334a1a15499914a816cf/pypatronus-0.39.4-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f1501a66d6b19914054f5e85f0a36fb4c62408d227bc61850752fc5affca4689", size = 11388751, upload-time = "2026-09-23T15:26:39.401Z" }, + { url = "https://files.pythonhosted.org/packages/c7/e9/ef03f0234bc27d0d467da816e94da53a4240449ab93f4baf25671f5c085d/pypatronus-0.39.4-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9e7d4a1b1a1ea861e77926ff9f61c1ed9185b6fd5aa67ff83877d12139e72029", size = 12819176, upload-time = "2026-09-23T15:26:57.68Z" }, + { url = "https://files.pythonhosted.org/packages/e6/9e/ca47355de00e1ec1212ff236a1efbb2db963f33c637bbfc3060ef8c59a1e/pypatronus-0.39.4-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:281e40fd874ce3f313063c59f12d19b360cdd75e55296cae49fda7532c01edb3", size = 11378886, upload-time = "2026-09-23T15:26:42.026Z" }, + { url = "https://files.pythonhosted.org/packages/b8/9f/2a9e028c01bce830ae6a1a56670eb30236591b318fcafb02c66f642a1f07/pypatronus-0.39.4-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0ae20e59f9c555a18add4e1d8590f2fe36b43783e3a760f7486e6aab860327d2", size = 12808220, upload-time = "2026-09-23T15:27:00.588Z" }, + { url = "https://files.pythonhosted.org/packages/05/69/3858448f6e0c04191f736b5be61eca719c3dbdd774f14eb3d081524c8b99/pypatronus-0.39.4-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8306db067caf115cf139defa9d515f28fe648ca886e47b418c0ec6e8dbc04428", size = 12818469, upload-time = "2026-09-23T15:27:03.576Z" }, + { url = "https://files.pythonhosted.org/packages/79/43/c03116e7e9f2060a2c791386ae70dc838061bad20df10987e8c4517beea1/pypatronus-0.39.4-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5d6a73801c97b4b2fd18e762a9ca9f0c4af5a60f2065501792deb43c33d4a784", size = 12813180, upload-time = "2026-09-23T15:27:06.684Z" }, +] + [[package]] name = "ruff" version = "0.15.1" From c2165ed573805536086d3e815086e514bdd45457 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 23 Sep 2026 15:24:55 -0400 Subject: [PATCH 03/15] wip: functional model Rust library --- Cargo.toml | 2 +- functional-models/Cargo.toml | 18 ++++++++++++++++++ functional-models/src/lib.rs | 31 +++++++++++++++++++++++++++++++ 3 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 functional-models/Cargo.toml create mode 100644 functional-models/src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index fbc34bba..27ff696c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [workspace] resolver = "3" -members = ["bi", "interp", "protocols", "cli", "graph-interp"] +members = ["bi", "functional-models", "interp", "protocols", "cli", "graph-interp"] [workspace.package] diff --git a/functional-models/Cargo.toml b/functional-models/Cargo.toml new file mode 100644 index 00000000..6460853c --- /dev/null +++ b/functional-models/Cargo.toml @@ -0,0 +1,18 @@ +[package] +name = "functional" +version = "0.1.0" +description = "load functional models generated by our python library" +edition.workspace = true +rust-version.workspace = true +repository.workspace = true +license.workspace = true + +[dependencies] +protocols.workspace = true +clap-verbosity-flag = "3.0.4" +clap.workspace = true +baa.workspace = true +patronus.workspace = true +rustc-hash.workspace = true +serde = { version = "1.0.229", features = ["derive"] } +serde_json = "1.0.151" diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs new file mode 100644 index 00000000..c29dd541 --- /dev/null +++ b/functional-models/src/lib.rs @@ -0,0 +1,31 @@ +// Copyright 2026 Cornell University +// released under MIT License +// author: Kevin Laeufer + +use patronus::system::TransitionSystem; +use serde::{Deserialize, Serialize}; +use serde_json::Result; + +#[derive(Debug)] +struct FunctionalModel { + meta: FunctionalModelInfo, + sys: TransitionSystem, +} + +#[derive(Debug, Deserialize, Serialize)] +struct FunctionalModelJson { + meta: FunctionalModelInfo, + sys: String, +} + +#[derive(Debug, Deserialize, Serialize)] +struct FunctionalModelInfo { + name: String, + transactions: Vec, + states: Vec, +} + +#[derive(Debug, Deserialize, Serialize)] +struct Transaction { + name: String, +} From e8c8e258a3885bed0d6a9dbe4b772f5357503438 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 24 Sep 2026 16:24:00 -0400 Subject: [PATCH 04/15] wip: functional models in interpreter --- functional-models/fun.py | 36 ++++--- functional-models/main.py | 12 +-- functional-models/src/lib.rs | 204 +++++++++++++++++++++++++++++++++-- interp/src/main.rs | 4 + 4 files changed, 227 insertions(+), 29 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index 8755b954..ce552cc6 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -1,33 +1,43 @@ import json from dataclasses import dataclass, field -from pypatronus import TransitionSystem, BitVec +from typing import Optional + +from pypatronus import TransitionSystem, BitVec, ExprRef, BitVecVal @dataclass class FunctionalModel: name: str - transactions: list = field(default_factory=list) + methods: list = field(default_factory=list) states: list = field(default_factory=list) @dataclass -class Transaction: +class Method: name: str inputs: list = field(default_factory=list) outputs: list = field(default_factory=list) state_updates: list = field(default_factory=list) + # indicates whether the method can be executed based on state and inputs + guard: Optional[ExprRef] = None def verify_model(m: FunctionalModel): assert len(m.states) == 0, "TODO: deal with states" - for transaction in m.transactions: - assert len(transaction.state_updates) == len(m.states) - allowed_symbols = set(m.states) | set(transaction.inputs) + for method in m.methods: + assert len(method.state_updates) == len(m.states) + allowed_symbols = set(m.states) | set(method.inputs) - for out_name, out_expr in transaction.outputs: + for out_name, out_expr in method.outputs: unallowed = out_expr.symbols() - allowed_symbols assert len(unallowed) == 0, ( - f"Output {out_name} uses symbols that are neither inputs nor state: {unallowed}" + f"Output {out_name}={out_expr} uses symbols that are neither inputs nor state: {unallowed}" + ) + # check guard + if method.guard is not None: + unallowed = method.guard.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"Guard {method.guard} uses symbols that are neither inputs nor state: {unallowed}" ) @@ -35,9 +45,11 @@ def serialize(m: FunctionalModel, filename): assert len(m.states) == 0, "TODO: deal with states" verify_model(m) sys = TransitionSystem(name=m.name) - for t in m.transactions: + for t in m.methods: commit_signal = BitVec(f"{t.name}_commit", 1) sys.add_input(commit_signal) + guard_signal = BitVecVal(1, 1) if t.guard is None else t.guard + sys.add_output(f"{t.name}_guard", guard_signal) input_map = {} for inp in t.inputs: renamed = BitVec(f"{t.name}_in_{inp.name()}", inp.width()) @@ -47,13 +59,11 @@ def serialize(m: FunctionalModel, filename): out_expr = out_expr.replace(input_map) sys.add_output(f"{t.name}_out_{out_name}", out_expr) - transactions = [{"name": t.name} for t in m.transactions] info = { "name": m.name, - "transactions": transactions, + "methods": [t.name for t in m.methods], "states": [s.name for s in m.states], - "sys": sys.to_btor2_str(), } with open(filename, "w") as f: - json.dump(info, f) + json.dump({"info": info, "sys": sys.to_btor2_str()}, f) diff --git a/functional-models/main.py b/functional-models/main.py index 0071c53d..a579da2e 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -3,7 +3,7 @@ # author: Kevin Laeufer from pypatronus import BitVec, SignExt, ZeroExt, Slice -from fun import FunctionalModel, Transaction, serialize +from fun import FunctionalModel, Method, serialize def picorv32_pcpi_mul(): @@ -12,19 +12,19 @@ def picorv32_pcpi_mul(): """ m = FunctionalModel(name="picorv32_pcpi_mul") rs1, rs2 = BitVec("rs1_data", 32), BitVec("rs2_data", 32) - m.transactions = [ - Transaction("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]), - Transaction( + m.methods = [ + Method("pcpi_mul", [rs1, rs2], [("rd_data", rs1 * rs2)]), + Method( "pcpi_mulh", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * SignExt(32, rs2)))], ), - Transaction( + Method( "pcpi_mulhu", [rs1, rs2], [("rd_data", Slice(63, 32, ZeroExt(32, rs1) * ZeroExt(32, rs2)))], ), - Transaction( + Method( "pcpi_mulhsu", [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))], diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs index c29dd541..3ea83bdb 100644 --- a/functional-models/src/lib.rs +++ b/functional-models/src/lib.rs @@ -2,30 +2,214 @@ // released under MIT License // author: Kevin Laeufer -use patronus::system::TransitionSystem; +use baa::{BitVecOps, BitVecValue}; +use patronus::expr::{Context, ExprRef}; +use patronus::sim::Simulator; +use patronus::system::{Output, TransitionSystem}; +use rustc_hash::FxHashMap; use serde::{Deserialize, Serialize}; -use serde_json::Result; +use std::ops::Index; #[derive(Debug)] -struct FunctionalModel { - meta: FunctionalModelInfo, +pub struct FunctionalModel { sys: TransitionSystem, + method_names: FxHashMap, + methods: Vec, +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq)] +pub struct MethodId(u32); + +#[derive(Debug)] +pub struct Method { + id: MethodId, + name: String, + guard: ExprRef, + commit: ExprRef, + inputs: Vec<(String, ExprRef)>, + outputs: Vec<(String, ExprRef)>, +} + +impl FunctionalModel { + pub fn load(ctx: &mut Context, reader: &mut impl std::io::BufRead) -> std::io::Result { + let m: FunctionalModelJson = serde_json::from_reader(reader)?; + let sys = patronus::btor2::parse_str(ctx, &m.sys, Some(&m.info.name)).unwrap(); + let methods: Vec<_> = m + .info + .methods + .into_iter() + .enumerate() + .map(|(idx, name)| { + let id = MethodId(idx as u32); + let guard = sys + .lookup_output(ctx, &format!("{name}_guard")) + .expect("Failed to find guard output."); + let commit = sys + .lookup_input(ctx, &format!("{name}_commit")) + .expect("Failed to find commit input."); + let input_prefix = format!("{name}_in_"); + let inputs = sys + .inputs + .iter() + .filter_map(|i| { + ctx.get_symbol_name(*i) + .and_then(|name| name.strip_prefix(&input_prefix)) + .map(|name| (name.to_string(), *i)) + }) + .collect(); + let output_prefix = format!("{name}_out_"); + let outputs = sys + .outputs + .iter() + .filter_map(|o| { + ctx[o.name] + .strip_prefix(&output_prefix) + .map(|name| (name.to_string(), o.expr)) + }) + .collect(); + Method { + id, + name, + guard, + commit, + inputs, + outputs, + } + }) + .collect(); + let method_names = methods + .iter() + .enumerate() + .map(|(idx, m)| (m.name.to_string(), MethodId(idx as u32))) + .collect(); + Ok(Self { + sys, + methods, + method_names, + }) + } + + pub fn name(&self) -> &str { + &self.sys.name + } + + pub fn sys(&self) -> &TransitionSystem { + &self.sys + } + + pub fn method_id(&self, name: &str) -> Option { + self.method_names.get(name).cloned() + } + + pub fn method(&self, name: &str) -> Option<&Method> { + self.method_id(name).map(|id| &self[id]) + } +} + +impl Index for FunctionalModel { + type Output = Method; + + fn index(&self, index: MethodId) -> &Self::Output { + &self.methods[index.0 as usize] + } +} + +pub struct FunctionalModelSimulator { + model: FunctionalModel, + sim: patronus::sim::Interpreter, + tru: BitVecValue, + fals: BitVecValue, +} + +impl FunctionalModelSimulator { + pub fn load(reader: &mut impl std::io::BufRead) -> std::io::Result { + let mut ctx = Context::default(); + let model = FunctionalModel::load(&mut ctx, reader)?; + Ok(Self::new(&mut ctx, model)) + } + + pub fn new(ctx: &Context, model: FunctionalModel) -> Self { + let sim = patronus::sim::Interpreter::new(ctx, &model.sys); + let tru = BitVecValue::from_bool(true); + let fals = BitVecValue::from_bool(false); + Self { + sim, + model, + tru, + fals, + } + } + + pub fn name(&self) -> &str { + self.model.name() + } + + pub fn guard(&self, method: MethodId) -> bool { + let e = self.model[method].guard; + let bv: BitVecValue = self.sim.get(e).try_into().unwrap(); + bv.is_bit_set(0) + } + + pub fn commit(&mut self, method: MethodId) { + let e = self.model[method].commit; + debug_assert!(self.guard(method), "method is not available!"); + self.sim.set(e, &self.tru); + self.sim.step(); + self.sim.set(e, &self.fals); + } + + pub fn set_input(&mut self, method: MethodId) { + todo!() + } + + pub fn get_output(&self, method: MethodId) { + todo!() + } +} + +#[derive(Debug)] +pub struct Transaction { + pub name: String, + pub commit: Vec, + pub inputs: Vec, + pub outputs: Vec, } #[derive(Debug, Deserialize, Serialize)] struct FunctionalModelJson { - meta: FunctionalModelInfo, + info: FunctionalModelInfoJson, sys: String, } #[derive(Debug, Deserialize, Serialize)] -struct FunctionalModelInfo { +struct FunctionalModelInfoJson { name: String, - transactions: Vec, + methods: Vec, states: Vec, } -#[derive(Debug, Deserialize, Serialize)] -struct Transaction { - name: String, +#[cfg(test)] +pub mod tests { + use super::*; + + const MUL_JSON: &[u8] = r##"{"info": {"name": "picorv32_pcpi_mul", "methods": ["pcpi_mul", "pcpi_mulh", "pcpi_mulhu", "pcpi_mulhsu"], "states": []}, "sys": "; btor2 description of `picorv32_pcpi_mul` generated by patronus 0.39.4\n1 sort bitvec 1\n2 input 1 pcpi_mul_commit\n3 sort bitvec 32\n4 input 3 pcpi_mul_in_rs1_data\n5 input 3 pcpi_mul_in_rs2_data\n6 input 1 pcpi_mulh_commit\n7 input 3 pcpi_mulh_in_rs1_data\n8 input 3 pcpi_mulh_in_rs2_data\n9 input 1 pcpi_mulhu_commit\n10 input 3 pcpi_mulhu_in_rs1_data\n11 input 3 pcpi_mulhu_in_rs2_data\n12 input 1 pcpi_mulhsu_commit\n13 input 3 pcpi_mulhsu_in_rs1_data\n14 input 3 pcpi_mulhsu_in_rs2_data\n15 one 1\n16 output 15 pcpi_mul_guard\n17 mul 3 4 5\n18 output 17 pcpi_mul_out_rd_data\n19 output 15 pcpi_mulh_guard\n20 sort bitvec 64\n21 sext 20 7 32\n22 sext 20 8 32\n23 mul 20 21 22\n24 slice 3 23 63 32\n25 output 24 pcpi_mulh_out_rd_data\n26 output 15 pcpi_mulhu_guard\n27 uext 20 10 32\n28 uext 20 11 32\n29 mul 20 27 28\n30 slice 3 29 63 32\n31 output 30 pcpi_mulhu_out_rd_data\n32 output 15 pcpi_mulhsu_guard\n33 sext 20 13 32\n34 uext 20 14 32\n35 mul 20 33 34\n36 slice 3 35 63 32\n37 output 36 pcpi_mulhsu_out_rd_data\n"}"##.as_bytes(); + + #[test] + fn test_load_mul_json() { + let mut ctx = Context::default(); + let m = FunctionalModel::load(&mut ctx, &mut std::io::Cursor::new(MUL_JSON)).unwrap(); + assert_eq!(m.name(), "picorv32_pcpi_mul"); + for name in ["pcpi_mul", "pcpi_mulh", "pcpi_mulhu", "pcpi_mulhsu"] { + let method = m.method(name).unwrap(); + assert_eq!(method.inputs[0].0, "rs1_data"); + assert_eq!(method.inputs[1].0, "rs2_data"); + assert_eq!(method.outputs[0].0, "rd_data"); + assert_eq!(method.guard, ctx.get_true()); + } + } + + #[test] + fn test_sim() { + let mut sim = FunctionalModelSimulator::load(&mut std::io::Cursor::new(MUL_JSON)).unwrap(); + } } diff --git a/interp/src/main.rs b/interp/src/main.rs index ca1a1b6c..85d746d4 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -39,6 +39,10 @@ struct Cli { #[arg(short, long, value_name = "WAVEFORM_FILE")] fst: Option, + /// Functional model JSON file. (optional) + #[arg(short, long)] + functional_model: Vec, + /// Users can specify `-v` or `--verbose` to toggle logging #[command(flatten)] verbosity: Verbosity, From 14b1eb616af6607fa3d3bfc9890d4d3ef2f59bcf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 24 Sep 2026 16:33:04 -0400 Subject: [PATCH 05/15] interp: wip functional model support --- interp/src/main.rs | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/interp/src/main.rs b/interp/src/main.rs index 85d746d4..13770f83 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -29,7 +29,7 @@ struct Cli { /// Path to a Transactions (.tx) file #[arg(short, long, value_name = "TRANSACTIONS_FILE")] - transactions: String, + transactions: Option, /// Name of the top-level module (if one exists) #[arg(short, long, value_name = "MODULE_NAME")] @@ -159,16 +159,15 @@ fn main() -> anyhow::Result<()> { emit_warnings, cli.display_hex, ); - let traces = match transaction_frontend( - cli.transactions, - &st, - &module.protos, - &mut transactions_handler, - ) { - Ok(result) => result, - Err(error) => { - exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) + let traces = if let Some(t) = cli.transactions.as_deref() { + match transaction_frontend(t, &st, &module.protos, &mut transactions_handler) { + Ok(result) => Some(result), + Err(error) => { + exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) + } } + } else { + None }; let mut any_failed = false; From 47f9d99eb8e20c53117c916d8605245440c0c945 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 24 Sep 2026 16:34:11 -0400 Subject: [PATCH 06/15] fun: guard only depends on state --- functional-models/fun.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index ce552cc6..9e9fb1a0 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -18,7 +18,7 @@ class Method: inputs: list = field(default_factory=list) outputs: list = field(default_factory=list) state_updates: list = field(default_factory=list) - # indicates whether the method can be executed based on state and inputs + # indicates whether the method can be executed based on the current model state guard: Optional[ExprRef] = None @@ -35,9 +35,10 @@ def verify_model(m: FunctionalModel): ) # check guard if method.guard is not None: + allowed_symbols = set(m.states) unallowed = method.guard.symbols() - allowed_symbols assert len(unallowed) == 0, ( - f"Guard {method.guard} uses symbols that are neither inputs nor state: {unallowed}" + f"Guard {method.guard} uses symbols that are not state: {unallowed}" ) From 0149dd09061450169d3c15a1f76eaba1bef5b0ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 25 Sep 2026 10:44:36 -0400 Subject: [PATCH 07/15] interp: skeleton for trace generation and validation from functional model --- Cargo.toml | 1 + functional-models/src/lib.rs | 16 +++++++- interp/Cargo.toml | 2 + interp/src/main.rs | 77 +++++++++++++++++++++++++++++------- 4 files changed, 81 insertions(+), 15 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 27ff696c..759ab37c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,6 +13,7 @@ license = "MIT" [workspace.dependencies] protocols = { path = "protocols" } +functional = { path = "functional-models" } baa = { version = "0.19.3", features = ["rand1"] } patronus = { git="https://github.com/Nikil-Shyamsunder/patronus#" } rand = "0.10" diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs index 3ea83bdb..5632bc01 100644 --- a/functional-models/src/lib.rs +++ b/functional-models/src/lib.rs @@ -9,6 +9,7 @@ use patronus::system::{Output, TransitionSystem}; use rustc_hash::FxHashMap; use serde::{Deserialize, Serialize}; use std::ops::Index; +use std::path::Path; #[derive(Debug)] pub struct FunctionalModel { @@ -119,9 +120,16 @@ pub struct FunctionalModelSimulator { sim: patronus::sim::Interpreter, tru: BitVecValue, fals: BitVecValue, + init_snapshot: u32, } impl FunctionalModelSimulator { + pub fn from_file(filename: impl AsRef) -> std::io::Result { + let file = std::fs::File::open(filename)?; + let mut reader = std::io::BufReader::new(file); + Self::load(&mut reader) + } + pub fn load(reader: &mut impl std::io::BufRead) -> std::io::Result { let mut ctx = Context::default(); let model = FunctionalModel::load(&mut ctx, reader)?; @@ -129,7 +137,8 @@ impl FunctionalModelSimulator { } pub fn new(ctx: &Context, model: FunctionalModel) -> Self { - let sim = patronus::sim::Interpreter::new(ctx, &model.sys); + let mut sim = patronus::sim::Interpreter::new(ctx, &model.sys); + let init_snapshot = sim.take_snapshot(); let tru = BitVecValue::from_bool(true); let fals = BitVecValue::from_bool(false); Self { @@ -137,6 +146,7 @@ impl FunctionalModelSimulator { model, tru, fals, + init_snapshot, } } @@ -165,6 +175,10 @@ impl FunctionalModelSimulator { pub fn get_output(&self, method: MethodId) { todo!() } + + pub fn reset(&mut self) { + self.sim.restore_snapshot(self.init_snapshot); + } } #[derive(Debug)] diff --git a/interp/Cargo.toml b/interp/Cargo.toml index 60e499db..f0a137a3 100644 --- a/interp/Cargo.toml +++ b/interp/Cargo.toml @@ -13,3 +13,5 @@ clap.workspace = true clap-verbosity-flag = "3.0.4" env_logger = "0.11.8" anyhow.workspace = true +functional.workspace = true +patronus.workspace = true diff --git a/interp/src/main.rs b/interp/src/main.rs index 13770f83..20ecf56b 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -5,10 +5,13 @@ use clap::{ColorChoice, Parser}; use clap_verbosity_flag::log::LevelFilter; use clap_verbosity_flag::{Verbosity, WarnLevel}; +use functional::FunctionalModelSimulator; use protocols::ascii_waveform::print_ascii_waveform; use protocols::frontend::diagnostic::DiagnosticHandler; -use protocols::frontend::require_single_module; -use protocols::scheduler::Scheduler; +use protocols::frontend::symbol::SymbolTable; +use protocols::frontend::{Module, require_single_module}; +use protocols::scheduler::{Invocation, Scheduler}; +use protocols::transactions::Traces; use protocols::{PatronusSim, frontend, transaction_frontend}; /// Args for the interpreter CLI @@ -41,7 +44,12 @@ struct Cli { /// Functional model JSON file. (optional) #[arg(short, long)] - functional_model: Vec, + functional_model: Option, + + /// Number of transactions to randomly generate from the functional model. + /// These will be appended to any transactions loaded from the transaction file. + #[arg(short, long, default_value_t = 0)] + num_random_transactions: u32, /// Users can specify `-v` or `--verbose` to toggle logging #[command(flatten)] @@ -153,22 +161,13 @@ fn main() -> anyhow::Result<()> { let module = require_single_module(modules, &cli.protocol)?; // Create a separate `DiagnosticHandler` when parsing the transactions file - let mut transactions_handler = DiagnosticHandler::new( + let transactions_handler = DiagnosticHandler::new( color_choice, cli.no_error_locations, emit_warnings, cli.display_hex, ); - let traces = if let Some(t) = cli.transactions.as_deref() { - match transaction_frontend(t, &st, &module.protos, &mut transactions_handler) { - Ok(result) => Some(result), - Err(error) => { - exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) - } - } - } else { - None - }; + let traces = load_traces(&cli, transactions_handler, &st, &module); let mut any_failed = false; for (trace_index, todos) in traces.into_iter().enumerate() { @@ -219,3 +218,53 @@ fn main() -> anyhow::Result<()> { } Ok(()) } + +fn load_traces( + cli: &Cli, + mut transactions_handler: DiagnosticHandler, + st: &SymbolTable, + module: &Module, +) -> Traces { + let mut traces = if let Some(t) = cli.transactions.as_deref() { + match transaction_frontend(t, st, &module.protos, &mut transactions_handler) { + Ok(result) => result, + Err(error) => { + exit_after_setup_error(error, !transactions_handler.error_string().is_empty()) + } + } + } else { + vec![] + }; + + if let Some(fun) = cli.functional_model.as_deref() { + let mut sim = + FunctionalModelSimulator::from_file(fun).expect("failed to load functional model"); + // 1) verify existing traces + for trace in &traces { + verify_trace(&mut sim, trace); + } + + // 2) generate a new trace + let trace = sample_functional_model(&mut sim, cli.num_random_transactions); + if !trace.is_empty() { + traces.push(trace); + } + } else { + assert_eq!( + cli.num_random_transactions, 0, + "cannot generate random transactions without a functional model" + ); + } + + traces +} + +fn sample_functional_model(sim: &mut FunctionalModelSimulator, num: u32) -> Vec { + sim.reset(); + todo!() +} + +fn verify_trace(sim: &mut FunctionalModelSimulator, trace: &[Invocation]) { + sim.reset(); + todo!() +} From 476012990f249da22f2a159abeab2720f1a003c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 25 Sep 2026 13:27:09 -0400 Subject: [PATCH 08/15] functional model: use to validate trace --- functional-models/main.py | 2 + functional-models/src/lib.rs | 71 +++++++++++++++++++++-- interp/src/main.rs | 109 ++++++++++++++++++++++++++++++++--- protocols/src/value.rs | 30 +++++++--- 4 files changed, 190 insertions(+), 22 deletions(-) diff --git a/functional-models/main.py b/functional-models/main.py index a579da2e..a9ba55cd 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -29,6 +29,8 @@ def picorv32_pcpi_mul(): [rs1, rs2], [("rd_data", Slice(63, 32, SignExt(32, rs1) * ZeroExt(32, rs2)))], ), + Method("pcpi_mul_reset"), + Method("idle"), ] return m diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs index 5632bc01..230824e8 100644 --- a/functional-models/src/lib.rs +++ b/functional-models/src/lib.rs @@ -3,9 +3,10 @@ // author: Kevin Laeufer use baa::{BitVecOps, BitVecValue}; -use patronus::expr::{Context, ExprRef}; -use patronus::sim::Simulator; +use patronus::expr::{Context, ExprRef, SerializableIrNode}; +use patronus::sim::{InitKind, Simulator}; use patronus::system::{Output, TransitionSystem}; +use protocols::Value; use rustc_hash::FxHashMap; use serde::{Deserialize, Serialize}; use std::ops::Index; @@ -21,6 +22,25 @@ pub struct FunctionalModel { #[derive(Debug, Copy, Clone, Eq, PartialEq)] pub struct MethodId(u32); +impl From for usize { + fn from(value: MethodId) -> Self { + value.0 as usize + } +} + +#[derive(Debug, Copy, Clone, Eq, PartialEq)] +pub struct ParameterId { + method: MethodId, + is_input: bool, + index: u16, +} + +impl ParameterId { + pub fn is_input(&self) -> bool { + self.is_input + } +} + #[derive(Debug)] pub struct Method { id: MethodId, @@ -31,10 +51,31 @@ pub struct Method { outputs: Vec<(String, ExprRef)>, } +impl Method { + pub fn parameter_id(&self, name: &str) -> Option { + if let Some(idx) = self.inputs.iter().position(|(n, _)| n == name) { + Some(ParameterId { + method: self.id, + is_input: true, + index: idx as u16, + }) + } else if let Some(idx) = self.outputs.iter().position(|(n, _)| n == name) { + Some(ParameterId { + method: self.id, + is_input: false, + index: idx as u16, + }) + } else { + None + } + } +} + impl FunctionalModel { pub fn load(ctx: &mut Context, reader: &mut impl std::io::BufRead) -> std::io::Result { let m: FunctionalModelJson = serde_json::from_reader(reader)?; let sys = patronus::btor2::parse_str(ctx, &m.sys, Some(&m.info.name)).unwrap(); + println!("{}", sys.serialize_to_str(ctx)); let methods: Vec<_> = m .info .methods @@ -48,6 +89,7 @@ impl FunctionalModel { let commit = sys .lookup_input(ctx, &format!("{name}_commit")) .expect("Failed to find commit input."); + println!("COMMIT: {}", commit.serialize_to_str(ctx)); let input_prefix = format!("{name}_in_"); let inputs = sys .inputs @@ -138,6 +180,7 @@ impl FunctionalModelSimulator { pub fn new(ctx: &Context, model: FunctionalModel) -> Self { let mut sim = patronus::sim::Interpreter::new(ctx, &model.sys); + sim.init(InitKind::Zero); let init_snapshot = sim.take_snapshot(); let tru = BitVecValue::from_bool(true); let fals = BitVecValue::from_bool(false); @@ -154,6 +197,10 @@ impl FunctionalModelSimulator { self.model.name() } + pub fn model(&self) -> &FunctionalModel { + &self.model + } + pub fn guard(&self, method: MethodId) -> bool { let e = self.model[method].guard; let bv: BitVecValue = self.sim.get(e).try_into().unwrap(); @@ -168,12 +215,24 @@ impl FunctionalModelSimulator { self.sim.set(e, &self.fals); } - pub fn set_input(&mut self, method: MethodId) { - todo!() + pub fn set_input(&mut self, param: ParameterId, value: &Value) { + assert!(param.is_input()); + let (_, e) = self.model[param.method].inputs[param.index as usize]; + if let Ok(bv) = BitVecValue::try_from(value.clone()) { + self.sim.set(e, &bv); + } else { + todo!("Deal with non-scalar values.") + } } - pub fn get_output(&self, method: MethodId) { - todo!() + pub fn get_output(&self, param: ParameterId) -> Value { + assert!(!param.is_input()); + let (_, e) = self.model[param.method].outputs[param.index as usize]; + if let Ok(bv) = BitVecValue::try_from(self.sim.get(e)) { + bv.into() + } else { + todo!() + } } pub fn reset(&mut self) { diff --git a/interp/src/main.rs b/interp/src/main.rs index 20ecf56b..99fc9256 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -5,7 +5,7 @@ use clap::{ColorChoice, Parser}; use clap_verbosity_flag::log::LevelFilter; use clap_verbosity_flag::{Verbosity, WarnLevel}; -use functional::FunctionalModelSimulator; +use functional::{FunctionalModel, FunctionalModelSimulator, Method, MethodId, ParameterId}; use protocols::ascii_waveform::print_ascii_waveform; use protocols::frontend::diagnostic::DiagnosticHandler; use protocols::frontend::symbol::SymbolTable; @@ -43,12 +43,12 @@ struct Cli { fst: Option, /// Functional model JSON file. (optional) - #[arg(short, long)] + #[arg(long)] functional_model: Option, /// Number of transactions to randomly generate from the functional model. /// These will be appended to any transactions loaded from the transaction file. - #[arg(short, long, default_value_t = 0)] + #[arg(long, default_value_t = 0)] num_random_transactions: u32, /// Users can specify `-v` or `--verbose` to toggle logging @@ -239,13 +239,14 @@ fn load_traces( if let Some(fun) = cli.functional_model.as_deref() { let mut sim = FunctionalModelSimulator::from_file(fun).expect("failed to load functional model"); + let map = FunMap::new(st, sim.model(), &module); // 1) verify existing traces for trace in &traces { - verify_trace(&mut sim, trace); + verify_trace(&mut sim, &map, trace, cli.display_hex); } // 2) generate a new trace - let trace = sample_functional_model(&mut sim, cli.num_random_transactions); + let trace = sample_functional_model(&mut sim, &map, cli.num_random_transactions); if !trace.is_empty() { traces.push(trace); } @@ -259,12 +260,102 @@ fn load_traces( traces } -fn sample_functional_model(sim: &mut FunctionalModelSimulator, num: u32) -> Vec { +fn sample_functional_model( + sim: &mut FunctionalModelSimulator, + map: &FunMap, + num: u32, +) -> Vec { sim.reset(); - todo!() + let out = Vec::with_capacity(num as usize); + for _ in 0..num { + todo!() + } + out } -fn verify_trace(sim: &mut FunctionalModelSimulator, trace: &[Invocation]) { +fn verify_trace( + sim: &mut FunctionalModelSimulator, + map: &FunMap, + trace: &[Invocation], + display_hex: bool, +) { sim.reset(); - todo!() + for (name, args) in trace { + if let Some(method) = sim.model().method_id(name) { + assert!(sim.guard(method), "Transaction {name} cannot be executed"); + let params = map.params(method); + debug_assert_eq!(params.len(), args.len()); + for (p, a) in params.iter().zip(args.iter()) { + if p.is_input() { + sim.set_input(*p, a); + } + } + for (p, a) in params.iter().zip(args.iter()) { + if !p.is_input() { + let actual = sim.get_output(*p); + assert_eq!( + &actual, + a, + "Transaction {name} is supposed to produce {}, but the functional model indicates that is should produce {}", + a.to_string(display_hex), + actual.to_string(display_hex) + ); + } + } + sim.commit(method); + } else { + panic!( + "Unknown transaction {name}. Not part of the functional model {}", + sim.name() + ); + } + } +} + +struct FunMap { + params: Vec>, +} + +impl FunMap { + fn new(st: &SymbolTable, model: &FunctionalModel, module: &Module) -> Self { + let mut params = vec![]; + for proto in &module.protos { + if let Some(method_id) = model.method_id(&proto.name) { + let idx: usize = method_id.into(); + if idx >= params.len() { + params.resize(idx + 1, vec![]); + } + let method = &model[method_id]; + params[idx] = proto + .args + .iter() + .map(|arg| { + let sym = &st[arg.symbol()]; + if let Some(p) = method.parameter_id(sym.name()) { + p + } else { + panic!( + "Method {} is missing parameter `{}`", + proto.name, + sym.name() + ); + } + }) + .collect(); + } else { + panic!( + "Functional model {} is missing a method for protocol `{}` from {}.", + model.name(), + proto.name, + module.name + ); + } + } + + Self { params } + } + + fn params(&self, method: MethodId) -> &[ParameterId] { + &self.params[usize::from(method)] + } } diff --git a/protocols/src/value.rs b/protocols/src/value.rs index 3d496fe2..2f3f1aa9 100644 --- a/protocols/src/value.rs +++ b/protocols/src/value.rs @@ -9,10 +9,30 @@ use baa::{BitVecOps, BitVecValue}; /// A concrete value of any type. -#[derive(Debug, Clone)] +#[derive(Debug, Clone, Eq, PartialEq)] pub struct Value(ValueKind); -#[derive(Debug, Clone)] +impl Value { + pub fn to_string(&self, display_hex: bool) -> String { + match &self.0 { + ValueKind::Scalar(v) => bv_to_string(v, display_hex), + ValueKind::Seq(v) => { + let entries: Vec<_> = v.iter().map(|e| bv_to_string(e, display_hex)).collect(); + format!("[{}]", entries.join(", ")) + } + } + } +} + +fn bv_to_string(value: &BitVecValue, display_hex: bool) -> String { + if display_hex { + format!("0x{}", value.to_hex_str()) + } else { + value.to_dec_str() + } +} + +#[derive(Debug, Clone, Eq, PartialEq)] enum ValueKind { Scalar(BitVecValue), Seq(Vec), @@ -116,11 +136,7 @@ impl SymBitVecValue { pub fn to_string(&self, display_hex: bool) -> String { if self.known.is_all_ones() { - if display_hex { - format!("0x{}", self.value.to_hex_str()) - } else { - self.value.to_dec_str() - } + bv_to_string(&self.value, display_hex) } else if self.known.is_zero() { // TODO: do we actually want to keep this behavior? "X".to_string() From 9ee4a50f1fc07b0fe292b51cd89f8e1b87a7371f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 25 Sep 2026 14:45:33 -0400 Subject: [PATCH 09/15] interp: random testing with functional model --- functional-models/src/lib.rs | 57 +++++++++++++++++++++++++----------- interp/Cargo.toml | 2 ++ interp/src/main.rs | 54 +++++++++++++++++++++++++++++----- 3 files changed, 88 insertions(+), 25 deletions(-) diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs index 230824e8..38d03060 100644 --- a/functional-models/src/lib.rs +++ b/functional-models/src/lib.rs @@ -2,8 +2,8 @@ // released under MIT License // author: Kevin Laeufer -use baa::{BitVecOps, BitVecValue}; -use patronus::expr::{Context, ExprRef, SerializableIrNode}; +use baa::{BitVecOps, BitVecValue, WidthInt}; +use patronus::expr::{Context, ExprRef, TypeCheck}; use patronus::sim::{InitKind, Simulator}; use patronus::system::{Output, TransitionSystem}; use protocols::Value; @@ -31,8 +31,15 @@ impl From for usize { #[derive(Debug, Copy, Clone, Eq, PartialEq)] pub struct ParameterId { method: MethodId, - is_input: bool, index: u16, + is_input: bool, + width: WidthInt, +} + +impl ParameterId { + pub fn width(&self) -> WidthInt { + self.width + } } impl ParameterId { @@ -47,35 +54,41 @@ pub struct Method { name: String, guard: ExprRef, commit: ExprRef, - inputs: Vec<(String, ExprRef)>, - outputs: Vec<(String, ExprRef)>, + inputs: Vec<(String, WidthInt, ExprRef)>, + outputs: Vec<(String, WidthInt, ExprRef)>, } impl Method { pub fn parameter_id(&self, name: &str) -> Option { - if let Some(idx) = self.inputs.iter().position(|(n, _)| n == name) { + if let Some(idx) = self.inputs.iter().position(|(n, _, _)| n == name) { Some(ParameterId { method: self.id, is_input: true, index: idx as u16, + width: self.inputs[idx].1, }) - } else if let Some(idx) = self.outputs.iter().position(|(n, _)| n == name) { + } else if let Some(idx) = self.outputs.iter().position(|(n, _, _)| n == name) { Some(ParameterId { method: self.id, is_input: false, index: idx as u16, + width: self.outputs[idx].1, }) } else { None } } + + pub fn name(&self) -> &str { + &self.name + } } impl FunctionalModel { pub fn load(ctx: &mut Context, reader: &mut impl std::io::BufRead) -> std::io::Result { let m: FunctionalModelJson = serde_json::from_reader(reader)?; let sys = patronus::btor2::parse_str(ctx, &m.sys, Some(&m.info.name)).unwrap(); - println!("{}", sys.serialize_to_str(ctx)); + let methods: Vec<_> = m .info .methods @@ -89,7 +102,6 @@ impl FunctionalModel { let commit = sys .lookup_input(ctx, &format!("{name}_commit")) .expect("Failed to find commit input."); - println!("COMMIT: {}", commit.serialize_to_str(ctx)); let input_prefix = format!("{name}_in_"); let inputs = sys .inputs @@ -97,7 +109,7 @@ impl FunctionalModel { .filter_map(|i| { ctx.get_symbol_name(*i) .and_then(|name| name.strip_prefix(&input_prefix)) - .map(|name| (name.to_string(), *i)) + .map(|name| (name.to_string(), i.get_bv_type(ctx).unwrap(), *i)) }) .collect(); let output_prefix = format!("{name}_out_"); @@ -105,9 +117,9 @@ impl FunctionalModel { .outputs .iter() .filter_map(|o| { - ctx[o.name] - .strip_prefix(&output_prefix) - .map(|name| (name.to_string(), o.expr)) + ctx[o.name].strip_prefix(&output_prefix).map(|name| { + (name.to_string(), o.expr.get_bv_type(ctx).unwrap(), o.expr) + }) }) .collect(); Method { @@ -217,24 +229,35 @@ impl FunctionalModelSimulator { pub fn set_input(&mut self, param: ParameterId, value: &Value) { assert!(param.is_input()); - let (_, e) = self.model[param.method].inputs[param.index as usize]; + let (width, e) = self.param_id_to_width_and_e(param); if let Ok(bv) = BitVecValue::try_from(value.clone()) { + debug_assert_eq!(width, bv.width()); self.sim.set(e, &bv); } else { todo!("Deal with non-scalar values.") } } - pub fn get_output(&self, param: ParameterId) -> Value { - assert!(!param.is_input()); - let (_, e) = self.model[param.method].outputs[param.index as usize]; + /// get the value of an input or output parameter + pub fn get(&self, param: ParameterId) -> Value { + let (width, e) = self.param_id_to_width_and_e(param); if let Ok(bv) = BitVecValue::try_from(self.sim.get(e)) { + debug_assert_eq!(width, bv.width()); bv.into() } else { todo!() } } + fn param_id_to_width_and_e(&self, param: ParameterId) -> (WidthInt, ExprRef) { + let (_, width, e) = if param.is_input() { + &self.model[param.method].inputs[param.index as usize] + } else { + &self.model[param.method].outputs[param.index as usize] + }; + (*width, *e) + } + pub fn reset(&mut self) { self.sim.restore_snapshot(self.init_snapshot); } diff --git a/interp/Cargo.toml b/interp/Cargo.toml index f0a137a3..5fb51a47 100644 --- a/interp/Cargo.toml +++ b/interp/Cargo.toml @@ -15,3 +15,5 @@ env_logger = "0.11.8" anyhow.workspace = true functional.workspace = true patronus.workspace = true +rand.workspace = true +baa.workspace = true diff --git a/interp/src/main.rs b/interp/src/main.rs index 99fc9256..fa4f318e 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -2,17 +2,21 @@ // released under MIT License // author: Ernest Ng +use baa::BitVecValue; use clap::{ColorChoice, Parser}; use clap_verbosity_flag::log::LevelFilter; use clap_verbosity_flag::{Verbosity, WarnLevel}; -use functional::{FunctionalModel, FunctionalModelSimulator, Method, MethodId, ParameterId}; +use functional::{FunctionalModel, FunctionalModelSimulator, MethodId, ParameterId}; use protocols::ascii_waveform::print_ascii_waveform; use protocols::frontend::diagnostic::DiagnosticHandler; use protocols::frontend::symbol::SymbolTable; use protocols::frontend::{Module, require_single_module}; use protocols::scheduler::{Invocation, Scheduler}; use protocols::transactions::Traces; -use protocols::{PatronusSim, frontend, transaction_frontend}; +use protocols::{PatronusSim, Value, frontend, transaction_frontend}; +use rand::SeedableRng; +use rand::prelude::StdRng; +use rand::seq::IndexedRandom; /// Args for the interpreter CLI #[derive(Parser, Debug)] @@ -167,7 +171,8 @@ fn main() -> anyhow::Result<()> { emit_warnings, cli.display_hex, ); - let traces = load_traces(&cli, transactions_handler, &st, &module); + let mut trace_rng = StdRng::seed_from_u64(0); + let traces = load_traces(&cli, transactions_handler, &st, &module, &mut trace_rng); let mut any_failed = false; for (trace_index, todos) in traces.into_iter().enumerate() { @@ -224,6 +229,7 @@ fn load_traces( mut transactions_handler: DiagnosticHandler, st: &SymbolTable, module: &Module, + rng: &mut impl rand::Rng, ) -> Traces { let mut traces = if let Some(t) = cli.transactions.as_deref() { match transaction_frontend(t, st, &module.protos, &mut transactions_handler) { @@ -246,7 +252,7 @@ fn load_traces( } // 2) generate a new trace - let trace = sample_functional_model(&mut sim, &map, cli.num_random_transactions); + let trace = sample_functional_model(&mut sim, &map, cli.num_random_transactions, rng); if !trace.is_empty() { traces.push(trace); } @@ -264,11 +270,33 @@ fn sample_functional_model( sim: &mut FunctionalModelSimulator, map: &FunMap, num: u32, + rng: &mut impl rand::Rng, ) -> Vec { sim.reset(); - let out = Vec::with_capacity(num as usize); + let mut out = Vec::with_capacity(num as usize); for _ in 0..num { - todo!() + // pick method + let available: Vec<_> = map.methods().iter().filter(|m| sim.guard(**m)).collect(); + assert!(!available.is_empty()); + if let Some(&&method) = available.choose(rng) { + // generate and apply inputs + for &p in map.params(method) { + if p.is_input() { + let value: Value = BitVecValue::random(rng, p.width()).into(); + sim.set_input(p, &value) + } + } + // read all values + let args: Vec = map.params(method).iter().map(|&p| sim.get(p)).collect(); + // commit + sim.commit(method); + out.push((sim.model()[method].name().to_string(), args)); + } else { + panic!( + "Cannot generate invocation #{}, because none of the methods have active guards.", + out.len() + 1 + ); + } } out } @@ -292,7 +320,7 @@ fn verify_trace( } for (p, a) in params.iter().zip(args.iter()) { if !p.is_input() { - let actual = sim.get_output(*p); + let actual = sim.get(*p); assert_eq!( &actual, a, @@ -314,13 +342,16 @@ fn verify_trace( struct FunMap { params: Vec>, + methods: Vec, } impl FunMap { fn new(st: &SymbolTable, model: &FunctionalModel, module: &Module) -> Self { let mut params = vec![]; + let mut methods = vec![]; for proto in &module.protos { if let Some(method_id) = model.method_id(&proto.name) { + methods.push(method_id); let idx: usize = method_id.into(); if idx >= params.len() { params.resize(idx + 1, vec![]); @@ -352,10 +383,17 @@ impl FunMap { } } - Self { params } + Self { params, methods } } + /// The parameters of a given method in the same order as the args of the corresponding protocol. fn params(&self, method: MethodId) -> &[ParameterId] { &self.params[usize::from(method)] } + + /// The methods in the functional model in the same order as the corresponding protocol in the + /// module. + fn methods(&self) -> &[MethodId] { + &self.methods + } } From 0e594ba160b1096f8705d2ccb88b88a464094561 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 25 Sep 2026 14:51:20 -0400 Subject: [PATCH 10/15] clippy fixes --- functional-models/src/lib.rs | 21 +++++++++++---------- interp/src/main.rs | 2 +- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/functional-models/src/lib.rs b/functional-models/src/lib.rs index 38d03060..8d7d755e 100644 --- a/functional-models/src/lib.rs +++ b/functional-models/src/lib.rs @@ -67,15 +67,16 @@ impl Method { index: idx as u16, width: self.inputs[idx].1, }) - } else if let Some(idx) = self.outputs.iter().position(|(n, _, _)| n == name) { - Some(ParameterId { - method: self.id, - is_input: false, - index: idx as u16, - width: self.outputs[idx].1, - }) } else { - None + self.outputs + .iter() + .position(|(n, _, _)| n == name) + .map(|idx| ParameterId { + method: self.id, + is_input: false, + index: idx as u16, + width: self.outputs[idx].1, + }) } } @@ -187,7 +188,7 @@ impl FunctionalModelSimulator { pub fn load(reader: &mut impl std::io::BufRead) -> std::io::Result { let mut ctx = Context::default(); let model = FunctionalModel::load(&mut ctx, reader)?; - Ok(Self::new(&mut ctx, model)) + Ok(Self::new(&ctx, model)) } pub fn new(ctx: &Context, model: FunctionalModel) -> Self { @@ -306,6 +307,6 @@ pub mod tests { #[test] fn test_sim() { - let mut sim = FunctionalModelSimulator::load(&mut std::io::Cursor::new(MUL_JSON)).unwrap(); + let _sim = FunctionalModelSimulator::load(&mut std::io::Cursor::new(MUL_JSON)).unwrap(); } } diff --git a/interp/src/main.rs b/interp/src/main.rs index fa4f318e..48ea9409 100644 --- a/interp/src/main.rs +++ b/interp/src/main.rs @@ -245,7 +245,7 @@ fn load_traces( if let Some(fun) = cli.functional_model.as_deref() { let mut sim = FunctionalModelSimulator::from_file(fun).expect("failed to load functional model"); - let map = FunMap::new(st, sim.model(), &module); + let map = FunMap::new(st, sim.model(), module); // 1) verify existing traces for trace in &traces { verify_trace(&mut sim, &map, trace, cli.display_hex); From 8ef6d4465a5af2a902f7cdf128e68c8fe406d543 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 25 Sep 2026 16:15:03 -0400 Subject: [PATCH 11/15] wip: fifo model --- functional-models/main.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/functional-models/main.py b/functional-models/main.py index a9ba55cd..68cdb479 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -35,6 +35,12 @@ def picorv32_pcpi_mul(): return m +def fifo(data_width: int, num_elements: int): + m = FunctionalModel(name="fifo") + # elements = Array(data_width, num_elements) + # TODO: update to latest pypatronus for array support + + def main(): m = picorv32_pcpi_mul() print(m) From ea119a2cc486c95238544cf5263a4e171c64fd26 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 28 Sep 2026 11:52:15 -0400 Subject: [PATCH 12/15] fun: wip fifo model --- functional-models/fun.py | 4 +- functional-models/main.py | 76 ++++++++++++++++++++++++++++---- functional-models/pyproject.toml | 2 +- uv.lock | 38 ++++++++-------- 4 files changed, 90 insertions(+), 30 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index 9e9fb1a0..bc9b9753 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -17,7 +17,7 @@ class Method: name: str inputs: list = field(default_factory=list) outputs: list = field(default_factory=list) - state_updates: list = field(default_factory=list) + nexts: list = field(default_factory=list) # indicates whether the method can be executed based on the current model state guard: Optional[ExprRef] = None @@ -25,7 +25,7 @@ class Method: def verify_model(m: FunctionalModel): assert len(m.states) == 0, "TODO: deal with states" for method in m.methods: - assert len(method.state_updates) == len(m.states) + assert len(method.nexts) == len(m.states) allowed_symbols = set(m.states) | set(method.inputs) for out_name, out_expr in method.outputs: diff --git a/functional-models/main.py b/functional-models/main.py index 68cdb479..4b4de514 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -2,7 +2,7 @@ # released under MIT License # author: Kevin Laeufer -from pypatronus import BitVec, SignExt, ZeroExt, Slice +from pypatronus import BitVec, SignExt, ZeroExt, Slice, Update, If, Array, BitVecVal from fun import FunctionalModel, Method, serialize @@ -35,16 +35,76 @@ def picorv32_pcpi_mul(): return m -def fifo(data_width: int, num_elements: int): - m = FunctionalModel(name="fifo") - # elements = Array(data_width, num_elements) - # TODO: update to latest pypatronus for array support +def fifo(data_width: int, num_elements: int, push_pop: bool = False): + """https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/fifo/FifoSpec.scala""" + counter_width = 12 + assert num_elements < ((1 << (counter_width - 1)) - 1) + mem = Array("mem", data_width, num_elements) + count = BitVec("count", counter_width) + read = BitVec("read", counter_width) + m = FunctionalModel(name="fifo", states=[mem, count, read]) + num_elements_bv = BitVecVal(num_elements, counter_width) + full = count.equals(num_elements_bv) + empty = count.equals(BitVecVal(0, counter_width)) + input = BitVec("input", data_width) + + non_wrap = count + read + write_adr = If(non_wrap < num_elements_bv, non_wrap, non_wrap - num_elements_bv) + read_plus_one = read + BitVecVal(1, counter_width) + read_incr = If( + read_plus_one.equals(num_elements_bv), + BitVecVal(0, counter_width), + read_plus_one, + ) + + m.methods = [ + Method( + "push", + [input], + [], + [ + Update(mem, write_adr, input), # mem + count + BitVecVal(1, counter_width), # count + read, # read + ], + ~full, + ), + Method( + "pop", + [], + [("output", mem[read])], + [ + mem, # mem + count - BitVecVal(1, counter_width), # count + read_incr, # read + ], + ~empty, + ), + Method("reset"), + Method("idle"), + ] + if push_pop: + m.methods.append( + Method( + "push_pop", + [input], + [("output", mem[read])], + [ + Update(mem, write_adr, input), # mem + count, # count + read_incr, # read + ], + ), + ) + return m def main(): - m = picorv32_pcpi_mul() - print(m) - serialize(m, "picorv32_pcpi_mul.json") + serialize(picorv32_pcpi_mul(), "picorv32_pcpi_mul.json") + params = [{"data_width": 32, "num_elements": 5}] + for p in params: + file_name = "fifo_" + "_".join(f"{k}={v}" for k, v in p.items()) + ".json" + serialize(fifo(**p), file_name) if __name__ == "__main__": diff --git a/functional-models/pyproject.toml b/functional-models/pyproject.toml index 8c1a7d59..278850e2 100644 --- a/functional-models/pyproject.toml +++ b/functional-models/pyproject.toml @@ -5,5 +5,5 @@ description = "Add your description here" readme = "README.md" requires-python = ">=3.12" dependencies = [ - "pypatronus==0.39.4", + "pypatronus==0.39.5", ] diff --git a/uv.lock b/uv.lock index d54dc550..afb970c6 100644 --- a/uv.lock +++ b/uv.lock @@ -17,7 +17,7 @@ dependencies = [ ] [package.metadata] -requires-dist = [{ name = "pypatronus", specifier = "==0.39.4" }] +requires-dist = [{ name = "pypatronus", specifier = "==0.39.5" }] [[package]] name = "protocols" @@ -40,26 +40,26 @@ dev = [ [[package]] name = "pypatronus" -version = "0.39.4" +version = "0.39.5" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/31/48/247a70b9ea7b07862c31ec169fd6f3ab23521e407a765bc99939f091aa7d/pypatronus-0.39.4.tar.gz", hash = "sha256:774da01f8af5b3b4447054d4b719a4cdd3dd0c8b06541aa38fbf31de4d371015", size = 164797, upload-time = "2026-09-23T15:27:28.082Z" } +sdist = { url = "https://files.pythonhosted.org/packages/35/2d/faf77267fffdf83f6eba8d5df9eaa23d25fa12aa6685578b0b96fd3849de/pypatronus-0.39.5.tar.gz", hash = "sha256:0d32e1d3f6c2c948b1c08c8a15d347fb65bcbc7443604a651f4eb73aca68b224", size = 165664, upload-time = "2026-09-25T20:19:07.386Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/49/c5/3e9953ed91870eda4387113bb8ecd040ebede477483b8801ff8658f2cbb2/pypatronus-0.39.4-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:9335a6fb15cb0a53b5f29d5e55bb090a0fc1cfc4187b7a85c9e7e3cbb01b787f", size = 1353907, upload-time = "2026-09-23T15:27:23.659Z" }, - { url = "https://files.pythonhosted.org/packages/94/8f/24e37b42f7a3580e995550ab23c6e92b28f782845a17dcada1743a321576/pypatronus-0.39.4-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:7e8fd40d25f6d1773a67108401942536230c8751ea56f977617bd1030b4fb288", size = 1304486, upload-time = "2026-09-23T15:27:15.639Z" }, - { url = "https://files.pythonhosted.org/packages/f2/67/ad4f33c1c1d7a41e9ca5ce55a77e01df954ae702cd5fa2cd52f1ef8760e2/pypatronus-0.39.4-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:26c5f4f1f9504f0f1994028d538df2352fc1065c597116a725e89260d0876cfe", size = 11389009, upload-time = "2026-09-23T15:26:33.901Z" }, - { url = "https://files.pythonhosted.org/packages/2c/3a/efa7c4956ed08a5e8adf37d71f0a86ad36c8b69a2e99046f9be5665ae0b5/pypatronus-0.39.4-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:73c20828fc045278c230c3efb531467036cb1eee8699fb51feadf1531c609823", size = 12820150, upload-time = "2026-09-23T15:26:52.236Z" }, - { url = "https://files.pythonhosted.org/packages/ab/55/b6da29d5e5854d418bbaa3a81380718831fa0b683ff0c6d997eb68410e79/pypatronus-0.39.4-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:1b0bffd469615b28d8748d65022c60f826a49fa5cd95198b2c048a13a485768a", size = 1355081, upload-time = "2026-09-23T15:27:25.268Z" }, - { url = "https://files.pythonhosted.org/packages/07/7c/9213a3c4b8a1e84069e3d3c54a1041178c934fb1c0df5a6ab5f0b380f6be/pypatronus-0.39.4-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:829b9bfacb8116c1428ce50cf4ec381fef541d3f6da6bee2a2dfec26f0e7a39a", size = 1304210, upload-time = "2026-09-23T15:27:17.167Z" }, - { url = "https://files.pythonhosted.org/packages/5f/61/a86235251796315a15998c946ccddb6407dc32f3d43a42fa409f55296cc0/pypatronus-0.39.4-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e4ae9ec45854d57a3e9e28565bf2322b6955c1498daf95ceee2367b0b061df58", size = 11375383, upload-time = "2026-09-23T15:26:36.641Z" }, - { url = "https://files.pythonhosted.org/packages/c1/e5/ab2e88dbc8356905eff42693ef56ab765fa7acee45219d4dd57a6fd8b32f/pypatronus-0.39.4-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c71a95c261506f7b1c8c633da1d0c98b0ef5f3f59a85238d9c6792862f9c3c0d", size = 12804551, upload-time = "2026-09-23T15:26:54.943Z" }, - { url = "https://files.pythonhosted.org/packages/41/58/074783e08da59192c778f2306fe1b4c02206bb71276243964e4a2c24dd0f/pypatronus-0.39.4-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:0908bae1784a557c6988212b5069a70b002f5229ec823f56e6533abba243e7ae", size = 1356758, upload-time = "2026-09-23T15:27:26.723Z" }, - { url = "https://files.pythonhosted.org/packages/50/cf/5efdd697772bbf1dee3aef2d326765b00029a908b4189e74b0c61995ecff/pypatronus-0.39.4-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:935ef51c47fd9cb3447c9da3aafbe9cf13baf5a7bfaa09b7cdcde0a1cbb09d6b", size = 1304542, upload-time = "2026-09-23T15:27:18.803Z" }, - { url = "https://files.pythonhosted.org/packages/d6/c9/f5305c838e2ff8df951937f7e3e13b0a730c39b1334a1a15499914a816cf/pypatronus-0.39.4-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f1501a66d6b19914054f5e85f0a36fb4c62408d227bc61850752fc5affca4689", size = 11388751, upload-time = "2026-09-23T15:26:39.401Z" }, - { url = "https://files.pythonhosted.org/packages/c7/e9/ef03f0234bc27d0d467da816e94da53a4240449ab93f4baf25671f5c085d/pypatronus-0.39.4-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9e7d4a1b1a1ea861e77926ff9f61c1ed9185b6fd5aa67ff83877d12139e72029", size = 12819176, upload-time = "2026-09-23T15:26:57.68Z" }, - { url = "https://files.pythonhosted.org/packages/e6/9e/ca47355de00e1ec1212ff236a1efbb2db963f33c637bbfc3060ef8c59a1e/pypatronus-0.39.4-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:281e40fd874ce3f313063c59f12d19b360cdd75e55296cae49fda7532c01edb3", size = 11378886, upload-time = "2026-09-23T15:26:42.026Z" }, - { url = "https://files.pythonhosted.org/packages/b8/9f/2a9e028c01bce830ae6a1a56670eb30236591b318fcafb02c66f642a1f07/pypatronus-0.39.4-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0ae20e59f9c555a18add4e1d8590f2fe36b43783e3a760f7486e6aab860327d2", size = 12808220, upload-time = "2026-09-23T15:27:00.588Z" }, - { url = "https://files.pythonhosted.org/packages/05/69/3858448f6e0c04191f736b5be61eca719c3dbdd774f14eb3d081524c8b99/pypatronus-0.39.4-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8306db067caf115cf139defa9d515f28fe648ca886e47b418c0ec6e8dbc04428", size = 12818469, upload-time = "2026-09-23T15:27:03.576Z" }, - { url = "https://files.pythonhosted.org/packages/79/43/c03116e7e9f2060a2c791386ae70dc838061bad20df10987e8c4517beea1/pypatronus-0.39.4-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5d6a73801c97b4b2fd18e762a9ca9f0c4af5a60f2065501792deb43c33d4a784", size = 12813180, upload-time = "2026-09-23T15:27:06.684Z" }, + { url = "https://files.pythonhosted.org/packages/b2/8c/d753c244df8d436634b0c1da0a33074f1b5128922717fdd91e5c989517e0/pypatronus-0.39.5-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:adbada4e50463dcd51e1ecefcc994542f699b756777ee570b438196643de5ef9", size = 1368775, upload-time = "2026-09-25T20:19:02.761Z" }, + { url = "https://files.pythonhosted.org/packages/55/b8/0ca721b513bbbfd675005cbcd4cc3116811a59d8bdfe33ce41edf4ac3f0a/pypatronus-0.39.5-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:96d1e0722b402efff02f2a63cf2fc2907b67bda8a13adcab8d66a19755d34446", size = 1314158, upload-time = "2026-09-25T20:18:55.137Z" }, + { url = "https://files.pythonhosted.org/packages/b1/f3/7d77e350abd380efd89df7e4ba325e5ea4209889b8734168cfb06338b170/pypatronus-0.39.5-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2cf8fbdb9c39996dd1ebef614076fe9a33c142570442ac1ce5b19b9e3f1aa3d5", size = 11437871, upload-time = "2026-09-25T20:18:16.998Z" }, + { url = "https://files.pythonhosted.org/packages/13/51/ae378088d50e5cf6a9b0363aae0de37f6b73fb8a77488efb75cc74d6500b/pypatronus-0.39.5-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c4dc6770af3c8b97539587ec3e2252f663f20b6b07edfa4e4e4a1ec496e886a7", size = 12863483, upload-time = "2026-09-25T20:18:35.031Z" }, + { url = "https://files.pythonhosted.org/packages/b0/2f/0f4e5398285a7f4fd30fb3c772165f0da3ca08db2ed09ced776527ab528f/pypatronus-0.39.5-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:033c634754b5c75548546249b372bbf00da4f6c1db9476d9a5e0d7e0f65d0665", size = 1365593, upload-time = "2026-09-25T20:19:04.137Z" }, + { url = "https://files.pythonhosted.org/packages/31/76/d02f486099926dc1adde3b818ecc0d3ddba43f2e1a6ea95596d6451ae723/pypatronus-0.39.5-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:ce4c7b3dd43edc26f68de4710c0b96919063c61f3eeef776a3bc964f4c89414d", size = 1312488, upload-time = "2026-09-25T20:18:56.666Z" }, + { url = "https://files.pythonhosted.org/packages/5e/2e/9b1a3cae640e0a59b73a03a9ff3d2269d607081c6bfc2557b57e80929da3/pypatronus-0.39.5-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:54795acba6c4725581d5e3fef9a1702b175c79a4b71538951bd2f59625730be9", size = 11430450, upload-time = "2026-09-25T20:18:19.483Z" }, + { url = "https://files.pythonhosted.org/packages/d0/01/7e1b311c023448e24a1a03d11d2a76c787eecabc7f291260cf2e491f535d/pypatronus-0.39.5-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c153fcc31d53cc2bd0dafb56310134105248918f30edda7f636e8b13149a750e", size = 12861356, upload-time = "2026-09-25T20:18:37.759Z" }, + { url = "https://files.pythonhosted.org/packages/15/10/fded6138dfa69b52b1663ece790b0609722004e3a4752129e6009f2604cd/pypatronus-0.39.5-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:64de5946abc19f9dec7650aa7b91fa9ac35d0172a735d72723efa712a7264804", size = 1367451, upload-time = "2026-09-25T20:19:05.886Z" }, + { url = "https://files.pythonhosted.org/packages/25/ca/5193090cdbe69affae4ca5d1633bc1977fd0d3a47110c3acd09b742b497c/pypatronus-0.39.5-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:d79d2fe6a97a5c220257a43ad387afea5eac113e1ba3b9a784c480662034109a", size = 1313529, upload-time = "2026-09-25T20:18:58.063Z" }, + { url = "https://files.pythonhosted.org/packages/6d/f6/43d5ede4aa093ffe2b207b0535b4fa236ab24d1c6e50678f3d371e3c097a/pypatronus-0.39.5-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:859ef04c3fc657005ad9f9b2b56162195d7f2caf2bd0397ad1b0be1d3a86f51d", size = 11447634, upload-time = "2026-09-25T20:18:22.032Z" }, + { url = "https://files.pythonhosted.org/packages/28/1f/6fe5603bb64212d51322632dc350b3a9d2fd0c7510a8937c63cedb200f68/pypatronus-0.39.5-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b57aed7f26e88822f130c1458eade8a766fd6dbde0e599b6e538437ee206775a", size = 12876729, upload-time = "2026-09-25T20:18:40.404Z" }, + { url = "https://files.pythonhosted.org/packages/81/21/ca2f8bb5d893e80099fc893bb2b406ee888f9c848ee8746cb5f0613d63d8/pypatronus-0.39.5-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:25e3590c7fba02b77254180c4d5086e0a24889c2254d363f5f7e038b7fbd07a8", size = 11428036, upload-time = "2026-09-25T20:18:24.874Z" }, + { url = "https://files.pythonhosted.org/packages/00/dc/d3c8af251d614e8725e7f68f790c8be787b14cde45d32ec0efb67792eb13/pypatronus-0.39.5-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c93398ec3e5f247406c45870a504961f765e9097c2bc1f376795c81b202f961f", size = 12857872, upload-time = "2026-09-25T20:18:42.956Z" }, + { url = "https://files.pythonhosted.org/packages/be/cb/1d136c62154d9182783e372a2554131762a377ecfb9d099b44523dea6436/pypatronus-0.39.5-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d3a09c832fea282d3187ee3a527f1c853857d770eecc502972fcb23cd055b039", size = 12874848, upload-time = "2026-09-25T20:18:45.354Z" }, + { url = "https://files.pythonhosted.org/packages/81/b5/f1d79bd45167b7c97203ebad60f196d60b3e74f185e613cb81377310b872/pypatronus-0.39.5-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:cbe7cb2c6cfea3d77b15bf62c95fef883e93bb4dd2c7ae297f71a0c43eb48ed5", size = 12865604, upload-time = "2026-09-25T20:18:48.033Z" }, ] [[package]] From 5ac96c14acf91894769396233fc7a3e6c3eac309 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 28 Sep 2026 12:53:51 -0400 Subject: [PATCH 13/15] fun: wip models with state --- functional-models/fun.py | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index bc9b9753..2b2655cd 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -2,7 +2,7 @@ from dataclasses import dataclass, field from typing import Optional -from pypatronus import TransitionSystem, BitVec, ExprRef, BitVecVal +from pypatronus import TransitionSystem, State, BitVec, ExprRef, BitVecVal, If @dataclass @@ -17,15 +17,13 @@ class Method: name: str inputs: list = field(default_factory=list) outputs: list = field(default_factory=list) - nexts: list = field(default_factory=list) + nexts: Optional[list] = None # indicates whether the method can be executed based on the current model state guard: Optional[ExprRef] = None def verify_model(m: FunctionalModel): - assert len(m.states) == 0, "TODO: deal with states" for method in m.methods: - assert len(method.nexts) == len(m.states) allowed_symbols = set(m.states) | set(method.inputs) for out_name, out_expr in method.outputs: @@ -33,6 +31,20 @@ def verify_model(m: FunctionalModel): assert len(unallowed) == 0, ( f"Output {out_name}={out_expr} uses symbols that are neither inputs nor state: {unallowed}" ) + + if method.nexts is not None: + assert len(method.nexts) == len(m.states), ( + f"[{method.name}] {len(method.nexts)} next state assignments, but model has {len(m.states)} states." + ) + for state, next in zip(m.states, method.nexts): + assert state.sort() == next.sort(), ( + f"[{method.name}] {state} : {state.sort()} = {next} : {next.sort()}" + ) + unallowed = next.symbols() - allowed_symbols + assert len(unallowed) == 0, ( + f"[{method.name}] State update {state}={next} uses symbols that are neither inputs nor state: {unallowed}" + ) + # check guard if method.guard is not None: allowed_symbols = set(m.states) @@ -43,9 +55,9 @@ def verify_model(m: FunctionalModel): def serialize(m: FunctionalModel, filename): - assert len(m.states) == 0, "TODO: deal with states" verify_model(m) sys = TransitionSystem(name=m.name) + next_states = list(m.states) for t in m.methods: commit_signal = BitVec(f"{t.name}_commit", 1) sys.add_input(commit_signal) @@ -59,6 +71,14 @@ def serialize(m: FunctionalModel, filename): for out_name, out_expr in t.outputs: out_expr = out_expr.replace(input_map) sys.add_output(f"{t.name}_out_{out_name}", out_expr) + if t.nexts is not None: + for idx, next in enumerate(t.nexts): + expr = next.replace(input_map) + next_states[idx] = If(commit_signal, expr, next_states[idx]) + assert len(next_states) == len(m.states) + sys.states = [ + State(sym.name(), next=next) for (sym, next) in zip(m.states, next_states) + ] info = { "name": m.name, From 932f1674735b5ce2ff3588fadb65e6b493651088 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 28 Sep 2026 20:23:24 -0400 Subject: [PATCH 14/15] fifo functional model working --- functional-models/fun.py | 4 +++- functional-models/main.py | 9 ++++---- functional-models/pyproject.toml | 2 +- uv.lock | 38 ++++++++++++++++---------------- 4 files changed, 28 insertions(+), 25 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index 2b2655cd..89f15548 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -83,8 +83,10 @@ def serialize(m: FunctionalModel, filename): info = { "name": m.name, "methods": [t.name for t in m.methods], - "states": [s.name for s in m.states], + "states": [s.name() for s in m.states], } + print(sys) + with open(filename, "w") as f: json.dump({"info": info, "sys": sys.to_btor2_str()}, f) diff --git a/functional-models/main.py b/functional-models/main.py index 4b4de514..dc5ec205 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -39,13 +39,14 @@ def fifo(data_width: int, num_elements: int, push_pop: bool = False): """https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/fifo/FifoSpec.scala""" counter_width = 12 assert num_elements < ((1 << (counter_width - 1)) - 1) - mem = Array("mem", data_width, num_elements) + mem = Array("mem", counter_width, data_width) count = BitVec("count", counter_width) read = BitVec("read", counter_width) m = FunctionalModel(name="fifo", states=[mem, count, read]) num_elements_bv = BitVecVal(num_elements, counter_width) full = count.equals(num_elements_bv) - empty = count.equals(BitVecVal(0, counter_width)) + zero = BitVecVal(0, counter_width) + empty = count.equals(zero) input = BitVec("input", data_width) non_wrap = count + read @@ -53,7 +54,7 @@ def fifo(data_width: int, num_elements: int, push_pop: bool = False): read_plus_one = read + BitVecVal(1, counter_width) read_incr = If( read_plus_one.equals(num_elements_bv), - BitVecVal(0, counter_width), + zero, read_plus_one, ) @@ -80,7 +81,7 @@ def fifo(data_width: int, num_elements: int, push_pop: bool = False): ], ~empty, ), - Method("reset"), + Method("reset", nexts=[mem, zero, zero]), Method("idle"), ] if push_pop: diff --git a/functional-models/pyproject.toml b/functional-models/pyproject.toml index 278850e2..daf1593b 100644 --- a/functional-models/pyproject.toml +++ b/functional-models/pyproject.toml @@ -5,5 +5,5 @@ description = "Add your description here" readme = "README.md" requires-python = ">=3.12" dependencies = [ - "pypatronus==0.39.5", + "pypatronus==0.39.6", ] diff --git a/uv.lock b/uv.lock index afb970c6..d34c42b9 100644 --- a/uv.lock +++ b/uv.lock @@ -17,7 +17,7 @@ dependencies = [ ] [package.metadata] -requires-dist = [{ name = "pypatronus", specifier = "==0.39.5" }] +requires-dist = [{ name = "pypatronus", specifier = "==0.39.6" }] [[package]] name = "protocols" @@ -40,26 +40,26 @@ dev = [ [[package]] name = "pypatronus" -version = "0.39.5" +version = "0.39.6" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/35/2d/faf77267fffdf83f6eba8d5df9eaa23d25fa12aa6685578b0b96fd3849de/pypatronus-0.39.5.tar.gz", hash = "sha256:0d32e1d3f6c2c948b1c08c8a15d347fb65bcbc7443604a651f4eb73aca68b224", size = 165664, upload-time = "2026-09-25T20:19:07.386Z" } +sdist = { url = "https://files.pythonhosted.org/packages/cd/85/e410a6b325d785c3d972afaca878133014897982b1530d68dbbf6ee4d73c/pypatronus-0.39.6.tar.gz", hash = "sha256:e6e12b2424d615b991dc7af64fe5a8fd30cf9df561532a0bf269095eadd94ace", size = 166087, upload-time = "2026-09-28T20:33:53.254Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/b2/8c/d753c244df8d436634b0c1da0a33074f1b5128922717fdd91e5c989517e0/pypatronus-0.39.5-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:adbada4e50463dcd51e1ecefcc994542f699b756777ee570b438196643de5ef9", size = 1368775, upload-time = "2026-09-25T20:19:02.761Z" }, - { url = "https://files.pythonhosted.org/packages/55/b8/0ca721b513bbbfd675005cbcd4cc3116811a59d8bdfe33ce41edf4ac3f0a/pypatronus-0.39.5-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:96d1e0722b402efff02f2a63cf2fc2907b67bda8a13adcab8d66a19755d34446", size = 1314158, upload-time = "2026-09-25T20:18:55.137Z" }, - { url = "https://files.pythonhosted.org/packages/b1/f3/7d77e350abd380efd89df7e4ba325e5ea4209889b8734168cfb06338b170/pypatronus-0.39.5-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2cf8fbdb9c39996dd1ebef614076fe9a33c142570442ac1ce5b19b9e3f1aa3d5", size = 11437871, upload-time = "2026-09-25T20:18:16.998Z" }, - { url = "https://files.pythonhosted.org/packages/13/51/ae378088d50e5cf6a9b0363aae0de37f6b73fb8a77488efb75cc74d6500b/pypatronus-0.39.5-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c4dc6770af3c8b97539587ec3e2252f663f20b6b07edfa4e4e4a1ec496e886a7", size = 12863483, upload-time = "2026-09-25T20:18:35.031Z" }, - { url = "https://files.pythonhosted.org/packages/b0/2f/0f4e5398285a7f4fd30fb3c772165f0da3ca08db2ed09ced776527ab528f/pypatronus-0.39.5-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:033c634754b5c75548546249b372bbf00da4f6c1db9476d9a5e0d7e0f65d0665", size = 1365593, upload-time = "2026-09-25T20:19:04.137Z" }, - { url = "https://files.pythonhosted.org/packages/31/76/d02f486099926dc1adde3b818ecc0d3ddba43f2e1a6ea95596d6451ae723/pypatronus-0.39.5-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:ce4c7b3dd43edc26f68de4710c0b96919063c61f3eeef776a3bc964f4c89414d", size = 1312488, upload-time = "2026-09-25T20:18:56.666Z" }, - { url = "https://files.pythonhosted.org/packages/5e/2e/9b1a3cae640e0a59b73a03a9ff3d2269d607081c6bfc2557b57e80929da3/pypatronus-0.39.5-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:54795acba6c4725581d5e3fef9a1702b175c79a4b71538951bd2f59625730be9", size = 11430450, upload-time = "2026-09-25T20:18:19.483Z" }, - { url = "https://files.pythonhosted.org/packages/d0/01/7e1b311c023448e24a1a03d11d2a76c787eecabc7f291260cf2e491f535d/pypatronus-0.39.5-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c153fcc31d53cc2bd0dafb56310134105248918f30edda7f636e8b13149a750e", size = 12861356, upload-time = "2026-09-25T20:18:37.759Z" }, - { url = "https://files.pythonhosted.org/packages/15/10/fded6138dfa69b52b1663ece790b0609722004e3a4752129e6009f2604cd/pypatronus-0.39.5-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:64de5946abc19f9dec7650aa7b91fa9ac35d0172a735d72723efa712a7264804", size = 1367451, upload-time = "2026-09-25T20:19:05.886Z" }, - { url = "https://files.pythonhosted.org/packages/25/ca/5193090cdbe69affae4ca5d1633bc1977fd0d3a47110c3acd09b742b497c/pypatronus-0.39.5-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:d79d2fe6a97a5c220257a43ad387afea5eac113e1ba3b9a784c480662034109a", size = 1313529, upload-time = "2026-09-25T20:18:58.063Z" }, - { url = "https://files.pythonhosted.org/packages/6d/f6/43d5ede4aa093ffe2b207b0535b4fa236ab24d1c6e50678f3d371e3c097a/pypatronus-0.39.5-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:859ef04c3fc657005ad9f9b2b56162195d7f2caf2bd0397ad1b0be1d3a86f51d", size = 11447634, upload-time = "2026-09-25T20:18:22.032Z" }, - { url = "https://files.pythonhosted.org/packages/28/1f/6fe5603bb64212d51322632dc350b3a9d2fd0c7510a8937c63cedb200f68/pypatronus-0.39.5-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b57aed7f26e88822f130c1458eade8a766fd6dbde0e599b6e538437ee206775a", size = 12876729, upload-time = "2026-09-25T20:18:40.404Z" }, - { url = "https://files.pythonhosted.org/packages/81/21/ca2f8bb5d893e80099fc893bb2b406ee888f9c848ee8746cb5f0613d63d8/pypatronus-0.39.5-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:25e3590c7fba02b77254180c4d5086e0a24889c2254d363f5f7e038b7fbd07a8", size = 11428036, upload-time = "2026-09-25T20:18:24.874Z" }, - { url = "https://files.pythonhosted.org/packages/00/dc/d3c8af251d614e8725e7f68f790c8be787b14cde45d32ec0efb67792eb13/pypatronus-0.39.5-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c93398ec3e5f247406c45870a504961f765e9097c2bc1f376795c81b202f961f", size = 12857872, upload-time = "2026-09-25T20:18:42.956Z" }, - { url = "https://files.pythonhosted.org/packages/be/cb/1d136c62154d9182783e372a2554131762a377ecfb9d099b44523dea6436/pypatronus-0.39.5-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d3a09c832fea282d3187ee3a527f1c853857d770eecc502972fcb23cd055b039", size = 12874848, upload-time = "2026-09-25T20:18:45.354Z" }, - { url = "https://files.pythonhosted.org/packages/81/b5/f1d79bd45167b7c97203ebad60f196d60b3e74f185e613cb81377310b872/pypatronus-0.39.5-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:cbe7cb2c6cfea3d77b15bf62c95fef883e93bb4dd2c7ae297f71a0c43eb48ed5", size = 12865604, upload-time = "2026-09-25T20:18:48.033Z" }, + { url = "https://files.pythonhosted.org/packages/9f/0a/29baaaee767a80ed8982aaaee2addf7cf6afe118f4a7e283a81e64d697bd/pypatronus-0.39.6-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:49d80ce4aa5940e0d0f9c393af95decadba685984b834e988c81feafe22a4585", size = 1369317, upload-time = "2026-09-28T20:33:48.129Z" }, + { url = "https://files.pythonhosted.org/packages/44/3e/2afdedbe5b7a2392dbdb4282d8aa1e68cac588eefee6a2b3bc113e7a87ea/pypatronus-0.39.6-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f427e8941f1ccdd0b0cdb2769e7c03f0d4697907f18bff9da106f91d0d5465a8", size = 1315216, upload-time = "2026-09-28T20:33:40.127Z" }, + { url = "https://files.pythonhosted.org/packages/ac/5a/6534999bd1b5fce10d1a00d94294c46160beb93e8ac49875f35d797baf9b/pypatronus-0.39.6-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:59c37c4d10441c45890aafe86d0f788064bcece288bc4327d926ca8a8363f944", size = 11461735, upload-time = "2026-09-28T20:33:02.393Z" }, + { url = "https://files.pythonhosted.org/packages/a9/9a/065a980897c626297415c4e661e9a8ef7cc1a79dea80b68551932536c2cd/pypatronus-0.39.6-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:57bfdd3708f1381d9b1344ee505c7d56b0763f4d5b542a1c5237fd3073c517b4", size = 12893120, upload-time = "2026-09-28T20:33:19.827Z" }, + { url = "https://files.pythonhosted.org/packages/26/c2/d9fe790d27c8697c18455d7b5d32a47021d94a10359d21405e7096152c5b/pypatronus-0.39.6-cp313-cp313-macosx_10_12_x86_64.whl", hash = "sha256:e523531200d65d6d739fc7793340e12623f10b591178c8342331ca80a870e150", size = 1368247, upload-time = "2026-09-28T20:33:49.713Z" }, + { url = "https://files.pythonhosted.org/packages/ee/bd/05c2bfa7da1e5ca8cb1c9d0de1ab15d1e0ffc45681f3b0e6b71644dc8a85/pypatronus-0.39.6-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:7a288550ced1c6ab6c605866447439228132e70ae1a6de18896467c6c82dad92", size = 1314683, upload-time = "2026-09-28T20:33:41.803Z" }, + { url = "https://files.pythonhosted.org/packages/b8/d4/63992b9ce8b61a4a1cc07dd09897bcf2bee28b9773aaed201875a7855fd2/pypatronus-0.39.6-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:bf41eae6a93aeb0a2833e545fa4c7bdb9c7238e3ac76351a2472676e714b1725", size = 11461964, upload-time = "2026-09-28T20:33:04.647Z" }, + { url = "https://files.pythonhosted.org/packages/53/c0/95a2a9f1af211fbdb3c513137c8d36ca73ebe4c923ef45c352bae02070cc/pypatronus-0.39.6-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d68fc25825396671ce9e78bb957097c2ac7775aac51989a2eb36824aa1ca68cb", size = 12879933, upload-time = "2026-09-28T20:33:22.277Z" }, + { url = "https://files.pythonhosted.org/packages/60/9b/9b08580ecbdcab0ad1fa09a56803d5d498ac0a16a94c4cf9056f5c5ce90e/pypatronus-0.39.6-cp314-cp314-macosx_10_12_x86_64.whl", hash = "sha256:3b66b2a7219a69a82608477fed2db9a008be0a56da12799ec0136c8930ee22d9", size = 1369875, upload-time = "2026-09-28T20:33:51.932Z" }, + { url = "https://files.pythonhosted.org/packages/d8/44/1f99e3b2719d4f8ab89b9161b5d8abc7b30180cef02174cb27c58df60aad/pypatronus-0.39.6-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:4a71b25176b43c0da296001e36c8844d0e16a393fefe14933095f8559778e521", size = 1315648, upload-time = "2026-09-28T20:33:43.259Z" }, + { url = "https://files.pythonhosted.org/packages/6c/48/99c56ca7822e49f9b8f30564534386abd1901d5abff687b6a62c72938a29/pypatronus-0.39.6-cp314-cp314-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7da76e07d964cb89ce5a31d1e588ca9d5c479b3d3c466d0dd9b8be2e2220680f", size = 11470857, upload-time = "2026-09-28T20:33:07.36Z" }, + { url = "https://files.pythonhosted.org/packages/0d/bb/e93ee9569de4c760b98947cce80bfdbd63434d0a0326c89d2aa30a4c9c7d/pypatronus-0.39.6-cp314-cp314-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e20c3db284e858429dd242f064f226229a1bd8e83a0d995dcda43a6ce551ba68", size = 12898658, upload-time = "2026-09-28T20:33:24.741Z" }, + { url = "https://files.pythonhosted.org/packages/19/4d/b530a6480c8517af372807f90c0392cfbf05eb44bb98fa6da290e845a6cd/pypatronus-0.39.6-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:991cfdb0a835ba949b9838476ba4113566e62d7e2fca2fc414c1f33cd7c6168d", size = 11448543, upload-time = "2026-09-28T20:33:09.915Z" }, + { url = "https://files.pythonhosted.org/packages/46/99/30b72c81569dff0df6119ffdc12c9648d22332c0e82559301be954955d6a/pypatronus-0.39.6-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:aeb6a1aa38f1d8de5157633cb2484c6789121852219fb113b0c33ca00b6e244d", size = 12878008, upload-time = "2026-09-28T20:33:27.455Z" }, + { url = "https://files.pythonhosted.org/packages/9f/77/81fa121d8c10ca6dce74bac9ff0ab751d42e78c165e4503ee410775a6562/pypatronus-0.39.6-cp315-cp315-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fa95bb311e5d2f9cc224bb958aa7475d89b268420e447d88c015aad58d8ecd3e", size = 12897710, upload-time = "2026-09-28T20:33:30.023Z" }, + { url = "https://files.pythonhosted.org/packages/59/73/dd8bc9350163762dbbf4b52287c15023dc6ff80a097f877dbe4e6c19dd73/pypatronus-0.39.6-cp315-cp315t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d64dddd65ee6ee86a12c7c729aeed0a39a9333088c2e4baddcd09004a0faf600", size = 12884091, upload-time = "2026-09-28T20:33:32.571Z" }, ] [[package]] From fe8369bb42f7ba695834c66434b310d5223aa7ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 29 Sep 2026 09:29:00 -0400 Subject: [PATCH 15/15] generate more fifo models + wip python simulator --- functional-models/fun.py | 66 ++++++++++++++++++++++++++++++++------- functional-models/main.py | 19 +++++++++-- 2 files changed, 70 insertions(+), 15 deletions(-) diff --git a/functional-models/fun.py b/functional-models/fun.py index 89f15548..1cb7409e 100644 --- a/functional-models/fun.py +++ b/functional-models/fun.py @@ -1,25 +1,62 @@ import json from dataclasses import dataclass, field -from typing import Optional +from typing import Optional, Tuple -from pypatronus import TransitionSystem, State, BitVec, ExprRef, BitVecVal, If +from pypatronus import ( + TransitionSystem, + State, + BitVec, + ExprRef, + BitVecVal, + If, + Interpreter, +) @dataclass -class FunctionalModel: +class Method: name: str - methods: list = field(default_factory=list) - states: list = field(default_factory=list) + inputs: list[ExprRef] = field(default_factory=list) + outputs: list[Tuple[str, ExprRef]] = field(default_factory=list) + nexts: Optional[list[ExprRef]] = None + # indicates whether the method can be executed based on the current model state + guard: Optional[ExprRef] = None @dataclass -class Method: +class FunctionalModel: name: str - inputs: list = field(default_factory=list) - outputs: list = field(default_factory=list) - nexts: Optional[list] = None - # indicates whether the method can be executed based on the current model state - guard: Optional[ExprRef] = None + methods: list[Method] = field(default_factory=list) + states: list[ExprRef] = field(default_factory=list) + + +class Sim: + def __init__(self, model: FunctionalModel): + self.sys = _build_sys(model) + self.model = model + self.sim = Interpreter(self.sys) + for idx, m in enumerate(model.methods): + # note: python lambdas capture the context instead of the value of idx be default which is why + # we need the nested lambdas! + setattr( + self, + m.name, + ( + lambda ii: ( + lambda *args, **kwargs: self._exec_method(ii, *args, **kwargs) + ) + )(idx), + ) + + def _exec_method(self, idx: int, *args, **kwargs): + assert len(kwargs) == 0, "TODO: support keyword args" + method = self.model.methods[idx] + inputs = list(args) + assert len(inputs) == len(method.inputs), ( + f"Wrong number of inputs {len(inputs)} != {len(method.inputs)}" + ) + + assert False, f"TODO: exec {method.name} {inputs}" def verify_model(m: FunctionalModel): @@ -54,7 +91,7 @@ def verify_model(m: FunctionalModel): ) -def serialize(m: FunctionalModel, filename): +def _build_sys(m: FunctionalModel) -> TransitionSystem: verify_model(m) sys = TransitionSystem(name=m.name) next_states = list(m.states) @@ -79,6 +116,11 @@ def serialize(m: FunctionalModel, filename): sys.states = [ State(sym.name(), next=next) for (sym, next) in zip(m.states, next_states) ] + return sys + + +def serialize(m: FunctionalModel, filename): + sys = _build_sys(m) info = { "name": m.name, diff --git a/functional-models/main.py b/functional-models/main.py index dc5ec205..891390e0 100644 --- a/functional-models/main.py +++ b/functional-models/main.py @@ -3,7 +3,7 @@ # author: Kevin Laeufer from pypatronus import BitVec, SignExt, ZeroExt, Slice, Update, If, Array, BitVecVal -from fun import FunctionalModel, Method, serialize +from fun import FunctionalModel, Method, serialize, Sim def picorv32_pcpi_mul(): @@ -100,12 +100,25 @@ def fifo(data_width: int, num_elements: int, push_pop: bool = False): return m +def test_fifo(m: FunctionalModel, num_elements: int, push_pop: bool = False): + sim = Sim(m) + # sim.push(123) + # assert sim.pop() == 123 + pass # TODO: implement simulator for testing + + def main(): serialize(picorv32_pcpi_mul(), "picorv32_pcpi_mul.json") - params = [{"data_width": 32, "num_elements": 5}] + params = [ + {"data_width": 32, "num_elements": 8}, + {"data_width": 32, "num_elements": 16}, + {"data_width": 32, "num_elements": 128}, + ] for p in params: file_name = "fifo_" + "_".join(f"{k}={v}" for k, v in p.items()) + ".json" - serialize(fifo(**p), file_name) + m = fifo(**p) + test_fifo(m, num_elements=p["num_elements"]) + serialize(m, file_name) if __name__ == "__main__":