From 9e744fb396ecbae385ae5fac586cfeca812c9fc9 Mon Sep 17 00:00:00 2001 From: Todd Strader Date: Wed, 1 Apr 2026 10:27:38 -0400 Subject: [PATCH 1/2] support nexttime --- src/verilog.y | 2 +- test_regress/t/t_assert_nexttime.py | 18 +++++ test_regress/t/t_assert_nexttime.v | 27 +++++++ test_regress/t/t_property_pexpr_unsup.out | 90 ++++++++++------------- test_regress/t/t_property_pexpr_unsup.v | 4 - 5 files changed, 85 insertions(+), 56 deletions(-) create mode 100755 test_regress/t/t_assert_nexttime.py create mode 100644 test_regress/t/t_assert_nexttime.v diff --git a/src/verilog.y b/src/verilog.y index acf14048c..f3348c45c 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6739,7 +6739,7 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex | ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr { $$ = $1; BBUNSUP($2, "Unsupported: #=# (in property expression)"); DEL($3); } | yNEXTTIME pexpr - { $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); } + { $$ = new AstImplication{$1, new AstConst{$1, AstConst::BitTrue{}}, $2, false}; } | yS_NEXTTIME pexpr { $$ = $2; BBUNSUP($1, "Unsupported: s_nexttime (in property expression)"); } | yNEXTTIME '[' constExpr ']' pexpr %prec yNEXTTIME diff --git a/test_regress/t/t_assert_nexttime.py b/test_regress/t/t_assert_nexttime.py new file mode 100755 index 000000000..c6cbe37ab --- /dev/null +++ b/test_regress/t/t_assert_nexttime.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios("simulator") + +test.compile(verilator_flags2=["--assert"], nc_flags2=["+assert"]) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_nexttime.v b/test_regress/t/t_assert_nexttime.v new file mode 100644 index 000000000..473cae787 --- /dev/null +++ b/test_regress/t/t_assert_nexttime.v @@ -0,0 +1,27 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Wilson Snyder +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk + ); + + input clk; + int cyc = 0; + + always @(posedge clk) begin + cyc <= cyc + 1; + end + + assert property (@(posedge clk) nexttime (cyc > 0)); + + always @(posedge clk) begin + if (cyc == 20) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index 72bf6e6d1..0411c5fb8 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/test_regress/t/t_property_pexpr_unsup.out @@ -23,23 +23,23 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:51:7: Unsupported: #=# (in property expression) 51 | a #=# b; | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:55:5: Unsupported: nexttime (in property expression) - 55 | nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:55:5: Unsupported: nexttime[] (in property expression) + 55 | nexttime [2] a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:59:5: Unsupported: nexttime[] (in property expression) - 59 | nexttime [2] a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime (in property expression) - 63 | s_nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:59:5: Unsupported: s_nexttime (in property expression) + 59 | s_nexttime a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: s_nexttime[] (in property expression) - 67 | s_nexttime [2] a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime[] (in property expression) + 63 | s_nexttime [2] a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:14: Unsupported: always (in property expression) - 71 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:14: Unsupported: always (in property expression) + 67 | nexttime always a; | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime (in property expression) - 71 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:18: Unsupported: always (in property expression) + 71 | nexttime [2] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime[] (in property expression) + 71 | nexttime [2] always a; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:18: Unsupported: always (in property expression) 75 | nexttime [2] always a; @@ -47,55 +47,43 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:5: Unsupported: nexttime[] (in property expression) 75 | nexttime [2] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:18: Unsupported: always (in property expression) - 79 | nexttime [2] always a; - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime[] (in property expression) - 79 | nexttime [2] always a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually (in property expression) - 83 | nexttime s_eventually a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:14: Unsupported: s_eventually (in property expression) + 79 | nexttime s_eventually a; | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:5: Unsupported: nexttime (in property expression) - 83 | nexttime s_eventually a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:33: Unsupported: always (in property expression) - 87 | nexttime s_eventually [2:$] always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:33: Unsupported: always (in property expression) + 83 | nexttime s_eventually [2:$] always a; | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:14: Unsupported: s_eventually[] (in property expression) - 87 | nexttime s_eventually [2:$] always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually[] (in property expression) + 83 | nexttime s_eventually [2:$] always a; | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:5: Unsupported: nexttime (in property expression) - 87 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:91:15: Unsupported: accept_on (in property expression) - 91 | accept_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:15: Unsupported: accept_on (in property expression) + 87 | accept_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:95:20: Unsupported: sync_accept_on (in property expression) - 95 | sync_accept_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:91:20: Unsupported: sync_accept_on (in property expression) + 91 | sync_accept_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:15: Unsupported: reject_on (in property expression) - 99 | reject_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:95:15: Unsupported: reject_on (in property expression) + 95 | reject_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:103:20: Unsupported: sync_reject_on (in property expression) - 103 | sync_reject_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:20: Unsupported: sync_reject_on (in property expression) + 99 | sync_reject_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:106:26: Unsupported: property argument data type - 106 | property p_arg_propery(property inprop); +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:26: Unsupported: property argument data type + 102 | property p_arg_propery(property inprop); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:109:26: Unsupported: sequence argument data type - 109 | property p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:105:26: Unsupported: sequence argument data type + 105 | property p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:114:5: Unsupported: property case expression - 114 | case (a) endcase +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:110:5: Unsupported: property case expression + 110 | case (a) endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:5: Unsupported: property case expression - 117 | case (a) default: b; endcase +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:113:5: Unsupported: property case expression + 113 | case (a) default: b; endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:5: Unsupported: property case expression - 120 | if (a) b +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:116:5: Unsupported: property case expression + 116 | if (a) b | ^~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:5: Unsupported: property case expression - 123 | if (a) b else c +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:119:5: Unsupported: property case expression + 119 | if (a) b else c | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_pexpr_unsup.v b/test_regress/t/t_property_pexpr_unsup.v index 2acbb3b40..508dbc0fb 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/test_regress/t/t_property_pexpr_unsup.v @@ -51,10 +51,6 @@ module t ( a #=# b; endproperty - property p_nexttime; - nexttime a; - endproperty - property p_nexttime2; nexttime [2] a; endproperty From ec90294e9f562a5571717a9e9510bdf1332db722 Mon Sep 17 00:00:00 2001 From: Todd Strader Date: Thu, 2 Apr 2026 15:11:13 -0400 Subject: [PATCH 2/2] CR -> CRC --- test_regress/t/t_assert_nexttime.v | 64 ++++++++++++++++++++++-------- 1 file changed, 48 insertions(+), 16 deletions(-) diff --git a/test_regress/t/t_assert_nexttime.v b/test_regress/t/t_assert_nexttime.v index 473cae787..9e9d1c6f9 100644 --- a/test_regress/t/t_assert_nexttime.v +++ b/test_regress/t/t_assert_nexttime.v @@ -4,24 +4,56 @@ // SPDX-FileCopyrightText: 2026 Wilson Snyder // SPDX-License-Identifier: CC0-1.0 -module t (/*AUTOARG*/ - // Inputs - clk - ); +// verilog_format: off +`define stop $stop +`define checkh(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on - input clk; - int cyc = 0; +module t ( + input clk +); + integer cyc = 0; + reg [63:0] crc = '0; + reg [63:0] sum = '0; - always @(posedge clk) begin - cyc <= cyc + 1; - end + // Derive test signals from CRC + wire a = crc[0]; + wire b = crc[1]; + wire c = crc[2]; + wire d = crc[3]; - assert property (@(posedge clk) nexttime (cyc > 0)); + // Aggregate outputs into a single result vector + wire [63:0] result = {60'h0, d, c, b, a}; + + always_ff @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", + $time, cyc, crc, a, b, c, d); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + sum <= result ^ {sum[62:0], sum[63] ^ sum[2] ^ sum[0]}; + + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + sum <= '0; + end else if (cyc < 10) begin + sum <= '0; + end else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091) + `checkh(sum, 64'hdb7bc8bfe61f987e) + $write("*-* All Finished *-*\n"); + $finish; + end + end + + // ========================================================================= + // nexttime: property must hold at the next clock tick + // ========================================================================= + + assert property (@(posedge clk) nexttime (1'b1)); + assert property (@(posedge clk) nexttime (cyc > 0)); + assert property (@(posedge clk) disable iff (b) nexttime ~c); + assert property (@(posedge clk) disable iff (~b) nexttime c); - always @(posedge clk) begin - if (cyc == 20) begin - $write("*-* All Finished *-*\n"); - $finish; - end - end endmodule