SV中|-＞ 和 |=＞的区别与关系

在 SystemVerilog 断言SVA中|-和|都是蕴含操作符用于连接前提条件antecedent和后续条件consequent。它们的核心区别在于检查后续条件的起始时间点。1. 重叠蕴含|-含义若前提条件在当前时钟周期成立则在同一时钟周期开始检查后续条件。时间关系前提和后续的第一个时钟周期重叠。示例property p_overlap; (posedge clk) a |- b; endproperty当a在时钟周期T为真则在同一个周期T检查b是否为真。如果后续条件是一个序列如##1 c则从周期T开始匹配序列b在T周期成立c在T1周期成立。2. 非重叠蕴含|含义若前提条件在当前时钟周期成立则从下一个时钟周期开始检查后续条件。时间关系前提和后续的第一个时钟周期间隔一个周期。示例property p_nonoverlap; (posedge clk) a | b; endproperty当a在周期T为真则在下一个周期T1检查b是否为真。这等价于a |- ##1 b。3. 对比表操作符后续检查起始点等价写法典型应用场景|-同一周期a |- b需在同一周期内检查的关系|下一周期a |- ##1 b需延迟一拍后才发生的关系4. 举例说明假设一个简单的协议请求req拉高后同一周期内允许gnt为高流水线响应或者下一个周期gnt必须为高。使用|-检查立即响应req |- gnt; // gnt 必须在 req 的同一周期有效使用|检查延迟响应req | gnt; // gnt 必须在 req 的下一周期有效5. 注意事项序列嵌套后续条件可以是复杂序列。|-序列的起点是当前周期|的起点是下一周期。多周期延迟若需要延迟多拍推荐用|- ##n ...更清晰。|仅用于正好一拍延迟。常见错误混淆两者会导致断言在错误的时间点检查产生误报或漏报。总结用|-前提满足后立即检查后续同一周期开始。用|前提满足后下一拍才开始检查后续。选择哪个取决于设计时序响应是组合逻辑路径同拍还是寄存输出下一拍。