Annex F

ISO 26262-5:2018、すなわち規格Part 5のAnnex Fには「4.2に従った第9節の目的を満足するという論理的根拠の例」が掲載されています。

ここで、4.2とはPart 5の一般的な要件であり第9節とはランダムハードウエア故障による安全目標侵害の評価です。つまりPart 5の第9節の要請に従ったメトリクス評価の実例が書かれています。ここでメトリクスとはランダムハードウエア故障による安全目標侵害のメトリクスであり、PMHFを指します。

もっとも第9節では第1の手法として「ランダムハードウエア故障の確率的メトリック」すなわちPMHFの要件を挙げ、第2の手法として「安全目標侵害の各原因の評価」すなわちEECを挙げていて、メトリクスはいずれかとなりますが、第2の手法には弊社は疑念があるため、第1の手法であるPMHFを採用したほうが良いと考えます。

PMHF式

出発点はAnnex Eで実施したFMEDAによるSPFM/LFMの導出の表です。この例に基づき、Annex FではPMHFの簡易評価式を次のように定めています。

$$M_\text{PMHF,est}\equiv \lambda_\text{SPF}+\lambda_\text{RF}+\lambda_\text{DPF_det}\cdot\lambda_\text{DPF_latent}\cdot T_\text{Lifetime}\tag{678.1}$$

一方、本来のPMHF式は規格において

• 1st edition、すなわちISO 26262:2011のPMHFを適用する、もしくは
• 2nd editionのパターン3, 4をゼロとみなす

のいずれかを適用します。後者を用いるとPMHFは次の図329.1において、パターン3, 4を無視する形となります。

さらに、定期検査・修理期間内で発生するDPFによるVSG確率は小さいため無視します。つまり図329.1においてパターン2も無視します。すると図329.1はパターン1のみが残るため、

$$M_\text{PMHF}\equiv \lambda_\text{IF,SPF}+\lambda_\text{IF,RF}+\frac{1}{2}\lambda_\text{IF,DPF,det}\cdot\lambda_\text{SM,DPF,lat}\cdot T_\text{Lifetime}\tag{678.2} $$ ここで、(678.1)と(678.2)のSPF/RFに関する項は同一なので、DPFに関する項のみを比較すれば、

1. $\lambda_\text{IF,DPF,det}$を$\lambda_\text{DPF_det}$とみなしている
2. $\lambda_\text{SM,DPF,lat}$を$\lambda_\text{DPF_latent}$とみなしている
3. $\frac{1}{2}$を無視している

の3つの近似を行っていることになります。それぞれを評価すれば、

1. 本来 $$ \begin{eqnarray} \lambda_\text{DPF_det}&=&\lambda_\text{(IF+SM),DPF,det}\\ &=&\lambda_\text{IF,DPF,det}+\lambda_\text{SM,DPF,det} \end{eqnarray} $$ であるが、非冗長系ではIFに比べてSMの物量は一般に小さいことから $$\lambda_\text{IF,DPF,det}\gg\lambda_\text{SM,DPF,det}$$ 従ってSMに関する項は無視可能
2. 本来 $$ \begin{eqnarray} \lambda_\text{DPF_latent}&=&\lambda_\text{(IF+SM),DPF,lat}\\ &=&\lambda_\text{IF,DPF,lat}+\lambda_\text{SM,DPF,lat} \end{eqnarray} $$ であるが、非冗長系ではIFのフォールトはLFにならないため、 $$\lambda_\text{IF,DPF,lat}=0$$ よってこの式は成立
3. 係数$\frac{1}{2}$は近似のため無視

以上より、もともとDPF項はSPF/RF項と比較して小さいことから本近似式は成立するといえます。

前のブログ 次のブログ

次に、下位モジュールにおいて、入力信号をレジスタ受けではなく、ワイヤ受けに変更します。以下に修正部分のみを示します。

Processor.bsv:

     Reg#(Bool) if_wait <- mkWire;
     Reg#(Bool) mc_wait <- mkWire;
     Reg#(Bool) ex_wait <- mkWire;
     Reg#(Bool) ma_wait <- mkWire;

この場合は上位がRegisterですが、下位はWireであるため、図677.1に示すようにwait信号は遅れません。上位で変化したサイクルでそのまま下位に伝わります。

前稿でも同様ですが、上位ではサイクル毎に下位にwait信号を伝えるルールを記述しています。

Tb.bsv:

    rule load_wait_values;
        proc.if_wait_load(if_wait);
        proc.mc_wait_load(mc_wait);
        proc.ex_wait_load(ex_wait);
        proc.ma_wait_load(ma_wait);
    endrule

前のブログ 次のブログ

モジュール内でデータを受け取るにはRegisterを設置する方法とWireを設置する方法があります。パイプラインプロセッサのwait信号を例にして、2つの違いを見てみます。

まず、Test-benchにおいてRegisterを設置するのは共通とします。例えば、

Tb.bsv:

import StmtFSM::*;
import Processor::*;

(* synthesize *)
module mkTb();
    Processor_ifc proc <- mkProcessor();
    Reg#(Bool) if_wait <- mkReg(True);
    Reg#(Bool) mc_wait <- mkReg(True);
    Reg#(Bool) ex_wait <- mkReg(True);
    Reg#(Bool) ma_wait <- mkReg(True);

    rule load_wait_values;
        proc.if_wait_load(if_wait);
        proc.mc_wait_load(mc_wait);
        proc.ex_wait_load(ex_wait);
        proc.ma_wait_load(ma_wait);
    endrule

    Stmt main = seq
        action
            if_wait <= False;
            mc_wait <= False;
            ex_wait <= False;
            ma_wait <= False;
        endaction
        delay(4);
        if_wait <= True;
        delay(0);
        if_wait <= False;
        delay(4);

(中略)

        $finish;
    endseq;
    mkAutoFSM(main);

endmodule

であり、下位のモジュールが、

Processor.bsv:

import FIFO::*;

interface Processor_ifc;
    (* prefix="" *)
    method Action if_wait_load(Bool in_if_wait);
    method Action mc_wait_load(Bool in_mc_wait);
    method Action ex_wait_load(Bool in_ex_wait);
    method Action ma_wait_load(Bool in_ma_wait);
endinterface

(* synthesize, always_ready *)
module mkProcessor(Processor_ifc);

    Reg#(int) pc <- mkReg(0);
    FIFO#(Maybe#(int)) ifs <- mkLFIFO;
    FIFO#(Maybe#(int)) ids <- mkLFIFO;
    FIFO#(Maybe#(int)) exs <- mkLFIFO;
    FIFO#(Maybe#(int)) mas <- mkLFIFO;
    FIFO#(Maybe#(int)) wbs <- mkLFIFO;
    Reg#(Bool) if_wait <- mkReg(False);
    Reg#(Bool) mc_wait <- mkReg(False);
    Reg#(Bool) ex_wait <- mkReg(False);
    Reg#(Bool) ma_wait <- mkReg(False);

    // <PC>
    rule pc_stage;
        if (pc > 100) $finish(0);
        $display("------");
        ifs.enq(tagged Valid pc);
        pc <= pc + 4;
    endrule

    // <IF>
    rule if_stage;
        let pc_if = ifs.first;
        if (!if_wait) begin
            ifs.deq;
            $display (" pc_if = %04h", pc_if);
            ids.enq (pc_if);
        end else begin
            ids.enq (tagged Invalid);
        end
    endrule

    // <ID>
    rule id_stage;
        let pc_id = ids.first;
        if (!mc_wait) begin
            ids.deq;
            $display (" pc_id = %04h", pc_id);
            exs.enq (pc_id);
        end else begin
            exs.enq (tagged Invalid);
        end
    endrule

    // <EX>
    rule ex_stage;
        let pc_ex = exs.first;
        if (!ex_wait) begin
            exs.deq;
            $display (" pc_ex = %04h", pc_ex);
            mas.enq (pc_ex);
        end else begin
            mas.enq (tagged Invalid);
        end
    endrule

    // <MA>
    rule ma_stage;
        let pc_ma = mas.first;
        if (!ma_wait) begin
            mas.deq;
            $display (" pc_ma = %04h", pc_ma);
            wbs.enq (pc_ma);
        end else begin
            wbs.enq (tagged Invalid);
        end
    endrule

    // <WB>
    rule wb_stage;
        let pc_wb = wbs.first;
        wbs.deq;
        $display (" pc_wb = %04h", pc_wb);
    endrule

    method Action if_wait_load(Bool in_if_wait);
        if_wait <= in_if_wait;
    endmethod
    method Action mc_wait_load(Bool in_mc_wait);
        mc_wait <= in_mc_wait;
    endmethod
    method Action ex_wait_load(Bool in_ex_wait);
        ex_wait <= in_ex_wait;
    endmethod
    method Action ma_wait_load(Bool in_ma_wait);
        ma_wait <= in_ma_wait;
    endmethod

endmodule: mkProcessor

この場合は上位がレジスタであり、下位もレジスタであるため、信号の伝播が1サイクル遅れます。

前のブログ 次のブログ

さらに前稿でインスタンスされるパイプラインFIFOであるFIFOL1のverilogライブラリのコードを見てみます。

assign FULL_N = !empty_reg || DEQ;
assign EMPTY_N = empty_reg ;

パイプラインFIFOは1段のF/Fなので、基本的にFULLとEMPTYは内部レジスタempty_regの背反ロジックとなりますが、例外的に下流からのDEQ要求がある場合は、仮にFULLであったとしても次のサイクルでFULLが解消されるため、DEQとのORをとり、not full(上位へのenq enable)とします。

always@(posedge CLK `BSV_ARESET_EDGE_META)
  begin
     if (RST == `BSV_RESET_VALUE)
        begin
          empty_reg <= `BSV_ASSIGNMENT_DELAY 1'b0;
        end
     else
        begin
           if (CLR)
             begin
                empty_reg <= `BSV_ASSIGNMENT_DELAY 1'b0;
             end
           else if (ENQ)
             begin
                empty_reg <= `BSV_ASSIGNMENT_DELAY 1'b1;
             end
           else if (DEQ)
             begin
                empty_reg <= `BSV_ASSIGNMENT_DELAY 1'b0;
              end // if (DEQ)
        end // else: !if(RST == `BSV_RESET_VALUE)
 end // always@ (posedge CLK or `BSV_RESET_EDGE RST)

empty_regはnot emptyを表す内部レジスタであり、ENQするとTrue(=1, not empty)となり、DEQするとFalse(=0, empty)となります。not fullは上位へのenq enable信号であり、not emptyは下位へのdeq enable信号です。当初なぜemptyもfullも負論理なのかと思いましたが、そういうことでした。

always@(posedge CLK `BSV_ARESET_EDGE_HEAD)
  begin
       begin
           if (ENQ)
             D_OUT     <= `BSV_ASSIGNMENT_DELAY D_IN;
        end // else: !if(RST == `BSV_RESET_VALUE)
  end // always@ (posedge CLK or `BSV_RESET_EDGE RST)

ENQはF/F入力の値を出力に移します。一方DEQはF/Fは何も変化させません。

これまで見たように、bscにより生成された回路を解析することは、論理設計能力の向上の一助となります。

前のブログ 次のブログ

Maybeを使用した制御パイプラインをbscで合成し、生成されたverilogコードの一部を示します。

  // submodule ifs                                                                                                                        
  assign ifs$D_IN = { 1'd1, pc } ;
  assign ifs$ENQ = ifs$FULL_N ;
  assign ifs$DEQ = WILL_FIRE_RL_if_stage && !if_wait ;
  assign ifs$CLR = 1'b0 ;

  // rule RL_if_stage                                                                                                                     
  assign WILL_FIRE_RL_if_stage = ids$FULL_N && ifs$EMPTY_N ;

  // submodule ids                                                                                                                        
  assign ids$D_IN = { !if_wait && ifs$D_OUT[32], ifs$D_OUT[31:0] } ;
  assign ids$ENQ = WILL_FIRE_RL_if_stage ;
  assign ids$DEQ = WILL_FIRE_RL_id_stage  && !mc_wait ;
  assign ids$CLR = 1'b0 ;

  // rule RL_id_stage                                                                                                                     
  assign WILL_FIRE_RL_id_stage = exs$FULL_N && ids$EMPTY_N ;

図674.2はこのコードを回路図に変換したものです。ハードウエア設計者はHDLコードよりもstaticな回路図のほうが理解し易いです。

各ステージ中のwait信号で上流方向は止めますが(中段左側のAND)、下流方向は止めずに(下段のAND)さらに下流にinvalidを流す(上段のAND)ところが、より単純な図673.1のデータパイプラインとの違いです。

前のブログ 次のブログ

前回まではパイプラインのうち<IF>にwaitを入力しましたが、基本的に<WB>以外のステージにwaitが入る可能性があります。

図673.1に各種wait信号を入力したデータパイプライン構造を示します。過去記事で調べた回路にwaitが追加されています。

図では信号名を3文字に短縮していますが、$\overline{\text{emp}}$は$\overline{\text{empty}}$の略でdeqのenable信号、$\overline{\text{ful}}$は$\overline{\text{full}}$の略で、enqのenable信号です。

前のブログ 次のブログ

今回設計したFIFOは2段FIFOでした。従って、1つ前の記事のようにif_waitを2サイクルにすると、図672.1で示すとおり0034, 0038とPCが先に進みます。

このようにパイプラインが次に進んでしまうということは、演算器等も2段分必要になります。従ってFIFOを1段に修正します。具体的にはmkFIFOをmkLFIFOに変更します。

以下に修正箇所を示します。

Processor.bsv

FIFO#(int) ifs    <- mkLFIFO;
FIFO#(int) ids    <- mkLFIFO;
FIFO#(int) exs    <- mkLFIFO;
FIFO#(int) mas    <- mkLFIFO;
FIFO#(int) wbs    <- mkLFIFO;

以下はbsimシミュレーション波形です。図672.1ではif_waitによりPCが止まらずwait中に0038までも進んでしまいましたが、1段FIFO(パイプラインFIFO)に変更することで、if_waitが0030で入力されるとPCはその次のアドレスである0034で正しく止まっています。

図672.1, 図672.2共、Gtkwaveではtagのinvalidを自動認識しないため、パイプラインバブルのサイクルを手で赤で塗っています。

前のブログ 次のブログ