CSP Over NSL
この記事は HDL Advent Calendar 2015( http://qiita.com/advent-calendar/2015/hdl )の記事です。
パルテノン研究会( http://www.parthenon-society.com/ )あたりに出そうかなぁと思っていたら塩漬けになってしまっていたものです(いくつか問題があることもあり)。実装はまだ作成しておらず、手作業による「こんな感じにできたらいいな」というProof of Concept未満のコンセプトだけの内容という感じですが、何かの参考になったら、と思います。
まずCSPについてですが、CSPはCommunicating Sequential Processesの略で、並行システムを相互に同期通信する逐次的なプロセス群としてモデル化するものです(詳細は wikipedia:Communicating Sequential Processes や、教科書『並行システムの検証と実装』を参照)
次の「NSL風」コードを見てください。
declare producer_consumer { output o; } module producer_consumer { reg init_reg[2] = 0b01; reg s_flip = 0b0; $channel_self(chan, 1) any { 0b1 : init_reg = {init_reg[0], 0b0}; init_reg : { } } $process(Main) $par { $start(Sender); $start(Receiver); } $process(Sender) $send(chan, s_flip) -> $start(Sender) $process(Receiver) $recv(chan, "o=") -> $start(Receiver) }
CSPによる「生産者-消費者」のモデリングを、マクロプロセッサで処理するっぽい構文でNSL中に記述したようなつもり、のものです。
CSPにおける単純なプロセスは、次のような形をしています(形式的な定義の一部を抜粋したものです)。
プロセス : プロセス名 プロセス : イベント → プロセス イベント : チャネル送信 イベント : チャネル受信 チャネル送信 : チャネル名!変数名 チャネル受信 : チャネル名?変数名
これらを使って、生産者と消費者(送信者と受信者)をプロセスとするように次のようにモデル化し、
Sender = chan!s_flip → Sender Receiver = chan?o → Receiver
これを言語(+マクロプロセッサ)による記述っぽく変換すると、最初に挙げたリストのようになる、というわけです。
最初のリストから、最終的には次のようなNSLを生成したい、という感じになります(このリストは実際にNSLとして有効なものです。また、CSPの実現として十分なものにはなっていません。それと、ランダムに待ちが入るようなコードが入っているのは、動作チェック用に追加しているもので、形式的な変換中に入れる意図ではありません)。
declare rand_gen simulation { output o; func_in get_rand():o; } module rand_gen { func get_rand { return _random[16]; } } declare producer_consumer simulation { output o; } module producer_consumer { rand_gen rand_a, rand_b; reg init_reg[2] = 0b01; reg s_flip = 0b0; /* $channel_self(chan, 1) */ func_self ch_chan_send(); func_self ch_chan_recv(); func_self ch_chan_estab(); wire ch_chan_dat[1]; func_self p_Main_req(); func_self p_Main_sub0(); func_self p_Main_sub1(); func_self p_Sender_req(); func_self p_Sender_ack(); func_self p_Receiver_req(); func_self p_Receiver_ack(); any { 0b1 : init_reg := {init_reg[0], 0b0}; init_reg[1] : { p_Main_req(); } (ch_chan_send & ch_chan_recv) : { ch_chan_estab(); } } /* $process(Main) $par { $start(Sender); $start(Receiver); } */ func p_Main_req { p_Main_sub0(); p_Main_sub1(); } func p_Main_sub0 seq { p_Sender_req(); } func p_Main_sub1 seq { p_Receiver_req(); } /* $process(Sender) $send(chan, s_flip) -> $start(Sender) */ func p_Sender_req seq { label_name s0, s1; s0 : any { 0b1 : ch_chan_send(); ~ch_chan_estab : goto s0; ch_chan_estab : { p_Sender_ack(); ch_chan_dat = s_flip; s_flip := ~s_flip; if (rand_a.get_rand()) goto s1; } } while (rand_a.get_rand()) { /* NOP */; } s1 : any { 0b1 : p_Sender_req(); ~p_Sender_ack : goto s1; } } /* $process(Receiver) $recv(chan, "o = ") -> $start(Receiver) */ func p_Receiver_req seq { s0 : any { 0b1 : ch_chan_recv(); ~ch_chan_estab : goto s0; ch_chan_estab : { p_Receiver_ack(); o = ch_chan_dat; if (rand_b.get_rand()) goto s1; } } while (rand_b.get_rand()) { /* NOP */; } s1 : any { 0b1 : p_Receiver_req(); ~p_Receiver_ack : goto s1; } } }
プロセスのシーケンシャルな動作をNSLで実装するためにseqを使っています。また、信号線として func_self による信号線を多用していますが、これは「特段に記述のない状態では Low になる」という特性が必要なためで func らしい機能を必要としているためではありません。
まず、元の記述では $start で表現しているプロセスの動作開始は *_req という信号線のアサートで要求され、実際に動作開始したら _ack がアサートされます。
チャネル通信ではもう少し込み入った動作が必要になります。
送信側は ch_*_send 、受信側は ch_*_recv という信号線をアサートし、両者が同時にアサートされていると ch_*_estab という信号がアサートされるので、送信側・受信側ともに、それを見て送信・受信の動作をし、シーケンスを次に進めます。
(CSPをご存知の方には、そんな単純なアービトレーションでは、(ガードが実現できないのは当然としても)外部選択がある場合に困るのではないか? という疑問があるでしょう。私としては、ハードウェア記述言語に非決定的な記述を入れるのはどうかと思ったため、外部選択を「左側が可能なら左側を、ダメなら右側を」という意味に再解釈し(CFGとPEGのようなイメージです)、少し複雑な例で実験して、「依存関係に循環があると破綻する」という結果を得ています)
最後に、残っている課題ですが、
- CSP的に正しいかどうかの確認(正しくないとCSPを使う意味がありません)
- チャネルだけでなくプロセスの動作開始にも調停を入れる(?)
- 実際にマクロ命令を元に、アービトレーション等の記述を生成するような実装の作成
という感じになるでしょうか(なお、今のところ予定しているわけではありません)。