The condition is that once sig_a is asserted, sig_b must be deasserted and must stay down until the next sig_a. I have written the assertions as follows
The condition is that once sig_a is asserted, sig_b must be deasserted and must stay down until the next sig_a. I have written the assertions as follows
Some comments:
[1] sig_a && !count |-> !sig_b throughout sig_a[->1] has issues:
sig_a[->1] is equivalent to: !sig_a[*0:$] ##1 sig_a
The antecedent is true when sig_a && !count is true, meaning that at that cycle sig_a==1.
( b throughout R ) is equivalent to ( b [*0:$] intersect R )
In your consequent, in the same cycle that sig_a==1, the sig_a[->1] is true.
Thus, your assertion boils down to simply:
*sig_a && !count |-> (!sig_b[*0] intersect sig_a) or (!sig_b[1] intersect sig_a)(
and that gets reduced to
*sig_a && !count |-> (0) or (!sig_b[1] intersect sig_a)( //!sig_b[*0] is a null
Thus, what you meant would be sig_a && !count |=> !sig_b throughout sig_a[->1]
[2] Your requirements are not clear. The code you wrote with the supporting logic asserts the following requirement:
Upon a rose of control signal “a” ==1 (your if(a && (count == 0)), at the next cycle of that
a" and when when sig_a ==1, sig_b must be deasserted and must stay down until the next sig_a.
MOST LIKELY NOT WHAT YOU WANT.
[3] On your " if(a && (count == 0))" did you mean “a” or “sig_a”?
If you meant “sig_a”, then you would miss the restart of the assertion on the 2nd occurrence of sig_a as the first occurrence would block the 2nd one (assuming you use |=> instead of |->).
[4]If you meant the use of a control signal called “a”, then you could write
[5]In my SVA Handbook 4th Edition I recommned that complex assertions be tested. I also describe a simple method to do that; htat method consists of putting the assertions into a test module, and using constrained-random tests on the variablea. Below is my template for verifying assertions (That template is saved in https://www.phraseexpress.com/ text abbreviation application, highl recommend this application.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
initial begin
$timeformat(-9, 1, "ns", 8);
$display("%t", $realtime);
end
always @(posedge clk) begin
end
// ASSERTIONS GOES HERE
// hERE IS A MODEL OF YOURS
ap: assert property(@ (posedge clk)
$rose(a) |-> b intersect a[->1] );
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
a <= va;
b <= vb;
end
$stop;
end
endmodule
The imlied requirements for this would be:
Upon a first occurrence of sig_a, sig_b remains at 0 until the next occurence of sig_a.
That 2nd occurrence of sig_a will not restart this sig_b check until a third occurrence of sig_a.
Is that really the requirements you want? I may be wrong, but intuitively, I would think that you have another triggering condition for that first occurrence of sig_a, maybe something from a combinational logic other than sog_a, or from a state machine. The reason I say that is that assertions should reflect requirements. The requirement that I implied from your code is odd. I would have expected something like:
When CONDx, then starting from the next (or current) cycle sig_b remains low until sig_a.
ap_siga2siga: assert property(@(posedge clk) $rose(CONDx) |=> // |-> ok here if needed
!sig_b throughout sig_a[->1]);
In reply to ben@SystemVerilog.us:
Thanks for the clarification Ben.
Actually, I am a novice in SVA. I was just practicing writing SVA for different conditions.
My SVA book explains 1800 chapter 16 and has many real examples, many of which were posed by users in forums.
My papers provide alternatives for handling complex assertions.
Ben systemverilog.us