SVA断言编译语法错误排查：@、full/empty附近报错原因咨询

原错误代码 #

assert property @(posedge(clk)) !rstN |-> n==0 && full==0 && empty==1;
assert property @(posedge clk) disable iff(!rstN) ( full |->(wr_en  && $stable (n) ) );
assert property @(posedge clk) disable iff(!rstN) (empty |->(rd_en && $stable (n)) );

报错情况 #

• 所有@符号附近存在语法错误
• full、empty附近的左括号位置存在语法错误

具体问题及修正方案 #

1. 时钟事件的括号误用 #

SVA规定posedge后接时钟信号时，不需要额外给时钟加括号。第一个断言里的@(posedge(clk))写法违规，正确格式是@(posedge clk)，这是@附近报错的核心原因。

2. 蕴含操作符|->的格式错误 #

• disable iff块内的属性表达式不需要额外套外层括号；
• |->的右操作数括号要紧跟操作符，不能留空格，同时左操作数无需用括号包裹。

比如原代码中( full |->(wr_en && $stable (n) ) )的外层括号冗余，且|->与后续括号间的空格不符合语法要求，正确写法应为full |-> (wr_en && $stable(n))。

修正后的代码 #

assert property @(posedge clk) !rstN |-> n==0 && full==0 && empty==1;
assert property @(posedge clk) disable iff(!rstN) full |-> (wr_en && $stable(n));
assert property @(posedge clk) disable iff(!rstN) empty |-> (rd_en && $stable(n));

内容的提问来源于stack exchange，提问作者Amala Joseph