Giáo trình Ngôn ngữ mô tả phần cứng Verilog - Vũ Đức Lung
Tóm tắt Giáo trình Ngôn ngữ mô tả phần cứng Verilog - Vũ Đức Lung: ...ả cũng là số thực 2**-3’sb1 0 2**-1=1/2, có phần nguyên là số 0 0**-1 ‘bx 0 lũy thừa số âm là một số không xác định 9**0.5 3.0 Kết quả là một số thực 9.0**(1/2) 1.0 ½ kết quả là 0 -3.0**2.0 9.0 Kết quả là một số thực Toán tử số học một ngôi: Toán tử này có quyền ưu tiên cao hơn đối v...ố thứ nhất trong danh sách tham số kết nối với đầu ra, tham số thứ hai kết nối với đầu vào, tham số thứ ba kết nối với đầu vào điều khiển. Khai báo thể hiện của một cổng logic ba trạng thái sẽ bắt đầu với một trong các từ khóa sau: bufif0 bufif1 notif1 notif0 Đặc tả trì hoãn sẽ là 0, 1, 2 hoặ...0. Những từ khóa sau sẽ mô tả độ mạnh của phép gán 1: supply1 strong1 pull1 weak1 highz1 Những từ khóa sau sẽ mô tả độ mạnh của phép gán 0: supply0 strong0 pull0 weak0 highz0 Thứ tự của sự mô tả hai độ mạnh trên là tùy ý. Hai nguyên tắc sau sẽ ràng buộc việc sử dụng sự mô tả độ mạnh điều khiển:...
h. Khi misr được gọi thể hiện, các biến này sẽ kết nối với các cổng thật sự của nó. Thể hiện của misr cũng bao gồm chi tiết về các tham số poly của nó. Ví dụ 9.4 module test_misr; reg clk=0, rst=0; reg [3:0] d_in; wire [3:0] d_out; misr #(4’b1100) MUT ( clk, rst, d_in, d_out ); initial begin #13 rst=1’b1; #19 d_in=4’b1000; #31 rst=0’b0; #330 $finish; end always #37 d_in = d_in + 3; always #11 clk = ~clk; endmodule Trong khối initial của testbench tạo ra một pulse lên vào lúc rst mà bắt đầu tại 13ns và kết thúc tại 63ns. Thời gian như vậy là sự lựa chọn để bao gồm ít nhất một cạnh lên của đồng hồ, vì vậy sự đồng bộ của đầu vào rst có thể khởi tạo trong thanh ghi misr. Đầu vào dữ liệu d_in bắt đầu là x, và trong khởi là 4’b1000 khi rst là 1. Ngoài các khối khởi tạo, module test_misr còn bao gồm 2 khối always để tạo dữ liệu cho d_in và clk. Clock cho ra một tín hiệu tuần hoàn với chu kỳ 11x2=22ns. Đầu vào misrd_in gán một giá trị mới sau mỗi chu kỳ 37ns. Để giảm trường hợp các đầu vào thay đổi cùng một lúc, chúng ta sử dụng số nguyên tố cho thời gian của đầu vào mạch tuần tự. Hình 9.2 mô tả một kết quả của testbench: Hình 9.2 Một kết quả của testbench Kĩ thuật tạo testbench Các kỹ thuật viết chương trình Verilog khác nhau để tạo dữ liệu kiểm tra và xem xét đáp ứng của mạch được thảo luận trong phần này. Chúng ta sử dụng module máy trạng thái Moore để phát hiện chuỗi 101 làm ví dụ cho phần này. Module này được định nghĩa như sau: Ví dụ 9.5 module moore_detector (input x, rst, clk, output z ); parameter [1:0] a=0, b=1, c=2, d=3; reg [1:0] current; always @( posedge clk ) if ( rst ) current = a; else case ( current ) a : current = x ? b : a ; b : current = x ? b : c ; c : current = x ? d : a ; d : current = x ? b : c ; default : current = a ; endcase assign z = (current==d) ? 1’b1 : 1’b0; endmodule Dữ liệu kiểm tra Một testbench cho module moore_detector được mô tả như sau: Ví dụ 9.6 module test_moore_detector; reg x, reset, clock; wire z; moore_detector MUT ( x, reset, clock, z ); initial begin clock=1’b0; x=1’b0; reset=1’b1; end initial #24 reset=1’b0; always #5 clock=~clock; always #7 x=~x; endmodule Module testbench là một module không có các cổng kết nối ra ngoài. Bên trong module, có 4 khối thủ tục cung cấp dữ liệu cho việc kiểm tra máy trạng thái. Các biến kết nối với MUT và sử dụng vào vế bên trái của các khối thủ tục phải được khai báo là reg. Thay vì khởi tạo các biến reg khi chúng khai báo, chúng ra có thể sử dụng khối initial để khởi tạo các biến reg. Điều quan trọng khi khai khởi tạo biến, giống như clock là giá trị cũ của chúng được sử dụng để xác định giá trị mới của chúng. Nếu không như vậy, clock sẽ bắt đầu với giá trị X và cho đến khi hoàn thành, giá trị của nó cũng không thay đổi. Khối always tạo chu kỳ tín hiện với chu kỳ 10ns trên một clock. Theo sau khối thủ tục always tạo clock, một khối always khác sẽ tạo chu kỳ tín hiệu cho x với chu kỳ 14ns. Dạng sóng tạo ra cho X có thể có hoặc không thể kiểm tra máy trạng thái của chúng ra đúng tuần tự 101. Tuy nhiên, chu kỳ của clock và X có thể thay đổi điều này. Với thời gian sử dụng ở đây, đầu ra của moore_detector lên 1 sau 55ns và sau mỗi 70ns tiếp theo. Điều khiển mô phỏng Một testbench khác cho mạch moore_detector bên trên được mô tả như sau: Ví dụ 9.7 module test_moore_detector; reg x=0, reset=1, clock=0; wire z; moore_detector MUT ( x, reset, clock, z ); initial #24 reset=1’b0; always #5 clock=~clock; always #7 x=~x; initial #189 $stop; endmodule Mặc dù, cấu trúc Verilog được sử dụng khác nhau, dữ liệu và clock áp dụng cho MUT trong testbench cũng giống với testbench bên trên. Tuy nhiên, nếu trình mô phỏng cho testbench trước không có ngắt, hoặc điểm dừng, nó sẽ chạy mãi mãi. Trong testbench này giải quyết vấn đề này bằng cách thêm vào một khối khác khối initial sẽ dừng quá trình mô phỏng sau 189ns. Các task điều khiển trình mô phỏng là $stop và $finish. Thời gian đầu tiên theo chu trình của một khối thủ tục được tiếp cận như một task, trình mô phỏng sẽ dừng lại hoặc hoàn thành. Một task $stop thì có thể nối lại, nhưng một task $finish thì không thể nối lại. Một testbench khác được mô tả như sau: Ví dụ 9.8 reg x=0, reset=1, clock=0; wire z; moore_detector MUT ( x, reset, clock, z ); initial begin #24 reset=1’b0; module test_moore_detector; #165 $finish; end always #5 clock=~clock; always #7 x=~x; endmodule Trong testbench này tích hợp trong khối initial cả tín hiệu reset tích cực thấp và tín hiện điều khiển thời gian trong một khối initial. Thời gian điều chỉnh chấm dứt quá trình mô phỏng tại thời gian 189ns giống như testbench bên trên. Thiết lập giới hạn dữ liệu Thay vì cài đặt giới hạn thời gian mô phỏng, một testbench có thể đặt một giới hạn trên số dữ liệu đặt vào đầu vào của MUT. Điều sẽ cũng có thể ngăn chặn việc mô phỏng không dừng lại. Chương trình sau mô tả một testbench cho module moore_detector MUT. Ví dụ 9.9 module test_moore_detector; reg x=0, reset=1, clock=0; wire z; moore_detector MUT ( x, reset, clock, z ); initial #24 reset=1’b0; initial repeat(13) #5 clock=~clock; initial repeat(10) #7 x=$random; endmodule Testbench này sử dụng $radom để tạo dữ liệu ngẫu nhiên cho đầu vào x của mạch, câu lệnh repeat trong khối initial tạo ra tín hiện clock 13 lần sau mỗi 5ns, và x nhận dữ liệu ngẫu nhiên 13 lần sau mỗi 7ns. Thay vì dùng một bộ tính quyết định dữ liệu để đảm bảo tính quyết định các trạng thái, thì dữ liệu ngẫu nhiên được sử dụng ở đây. Chiến lượt này làm cho nó dễ dàng hơn để tạo dữ liệu, nhưng phân tích đầu ra của mạch sẽ khó khăn hơn, do đầu vào không đoán trước. Trong các mạch lớn, dữ liệu ngẫu nhiên được sử dụng nhiều cho đầu vào dữ liệu hơn tín hiệu điều khiển. Testbench trong phần này sẽ dừng sau 70ns. Cung cấp dữ liệu đồng bộ Trong các ví dụ trước testbench cho MUT sử dụng thời gian độc lập cho clock và dữ liệu. Trong trường hợp nhiều bộ dữ liệu được áp dụng, việc đồng bộ hóa dữ liệu với đồng hồ hệ thống trở nên khó khăn. Hơn nữa, việc thay đổi tần số clock sẽ yêu cầu thay đổi thời gian của tất cả các dữ liệu đầu vào của module đang kiểm tra. Testbench sau được viết cho module moore_detector, sử dụng một câu lệnh để điều khiển sự đồng bộ giữa dữ liệu áp dụng vào X với clock tạo ra trong testbench. Tín hiệu clock này tạo ra trong câu lệnh initial sử dụng cấu trúc repeat. Một câu lệnh initial khác được sử dụng để tạo dữ liệu ngẫu nhiên cho X. Như ta thấy trong câu lệnh initial này, vòng lặp mãi mãi sẽ lặp đi lặp lại câu lệnh này để sử dụng ở đây. Vòng lặp này đợi cho tới cạnh lên của clock, và sau khi cạnh lên của clock 3ns, một dữ liệu ngẫu nhiên được tạo ra cho X. Trạng thái dữ liệu sau cạnh lên của clock sẽ sử dụng bởi moore_detector trên đầu cạnh tiếp theo của clock. Kỹ thuật này của dữ liệu đảm bảo rằng sự thay đổi dữ liệu và clock không trùng nhau. Ví dụ 9.10 module test_moore_detector; reg x=0, reset=1, clock=0; wire z; moore_detector MUT ( x, reset, clock, z ); initial #24 reset=0; initial repeat(13) #5 clock=~clock; initial forever @(posedge clock) #3 x=$random; endmodule Có trì hoãn 3ns được sử dụng ở đây làm nó có thể sử dụng testbench giống nhau trong mô phỏng sau khi tổng hợp thiết kế tốt như mô tả hành vi trong các phần trên.Trong quá trình mô phỏng sau khi tổng hợp, mô hình các thành phần sẽ thực sự trì hoãn như các giá trị được sử dụng, trì hoãn trong testbench cho phép truyền tín hiệu kiểm tra hoàn thành trước khi áp dụng tín hiệu khiểm tra mới. Tương tác testbench Trong quá trình tạo testbench tiếp theo chúng ta sử dụng một máy trạng thái khác. Đó là máy trạng thái moore phát hiện chuỗi 1101 với trạng thái bắt đầu (start) và reset (rst) điều khiển đầu vào. Nết start là 0 trong khi tìm kiếm chuối 1101, máy trạng thái sẽ reset về trạng thái khởi đầu. Như ta thấy trong mạch sau có 5 trạng thái, và đầu ra của nó lên 1 khi nó bắt đầu trạng thái e. Ví dụ 9.11 module moore_detector (input x, start, rst, clk, output z ); parameter a=0, b=1, c=2, d=3, e=4; reg [2:0] current; always @( posedge clk ) if ( rst ) current <= a; else if ( ~start ) current <= a; else case ( current ) a : current <= x ? b : a ; b: current <= x ? c : a ; c : current <= x ? c : d ; d : current <= x ? e : a ; e : current <= x ? c : a ; default: current <= a; endcase assign z = (current==e); endmodule Testbench cho máy trạng thái là một testbench tương tác một. module test_moore_detector; reg x=0, start, reset=1, clock=0; wire z; moore_detector MUT ( x, start, reset, clock, z ); initial begin #24 reset=1’b0; start=1’b1; wait(z==1’b1); #11 start=1’b0; #13 start=1’b1; repeat(3) begin #11 start=1’b0; #13 start=1’b1; wait(z==1’b1); end #50 $stop; end always #5 clock=~clock; always #7 x=$random; endmodule Trong khối initial, testbench giao tiếp với MUT. Đầu vào X và clock được tạo bởi 2 khối always. Một tín hiệu có chu kỳ liên tục được tạo ra cho clock và một dữ liệu có chu kỳ ngẫu nhiên được gán cho x. Đầu tiên, giá trị 0 và 1 được đặt cho reset và start để đưa máy trạng thái vào trạng thái bắt đầu. Theo sau đó, một câu lệnh wait để đợi z lên 1 như là kết quả đáp ứng của MUT tới giá trị x và clock. Sau sự kiện này, biến start được gán bằng 0 và sau đó là 1 sau 13ns để khởi động lại máy. Theo sau vòng kích hoạt đầu tiên này, một câu lệnh repeat lặp lại tiến trình bắt đầu máy trạng thái và độ x lên 1 ba lần nữa. Sau 50ns testbench dừng quá trình mô phỏng bằng một task $stop. Tạo những khoảng thời gian ngẫu nhiên Chúng ta thấy cách hàm #random có thể sử dụng để tạo một dữ liệu ngẫu nhiên. Phần này chúng ta sẽ thảo luận cách dùng ngẫu nhiên thời gian đợi để gán giá trị cho x. Testbench sau dùng để kiểm tra module phát hiện chuỗi 1101 sử dụng $random để điều khiển trì hoãn. Như ta thấy, câu lệnh initial tên running áp dụng dữ giá trị phù hợp lên biến reset và start để hệ thống bắt đầu tìm kiếm chuỗi 1101. Trong khối thủ tục này sử dụng lệnh gán không chặn (nonblocking) tạo ra các giá trị trì hoãn trong câu lệnh gán để được coi như là một giá trị thời gian tuyệt đối. Ví dụ 9.12 module test_moore_detector; reg x, start, reset, clock; wire z; reg [3:0] t; initial begin:running clock <= 1’b0; x <= 1’b0; reset <= 1’b1; reset <= #7 1’b0; start <= 1’b0; start <= #17 1’b1; repeat (13) begin @( posedge clock ); @( negedge clock ); end start=1’b0; #5; $finish moore_detector MUT ( x, start, reset, clock, z ); end always #5 clock=~clock; always begin i = $random; #(t) x=$random; end endmodule Sau khi đặt máy trạng thái vào trạng thái running, testbench đợi 13lần để hoàn thành xung clock trước khi nó đặt lại đầu vào start và hoàn thành mô phỏng. Như ta thầy, khối always đồng thời với khối running liên tục tạo xung clock 5ns. Cùng đồng thời với các khối này là một khối always khác tạo dữ liệu ngẫu nhiên cho t, và sử dụng t để trì hoãn lệnh gán ngẫu nhiên cho x. Cả khối này tạo dữ liệu cho đầu vào x cho đến khi câu lệnh $finish trong khối running được thực hiện. Kiểm tra thiết kế Trong phần trước đã thảo luận các kỹ thuật kiểm tra để kiểm tra một thiết kế Verilog. Trong phần này sẽ bàn tới một vài phương thức để tạo dữ liệu kiểm tra và áp dụng kiểm tra, và hỗ trợ một vài cách để xem xét và kiểm tra kết quả kiểm tra. Tạo các kích thích và phân tích đáp ứng của một thiết kế đòi hỏi một phần nỗ lực đáng kể của người thiết kết phần cứng. Tìm hiểu các kỹ thuật kiểm tra đúng là tốt, nhưng thiết kế tự động làm các thủ tục này sẽ rất hữu dụng cho các kỹ sư. Hình thức kiểm tra thiết kế là một cách tự động thiết kế kiểm tra bằng cách loại bỏ testbenches và các vấn đề liên quan đến việc tạo dữ liệu và quan sát các đáp ứng của mạch. Trong hình thức kiểm tra thiết kế, người thiết kế sẽ thiết kế một thuộc tính để kiểm tra thiết kế của anh ta. Công cụ kiểm tra thiết kế hình thức không thực hiện mô phỏng, nhưng đưa ra câu trả lời có/không có cho mỗi thuộc tính của thiết kế đang được kiểm tra. Mặc dù phương pháp kiểm tra thiết kế giúp tìm ra nhiều lỗi thiết kế nhưng hầu như nhiều thiết kế vẫn cần phát triển testbench và mô phỏng để xác nhận chương trình Verilog của họ thực hiện đúng chức năng mong đợi. Nói cách khác, tất cả các câu trả lời là “có” cho tất cả các thuộc tính kiểm tra bởi công cụ kiểm tra thiết kế hình thức là chưa đủ. Thay vì bỏ qua việc tạo dữ liệu và quan sát đáp ứng, một bước theo hướng tự động hóa thiết kế xác nhận là giảm hoặc bỏ qua các nỗ lực cần thiết cho phân tích kết quả đáp ứng. Kỷ thuật chèn để kiểm tra thiết kế được sử dụng theo hướng này, nó sẽ thêm giám sát để thiết kế cải thiện khả năng quan sát đáp ứng. Trong khi thiết kế đang được mô phỏng với dữ liệu testbench, trình quan sát được chèn vào đại diện cho một số thuộc tính của thiết kế liên tục kiểm tra có đúng với thiết kế hành vi bằng các xác minh những thuộc tính đó. Nếu dữ liệu mô phỏng dẫn đến điều kiện chỉ ra một trình giám sát chèn vào là không phù hợp với hành vi thiết kế, trình giám sát sẽ cảnh báo tới người thiết kế vấn đề đó. Như đã đề cập, chúng ta vẫn phải phát triển một testbench và thiết kế cẩn thần các đầu vào kiểm tra cho thiết kế cần kiểm tra là cần thiết cho kỹ thuật chèn để kiểm tra thiết kế. Nhưng trong nhiều trường hợp, kỹ thuật chèn tự động kiểm tra để chắc chắn sự kiện xảy ra trong thiết kế là đúng như mong đợi. Điều này có ý nghĩa làm giảm sự cần thiết cho việc xử lý một danh sách dài các đầu ra và dạng sóng. Kĩ thuật chèn (assertion) dùng để kiểm tra thiết kế Không giống như mô phỏng với một testbench hoặc con người để giải thích kết quả, trong kỹ thuật chèn để kiểm tra kết quả chương trình giám sát chịu trách nhiệm phát hành một thông báo nếu có một điều gì đó xảy ra không như mong đợi. Trong Verilog, các trình giám sát là các module, và chúng được khởi tạo trong một thiết kế để kiểm tra các thuộc tính của thiết kế. Thể hiện của một module chèn (assertion module) không được xem như là một module phần cứng. Thay vào đó, loại thể hiện này giống như một thủ tục luôn luôn hoạt động và liên tục kiểm tra các sự kiện trong module thiết kế. Thiết lập hiện tại của một trình giám sát chèn (assertion monitor) có sẵn trong một thư viện được biết đến như là một thư viện kiểm tra mở (OVL). Người thiết kế có thể phát triển các cài đặt riêng của họ vào trong module chèn. Những gì tồn tại trong trình giám sát kiểm tra giá trị của tín hiệu, quan hệ của một vài tín hiệu với các cái khác, sự tuần tự của các sự kiện, và các mô hình dự kiến trên vector hoặc nhóm tín hiệu. Để sử dụng kỹ thuật chèn, người thiết kế biên dịch OVL và thư viện có sẵn trong thiết kế cần kiểm tra. Khi một thiết kế được phát triển, kỹ thuật chèn sẽ thay thế các điểm cần thiết trong thiết kế đẻ kiểm tra các chức năng cần thiết. Khi thiết kế được mô phỏng như một thành phần đơn chuẩn, hoặc trong một cấu trúc phân cấp của một thiết kế lớn, trình giám sát kiểm tra tín hiệu cho các giá trị ngoại lệ. Nếu tín hiệu không có giá trị ngoại lệ bằng sự giám sát, trình giám sát chèn vào sẽ hiển thị một thông điệp và thời gian sự khác biệt (vi phạm của các thuộc tính) đã xảy ra. Thông thường, thông điệp xuất hiện trong vùng báo cáo của mô phỏng, bản dịch hoặc khung hiển thị điều khiển (console). Lợi ích của kỹ thuật chèn kiểm tra. Cách để tìm nơi để chèn một trình giám sát sao cho có lợi nhất sẽ được thảo luận trong phần này. Kỷ luật thiết kế: Khi một người thiết kế đặt một nơi để chèn trong thiết kế, người thiết kế cần phải tự yêu cầu bản thân mình xem xét cẩn thận thiết kế và trích xuất các thuộc tính cần thiết. Khả năng quan sát: Chèn thêm các trình giám sát vào các điểm cần giám sát của thiết kế làm sao cho dễ quan sát nhất. Quá trình kiểm tra chính thức sẵn sàng: Các chương trình chèn tương ứng với các thuộc tính được sử dụng trong công cụ kiểm tra chính thức. Có chèn vào một trình giám vào một thiết kế, sẵn sàng cho nó kiểm tra bằng công cụ kiểm tra thiết kế chính thức. Thực thi chú thích: Trình giám sát chèn vào có thể xem như là chú thích để chú thích một vài tính năng hoặc hành vi của thiết kế. Các chú thích này tạo ra một thông điệp khi hành vi của chúng được giải thích là vi phạm. Tự thiết kế kín: Một thiết kế với kỹ thuật chèn giám sát đã mô tả thiết kế và các thủ tục kiểm tra nó trong một module Verilog. Thư viện thiết kế mở (OVL) OVL có sẵn từ tổ chức Accellera ( và các tổ chức EDA khác. Hướng dẫn tham khảo ngôn ngữ, hướng dẫn sử dụng, và thư viện chương trình của Verilog và VHDL cũng có sẵn trong các tổ chức EDA này. Danh sách các chương trình chèn có sẵn được liệt kê trong danh sách sau: assert_change assert_decrement assert_even_parity assert_frame assert_implication assert_never assert_next assert_no_transition assert_odd_parity assert_one_hot assert_quiescent_state Một assertion được đặt trong chương trình giống như một thể hiện của module. Cấu trúc sau mô tả một khai báo thể hiện module assertion. Cú pháp 9-1 assert_name #(static_parameters) instance_name (dynamic_arguments); Nó bắt đầu với tên của module assertion, theo sau là các tham số tĩnh (satatic_parameters) như là kích thước của vector hoặc các tùy chọn. Sau đó là tên duy nhất bất kỳ của thể hiện, và phần cuối cùng là một trình giám sát chèn vào bao gồm các tham chiếu, giám sát tín hiệu và các đối số động khác. Các đối số động này là các cổng của module và cũng được xem như là các cổng của assertion module. Sử dụng kỹ thuật chèn giám sát. assert_always Cú pháp để sử dụng kỹ thuật chèn giám sát được mô tả như sau: Cú pháp 9-2 assert_always #( severity_level, property_type, msg, coverage_level ) instance_name ( clk, reset_n, test_expr ) Lệnh này sẽ liên tục chèn kiểm tra test_expr để chắc chắn nó luôn luôn đúng trên mỗi cạnh của clock. Nếu biểu thức kiểm tra sai, một thông điệp tương ứng sẽ được hiển thị. Ví dụ 9.13 module BCD_Counter (input rst, clk, outputreg [3:0] cnt); always @(posedge clk) begin if (rst || cnt >= 10) cnt = 0; else cnt = cnt + 1; end assert_always #(1, 0, “Err: Non BCD Count”, 0) AA1 (clk, 1’b1, (cnt >= 0) && (cnt <= 9)); endmodule Testbench để kiểm tra module: module BCD_Counter_Tester; reg r, c; wire [3:0] count; BCD_Counter UUT (r, c, count); initial begin r = 0; c = 0; end initial repeat (200) #17 c= ~c; initial repeat (03) #807 r= ~r; endmodule assert_change Lệnh chèn này giám sát kiểm tra trong một số chu kỳ đồng hồ sau sự kiện bắt đầu, biểu thức kiểm tra sẽ thay đổi, cú pháp được sử dụng như sau: Cú pháp 9-3 assert_change #( severity_level, width, num_cks, action_on_new_start, property_type, msg, coverage_level ) instance_name ( clk, reset_n, start_event, test_expr ) assert_one_hot Kỹ thuật chèn giám sát này dùng để kiểm tra chỉ một bit trong n bit của biểu thức kiểm tra là 1 trong khi trình giám sát vẫn đang hoạt động, cú pháp như sau: Cú pháp 9-4 assert_one_hot #( severity_level, width, property_type, msg, coverage_level ) instance_name ( clk, reset_n, test_expr ) assert_cycle_sequence Kỹ thuật chèn này dùng để kiểm tra máy trạng thái, cú pháp như sau: Cú pháp 9-5 assert_cycle_sequence #( severity_level, num_cks, necessary_condition, property_type, msg, coverage_level ) instance_name ( clk, reset_n, event_sequence ) assert_next: kỹ thuật chèn này sử dụng cú pháp bên dưới và kiểm tra các sự kiện xảy ra tại các chu kỳ đồng hồ ở giữa sự kiện bắt đầu và kết thúc: Cú pháp 9-6 assert_next #( severity_level, num_cks, check_overlapping, check_missing_start, property_type, msg, coverage_level ) instance_name ( clk, reset_n, start_event, test_expr ) Bài tập Tại sao phải kiểm tra thiết kế? Có mấy cách để kiểm tra thiết kế, nêu cụ thể? Phân biệt hai hình thức kiểm tra thiết kế sử dụng testbench và verification? Các kỹ thuật để tạo một testbench hiệu quả ? Viết testbench cho mạch tổ hợp và mạch tuần tự có gì khác nhau? Thế nào là chèn để kiểm tra thiết kế (assertion verification)? Lợi ích của kỹ thuật này? Thư viện mởi OVL bao gồm những câu lệnh chèn cơ bản nào và các sử dụng chúng?
File đính kèm:
- giao_trinh_ngon_ngu_mo_ta_phan_cung_verilog_vu_duc_lung.doc