 |
24 |
BSVの例題 (4) |
 |
もともとinuseが不定だったのはバグと言えます。ただ、初期値を設定する代わりに最初にputdownシーケンスを入れたら良いと考え、実行したところうまく動作しました。ついでにChatGPTにコメントを付けてもらいました。以下にソースコードを示します。
ソースコード
//
// CBG SQUANDERER : Dining Philosophers In Bluespec
// (C) 2012 David Greaves, University of Cambridge
// 必要なモジュールをインポート
import StmtFSM::*;
// スプーンのインターフェースを定義
interface Spoon_if;
method Action pickup; // スプーンを持ち上げるメソッド
method Action putdown; // スプーンを置くメソッド
method Action putnumber(UInt#(5) value); // スプーンに番号を設定するメソッド
endinterface
// スプーンのモジュールを定義
(* synthesize *)
module spoon (Spoon_if);
Reg#(Bool) inuse <- mkReg(?); // スプーンの使用状況を表すレジスタ
Reg#(UInt#(5)) number <- mkReg(?); // スプーンの番号を保持するレジスタ
// スプーンを持ち上げるメソッドの実装
method Action pickup if (!inuse);
inuse <= True;
endmethod
// スプーンを置くメソッドの実装
method Action putdown;
inuse <= False;
endmethod
// スプーンに番号を設定するメソッドの実装
method Action putnumber(UInt#(5) value);
number <= value;
endmethod
endmodule
// 哲学者のベンチモジュールを定義
(* synthesize *)
module philoBENCH (Empty);
// 5つのスプーンインスタンスを作成
Spoon_if spoon0 <- spoon;
Spoon_if spoon1 <- spoon;
Spoon_if spoon2 <- spoon;
Spoon_if spoon3 <- spoon;
Spoon_if spoon4 <- spoon;
// 5人の哲学者インスタンスを作成
Diner_if din0 <- mkDiner(0, 7, 7, spoon0, spoon1);
Diner_if din1 <- mkDiner(1, 6, 4, spoon2, spoon1); // <---- 逆順で持ち上げる
Diner_if din2 <- mkDiner(2, 5, 9, spoon2, spoon3);
Diner_if din3 <- mkDiner(3, 6, 6, spoon3, spoon4);
Diner_if din4 <- mkDiner(4, 8, 8, spoon4, spoon0);
// タイマーのレジスタを作成
Reg#(UInt#(15)) timer <- mkReg(1000);
// タイマーをカウントダウンするルール
rule foo;
timer <= timer - 1;
if (timer == 0) $finish;
endrule
endmodule: philoBENCH
// ランダム数生成器のインターフェースを定義
interface Random_if;
method ActionValue#(UInt#(15)) gen; // ランダムな値を生成するメソッド
endinterface
// ランダム数生成器のモジュールを定義
module mkRandom_gen #(UInt#(15) seed) (Random_if);
Reg#(UInt#(15)) prbs <- mkReg(seed); // ランダム数を保持するレジスタ
// ランダムな値を生成するメソッドの実装
method ActionValue#(UInt#(15)) gen;
prbs <= (prbs << 1) | (((prbs >> 14) ^ (prbs >> 13)) & 1); // シフトとXORを使用してランダム値を生成
return prbs;
endmethod
endmodule
// 哲学者のインターフェースを定義
interface Diner_if;
endinterface
// 哲学者のモジュールを定義
module mkDiner #(UInt#(5) number, UInt#(15) on, UInt#(15) seed) (Spoon_if left, Spoon_if right, Diner_if i);
Reg#(Bool) eating <- mkReg(?); // 食事中かどうかを表すレジスタ
Reg#(UInt#(15)) timer <- mkReg(0); // タイマーのレジスタ
Random_if random<- mkRandom_gen(seed); // ランダム数生成器のインスタンスを作成
// タイマーをカウントダウンするルール
rule foo (timer != 0);
timer <= timer - 1;
endrule
// 哲学者の動作シーケンスを定義
Stmt seq_behaviour = (seq
while (True) seq
action // 初期状態を確定するサイクル(食事の後だったのを前に持ってきた)
eating <= False;
left.putdown;
right.putdown;
left.putnumber(?);
right.putnumber(?);
endaction
action
UInt#(15) x <- random.gen;
timer <= x & 31; // ランダムな時間を設定
endaction
await(timer== 0);
left.pickup; // 左のスプーンを持ち上げる
action
UInt#(15) x <- random.gen;
timer <= x & 31; // ランダムな時間を設定
endaction
await(timer== 0);
right.pickup; // 右のスプーンを持ち上げる
action
eating <= True; // 食事を開始
timer <= on; // 食事時間を設定
left.putnumber(number); // スプーンに哲学者の番号を設定
right.putnumber(number); // スプーンに哲学者の番号を設定
endaction
await(timer==0);
endseq
endseq);
// シーケンスを自動的に実行するFSMを作成
mkAutoFSM(seq_behaviour);
endmodule
以下にシミュレーション波形を示します。putdownは終了処理だった(pickup→putdown)ものをシーケンスの最初に持ってくる(putdown→pickup)ことにより、初期状態が確定し不定が継続しなくなりました。
図らずも元のコードのバグを発見しましたが、あえて不定を設定しないと見つからないため、シミュレーションは不定も込みで実施したほうが良いと思います。
