Các thao tác của các thiết bị dùng để cài đặt cho hệ thống điều khiển có thể đ-ợc mô phỏng bởi ch-ơng trình, điều đó cho phép phần cứng đ-ợc kiểm chứng bằng các công cụ phần mềm chuẩn. Trong bài báo này chúng tôi hình thức hoá ngữ nghĩa sự kiện của ngôn ngữ mô tả phần cứng d-ới dạng các quan hệ và sử dụng các quan hệ đó để chứng minh một số tính chất của các ch-ơng trình tổ hợp, mà mỗi chu trình hoạt động của nó là một vòng lặp có điều. | NGỮ NGHĨA QUAN HỆ CỦA CÁC CHƯƠNG TRÌNH Tổ HỢP TS. TRẦN VĂN DŨNG Bộ môn Toán - ĐH GTVT Tóm tắt Các thao tác cũa các thiết bị dũng để cài đặt cho hệ thống điều khiển có thể được mô phỏng bởi chương trình điều đó cho phép phần cứng được kiểm chứng bằng các công cụ phần mềm chuẩn. Trong bài báo này chúng tôi hình thức hoá ngữ nghĩa sự kiện cũa ngôn ngữ mô tả phần cứng dưới dạng các quan hệ và sử dụng các quan hệ đó để chứng minh một số tính chất cũa các chương trình tổ hợp mà mỗi chu trình hoạt động cũa nó là một vòng lặp có điều kiện cũa một số các phép gán song song. Summary The actual behaviour of hardware devices available for installation of a control system can be simulated by a program and this allows the hardware to be proved correct by standard software techniques. In this paper we formalise event semantics of Hardware Description Language in the form of relations and use relation calculus to prove properties including termination and stability and uniqueness of final state of combined programs each operational cycle of which is defined as a conditional loop of non-deterministic choices among generalised parallel assignments. 1. MỞ ĐẦU Chương trình VERILOG 6 được sử dụng rông rãi để mô hình cấu trúc và hành vi của các thiết bị phần cứng từ các thiết bị đơn giản đến các mạng máy tính. Ngữ nghĩa mô phỏng định hướng của sự kiện đã được đề cập nghiên cứu trong 3 tuy nhiên khi mô tả hoạt đông không đồng bô của hệ thống gồm nhiều thiế t bị song song nó rẽ nhánh dẫn đế n nhiều kế t quả khác nhau. Vì vậy ngữ nghĩa đó không hỗ trợ việc kiểm chứng các thiế t bị phần cứng. Do đó cần phải có phương pháp hình thức hoá ngữ nghĩa sự kiện. Bài báo này tổng quát hoá ngữ nghĩa mô phỏng bằng cách đưa ra mô hình quan hệ cho VERILOG dựa trên quan hệ của các trạng thái kết thúc. Bài báo này xem xét ba lớp chương trình mô tả hoạt đông của các mạch tổ hợp. Hai phần đầu của Bài báo hình thức hoá ngữ nghĩa sự kiện của VERILOG. Phần sau cùng dành cho việc nghiên cứu các chương trình tổ
