IBM®
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:

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

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

*/
  assign
    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. */

   esac;
}

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




 
 





    About IBMPrivacyContact