In reply to emin:
Also, I don’t get the use of first_match clearly. What we would expect if there is no first_match in your
|-> first_match(##[1:10] pop && now_serving==v_serving_ticket)
##0 (out_data == push_data);
/* For a constrained range (e.g., ##[1:10] you can getaway without the first_match(),
but the error will be flagged on the 10th cycle in the above example.
Case 1: What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but
(out_data is unequal push_data)? In that case, you continue the search for other ##s
Now, what if in all the other ##s pop==0. The assertion fails on that last 10th cycle.
Case 2: */
|-> (##[1:$] pop && now_serving==v_serving_ticket)
##0 (out_data == push_data);
/* What if in ##2 (the 10 possible ##s) pop && now_serving==v_serving_ticket)==1 but
(out_data is unequal push_data)? In that case, you continue the search for other ##s
Now, what if in all the other ##s pop==0. The assertion NEVER fails.
You lost the opportunity to check it when pop && now_serving==v_serving_ticket)was ==1
at cycle 2. */
On the other question on uniqueness, see below (it is lengthy).
/* First-come/First-served, First-come/NO-others/Next-First-come, Expect.
* Since every successful attempt at an assertion initiate its own consequent,
if multiple concurrent assertions are in the active state waiting for a successful
consequent, any successful consequent with complete ALL of the pending assertions.
For example: @(posedge clk) $rose(req) |-> ##[1:10] ack;
* There are cases though when the requirements are searching for uniqueness,
and there are two possibilities for uniqueness:
- First-come/First-served and
- First-come/NO-others/Next-First-come
In a first-come puts all other-comes as recognized, but put into a waiting queue
to be served in that order when each first-come is finished with the transaction
(with a pass or a fail).
To accomplish this, one could use concepts of a familiar model seen in hardware stores
in the paint department. There, the store provides a spool of tickets, each with a number.
As a customer comes in, he takes a ticket. The clerk serving the customers has a sign that reads
"NOW SERVING, TICKET #X". The customer that has the ticket gets served,
the others have to wait. When done, the number X in incremented,
and the next in-line customer gets served. Here is a model for that: */
module top;
import uvm_pkg::*; `include "uvm_macros.svh"
timeunit 1ns; timeprecision 100ps;
bit clk,req, ack;
int ticket, now_serving;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
function void inc_ticket();
ticket = ticket + 1'b1;
endfunction
property reqack_unique;
int v_serving_ticket;
@(posedge clk) ($rose(req), v_serving_ticket=ticket, inc_ticket()) |->
first_match(##[1:10] now_serving==v_serving_ticket) ##0 ack;
endproperty
ap_reqack_unique: assert property(reqack_unique)
now_serving =now_serving+1; else now_serving =now_serving+1;
initial begin
repeat(100) begin
@(posedge clk); #1;
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error")
end
repeat(200) begin
@(posedge clk); #1
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=0, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
/* First-come/NO-others/Next-First-come
In this model, after a first-come the door is closed and all other-comes are not recognized.
When that first-come is done (pass or fail), the next first-come is accepted and the door is closed again.
To accomplish this, one could use concepts of a familiar model seen in a
store that only has a ONE-SPACE parking spot. If the spot is empty, a customer can park
and go to the store. If the spot is full, any new comer MUST leave because regulations do not allow
parking waiting for the spot; he can go around the block if he wants, but when he comes
back it is considered a new arrival.
The implemntation is similar to the previous model, but uses a lock/unlock. If lock is ON,
any new attempt beccomes vacuous. Below is a model: */
module top;
import uvm_pkg::*; `include "uvm_macros.svh"
timeunit 1ns; timeprecision 100ps;
typedef enum {UNLOCKED, LOCKED} lock_enum;
bit clk,req, ack;
lock_enum lock=UNLOCKED;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
function void lock_fnct(lock_enum x);
lock = x;
endfunction
property reqack_unique;
int v_serving_lock;
@(posedge clk) ($rose(req) && lock==UNLOCKED, lock_fnct(LOCKED)) |->
##[1:10] (ack, lock_fnct(UNLOCKED));
endproperty
ap_reqack_unique: assert property(reqack_unique) else lock_fnct(UNLOCKED);
initial begin
repeat(100) begin
@(posedge clk); #1;
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error")
end
repeat(200) begin
@(posedge clk); #1
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=0, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
/* What about the "expect" construct to achieve uniqueness.
The expect construct is not part of the “verification layer” because it does not make a statement
about what should be done with a property in terms of verification. However, the expect statement
makes use of a property. Specifically, the expect statement can appear anywhere a wait statement
can appear (e.g., always procedure, task (but not in classes!!!)). The expect statement is a procedural
blocking statement that allows waiting on a property evaluation.
The expect statement accepts the same syntax used to assert a property.
expect_property_statement ::= expect ( property_spec ) action_block
An expect statement causes the executing process to block until the given property succeeds or fails.
The statement following the expect is scheduled to execute after processing the Observed region
in which the property completes its evaluation.
When the property succeeds or fails, the process unblocks, and the property stops being evaluated
(i.e., no property evaluation is started until that expect statement is executed again).
<<< -- When executed, the expect statement starts a single thread of evaluation for the given property
on the subsequent clocking event, that is, the first evaluation shall take place on the next clocking event. -->>
If the property fails at its clocking event, the optional else clause of the action block is executed.
If the property succeeds, the optional pass statement of the action block is executed.
The execution of pass and fail statements can be controlled by using assertion action control tasks
The model below works like the unique-lock, but the simulator reports no statistis or
waveform or debug features. : */
module top;
import uvm_pkg::*; `include "uvm_macros.svh"
timeunit 1ns; timeprecision 100ps;
typedef enum {UNLOCKED, LOCKED} lock_enum;
bit clk,req, ack;
lock_enum lock=UNLOCKED;
event pass, fail;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
function void lock_fnct(lock_enum x);
lock = x;
endfunction
property reqack_unique;
int v_serving_lock;
@(posedge clk) ($rose(req) && lock==UNLOCKED, lock_fnct(LOCKED)) |->
##[1:10] (ack, lock_fnct(UNLOCKED));
endproperty
ap_reqack_unique: assert property(reqack_unique) else lock_fnct(UNLOCKED);
property reqack_expect;
int v_serving_lock;
@(posedge clk) $rose(req) |-> ##[1:10] ack;
endproperty
always
expect (reqack_expect) -> pass; else -> fail;
initial begin
repeat(100) begin
@(posedge clk); #1;
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=1, 1'b0:=5};
}) `uvm_error("MYERR", "This is a randomize error")
end
repeat(200) begin
@(posedge clk); #1
if (!randomize(req, ack) with
{ req dist {1'b1:=1, 1'b0:=3};
ack dist {1'b1:=0, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- Free books: Component Design by Example https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
- Papers: