From 12e20b1da2df1d347b0badab80b23aa7f653482b Mon Sep 17 00:00:00 2001
From: Torsten Meissner <programming@goodcleanfun.de>
Date: Wed, 14 Nov 2018 12:08:31 +0100
Subject: [PATCH] Some small improvements

* Adopt init state generation for initial reset constraining
* Add assume about inactive reset after initial active
* Replaced OPC consts by macros
* Replace SVA reset check by simple unclocked immediate assertion
---
 alu/alu_t.sv | 51 +++++++++++++++++++++++++++++++--------------------
 1 file changed, 31 insertions(+), 20 deletions(-)

diff --git a/alu/alu_t.sv b/alu/alu_t.sv
index 2f98064..09dbbe8 100644
--- a/alu/alu_t.sv
+++ b/alu/alu_t.sv
@@ -1,7 +1,7 @@
 module alu_t (
-    input        Reset_n_i,
-    input        Clk_i,
-    input  [1:0] Opc_i,
+    input         Reset_n_i,
+    input         Clk_i,
+    input  [1:0]  Opc_i,
     input  [31:0] DinA_i,
     input  [31:0] DinB_i,
     output [31:0] Dout_o,
@@ -9,6 +9,12 @@ module alu_t (
 );
 
 
+  `define OPC_ADD 0
+  `define OPC_SUB 1
+  `define OPC_AND 2
+  `define OPC_OR  3
+
+
   alu alu_i (
     .Reset_n_i(Reset_n_i),
     .Clk_i(Clk_i),
@@ -19,38 +25,43 @@ module alu_t (
     .OverFlow_o(OverFlow_o)
   );
 
-  const logic [1:0] OPC_ADD = 0;
-  const logic [1:0] OPC_SUB = 1;
-  const logic [1:0] OPC_AND = 2;
-  const logic [1:0] OPC_OR  = 3;
 
-  initial begin
-    assume (!Reset_n_i);
+  reg init_state = 1;
+
+  // Initial reset
+  always @(*) begin
+    if (init_state) assume (!Reset_n_i);
+    if (!init_state) assume (Reset_n_i);
   end
 
+  always @(posedge Clk_i)
+    init_state = 0;
+
+
   bit unsigned [32:0] dina, dinb;
 
   assign dina = DinA_i;
   assign dinb = DinB_i;
 
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_ADD && (dina + dinb) > 2**32-1 |=> OverFlow_o);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_SUB && (dina - dinb) > 2**32-1 |=> OverFlow_o);
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
-  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD |=> Dout_o == ($past(DinA_i) + $past(DinB_i)));
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_ADD && (dina + dinb) > 2**32-1 |=> OverFlow_o);
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB |=> Dout_o == ($past(DinA_i) - $past(DinB_i)));
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_SUB && (dina - dinb) > 2**32-1 |=> OverFlow_o);
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_AND |=> Dout_o == ($past(DinA_i) & $past(DinB_i)));
+  assert property (@(posedge Clk_i) disable iff (!Reset_n_i) Opc_i == `OPC_OR |=> Dout_o == ($past(DinA_i) | $past(DinB_i)));
 
-  assert property (@(posedge Clk_i or negedge Clk_i) !Reset_n_i |-> Dout_o == 0);
+  always @(*)
+    if (!Reset_n_i) assert (Dout_o == 0);
 
   property cover_opc (opc);
     @(posedge Clk_i)
       disable iff (!Reset_n_i) Opc_i == opc;
   endproperty
 
-  cover property (cover_opc(OPC_ADD));
-  cover property (cover_opc(OPC_SUB));
-  cover property (cover_opc(OPC_AND));
-  cover property (cover_opc(OPC_OR));
+  cover property (cover_opc(`OPC_ADD));
+  cover property (cover_opc(`OPC_SUB));
+  cover property (cover_opc(`OPC_AND));
+  cover property (cover_opc(`OPC_OR));
 
 
 endmodule