From b89d29cab996aa9f9a4a55b5f5b23791d79f6c6e Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Thu, 5 Mar 2026 20:03:48 -0500 Subject: [PATCH] * Support procedural concurrent assertion simple cases (#6944). Fixes #6944. --- Changes | 1 + src/V3Assert.cpp | 37 +++++++++------ src/V3AssertPre.cpp | 14 ++++-- src/V3AstNodeStmt.h | 28 ++++++----- src/V3AstNodes.cpp | 8 +++- src/V3EmitV.cpp | 6 +-- src/V3Global.cpp | 5 +- src/V3Global.h | 4 +- test_regress/t/t_assert_procedural.py | 18 +++++++ test_regress/t/t_assert_procedural.v | 68 +++++++++++++++++++++++++++ test_regress/t/t_cover_assert.out | 6 --- test_regress/t/t_cover_assert.py | 6 +-- test_regress/t/t_dump_json.out | 50 ++++++++++---------- 13 files changed, 178 insertions(+), 73 deletions(-) create mode 100755 test_regress/t/t_assert_procedural.py create mode 100644 test_regress/t/t_assert_procedural.v delete mode 100644 test_regress/t/t_cover_assert.out diff --git a/Changes b/Changes index 3473599e2..c166d65f0 100644 --- a/Changes +++ b/Changes @@ -16,6 +16,7 @@ Verilator 5.047 devel * Support inout inside SV interface (#3466) (#7134). [Nick Brereton] * Support array reduction methods with 'with' clause in constraints (#6455) (#6999). [Rahul Behl] * Support constraint imperfect distributions (#6811) (#7168). [Yilou Wang] +* Support procedural concurrent assertion simple cases (#6944). * Support force assignments to array elements of real type (#7048). [Ryszard Rozak, Antmicro Ltd.] * Support VPI array indexing in signal names (#7097) (#7187). [Christian Hecken] * Support soft constraint solving (#7124) (#7166). [Yilou Wang] diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index e3f1a1cd6..c844ebaaf 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -139,7 +139,7 @@ class AssertVisitor final : public VNVisitor { AstVar* m_monitorOffVarp = nullptr; // $monitoroff variable unsigned m_modPastNum = 0; // Module past numbering unsigned m_modStrobeNum = 0; // Module $strobe numbering - const AstNodeProcedure* m_procedurep = nullptr; // Current procedure + AstNodeProcedure* m_procedurep = nullptr; // Current procedure VDouble0 m_statCover; // Statistic tracking VDouble0 m_statAsNotImm; // Statistic tracking VDouble0 m_statAsImm; // Statistic tracking @@ -308,7 +308,7 @@ class AssertVisitor final : public VNVisitor { } else { bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp); } - return newIfAssertOn(bodyp, nodep->directive(), nodep->type()); + return newIfAssertOn(bodyp, nodep->directive(), nodep->userType()); } AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message, @@ -398,24 +398,31 @@ class AssertVisitor final : public VNVisitor { iterateChildren(nodep); AstSenTree* const sentreep = nodep->sentreep(); + if (nodep->immediate()) { + UASSERT_OBJ(!sentreep, nodep, "Immediate assertions don't have sensitivity"); + } else { + UASSERT_OBJ(sentreep, nodep, "Concurrent assertions must have sensitivity"); + if (m_procedurep) { + if (!nodep->senFromAlways()) { + // To support this need queue of asserts to activate + nodep->v3warn(E_UNSUPPORTED, + "Unsupported: Procedural concurrent assertion with" + " clocking event inside always (IEEE 1800-2023 16.14.6)"); + } + // Change type to concurrent and relink after process + nodep->immediate(false); + static_cast(m_procedurep)->addNext(nodep->unlinkFrBack()); + return; // Later iterate will pick up + } else { + sentreep->unlinkFrBack(); + } + } + // const string& message = nodep->name(); AstNode* passsp = nodep->passsp(); if (passsp) passsp->unlinkFrBackWithNext(); if (failsp) failsp->unlinkFrBackWithNext(); - if (nodep->immediate()) { - UASSERT_OBJ(!sentreep, nodep, "Immediate assertions don't have sensitivity"); - } else { - UASSERT_OBJ(sentreep, nodep, "Concurrent assertions must have sensitivity"); - sentreep->unlinkFrBack(); - if (m_procedurep) { - // To support this need queue of asserts to activate - nodep->v3warn(E_UNSUPPORTED, - "Unsupported: Procedural concurrent assertion with" - " clocking event inside always (IEEE 1800-2023 16.14.6)"); - } - } - // bool selfDestruct = false; if (const AstCover* const snodep = VN_CAST(nodep, Cover)) { ++m_statCover; diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index f740de1c9..515976c4a 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -66,18 +66,24 @@ private: // METHODS - AstSenTree* newSenTree(AstNode* nodep, AstSenTree* useTreep = nullptr) { + AstSenTree* newSenTree(AstNode* nodep, AstSenTree* useTreep = nullptr, + AstNodeCoverOrAssert* cassertp = nullptr) { // Create sentree based on clocked or default clock // Return nullptr for always if (useTreep) return useTreep; AstSenTree* newp = nullptr; AstSenItem* senip = m_senip; + bool fromAlways = false; if (!senip && m_defaultClockingp) senip = m_defaultClockingp->sensesp(); - if (!senip) senip = m_seniAlwaysp; + if (!senip) { + senip = m_seniAlwaysp; + fromAlways = true; + } if (!senip) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: Unclocked assertion"); newp = new AstSenTree{nodep->fileline(), nullptr}; } else { + if (cassertp && fromAlways) cassertp->senFromAlways(true); newp = new AstSenTree{nodep->fileline(), senip->cloneTree(true)}; } return newp; @@ -494,7 +500,7 @@ private: // Find Clocking's buried under nodep->exprsp iterateChildren(nodep); - if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep)); + if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep, nullptr, nodep)); } void visit(AstFalling* nodep) override { if (nodep->user1SetOnce()) return; @@ -647,7 +653,7 @@ private: // Unlink and just keep a pointer to it, convert to sentree as needed m_senip = nodep->sensesp(); iterateNull(nodep->disablep()); - if (VN_AS(nodep->backp(), NodeCoverOrAssert)->type() == VAssertType::CONCURRENT) { + if (!VN_AS(nodep->backp(), NodeCoverOrAssert)->immediate()) { const AstNodeDType* const propDtp = nodep->propp()->dtypep(); nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack()}); nodep->propp()->dtypeFrom(propDtp); diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 3b9b7da94..2430b1641 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -97,18 +97,25 @@ class AstNodeCoverOrAssert VL_NOT_FINAL : public AstNodeStmt { // op3 used by some sub-types only // @astgen op4 := passsp: List[AstNode] // Statements when propp is passing/truthly string m_name; // Name to report - const VAssertType m_type; // Assertion/cover type + const VAssertType m_userType; // Assertion/cover type for user enable/disable const VAssertDirectiveType m_directive; // Assertion directive type + bool m_senFromAlways = false; // Sensitivity list copied from upper always + bool m_immediate = false; // Immediate assert (may differ from userType being immediate) public: - AstNodeCoverOrAssert(VNType t, FileLine* fl, AstNode* propp, AstNode* passsp, VAssertType type, - VAssertDirectiveType directive, const string& name = "") + AstNodeCoverOrAssert(VNType t, FileLine* fl, AstNode* propp, AstNode* passsp, + VAssertType userType, VAssertDirectiveType directive, + const string& name = "") : AstNodeStmt{t, fl} , m_name{name} - , m_type{type} + , m_userType{userType} , m_directive{directive} { this->propp(propp); addPasssp(passsp); + m_immediate = m_userType.containsAny(VAssertType::SIMPLE_IMMEDIATE + | VAssertType::OBSERVED_DEFERRED_IMMEDIATE + | VAssertType::FINAL_DEFERRED_IMMEDIATE) + || m_userType == VAssertType::INTERNAL; } ASTGEN_MEMBERS_AstNodeCoverOrAssert; string name() const override VL_MT_STABLE { return m_name; } // * = Var name @@ -116,14 +123,13 @@ public: void name(const string& name) override { m_name = name; } void dump(std::ostream& str = std::cout) const override; void dumpJson(std::ostream& str = std::cout) const override; - VAssertType type() const VL_MT_SAFE { return m_type; } + string type() { return ""; } + VAssertType userType() const VL_MT_SAFE { return m_userType; } VAssertDirectiveType directive() const { return m_directive; } - bool immediate() const { - return this->type().containsAny(VAssertType::SIMPLE_IMMEDIATE - | VAssertType::OBSERVED_DEFERRED_IMMEDIATE - | VAssertType::FINAL_DEFERRED_IMMEDIATE) - || this->type() == VAssertType::INTERNAL; - } + bool immediate() const { return m_immediate; } + void immediate(bool flag) { m_immediate = flag; } + bool senFromAlways() const VL_MT_STABLE { return m_senFromAlways; } + void senFromAlways(bool flag) { m_senFromAlways = flag; } }; class AstNodeForeach VL_NOT_FINAL : public AstNodeStmt { // @astgen op1 := headerp : AstForeachHeader diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index de8e06d64..3af4938a3 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -1957,11 +1957,15 @@ string AstClassRefDType::prettyDTypeName(bool) const { return "class{}"s + prett string AstClassRefDType::name() const { return classp() ? classp()->name() : ""; } void AstNodeCoverOrAssert::dump(std::ostream& str) const { this->AstNodeStmt::dump(str); - str << " ["s + this->type().ascii() + "]"; + str << " ["s + this->userType().ascii() + "]"; + if (immediate()) str << " [IMMEDIATE]"; + if (senFromAlways()) str << " [SENALW]"; } void AstNodeCoverOrAssert::dumpJson(std::ostream& str) const { - dumpJsonStr(str, "type", "["s + this->type().ascii() + "]"); + dumpJsonStr(str, "type", "["s + this->userType().ascii() + "]"); dumpJsonGen(str); + dumpJsonBoolFuncIf(str, immediate); + dumpJsonBoolFuncIf(str, senFromAlways); } void AstClocking::dump(std::ostream& str) const { this->AstNode::dump(str); diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index 904da3186..b2d1f3e7a 100644 --- a/src/V3EmitV.cpp +++ b/src/V3EmitV.cpp @@ -804,11 +804,11 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { } void visit(AstNodeCoverOrAssert* nodep) override { putfs(nodep, nodep->verilogKwd() + " "); - if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) { + if (nodep->userType() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) { puts("#0 "); - } else if (nodep->type() == VAssertType::FINAL_DEFERRED_IMMEDIATE) { + } else if (nodep->userType() == VAssertType::FINAL_DEFERRED_IMMEDIATE) { puts("final "); - } else if (nodep->type() == VAssertType::CONCURRENT) { + } else if (nodep->userType() == VAssertType::CONCURRENT) { puts("property "); } iterateConstNull(nodep->sentreep()); diff --git a/src/V3Global.cpp b/src/V3Global.cpp index eb96a3b70..9cd9dc512 100644 --- a/src/V3Global.cpp +++ b/src/V3Global.cpp @@ -174,7 +174,8 @@ string V3Global::digitsFilename(int number) { return ss.str(); } -void V3Global::dumpCheckGlobalTree(const string& stagename, int newNumber, bool doDump) { +void V3Global::dumpCheckGlobalTree(const string& stagename, int newNumber, bool doDump, + bool doCheck) { const string treeFilename = v3Global.debugFilename(stagename + ".tree", newNumber); if (dumpTreeLevel()) v3Global.rootp()->dumpTreeFile(treeFilename, doDump); if (dumpTreeJsonLevel()) { @@ -186,7 +187,7 @@ void V3Global::dumpCheckGlobalTree(const string& stagename, int newNumber, bool if (v3Global.opt.stats()) V3Stats::statsStage(stagename); if (doDump && v3Global.opt.debugEmitV()) V3EmitV::debugEmitV(treeFilename + ".v"); - if (v3Global.opt.debugCheck() || dumpTreeEitherLevel()) { + if (doCheck && (v3Global.opt.debugCheck() || dumpTreeEitherLevel())) { // Error check v3Global.rootp()->checkTree(); // Broken isn't part of check tree because it can munge iterp's diff --git a/src/V3Global.h b/src/V3Global.h index 245cc05db..3f778285a 100644 --- a/src/V3Global.h +++ b/src/V3Global.h @@ -170,8 +170,8 @@ public: void readFiles() VL_MT_DISABLED; void removeStd() VL_MT_DISABLED; void checkTree() const; - static void dumpCheckGlobalTree(const string& stagename, int newNumber = 0, - bool doDump = true); + static void dumpCheckGlobalTree(const string& stagename, int newNumber = 0, bool doDump = true, + bool doCheck = true); void assertDTypesResolved(bool flag) { m_assertDTypesResolved = flag; } void assertScoped(bool flag) { m_assertScoped = flag; } void widthMinUsage(const VWidthMinUsage& flag) { m_widthMinUsage = flag; } diff --git a/test_regress/t/t_assert_procedural.py b/test_regress/t/t_assert_procedural.py new file mode 100755 index 000000000..8a938befd --- /dev/null +++ b/test_regress/t/t_assert_procedural.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() + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_procedural.v b/test_regress/t/t_assert_procedural.v new file mode 100644 index 000000000..f637d29a5 --- /dev/null +++ b/test_regress/t/t_assert_procedural.v @@ -0,0 +1,68 @@ +// 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 + +// verilog_format: off +`define stop $stop +`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + int cyc; + int cntneg; + logic rst_l; + wire [1:0] req = cyc[2:1]; + wire gnt = cyc[0]; + + // verilator lint_off MULTIDRIVEN + logic assert_procedural; + logic assert_immediate; + wire logic assert_exp = (req == 2'b11) && !gnt && rst_l; + // verilator lint_off MULTIDRIVEN + + always @(negedge clk) begin + assert property (disable iff (!rst_l) ((&req) |-> gnt)) + else + assert_procedural <= 1'b1; + cntneg <= cntneg + 1; // To check unlink of above assert + end + + assert property (@(negedge clk) disable iff (!rst_l) ((&req) |-> gnt)) + else + assert_immediate <= 1'b1; + + // Test loop + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d req='b%b gnt=%b exp=%x proc=%x imm=%x\n", $time, cyc, req, gnt, assert_exp, assert_procedural, assert_immediate); +`endif + cyc <= cyc + 1; + assert_procedural <= 0; // Careful, will race unless assert is on negedge + assert_immediate <= 0; // Careful, will race unless assert is on negedge + if (cyc == 0) begin + // Setup + rst_l <= !1'b1; + end + else if (cyc < 10) begin + `checkh(assert_procedural, assert_exp); + `checkh(assert_immediate, assert_exp); + end + else if (cyc == 19) begin + rst_l <= !1'b0; + end + else if (cyc < 30) begin + `checkh(assert_procedural, assert_exp); + `checkh(assert_immediate, assert_exp); + end + else if (cyc == 99) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule diff --git a/test_regress/t/t_cover_assert.out b/test_regress/t/t_cover_assert.out deleted file mode 100644 index f376db8e7..000000000 --- a/test_regress/t/t_cover_assert.out +++ /dev/null @@ -1,6 +0,0 @@ -%Error-UNSUPPORTED: t/t_cover_assert.v:38:5: Unsupported: Procedural concurrent assertion with clocking event inside always (IEEE 1800-2023 16.14.6) - : ... note: In instance 't' - 38 | cover property (a) begin - | ^~~~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error: Exiting due to diff --git a/test_regress/t/t_cover_assert.py b/test_regress/t/t_cover_assert.py index 5a06bae30..167d3f0b5 100755 --- a/test_regress/t/t_cover_assert.py +++ b/test_regress/t/t_cover_assert.py @@ -11,8 +11,8 @@ import vltest_bootstrap test.scenarios('vlt') -test.lint(verilator_flags2=["-Wall -Wno-DECLFILENAME --coverage"], - fails=True, - expect_filename=test.golden_filename) +test.compile(verilator_flags2=["-Wall -Wno-DECLFILENAME --coverage"]) + +test.execute() test.passes() diff --git a/test_regress/t/t_dump_json.out b/test_regress/t/t_dump_json.out index 7d4153c63..faaed000c 100644 --- a/test_regress/t/t_dump_json.out +++ b/test_regress/t/t_dump_json.out @@ -514,7 +514,7 @@ "directiveTypesp": [ {"type":"CONST","name":"32'h7","addr":"(HI)","loc":"e,87:7,87:18","dtypep":"(QC)"} ]}, - {"type":"ASSERT","name":"","addr":"(II)","loc":"e,88:7,88:13","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(II)","loc":"e,88:7,88:13","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(JI)","loc":"e,88:14,88:15","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []}, @@ -551,7 +551,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_simple_immediate_else","addr":"(WI)","loc":"e,96:7,96:35","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(XI)","loc":"e,96:37,96:43","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(XI)","loc":"e,96:37,96:43","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(YI)","loc":"e,96:44,96:45","dtypep":"(N)"} ],"sentreep": [], @@ -567,7 +567,7 @@ ]}, {"type":"BEGIN","name":"assert_simple_immediate_stmt","addr":"(CJ)","loc":"e,97:7,97:35","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(DJ)","loc":"e,97:37,97:43","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(DJ)","loc":"e,97:37,97:43","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(EJ)","loc":"e,97:44,97:45","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -583,7 +583,7 @@ ]}, {"type":"BEGIN","name":"assert_simple_immediate_stmt_else","addr":"(IJ)","loc":"e,98:7,98:40","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(JJ)","loc":"e,98:42,98:48","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(JJ)","loc":"e,98:42,98:48","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(KJ)","loc":"e,98:49,98:50","dtypep":"(N)"} ],"sentreep": [], @@ -608,14 +608,14 @@ ]}, {"type":"BEGIN","name":"assume_simple_immediate","addr":"(RJ)","loc":"e,100:7,100:30","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(SJ)","loc":"e,100:32,100:38","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(SJ)","loc":"e,100:32,100:38","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(TJ)","loc":"e,100:39,100:40","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []} ]}, {"type":"BEGIN","name":"assume_simple_immediate_else","addr":"(UJ)","loc":"e,101:7,101:35","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(VJ)","loc":"e,101:37,101:43","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(VJ)","loc":"e,101:37,101:43","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(WJ)","loc":"e,101:44,101:45","dtypep":"(N)"} ],"sentreep": [], @@ -631,7 +631,7 @@ ]}, {"type":"BEGIN","name":"assume_simple_immediate_stmt","addr":"(AK)","loc":"e,102:7,102:35","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(BK)","loc":"e,102:37,102:43","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(BK)","loc":"e,102:37,102:43","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(CK)","loc":"e,102:44,102:45","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -647,7 +647,7 @@ ]}, {"type":"BEGIN","name":"assume_simple_immediate_stmt_else","addr":"(GK)","loc":"e,103:7,103:40","declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(HK)","loc":"e,103:42,103:48","type":"[SIMPLE_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(HK)","loc":"e,103:42,103:48","type":"[SIMPLE_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(IK)","loc":"e,103:49,103:50","dtypep":"(N)"} ],"sentreep": [], @@ -676,7 +676,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_observed_deferred_immediate","addr":"(QK)","loc":"e,106:4,106:38","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(RK)","loc":"e,106:40,106:46","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(RK)","loc":"e,106:40,106:46","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(SK)","loc":"e,106:51,106:52","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []} @@ -686,7 +686,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_observed_deferred_immediate_else","addr":"(UK)","loc":"e,107:4,107:43","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(VK)","loc":"e,107:45,107:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(VK)","loc":"e,107:45,107:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(WK)","loc":"e,107:56,107:57","dtypep":"(N)"} ],"sentreep": [], @@ -705,7 +705,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_observed_deferred_immediate_stmt","addr":"(BL)","loc":"e,108:4,108:43","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(CL)","loc":"e,108:45,108:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(CL)","loc":"e,108:45,108:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(DL)","loc":"e,108:56,108:57","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -724,7 +724,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_observed_deferred_immediate_stmt_else","addr":"(IL)","loc":"e,109:4,109:48","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(JL)","loc":"e,109:50,109:56","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(JL)","loc":"e,109:50,109:56","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(KL)","loc":"e,109:61,109:62","dtypep":"(N)"} ],"sentreep": [], @@ -752,7 +752,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_observed_deferred_immediate","addr":"(SL)","loc":"e,111:4,111:38","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(TL)","loc":"e,111:40,111:46","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(TL)","loc":"e,111:40,111:46","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(UL)","loc":"e,111:51,111:52","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []} @@ -762,7 +762,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_observed_deferred_immediate_else","addr":"(WL)","loc":"e,112:4,112:43","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(XL)","loc":"e,112:45,112:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(XL)","loc":"e,112:45,112:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(YL)","loc":"e,112:56,112:57","dtypep":"(N)"} ],"sentreep": [], @@ -781,7 +781,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_observed_deferred_immediate_stmt","addr":"(DM)","loc":"e,113:4,113:43","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(EM)","loc":"e,113:45,113:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(EM)","loc":"e,113:45,113:51","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(FM)","loc":"e,113:56,113:57","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -800,7 +800,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_observed_deferred_immediate_stmt_else","addr":"(KM)","loc":"e,114:4,114:48","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(LM)","loc":"e,114:50,114:56","type":"[OBSERVED_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(LM)","loc":"e,114:50,114:56","type":"[OBSERVED_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(MM)","loc":"e,114:61,114:62","dtypep":"(N)"} ],"sentreep": [], @@ -828,7 +828,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_final_deferred_immediate","addr":"(UM)","loc":"e,116:4,116:35","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(VM)","loc":"e,116:37,116:43","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(VM)","loc":"e,116:37,116:43","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(WM)","loc":"e,116:51,116:52","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []} @@ -838,7 +838,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_final_deferred_immediate_else","addr":"(YM)","loc":"e,117:4,117:40","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(ZM)","loc":"e,117:42,117:48","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(ZM)","loc":"e,117:42,117:48","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(AN)","loc":"e,117:56,117:57","dtypep":"(N)"} ],"sentreep": [], @@ -857,7 +857,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_final_deferred_immediate_stmt","addr":"(FN)","loc":"e,118:4,118:40","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(GN)","loc":"e,118:42,118:48","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(GN)","loc":"e,118:42,118:48","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(HN)","loc":"e,118:56,118:57","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -876,7 +876,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assert_final_deferred_immediate_stmt_else","addr":"(MN)","loc":"e,119:4,119:45","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(NN)","loc":"e,119:47,119:53","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(NN)","loc":"e,119:47,119:53","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(ON)","loc":"e,119:61,119:62","dtypep":"(N)"} ],"sentreep": [], @@ -904,7 +904,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_final_deferred_immediate","addr":"(WN)","loc":"e,121:4,121:35","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(XN)","loc":"e,121:37,121:43","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(XN)","loc":"e,121:37,121:43","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(YN)","loc":"e,121:51,121:52","dtypep":"(N)"} ],"sentreep": [],"failsp": [],"passsp": []} @@ -914,7 +914,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_final_deferred_immediate_else","addr":"(AO)","loc":"e,122:4,122:40","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(BO)","loc":"e,122:42,122:48","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(BO)","loc":"e,122:42,122:48","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(CO)","loc":"e,122:56,122:57","dtypep":"(N)"} ],"sentreep": [], @@ -933,7 +933,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_final_deferred_immediate_stmt","addr":"(HO)","loc":"e,123:4,123:40","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(IO)","loc":"e,123:42,123:48","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(IO)","loc":"e,123:42,123:48","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(JO)","loc":"e,123:56,123:57","dtypep":"(N)"} ],"sentreep": [],"failsp": [], @@ -952,7 +952,7 @@ "stmtsp": [ {"type":"BEGIN","name":"assume_final_deferred_immediate_stmt_else","addr":"(OO)","loc":"e,124:4,124:45","implied":true,"declsp": [], "stmtsp": [ - {"type":"ASSERT","name":"","addr":"(PO)","loc":"e,124:47,124:53","type":"[FINAL_DEFERRED_IMMEDIATE]", + {"type":"ASSERT","name":"","addr":"(PO)","loc":"e,124:47,124:53","type":"[FINAL_DEFERRED_IMMEDIATE]","immediate":true, "propp": [ {"type":"CONST","name":"?32?sh0","addr":"(QO)","loc":"e,124:61,124:62","dtypep":"(N)"} ],"sentreep": [], @@ -1170,7 +1170,7 @@ ],"filep": []} ]} ]}, - {"type":"RESTRICT","name":"","addr":"(RR)","loc":"e,143:4,143:12","type":"[INTERNAL]", + {"type":"RESTRICT","name":"","addr":"(RR)","loc":"e,143:4,143:12","type":"[INTERNAL]","immediate":true, "propp": [ {"type":"PROPSPEC","name":"","addr":"(SR)","loc":"e,143:23,143:27","dtypep":"UNLINKED","sensesp": [],"disablep": [], "propp": [