ÇѱÛÁ¦¸ñ(Korean Title) |
Verilog HDL ·Î ±â¼úµÈ Á¶ÇÕ ³í¸®È¸·ÎÀÇ Cadence SMV ±â¹Ý Á¤Çü °ËÁõ ¹æ¹ý |
¿µ¹®Á¦¸ñ(English Title) |
A Cadence SMV Based Formal Verification Method for Combinational Logics Written in Verilog HDL |
ÀúÀÚ(Author) |
Á¶¼ºµæ
±è¿µ±Ô
¹®º´ÀÎ
ÃÖÀ±ÀÚ
Seond-Deuk Jo
Young-Kyu Kim
Byungin Moon
Yunja Choi
|
¿ø¹®¼ö·Ïó(Citation) |
VOL 22 NO. 02 PP. 1027 ~ 1030 (2015. 10) |
Çѱ۳»¿ë (Korean Abstract) |
Çϵå¿þ¾î µðÀÚÀÎ ¼³°Ô¿¡¼ Ãʱ⠴ܰèÀÇ ¼³°è ¿À·ù ¹ß°ßÀº °³¹ß ºñ¿ë °¨¼Ò ¹× ¼³°è ½Ã°£ ´ÜÃà Ãø¸é¿¡¼ ±× È¿°ú°¡ ¸Å¿ì Å©´Ù. ÀÌ·¯ÇÑ Ãʱ⠼³°è ¿À·ù ¹ß°ßÀ» À§ÇÑ ´ëÇ¥ÀûÀÎ ¹æ¹ýÀ¸·Î´Â Á¤Çü °ËÁõ(formal verification)ÀÌ ÀÖÀ¸¸ç, Cadence SMV(Symbolic Model Verifier)´Â Á¤Çü °ËÁõÀ» À§ÇØ Verlog HEL(Hardware Description Language) À» SMV ·Î ÀÚµ¿ º¯È¯ ÇØÁÖ´Â ÀåÁ¡ÀÌ ÀÖÁö¸¸, »ç°Ç ±â¹Ý ±¸Á¶(event based structure)ÀÇ sensitivity list ¿¡ ´ëÇÑ Áö¿øÀ» ÇÏÁö ¾Ê´Â ÇÑ°è°¡ ÀÖ´Ù. ÀÌ¿¡ º» ³í¹®¿¡¼´Â Cadence SMV ¿¡¼ µðÁöÅÐȸ·Î(digital circuit) Áß ÇϳªÀÎ Á¶ÇÕ ³í¸®È¸·Î(combinational logic circuit)¸¦ sensitivity list °¡ °í·ÁµÈ °ËÁõÀÌ °¡´ÉÇϵµ·Ï ÇÏ´Â ¹æ¹ýÀ» Á¦¾ÈÇÑ´Ù. ½Å·Ú¼º ÀÖ´Â ½ÇÇèÀ» À§ÇØ º» ³í¹®¿¡¼´Â Á¦¾ÈÇÏ´Â ¹æ¹ýÀÇ ÀϹÝÀûÀÎ ±ÔÄ¢À» µµÃâÇÏ¿´°í, µµÃâµÈ ±ÔÄ¢ÀÌ Àû¿ëµÈ SMV ÆÄÀÏÀ» »ý¼ºÇÏ´Â ÀÚµ¿È ÇÁ·Î±×·¥À» ±¸ÇöÇÏ¿© ½ÇÇèÇÏ¿´´Ù. ½ÇÇè°á°ú Á¦¾ÈÇÑ ¹æ¹ýÀ» Àû¿ëÇÑ °æ¿ì ±âÁ¸ cadence SMV°¡ ¹ß°ßÇÏÁö ¸øÇÑ ¼³°ìÇ×ÀÇ ¿À·ù¸¦ ¹ß°ßÇÒ ¼ö ÀÖ¾ú´Ù.
|
¿µ¹®³»¿ë (English Abstract) |
|
Å°¿öµå(Keyword) |
|
ÆÄÀÏ÷ºÎ |
PDF ´Ù¿î·Îµå
|