Support $sampled (#3569)

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

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 {

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;
 };
 

src/verilog.y

@@ -5313,10 +5313,12 @@ concurrent_assertion_item<nodep>:       // IEEE: concurrent_assertion_item
 concurrent_assertion_statement<nodep>:  // ==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); }

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;

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

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;

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

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

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;

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

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;

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

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

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;

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