Merge remote-tracking branch 'origin/main' into update_monitor

Author: ngernest

.github/workflows/test.yml

@@ -22,13 +22,22 @@ jobs:
     - name: Update Rust to ${{ matrix.toolchain }}
       run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
     - uses: actions/checkout@v4
+    - uses: actions/setup-python@v4
+      with:
+        python-version: '3.13'
     - uses: YosysHQ/setup-oss-cad-suite@v3
       with:
         version: '2024-05-07'
     - name: Build
       run: cargo build --verbose
-    - name: Run tests (Debug)
+    - name: Run unit tests (Debug)
       run: cargo test --verbose
+    - name: Install uv
+      uses: astral-sh/setup-uv@v5
+    - name: Install Turnt 
+      run: uv tool install turnt
+    - name: Run Turnt snapshot tests
+      run: turnt $(find . -type f -name '*.tx') 
 
   msrv:
     name: Check Minimum Rust Version for protocols library

README.md

@@ -13,6 +13,7 @@ A protocol is described using an `fn` definition containing a list of imperative
   - Note: this presumes you already have `uv` installed (if not, [follow these instructions](https://docs.astral.sh/uv/getting-started/installation/#pypi))
 - Run `cargo build` to build
 - Run `just test` to execute all unit tests (`cargo test`) + snapshot tests (via Turnt)
+  - Run `just turnt` to only run Turnt snapshot tests
 
 **CLI**:
 The interpreter has a CLI, which can be invoked as follows:

examples/picorv32/pcpi_mul.prot

@@ -1,4 +1,5 @@
-struct picorv32 {
+struct picorv32_pcpi_mul {
+  in resetn: u1,
   in pcpi_insn: u32,
   in pcpi_rs1: u32,
   in pcpi_rs2: u32,
@@ -8,32 +9,47 @@ struct picorv32 {
   out pcpi_rd: u32,
 }
 
-// Adapted from https://github.com/ekiwi/transactional-verification-with-protocols/blob/039fb8d5beafb3c4a464e5dac3dc8a3e00b69f04/picorv32/picorv32_pcpi_mul.py
-fn pcpi_mul<p: picorv32>(
+// Adapted from https://github.com/ekiwi/paso/blob/ad2bf83f420ca704ff0e76e7a583791a0e80a545/benchmarks/src/benchmarks/picorv32/PicoRV32Spec.scala#L27
+fn pcpi_mul<p: picorv32_pcpi_mul>(
     in rs1_data: u32,
     in rs2_data: u32,
     out rd_data: u32,
     in insn: u32,
   ) {
+  // TODO: can we decoupled this from the transaction?
+  p.resetn := 1'b1;
+
+
+  p.pcpi_valid := 1'b1;
+  // HACK: pass multiplication instruction as input
   p.pcpi_insn := insn;
   // p.pcpi_insn := 33554483; // multiplication insn. TODO: allow binary values
+
+
   p.pcpi_rs1 := rs1_data;
   p.pcpi_rs2 := rs2_data;
 
   assert_eq(p.pcpi_wr, 1'b0);
   assert_eq(p.pcpi_ready, 1'b0);
 
-  step();
+  while (!(p.pcpi_ready == 1'b1)) {
+    step();
+  }
 
   p.pcpi_valid := 1'b0;
   p.pcpi_insn := X;
   p.pcpi_rs1 := X;
   p.pcpi_rs2 := X;
 
-  while (!(p.pcpi_ready == 1'b1)) {
-    step();
-  }
 
   assert_eq(p.pcpi_wr, 1'b1);
   assert_eq(p.pcpi_rd, rd_data);
+
+  // TODO: do we need/want this step?
+  step();
 }
+
+fn pcpi_mul_reset<p: picorv32_pcpi_mul>() {
+  p.resetn := 1'b0;
+  step();
+}

examples/picorv32/unsigned_mul.out

@@ -0,0 +1 @@
+Protocol executed successfully!

examples/picorv32/unsigned_mul.tx

@@ -0,0 +1,6 @@
+// ARGS: --verilog picorv32/picorv32.v --protocol picorv32/pcpi_mul.prot --module picorv32_pcpi_mul
+pcpi_mul_reset();
+pcpi_mul(1, 1, 1, 0x2000033);
+pcpi_mul(1, 100, 100, 0x2000033);
+pcpi_mul(100, 1, 100, 0x2000033);
+pcpi_mul(33554483, 200, 2415929304, 0x2000033);

examples/serv/serv_regfile.out

@@ -0,0 +1 @@
+Protocol executed successfully!

examples/serv/serv_regfile.tx

@@ -0,0 +1,11 @@
+// ARGS: --verilog serv/rtl/serv_regfile.v --protocol serv/serv_regfile.prot 
+// Arguments to transaction are:
+// rs1_addr: u5
+// rs1_data: u32 (output)
+// rs2_data: u32 (output)
+// rs2_addr: u5
+// rd_enable: u1
+// rd_addr: u5
+// rd_data: u32
+read_write(0, 0, 0, 0, 1, 5, 0xdeadbeef);
+read_write(5, 0xdeadbeef, 0, 0, 0, 0, 0);

examples/tinyaes128/aes128.out

@@ -0,0 +1 @@
+Protocol executed successfully!

examples/tinyaes128/aes128.tx

@@ -0,0 +1,4 @@
+// ARGS: --verilog tinyaes128/aes_128.v --protocol tinyaes128/aes128.prot --module aes_128
+// Arguments are key, state, expected output
+aes128(0x000102030405060708090a0b0c0d0e0f, 0x00112233445566778899aabbccddeeff, 0x69c4e0d86a7b0430d8cdb78070b4c55a);
+aes128(0x00000000000000000000000000000000, 0x00000000000000000000000000000000, 0x66e94bd4ef8a2c3b884cfa59ca342b2e);

examples/turnt.toml

@@ -0,0 +1 @@
+command = "cargo run --package protocols-interp -- --color never --transactions {filename} {args}"