Kiểm chứng khối điều khiển bus Amba AHB.

- 10 - 1.1) Vai trò của kiểm chứng trong thiết kế vi mạch.
- 10 - 1.2) Phân loại lỗi và các loại kiểm chứng vi mạch.
- 13 - 1.4) Vị trí kiểm chứng vi mạch trong quy trình thiết kế vi mạch.
- 15 - 1.5) Nguyên tắc cơ bản của kiểm chứng vi mạch.
- 20 - 2.2) Khái niệm cơ bản của kiểm chứng hình thức.
- Kiểm chứng mô hình và tính toán biểu tượng.
- Kiểm chứng mô hình giới hạn (Bounded Model Checking.
- Kiểm chứng thuộc tính khoảng (Interval Property Checking.
- 68 - 4.6) Kết quả kiểm chứng các assertion trên phần mềm ONESPIN.
- 5 - Danh mục các kỹ hiệu và chữ viết tắt AHB AMBA High-performance Bus Nâng cao hiệu quả Bus AMBA AMBA Advanced Microcontroller Bus Architecture Kiến trúc Bus vi điều khiển tiên tiến APB Advanced Peripheral Bus Nâng cao Bus giao điện ASB Advanced System Bus Nâng cao Bus hệ thống AVB Assertion Based Verification Kiểm chứng dựa trên khẳng định BDD Binary Decision Diagram Biểu đồ quyết định nhị phân BMC Bounded Model Checking Kiểm tra mô hình giới hạn CNF Conjuntion Normal Form Dạng chuẩn hội CTL Computation tree logic Logic cây tính toán FSM Finite State Machine Máy trạng thái hữu hạn FV Formal Verification Kiểm chứng hình thức HDL Hardware Description Language Ngôn ngữ mô tả phần cứng IC Integrated Circuit Vi mạch tích hợp IPC Interval Property Checking Kiểm tra thuộc tính khoảng LTL Linear temporal logic Logic thời gian tuyến tính RTL Register Transfer Level Mức dịch chuyển thanh ghi SAT Satisfiability Thuật toán SAT SoC System on Chip Hệ thống trên chip VLSI Very-large-scale Integration Vi mạch tích hợp rất lớn STG State Transition Graph Đồ thị chuyển trạng thái SMC Symbolic Model Checking Kiểm tra mô hình biểu tượng SVA System Verilog Assertion Ngôn ngữ SVA VIP Verification Intellectual Property Sở hữu trí tuệ kiểm chứng - 6 - Danh mục các bảng Bảng 1.1 Phân bổ lỗi trong chip Pentium 4.
- 8 Kết quả kiểm chứng các assertion trên phần mềm ONESPIN.
- 71 - Danh mục hình vẽ Hình 1.1 Khoảng cách giữa năng suất sản và năng suất thiết kế vi mạch.
- 11 - Hình 1.2 Giá thành thiết kế hệ thống trên chip.
- 12 - Hình 1.3 Phân bổ các loại lỗi trong vi mạch.
- 13 - Hình 1.4 Phân bổ lỗi trong chip Pentium 4.
- 14 - Hình 1.5 Các loại kiểm chứng khác nhau và phân bổ công sức khi kiểm chứng - 15 - Hình 1.6 Bậc thang độ trừu tượng của thiết kế.
- 16 - Hình 1.7 Quan hệ giữa quá trình thiết kế và quá trình kiểm chứng.
- 17 - Hình 1.8 Nguyên tắc cơ bản của kiểm chứng.
- 19 - Hình 2.1 Các yếu tố của kiểm chứng hình thức.
- 21 - Hình 2.2 Ví dụ về BDD.
- 23 - Hình 2.4 Hai BDD (A,B) của cùng một hàm.
- 7 - Hình 2.5 Ví dụ về mạch tổ hợp.
- 26 - Hình 2.6 Ví dụ về gate-net-list.
- 27 - Hình 2.8 Component–net-list.
- 27 - Hình 2.9 Cấu trúc của mạch tuần tự đồng bộ.
- 29 - Hình 2.10 Mô hình mạch trải.
- 29 - Hình 2.11 Ý nghĩa các toán tử LTL.
- 32 - Hình 2.12 Các khối của assertion.
- 36 - Hình 2.13 Ví dụ về sequence.
- 36 - Hình 2.14 Ví dụ về toán tử lặp.
- 37 - Hình 2.15 Mô hình mạch trải.
- 42 - Hình 2.16 Mô hình mạch dùng trong IPC.
- 44 - Hình 3.1 Sơ đồ tổng quát cấu trúc của chuẩn giao tiếp AMBA.
- 49 - Hình 3.3 Các giao diện của AHB bus master.
- 49 - Hình 3.4 Quá trình chuyển giao cơ bản.
- 50 - Hình 3.5 Ví dụ về các kiểu chuyển giao.
- 52 - Hình 3.6 Four-beat wrapping burst.
- 53 - Hình 3.7 Four-beat incrementing burst.
- 53 - Hình 3.8 Eight-beat wrapping burst.
- 54 - Hình 3.9 Error response.
- 55 - Hình 3.10 Transfer with retry response.
- 55 - Hình 4.1 Một phần của máy ghi cho giao thức AHB.
- 60 - Hình 4.2 FST của Wrap4 burst operation.
- 63 - Hình 4.3 Giao diện chính của chương trình.
- 64 - Hình 4.4 Hộp thoại Read VHDL.
- 64 - Hình 4.5 Hộp thoại Elaborate.
- 65 - Hình 4.6 Chế độ MV.
- 65 - Hình 4.7 Hộp thoại Manage Assertions.
- 66 - Hình 4.8 Thiết kế không thoả mãn thuộc tính.
- 66 - Hình 4.9 Màn hình debug giúp tìm lỗi.
- 67 - Hình 4.10 Thiết kế thoả mãn thuộc tính.
- 8 - MỞ ĐẦU Hiện nay, kiểm chứng thiết kế phần cứng IC (IC hardware design verification) là trở ngại chính và chiếm nhiều công sức nhất trong quá trình thiết kế và chế tạo IC.
- Kiểm chứng chiếm tới 70% giá thành và công sức thiết kế phần cứng IC và chiếm tới 40% giá thành thiết kế hệ thống điện tử gồm phần cứng IC và phần mềm [nguồn: Internation Technology Roadmap for Semicoductors 2009].
- Vì vậy, các giải pháp công nghệ nhằm nâng cao chất lượng, tăng năng suất và giảm giá thành kiểm chứng IC đang là trọng tâm nghiên cứu, phát triển của các trường đại học, trung tâm nghiên cứu và các công ty thiết kế sản xuất IC trên thế giới [nguồn: IBM, Intel websites].
- Thị trường kiểm chứng thiết kế IC còn là một thị trường khá mới mẻ, chưa phát triển như thị trường thiết kế IC.
- Trên thế giới, hiện chỉ có một vài công ty lớn cung cấp các nhân IP kiểm chứng (Verification IP) tiêu chuẩn.
- Ở Việt Nam, thị trường này hoàn toàn để ngỏ, các nhóm thiết kế, phát triển IC thường tự kiểm chứng thiết kế của mình bằng phương pháp thủ công, năng suất thấp.
- Tuy nhiên, để phát triển được ngành công nghiệp thiết kế IC của Việt Nam, việc phát triển các nhân IP kiểm chứng cũng quan trọng như việc thiết kế ra các nhân IP chức năng.
- Hiểu được tầm quan trọng của kiểm chứng trong quá trình thiết kế vi mạch, em quyết định làm luận văn liên quan đến lĩnh vực này và cụ thể là là phát triển một lõi IP kiểm chứng bộ điều khiển AHB Master.
- Kỹ thuật kiểm tra thuộc tính khoảng được sử dụng để kiểm chứng các hoạt động của một bộ điểu khiển AHB Master mã nguồn mở tuân theo các đặc điểm kỹ thuật tiêu chuẩn.
- Luận văn này gồm 4 chương với cấu trúc như sau: Chương 1: Giới thiệu tổng quan về kiểm chứng vi mạch.
- Chương này cho ta biết về quá trình thiết kế mạch số, vai trò và vị trí của kiểm tra chức năng trong quá - 9 - trình đó.
- Chương 2: Giới thiệu về kiểm chứng hình thức.
- Chương này sẽ đề cập đến các khái niệm cơ bản của kiểm chứng hình thức, cách mô hình hoá một mạch số thành các mô hình toán học, các ngôn ngữ được sử dụng để mô tả thuộc tính và các phương pháp để chứng minh.
- Chương này giới thiệu các chỉ tiêu kỹ thuật của AMBA AHB và khối AHB Master Chương 4: Xây dựng FST cho WRAP4 và kiểm chứng trên phần mềm Onespin.
- Đưa ra các bước để triển khai nhân kiểm chứng, công cụ được sử dụng để kiểm chứng và các kết quả đạt được.
- 10 - Chương 1 - GIỚI THIỆU KIỂM CHỨNG VI MẠCH 1.1) Vai trò của kiểm chứng trong thiết kế vi mạch Để có thể thiết kế được các mạch tích hợp có độ phức tạp lớn một yêu cầu tiên quyết là các nhà khoa học phải làm chủ được các công nghệ nền tảng về tổng hợp, tối ưu và kiểm tra tự động phần cứng số.
- Sử dụng các phần mềm thiết kế, kiểm tra tự động như vậy cho phép giải quyết hai vấn đề cơ bản trong thiết kế chế tạo mạch tích hợp đó là năng suất thiết kế và chất lượng vi mạch.
- Vì vậy, việc kiểm tra thiết kế phần cứng của vi mạch luôn là một vấn đề nóng trong lĩnh vực chế tạo thiết bị điện tử.
- Để thiết kế và kiểm tra chất lượng các vi mạch, các hãng chế tạo lớn sử dụng các bộ công cụ thiết kế, kiểm tra rất phức tạp có giá thành rất cao.
- Ví dụ như phần mềm thiết kế và kiểm tra của hãng Cadence hay Synopsys có giá lên đến hàng trăm nghìn USD cho một năm sử dụng.
- Trong lĩnh vực thiết kế vi mạch, nghiên cứu phát triển các giải pháp, các thuật toán cho phép tự động tổng hợp và kiểm tra thiết kế vi mạch luôn là một chủ đề nghiên cứu nóng đòi hỏi có các ý tưởng và phát minh mới vì ngành công nghiệp vi - 11 - mạch đang và sẽ tiếp tục phải đối mặt với một thách thức lớn về khoảng cách giữa khả năng (về năng suất) sản xuất và khả năng thiết kế, kiểm tra như minh họa trong Hình 1.1 Hình 1.1 Khoảng cách giữa năng suất sản và năng suất thiết kế vi mạch [13] Công nghệ sản xuất vi mạch phát triển nhanh chóng cho phép sản xuất các vi mạch có độ tích hợp rất lớn lên đến hàng trăm triệu phần tử logic trên một phiến silicon.
- Tuy nhiên, giải pháp thiết kế và kiểm tra hiện nay chưa phát triển đầy đủ để cho phép thiết kế, kiểm tra nhanh chóng, năng suất các hệ thống phức tạp như vậy.
- Do đó, các thuật toán tự động tổng hợp, tối ưu và kiểm tra vi mạch là vấn đề nhận được sự quan tâm đặc biệt của cộng đồng nghiên cứu thiết kế vi mạch.
- Tự động tổng hợp tối ưu cho phép người thiết kế mô tả (thiết kế) hệ thống ở lớp trừu tượng cao hơn, sau đó thuật toán sẽ tự động chuyển đổi mô hình ở lớp cao thành các mô hình ở lớp thấp chi tiết hơn.
- Điều đó giúp người thiết kế có thể xây dựng những hệ thống phức tạp hơn trong thời gian ngắn hơn và chính xác hơn.
- Khoảng cách năng suất thiết kế.
- Do vậy, trong toàn bộ giá thành thiết kế hệ thống trên chip, giá thành phát triển phần mềm và giá thành kiểm tra trở thành 2 phần lớn nhất và tăng trưởng nhanh nhất (Hình 1.2).
- Hình 1.2 Giá thành thiết kế hệ thống trên chip [14.
- 13 - 1.2) Phân loại lỗi và các loại kiểm chứng vi mạch Phân bổ các loại lỗi trong vi mạch được thể hiện trong biểu đồ Hình 1.3.
- Hình 1.3 Phân bổ các loại lỗi trong vi mạch [15] Biểu đồ trong Hình 1.3 chỉ rõ rằng, các lỗi logic và lỗi chức năng chiếm đa số lên tới 45%.
- Trong nhiều trường hợp, việc phát hiện lỗi là không thể, việc kiểm tra các thiết kế bằng những phương pháp hiện tại chưa đáp ứng được với những thiết kế ngày một phức tạp.
- Vì vậy cần phải có những phương pháp kiểm chứng mới phát hiện những lỗi này.
- Biểu đồ Hình 1.4 chỉ ra các lỗi trong quá trình thiết kế chip Pentium 4 của Intel.
- Sự phân bố không đều nguyên nhân lỗi được chỉ ra với cao nhất là các lỗi ngớ ngẩn 12,7% do người dùng đánh máy, viết code thiếu cẩn thận trong khí chỉ có 2,6% là các lỗi hiểu sai thiết kế.
- Đây là hai lỗi có thể hoàn toàn được cải thiện nhờ sự cẩn thận của kỹ sư thiết kế.
- Lỗi do các kỹ sư thiết kế không hiểu nhau cũng có tỷ lệ khá cao tới 11.4%, thấp hơn một chút, hai lỗi do định nghĩa kiến trúc và thay đổi code để sửa lỗi timing đứng ở vị trí thứ ba với 9.3%.
- Những lỗi này thường khó phát hiện và cần đầu tư công sức lớn trong quá trình thiết kế.
- Theo sau là các lỗi do tài liệu không hoàn chỉnh, vi kiến trúc quá phức tạp, hoặc như 50% là các lỗi logic và chức năng  cần các phương pháp kiểm chứng để phát hiện lỗi logic, lỗi chức năng.
- Bất kỳ lỗi nào dù nhỏ cũng sẽ là thách thức đối với các kỹ sư thiết kế.
- Hình 1.4 Phân bổ lỗi trong chip Pentium 4 [16] Bảng 1.1 Phân bổ lỗi trong chip Pentium 4 [16] Goof Lỗi ngớ ngẩn: đánh máy, cắt-dán, viết code thiếu cẩn thận 12.70% Miscommunication Những kỹ sư thiết kế, kỹ sư kiến trúc không hiểu nhau 11.40% Microarchitecture Thiếu, lỗi trong định nghĩa vi kiến trúc 9.30% Logic/Microcode Lỗi khi thay đổi code để sửa lỗi, sửa vấn đề timing 9.30% Corner cases Các trường hợp đặc biệt không được triển khai đúng 8% Power down issues Các đặc điểm tiết kiệm điện bằng cách tắt xung đồng hồ 5.70% Documentation Tài liệu không đúng, không hoàn chỉnh 4.40% Complexity Vi kiến trúc quá phức tạp 3.90% Random initialization Các trạng thái không được xóa hoặc khởi tạo đúng 3.40% Late definition Các đặc điểm không có ở vi kiến trúc ban đầu mà đước thêm vào sau GoofMiscommunicationMicroarchitectureLogic/MicrocodeCorner casesPower down issuesDocumentation - 15 - Incorrect RTL assertions Các điểm kiểm tra khẳng định sai, bị làm sai khi sửa lỗi 2.80% Design mistake Người thiết kế hiểu sai phần cần triển khai do không đọc hoặc đọc không đầy đủ bản yêu cầu kỹ thuật 2.60% Hình 1.5 Các loại kiểm chứng khác nhau và phân bổ công sức khi kiểm chứng Hình 1.5 [13] mô tả các loại kiểm chứng khác nhau và phân bổ công sức khi kiểm chứng.
- Kiểm chứng hệ thống là sự xác minh các chức năng của hệ thống có hoạt động đúng theo các yêu cầu trong tài liệu hay không.
- Từ biểu đồ ta thấy đó là loại kiểm chứng khó khăn và tốn kém nhất khi chiếm đến 40% công sức.
- 1.4) Vị trí kiểm chứng vi mạch trong quy trình thiết kế vi mạch Quá trình thiết kế có thể hiểu là quá trình triển khai các mô tả kỹ thuật.Ở mức mô tả kỹ thuật, các đặc điểm kỹ thuật nêu rõ các chức năng thiết kế phải thực hiện nhưng không cho biết nó được thực hiện như thế nào.
- Hình 1.6 Bậc thang độ trừu tượng của thiết kế [9] Kiểm chứng thiết kế là quá trình ngược lại của thiết kế.Kiểm chứng thiết kế bắt đầu với việc thực hiện và khẳng định rằng việc thực hiện đáp ứng các thông số kỹ thuật của nó.
- Ví dụ, một bước thiết kế chuyển mô tả chức năng thành việc thực hiện thuật toán đòi hỏi phải có một bước kiểm chứng để đảm bảo rằng các thuật toán sẽ thực hiện đúng các chức năng đã được mô tả.
- Tương tự như vậy, một thiết kế vật lý tạo ra layout từ một gate netlist cần phải được kiểm chứng để đảm bảo rằng layout sẽ tương đương với gate netlist.
- Nhìn chung, việc kiểm chứng thiết kế sẽ bao gồm rất nhiều lĩnh vực như kiểm chứng chức năng, kiểm chứng thời gian, kiểm chứng layout, kiểm chứng về nguồn điện.
- Trong luận văn này, chúng ta sẽ chỉ đề cập đến kiểm chứng về chức năng và coi nó như là việc kiểm chứng thiết kế.
- Hình 1.7 cho thấy mối quan hệ giữa quá trình thiết kế và quá trình kiểm chứng.

Xem thử không khả dụng, vui lòng xem tại trang nguồn
hoặc xem Tóm tắt