请问一下systemverilog 断言中assume 和assert的区别

一点点浅薄的理解，断言（assert）可以用来检查行为或者时序的正确性。
对assume没太听过。期待下文！

assume用于做formal verification，如果输入和assume不一样，会出错

formal verification 一般不都是用工具formality直接完成吗，assume怎么进行形式验证呢，能不能举个例子，多谢

形式验证分 也分种类吧。具体不是很了解，可以去看下cadence ifv的文档

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

多谢

6L说的这个文档是哪个文档啊? 多谢~

哥哥们，你们倒是通俗易懂的说一下到底什么区别啊。
在网上查来查去，要么就是3楼，要么就是6楼答案。
to3楼：assume是用来做形式验证的，但是看6楼的例子里是这样么?
to6楼：如果属性values_of_p用assert去检查，结果会有什么不同么?

醉了，醉了。断言的书上还没有给解释assume的，啊啊好烦

SystemVerilog 上的解释：
The immediateassume statement specifies that its expression is assumed to hold. For example, immediate
assume statements can be used with formal verification tools to specify assumptions on design inputs that
constrain the verification computation. When used in this way, they specify the expected behavior of the
environment of the design as opposed to that of the design itself. In simulation, an immediate assume may
behave as an immediateassert to verify that the environment behaves as assumed. A simulation tool shall
provide the capability to check the immediateassume statement in this way.

仿真时，assert与assume用途一样
形式验证时，assume可用于约束DUT的输入，用于过滤不需要的时序组合

6楼的例子就是这样assume用于约束p，防止状态爆炸

LOUZHUJIAYOU

assume 相当于约束, 就是假设条件成立