Formal methods for test and reliability

Abstract

In the rapidly evolving landscape of nanotechnology, where innovations promise groundbreaking advancements in various industries, ensuring the reliability and safety of digital circuits becomes paramount. While applicable to the broad category of commercial off-the-shelf products, this becomes significantly more evident when examining domains or industry sectors, such as automotive, aviation, railways, and the biomedical sector, that fall into the category of safety-critical applications. In these cases, the probability that a fault may activate an error and propagate to a failure that would endanger human lives or cause environmental damage should be carefully evaluated and kept under predefined thresholds. To achieve this result, the manufacturers must comply with strict safety standards and procedures that mandate rigorous coverage thresholds and comprehensive testing protocols. From end-of-manufacturing up until the in-field phase, each integrated circuit (IC) is subjected to several testing procedures to ensure that it meets stringent quality standards, functions reliably within specified parameters, and remains resilient to various environmental conditions throughout its operational lifespan. Design-for-testability (DfT) techniques are incorporated during the design phases of electronic circuits to enhance the testing process. However, despite the presence of powerful electronic design automation (EDA) utilities, such as automatic test pattern generation (ATPG) tools, intended for use alongside DfT-compliant designs during testing, the relentless evolution of technology brings about faster, smaller, and denser circuits. This evolution renders certain utilities inadequate as the complexity of the test procedure significantly increases, as seen with Burn-In (BI) test. Burn-In, an omnipresent step in the test chain for products intended for use in safety-critical domains, was, until recently, conducted in its traditional static format. Notwithstanding its effectiveness, static BI test became less effective for newer, denser technologies as in its static form it was found not to fully exercise all internal parts of the ICs. Hence, it evolved into new dynamic forms, where stress stimuli are applied in an internal manner on top of the external temperature and voltage increase. However, the generation of appropriate stress-inducing stimuli is a costly and arduous task for the test engineers, due to the lack of automation to aid the generation process. Another test domain that could substantially benefit from automation is the in-field test. Continuous in-field testing enables the detection of faults or anomalies that may occur over time. Early detection of potential issues allows for proactive maintenance or corrective measures, reducing the risk of system failures in critical situations. However, the task of developing appropriate software test libraries (STLs) for such scenarios is typically a task that requires a lot of manual effort from the perspective of the test engineer. In fact, not only the test must consider parameters such as application time and memory footprint but it must also avoid targeting untestable faults of the design. This means that the test should only focus on those faults that are able to produce a failure in the operating scenario, ignoring those that can not produce any (critical) failure. This PhD thesis proposes solutions, based on Formal Methods (FMs), addressing the aforementioned test topics. The manuscript is organized in three main parts. The initial part provides an introduction and overview of the imperative need for testing and reliability in the modern digital era. It delves into the distinct testing areas that form the focus of this thesis. The second part includes the three main contributions of the thesis. A section proposing FM-based solutions for dynamic BI test stress stimuli generation is first presented. These methods consider various switching activity metrics, and their effectiveness is showcased by applying them on scalar pipelined processors. The second contribution regards FM-based solutions targeting the identification of functionally untestable faults under the stuck-at and the cell-aware fault models. Lastly, the final contribution regards methodologies that aid the generation of STLs for microprocessors and GPUs. The last part provides the conclusions of the overall work.

Στο ταχέως εξελισσόμενο τοπίο της νανοτεχνολογίας, όπου οι καινοτομίες υπόσχονται πρωτοποριακές εξελίξεις σε διάφορους κλάδους, η διασφάλιση της αξιοπιστίας και της ασφάλειας των ψηφιακών κυκλωμάτων καθίσταται υψίστης σημασίας. Αν και αυτό ισχύει για την ευρεία κατηγορία των εμπορικών έτοιμων προϊόντων, γίνεται σημαντικά πιο εμφανές όταν εξετάζονται τομείς ή βιομηχανικοί κλάδοι, όπως η αυτοκινητοβιομηχανία, η αεροπορία, οι σιδηρόδρομοι και ο βιοϊατρικός τομέας, που εμπίπτουν στην κατηγορία των κρίσιμων για την ασφάλεια εφαρμογών. Σε αυτές τις περιπτώσεις, η πιθανότητα ένα σφάλμα να ενεργοποιηθεί και να μεταδοθεί σε αστοχία που θα έθετε σε κίνδυνο ανθρώπινες ζωές ή θα προκαλούσε περιβαλλοντική ζημία θα πρέπει να αξιολογείται προσεκτικά και να διατηρείται κάτω από προκαθορισμένα όρια. Για να επιτευχθεί αυτό το αποτέλεσμα, οι κατασκευαστές πρέπει να συμμορφώνονται με αυστηρά πρότυπα και διαδικασίες ασφαλείας που επιβάλλουν αυστηρά όρια κάλυψης και ολοκληρωμένα πρωτόκολλα δοκιμών. Από το τέλος της κατασκευής έως και τη φάση της εγκατάστασης στο πεδίο, κάθε ολοκληρωμένο κύκλωμα (IC) υποβάλλεται σε διάφορες διαδικασίες δοκιμών για να διασφαλιστεί ότι πληροί αυστηρά πρότυπα ποιότητας, λειτουργεί αξιόπιστα εντός καθορισμένων παραμέτρων και παραμένει ανθεκτικό σε διάφορες περιβαλλοντικές συνθήκες καθ' όλη τη διάρκεια της λειτουργικής του ζωής. Οι τεχνικές Design-for-Testability (DfT) ενσωματώνονται κατά τις φάσεις σχεδιασμού των ηλεκτρονικών κυκλωμάτων για τη βελτίωση της διαδικασίας δοκιμής.Ωστόσο, παρά την παρουσία ισχυρών βοηθητικών προγραμμάτων αυτοματοποίησης ηλεκτρονικού σχεδιασμού (EDA), όπως τα automatic test pattern generation (ATPG) εργαλεία, που προορίζονται για χρήση παράλληλα με κυκλώματα συμβατά με DfT κατά τη διάρκεια των δοκιμών, η αδιάκοπη εξέλιξη της τεχνολογίας επιφέρει ταχύτερα, μικρότερα και πυκνότερα κυκλώματα. Αυτή η εξέλιξη καθιστά ορισμένα βοηθητικά προγράμματα ανεπαρκή, καθώς η πολυπλοκότητα της διαδικασίας δοκιμής αυξάνεται σημαντικά, όπως συμβαίνει με το Burn-In (BI) τέστ. Το Burn-In, ένα πανταχού παρόν βήμα στην αλυσίδα δοκιμών για προϊόντα που προορίζονται για χρήση σε κρίσιμους τομείς ασφαλείας, διεξαγόταν, μέχρι πρόσφατα, με την παραδοσιακή στατική μορφή του. Παρά την αποτελεσματικότητά της, η στατική δοκιμή BI κατέστη λιγότερο αποτελεσματική για τις νεότερες, πυκνότερες τεχνολογίες, καθώς διαπιστώθηκε ότι στη στατική της μορφή δεν εξασκούσε πλήρως όλα τα εσωτερικά μέρη των ολοκληρωμένων κυκλωμάτων. Ως εκ τούτου, εξελίχθηκε σε νέες δυναμικές μορφές, όπου τα διανύσματα καταπόνησης εφαρμόζονται με εσωτερικό τρόπο επιπλέον της εξωτερικής αύξησης της θερμοκρασίας και της τάσης. Ωστόσο, η δημιουργία κατάλληλου κώδικα που προκαλεί καταπόνηση είναι μια δαπανηρή και επίπονη εργασία για τους μηχανικούς, λόγω της έλλειψης αυτοματισμού που θα βοηθούσε τη διαδικασία της δημιουργίας τους. Ένας άλλος τομέας που θα μπορούσε να επωφεληθεί σημαντικά από την αυτοματοποίηση είναι το in-field τεστ. Το in-field τέστ επιτρέπει την ανίχνευση σφαλμάτων ή ανωμαλιών που μπορεί να εμφανιστούν με την πάροδο του χρόνου. Η έγκαιρη ανίχνευση πιθανών προβλημάτων επιτρέπει την προληπτική συντήρηση ή τη λήψη διορθωτικών μέτρων, μειώνοντας τον κίνδυνο αποτυχίας του συστήματος σε κρίσιμες καταστάσεις. Ωστόσο, το έργο της ανάπτυξης κατάλληλων βιβλιοθηκών, Software Test Libraries (STL), για τέτοια σενάρια είναι συνήθως ένα έργο που απαιτεί μεγάλη χειρωνακτική προσπάθεια από την πλευρά του μηχανικού. Στην πραγματικότητα, όχι μόνο το τέστ πρέπει να λαμβάνει υπόψη παραμέτρους όπως ο χρόνος εφαρμογής και το αποτύπωμα μνήμης, αλλά και να αποφεύγει τη στόχευση σε μη ελέγξιμα σφάλματα του σχεδιασμού. Αυτό σημαίνει ότι η δοκιμή πρέπει να εστιάζει μόνο σε εκείνα τα σφάλματα που είναι σε θέση να προκαλέσουν αποτυχία στο σενάριο λειτουργίας, αγνοώντας εκείνα που δεν μπορούν να προκαλέσουν καμία (κρίσιμη) αποτυχία. Η παρούσα διδακτορική διατριβή προτείνει λύσεις, βασισμένες σε Τυπικές Μεθόδους, Formal Methods (FM), που αντιμετωπίζουν τα προαναφερθέντα θέματα δοκιμών. Το χειρόγραφο οργανώνεται σε τρία κύρια μέρη. Το αρχικό μέρος παρέχει μια εισαγωγή και επισκόπηση της επιτακτικής ανάγκης για δοκιμές και αξιοπιστία στη σύγχρονη ψηφιακή εποχή. Εμβαθύνει στους διακριτούς τομείς δοκιμών που αποτελούν το επίκεντρο της παρούσας διατριβής. Το δεύτερο μέρος περιλαμβάνει τις τρεις κύριες συνεισφορές της διατριβής. Αρχικά παρουσιάζεται μια ενότητα που προτείνει λύσεις βασισμένες στις FM για τη δημιουργία δυναμικών διανυσμάτων καταπόνησης που προορίζονται για το BI. Αυτές οι μέθοδοι εξετάζουν διάφορες μετρικές μεταγωγικής δραστηριότητας και η αποτελεσματικότητά τους παρουσιάζεται με την εφαρμογή τους σε κλιμακωτούς επεξεργαστές. Η δεύτερη συνεισφορά αφορά λύσεις βασισμένες σε FM που στοχεύουν στον εντοπισμό λειτουργικά μη ελέγξιμων σφαλμάτων σύμφωνα με τα μοντέλα σφαλμάτων stuck-at και cell-aware. Τέλος, η τελευταία συνεισφορά αφορά μεθοδολογίες που βοηθούν στη δημιουργία STL για μικροεπεξεργαστές και GPUs. Στο τελευταίο μέρος παρατίθενται τα συμπεράσματα της συνολικής εργασίας.