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)

Sender definition

module sender_module( RST, BtoS_ACK )( StoB_REQ, DI(0..31) )
{
  var StoB_REQ  : boolean;
  var DI(0..1) : boolean;

  assign
    init(StoB_REQ) := 0;
    next(StoB_REQ) := case
        RST        : 0;
        !StoB_REQ &
            !BtoS_ACK : {0,1}; /* If not asserted
                                        and not at the end
                                        of a transaction,
                                        then a request can
                                        be made */

        StoB_REQ & BtoS_ACK             : 0;          /* If asserted
                                                         and acknowledged
                                                         deassert */
        else       : StoB_REQ;
    esac;

/* Note : We use only two bits of the data bus to symbolize data,
          while the rest of the bits will be fixed to 0.
          This is a technique designed to "save variables" and avoid explosion. */

  assign
    init(DI(0..1)) := 0;
    next(DI(0..1)) := case
        RST                 : 0;
        rose(StoB_REQ)      : nondets(2); /* We assert (non deterministic)
                                             data one cycle after the
                                             request */
        StoB_REQ & BtoS_ACK : 0;          /* If buffer acknowledged our
                                             request then invalidate
                                             the data */
        else           : DI(0..1);
    esac;

    define DI(2..31) := 0;
}

%for i in 0..3 do
    instance sender_%{i} : sender_module( RST, BtoS_ACK( %{i} ))
                                        ( StoB_REQ( %{i} ), DI(%{i}*32..%{i+1}*32-1));
%end




 
 





    About IBMPrivacyContact