Skip to main content
    Israel [change]    Terms of use
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

RuleBase Parallel Edition

Formal Verification

Generalized Buffer (PSL/Sugar version)


To start writing rules, it is best to start with simple ones that check basic properties of our model. Here's an example:

Let's make sure that a request eventually gets acknowledged. We will write two rules, one for the sender and one for the receiver. First, write a verification unit for the sender.

Verification unit: sender_req_get_ack

We still have to write a verification unit to ensure that every request from GenBuf to one of the receivers is followed by an acknowledgement from the receiver.

Note that the specification designed for this course was unreasonably restrictive (e.g., the demand that a receiver will respond within one cycle of the request). The specification was formulated that way in order to keep this tutorial simple. However, a real-life specification would probably demand only that the receiver eventualy respond. In such a case, one should write a receiver module that models "delayed acknowledgements." The correct way to write such modules involves fairness statements. Since fairness statements are dangerous tools for an inexperienced user to use, this tutorial does not use them.

Verification unit: genbuf_req_get_ack

In the same way that every request should eventually be acknowledged, there should not be an acknowledgement without a corresponding request. We can express this property with the following verification unit:

Verification unit: no_ack_without_a_req

Let's check some properties about the receivers' acknowledgement. We will write a verification unit with several assertions to check that:
  1. The GenBuf request will be deasserted one cycle after the receiver's acknowledgement, and will not be reasserted until the end of the transaction. (Recall that GenBuf is not allowed to initiate a new transaction until a cycle after the receiver deasserts its acknowledgment.)
  2. GenBuf does not request both receivers at the same time.
  3. GenBuf will not make two consecutive requests to the same receiver.
  4. GenBuf deasserts BtoR_REQ in the cycle that it puts the data on bus.

(you might find it useful to define B2R_REQ := BtoR_REQ(0) | BtoR_REQ(1))
Verification unit: receiver_ack

We have written some rules. However, we would like to check some "higher-level" properties of the design. The following is a list of the properties we would like to check:
  1. GenBuf obeys the four-phase handshaking with the senders. Specifically, we would like to check that:
    1. GenBuf eventually responds to a sender request. (We already verified that in sender_req_get_ack.)
    2. GenBuf does not acknowledge unless requested. (We already verified that in no_ack_without_req.)
    3. In case the sender deasserts its request, GenBuf will eventually deassert its acknowledgement.
    4. GenBuf will not deassert its acknowledgement unless the sender first deasserts its request (even one that was verified).
    We are left to verify properties III and IV.

    Verification unit: genbuf_to_sender_handshake

  2. Only one sender can send data at any given time.

    Verification unit: only_one_sender_at_a_time

  3. Only one receiver can read data at any given time.

    Verification unit: only_one_receiver_at_a_time

  4. GenBuf does not receive when the queue is full. (Recall that the depth of GenBuf is 4). Note this can (and should) be done without looking at the implementation of the GenBuf.

    Verification unit: genbuf_does_not_receive_when_queue_full

  5. Genbuf does not send when the queue is empty.

    Verification unit: genbuf_does_not_send_when_queue_empty

  6. Every data word read by GenBuf will be eventually sent out to a receiver. This should be a liveness formula, which means that sometime in the future the data will be written.
    Only the Discovery & SmartLoc engines can handle this kind of vunits.

    Verification unit: data_read_is_eventually_written

  7. Data are kept in order.

    Verification unit: genbuf_keeps_fifo_order

  8. All data received by the receivers has previously been sent by the sender (i.e., the queue is not sending invalid data to the receiver).

    Hint: To avoid state explosion, we may try to fix the data.

    Verification unit: genbuf_is_not_creative


    About IBMPrivacyContact