From f2569b8ebed46d09511d493ec18219a3d98b26dc Mon Sep 17 00:00:00 2001
From: Mir Ruwayd Afeef <109923578+ruwayd99@users.noreply.github.com>
Date: Wed, 17 Jan 2024 19:42:20 -0800
Subject: [PATCH] Update bit4counter_assertions.sv

---
 bit4counter_assertions.sv | 33 +++++++++++++++------------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/bit4counter_assertions.sv b/bit4counter_assertions.sv
index d6dbcd4..8c7b17e 100644
--- a/bit4counter_assertions.sv
+++ b/bit4counter_assertions.sv
@@ -9,32 +9,29 @@ module bit4counter_assertions (
   // Property declarations
 
   // Property to check if reset resets the counter
-  property reset_resets_counter;
-    @(posedge clk) disable iff (!reset)
-    counter == 4'b0000;
+  property p_reset;
+  @(posedge clk)
+  reset |-> ##1 (counter == 4'b0000 && overflow == 0);
   endproperty
 
   // Property to check if the counter increments by 1
-  property combined_property;
-  @(posedge clk) disable iff (reset || counter == 4'b1111)
-  (
-    counter == $past(counter) + 1 &&
-    overflow == 0
-  );
-  endproperty
+  property p_increment;
+  @(posedge clk)
+  (!reset && $past(counter) != 4'b1111) |-> ##1 (counter == $past(counter) + 4'b0001 && overflow == 0);
+endproperty
 
   // Property to check if the counter overflows
-  property counter_overflow;
-    @(posedge clk) disable iff (reset || counter != 4'b1111)
-    overflow == 1;
-  endproperty
-
+  property p_overflow;
+  @(posedge clk)
+  (!reset && $past(counter) == 4'b1111) |-> ##1 (counter == 4'b0000 && overflow == 1);
+endproperty
+  
   // Assertion block to check the properties
   initial begin
     // Apply the properties in simulation
-    assert property (reset_resets_counter) else $fatal("Assertion reset_resets_counter failed");
-    assert property (combined_property) else $fatal("Assertion combined_property failed");
-    assert property (counter_overflow) else $fatal("Assertion counter_overflow failed");
+    assert property (p_counter) else $fatal("Assertion reset_resets_counter failed");
+      assert property (p_property) else $fatal("Assertion combined_property failed");
+      assert property (p_overflow) else $fatal("Assertion counter_overflow failed");
   end
 
 endmodule: bit4counter_assertions