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)

Receiver definition

module receiver_module( RST, BtoR_REQ, DO(0..31) )( RtoB_ACK )

  var RtoB_ACK : boolean;

/*  The usual way we would approach writing the environment
    would be along the lines of:

    next(RtoB_ACK) := case
        RST            : 0;
        BtoR_REQ       : 1;
        !BtoR_REQ      : 0;
        else           : RtoB_ACK;

    (Specifying when a signal changes.)
    However, notice that here we never get to the "else"
    case. In fact, we can write a simpler environment:

    init(RtoB_ACK) := 0;
    next(RtoB_ACK) := case
        RST  : 0;
        else : BtoR_REQ; /* RtoB_ACK must be asserted a cycle after
                            the assertion of BtoR_REQ and deasserted
                            a cycle after the deassertion of BtoR_REQ.
                            This unusually simple specification was
                            made to keep this tutorial simple. */


%for i in 0..1 do
    instance receiver_%{i} : receiver_module( RST, BtoR_REQ(%{i}), DO(0..31) )
                                            ( RtoB_ACK( %{i}) );


    About IBMPrivacyContact