In reply to ben@SystemVerilog.us:
Hi,
I try to figure out the process from “ap_equivalent_to_ap_never_succeed”
to “every thread must succeed to succeed the assertion” ?
ap_never_succeed: assert property(
(rose(a) ##[2:] b) |=> c);
The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
My understanding of “all thread must succeed to succeed the assertion”
looks like below, there are “and” between them
//my understanding
ap_equivalent_to_ap_never_succeed_mod: assert property(
($rose(a) ##2 b) and
($rose(a) ##3 b) and
…
($rose(a) ##n b)|=> c); // where n is infinity
and the original “ap_equivalent_to_ap_never_succeed”
should be “one of threads succeed will succeed the assertion”
In my understanding,
“##[2:$]” means “between cycle-2 and cycle-infinity, there should be at least one…”
Could anyone tells me where my misunderstandings are?
Regards
SC