How can I model a constraint for a signal that is supposed to be high only oncein PSL?
What about:// psl assume_single_high_pulse: assume {!a[*];[a];!a[*]};
Thanks jb.Tried it but it seems not to work.I can get two times a - even consecutively with this constraint applied.Might be due to to the last term in the sequence !a[*] - where !a[*0] (meta code) is a legal match.Any other suggestions?
You need another constraint:// psl assume_no_second_pulse : assume never {a; !a[*]; a};
The following single constrtaint seems to work:// psl no2a: assume never { a[->2] };It doesn't say that 'a' has to occur once, it only says that it can't occur twice.
Thanks guys - both never version work great.I found another alternative: never {a[=2]};