18 / 37 · 理解度チェック

設計確認：幅・優先順位・循環の境界

与えられた状態遷移の仕様から、境界値と同時制御入力を判断します。

modulo-10 カウンタの取り決め

4 ビット unsigned^{unsigned ビット列を非負整数として解釈する規則です。n ビットの範囲は 0 から 2^n−1 で、同じビット列の signed 解釈と異なる場合があります。詳しく見る} の count に対し、優先順位は reset、enable、保持です。reset が 1 なら 0、enable が 1 なら 9 以上で 0 に戻り、それ以外は 1 増加します。

N=\lceil\log_2 10\rceil=4

4 ビットとは、記憶できる状態が 16 個という意味です。使いたい状態が 10 個という仕様まで自動実装するわけではありません。特に count=9、enable=0 で 0 に戻ってはいけません。

下の各列は立上りエッジ^{立上りエッジクロックが 0 から 1 に変わる瞬間です。CLK=1 の区間全体を指すレベルとは区別します。詳しく見る}の記録です。入力はエッジ直前、「更新後」の状態は更新直後です。並びはサンプル順で、物理的な伝搬遅延^{伝搬遅延入力が変わってから、出力が正しい値に安定するまでの時間です。論理式の等価性と時間特性は別の性質です。詳しく見る}ではありません。初期 count=9 です。reset のない最初の列で enable=0 なら 9 を保持し、次の列で enable=1 のときだけ 0 に戻ります。

境界値でも保持は維持する

波形データを表示

波形データ：各文字は一つの区間、ドットは前の状態の保持、p はクロック 1 周期を表します。
信号	波形	バスの値
エッジ	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
更新後 count	`23.4`	9 → 0 → 1

追加の設計問題

count=9、reset=0、enable=0 の次の値を求めてください。
count=15 で enable=1 を与えたときの回復方針を説明してください。
count=9、reset=1、enable=1 で終了パルスを出すべきかを定めてください。リセット^{リセット状態を仕様で定めた初期値に戻す制御です。同期式か非同期式か、他の制御より優先されるかを合わせて定めます。詳しく見る}中の出力は 0 と定義したものとします。

自分で考えてみましょう

count の全値 0～15 と reset・enable の全組合せを一段階遷移で検査するには、何例必要ですか。これだけで長い状態列の全要求が自動的に証明されますか。

解説を見る

$16\times2\times2=64$ 例です。この設計のように count が完全な状態を表し、次状態・出力仕様が正確なら、一段階の検査は強い根拠になります。ただし初期化・入力仮定・終了パルスの別状態・実タイミングなど、含めていない要求まで証明するものではありません。

現在 count=9 で、reset=1 と enable=1 が同時にサンプルされました。リセット優先に合う次の count と終了パルスは何ですか。

答えを選択count=0、終了パルス=1：正常な循環として扱う。count=10、終了パルス=0：enable が優先される。count=0、終了パルス=0：リセットが状態とパルスを初期化する。