Intel Keynote On Formal A Mind-Stretcher

הועלה מחדש על ידי אפלטון

עוקב: 0

Synopsys פרסמה באתר SolvNet הרצאה מרתקת שהעביר ד"ר תיאו דריין מ-Intel Graphics. הנושא הוא בדיקת שוויון נתיב נתונים. אולי נשמע כמו עוד אישור DPV פורמלי של Synopsys VC, אבל אתה צריך לראות את זה בכל מקרה. זהו דיון מרחיב תודעה על השימושים והשיקולים בפורמלי, אשר ייקח אותך מעבר לסוג של מדריך למשתמש השגרתי של נדנדה לטריטוריה מרתקת יותר.

Intel Keynote על פורמלי

הבנה אינטלקטואלית לעומת בדיקה לדוגמה

סימולציה מונעת מבחן על כל צורותיה היא מצוינת ולעיתים בלתי ניתנת להחלפה באימות נכונות מפרט או יישום תכנון. זה גם קל להתחיל. פשוט כתוב תוכנית בדיקה ותתחיל לדמות. אבל הצד השני של הפשטות הזו הוא שאנחנו לא צריכים לגמרי להבין מה אנחנו בודקים כדי להתחיל. אנחנו משכנעים את עצמנו שקראנו את המפרט בעיון ומבינים את כל המקרים הפיננסיים, אבל לא צריך הרבה מורכבות מורכבת כדי להציף את ההבנה שלנו.

פורמלי מעודד אותך להבין את הפונקציונליות ברמה עמוקה (לפחות אם אתה רוצה לספק תוצאה בעלת ערך). בדוגמה שלמעלה, שאלה פשוטה - האם z יכול להיות כל 1 - לא מצליחה להדגים דוגמה במיליארד מחזורים בסימולטור. לא מפתיע, שכן מדובר במקרה פינתי קיצוני. מבחן רשמי מספק דוגמה ספציפית ומאוד לא ברורה ב-188 שניות ויכול להוכיח שזהו המקרה היחידי בקצת פחות זמן.

בסדר רשמי עשה את מה שבדיקות דינמיות לא יכלו לעשות, אבל חשוב מכך למדת משהו שהסימולטור אולי לא אמר לך מעולם. שהיה רק מקרה אחד אפשרי שבו המצב הזה יכול לקרות. פורמלי עזר לך להבין טוב יותר את העיצוב ברמה אינטלקטואלית, לא רק כסיכום הסתברותי על פני קבוצה סופית של מקרי מבחן.

בעיות במפרט

הדוגמה הבאה של תיאו מבוססת על מכונה אוטומטית של באגים (נקראת כך כי כשאתה לוחץ על כפתור אתה מקבל באג). זה נראה כמו בעיה די פשוטה של בדיקת שוויון C ל-RTL, דגם C משמאל, דגם RTL מימין. אחת ההפתעות עבור תיאו בימיו הראשונים בפורמליות הייתה שהתנהגות העברה ימנית בדגם C אינה מוגדרת לחלוטין בתקן C, למרות ש-gcc יתנהג בצורה סבירה. עם זאת, DPV תתלונן על אי התאמה בהשוואה ל-RTL, כפי שצריך. התנהגות לא מוגדרת היא דבר מסוכן להסתמך עליו.

פורמלית כמכונה אוטומטית של באגים

השוואת מפרט בין C ל-RTL מגיעה עם סיכונים אחרים, במיוחד סביב רוחבי סיביות. חיתוך או אובדן של סיבית העברה באות ביניים (מס' 3 לעיל) הן דוגמאות טובות. האם אלו בעיות מפרט? אולי אזור אפור בין מפרט ובחירות יישום.

מעבר לבדיקת שוויון

המטרה העיקרית של DPV, כך נראה, היא לבדוק שוויון בין התייחסות C או RTL לבין יישום RTL. אבל הצורך הזה הוא נדיר יחסית ויש דרכים שימושיות אחרות שטכנולוגיה כזו עשויה להיות מיושמת, אם היא קצת מחוץ לקופסה. תחילה קלאסיקה בעולם ההטמעה - עשיתי שינוי, תיקנתי באג - האם הצגתי באגים חדשים כתוצאה מכך? קצת כמו בדיקת SEQ לאחר הוספת שער שעון. ניתוח נגישות בפלטי בלוק עשוי להיות יישום שימושי נוסף במקרים מסוימים.

לא רק בדיקת שוויון

תיאו נעשה אפילו יותר יצירתי, ומבקש מהחניכים להשתמש בדוגמאות נגד כדי להבין טוב יותר את העיצוב, לפתור סודוקוס or לפרק מספרים שלמים. הוא מכיר בכך ש-DPV מהווה דרך מוזרה לגשת לבעיות כאלה, אך מציין שכוונתו היא לשבור את האשליה ש-DPV מיועד רק לבדיקת שוויון. רעיון מעניין ובהחלט מותח את המוח לחשוב על אתגרים כאלה. (אני מודה שהתחלתי מיד לחשוב על בעיית הסודוקו ברגע שהוא הזכיר אותה.)

לעטוף

תיאו מסיים בדיון על מתודולוגיות חשובות בשימוש בייצור, סביב אילוצים, רגרסיות והשוואות עם מודלים של RTL מדור קודם. כמו כן האתגרים לדעת אם מה שאתה בודק אכן תואם את מפרט השפה הטבעית ברמה העליונה.

דיבור ממריץ מאוד, שווה צפייה כאן ב-SolvNet!

שתף את הפוסט הזה באמצעות: