Add support for |=> inside properties (#1292).

Changes

@@ -32,6 +32,8 @@ The contributors that suggested a given feature are shown in []. Thanks!
 
 ****  Add support for assume property. [Peter Monsson]
 
+****  Add support for |=> inside properties (#1292). [Peter Monsson]
+
 
 * Verilator 4.040 2020-08-15
 

src/V3AssertPre.cpp

@@ -39,6 +39,8 @@ private:
     AstSenItem* m_senip = nullptr;  // Last sensitivity
     // Reset each always:
     AstSenItem* m_seniAlwaysp = nullptr;  // Last sensitivity in always
+    // Reset each assertion:
+    AstNode* m_disablep = nullptr;  // Last disable
 
     // METHODS
     VL_DEBUG_FUNC;  // Declare debug()
@@ -58,7 +60,10 @@ private:
         }
         return newp;
     }
-    void clearAssertInfo() { m_senip = nullptr; }
+    void clearAssertInfo() {
+        m_senip = nullptr;
+        m_disablep = nullptr;
+    }
 
     // VISITORS
     //========== Statements
@@ -130,7 +135,25 @@ private:
         AstNode* past = new AstPast(fl, exprp, nullptr);
         past->dtypeFrom(exprp);
         exprp = new AstEq(fl, past,
-                          exprp->cloneTree(false));  // new AstVarRef(fl, exprp, true)
+                          exprp->cloneTree(false));
+        exprp->dtypeSetLogicBool();
+        nodep->replaceWith(exprp);
+        nodep->sentreep(newSenTree(nodep));
+        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+    }
+
+    virtual void visit(AstImplication* nodep) override {
+        if (nodep->sentreep()) return;  // Already processed
+
+        FileLine* fl = nodep->fileline();
+        AstNode* rhsp = nodep->rhsp()->unlinkFrBack();
+        AstNode* lhsp = nodep->lhsp()->unlinkFrBack();
+
+        if (m_disablep) { lhsp = new AstAnd(fl, new AstNot(fl, m_disablep), lhsp); }
+
+        AstNode* past = new AstPast(fl, lhsp, nullptr);
+        past->dtypeFrom(lhsp);
+        AstNode* exprp = new AstOr(fl, new AstNot(fl, past), rhsp);
         exprp->dtypeSetLogicBool();
         nodep->replaceWith(exprp);
         nodep->sentreep(newSenTree(nodep));
@@ -145,6 +168,7 @@ private:
         // Block is the new expression to evaluate
         AstNode* blockp = nodep->propp()->unlinkFrBack();
         if (nodep->disablep()) {
+            m_disablep = nodep->disablep()->cloneTree(false);
             if (VN_IS(nodep->backp(), Cover)) {
                 blockp = new AstAnd(
                     nodep->disablep()->fileline(),

src/V3AstNodes.h

@@ -8244,6 +8244,32 @@ public:
     void isDefault(bool flag) { m_default = flag; }
 };
 
+class AstImplication : public AstNodeMath {
+    // Verilog |-> |=>
+    // Parents: math
+    // Children: expression
+public:
+    AstImplication(FileLine* fl, AstNode* lhs, AstNode* rhs)
+        : ASTGEN_SUPER(fl) {
+        setOp1p(lhs);
+        setOp2p(rhs);
+    }
+    ASTNODE_NODE_FUNCS(Implication)
+    virtual string emitVerilog() override { V3ERROR_NA_RETURN(""); }
+    virtual string emitC() override { V3ERROR_NA_RETURN(""); }
+    virtual string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
+    virtual bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
+    virtual int instrCount() const override { return widthInstrs(); }
+    AstNode* lhsp() const { return op1p(); }
+    AstNode* rhsp() const { return op2p(); }
+    void lhsp(AstNode* nodep) { return setOp1p(nodep); }
+    void rhsp(AstNode* nodep) { return setOp2p(nodep); }
+    AstSenTree* sentreep() const { return VN_CAST(op4p(), SenTree); }  // op4 = clock domain
+    void sentreep(AstSenTree* sentreep) { addOp4p(sentreep); }  // op4 = clock domain
+    virtual V3Hash sameHash() const override { return V3Hash(); }
+    virtual bool same(const AstNode* samep) const override { return true; }
+};
+
 //======================================================================
 // Assertions
 

src/V3Width.cpp

@@ -1101,6 +1101,14 @@ private:
         }
     }
 
+    virtual void visit(AstImplication* nodep) override {
+        if (m_vup->prelim()) {
+            iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH);
+            iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH);
+            nodep->dtypeSetLogicBool();
+        }
+    }
+
     virtual void visit(AstRand* nodep) override {
         if (m_vup->prelim()) {
             nodep->dtypeSetSigned32();  // Says the spec

src/verilog.y

@@ -5268,7 +5268,7 @@ pexpr<nodep>:  // IEEE: property_expr  (The name pexpr is important as regexps j
 	//UNSUP: This rule has been super-specialized to what is supported now
 	//UNSUP remove below
 		expr yP_ORMINUSGT pexpr			{ $$ = new AstLogOr($2, new AstLogNot($2, $1), $3); }
-	//UNSUP	expr yP_OREQGT pexpr			{ $$ = new AstLogOr($2, new AstLogNot($2, new AstPast($2, $1, nullptr)), $3); } // This handles disable iff in the past time step incorrectly
+	|	expr yP_OREQGT pexpr			{ $$ = new AstImplication($2, $1, $3); }
 	|	expr					{ $$ = $1; }
 	//UNSUP remove above, use below:
 	//

test_regress/t/t_assert_implication.v

@@ -14,11 +14,15 @@ module t (/*AUTOARG*/
 
    Test test (/*AUTOINST*/
               // Inputs
-              .clk                      (clk));
+              .clk(clk),
+              .cyc(cyc));
 
    always @ (posedge clk) begin
       if (cyc!=0) begin
          cyc <= cyc + 1;
+`ifdef TEST_VERBOSE
+         $display("cyc=%0d", cyc);
+`endif
          if (cyc==10) begin
             $write("*-* All Finished *-*\n");
             $finish;
@@ -30,7 +34,8 @@ endmodule
 
 module Test
   (
-   input clk
+   input clk,
+   input integer cyc
    );
 
 `ifdef FAIL_ASSERT_1
@@ -38,8 +43,35 @@ module Test
      @(posedge clk)
      1 |-> 0
    ) else $display("[%0t] wrong implication", $time);
+
+   assert property (
+     @(posedge clk)
+     1 |=> 0
+   ) else $display("[%0t] wrong implication", $time);
+
+   assert property (
+     @(posedge clk)
+     cyc%3==1 |=> cyc%3==1
+   ) else $display("[%0t] wrong implication (step)", $time);
+
+   assert property (
+     @(posedge clk)
+     cyc%3==1 |=> cyc%3==0
+   ) else $display("[%0t] wrong implication (step)", $time);
+
+   assert property (
+     @(posedge clk) disable iff (cyc == 3)
+     (cyc == 4) |=> 0
+   ) else $display("[%0t] wrong implication (disable)", $time);
+
+   assert property (
+     @(posedge clk) disable iff (cyc == 6)
+     (cyc == 4) |=> 0
+   ) else $display("[%0t] wrong implication (disable)", $time);
+
 `endif
 
+   // Test |->
    assert property (
      @(posedge clk)
      1 |-> 1
@@ -55,4 +87,44 @@ module Test
      0 |-> 1
    );
 
+   // Test |=>
+   assert property (
+     @(posedge clk)
+     1 |=> 1
+   );
+
+   assert property (
+     @(posedge clk)
+     0 |=> 0
+   );
+
+   assert property (
+     @(posedge clk)
+     0 |=> 1
+   );
+
+   // Test correct handling of time step in |=>
+   assert property (
+     @(posedge clk)
+     cyc%3==1 |=> cyc%3==2
+   );
+
+   // Test correct handling of disable iff
+   assert property (
+     @(posedge clk) disable iff (cyc < 3)
+     1 |=> cyc > 3
+   );
+
+   // Test correct handling of disable iff in current cycle
+   assert property (
+     @(posedge clk) disable iff (cyc == 4)
+     (cyc == 4) |=> 0
+   );
+
+   // Test correct handling of disable iff in previous cycle
+   assert property (
+     @(posedge clk) disable iff (cyc == 5)
+     (cyc == 4) |=> 0
+   );
+
 endmodule