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:
- 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
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
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3 - SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle
http://systemverilog.us/cmpts_free.pdf