คำปราศรัยของ Intel เรื่อง Mind-Stretcher

Synopsys ได้โพสต์บนเว็บไซต์ SolvNet เกี่ยวกับการพูดคุยที่น่าสนใจโดย Dr. Theo Drane จาก Intel Graphics หัวข้อคือการตรวจสอบความเทียบเท่าของดาต้าพาธ อาจฟังดูเหมือนเป็นการรับรอง DPV อย่างเป็นทางการของ Synopsys VC อีกครั้ง แต่คุณควรดูต่อไป นี่คือการสนทนาที่ขยายความคิดเกี่ยวกับการใช้และการพิจารณาอย่างเป็นทางการ ซึ่งจะนำคุณไปไกลกว่าการแนะนำผู้ใช้ตามปกติ ไปสู่ขอบเขตที่น่าสนใจยิ่งขึ้น

ความเข้าใจทางปัญญากับการทดสอบตัวอย่าง

การจำลองที่ขับเคลื่อนด้วยการทดสอบในทุกรูปแบบนั้นยอดเยี่ยมและมักจะไม่สามารถทดแทนได้ในการตรวจสอบความถูกต้องของข้อกำหนดการออกแบบหรือการนำไปปฏิบัติ นอกจากนี้ยังง่ายต่อการเริ่มต้น เพียงเขียนโปรแกรมทดสอบและเริ่มจำลอง แต่ด้านกลับของความเรียบง่ายนั้นก็คือเราไม่จำเป็นต้องทำ อย่างเต็มที่ ทำความเข้าใจสิ่งที่เรากำลังทดสอบเพื่อเริ่มต้น เราโน้มน้าวตัวเองว่าเราได้อ่านข้อมูลจำเพาะอย่างละเอียดและเข้าใจทุกกรณี แต่ก็ไม่ต้องใช้ความซับซ้อนมากนักในการครอบงำความเข้าใจของเรา

เป็นทางการสนับสนุนให้คุณเข้าใจฟังก์ชันการทำงานในระดับลึก (อย่างน้อยก็ถ้าคุณต้องการให้ผลลัพธ์ที่มีคุณค่า) ในตัวอย่างข้างต้น คำถามง่ายๆ - สามารถเป็น 1 ทั้งหมดได้หรือไม่ - ไม่สามารถแสดงตัวอย่างในรอบพันล้านรอบบนเครื่องจำลอง ไม่น่าแปลกใจเนื่องจากนี่เป็นกรณีมุมที่รุนแรง การทดสอบอย่างเป็นทางการจะให้ตัวอย่างที่เจาะจงและไม่ชัดเจนภายใน 188 วินาที และสามารถพิสูจน์ได้ว่านี่เป็นกรณีเดียวเท่านั้นโดยใช้เวลาน้อยกว่าเล็กน้อย

ตกลง อย่างเป็นทางการได้ทำสิ่งที่การทดสอบแบบไดนามิกไม่สามารถทำได้ แต่ที่สำคัญกว่านั้นคือคุณได้เรียนรู้บางสิ่งที่เครื่องจำลองอาจไม่เคยบอกคุณ มีเพียงกรณีเดียวที่เป็นไปได้ที่เงื่อนไขนั้นจะเกิดขึ้น รูปแบบทางการช่วยให้คุณเข้าใจการออกแบบได้ดีขึ้นในระดับสติปัญญา ไม่ใช่แค่สรุปความน่าจะเป็นในชุดทดสอบที่มีจำกัด

ประเด็นเฉพาะ

ตัวอย่างถัดไปของ Theo อิงจากตู้จำหน่ายแมลงอัตโนมัติ (เรียกเช่นนี้เพราะเมื่อคุณกดปุ่ม คุณจะได้รับแมลง) ดูเหมือนว่าปัญหาการตรวจสอบความเท่าเทียมกันของ C ถึง RTL ที่ค่อนข้างตรงไปตรงมา โมเดล C ทางด้านซ้าย โมเดล RTL ทางด้านขวา สิ่งที่น่าประหลาดใจอย่างหนึ่งสำหรับ Theo ในช่วงแรกๆ ที่เป็นทางการก็คือพฤติกรรมการเลื่อนขวาในโมเดล C ไม่ได้ถูกกำหนดไว้อย่างสมบูรณ์ในมาตรฐาน C แม้ว่า gcc จะทำงานอย่างสมเหตุสมผลก็ตาม อย่างไรก็ตาม DPV จะบ่นเกี่ยวกับความไม่ตรงกันเมื่อเปรียบเทียบกับ RTL ตามที่ควร พฤติกรรมที่ไม่ได้กำหนดไว้เป็นสิ่งที่อันตรายที่ต้องพึ่งพา

การเปรียบเทียบข้อมูลจำเพาะระหว่าง C และ RTL มาพร้อมกับอันตรายอื่นๆ โดยเฉพาะความกว้างของบิต การตัดทอนหรือการสูญเสียแครี่บิตในสัญญาณระดับกลาง (#3 ด้านบน) เป็นตัวอย่างที่ดี สิ่งเหล่านี้เป็นปัญหาสเป็คหรือไม่? อาจเป็นพื้นที่สีเทาระหว่างตัวเลือกข้อมูลจำเพาะและการใช้งาน

นอกเหนือจากการตรวจสอบความเท่าเทียมกัน

ดูเหมือนว่าวัตถุประสงค์หลักของ DPV คือการตรวจสอบความเท่าเทียมกันระหว่างการอ้างอิง C หรือ RTL และการนำ RTL ไปใช้ แต่ความต้องการดังกล่าวมีไม่บ่อยนัก และมีวิธีอื่นๆ ที่มีประโยชน์ที่อาจนำเทคโนโลยีดังกล่าวไปประยุกต์ใช้ หากเป็นความต้องการนอกกรอบเล็กน้อย สิ่งแรกสุดคลาสสิกในโลกแห่งการใช้งาน – ฉันทำการเปลี่ยนแปลง แก้ไขข้อบกพร่อง – ฉันแนะนำข้อบกพร่องใหม่ ๆ หรือไม่? เหมือนกับการตรวจสอบ SEQ หลังจากที่คุณเพิ่ม clock gating การวิเคราะห์ความสามารถในการเข้าถึงในเอาท์พุตแบบบล็อกอาจเป็นอีกแอปพลิเคชันที่มีประโยชน์ในบางกรณี

Theo มีความคิดสร้างสรรค์มากขึ้น โดยขอให้ผู้เข้ารับการฝึกอบรมใช้ตัวอย่างโต้แย้งเพื่อทำความเข้าใจการออกแบบให้ดียิ่งขึ้น แก้ซูโดกุ or แยกตัวประกอบจำนวนเต็ม. เขารับทราบว่า DPV เป็นวิธีที่แปลกในการแก้ไขปัญหาดังกล่าว แต่ชี้ให้เห็นว่าเจตนาของเขาคือการทำลายภาพลวงตาที่ว่า DPV มีไว้เพื่อการตรวจสอบความเท่าเทียมกันเท่านั้น ความคิดที่น่าสนใจและต้องใช้สมองในการคิดผ่านความท้าทายดังกล่าว (ฉันสารภาพว่าฉันเริ่มคิดถึงปัญหา Sudoku ทันทีที่เขาพูดถึง)

ห่อ

Theo ปิดท้ายด้วยการอภิปรายเกี่ยวกับวิธีการที่สำคัญในการใช้งานจริง เกี่ยวกับข้อจำกัด การถดถอย และการเปรียบเทียบกับโมเดล RTL รุ่นเก่า ความท้าทายในการทราบว่าสิ่งที่คุณกำลังตรวจสอบนั้นตรงกับข้อกำหนดภาษาธรรมชาติระดับบนสุดหรือไม่

บรรยายได้เร้าใจมาก น่าติดตามครับ ที่นี่บน SolvNet!

แชร์โพสต์นี้ผ่าน:

• เนื้อหาที่ขับเคลื่อนด้วย SEO และการเผยแพร่ประชาสัมพันธ์ รับการขยายวันนี้
• เพลโตบล็อคเชน Web3 Metaverse ข่าวกรอง ขยายความรู้. เข้าถึงได้ที่นี่.
• ที่มา: https://semiwiki.com/eda/325878-intel-keynote-on-formal-a-mind-stretcher/