Difference between |->(implication) and ##delay

Implication operator
|- >  work like a trigger

the simulation will be divided into two parts left and right 

will wait first for left side simulation, then will simulate right side

Delay :
##delay : simulation will occur on one line
so implication operator is beneficial as it will save a lot of tool effort and simulation will be faster

Difference between implication (->) and ##0 in SVA

First thing that you have to check is syntax of single implication operator that is a |-> b.

In SystemVerilog assertion, there are two expressions.
a ##0 b
a |-> b

Actually, it looks like a similar in expressions. First of this expression is checking a is asserted(1) and after 0 clock cycle b is asserted(1) or not. Second expression is checking b is (on)asserted when a is asserted(1) then on same posedge b is asserted(1) or not.

Now, practically when verification engineers wrote this kind of assertions they take care of following things.
a ##0 b: In this expression, if a is not asserted then it shows failure.
When a is asserted(1) and on same time stamp b is not asserted then also shows failure.

a |-> b: In this expression, if a is asserted and b is not asserted then it will show a failure.
If a is not asserted then it is not going to check whether b is asserted or not. This behaviour is different than a ##0 b.

If you apply different inputs data then you can see that expression a ##0 b will give you more failure than a |-> b. Reason for same is already explained above.

One more thing to note down is "The implication construct can be used only with property definitions. It cannot be used in sequences."

Source: stack overflow

Assertion

1. An Assertion specifies the behaviour of the system.
2. It validates the behaviour of design 
3. In addition, assertion can be used to provide functional coverage and generate input stimulus for validation


The advantage of assertion:
1. Improving observability 
2. reduce the debug time 
3. bugs can be found earlier and more isolated 
4. can interact with C function



types of assertion:
1.Immediate 
2. concurrent 


Immediate                                                                concurrent                            

based on simulation event                                       based on a clock cycle 
used without property keyword                                used with property keyword
placed in procedure block definition                        placed in procedural blocks, modules, interfaces or program                                                                                     definition

i) Immediate assertions are useful for combinational expression, similar to if else statement but with assertion control.
ii) Assertions are non-synthesizable
iii) Assertions can be written in design and TB both but in design, while synthesising need to remove so use `define


Difference between assert and cover :

assert: if you want scenario to be hold true then you write an assertion.
cover : Whether scenario ever happened in your simulation or not.


|-> implication operator

sequence s;
    @(posedge clk) a ##1 b;
  endsequence
 
  property p;
    a |-> s;
  endproperty
 
  assert property (p);
  cover property (p);