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. | 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ở CNTT- 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ủa 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 .
