Hi SVA Experts,
I have few requirements wherein I need the register information inside my assertion to take necessary decisions.
An 8 bit Register decides the duration of the signal high duration.
Let’s say Register RegX[7:0] bit field [2:0] decide the High duration of Signal A(Programmable).
000 → 25uS, …,111 → 200uS
A …(Signal LOW)…|<---------RegX[2:0]----(Signal HIGH)---------------------------------------------------->|…(Signal LOW)…
B …|…4-Clk/8-Clk delay…<----Signal HIGH for 4-Clk/8-Clk—>…>|…
Signal-A is High for the duration set by RegisterX value [2:0]
Signal-B is Low from Signal A going HIGH for 4/8-Clk, then a HIGH Pulse for 4/8-Clks and then Low again till the duration of Signal A High.
The 4/8-Clk delay is also a setting from the Register RegX bit field [3].
In reply to ben@SystemVerilog.us:
Thanks Ben to point to the link with an example.
Could you please explain it in a very simple way as I did not find any comments explaining the intent.
I also did not get how the design register gets mapped here as there is no hierarchy reference that the user needs to add to it.
I also tried running the same in EDA-Playground, but loop count 1000,1500 combinations are too high to execute them.
In reply to ben@SystemVerilog.us:
Could you please explain it in a very simple way as I did not find any comments explaining the intent.
Mot sure I understand your question. If, instead of dynamic ranges based on the value of a variable, you have a fixed static delay (e.g., 3) then
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
q_dynamic_repeat(a, duration) ##1 $fell(a));
// is equivalent to
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
a[*3] ##1 $fell(a));
// If you want to understand how the sequence q_dynamic_repeat(a, duration) works,
// you'll have to dig into the package and see its implementation.
I also did not get how the design register gets mapped here as there is no hierarchy reference that the user needs to add to it.
I also tried running the same in EDA-Playground, but loop count 1000,1500 combinations are too high to execute them.
I don’t understand your question design register gets mapped here as there is no hierarchy reference??
provide the link to the edaplayground
You’ll need to rephrase your requirements in English and ask what are you looking for, an assertion> a design question? I had to guess as to your intent.
In reply to raviji:
Mot sure I understand your question. If, instead of dynamic ranges based on the value of a variable, you have a fixed static delay (e.g., 3) then
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
q_dynamic_repeat(a, duration) ##1 $fell(a));
// is equivalent to
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
a[*3] ##1 $fell(a));
// If you want to understand how the sequence q_dynamic_repeat(a, duration) works,
// you'll have to dig into the package and see its implementation.
I don’t understand your question design register gets mapped here as there is no hierarchy reference??
provide the link to the edaplayground
You’ll need to rephrase your requirements in English and ask what are you looking for, an assertion> a design question? I had to guess as to your intent.
In a single run of testcase, the value programmed from into the register X[7:0] is going to be fixed throughout, so ultimately the duration [2:0] shall also be fixed.
clk, a and b are part of interface to which the assertion shall be binded, but not the register bits, so how do those get mapped here to duration?
module top;
import sva_delay_repeat_range_pkg::*;
logic[7:0] x;
let duration = x[2:0]; // This is local to assertion usage, how does it map to the design register bits.
bit clk, a, b;
initial forever #10 clk=!clk;
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
q_dynamic_repeat(a, duration) ##1 $fell(a));
endmodule
The below one if implemeted has to be working for all 8 combinations a[*0] to a[*7] based on the register X [2:0] programming.
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
a[*3] ##1 $fell(a));
EDA Playground was to run the link example provided.
My package uses sequences with arguments to enable the use of dynamic values from a variable
[SystemVerilog]
ap_a_sig: assert property(@ (posedge clk) $rose(a) |->
q_dynamic_repeat(a, duration) ##1 $fell(a));
// If you want to understand how the sequence q_dynamic_repeat(a, duration) works,
// you’ll have to dig into the package and see its implementation.
- Another approach is to use the **generate**. From my SVA book, I provide the following example:
``` verilog
generate for (genvar i=0; i<=15; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1'b1, v=0, v[i+1]=1'b1) ##0 req < v |->
grnt[i]==1'b1 ##0 $onehot(grnt);
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
ap_zero_req0: assert property(@(posedge clk) req==0 |-> grnt==0);
the Edit code - EDA Playground is just my package and a testbench for the package. You need to create your own tb for your model. That tb will provide different values for the variable “x” with “duration” being a field of “x”.
The above 2 points provide variations in applying dynamic ranges for SVA; 1) the use of a package, 2) the use of the generate statement (here the a[*3] is replaced with a[i].