diff --git a/docs/CONTRIBUTORS b/docs/CONTRIBUTORS index 5f2441d2d..b8f55e112 100644 --- a/docs/CONTRIBUTORS +++ b/docs/CONTRIBUTORS @@ -5,6 +5,7 @@ Please see the Verilator manual for 200+ additional contributors. Thanks to all. Adrien Le Masle Ahmed El-Mahmoudy +Aleksander Kiryk Alex Chadwick Àlex Torregrosa Aliaksei Chapyzhenka diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 86e8710a8..5a46f1ad9 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -45,6 +45,7 @@ private: VDouble0 m_statAsNotImm; // Statistic tracking VDouble0 m_statAsImm; // Statistic tracking VDouble0 m_statAsFull; // Statistic tracking + bool m_inSampled = false; // True inside a sampled expression // METHODS string assertDisplayMessage(AstNode* nodep, const string& prefix, const string& message) { @@ -66,6 +67,11 @@ private: nodep->fmtp()->scopeNamep(new AstScopeName{nodep->fileline(), true}); } } + AstSampled* newSampledExpr(AstNode* nodep) { + const auto sampledp = new AstSampled{nodep->fileline(), nodep}; + sampledp->dtypeFrom(nodep); + return sampledp; + } AstVarRef* newMonitorNumVarRefp(AstNode* nodep, VAccess access) { if (!m_monitorNumVarp) { m_monitorNumVarp = new AstVar{nodep->fileline(), VVarType::MODULETEMP, "__VmonitorNum", @@ -332,7 +338,8 @@ private: ticks = VN_AS(nodep->ticksp(), Const)->toUInt(); } UASSERT_OBJ(ticks >= 1, nodep, "0 tick should have been checked in V3Width"); - AstNode* inp = nodep->exprp()->unlinkFrBack(); + AstNode* const exprp = nodep->exprp()->unlinkFrBack(); + AstNode* inp = newSampledExpr(exprp); AstVar* invarp = nullptr; AstSenTree* const sentreep = nodep->sentreep(); sentreep->unlinkFrBack(); @@ -353,10 +360,41 @@ private: } nodep->replaceWith(inp); } + + //========== Move $sampled down to read-only variables virtual void visit(AstSampled* nodep) override { + if (nodep->user1()) return; + VL_RESTORER(m_inSampled); + { + m_inSampled = true; + iterateChildren(nodep); + } nodep->replaceWith(nodep->exprp()->unlinkFrBack()); VL_DO_DANGLING(pushDeletep(nodep), nodep); } + virtual void visit(AstVarRef* nodep) override { + iterateChildren(nodep); + if (m_inSampled) { + if (!nodep->access().isReadOnly()) { + nodep->v3warn(E_UNSUPPORTED, + "Unsupported: Write to variable in sampled expression"); + } else { + VNRelinker relinkHandle; + nodep->unlinkFrBack(&relinkHandle); + AstSampled* const newp = newSampledExpr(nodep); + relinkHandle.relink(newp); + newp->user1(1); + } + } + } + // Don't sample sensitivities + virtual void visit(AstSenItem* nodep) override { + VL_RESTORER(m_inSampled); + { + m_inSampled = false; + iterateChildren(nodep); + } + } //========== Statements virtual void visit(AstDisplay* nodep) override { diff --git a/src/V3Clock.cpp b/src/V3Clock.cpp index 0b5a62730..be1dec524 100644 --- a/src/V3Clock.cpp +++ b/src/V3Clock.cpp @@ -72,8 +72,11 @@ public: class ClockVisitor final : public VNVisitor { private: // STATE + AstCFunc* m_evalp = nullptr; // The '_eval' function + AstScope* m_scopep = nullptr; // Current scope AstSenTree* m_lastSenp = nullptr; // Last sensitivity match, so we can detect duplicates. AstIf* m_lastIfp = nullptr; // Last sensitivity if active to add more under + bool m_inSampled = false; // True inside a sampled expression // METHODS VL_DEBUG_FUNC; // Declare debug() @@ -87,6 +90,25 @@ private: } return senEqnp; } + AstVarScope* createSampledVar(AstVarScope* vscp) { + if (vscp->user1p()) return VN_AS(vscp->user1p(), VarScope); + const AstVar* const varp = vscp->varp(); + const string newvarname + = string("__Vsampled__") + vscp->scopep()->nameDotless() + "__" + varp->name(); + FileLine* const flp = vscp->fileline(); + AstVar* const newvarp = new AstVar{flp, VVarType::MODULETEMP, newvarname, varp->dtypep()}; + newvarp->noReset(true); // Reset by below assign + m_scopep->modp()->addStmtp(newvarp); + AstVarScope* const newvscp = new AstVarScope{flp, m_scopep, newvarp}; + vscp->user1p(newvscp); + m_scopep->addVarp(newvscp); + // At the top of _eval, assign them + AstAssign* const finalp = new AstAssign{flp, new AstVarRef{flp, newvscp, VAccess::WRITE}, + new AstVarRef{flp, vscp, VAccess::READ}}; + m_evalp->addInitsp(finalp); + UINFO(4, "New Sampled: " << newvscp << endl); + return newvscp; + } AstIf* makeActiveIf(AstSenTree* sensesp) { AstNode* const senEqnp = createSenseEquation(sensesp->sensesp()); UASSERT_OBJ(senEqnp, sensesp, "No sense equation, shouldn't be in sequent activation."); @@ -151,12 +173,45 @@ private: clearLastSen(); } + //========== Create sampled values + virtual void visit(AstScope* nodep) override { + VL_RESTORER(m_scopep); + { + m_scopep = nodep; + iterateChildren(nodep); + } + } + virtual void visit(AstSampled* nodep) override { + VL_RESTORER(m_inSampled); + { + m_inSampled = true; + iterateChildren(nodep); + nodep->replaceWith(nodep->exprp()->unlinkFrBack()); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } + } + virtual void visit(AstVarRef* nodep) override { + iterateChildren(nodep); + if (m_inSampled && !nodep->user1SetOnce()) { + UASSERT_OBJ(nodep->access().isReadOnly(), nodep, "Should have failed in V3Access"); + AstVarScope* const varscp = nodep->varScopep(); + AstVarScope* const lastscp = createSampledVar(varscp); + AstNode* const newp = new AstVarRef{nodep->fileline(), lastscp, VAccess::READ}; + newp->user1SetOnce(); // Don't sample this one + nodep->replaceWith(newp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } + } + //-------------------- virtual void visit(AstNode* nodep) override { iterateChildren(nodep); } public: // CONSTRUCTORS - explicit ClockVisitor(AstNetlist* netlistp) { iterate(netlistp); } + explicit ClockVisitor(AstNetlist* netlistp) { + m_evalp = netlistp->evalp(); + iterate(netlistp); + } virtual ~ClockVisitor() override = default; }; diff --git a/src/verilog.y b/src/verilog.y index 938a2e82f..0362db208 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -5313,10 +5313,12 @@ concurrent_assertion_item: // IEEE: concurrent_assertion_item concurrent_assertion_statement: // ==IEEE: concurrent_assertion_statement // // IEEE: assert_property_statement //UNSUP remove below: - yASSERT yPROPERTY '(' property_spec ')' elseStmtBlock { $$ = new AstAssert($1, $4, nullptr, $6, false); } + yASSERT yPROPERTY '(' property_spec ')' elseStmtBlock + { $$ = new AstAssert{$1, new AstSampled{$1, $4}, nullptr, $6, false}; } //UNSUP yASSERT yPROPERTY '(' property_spec ')' action_block { } // // IEEE: assume_property_statement - | yASSUME yPROPERTY '(' property_spec ')' elseStmtBlock { $$ = new AstAssert($1, $4, nullptr, $6, false); } + | yASSUME yPROPERTY '(' property_spec ')' elseStmtBlock + { $$ = new AstAssert{$1, new AstSampled{$1, $4}, nullptr, $6, false}; } //UNSUP yASSUME yPROPERTY '(' property_spec ')' action_block { } // // IEEE: cover_property_statement | yCOVER yPROPERTY '(' property_spec ')' stmtBlock { $$ = new AstCover($1, $4, $6, false); } diff --git a/test_regress/t/t_assert_past.pl b/test_regress/t/t_assert_past.pl new file mode 100755 index 000000000..c505d6263 --- /dev/null +++ b/test_regress/t/t_assert_past.pl @@ -0,0 +1,22 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Antmicro Ltd. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(simulator => 1); + +compile( + verilator_flags2 => ['--assert'], + ); + +execute( + check_finished => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_past.v b/test_regress/t/t_assert_past.v new file mode 100644 index 000000000..df6c6a920 --- /dev/null +++ b/test_regress/t/t_assert_past.v @@ -0,0 +1,28 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2022 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + clk + ); + input clk; + int cyc = 0; + logic val = 0; + // Example: + always @(posedge clk) begin + cyc <= cyc + 1; + val = ~val; + $display("t=%0t cyc=%0d val=%b", $time, cyc, val); + if (cyc == 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + assert property(@(posedge clk) cyc % 2 == 0 |=> $past(val) == 0) + else $display("$past assert 1 failed"); + assert property(@(posedge clk) cyc % 2 == 1 |=> $past(val) == 1) + else $display("$past assert 2 failed"); + // Example end +endmodule diff --git a/test_regress/t/t_assert_sampled.pl b/test_regress/t/t_assert_sampled.pl new file mode 100755 index 000000000..c505d6263 --- /dev/null +++ b/test_regress/t/t_assert_sampled.pl @@ -0,0 +1,22 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Antmicro Ltd. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(simulator => 1); + +compile( + verilator_flags2 => ['--assert'], + ); + +execute( + check_finished => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_assert_sampled.v b/test_regress/t/t_assert_sampled.v new file mode 100644 index 000000000..49c7cc71e --- /dev/null +++ b/test_regress/t/t_assert_sampled.v @@ -0,0 +1,56 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2022 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk + ); + input clk; + + reg [3:0] a, b; + + Test1 t1(clk, a, b); + Test2 t2(clk, a, b); + + initial begin + a = 0; + b = 0; + end + + always @(posedge clk) begin + a <= a + 1; + b = b + 1; + + $display("a = %0d, b = %0d, %0d == %0d", a, b, $sampled(a), $sampled(b)); + + if (b >= 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule + +module Test1( + clk, a, b + ); + + input clk; + input [3:0] a, b; + + assert property (@(posedge clk) $sampled(a) == $sampled(b)); + +endmodule + +module Test2( + clk, a, b + ); + + input clk; + input [3:0] a, b; + + assert property (@(posedge clk) a == b); + +endmodule diff --git a/test_regress/t/t_past_strobe.out b/test_regress/t/t_past_strobe.out new file mode 100644 index 000000000..9df6ce6ca --- /dev/null +++ b/test_regress/t/t_past_strobe.out @@ -0,0 +1,11 @@ +1 == 1, 0 == 0 +2 == 2, 1 == 1 +3 == 3, 2 == 2 +4 == 4, 3 == 3 +5 == 5, 4 == 4 +6 == 6, 5 == 5 +7 == 7, 6 == 6 +8 == 8, 7 == 7 +9 == 9, 8 == 8 +*-* All Finished *-* +10 == 10, 9 == 9 diff --git a/test_regress/t/t_past_strobe.pl b/test_regress/t/t_past_strobe.pl new file mode 100755 index 000000000..4bbe254e3 --- /dev/null +++ b/test_regress/t/t_past_strobe.pl @@ -0,0 +1,22 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Antmicro Ltd. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(simulator => 1); + +compile( + ); + +execute( + check_finished => 1, + expect_filename => $Self->{golden_filename}, + ); + +ok(1); +1; diff --git a/test_regress/t/t_past_strobe.v b/test_regress/t/t_past_strobe.v new file mode 100644 index 000000000..b7e58466a --- /dev/null +++ b/test_regress/t/t_past_strobe.v @@ -0,0 +1,44 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2022 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk + ); + input clk; + + reg [3:0] a, b; + + Test1 t1(clk, a, b); + + initial begin + a = 0; + b = 0; + end + + always @(posedge clk) begin + a <= a + 1; + b = b + 1; + + if (b >= 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule + +module Test1( + clk, a, b + ); + + input clk; + input [3:0] a, b; + + always @(posedge clk) begin + $strobe("%0d == %0d, %0d == %0d", a, b, $past(a), $past(b)); + end + +endmodule diff --git a/test_regress/t/t_sampled_expr.pl b/test_regress/t/t_sampled_expr.pl new file mode 100755 index 000000000..c505d6263 --- /dev/null +++ b/test_regress/t/t_sampled_expr.pl @@ -0,0 +1,22 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Antmicro Ltd. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(simulator => 1); + +compile( + verilator_flags2 => ['--assert'], + ); + +execute( + check_finished => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_sampled_expr.v b/test_regress/t/t_sampled_expr.v new file mode 100644 index 000000000..9447b48f8 --- /dev/null +++ b/test_regress/t/t_sampled_expr.v @@ -0,0 +1,68 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2022 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk + ); + input clk; + + reg [3:0] a, b; + + Test1 t1(clk, a, b); + Test2 t2(clk, a, b); + Test3 t3(clk); + + initial begin + a = 0; + b = 0; + end + + always @(posedge clk) begin + a <= a + 1; + b = b + 1; + + $display("a = %0d, b = %0d, %0d == %0d", a, b, $sampled(a), $sampled(b)); + + if (b >= 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule + +module Test1( + clk, a, b + ); + + input clk; + input [3:0] a, b; + + assert property (@(posedge clk) $sampled(a == b) == ($sampled(a) == $sampled(b))); +endmodule + +module Test2( + clk, a, b + ); + + input clk; + input [3:0] a, b; + + assert property (@(posedge clk) eq(a, b)); + + function [0:0] eq([3:0] x, y); + return x == y; + endfunction +endmodule + +module Test3( + clk + ); + + input clk; + + assert property (@(posedge clk) $sampled($time) == $time); +endmodule diff --git a/test_regress/t/t_sampled_expr_unsup.out b/test_regress/t/t_sampled_expr_unsup.out new file mode 100644 index 000000000..170ef48f8 --- /dev/null +++ b/test_regress/t/t_sampled_expr_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_sampled_expr_unsup.v:34:36: Unsupported: Write to variable in sampled expression + : ... In instance t.t1 + 34 | assert property (@(posedge clk) a++ >= 0); + | ^ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_sampled_expr_unsup.pl b/test_regress/t/t_sampled_expr_unsup.pl new file mode 100755 index 000000000..24a95330a --- /dev/null +++ b/test_regress/t/t_sampled_expr_unsup.pl @@ -0,0 +1,20 @@ +#!/usr/bin/env perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2022 by Antmicro Ltd. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +scenarios(vlt => 1); + +compile( + expect_filename=>$Self->{golden_filename}, + verilator_flags2=> ['--assert -Wno-UNSIGNED'], + fails => 1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_sampled_expr_unsup.v b/test_regress/t/t_sampled_expr_unsup.v new file mode 100644 index 000000000..1e8eb9de2 --- /dev/null +++ b/test_regress/t/t_sampled_expr_unsup.v @@ -0,0 +1,35 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2022 by Antmicro Ltd. +// SPDX-License-Identifier: CC0-1.0 + +module t (/*AUTOARG*/ + // Inputs + clk + ); + input clk; + + integer cyc; + + Test1 t1(clk); + + always @(posedge clk) begin + cyc <= cyc + 1; + + if (cyc >= 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule + +module Test1( + clk + ); + + input clk; + reg [3:0] a = 0; + + assert property (@(posedge clk) a++ >= 0); +endmodule