@techreport{oai:ipsj.ixsq.nii.ac.jp:00027041,
 author = {松本, 剛史 and 小松, 聡 and 藤田, 昌宏 and Takeshi, MATSUMOTO and Satoshi, KOMATSU and Masahiro, FUJITA},
 issue = {41(2006-SLDM-125)},
 month = {May},
 note = {システムレベル設計によって得られた動作記述と制約から、動作合成によってＲＴＬ設計を導出する設計フローにおいては、動作合成前後の動作記述とＲＴＬ設計の動作の等価性が保証されていることが重要である。しかし、そのための等価性検証手法、特に形式的手法は、実用化されているものはほとんどないのが現状である。そこで、本稿では、動作合成前後の設計の等価性を形式的に検証する一手法を提案し、その評価を行う。提案する手法では、ＲＴＬ設計を解析して抽出された、１サイクルで行われる動作と、合成前の動作記述を記号的に実行して、形式的に等価性を検証する。ＲＴＬ設計から動作を抽出する作業では、いくつかの変換規則を適用することによって、ＲＴＬ設計中のビット結合などのビットレベル処理をワードレベルの処理に置き換え、個々の演算を解釈せずに検証が可能になるようにしている。また、いくつかの設計例に対して実験を行い、指定された適当な等価性を検証できることを確認した。, ln system-level design，RTL designs are generated by behavioral synthesizers from behavior descriptions, and the equivalence between designs before and after behaviral synthesis should be guaranteed. However, few verification methods，especially formal ones，are available for this purpose. ln this paper, we propose a method to formally verify the equivalence. In the method, behaviors executed in a clock cycle in RTL designs are extracted，and symbolically simulated with the original behavior descriptions. When extracting behaviors from RTL designs，several rules are applied to translate bit-level operations in RTL into word-level ones so that the equivalence can be verified uninterpretedly. Also, we show the experimental results on some design examples.},
 title = {動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討},
 year = {2006}
}