Algebraic Specification of Sequential Circuit with an Unfixed Number of Modules and Its Verification

HOU Yurong
SATO Youichirou
SUGIYAMA Yuji
OKAMOTO Takuji

同一モジュールを複数個含む順序回路では,モジュール数がパラメータ化されることがあり,また満たすべき性質もモジュール数がパラメータ化されたまま与えられることがある.本論文では,そのような順序回路と性質を対象に,モジュール数がパラメータ化されたままの状態で行うことのできる代数的検証法について検討し,検証が可能であるための十分条件を示している.この十分条件は,同一モジュール群の接続関係が同型であることなどを含んでいる.また,この十分条件の最用例として,リングアービタの抽象的動作の仕様を代数的に記述し,それが満たすべき二つの性質である"相互排他性"と"ノーデッドロック性"の検証を行っている.

The Transactions of the Institute of Electronics,Information and Communication Engineers.

The Institute of Electronics, Information and Communication Engineers

J76-D-I

11

594

603

http://ci.nii.ac.jp/naid/110003315850
http://ci.nii.ac.jp/ncid/AN10071319
http://id.ndl.go.jp/bib/3845835