diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index 51f3ece..b764540 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -1,63 +1,63 @@ module DUT ( - input logic clk, - output logic req, - output logic ack + input logic clk, + output logic req, + output logic ack ); `ifdef FORMAL - logic [1:0] reqs_seen; - logic [31:0] cycle_count; + logic [1:0] reqs_seen; + logic [31:0] cycle_count; - // Deterministic initial state - initial begin - // req = 1'b0; - reqs_seen = 2'b00; - cycle_count = 32'b0; - end + // Deterministic initial state + initial begin + reqs_seen = 2'b00; + cycle_count = 32'b0; + end - always @ (posedge clk) begin - if (req) reqs_seen <= reqs_seen + 1; - cycle_count <= cycle_count + 1; - end + always @ (posedge clk) begin + if (req) reqs_seen <= reqs_seen + 1; + cycle_count <= cycle_count + 1; + end - // Req is only high for one cycle - assume property (@(posedge clk) - req |-> ##1 !req - ); + // Req is only high for one cycle + assume property (@(posedge clk) + req |-> ##1 !req + ); - // Reqs are at least 8 cycles apart - assume property (@(posedge clk) - req |-> ##1 (!req [*7]) - ); + // Reqs are at least 8 cycles apart + assume property (@(posedge clk) + req |-> ##1 (!req [*7]) + ); - // ack comes exactly 4 cycles after req - assume property (@(posedge clk) - req |-> ##4 ack - ); + // ack comes exactly 4 cycles after req + assume property (@(posedge clk) + req |-> ##4 ack + ); - // ack must remain low if no req 4 cycles ago - assume property (@(posedge clk) - !$past(req,4) |-> !ack - ); + // ack must remain low if no req 4 cycles ago + assume property (@(posedge clk) + !$past(req,4) |-> !ack + ); - // For the purpose of demonstration, stop exactly when second req pulse - // occurs. This leaves us in a state where we're waiting for the second ack. - always @(posedge clk) begin - (* phase = "1" *) - cover(reqs_seen == 2); - end + // For the purpose of demonstration, stop exactly when second req pulse + // occurs. This leaves us in a state where we're waiting for the second + // ack. + always @(posedge clk) begin + (* phase = "1" *) + cover(reqs_seen == 2); + end - // In phase 2, assume that there's no more reqs; despite this, assert that - // an ack will eventually come for the second req. - always @ (posedge clk) begin - (* phase = "2" *) - assume(!req); - end - always @(posedge clk) begin - (* phase = "2" *) - cover(ack); - end + // In phase 2, assume that there's no more reqs; despite this, assert + // that an ack will eventually come for the second req. + always @ (posedge clk) begin + (* phase = "2" *) + assume(!req); + end + always @(posedge clk) begin + (* phase = "2" *) + cover(ack); + end `endif