Thursday, October 20, 2011

SystemVerilog Assertions: Introduction to the language

What is  SystemVerilog Assertions (SVA) ?
SystemVerilog Assertions (SVA) is a  language for precisely specifying the DUT behavior ( functionality or property ) but do not constitute a golden model.

SVA is describing DUT functionality ( property ) that is to be there and it is given directive to verification to
  • verify                         ( assert    (  property )     verification directive )
  • assume                      ( assume (  property )     verification directive )
  • measure coverage    ( cover    (  property )     verification directive )

the functionality described.

Assertion checking is a simple addition to a  simulation-based verification methodology, adding additional monitors of DUT functionality.
e.g. You can use assertions to monitor the interface of a module: assertions will quickly identify when the protocols or sequences of the interface signals are incorrect.

The DUT functionality  represented by an assertion can be
  • combinational (boolean) or
  • temporal (extended over time).


  • Default  $error severity task

By default, when an assertion fails, the simulator calls the $error severity task, which displays an error message. No action is taken by default when an assertion passes.

All possibilities of a SVA failure severity tasks are:
$fatal is a run-time fatal.
$error is a run-time error.
$warning is a run-time warning, which can be suppressed in a tool-specific manner.
—  $info indicates that the assertion failure carries no specific severity.




SVA described here are represented in a testbench as a custom property.

There are two kinds of assertions: concurrent and immediate:

  • Immediate assertions tests an expression when the statement is executed in the procedural code.
  • Concurrent assertions are based on clock and  can describe Boolean behaviors or patterns of behavior that span over time.



From design specification to SVA based verification

e.g.  A simple synchronous request - acknowledge protocol design (DUT)

  • Excerpt from the DUT specification

This is a synchronous design on clock (clk), in other words all input and output signals change ( except POR,  input signal reset_n)  only on a positive edge of clk.
Output signal ack has value 0 while POR ( input signal reset_n=0).  Input signal  req can be raised at any time  and must stay asserted until output signal ack is asserted Once both req and ack are asserted in the next clock cycle both req and ack must be de-asserted.

  • How SVA is extracted from the specification:

      • DUT has three inputs ( clock, reset_n and req)  and one output (ack)
      • reset_n is asynchronous, active low signal


      • Test vector generation assumptions ( SVA Implementation HINT,  use :assume )  about input signal req that must be respected during verification ( in relation to  DUT output signal ack)
        • one cycle after ack, req must be de-asserted

property pr2;
 @(posedge clk) ack |=> !req;
endproperty
assume_ack2:assume property (pr2);


        • hold req asserted until and one clock cycle after ack is asserted

property pr3;
 @(posedge clk) req |-> req[*1:$] ##0 ack;    
endproperty
assume_ack3:assume property (pr3);

      • Verify following DUT functionality (SVA Implementation HINT,  use :assert )of DUT the output signal  ack
        • while  reset_n=0 or req=0, ack must be held: 0

property pa1;
 @(posedge clk) !reset_n || !req |-> !ack;
endproperty
assert_req1:assert property (pa1)
 else $display("\n ack asserted while req is still de-asserted");

        • once   reset_n=1 and req=1, ack must become and stay 1, during one clock cycle and after the clock cycle go back to 0 again.

property pa2;
 @(posedge clk) ack |=> !ack;
endproperty
assert_req2:assert property (pa2)
 else $display("\n ack is extended over more than one cycle");




SVA vs. Verilog HDL


e.g. A detail of DUT functionality  to verify:  

  • signal if request ( req ) change from 0 to 1, within next 3 rising edge clocks  ( clk  ), signal acknowledge ( ack ) should change from 0 to 1 too.


  • Verilog HDL

always @(posedge req)
    begin

           repeat (1) @(posedge clk);

           fork: pos_pos
                  begin
                           @(posedge ack)
                           $display("Assertion Success",$time);
                           disable pos_pos;
                  end

                 begin
                         repeat (2) @(posedge clk);
                        $display("Assertion Failure",$time);
                        disable pos_pos;
                 end
        join

end // always

  • SVA equivalent to previous HDL


assert property (
@(posedge clk) $rose(req)|-> ##[1:3] $rose(ack)
)
else $display(“Assertion Failure",$time) ;

SVA Immediate Assertions


assert(expression) action_block

An immediate assertion tests an expression when the statement is executed in the procedural code. If the expression is interpreted as true, the assertion passes. If the expression is interpreted as false, the assertion fails.

The expression is non-temporal and is interpreted the same way as an expression in the condition
of a procedural if statement. Also the expression is not defined under a sequence or propery.



SVA Immediate Assertions  are good for combinational checks

e.g. On positive edge clk, every time state is in REQ , check there is either req1or req2. If this in not truth assertion fail, otherwise pass.
time t;
always @(posedge clk)
  if (state == REQ)
     assert (req1 || req2)
     else begin
       t = $time;
      #5 $error("assert failed at time %0t",t);
     end


Since the fail statement, like the pass statement, is any legal SystemVerilog procedural statement, it can also be used to signal a failure to another part of the testbench.

e.g > assert (myfunc(a,b)) count1 = count + 1; else ->event1;

e.g > assert (y == 0) else flag = 1;

e.g >

always @(read_n || address) begin

 case (bank)
  "RAM_BANK_0" : mem_delay = 5;
  "ROM_BANK_0" : mem_delay = 10;
  "RAM_BANK_1" : mem_delay = 15;
 default :
    begin
// Here, an assertion is used inside a case statement.
// It checks that the correct names of memory bank variables are used.
//
        assert(0); else $error("Unexpected bank setting. %s\n",bank);
        mem_delay = 0; /* Default */
    end
endcase
end



SVA Concurrent Assertions


Unlike immediate assertions, the evaluation model is based on a clock such that a concurrent assertion is evaluated only at the occurrence of a clock tick.

The clock expression that controls evaluation of a sequence can be more complex than just a single signal name.
e.g;  Expressions such as (clk && gating_signal) and (clk iff gating_signal) can be used to represent a gated clock

The simplest form of concurrent assertion checks a combinational logic at every clock event.

e.g. at every rising edge of the clk both of request signals can not be high at the same time

assert property (
  ( @ posedge clk )
! ( request1 && request2 )
) else $error( “ ERROR: Both requests active at the same time”)

SVA Language Layers


Boolean expressions

• Evaluated at a single clocking event (combinational).
  • Verilog operators supported with Verilog semantics


Sequences

DUT functionality ( or property ) can be described in sequences or  may involve checking of one or more sequences beginning at various times.  

e.g. > Sequence : a ##1 b ##c, describes this DUT functionality:
  • after  signal  a transitions from 0 to 1, signal b MUST transition 0 to 1 on  next clock cycle and finally after b becomes 1 signal c MUST transition to 0 t 1 in the next clock cycle .

e.g. > Sequence : b ##[1:4] c, describes this DUT functionality:
  • after  signal  b transitions from 0 to 1,  after 1 or 2 or 3 or 4 clock cycles signal c MUST transition 0 to 1 as well.



      ##n

Specifies the number of clock cycles that occur between sequence expressions. The number of clock cycles can be 0, to specify no delay.

Leading Delay

“##n S” specifies a delay of n clock events until the beginning of the match of S
- n must be a non-negative integer, compile-time
constant
- “##0 S” is equivalent to “S”
- “##n S” is equivalent to “1’b1 ##n S”, n > 0
-      ##1 a // means 1’b1 ##1 a
-      ##2 a // means 1’b1 ##1 1’b1 ##1 a

e.g > a ##2 b // means a ##1 1’b1 ##1 b


e.g. > The following example defines a property, P1, which checks that if a is true, and b is true two clock cycles later, then c must be true one clock cycle after that. The concurrent assertion, A1, causes this property to be checked during simulation or formal analysis.
property P1;
    @(negedge clk) (a ##2 b) |=> (c);
endproperty

A1: assert property (P1);


e.g> This example defines a sequence, S1, that takes two arguments. S1 specifies that after the first argument occurs, the second argument must occur from zero to two clock cycles later. The sequence S2 instantiates S1 and passes the arguments b and a to S1.

sequence S1(AA, BB);
  (AA ##[0:2] BB);
endsequence

sequence S2;
    S1(b,a);
endsequence

    ##[start:end]

Specifies a range of clock cycles. Specifies a delay range of at least
start and at most end clock events

e.g. “req” that changes 0 to 1  on positive edge of the clock, will be followed with “ack” change from 0 to 1, 1 to 3 positive edge clock later

sequence x ;
 req ##[1:3] ack ;
endsequence

req ##[1:3] ack is same as:

req |-> ##[1] ack or
req |-> ##[2] ack or
req |-> ##[3] ack

e.g. ##[0:3]a // means (a) or (1’b1 ##1 a) or (1’b1 ##1 1’b1 ##1 a) or
(1’b1 ##1 1’b1 ##1 1’b1 ##1 a)



  • Sequences can be composed of other sequences.


e.g>
sequence s;
a ##1 b ##1 c;
endsequence

sequence rule;
@(posedge sysclk)
trans ##1 start_trans ##1 s ##1 end_trans;
endsequence

Sequence rule in the preceding example is equivalent to:
sequence rule;
@(posedge sysclk)
trans ##1 start_trans ##1 a ##1 b ##1 c ##1 end_trans ;
endsequence


  • Although sequences can be composed of other sequences, cyclic dependency of sequences is not allowed

e.g. Example of illegal cyclical dependency of two sequences: sequence s1 depends on sequence s2 and further s2 depend on s1

sequence s1;
@(posedge sysclk) (x ##1 s2);
endsequence

sequence s2;
@(posedge sysclk) (y ##1 s1);
endsequence



Concatenation sequences

Sequences can be composed by concatenation.
The concatenation specifies a delay, using ##, from the end of the first sequence until the beginning of the second sequence.




Overlapped concatination
If in a sequence composed by concatination, specifified delay between two sequencies with overlapped concatination  ##0, this means that second sequnce can start eventhough the first one did not finished yet.

e.g. (a ##1 b ##1 c) ##0 (d ##1 e ##1 f) // overlapped concatenation
Is equal to
a ##1 b ##1 c&&d ##1 e ##1 f


Consecutive Repetition


<boolean expression> [*count]

b[*n] matches over n consecutive clock events, b Boolean expression
b[*0] matches over . . . zero clock events!

e.g > a[*1:3] is equivalent to
a or (a ##1 a) or (a ##1 a ##1 a)

e.g. when  ready transitioned from 0 to 1,it  stays 1 during 3 consecutive clock cycles

sequence ready_3 ;
 ready ##1 ready ##1 ready :
endsequence

OR

sequence ready_3 ;
 ready[ * 3] :
endsequence

e.g> ack cannot be active for k consecutive cycles,” where k is a parameter

assert property ( not ack[*k ] ) ;

e.g. >
( clk ##1 !clk )[*3]
is equivalent to
( ( clk ##1 !clk ) ##1 ( clk ##1 !clk ) ##1 ( clk ##1 !clk ) )
which is equivalent to
( clk ##1 !clk ##1 clk ##1 !clk ##1 clk ##1 !clk )

You can also use  [*] for [0:$], and [+] for [1:$].

delay and repetition in the same sequence
e.g> 1’b1 ##3 (a [*3]) // means 1’b1 ##1 1’b1 ##1 1’b1 ##1 a ##1 a ##1 a

e.g> (1’b1 ##2 a) [*3] // means (1’b1 ##2 a) ##1 (1’b1 ##2 a) ##1
// (1’b1 ##2 a), which in turn means 1’b1 ##1 1’b1 ##1
// a ##1 1’b1 ##1 1’b1 ##1 a ##1 1’b1 ##1 1’b1 ##1 a

e.g> (a ##2 b) [*5]
This is the same as:
(a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)

consecutive repetition operator [*min:max]
A repetition with a range of min minimum and max maximum number of iterations

e.g> (a ##2 b)[*1:5]
is equivalent to
(a ##2 b)
or (a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)
or (a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)

e.g>
(a[*0:3] ##1 b ##1 c)
is equivalent to
(b ##1 c)
or (a ##1 b ##1 c)
or (a ##1 a ##1 b ##1 c)
or (a ##1 a ##1 a ##1 b ##1 c)

e.g>
Once risen, xfer must remain high up to and including the
cycle of the next activation of done

|-> (Overlapped implication) and ##0 are used to allow done to rise concurrently with xfer

e.g>
•         The following are equivalent:
§  S |-> (T |-> U)
§  (S ##0 T) |-> U


assert property (
 $rose(xfer) |-> xfer [*1:$] ##0 done
);



Non-consecutive repetition ( [= )
This operator applies to a Boolean. The resulting sequence matches any trace in which
the operand occurs for a specified number or range of cycles, which might or might not
be consecutive.

e.g. > a[=3] matches the traces (a, a, a), (a, b, b, a, b, a), and (b, a, b, b, a, b, a, b, b, b)


Go to repetition operator[-> …
This operator applies to a Boolean. The resulting sequence matches any trace in whichthe operand occurs for a specified number or range of cycles, which might or might not be consecutive, provided that the last occurrence is in the last cycle in the trace

e.g. > a[->3] matches the traces (a, a, a), (a, b, b, a, b, a), and (b, a, b, b, a, b, a)

e.g If there is a valid start signal ( on posetive edge of the clock) , 2 clocks latter, signal “a” will repeat 3 times ( continuously or intermittently ) before there is a valid “stop” signal

assert property ( clk)
 @(posedge clk) $rose(start) |->
   ##2 (a[->3] ) ##1 stop ;
endproperty
);.

•         “!b[*0:$] ##1 b” matches at the nearest concurrent or future occurrence of boolean b
  • SVA provides goto operator “b[->1]” for this idiom


•         “(!b[*0:$] ##1 b)[*n]” is a common idiom for the nth occurrence of b
  • SVA provides goto operator “b[->n]” for this idiom


Goto Operator

b[ -> n ] :  Go to n-th occurance of
Unbounded consecutive repetition

e.g. if “req” rises, then as long as “wait” is held high
consecutively, “ack” must not be asserted

property wait_no_ack;
($rose(req) ##0 wait[*1:$]|-> !ack) ;
endproperty

: e.g> req is high up to, but not necessarily including, the next cycle
that ack is high

sequence req_until_ack_2;
req [*0:$] ##1 ack;
endsequence

Same As:

sequence req_until_ack_2;
ack or
req[*1] ##1 ack or
req[*2] ##1 ack or
...
endsequence


  • Using very large repeat values, such as ack[*20000000], uses a large amount of memory, but unbounded repeat values, such as ack[*], do not.


SVA Sequence Operators



SVA Operator: and


The requirement for the match of  the and operation is that both the sequences must match.

Specifies that two sequence expressions must begin in the same clock cycle, but they do not need to end during the same cycle.

When one of the operand sequences matches, it waits for the other to match. The end time of the composite sequence is the end time of the operand sequence that completes last.

e.g> (a ##2 b) and (c ##2 d ##2 e)


Properties


Properties are built up out of sequence.

The result of property evaluation is either true or false.

There are seven kinds of property:
1)       sequence,
2)        negation
e.g> For each evaluation attempt of the property, there is an evaluation attempt of
not property_expr

3)       Disjunction
property_expr1 or property_expr2

4)    Conjunction
property_expr1 and property_expr2

5)    , if...else
if (expression_or_dist) property_expr1 else property_expr2

6)    implication,
       sequence_expr |-> property_expr ( overlapped implication )
            or the form
    sequence_expr |=> property_expr ( non-overlapped implication )


7)    and instantiation


If the statement appears in an always block, the property is always monitored. If the statement appears in an initial block, then the monitoring is performed only on the first clock tick.
e.g>
property rule;
 a ##1 b ##1 c;
endproperty

always @(posedge clk) begin
  <statements>
  assert property (rule);
end

In general it is a good idea to define the clocks in property definitions and keep the sequences independent of the clocks, to reuse sequences.
e.g; clocking example in relation to sequences and properties
sequence x ;
a ##2 b ;
endsequence

property y ;
@(posedge clk )  x ;
endproperty

assert property (y) ;

“disable iff (exp)”

  • specifies that property evaluation should abort and return true any time

“exp” evaluates to true. When “exp” is a signal, it is checked asynchronously.

  • “disable iff (exp)” can be placed only at the top level of an assert/cover property statement.
  • Nested disable iff directives are not allowed.


e.g > aborting checks on reset

|=> (Non-overlapped implication)

sequence_expr |=> property_expr
is equivalent to:
sequence_expr ##1 1’b1 |-> property_expr

e.g>
•         The following are equivalent:
§  S |=> (T |=> U)
§  (S ##1 T) |=> U


Don’t confuse “a ##1 b” ( continuously checked ) with “a |=> b” ( only checked when a is true, with the exception when used in initial block .


|=>” is essentially the same as “|-> ##1”. The latter can be
generalized to “|-> ##n


e.g. if  “ack” change from  0 to 1 it will stay 1 only one clock cycle.In other words “ack ”can not be active two consecutive cycles.

assert property ( ack |=> !ack ) ; // if ack next clock cycle !ack

OR

assert property ( ack |-> ##1  !ack ) ; // if ack next clock cycle !ack

OR

assert property ( not ( ack ##1 ack ) ;

OR

assert property ( not ( ack [*2]  ) ;


SVA Untyped ( arguments declared without a data type )  Formal Arguments

Not recommended

e. g. > sequence S2 (CC, DD);
    (a ##1 CC) or (b ##1 DD);
endsequence

S1_assertion: assert property
    (@(negedge clk) (S1(b,c)) |=> S2((e||f), g));

SVA Typed ( arguments declared with a data type )   Formal  Arguments


Recommeded

e.g > sequence S1 (bit AA, bit BB);
    (a ##1 AA ##1 BB);
endsequence

e.g. > In the following example, Property P5 shows one argument, AA, that is untyped, and one argument that is of type bit, b.
property P5 (AA, bit BB);
            @(negedge clk)
            (BB ##1 c) |=> (AA ##[1:2] (d||AA));
endproperty

e.g. > You can pass a signal that is used as an event argument (clk), but not the event (@clk). For example, you can use
property exampl1(clk,x,y);
            @(clk) x |=> y;
endproperty

but you cannot use
property exampl1(@clk,x,y);
@(clk) x |=> y;
endproperty


  • When you instantiate a sequence or property, the argument list can be either:

1) name-associated or
2) positional.

e.g.> named_association: assert property P5 (.AA(my_AA), .BB(my_BB));

e.g.> sequence BusReq (min=0, max=0);
           REQ ##[min:max] ACK;
        endsequence

Default clocking: (Recommended)


A default clocking block:
  • specifies the clock or event that controls the evaluation of sequences or properties within the block.  Or


  • attaches a clocking event to every assume/assert/cover property statement in the module that does not have its clock specified otherwise.


assertions in clocking blocks are not permitted by the IEEE 1800 standard

e.g. > default clocking master_clk @(posedge clk);
            property p4; (a |=> ##2 b); endproperty
            endclocking : master_clk
assert property (p4);

e.g. > default clocking master_clk @(posedge clk);
       endclocking

sequence x ;
 req ##1 ack ;
endsequence

assert property (x) ;
assert property ( req ##1 ack && req ##1 ack );

e.g>
clocking pos_clk @(posedge clk);
...
endclocking : pos_clk
default clocking pos_clk;


As an alternative to specifying a default clock, you can place assertions in an always or initial block

An inferred clock takes precedence over a default clock.

e.g> // @(posedge clk) applies to all assertions in the block.
always @(posedge clk) begin
 A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
 A2i: assert property ( (a[*3]) |=> ~c );
 A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end

An initial block might or might not have an inferred clock. It is executed once.
// @(posedge clk) applies to all assertions in the block.
initial @(posedge clk) begin
 A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
 A2i: assert property ( (a[*3]) |=> ~c );
 A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end

A local clock targeted at limited number of properties

e.g>
clocking boo @( posedge clk)

  property bleh ;
     req |=> ack ;
  endproperty

endclocking

a_bieh: assert property (boo.bleh) ;


Clocking options


The clock for a property can be specified in several ways

  • Clock inferred from always block


Eg> always @(posedge clk) begin
            A1i: assert property ( (a ##1 b) |=> (c ##1 d) );
            A2i: assert property ( (a[*3]) |=> ~c );

            A3i: assert property ( (a ##1 b ##1 c) |=> (d[*2:4]) );
end


eg> always @(posedge clk)
begin
a1: assert property($past(ack) |-> !ack);
c1: cover property(req ##1 ack);
end

  • Explicit clock in assert/cover property statement:


eg>

a1: assert property(
@(posedge clk) $past(ack) |-> !ack
);

e.g>
a1: assert property(
@(posedge clk) $past(ack) |-> !ack
);
c1: cover property(
@(posedge clk) req ##1 ack
);

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

o Explicitly specified in the property:
 property p;
    @(posedge clk) a ##1 b;
 endproperty
 assert property (p);

o Explicitly specified in the concurrent assertion:
 assert property (@(posedge clk) a ##1 b);

o Inferred from a procedural block:
 property p;
    a ##1 b;
 endproperty
always @(posedge clk) assert property (p);

SVA Multiple Clocks

Multiply-clocked sequences are built by concatenating singly-clocked subsequences using the single-delay
concatenation operator ##1

e.g. > assert property (@(posedge clk1) (a ##1 b) |=> @(posedge clk2) (c ##1 d));

Multiple-clock sequences must be built by concatenating single-clocked sub-sequences using the single-delay concatenation operator, ##1, or the |=> implication operator.

The delay is understood to be from the endpoint of the first sequence that occurs at the tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins.

For a multi-clocked assertion, the clocks are explicitly specified. No default clock or inferred clock is used. Inaddition, multi-clocked properties are not allowed to be defined within a clocking block.

A multi-clocked property assert statement must not be embedded in procedural code where a clock is inferred.
For example, following forms are not allowed.
always @(clk) assert property (mult_clock_prop);// illegal
initial @(clk) assert property (mult_clock_prop);// illegal

multiply-clocked properties

The boolean property operators (not, and, or) can be used freely to combine singly- and multiply-clocked
Properties

e.g> (@(posedge clk0) sig0) and (@(posedge clk1) sig1)
is a multiply-clocked property, but it is not a multiply-clocked sequence.

This property evaluates to true at a point if and only if the two sequences
@(posedge clk0) sig0
and
@(posedge clk1) sig1
both have matches beginning at the point.

e.g> property using clock flow and if...else

property mult_p8;
 @(posedge clk) a ##1 b |->
 if (c)
    (1 |=> @(posedge clk1) d)
 else
    e ##1 @(posedge clk2) f ;
endproperty
Here, a, b, c, and e are clocked at posedge clk.

e.g>
sequence s;
//sequence composed of two named subsequences
@(posedge s_clk) e ##1 s1 ##1 s2 ##1 f;
endsequence


sequence s1;
@(posedge clk1) a ##1 b; // single clock sequence
Endsequence

sequence s2;
@(posedge clk2) c ##1 d; // single clock sequence
endsequence


SVA Local Variable Usage

The local variables declared in one sequence are not visible in the sequence where it gets instantiated

As shown in the following example, when valid_in is true, the x variable is assigned the value of data_in. If data_out is equal to x + 1 five cycles later, the property is true. Otherwise, the property is false. When valid_in is false, this property evaluates vacuously (idle, empty:  devoid of serious occupation) to true.
e.g. >  property pipeline;
            int x;
            @(posedge clk) disable iff (reset)
            (valid_in, x = data_in) |=> ##5 (data_out == (x+1));
endproperty

The following example shows the use of a packed struct as a local variable:
e.g. > // Pipeline data check
typedef struct packed signed {reg[7:0] x, y;} data_struct;

property ex1;
            data_struct ldata;
            @(posedge clk)
            (valid_in, ldata.x=data_in) |-> ##5 (data_out == ldata.x)
endproperty


e.g.
  • When “req” change from 0 to 1, max_delay[3:0]  is valid.
  • max_delay[3:0] is assumed to be nonzero when it  is valid.
  • if  “req” rises and remain high, then “ack” must be asserted no later then max_delay-th cycle after the “req”


property variable_ack_response_time;
reg[3:0] l_md ;
( $rose(req), l_md = max_delay )
         |=>
         ( req && !ack, l_md = l_md -1)[*1:$]
         |-> ( l_md > 0 ) ;
endproperty



Coverage



·         Functional coverage
offers an insight on how the verification goals set by a test plan are being met, and can be performed on user-defined coverage points, specified using SystemVerilog assertions, or covergroup statements

Functional coverage can be:
  • Control-Oriented Using SVA Statements
  • Data-Oriented Using SystemVerilog Covergroup


coverage metrics:
1) Line coverage
Counts executions of each line in the specification file.

2) cover property statement coverage
           “cover property (p)” should be used only when “p” is a sequential property

3)  covergroup coverage
Tracks a user-specified set of variable values and reports combinations of values that are not covered.

1 comment:

  1. This comment has been removed by a blog administrator.

    ReplyDelete