moka - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

MOKA - Tổ tiên của trình kiểm tra mô hình

SYNOPSIS

moka [-VDB] fsm_filename tên tệp ctl_file

MÔ TẢ

moka là một trình kiểm tra mô hình CTL.

Được tạo để chạy trên các mô tả FSM hoặc RTL, moka hỗ trợ cùng một tập hợp con VHDL như syf hoặc boom
(để biết thêm thông tin về tập hợp con này, hãy xem SYF(1) BOOM(1) FSM(5) VBE(5)).
Tuy nhiên moka áp đặt rằng mỗi thanh ghi của mô tả hành vi có cùng
điều kiện đồng hồ và không có xe buýt tristate hoặc ghép kênh. Nói riêng VHDL
loại MUX_BIT và WOR_BIT không được hỗ trợ.
Đầu tiên của tất cả các moka xây dựng quá trình chuyển đổi cơ sở của FSM bằng cách sử dụng Binary có thứ tự giảm
Biểu diễn sơ đồ quyết định.
Sau đó, nó áp dụng các điều kiện ban đầu để tìm trạng thái đầu tiên (từ khóa BAN ĐẦU và / hoặc
RESET_COND trong CTL(5) định dạng tệp).
Sau khi nó tính toán một mô phỏng tượng trưng của FSM để tìm tất cả các trạng thái có thể truy cập được.
Tính toán này có tính đến các điều kiện giả định (từ khóa ASSUME trong
CTL(5) định dạng tệp).
moka cuối cùng xác minh từng công thức CTL. (Thấy chưa CTL(5) cho định dạng tệp CTL
thông tin chi tiết).

CTL ĐIỀU HÀNH

Đối với mỗi biểu thức con CTL moka sẽ trả về tập hợp các trạng thái xác minh công thức.
Ví dụ EX (p) sẽ trả về tập hợp các trạng thái có thể truy cập xác minh EX (p).
Các toán tử CTL:
EX (p): trả về tất cả các trạng thái có gần như một trạng thái chính kế thừa
xác minh p.
EU (p, q): trả về tất cả các trạng thái là gốc của hầu hết một đường dẫn, sao cho p is
đúng cho đến khi q luôn luôn đúng.
EG (p): trả về tất cả các trạng thái là gốc của hầu hết một đường dẫn, như vậy p is
luôn luôn đúng.
AX (p): trả về tất cả các trạng thái có tất cả các trạng thái kế thừa trạng thái chính của chúng
xác minh p.
AU (p, q): trả về tất cả các trạng thái là gốc của chỉ các pat từ đó p là đúng
cho đến khi q luôn luôn đúng.
AG (p): trả về tất cả các trạng thái là gốc của chỉ các lần vỗ nhẹ, như vậy p luôn luôn là
sự thật.

MÔI TRƯỜNG BIẾN

MBK_WORK_LIB cung cấp đường dẫn cho mô tả và tệp CTL. Giá trị mặc định là
thư mục hiện tại.

MBK_CATA_LIB đưa ra một số dấu hiệu bổ trợ cho các mô tả và tệp CTL. Các
giá trị mặc định là thư mục hiện tại.

LỰA CHỌN

-V Đặt chế độ tiết. Mỗi bước kiểm tra mô hình được hiển thị trên tiêu chuẩn
đầu ra.

-Đặt chế độ gỡ lỗi trên. Mỗi bước kiểm tra mô hình được trình bày chi tiết trên đầu ra tiêu chuẩn.
Đặc biệt, tất cả các trạng thái được thiết lập đều được hiển thị cho mỗi biểu thức con CTL.

- Tệp đầu vào là một mô tả VHDL sử dụng tập hợp con VHDL Alliance (xem VBE(5) tệp
định dạng).

FSM THÍ DỤ

- Một ví dụ đa fsm

Ví dụ ENTITY mới là
PORT
(
ck: bằng BIT;
data_in: trong BIT;
đặt lại: trong BIT;
data_out: hết BIT
);
END ví dụ;

Ví dụ về KIẾN TRÚC FSM OF là

LOẠI A_ETAT_TYPE IS (A_E0, A_E1);
TÍN HIỆU A_NS, A_CS: A_ETAT_TYPE;

LOẠI B_ETAT_TYPE IS (B_E0, B_E1);
TÍN HIỆU B_NS, B_CS: B_ETAT_TYPE;

--PRAGMA CURRENT_STATE A_CS FSM_A
--PRAGMA NEXT_STATE A_NS FSM_A
--PRAGMA ĐỒNG HỒ ck FSM_A
--PRAGMA FIRST_STATE A_E0 FSM_A

--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--PRAGMA ĐỒNG HỒ ck FSM_B
--PRAGMA FIRST_STATE B_E0 FSM_B

SIGNAL ACK, REQ, DATA_INT: BIT;

BEGIN

A_1: QUY TRÌNH (A_CS, ACK)
BEGIN
IF (đặt lại = '1')
VẬY A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ELSE
CASE A_CS là
KHI A_E0 =>
IF (ACK = '1') THÌ A_NS <= A_E1;
ELSE A_NS <= A_E0;
END IF;
DATA_OUT <= '0';
REQ <= '1';
KHI A_E1 =>
IF (ACK = '1') THÌ A_NS <= A_E1;
ELSE A_NS <= A_E0;
END IF;
DATA_OUT <= DATA_INT;
REQ <= '0';
KẾT THÚC TRƯỜNG HỢP;
END IF;
KẾT THÚC QUÁ TRÌNH A_1;

A_2: QUY TRÌNH (ck)
BEGIN
IF (ck = '1' VÀ KHÔNG THỂ ck'STABLE)
VẬY A_CS <= A_NS;
END IF;
KẾT THÚC QUÁ TRÌNH A_2;

-------

B_1: QUY TRÌNH (B_CS, ACK)
BEGIN
IF (đặt lại = '1')
THÌ B_NS <= B_E0;
DATA_INT <= '0';
ACK <= '0';
ELSE
CASE B_CS là
KHI B_E0 =>
IF (REQ = '1') THÌ B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DATA_INT <= '0';
ACK <= '0';
KHI B_E1 =>
IF (REQ = '1') THÌ B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DATA_INT <= DATA_IN;
ACK <= '1';
KẾT THÚC TRƯỜNG HỢP;
END IF;
KẾT THÚC QUY TRÌNH B_1;

B_2: QUY TRÌNH (ck)
BEGIN
IF (ck = '1' VÀ KHÔNG THỂ ck'STABLE)
VẬY B_CS <= B_NS;
END IF;
KẾT THÚC QUY TRÌNH B_2;

KẾT THÚC FSM;

CTL THÍ DỤ

- Ví dụ về tệp CTL

LOẠI A_ETAT_TYPE IS (A_E0, A_E1);
LOẠI B_ETAT_TYPE IS (B_E0, B_E1);

BIẾN A_NS, A_CS: A_ETAT_TYPE;
BIẾN B_NS, B_CS: B_ETAT_TYPE;

BIẾN CỐ ck: BIT;
VARIABLE data_in: BIT;
VARIABLE data_out: BIT;
Đặt lại VARIABLE: BIT;
BIẾN ÁP ack: BIT;
Yêu cầu VARIABLE: BIT;

RESET_COND init1: = (reset = '1');
ASSUME ass1: = (reset = '0');

bắt đầu

prop1: EX (ack = '1');
prop2: AG (yêu cầu -> AF (ack));
prop4: AU (req = '1', ack = '1');

kết thúc;

MOCHA THÍ DỤ

ví dụ về moka -V

Sử dụng moka trực tuyến bằng các dịch vụ onworks.net