Hi,
I was trying to understand the working of ‘implies’ operator : edalink using code from stackoverflow
As per the link :
( p1 implies p2 ) is equivalent to ( not p1 or p2 )
So my expectation was :
(1) For +define+M1: As not( a ##1 b ) is false , my expectation is that assertion should pass at T:15
(2) For +define+M2: As ( a ##1 b ) is true at T:15 , not( a ##1 b ) is false . Hence assertion fails at T:15
(3) For +define+M3: As ‘c’ is true at T:5 , the expectation was that assertion passes at T:5. However there is No pass or failure
(4) For +define+M4: My expectation is that since ‘a’ is false at T:5, not( a ##1 b ) is true at T:5 . As a result assertion should have passed at T:5
However there is no pass at T:5
Any suggestions why the output is different ? Is the equivalent expression incorrect ?
A quick google search led me to the following link : htmllink
The signal sig should be high from m>=0clock ticks before event ev happens until n>=0clock ticks after it.
That is, if ev happens at time 10, m=2,and n=3, then sig should be high at times 8, 9, .. , 13
// For m = 2 and n =3 :
a1: assert property (strong(##2 ev) implies sig[*(6)]) ; // Assume default clocking exists
[Q2] What is the equivalent expression for a1 ? I am not clear on how it satisfies the requirement
On your requirements, I suggest one of the following solutions. I assumed that ev is a variable and not an event. The a2 is for delays and repeats that are fixed at elaboration time. The a1 solution uses delays and repeat values that are defined in variables; that uses my SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh Provides a library and model solutions
module tb;
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_range_pkg::*;
int pre=2, post=3;
bit sig, ev;
// Using from the package
// sequence dynamic_delay(count);
// sequence sq_rpt_simple_count(sq, count);
// For m = 2 and n =3 :
a1: assert property (strong(dynamic_delay(pre) ##0 ev) implies sig[*1:$] ##1 ev ##1 sq_rpt_simple_count(sig, post)) ;
a2: assert property (strong(##2 ev) implies sig[*1:$] ##1 ev ##1 sig[*3]) ;
sig 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
ev - - - - - 1 - - - - - - - - - - - - - - - - -
<--->
<--------->
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Hi Ben,
As you explain in the link that the equivalent expression is:
( ( not ( a ##1 b ) ) or c )
(1) For +define+M1: There are 2 attempts , one at T:5 and then the 2nd one at T:15
For the 1st attempt, sequence ( a ##1 b ) is False at T:15 , as a result my expectation was that assertion passes at T:15 ( due to not( false ) )
For the 2nd attempt due to not being a string operator the assertion fails at T:16 ( when simulation ends ), as the sequence ( a ##1 b ) isn’t complete i.e neither true or false.
The output I observe only shows an error at T:16 , why is there no pass at T:15 for the 1st thread ?
(2) For +define+M3: Since ‘c’ is true at T:5 and T:15 , my expectation was that there should 2 pass. one at T:5 and other at T:15.
However there is no pass or failure in the output.
(3) For +define+M4: As both ‘a’ and ‘c’ are false at T:5 , 15 there should have been 2 pass. One at T:5 and other at T:15 ( due to not ).
However there is no pass or failure in the output
As per the output I seem to be missing out on something , any suggestions ?