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
property p1;
@(posedge clk) sig_a && !count |-> (!sig_b throughout sig_a[->1]);
endproperty
always@(posedge clk)
begin
if(a && (count == 0))
count <= 1;
else if(a && count == 1)
count <= 0;
end
Is there any another way of writing assertions for the above condition without using always block?
In reply to Manoj J:
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:
[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
ap_ab: assert property(@(posedge clk)
sig_a && $rose(a) |=> (!sig_b throughout sig_a[->1]);
[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
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
[3] On your " if(a && (count == 0))" did you mean “a” or “sig_a”?
Sorry for the mistake. It is
always@(posedge clk)
begin
if(sig_a && (count == 0))
count <= 1;
else if(sig_a && count == 1)
count <= 0;
end
In reply to Manoj J:
With this assertion
ap_siga2siga: assert property(@(posedge clk) sig_a && !count |=>
!sig_b throughout sig_a[->1]);
always@(posedge clk)
begin
if(sig_a && (count == 0))
count <= 1;
else if(sig_a && count == 1)
count <= 0;
end
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]);
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
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.
In reply to Manoj J:
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.