I am trying to write a assertion for APB write cycle with no wait states. Here is what i have written, the assertion doesnt seem to pass at all. Can any one tell me what is wrong here?
// Code your testbench here
// or browse Examples
import uvm_pkg::*;
`include "uvm_macros.svh"
module top;
bit pclk,pwrite,psel,penable,pready;
bit [7:0] pwdata,paddr;
default clocking @(posedge pclk); endclocking
initial forever #10 pclk=!pclk;
property p1;
@(posedge pclk) $rose (pwrite && psel) |-> ($stable(paddr && pwdata)[*2]) ##1 $rose (penable && pready) ##1 $fell (pwrite && psel && penable && pready);
endproperty
assert property (p1) $display ("Assertion passed",$time);
initial begin
$dumpfile ("hello.vcd");
$dumpvars (0,top);
end
initial begin
repeat(100) begin
repeat(1) @(posedge pclk) #1;
if (!randomize(pwrite,psel,penable,pready) with
{pwrite dist {1'b1:=1,1'b0:=1};
psel dist { 1'b1:=1,1'b0:=1};
penable dist { 1'b1:=1,1'b0:=1};
pready dist { 1'b1:=1,1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error");
repeat (2) @ (posedge pclk) #1;
if (!randomize(paddr,pwdata))
`uvm_error("MYERR", "This is a randomize error");
end
$stop;
end
endmodule
In reply to rag123:
As you know, I generally use the randomize with weighted probabilities.
It is tricky to get what you need when you have complex scenarios with
stuff like [*2] and $rose and $fell of a combination of signals.
To do that I generally play with the weights, and avoid doing things like
if (!randomize(..);
repeat (2) @ (posedge pclk) #1; // <-- avoid
if (!randomize(..);
// *********
// instead, fix your constraints in one shot
if (!randomize(pwrite,psel,penable,pready) with
{pwrite dist {1'b1:=1,1'b0:=1};
psel dist { 1'b1:=1,1'b0:=1};
penable dist { 1'b1:=1,1'b0:=1};
pready dist { 1'b1:=1,1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error");
// repeat (2) @ (posedge pclk) #1;
if (!randomize(paddr,pwdata) with
{paddr dist {1'b1 :=5, 1'b0:=1}; // Play with the weights
pwdata dist {1'b1:=5, 1'b0:= 1};})
`uvm_error("MYERR", "This is a randomize error");
I played with the weights of all the variables and I got failures.
There are too many variables and conditions to get things to work by change thru randomization.
You’ll need to create directed tests, maybe with some randomization.
It’s hard to win the pick-6 lottery!
:)
Thanks Ben :) I understand there are lot of variables involved. I will write a directed testbench. Can you review the assertion i wrote and give feedback? I have attached the image.
In reply to rag123:
Spec: ARM_AMBA3_APB.pdf
You are attempting to write an assertion for a Write transfer with no wait states. However the spec states that there are two types of write transfers:
• With no wait states
• With wait states.
The assertion you wrote, though incorrect, still needs a term in the antecedent to specify that this is a no wait transfer, else it will fail if more than one state.
@(posedge pclk) no_wait_write ##0 // generated by the testbench or slave
$rose (pwrite && psel) |-> ##1 // 1
$stable(paddr && pwdata) ##0 // 2 **ERROR in construct, see next posts
$rose (penable && pready) ##1 // 3
pwrite && !psel && !penable); // 4
The figure below shows the timing. The term no_wait_write ##0 is missing in the diagram.
Thanks for the reply. Yes there are two cases one with wait state and one without wait state.
@(posedge pclk) no_wait_write ##0 // generated by the testbench or slave
$rose (pwrite && psel) |-> ##1 // 1
$stable(paddr && pwdata) ##0 // 2
$rose (penable && pready) ##1 // 3
pwrite && !psel && !penable); // 4
$stable(paddr && pwdata) // For this line
Are we not expecting the paddr and pwdata to be stable for 2 clks?
I made a mistake in $stable(paddr && pwdata) because they are vectors, and you do to want to AND the vectors and then check for stability. Should be $stable(paddr) && $stable(pwdata).
If you look at the timing, addr@T2 == addr@T3, i.e., thus stable
The $stable is tested at T3, the cycle after the rose in the antecedent.
I see 2 clocks in the stabibilty, one at the $rose (at t2) and other in the next cycle at T3.
ap: assert property(
@(posedge pclk) now_waite_write ##0
$rose (pwrite && psel) |-> ##1 // 1 $rose is at T2
$stable(paddr) && $stable(pwdata) ##0 / 2 at T3
// addr@T2 == addr@T3, i.e., thus stable
$rose (penable && pready) ##1 // 3 at $rose at T3
pwrite && !psel && !penable); // 4 at T4
First of all, I am NOT a fan of multiple sequence declarations unless each sequence is complex and serves a specific function, or if I need an endpoint.
I am also NOT a fan of multiple implication operators because of vacuity.
sq1 |=> sq2 |=> sq3
// If sq2 is not a match, the property is vacuous
Your sequence s1: sequenceA |-> sequenceB IS NOT A sequence, it is a PROPERTY. It cannot be declared in a sequence declaration
SPECS says “PSELx, also goes LOW unless the transfer is to be followed immediately by another transfer to the same peripheral”. That is not handled here.
// in ( pwrite && !psel && !penable), there is a need to
// detect another xfr to another peripheral for the !psel
// My take
ap_ahb_write_with_without_wait: assert property(
$rose (pwrite && psel) |-> !penable ##1
$rose (penable) ##0
$stable ((paddr) && $stable (pwdata)) until_with pready ##1
pwrite && !psel && !penable // !psel is questionable here
);
