• אודות
  • כנסים ואירועים
  • צור קשר
  • הצטרפות לניוזלטר
  • TapeOut Magazine
  • ChipEx
  • סיליקון קלאב
  • Jobs
מבית
EN
Tech News, Magazine & Review WordPress Theme 2017
  • עיקר החדשות
    מכונית אוטונומית. אילוסטרציה: depositphotos.com

    יצרני הרכב על פרשת דרכים בתחום החיישנים לכלי רכב אוטונומיים

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

    ChipEx2022: “נשארו מעט מאוד ספקים של שירותי ייצור מתקדם של שבבים, זו אחריות גדולה מאוד”

    חברת ג'נרל מוטורס הציגה ביתן וירטואלי בכנס CES 2022. צילום יחצ

    ג’נרל מוטורס מודיעה על שיתוף פעולה עם חברת Red Hat

    מנכ"ל אפל ישראל רוני פרידמן בכנס ChipEx2022. צילום: ניב קנטור

    רוני פרידמן מנכ”ל אפל ישראל: היעילות האנרגטית היא ה”דת” של אפל

    לקראת ChipEx2022: פרופ’ דייויד בלאו, אוניברסיטת מישיגן ל-Chiportal: פיתחנו מאיצי בינה מלאכותית למכשירי קצה זעירים

    לקראת ChipEx2022: פרופ’ דייויד בלאו, אוניברסיטת מישיגן ל-Chiportal: פיתחנו מאיצי בינה מלאכותית למכשירי קצה זעירים

    לקראת ChipEx2022: מנכ”לית איגוד RISC-V הבינלאומי: טכנולוגית הקוד הפתוח שלנו תחדור ל-14% מהמעבדים

    לקראת ChipEx2022: מנכ”לית איגוד RISC-V הבינלאומי: טכנולוגית הקוד הפתוח שלנו תחדור ל-14% מהמעבדים

    Trending Tags

    • בישראל
      חנן ברנד מונה לסמנכ"ל ומנהל חטיבת ההזנק ברשות החדשנות. צילום יחצ

      חנן ברנד מונה לסמנכ”ל ומנהל חטיבת ההזנק ברשות החדשנות

      מנכ"ל סלברייט יוסי כרמיל. צילום: שלומי יוסף.

      סלברייט: הכנסות של 62.4 מליון דולר ברבעון הראשון, עליה של 17%

      הרכב האוטונומי של מאגד אוואטר בכנס אקומושן 2022. צילום יחצ

      מאגד אוואטר הציג באקומושן להצגת שיתוף פעולה ייחודי עם מעבדת החדשנות של רנו-ניסאן-מיצובישי בישראל

      מנכ”ל וואלנס: היוניקורנים נוצרו כי קרנות פנסיה וגמל חיפשו אפיקים חלופיים בריבית אפס

      אומניויז’ן וואלנס יציעו מצלמה תואמת MIPI A-PHY עבור מערכות סיוע לנהג

      יואב זייף צילום באדיבות חברת סטרטסיס

      סטרטסיס ממזגת את חברת הבת MakerBot עם Ultimaker ליצירת שחקנית משמעותית של מדפסות שולחניות

      איתן אופנהיים, נשיא ומנכ"ל נובה. צילום: בני גם זו לטובה

      נובה מדווחת על תוצאות הרבעון הראשון עם שיא בהכנסות – 134 מ’ ד’

      Trending Tags

      • מדורים
        • אוטומוטיב
        • בינה מלאכותית (AI/ML)
        • בטחון, תעופה וחלל
        • ‫טכנולוגיות ירוקות‬
        • ‫יצור (‪(FABs‬‬
        • ‫צב”ד‬
        • ‫שבבים‬
        • ‫רכיבים‬ (IOT)
        • ‫תוכנות משובצות‬
        • ‫תכנון אלק’ (‪(EDA‬‬
        • תקשורת מהירה
        • ‫‪FPGA‬‬
        • ‫ ‪וזכרונות IPs‬‬
      • מאמרים ומחקרים
      • צ’יפסים
      • Chiportal Index
        • Search By Category
        • Search By ABC
      No Result
      View All Result
      Chiportal
      • עיקר החדשות
        מכונית אוטונומית. אילוסטרציה: depositphotos.com

        יצרני הרכב על פרשת דרכים בתחום החיישנים לכלי רכב אוטונומיים

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

        ChipEx2022: “נשארו מעט מאוד ספקים של שירותי ייצור מתקדם של שבבים, זו אחריות גדולה מאוד”

        חברת ג'נרל מוטורס הציגה ביתן וירטואלי בכנס CES 2022. צילום יחצ

        ג’נרל מוטורס מודיעה על שיתוף פעולה עם חברת Red Hat

        מנכ"ל אפל ישראל רוני פרידמן בכנס ChipEx2022. צילום: ניב קנטור

        רוני פרידמן מנכ”ל אפל ישראל: היעילות האנרגטית היא ה”דת” של אפל

        לקראת ChipEx2022: פרופ’ דייויד בלאו, אוניברסיטת מישיגן ל-Chiportal: פיתחנו מאיצי בינה מלאכותית למכשירי קצה זעירים

        לקראת ChipEx2022: פרופ’ דייויד בלאו, אוניברסיטת מישיגן ל-Chiportal: פיתחנו מאיצי בינה מלאכותית למכשירי קצה זעירים

        לקראת ChipEx2022: מנכ”לית איגוד RISC-V הבינלאומי: טכנולוגית הקוד הפתוח שלנו תחדור ל-14% מהמעבדים

        לקראת ChipEx2022: מנכ”לית איגוד RISC-V הבינלאומי: טכנולוגית הקוד הפתוח שלנו תחדור ל-14% מהמעבדים

        Trending Tags

        • בישראל
          חנן ברנד מונה לסמנכ"ל ומנהל חטיבת ההזנק ברשות החדשנות. צילום יחצ

          חנן ברנד מונה לסמנכ”ל ומנהל חטיבת ההזנק ברשות החדשנות

          מנכ"ל סלברייט יוסי כרמיל. צילום: שלומי יוסף.

          סלברייט: הכנסות של 62.4 מליון דולר ברבעון הראשון, עליה של 17%

          הרכב האוטונומי של מאגד אוואטר בכנס אקומושן 2022. צילום יחצ

          מאגד אוואטר הציג באקומושן להצגת שיתוף פעולה ייחודי עם מעבדת החדשנות של רנו-ניסאן-מיצובישי בישראל

          מנכ”ל וואלנס: היוניקורנים נוצרו כי קרנות פנסיה וגמל חיפשו אפיקים חלופיים בריבית אפס

          אומניויז’ן וואלנס יציעו מצלמה תואמת MIPI A-PHY עבור מערכות סיוע לנהג

          יואב זייף צילום באדיבות חברת סטרטסיס

          סטרטסיס ממזגת את חברת הבת MakerBot עם Ultimaker ליצירת שחקנית משמעותית של מדפסות שולחניות

          איתן אופנהיים, נשיא ומנכ"ל נובה. צילום: בני גם זו לטובה

          נובה מדווחת על תוצאות הרבעון הראשון עם שיא בהכנסות – 134 מ’ ד’

          Trending Tags

          • מדורים
            • אוטומוטיב
            • בינה מלאכותית (AI/ML)
            • בטחון, תעופה וחלל
            • ‫טכנולוגיות ירוקות‬
            • ‫יצור (‪(FABs‬‬
            • ‫צב”ד‬
            • ‫שבבים‬
            • ‫רכיבים‬ (IOT)
            • ‫תוכנות משובצות‬
            • ‫תכנון אלק’ (‪(EDA‬‬
            • תקשורת מהירה
            • ‫‪FPGA‬‬
            • ‫ ‪וזכרונות IPs‬‬
          • מאמרים ומחקרים
          • צ’יפסים
          • Chiportal Index
            • Search By Category
            • Search By ABC
          No Result
          View All Result
          Chiportal
          No Result
          View All Result

          בית דפי האתר ושונות בלוגים הבלוגים של Chiportal Has formal verification technology stalled

          Has formal verification technology stalled

          מאת Dr. Olivier Coudert
          16 אפריל 2010
          in הבלוגים של Chiportal
          Olivier_Coudert
          Share on FacebookShare on TwitterLinkedinWhastsapp

          Has formal verification technology stalled?


          Dr. Olivier Coudert

          underline-blog-409
          We all know that functional verification is the costliest and most time-consuming aspect of ASIC design –about 50% of the total cost, and from 40% to 70% of the total project duration. And we all know that simulation is by far the prevalent verification method, even though it is inherently incomplete due to an input space that is too large to be enumerated.

          ” .

          Has formal verification technology stalled?

          Dr. Olivier Coudert

          underline-blog-409

          We all know that functional verification is the Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 costliest and most time-consuming aspect of ASIC design –about 50% of the total cost, and from 40% to 70% of the total project duration. And we all know that simulation is by far the prevalent verification method, even though it is inherently incomplete due to an input space that is too large to be enumerated. So formal verification, which aims at completeness, should be a thriving field, given the impact it can have on the overall cost and schedule of ASIC designs.
          There is certainly no lack of competition in formal verification. The big three EDA public companies, Synopsys, Cadence, and Mentor Graphics, have all their own formal verification offering (Formality, Conformal, 0-in), and there are a number of startups, e.g., Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 Jasper, Atrenta, Real Intent, OneSpin, Blue Pearl Software,, to name a few. Formal verification products cover a wide range of applications: System Verilog Assertion Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 (SVA) and property checking; RTL static check; equivalence checking (EC); some limited IP verification; clock-domain crossing (CDC) verification; and timing exception verification (false paths and multi-cycle paths).
          Looking at the Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 DAC submissions this year though, I am puzzled by the overwhelming number of papers focused on increasing simulation speed and coverage, as opposed to the handful of papers discussing formal techniques. And this year is not different from last year. And the year before last. Does that mean there is a lack of innovation in formal verification core techniques?

          Improving simulation –higher coverage, less patterns, more automation— with formal techniques is a very active field, both in the academic and industrial world. Some inject faults in the RTL to separate the most discriminating patterns (e.g., Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 Certess). Others use SAT and integer constraint solvers to reduce the number of patterns, or to automatically generate patterns for hard-to-cover code branches (e.g., Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 NuSym). But success is all relative. Certess was quickly acquired last year, while NuSym is actively looking for a buyer. There are also semi-formal tools, mixing simulation and state exploration techniques (e.g., Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 Magellan), but they a have limited usage.
          What about the more fundamental formal verification technologies? The 80’s were dominated by the development of rigorous semantics models (e.g., multi-valued logic, Verilog and VHDL operational semantics for synthesis and simulation, Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 , temporal logics, and synchronous languages like Esterel and Lustre) and the introduction of BDDs. The 90’s saw EC tools spreading in the industry and the rise of model checking. The 00’s were all about Normal 0 false false false EN-US X-NONE HE MicrosoftInternetExplorer4 SAT and model abstraction to push the capacity of EC and bring property checking to the end-user, as well as static code analysis, CDC, and timing verification. What are we going to see in this decade?
          Verification has a lot of challenging problems, with incomplete or no solution at all. Here is my list:
          •    Merged arithmetic. There are robust methods to verify adders and multipliers of practically any size, but no one can verify merged arithmetics as small as 32-bits.
          •    Low power. This leads to complex properties capturing the correctness of sequential clock gating and power gating. The former is becoming more common, and there are techniques to address most of it (e.g., Calypto and Conformal). But the later is still waiting for a comprehensive and automated solution.
          •    RTL debugging. There are a number of static code checkers, but debugging is still very poor.
          •    HW/SW verification. Can we leverage deductive methods (predicate logic, HOL, rewriting system) to close the gap between software and RTL?
          •    Mixed signal (analog/digital) devices: this is a very young area of research, but it should see a lot of focus given the increasing ubiquity of mixed signal designs.
          If formal verification core technology is to evolve, we will see some original solutions to the problems listed above. What do you think should be added to this list? And which techniques will evolve as the most promising?

          Dr. Olivier Coudert has 20 years experience in software architecture and EDA product development, including 10 years in research. He received his PhD in Computer Sciences from Ecole nationale supérieure des Télécommunications, Paris , France , in 1991. He has published 50+ papers and book chapters, and he holds several patents on combinatorial optimization and physical synthesis. He is a recognized expert in the fields of formal verification, logic synthesis, low power, and physical synthesis. He led the development of several EDA products, including 3 from scratch in a startup environment. You can follow Olivier on Twitter, meet him on LinkedIn, or read his blog.

          {loadposition content-related}
          תגיות verificationאימות תכנון
          Dr. Olivier Coudert

          Dr. Olivier Coudert

          נוספים מאמרים

          Shlomo_Gradman_2
          בינה מלאכותית (AI/ML)

          האם הגענו לשלב בו מחשב יכול לנצח את המוח האנושי?

          Shlomo_Gradman_2
          הבלוגים של Chiportal

          ענקית השבבים החדשה

          ADI_KATAV
          הבלוגים של Chiportal

          היכן נפתח משרד פיתוח ושיווק כאשר פנינו לסין ושווקי אסיה?

          Shlomo_Gradman_2
          הבלוגים של Chiportal

          מה שהיה הוא לא מה שיהיה – גם בשוק האלקטרוניקה

          הפוסט הבא
          daniel_hershkowitz

          ChipEx2010 הכנס הבינלאומי הגדול ביותר של תעשיית השבבים הישראלית, יפתח ע"י שר המדע והטכנולוגיה, פרופסור דניאל הרשקוביץ

          כתיבת תגובה לבטל

          האימייל לא יוצג באתר. שדות החובה מסומנים *

          • הידיעות הנקראות ביותר
          • מאמרים פופולאריים

          הידיעות הנקראות ביותר

          • רוני פרידמן מנכ”ל אפל ישראל: היעילות האנרגטית היא ה”דת” של אפל
          • אנבידיה תגייס עוד 1,000 עובדים בשנה הקרובה בישראל – גידול של 25%
          • הבאנה משיקה את הדור השני של מעבדי הבינה המלאכותית לאימון ולהסקה
          • יצרני הרכב על פרשת דרכים בתחום החיישנים לכלי רכב אוטונומיים
          • מאגד אוואטר הציג באקומושן להצגת שיתוף פעולה ייחודי עם מעבדת החדשנות של רנו-ניסאן-מיצובישי בישראל

          מאמרים פופולאריים

          • חוקרים אמירתיים מכמתים את ההבטחה והמגבלות של אלגוריתם חדש לפיצוח הצפנות שפיתח חוקר בבן גוריון
          • שיפור דפנות כורי ההיתוך הגרעיני – התקדמות לעבר פתרונות אנרגיה חדשים
          • רואים קרוב, מודדים רחוק
          • ChipEx2022: שיטת ייצור בעלות נמוכה ודיוק גבוה עבור מראות דקות ופרוסות סיליקון
          • IBM מסמנת יעד: מחשב קוונטי מעשי עם מאות אלפי קיוביט תוך שנים ספורות

          השותפים שלנו

          לוגו TSMC
          לוגו TSMC

          לחצו למשרות פנויות בהייטק

          כנסים ואירועים

          כנסים ואירועים

          כנס ChipEx2022 יערך ב-9-10 במאי, 2022. הכנס מיועד לכל העוסקים בתעשיית הסמיקונדקטור  כולל מהנדסים, מומחים מקצועיים ובכירים. מועד מדויק יתפרסם סמוך למועד הכנס

          לחץ לפרטים

          הרשמה לניוזלטר של ChiPortal

          הצטרפו לרשימת הדיוור שלנו


            • פרסם אצלנו
            • עיקר החדשות
            • הצטרפות לניוזלטר
            • בישראל
            • צור קשר
            • צ’יפסים
            • Chiportal Index
            • TapeOut Magazine
            • אודות
            • מאמרים ומחקרים
            • תנאי שימוש
            • כנסים
            • אוטומוטיב
            • בינה מלאכותית
            • בטחון, תעופה וחלל
            • ‫טכנולוגיות ירוקות‬
            • ‫יצור (‪(FABs‬‬
            • ‫צב”ד‬
            • ‫רכיבים‬ (IOT)
            • ‫שבבים‬
            • ‫תוכנות משובצות‬
            • ‫תכנון אלק’ (‪(EDA‬‬
            • ‫‪FPGA‬‬
            • ‫ ‪וזכרונות IPs‬‬

            השותפים שלנו

            כל הזכויות שמורות Chiportal (c) 2010 תנאי שימוש ומדיניות פרטיותדרונט בניית אתרים

            No Result
            View All Result
            • עיקר החדשות
            • בישראל
            • מדורים
              • אוטומוטיב
              • בינה מלאכותית (AI/ML)
              • בטחון, תעופה וחלל
              • ‫טכנולוגיות ירוקות‬
              • ‫יצור (‪(FABs‬‬
              • ‫צב”ד‬
              • ‫שבבים‬
              • ‫רכיבים‬ (IoT)
              • ‫תוכנות משובצות‬
              • ‫תכנון אלק’ (‪(EDA‬‬
              • ‫‪FPGA‬‬
              • ‫ ‪וזכרונות IPs‬‬
              • תקשורת מהירה
            • מאמרים ומחקרים
            • צ’יפסים
            • כנסים
            • Chiportal Index
              • אינדקס חברות – קטגוריות
              • אינדקס חברות A-Z
            • אודות
            • הצטרפות לניוזלטר
            • TapeOut Magazine
            • צור קשר
            • ChipEx
            • סיליקון קלאב

            כל הזכויות שמורות Chiportal (c) 2010 תנאי שימוש ומדיניות פרטיותדרונט בניית אתרים

            דילוג לתוכן
            פתח סרגל נגישות

            כלי נגישות

            • הגדל טקסט
            • הקטן טקסט
            • גווני אפור
            • ניגודיות גבוהה
            • ניגודיות הפוכה
            • רקע בהיר
            • הדגשת קישורים
            • פונט קריא
            • איפוס