assume用於做formal verification，如果輸入和assume不一樣，會出錯, 斷言（assert）可以用來檢查行為或者時序的正確性。

Mentor 的文件說的比較清楚

Example 2-7 defines two cut points (p and q) in order to explore a hard-to-prove assertion

(assert property (r_eq_s)) by reducing the problem to one that can be analyzed successfully.

The variables p and q are large arithmetic expressions, which are typically hard to analyze.

Suppose heuristic knowledge indicates p must be 3, 4 or 5. Then, by adding an assumption for this (i.e., assume property (values_of_p)), the assertion can be proven.

Example 2-7. User-defined Cut Point dut.v

module dut(clk, rst, a, b, c, d, e, f);

input clk, rst;

input [31:0] a,b,c,d,e,f;

wire [31:0] p,q,r,s;

assign p = a * b + (c - d) * (b - f) * (e*f);

assign q = d + e + f + e*e + f*f + a*a;

assign r = (p + 1) + (q - 1) + p;

assign s = 2*p + q;

property r_eq_s;

@(posedge clk) disable iff (rst) r==s;

endproperty

property values_of_p;

@(posedge clk) disable iff (rst) p==3 || p==4 || p==5;

endproperty

assert property (r_eq_s);

assume property (values_of_p);

endmodule