luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

* Support procedural concurrent assertion simple cases (#6944). 

Fixes #6944.
This commit is contained in:
Wilson Snyder 2026-03-05 20:03:48 -05:00
parent c2d65c2e13
commit b89d29cab9
13 changed files with 178 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changes
View File

@ -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]

37
src/V3Assert.cpp
View File

@ -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<AstNode*>(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;

14
src/V3AssertPre.cpp
View File

@ -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);

28
src/V3AstNodeStmt.h
View File

@ -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

8
src/V3AstNodes.cpp
View File

@ -1957,11 +1957,15 @@ string AstClassRefDType::prettyDTypeName(bool) const { return "class{}"s + prett
string AstClassRefDType::name() const { return classp() ? classp()->name() : "<unlinked>"; }
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);

6
src/V3EmitV.cpp
View File

@ -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());

5
src/V3Global.cpp
View File

@ -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

4
src/V3Global.h
View File

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

18
test_regress/t/t_assert_procedural.py Executable file
View File

@ -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()

68
test_regress/t/t_assert_procedural.v Normal file
View File

@ -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

6
test_regress/t/t_cover_assert.out
View File

@ -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

6
test_regress/t/t_cover_assert.py
View File

@ -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()

50
test_regress/t/t_dump_json.out
View File

@ -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": [