Báo cáo khoa học: VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ

Tóm tắt: Bài báo sử dụng ngữ nghĩa quan hệ của chương trình tổ hợp [1, 2] để mô phỏng và chứng minh tính dừng của các mạch không đồng bộ có một số tính chất xác định. Điều đó cho phép dùng các kỹ thuật phần mềm chuẩn để kiểm chứng các hành vi của các mạch tổ hợp.
Nội dung trích xuất từ tài liệu:
Báo cáo khoa học: "VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ" VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ TS. TRẦN VĂN DŨNG Bộ môn Khoa học máy tính Khoa Công nghệ thông tin Trường Đại học Giao thông Vận tải Tóm tắt: Bài báo sử dụng ngữ nghĩa quan hệ của chương trình tổ hợp [1, 2] để mô phỏng và chứng minh tính dừng của các mạch không đồng bộ có một số tính chất xác định. Điều đó cho phép dùng các kỹ thuật phần mềm chuẩn để kiểm chứng các hành vi của các mạch tổ hợp. Summary: This paper using relational semantics of combinational programs [1,2] to simulate and prove a termination of some sequential circuits with determined properties. It allows to use standard software verification techniques to verify behaviours of some kinds of sequential circuits. I. MỞ ĐẦU Mục đích của bài báo nhằm đưa ra phương pháp hình thức để nghiên cứu một số tính chất quan trọng của các mạch không đồng bộ, tức là mạch xử lý thông tin mà ngoài đầu vào và đầu ra có thể cho phép quay vòng một số thông tin bên trong mạch. Các mạch không tuần tự là cơ sở phần cứng cho các mô hình máy tính, chính vì vậy việc tìm hiểu và suy luận về các hành vi củaCNTT-CB mạch có ý nghĩa quan trọng và thu hút sự quan tâm nghiên cứu của nhiều tác giả (xem [1,2]). Trong bài này ta xét mạch tuần tự không đồng bộ theo trình tự các bước như sau: * Bổ sung biến delay vào các vị trị cần thiết * Biểu diễn các biến bổ sung thông qua đầu vào, đầu ra và thông tin quay vòng * Tìm mối liên hệ giữa các biến xem có thoả mãn các điều kiện cần thiết không * Xét mạch có cho kết quả về hành vi duy nhất không. Ở đây ta xét chế độ thao tác cơ bản mở rộng theo nghĩa sau: các tín hiệu vào có thể đồng bộ thay đổi, nhưng sau đó mọi tín hiệu vào đều chờ đợi cho đến khi mạch đạt đến trạng thái cân bằng tiếp theo. Khi ghép nối các mạch, nếu các mạch thành phần là lũy đẳng (tức là nếu thực hiện thêm một lần thứ hai thì không đem lại kết quả gì mới) hoặc bản thân nó là mạch tổ hợp, thì nguyên tắc hoạt động trên được đảm bảo. II. MÔ PHỎNG MẠCH KHÔNG ĐỒNG BỘ Bây giờ chúng ta xét các mạch không đồng bộ, đó là các mạch có phản hồi nhưng không có đồng hồ đồng bộ. Ở đây các tín hiệu đầu vào có thể thay đổi, sau đó chờ cho mạch hoạt độngcho đến khi mọi giá trị đầu ra và thông tin quay vòng không thay đổi, nữa, đến lúc đó giá trị đầuvào mới lại có thể thay đổi. Trong [1, 2] chúng ta đã đưa ra định nghĩa chương trình tổ hợp Comb để mô phỏng hoạtđộng của mạch không đồng bộ. Trong mạch có thể có nhiều luồng thành phần, chúng thay nhauthực hiện một cách tùy ý, cho đến khi mọi việc thực hiện sẽ không đem lại kết quả mới nữa. Lúcđó ta nói mạch ở trạng thái ổn định và dừng. Chúng ta mong muốn tìm hiểu các điều kiện ràng buộc đối với các mạch mà kết quả cuốicùng khi thực hiện chúng là tất định, không phụ thuộc vào thứ tự thực hiện của các luồng. Ví dụ 1: Cho mạch không đồng bộ sau * Đầu vào S, R * Đầu ra Q. Vì Q có feedback, nên coi Q là biến trung gian (delay) * Biến trung gian delay tác động bên trong X * Vậy ta có hai mạch sau: Q = X’ · R’ (1) X = S’ · Q’ (2) CNTT-CB Ở đây để đơn giản ký hiệu A’ là phủ định của A và · là phép hội logic hai mệnh đề. Mạchkhông đồng bộ được xem như chương trình tổ hợp (xem [1,2]): Comb (Q # X) Điều đó cho ta biết, hai phép gán (1) và (2) thay nhau thực hiện cho đến khi giá trị của haivế các phương trình đó đồng nhất. Dễ dàng kiểm chứng thấy các trạng thái ổn định (R, S, X, Q) của chương trình tổ hợp trênbao gồm các trạng thái sau: (0, 0, 0, 1); (0, 0, 1, 0); (0, 1, 0, 1); (1, 0, 1, 0); (1, 1, 0, 0). * Xét trạng thái (0, 0, 0, 1) với R = 0, S = 0, X = 0, Q = 1: Giả sử R tăng giá trị lên 1, khi đó nó kích hoạt Q: + Q = X’ · R’ = 1 · 0 = 0. Q thay đổi kích hoạt X. + X = S’ · Q’ = 1 · 1 = 1. X thay đổi kích hoạt Q. + Q = X’ · R’ = 0 · 0 = 0. Q không thay đổi. + Dừng do không có biến nào thay đổi. Trạng thái ổn định đạt được (1, 0, 1, 0). Giả sử S tăng giá trị lên 1, khi đó nó kích hoạt X: + X = S’ · Q’ = 0 · 0 = 0. X không tha ...