Intel Keynote για επίσημο φορείο μυαλού

Η Synopsys δημοσίευσε στον ιστότοπο SolvNet μια συναρπαστική ομιλία του Δρ. Theo Drane της Intel Graphics. Το θέμα είναι ο έλεγχος ισοδυναμίας διαδρομής δεδομένων. Μπορεί να ακούγεται σαν μια ακόμη επίσημη έγκριση του Synopsys VC Formal DPV, αλλά θα πρέπει να το παρακολουθήσετε ούτως ή άλλως. Αυτή είναι μια συζήτηση που διευρύνει το μυαλό σχετικά με τις χρήσεις και τις εκτιμήσεις στην επίσημη, η οποία θα σας οδηγήσει πέρα ​​από το συνηθισμένο είδος του οδηγού χρήστη σε πιο συναρπαστικό έδαφος.

Διανοητική κατανόηση έναντι δειγματοληπτικής δοκιμής

Η δοκιμαστική προσομοίωση σε όλες τις μορφές της είναι εξαιρετική και συχνά αναντικατάστατη για την επαλήθευση της ορθότητας μιας προδιαγραφής σχεδιασμού ή υλοποίησης. Είναι επίσης εύκολο να ξεκινήσετε. Απλώς γράψτε ένα δοκιμαστικό πρόγραμμα και ξεκινήστε την προσομοίωση. Αλλά η άλλη πλευρά αυτής της απλότητας είναι ότι δεν χρειάζεται πλήρως καταλάβετε τι δοκιμάζουμε για να ξεκινήσετε. Πείθουμε τους εαυτούς μας ότι έχουμε διαβάσει προσεκτικά τις προδιαγραφές και κατανοούμε όλες τις γωνιακές περιπτώσεις, αλλά δεν χρειάζεται μεγάλη πολυπλοκότητα για να κατακλύσει την κατανόησή μας.

Το Formal σάς ενθαρρύνει να κατανοήσετε τη λειτουργικότητα σε βαθύ επίπεδο (τουλάχιστον εάν θέλετε να προσφέρετε ένα πολύτιμο αποτέλεσμα). Στο παραπάνω παράδειγμα, μια απλή ερώτηση – μπορεί το z να είναι και το 1 – αποτυγχάνει να δείξει ένα παράδειγμα σε ένα δισεκατομμύριο κύκλους σε έναν προσομοιωτή. Δεν αποτελεί έκπληξη, καθώς πρόκειται για μια ακραία γωνιακή περίπτωση. Ένα επίσημο τεστ παρέχει ένα συγκεκριμένο και πολύ μη προφανές παράδειγμα σε 188 δευτερόλεπτα και μπορεί να αποδείξει ότι αυτή είναι η μόνη τέτοια περίπτωση σε λίγο λιγότερο χρόνο.

Το OK formal έκανε αυτό που δεν μπορούσε να κάνει η δυναμική δοκιμή, αλλά το πιο σημαντικό, μάθατε κάτι που ο προσομοιωτής μπορεί να μην σας είχε πει ποτέ. Ότι υπήρχε μόνο μία πιθανή περίπτωση στην οποία θα μπορούσε να συμβεί αυτή η κατάσταση. Το Formal σάς βοήθησε να κατανοήσετε καλύτερα το σχέδιο σε πνευματικό επίπεδο, όχι απλώς ως πιθανολογική περίληψη σε ένα πεπερασμένο σύνολο δοκιμαστικών περιπτώσεων.

Θέματα προδιαγραφών

Το επόμενο παράδειγμα του Theo βασίζεται σε ένα μηχάνημα αυτόματης πώλησης σφαλμάτων (ονομάζεται έτσι επειδή όταν πατάτε ένα κουμπί εμφανίζεται ένα σφάλμα). Αυτό μοιάζει με ένα αρκετά απλό πρόβλημα ελέγχου ισοδυναμίας C σε RTL, μοντέλο C στα αριστερά, μοντέλο RTL στα δεξιά. Μια έκπληξη για τον Theo στις πρώτες μέρες του στα επίσημα ήταν ότι η συμπεριφορά στη δεξιά μετατόπιση στο μοντέλο C δεν ορίζεται πλήρως στο πρότυπο C, παρόλο που το gcc θα συμπεριφέρεται εύλογα. Ωστόσο, η DPV θα παραπονεθεί για μια αναντιστοιχία σε σύγκριση με το RTL, όπως θα έπρεπε. Η απροσδιόριστη συμπεριφορά είναι ένα επικίνδυνο πράγμα στο οποίο πρέπει να βασιστείς.

Η σύγκριση προδιαγραφών μεταξύ C και RTL συνοδεύεται από άλλους κινδύνους, ειδικά γύρω από τα πλάτη bit. Η περικοπή ή η απώλεια ενός bit μεταφοράς σε ένα ενδιάμεσο σήμα (#3 παραπάνω) είναι καλά παραδείγματα. Είναι αυτά θέματα προδιαγραφών; Ίσως μια γκρίζα περιοχή μεταξύ των επιλογών προδιαγραφών και υλοποίησης.

Πέρα από τον έλεγχο ισοδυναμίας

Ο πρωταρχικός σκοπός του DPV, φαίνεται, είναι να ελέγξει την ισοδυναμία μεταξύ μιας αναφοράς C ή RTL και μιας υλοποίησης RTL. Αλλά αυτή η ανάγκη είναι σχετικά σπάνια και υπάρχουν άλλοι χρήσιμοι τρόποι να εφαρμοστεί μια τέτοια τεχνολογία, αν είναι λίγο έξω από το κουτί. Πρώτα ένα κλασικό στον κόσμο της υλοποίησης – έκανα μια αλλαγή, διόρθωσα ένα σφάλμα – εισήγαγα κάποια νέα σφάλματα ως αποτέλεσμα; Λίγο σαν τον έλεγχο SEQ αφού προσθέσετε το clock gating. Η ανάλυση προσβασιμότητας στις εξόδους μπλοκ μπορεί να είναι μια άλλη χρήσιμη εφαρμογή σε ορισμένες περιπτώσεις.

Ο Theo γίνεται ακόμα πιο δημιουργικός, ζητώντας από τους εκπαιδευόμενους να χρησιμοποιήσουν αντίθετα παραδείγματα για να κατανοήσουν καλύτερα το σχέδιο, λύστε το Sudoku or παραγοντοποίηση ακεραίων. Αναγνωρίζει ότι το DPV είναι ένας περίεργος τρόπος προσέγγισης τέτοιων προβλημάτων, αλλά επισημαίνει ότι πρόθεσή του είναι να σπάσει την ψευδαίσθηση ότι το DPV είναι μόνο για έλεγχο ισοδυναμίας. Ενδιαφέρουσα ιδέα και σίγουρα κουραστική σκέψη για να σκεφτείς τέτοιες προκλήσεις. (Ομολογώ ότι άρχισα αμέσως να σκέφτομαι το πρόβλημα του Sudoku μόλις το ανέφερε.)

Τύλιξε

Ο Theo ολοκληρώνει με μια συζήτηση σχετικά με μεθοδολογίες που είναι σημαντικές στη χρήση της παραγωγής, γύρω από περιορισμούς, παλινδρομήσεις και συγκρίσεις με παλαιού τύπου μοντέλα RTL. Επίσης, οι προκλήσεις στο να γνωρίζετε εάν αυτό που ελέγχετε ταιριάζει πραγματικά με τις προδιαγραφές φυσικής γλώσσας ανώτατου επιπέδου.

Πολύ δυναμωτική συζήτηση, αξίζει να την παρακολουθήσετε εδώ στο SolvNet!

Μοιραστείτε αυτήν την ανάρτηση μέσω:

• SEO Powered Content & PR Distribution. Ενισχύστε σήμερα.
• Platoblockchain. Web3 Metaverse Intelligence. Ενισχύθηκε η γνώση. Πρόσβαση εδώ.
• πηγή: https://semiwiki.com/eda/325878-intel-keynote-on-formal-a-mind-stretcher/