%
% Implemenatation and Proof of a Next PC environment
% as given in [MP00]
%
% The PVS proof is copyright (C) 2000-2001 Daniel Kroening
%

nextpc_impl: THEORY
BEGIN

  dlxif: LIBRARY = "../dlxif";
  IMPORTING dlxif@nextpc_spec, dlxtombasics;

  bjtaken_imp(Iw: registert, Adata: registert):bool=
    I_j(Iw) OR I_jr(Iw) OR
    (I_branch(Iw) AND (I_branch_eq(Iw)=zerotester_impl[32](Adata)));

  bjtaken_imp_correct: LEMMA
    FORALL (Iw, Adata: registert):
    bjtaken_imp(Iw, Adata)=dlxspec_bjtaken(Iw, Adata);

  nextpc_imp(Iw: registert, Adata: registert,
             oldPC: registert): registert =
    IF I_jr(Iw) THEN
      Adata
    ELSE
      adder_2op_impl[32](oldPC,
        IF bjtaken_imp(Iw, Adata) THEN
          I_immediate(Iw)
        ELSE
          r4
        ENDIF)
    ENDIF;

  nextpc_imp_correct: LEMMA
    FORALL (Iw, Adata, oldPC: registert):
    nextpc_imp(Iw, Adata, oldPC)=dlxspec_nextpc(Iw, Adata, oldPC);

  nextpci_imp(Iw: registert, Adata: registert,
              oldPC: registert, EPC: registert): registert =
    IF I_rfe(Iw) THEN
      EPC
    ELSE
      nextpc_imp(Iw, Adata, oldPC)
    ENDIF;

  nextpci_imp_correct: LEMMA
    FORALL (Iw, Adata, oldPC, EPC: registert):
    nextpci_imp(Iw, Adata, oldPC, EPC)=dlxispec_nextpc(Iw, Adata, oldPC, EPC);

END nextpc_impl