From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001
From: Warrick Lo <wlo@warricklo.net>
Date: Wed, 24 Jun 2026 07:58:06 +0000
Subject: Add CI pipeline for formal verification

* Add formal verification tests with sby to CI
* Fix reviewdog having insufficient API permissions

See-also: #15
Signed-off-by: Warrick Lo <wlo@warricklo.net>
---
 dv/formal/simple_alu/simple_alu_bind.sv | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 dv/formal/simple_alu/simple_alu_bind.sv

(limited to 'dv/formal/simple_alu/simple_alu_bind.sv')

diff --git a/dv/formal/simple_alu/simple_alu_bind.sv b/dv/formal/simple_alu/simple_alu_bind.sv
new file mode 100644
index 0000000..8ed7057
--- /dev/null
+++ b/dv/formal/simple_alu/simple_alu_bind.sv
@@ -0,0 +1,15 @@
+// Bind file for simple_alu formal verification.
+// Attaches simple_alu_fv to every instance of simple_alu in the design.
+// RTL is completely unaware of this file.
+//
+// bind <dut_module> <fv_module> <instance_name> (<port_connections>);
+
+bind simple_alu simple_alu_fv u_simple_alu_fv (
+    .clk      (clk),
+    .rst      (rst),
+    .a        (a),
+    .b        (b),
+    .sel      (sel),
+    .y        (y),
+    .overflow (overflow)
+);
-- 
cgit v1.2.3