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)

Writing environment

First, we have to define the clock and the reset signal within the default environment. For additional clock modeling considerations, refer to the user manual.
vmode default {

define CLK := 1 ;

var RST : boolean ;
init(RST) := 1 ;
next(RST) := 0 ;
Next, we need to define the senders and the receivers. First, we define the receivers (as they are easier). Remember that you have to create two instantiations of receivers.

Instructions for writing the receiver module
The definition of the next state of the RtoB_ACK signal appears in the receiver module.
The receiver module input is the output data from buffer - D0 (32 bits) and the BtoR_REQ and RST signals. The output from the receiver module is the acknowledgment signal, with value according to the state of BtoR_REQ.
Our definition can be found here..

Instructions for writing the sender module
Next, try to define the sender module. Remember that you need to create four instantiations of the sender module.
The definition of the next state of the StoB_REQ signal appears in the sender module. The sender module input is the state of the BtoS_ACK and RST signals. The output from the sender module includes the input data - DI (32 bits) to the buffer, as well as the StoB_REQ state value.

Terms for defining the next state of StoB_REQ
  • If StoB_REQ is not asserted and there is no end of transaction, then a request can be made (the state can either be asserted or not)
  • If StoB_REQ is asserted, and the sender receives an acknowledgment to pass the data, then the signal must deassert (disallow a send request)
  • In any other situation, the signal should remain in the same state.

In addition, the sender module must determine the values of the data input bits and their validity. It is advisable to set most of the data input bits to a constant, since this helps to reduce the model, hence avoiding an explosion, without harming the basic logic.

In our definition of the senders, we set all but two input bit values to 0. This restricted model is enough to check the control properties of the design. Of course, the data path verification is not exhaustive. While RuleBase/PE is well-suited for control logic verification, it is not well-suited for data paths.

Terms for defining the next state of DI(0..31):
  • As noted in the specification, after the sender sends a request, it puts the data on its data bus. Then, if the request signal was raised from a non-set state (value 0) to a set state (value 1), the sender can prepare the data by setting the non-deterministic bits (the two bits that were mentioned in the previous section).
  • In a situation where a request (StoB_REQ asserted) was submitted and an acknowledgment was received for this request (BtoS_ACK asserted), the data bus will not be valid. Therefore, we need to un-set the DI (32 bits), thus setting it to an invalid state.

Our definition of the senders module can be found here.

In an ordinary verification project, that would have completed our environment description, and we would have gone off to write rules. However, in this tutorial, we add to the envs file the lines:
define ERROR_FOUND(1) :=0 ;
define ERROR_FOUND(2) :=0 ;
define ERROR_FOUND(3) :=0 ;
define ERROR_FOUND(4) :=0 ;
define ERROR_FOUND(5) :=0 ;
define ERROR_FOUND(6) :=0 ;
ERROR_FOUND(1..6) is a boolean array, which is used in the design, and helps in masking existing design bugs during the learning phase.

Each time you have identified an error, say error k, you can fix it by setting ERROR_FOUND(k) to 1.

Our "school solution" for the envs file can be found here.


    About IBMPrivacyContact