modeling a constraint for a signal that is only high once (ever)

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]};