Formality, fm_shell, RTL, ゲート, 検証, 一致
注意：解像度は横800以上にしてね．
Formalityを使って，RTLとゲートが一致しているかを検証する方法を軽く書いてみた．
たぶん，以下の手順でできると思う．
説明しやすいGUI版のみ．
まず，起動はどうするかというと，
>formality
もしくは，
>fm_shell
とすればよい．
ただし，fm_shellの場合は，そのままではGUI環境ではないので，
>start_gui
と最初に打ち込まないといけない．
1．立ち上がると，以下のような画面が出てくるはずである．
そして，まずは，RTLをformalityに食わせる．
そのためには，Verilogをクリックする．
2．すると，以下のような画面が出てくるんで，検証するRTLを選択する．
複数のファイルから構成されるモジュールを検証するときは，もちろん，必要なファイルを全て読み込む．
2．の続き
たとえば，以下のようななかんじ．
Windowsと一緒で，コントロールを押しながら選択すれば，まとめて読み込める．
3．Load Filesをクリックして，さらに，Optionsを設定する．
3．の続き
以下のような画面が出てくる．
3．の続き
なにはともあれ，VCS Style Optionsを設定(クリッくも)する．
まあ，とりあえず，Library DirectoryとDefinesは設定しよう．
あと，よく，Addをクリックし忘れるので注意．Addしてから，OKをクリックする．
4．Set Top Designをする．
はい，さっき呼んだRTLの中の最上位階層をしていする．
選んで，Set Topをクリックする．
4．の続き
すると，いろいろとミスがなければ，以下のように，1.Referenceにチェックが入る．
ダメだった場合は，なんかいっぱい怒られるから，すぐわかる．頑張って解決する．
5．Implementationの指定を次はするみたいだ．
5．の続き
ここで，DBファイル形式のネットリストだとすると，以下のように，DBをクリックしとく．
6．下の方のDBをクリックして，DBファイルを読み込む．
6．の続き
Load Filesをクリックする．
ここも，Optionsを付ける必要性のある人は付ける．
よく分からない人は，とりあえず，付けなくても，多分大丈夫でしょう．
7．Read DB Librariesを忘れずにやる．
これは，論理合成に用いたテクノロジライブラリを読むという操作です．
これを忘れると，いっぱい怒られます．使用した全セルにリンクできないって．
7．の続き
ここでは，DB形式のライブラリ(slow.db)を呼んでます．
8．ImplementationのSet Topも忘れずにやる．
8．の続き
ミスってなければ，以下のように，Implementationにチェックが入る．
9．Setupはやりたい人だけやってください．
とりあえず，よく分からない人はやらなくても多分大丈夫です．
10．Matchをする．
Run Matchingをクリックすると開始する．
10．の続き
うまくいくと，以下のような画面が出るはず．
11．Verifyする．
Verify Allをクリックするだけ．
11．の続き
うまくいくと，以下のような画面が出るはず．
12．自動的にこんな画面が出てくる．
Verifyにミスったときは，ここでdiagnoseして，修正しようということになっているが，
実際問題，ここから，修正をしていくのは至難の技である．
正直ミスが出ないことを祈るしかない．
それでも出てしまった場合は，近くに居るプロに質問してみよう．(なかなか居ないが)
以上、おわり、ありがとう。
メール出すなら、
ito@ddna.is.tsukuba.ac.jp
まで（ってまじで出す人居ないよな。）