VERY Tough Assertion Question (Hard)

SystemVerilog
1

We need to check when a=1 ,suppose at 3 ns we should start checking and if falls at 15 ns we should continue checking.
step 2 : once a is high start checking for either b or c is high during a remains high
step 3 : if they found even single or many times that b or c is high , assertion should show success only once. and that too at the fell of a.(15ns

step 4: if c or b is newer high during that period ,only one fail will be reported no multiple threads required , one fail will be reported at fell of a.(15ns
.
note : I have tried intersect, within not working I mean we need only one thread .as requirement

2

In reply to bhajanpreetsinght:

It is very tough to understand your question. It would really help to show a minimal, compete reproducible example. Specifically, show us an example of a stimulus that passes and fails your requirements.

3

In reply to bhajanpreetsinght:

first try snap
Google Photos

4

In reply to bhajanpreetsinght:

It would really help to show a minimal, compete reproducible example. Specifically, show us an example of a stimulus that passes and fails your requirements. Not a picture of it.

5

In reply to bhajanpreetsinght:

property p2;
@(posedge Clk) disable iff( (reset==0))
(a) |-> lock3 within (a==1);
endproperty
P2: assert property(p2)
else begin
uvm_pkg::uvm_report_error(“assertions”, "Error on assertion " );
end

6

In reply to dave_59:

In reply to bhajanpreetsinght:
It would really help to show a minimal, compete reproducible example. Specifically, show us an example of a stimulus that passes and fails your requirements. Not a picture of it.

I showed the simulation snap, where it show passes and fails please see the image

7

In reply to bhajanpreetsinght:

In reply to dave_59:
I showed the simulation snap, where it show passes and fails please see the image

Hi Dave,

Please nswer I gave all scenarios
code is below
property p2;
@(posedge Clk) disable iff( (reset==0))
(a) |-> lock3 within (a==1);
endproperty
P2: assert property(p2)
else begin
uvm_pkg::uvm_report_error(“assertions”, "Error on assertion " );
end

where lock3 is logic lock3;
always@(posedge clk)
begin
if (A==0| reset==0)
lock3<=0;
else
lock3<=(b|c);
end

expectation is if a is higha t 7 ns to 15ns, bis high at 9 ns and c is not high ,as we want to check during a is high which is from 15 ns-7 ns=8ns and be is high just after two clock edge of a and falls in between when a is high, it should show pass at 15 ns

similarly if neither b or c are high in between 7 to 15 ns ,i t should throw false at 15 ns

note b or c can toggle as many times in between a going high and reamin high we are only concerned with one toggle

Hope it clears now

8

In reply to dave_59:

Hi Dave,

consider this

signal a

/,/
t=7ns t=15ns

signal b
…/…/…
t=12ns
consider them as high edge

signalc
…

result would be pass

/…/
∆
pass at 15 ns

fail condition

signal a
…/ /…

signal b
…

signal c
…

as not once b or c is high when a is high it should show fails at 15 ns

9

Hi Dave,

suppose
consider this clk
which has 1ns =timeperiod

a signal
7=ns 15ns
…|````````````````````````````````|…

signal b

…||....||…

signal c

…

here b toggles in duration when a is high ,assertion should show pass at 7ns ,if we write ancedent as $rose(a) or it wrote $fell(a) it show passs at 15ns.

scenario 2(fail)

a signal
7=ns 15ns
…|````````````````````````````````|…

signal b

…

signal c

…

this is only scenario to fail, when both b or c remains low throughout the duration

it will show fail as explained above at 7ns or 15ns

a signal
7=ns 15ns
…|````````````````````````````````|…

signal b

…

signal c

…|```````|…

here c toggles it will show pass similarly like first case

I need help to get the assertion to trigger only thread of pass or fail, in my case it triggeres at every posedge of clk

property p2;
@(posedge Clk) disable iff( (reset==0))
(a) |-> (b|c) within (a==1);
endproperty
P2: assert property(p2)
else begin
uvm_pkg::uvm_report_error(“assertions”, "Error on assertion " );
end

so the result is as follows

a signal
7=ns 15ns
…|````````````````````````````````|…

signal b

…

signal c

…|```````|…
. .
. .
. .
. .
result
7=ns . ^ ^ ^ . 15ns
…|````````````````````````````````|…
8ns 9ns 11ns 12ns 13ns

so ^ represents pass at 9ns,10ns,11ns at c is high
but at 8ns,12ns,13ns,14ns it is low which is false condition so it triggere assertion false

but the requirement whether true or false we need only thread throughout checking?

10

In reply to bhajanpreetsinght:


bit start_a = 0 ;
automatic function void check_a(bit set_val);
  start_a= set_val ;
endfunction 

property check_b_or_c ;
@(posedge clk)
(a,start_a==0,check_a(a)) |-> (b|c)[->1] ##1 (!b & !c)[*0:$] intersect a[*0:$] ##1 $fell(a);
endproperty