DSIMで取得したSVAデータベースを解析する

やりたいこと

DSIMでアサーションやカバープロパティを実行すると、下記のようなログが出力される。

SVA Summary:  4 assertions, 52 evaluations, 5 nonvacuous passes
SVA Summary:  5 cover property statements, 65 evaluations, 8 nonvacuous passes, all statements covered

ただし、これだと全てのカバープロパティがカバーされたのか、特定のプロカティが複数回カバーされたのかがわかりにくい。

やったこと

カバレッジを取得してmetrics.dbに保存する。

dsim tb.sv dut.sv -top tb +acc+b -code-cov a -cov-db metrics.db

なお"a"はブロックカバレッジ、エクスプレッションカバレッジ、トグルカバレッジを全て取得するオプション。

  -code-cov ...                  Enables coverage for b[lock], e[xpression], t[oggle] or a[ll] code coverage features

metrics.dbを整形して表形式で結果を出力する。

sqlite3 -header -column metrics.db "
SELECT
    ac.name,
    ac.kind,
    ab.attempts,
    ab.passes,
    ab.fails,
    ab.vacPasses
FROM assertionCoverages ac
JOIN assertionBins ab
    ON ac.assertHash = ab.assertHash
ORDER BY ac.kind, ac.name;
"

結果はこんな感じ。

name                                  kind    attempts  passes  fails  vacPasses
------------------------------------  ------  --------  ------  -----  ---------
ass_WAIT_to_DISPENSE                  assert  13        1       0      12       
ass_WAIT_to_REFUND                    assert  13        2       0      11       
ass_WAIT_to_REFUND_prioritize_cancel  assert  13        1       0      12       
ass_dispense_asserted_at_DISPENSE     assert  13        1       0      12       
cov_IDLE_to_WAIT                      cover   13        3       0      10       
cov_WAIT_to_DISPENSE                  cover   13        1       0      12       
cov_WAIT_to_REFUND                    cover   13        2       0      11       
cov_WAIT_to_REFUND_prioritize_cancel  cover   13        1       0      12       
cov_WAIT_to_WAIT                      cover   13        1       0      12