フォーマル検証を機能安全の検証に使うべき3つの理由

機能安全という概念が、ここ最近急激にホットになってきています。この概念自体は昔からあったのですが、車載電子機器に対する機能安全の標準であるISO26262が2011年に制定されてから、この標準を満たすことがヨーロッパでの自動車販売の条件になるという観測により、日本の自動車業界でも盛り上がってきています。
機能安全とは、一言で言ってしまうと、製品の安全性を、品質や信頼性だけに頼らずに、セーフティーメカニズム(SMと略称されます)と呼ばれる安全機構を付加することで達成しようと言う考え方です。いわば追加システムによるリスク管理とも言えるものです。この考え方は、元々は化学プラントや発電所などの電子機器を対象としたIEC 61508で提唱され、使い方によっては人命を左右する製品である航空機や医療機器、鉄道、製造装置(また、先に述べた自動車)でそれぞれ派生規格(自動車の場合がISO26262)が定められています。

機能安全で対応すべき不具合の要因は、バグや仕様漏れに代表されるSystematic Issueといわゆる故障のイメージに近いRandom Issueの二種類に分類されます。ケイデンスはそれぞれに対応するソリューションをご提供しています。Systematic Issueに対しては、The Sound of CadenceのJUNE2014(vol.13)号の記事「機能安全におけるトレーサビリティー:要求トレーサビリティーと検証トレーサビリティー」で述べたIncisive vManagerによるトレーサビリティー確保が、Random Issueに対してはThe Sound of CadenceのDEC2014(vol.15)号の記事「機能安全検証の新ソリューション Incisive Functional Safety Simulator」で述べたIncisive Functional Safety Simulator(IFSS)による故障の影響解析がソリューションとなります。

図1:故障影響解析の基本的考え方図1:故障影響解析の基本的考え方

故障の影響解析を行う場合、IFSSでは故障のない回路(これは、影響解析したい回路記述そのものです)と、同じ回路に任意の故障を注入した回路の双方に対して同じテストパタンを与え、その出力を比較してその差分を故障の影響とみなします。図1にその例を示します。この図ではModuleが実現したい機能の実装部分であり、CheckerがSMとしてModule部分の故障の検出を行います。故障が実際の出力=機能に影響を与えるか否かはF-O(Function Out)を比較すれば分かります。また、故障が検出できるか否かはC-O(Checker Out)を見ればわかります。ここで賢明な読者の方であれば「二つの回路の動作の比較を行うのであれば、フォーマル検証を使うのもよいのではないか」とおっしゃるかもしれません。はい、その通りです。Jasper Goldのアプリケーションの一つにSEC(Sequential Equivalence Checking)という名前のアプリケーションがあります。故障の影響解析をフォーマル検証で行う場合、以下の3つのメリットがあります。

1.フォーマル検証は故障影響解析の確実性を向上する。

二つの回路の挙動に差が出ることを証明するためには、差が出るテストパタンを一つ提示すればよいのですが、差が出ないことの証明には、全てのテストパタンで差が出ないことを示さねばなりません。すなわち、「差が出ない」という結果が出た場合、本当に差が出ないのか、それともテストパタンが足りなくて差が出るパタンがたまたま与えられなかったのか、その判別は結構重い仕事です。ですが、フォーマル検証の網羅性の特性を使えば、テストパタンが足りなくて差が出ないのか、いかなるテストパタンでも差が出ないのかの識別は容易に行えます。機能安全における故障の影響解析では、故障検出の度合いが重要な成果物の一つとなり、ISO26262では、例えばもっとも安全性の高いASIL-Dを狙う場合、故障が1つあった場合に、F-Oに差がありながら(=故障が機能に影響を与えながら)C-Oに差が出ない(=故障を検出できない)比率を全故障に対して1%というとても小さな数値以内に抑えねばなりません。このような究極条件時には、故障一つが検出できるかどうかの可否が重要になってきますので、確実に網羅的手法で押さえておきたいものです。
ところで、SECにとって、故障影響解析は実は得意な分野です。SECは比較する回路に大きな差がない場合、計算時間を短くできる(裏から見ると、より大きな回路を扱うことができる)アルゴリズムを採用しています。故障の影響解析では、比較する回路は故障ポイントの有無の差があるだけで、ほぼ同じ回路と言えますので、それこそSECのためにあるような回路比較です。

2.フォーマル検証はソフトウェアSMの改善にも役立つ。

SMとしては、デュアルロックステップやECC回路のようなハードウェア的手法以外に、特にコストの面からハードウェアをあまり重くできない場合には、例えばパワーオン時や定期的なタイマ割り込みで診断パタンを入力し、その結果をチェックする、というような手法を取ることがあります。このような診断プログラム等のテストパタンを利用する故障検出手法をソフトウェアSMと呼ぶことにします。製造時故障に関して造詣の深い読者の方であればよくご存じのように、故障を検出するための診断パタンの作成は多くの工数を費やすものであり、それでも100%の故障検出率・診断率を達成するのは困難です。ソフトウェアSMでも同じことが言えます。より短い診断時間(回路の目的は働くことであって、診断に費やすことではありませんので、診断時間には上限が定められます)でより高い診断率を達成するためには、よく練られた診断パタンを用意する必要がありますが、言うは易し行うは難し。ですが、ある故障について、フォーマル検証ではSMの挙動に「差が出る」ことが分かっているのに、今の診断パタンでは「差が出ていない」場合、出来るだけ短いパタン追加で差が出るようにしたい、このような状況で、Jasper Goldでは、そのようなテストパタンを自動で作成することができます。このパタンを元の診断パタンに追加することでC-Oで差が出る(=故障を検出できる)ようにすることも可能なのです。

図2:Jasper Goldを使った追加テストパタンの自動生成図2:Jasper Goldを使った追加テストパタンの自動生成画像をクリックすると拡大表示されます

3.フォーマル検証は現状のSMで見つけることが絶対にできない故障をチェックできる。

故障の検出率を向上するためには、十分なSMを組み込む必要があります。裏を返すと、SMが不十分であれば、追加でSMを組み込まねばなりません。SMの監視できる範囲は、そのSMに関係する信号だけです。あたりまえのことを言っていますが、Jasper Goldのアプリケーションの一つCOV(Coverage)アプリケーションを活用すると、あるSMに関連する範囲を調べることができます。全てのSMの関連する範囲を全て集めても、回路全ての部分をカバーしていなければ、そのカバーしていない部分の故障は絶対に見つかりません。SMに関連する範囲の故障をそのSMが検出できるか否かは故障影響解析を行わないとわかりませんが、そのSMで見つけられない故障の範囲は確実に分かります。これにより、追加のSMが必要か否かについて簡単に判断できます。図3.で、黒点はSMを表します。モニタのようなハードウェアSMでは、そのSMのチェック項目をアサーションとして記述します。外部で比較判定を行うようなソフトウェアSMでは、SMとして何らかのチェックを回路内でしているわけではないので「$stableではない」のような簡単かつ一般的なアサーション等を与えて、SMの起点であることだけを明確にします。

図3.COVを使用した故障ホール部分の切り分け図3.COVを使用した故障ホール部分の切り分け

Jasper Gold COVでは、SMに「関係する信号」を分別するやりかたとして、2種類の手法をもっています。一つはSMと「構造的」に繋がっていることをチェックします。ファンインを入力方向にたどっていくことで、SMに影響を与える可能性のある範囲を特定します。この操作は計算時間も軽く、SM挿入の初期段階で使うとメリットがあります。もう一つは、SMと「関数的」に繋がっていることをチェックします。これは先の手法より計算時間を必要としますが、より厳密な「関係する信号」分別が可能です。図3の例では、右の故障は構造的カバレッジ解析で分かりますが、左の故障は関数的カバレッジ解析で初めてわかります。

故障の影響解析は、特にASIL-Dのような高い安全性を求められる場合、高い精度での解析が必要になります。そのためのソリューションのひとつとして、フォーマル検証を是非ご活用ください。また、ケイデンスでは、機能安全に特化した、Jasper Goldアプリケーションも準備中ですので、ご期待ください!

テクノロジーセールスリード
後藤 謙治

Page Top