Home > Community > Forums > Functional Verification > modeling a constraint for a signal that is only high once (ever)

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

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

Last post Wed, Nov 15 2006 12:47 PM by archive. 5 replies.
Started by archive 15 Nov 2006 12:47 PM. Topic has 5 replies and 1479 views
Page 1 of 1 (6 items)
Sort Posts:
  • Wed, Nov 15 2006 12:47 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    modeling a constraint for a signal that is only high once (ever) Reply

       
    How can I model a constraint for a signal that is supposed to be high only once
    in PSL?


    Originally posted in cdnusers.org by ssa
    • Post Points: 0
  • Wed, Nov 15 2006 1:37 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: modeling a constraint for a signal that is only high once (ever) Reply

    What about:

    // psl assume_single_high_pulse: assume {!a[*];[a];!a[*]};


    Originally posted in cdnusers.org by jb
    • Post Points: 0
  • Wed, Nov 15 2006 2:54 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: modeling a constraint for a signal that is only high once (ever) Reply


    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?


    Originally posted in cdnusers.org by ssa
    • Post Points: 0
  • Wed, Nov 15 2006 3:23 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: modeling a constraint for a signal that is only high once (ever) Reply

    You need another constraint:

    // psl assume_no_second_pulse : assume never {a; !a[*]; a};


    Originally posted in cdnusers.org by foster
    • Post Points: 0
  • Wed, Nov 15 2006 4:57 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: modeling a constraint for a signal that is only high once (ever) Reply

    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.


    Originally posted in cdnusers.org by TAM
    • Post Points: 0
  • Wed, Nov 15 2006 5:17 PM

    • archive
    • Top 75 Contributor
    • Joined on Fri, Jul 4 2008
    • Posts 88
    • Points 4,930
    RE: modeling a constraint for a signal that is only high once (ever) Reply


    Thanks guys - both never version work great.

    I found another alternative: never {a[=2]};


    Originally posted in cdnusers.org by ssa
    • Post Points: 0
Page 1 of 1 (6 items)
Sort Posts:
Started by archive at 15 Nov 2006 12:47 PM. Topic has 5 replies.