Chương 1 GIỚI THIỆU 1.1 Tính cấp thiết của đề tài Trong lĩnh vực thiết kế vi mạch tích hợp mật độ cao VLSI hiện nay, một trong lĩnh vực phát triển mũi nhọn của các quốc gia trên thế giới, hướng thiết kế vi mạch bất đồng bộ (asynchronous circuit) nổi lên như một giải pháp tự nhiên và vững chắc thay thế cho các hạn chế về việc đồng bộ mà vi mạch đồng bộ (synchronous circuit) gặp phải như là việc phân phối xung nhịp, năng lượng tiêu thụ, nhiễu [8]. Về bản chất, các vi mạch bất đồng bộ là tổ hợp các thành phần hoạt động độc lập và giao tiếp với nhau thông qua các tín hiệu (giao thức) thông báo trạng thái hoàn thành của các lệnh hoặc tác vụ. Một số loại vi mạch bất đồng bộ đã được nghiên cứu và phát triển cho những kết quả rất khả quan. Điều đó cho thấy nó là một cách thiết kế quan trọng trong tương lai.
Tuy vậy, mặc dù vi mạch bất đồng bộ có những ưu điểm và tiềm năng to lớn, các qui trình thiết kế vi mạch bất đồng bộ vẫn có chưa nhiều. Một trong các nguyên nhân là tính phổ quát của vi mạch bất đồng bộ ứng dụng trong công nghiệp còn thấp. Ngoài ra, việc thiết kế vi mạch theo kiểu đồng bộ đã đạt đến mức trưởng thành, tự động hoá cao làm trì trệ việc chuyển sang một kiểu thiết kế mới của các nhà thiết kế. Một trong nhưng nguyên nhân quan trọng nữa là hiện nay các phương pháp kiểm định hình thức (formal verification) để đảm bảo tính đúng đắn (correctness) của một thiết kế vi mạch bất đồng bộ vẫn còn đang được nghiên cứu [46][26][25][19][9].
Giả định rằng, các phương pháp kiểm định thiết kế là hiệu quả, một nhà thiết kế vi mạch có thể nhanh chóng xác định được các khiếm khuyết trong thiết kế của 1 vi mạch bất đồng bộ trước khi nó được chế tạo và tung ra thị trường. Hiển nhiên việc kiểm định này giúp tiết kiệm tài chính, nhân lực và thậm chí cả tính mạng của con người trong việc khắc phục sai sót của các vi mạch trong đời sống chúng ta. Tuy nhiên, các phương pháp kiểm định thiết kế là hiệu quả chỉ là giả định và bản thân khái niệm “hiệu quả” cũng không rõ ràng khi có sự đánh đổi giữa tài nguyên con người, máy móc với mục tiêu cần được kiểm định. Do các thành phần của vi mạch bất đồng bộ hoạt động độc lập và chỉ giao tiếp với nhau thông qua các giao thức, các nhà thiết kế có thể dùng các ngôn ngữ đặc tả hình thức cấp cao để biểu diễn vi mạch.
Đây là một điểm đặc biệt thuận lợi của hướng tiếp cận thiết kế bất đồng bộ. Các ngôn ngữ đặc tả hình thức cấp cao như CSP (Communicating Sequential Processes) [7], CHP (Communicating Hardware Processes) [19] hay ADL (Asynchronous Description Language) [3] cho phép người thiết kế có thể tập trung vào hành vi của vi mạch nhiều hơn. Nhờ 1 đó, người thiết kế được giải thoát khỏi lớp hiện thực bên dưới, nâng cao sự hiểu quả quá trình thiết kế. Ngoài các ngôn ngữ cấp cao trong biễu diễn các thiết kế vi mạch, các hình thức biểu diễn trung gian như mạng Petri [27], đồ thị dòng dữ liệu DFG [34] cũng được quan tâm nghiên cứu.
Những mô hình trung gian này có ý nghĩa rất quan trọng trong việc giả lập và phân tích thiết kế vi mạch bất đồng bộ. Trong nghiên cứu được thực hiện ở ĐH Bách Khoa Tp.HCM [12] về việc nghiên cứu xây dựng phương pháp luận thiết kế vi mạch bất đồng bộ loại QDI, các tác giả đã đưa ra được một framework phục vụ cho qui trình thiết kế vi mạch bất đồng bộ và hiện thực thành nó thành công cụ gọi là PAiD. Công cụ này cho phép nhà thiết kế đặc tả vi mạch bất đồng bộ ở ngôn ngữ cấp cao và thông qua các phép biến đổi trung gian tổng hợp thành vi mạch biểu diễn ở cấp thấp (netlist). Tuy nhiên, công cụ này chưa giải quyết bài toán kiểm định thiết kế.
Từ những tìm hiểu tổng quan nêu trên, tính cấp thiết của việc kiểm định tính đúng đắn của một thiết kế vi mạch bất đồng bộ tạo động lực mạnh mẽ cho các công việc được thực hiện trong luận văn này.2 Phát biểu vấn đề Nghiên cứu đề xuất phương pháp kiểm định thiết kế vào trong thiết kế vi mạch bất đồng bộ, có 2 vấn đề lớn cần giải quyết: (1) nghiên cứu tính khả thi của phương pháp kiểm định hình thức kiểm tra mô hình trong việc kiểm định vi mạch bất đồng bộ, đồng thời xây dựng một qui trình hoàn chỉnh các thủ tục tiến hành kiểm định; và (2) hiện thực tích hợp việc kiểm định vào qui trình thiết kế nhằm thử nghiệm đánh giá phương pháp đề xuất. Vấn đề thứ nhất thuộc phạm vi nghiên cứu lý thuyết về kiểm định hình thức. Về bản chất, vấn đề quan trọng nhất là giải quyết bài toán bùng nổ không gian trạng thái (state space explosion problem). Đây là vấn đề cơ bản của bất kỳ phương pháp kiểm định nào (phần mềm, phần cứng, qui trình công nghiệp, …).
Nói một cách tổng quát, chỉ khi nào tất cả các trạng thái có thể có của một vi mạch đều không dẫn đến khiếm khuyết nào, vi mạch đó mới được đảm bảo là đúng với mục đích thiết kế của nó. Khi công việc thiết kế tiến đến qui mô công nghiệp, không gian trạng thái của vi mạch sẽ nhanh chóng vượt ra ngoài tầm kiểm soát. Mặc dù người ta có thể dùng phương pháp mô phỏng (simulation) và kiểm thử (testing) để nâng độ an tâm đối với vi mạch, chúng không thể đảm bảo tính đúng đắn của một vi mạch [8]. Do đó, việc áp dụng thành công một phương pháp kiểm định hình thức sẽ là tiền đề quan trọng cho việc chứng minh sự đúng đắn của một vi mạch bất đồng bộ một cách đầy đủ.
Vấn đề thứ hai liên quan đến qui trình thiết kế và thời điểm tích hợp phương pháp kiểm định vào qui trình này. Như đã trình bày, các qui trình thiết kế ngày nay đều cho phép các nhà thiết kế mô tả vi mạch ở cấp ngôn ngữ cấp cao trước khi diễn tả ở một ngôn ngữ cấp thấp hơn (ví dụ như sơ đồ netlist) và hiện thực mạch bằng phần cứng. Do đó, việc tích hợp có thể diễn ra ở cấp ngôn ngữ cấp cao hoặc các cấp trung gian [23] và thậm chí ở mức ngôn ngữ cấp thấp [9]. Mỗi cách tích hợp sẽ giải quyết được những nhóm bài toán khác nhau đối với vấn đề kiểm định.
Ví dụ như, các hiện tượng nhiễu (hazard) chỉ có thể được kiểm định sau khi có bản thiết kế ở mức cổng phần cứng (netlist) [38]. Tuy nhiên, độ phức tạp của bài toán sẽ tăng lên rất nhiều khi mức biểu diễn càng xuống cấp thấp. Ngoài ra, ngôn ngữ càng cấp cao, trừu tượng càng gần gũi và dễ hiểu hơn với người thiết kế. Do vậy, các kiểm định ở các mức cấp cao này sẽ giúp nhà thiết 2 kế giải quyết vấn đề thiết kế hiệu quả hơn [60][19].
Lúc này, các công cụ thiết kế hỗ trợ ngôn ngữ cấp cao, có tích hợp các phép biến đổi đến các cấp thấp hơn và cấp cổng phần cứng, đồng thời tích hợp việc kiểm định, là một nhu cầu rất lớn. Ở các cấp biểu diễn trung gian, mặc dù đã có nhiều nghiên cứu có kết quả khả quan [25][46][47] như chuyển từ mạng Petri sang BDD [46] và dùng các công cụ kiểm định sẵn có, việc biểu diễn một vi mạch bất đồng bộ dùng các ngôn ngữ trung gian này (như mạng Petri) là khá khó khăn. Trong vấn đề này còn có thêm một vấn đề kèm theo đó là kiểm định tính đúng đắn của các phép biến đổi từ các đặc tả mức cao hơn xuống một mức thấp hơn [25][26]. Vấn đề này phần nào đã được giải quyết trong [12] bằng các qui luật biến đổi bảo toàn mục tiêu thiết kế.
Vì vậy, bài toán đặt ra cấp bách hiện nay chính là kiểm định tính đúng đắn trong thiết kế ở mức diễn đạt cấp cao và các cấp trung gian. Ngoài ra, để chứng minh cho tính khả thi của phương pháp kiểm định, luận văn cũng xây dựng một bộ các vi mạch mẫu để tiến hành thực nghiệm và lấy kết quả phân tích.3 Đóng góp của luận văn Những đóng góp chính của luận văn như sau: Qui trình kiểm định vi mạch bất đồng bộ ở mức trừu tượng hóa cáo bằng phương pháp kiểm tra mô hình. Các phương pháp biểu diễn mô hình trung gian vi mạch bất đồng bộ trong công cụ kiểm tra mô hình nổi tiếng NuSMV. Các phương pháp chuyển đổi này có ý nghĩa hết sức quan trọng trong việc xây dựng qui trình kiểm định.
Khối kiểm định mở rộng góp phần hoàn thiện hơn nữa môi trường thiết kế PAiD. Nhờ đó, nó góp phần nâng cao độ tin cậy cho vi mạch bất đồng bộ tạo ra bởi công cụ thiết kế này. Bộ vi mạch mẫu dùng cho việc kiểm tra, đánh giá qui trình kiểm định đề xuất. Ngoài ra, bộ vi mạch mẫu này còn có thể được sử dụng trong giảng dạy và nghiên cứu về vi mạch bất đồng bộ.
Cuối cùng, có thể nói kết quả của luận văn góp phần làm phong phú hơn bức tranh toàn cảnh nghiên cứu về thiết kế vi mạch số nói chung và hướng tiếp cận bất đồng bộ nói riêng.4 Công bố khoa học Trong quá trình thực hiện luận văn, các kết quả đạt được đã được công bố ở các tạp chí, hội nghị quốc tế uy tín như sau: Tạp chí quốc tế: Tin T. Nguyen, Khoi-Nguyen Le-Huu, Thang H. Bui, Anh-Vu Dinh-Duc, "A New Approach and Tool in Verifying Asynchronous Circuits," in REV Journal on Electronics and Communications, vol. Hội nghị quốc tế: 1.
Bui, Khoi-Nguyen Le-Huu, Anh-Vu Dinh-Duc, " Enhanced PAiD – An EDA Tool for Asynchronous Circuit Design and Verification," in Procs. of ECTI Conference 2014 (ECTI – Electrical Engineering/Electronics, Computer, Telecommunications and Information Technology), Nakhon Ratchasima, Thailand, May 14-17, 2014. Dinh-Duc, "A New Approach and Tool in Verifying Asynchronous Circuits," in Procs. of The International Conference on Advanced Technologies for Communications (ATC 2012), Hanoi, Vietnam, Oct 2012.
Dinh-Duc, "Experiences with Representations and Verification for Asynchronous Circuits," in Procs. of 4th Int. on Communications and Electronics (ICCE 2012), Hue, Vietnam, 2012.5 Cấu trúc luận văn Phần tiếp theo của luận văn sẽ trình bày các vấn đề như sau: Chương 2: Tổng quan về thiết kế vi mạch bất đồng bộ, bao gồm các khái niệm cơ bản trong vi mạch bất đồng bộ và các đặc tả cấp cao cũng như cấp trung gian. Chương 3: Giới thiệu về môi trường thiết kế vi mạch bất đồng bộ PAiD.
