From 4edfce0e03a32452b20fcbe23fff03c9cffb564d Mon Sep 17 00:00:00 2001
From: Alden0012 <ajs19@ic.ac.uk>
Date: Tue, 8 Nov 2022 17:27:39 +0000
Subject: [PATCH] Add initial assume to AHBGPIO.sv

---
 rtl/AHB_GPIO/AHBGPIO.sv | 61 +++++++++++++++++++++--------------------
 1 file changed, 32 insertions(+), 29 deletions(-)

diff --git a/rtl/AHB_GPIO/AHBGPIO.sv b/rtl/AHB_GPIO/AHBGPIO.sv
index 9140a48..48dc953 100644
--- a/rtl/AHB_GPIO/AHBGPIO.sv
+++ b/rtl/AHB_GPIO/AHBGPIO.sv
@@ -68,8 +68,6 @@ module AHBGPIO
   reg        last_HWRITE;
   reg        last_HSEL;
 
-  integer i;
-
   assign HREADYOUT = 1'b1;
 
 // Set Registers from address phase
@@ -115,38 +113,43 @@ module AHBGPIO
   //check behaviour
     
   assert_parity: assert property
-    ( @posedge(HCLK) disable iff (!HRESETn)
-      !PARITYERR;
-    );
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    !PARITYERR
+  );
 
   assert_gpio_write: assert property
-    ( @posedge(HCLK) disable iff (!HRESETn)
-      ((gpio_dir == 16'h0001)
-        && (HADDR[7:0] == gpio_data_addr)
-        && HSEL
-        && HWRITE
-        && HTRANS[1])
-      |-> (GPIOOUT[15:0] == $past(HWDATA[15:0], 1))
-    );
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((gpio_dir == 16'h0001)
+      && (HADDR[7:0] == gpio_data_addr)
+      && HSEL
+      && HWRITE
+      && HTRANS[1])
+    |-> (GPIOOUT[15:0] == $past(HWDATA[15:0], 1))
+  );
 
   assert_gpio_read: assert property
-    ( @posedge(HCLK) disable iff (!HRESETn)
-      ((gpio_dir == 16'h0000)
-        && (HADDR[7:0] == gpio_data_addr)
-        // && HSEL // HSEL not used in Read always_ff
-        && !HWRITE
-        && HTRANS[1])
-      |-> (HRDATA[15:0] == $past(GPIOIN[15:0], 1)
-           && HREADYOUT)
-    );
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((gpio_dir == 16'h0000)
+      && (HADDR[7:0] == gpio_data_addr)
+      // && HSEL // HSEL not used in Read always_ff
+      && !HWRITE
+      && HTRANS[1])
+    |-> (HRDATA[15:0] == $past(GPIOIN[15:0], 1)
+          && HREADYOUT)
+  );
 
   assert_gpio_dir: assert property
-    ( @posedge(HCLK) disable iff (!HRESETn)
-      ((HADDR[7:0] == gpio_dir_addr)
-        && HSEL
-        && HWRITE
-        && HTRANS[1])
-      |-> (gpio_dir == $past(HWDATA[15:0], 1))
-    );
+  ( @(posedge HCLK) disable iff (!HRESETn)
+    ((HADDR[7:0] == gpio_dir_addr)
+      && HSEL
+      && HWRITE
+      && HTRANS[1])
+    |-> (gpio_dir == $past(HWDATA[15:0], 1))
+  );
+
+  assume_initial_valid: assume
+  ( gpio_dir == 16'h0000
+    || gpio_dir == 16'h0001
+  );
 
 endmodule