psl assertion for dynamically created signal length

[David Belohrad]

Dear All,

I'd like to produce following like PSL construct:

psl assert always {StartPulsexS} |=> {PulsexS[*25]; not PulsexS};

However, the PulsexS duration is not given as constant, but its length
is setup by master entity. So ideally I'd like to have something like:

psl assert always {StartPulsexS} |=> {PulsexS[*PulseLengthxD]; not PulsexS};

where PulseLengthxD is a type of either
std_logic_vector/unsigned/integer... but apparently nothing like this
works in mentor modelsim....

How to write such constraint?

thanks

d.

 

[HT-Lab]

Dear All,

I'd like to produce following like PSL construct:

psl assert always {StartPulsexS} |=> {PulsexS[*25]; not PulsexS};

However, the PulsexS duration is not given as constant, but its length
is setup by master entity. So ideally I'd like to have something like:

psl assert always {StartPulsexS} |=> {PulsexS[*PulseLengthxD]; not PulsexS};

where PulseLengthxD is a type of either
std_logic_vector/unsigned/integer... but apparently nothing like this
works in mentor modelsim....

How to write such constraint?

thanks

d.

I believe that PSL ranges must be static (resolved during
compile/elaboration), thus PulseLengthxD must be a constant. Search the
PSL reference manual for "Range"

Can you run multiple tests? In that case you can make PulseLengthxD a
top level generic and invoke Modelsim with vsim -GPulseLengthxD=xx


Hans
www.ht-lab.com