Fix unique0 case side effects
Signed-off-by: Pawel Klopotek <pklopotek@internships.antmicro.com>
This commit is contained in:
parent
0e371d6e5c
commit
9ca9f07904
|
|
@ -20,6 +20,7 @@
|
||||||
|
|
||||||
#include "V3AstUserAllocator.h"
|
#include "V3AstUserAllocator.h"
|
||||||
#include "V3Stats.h"
|
#include "V3Stats.h"
|
||||||
|
#include "V3UniqueNames.h"
|
||||||
|
|
||||||
VL_DEFINE_DEBUG_FUNCTIONS;
|
VL_DEFINE_DEBUG_FUNCTIONS;
|
||||||
|
|
||||||
|
|
@ -228,6 +229,9 @@ class AssertVisitor final : public VNVisitor {
|
||||||
AstNode* m_failsp = nullptr; // Current fail statement
|
AstNode* m_failsp = nullptr; // Current fail statement
|
||||||
AstNodeCoverOrAssert* m_assertp = nullptr; // Current assertion
|
AstNodeCoverOrAssert* m_assertp = nullptr; // Current assertion
|
||||||
AstFinal* m_finalp = nullptr; // Current final block
|
AstFinal* m_finalp = nullptr; // Current final block
|
||||||
|
VDouble0 m_statLiftedCaseExprs; // Count of purified case expressions
|
||||||
|
AstNodeFTask* m_ftaskp = nullptr; // Current function/task
|
||||||
|
V3UniqueNames m_caseTempNames{"__VCase"};
|
||||||
// Map from (expression, senTree) to AstAlways that computes delayed values of the expression
|
// Map from (expression, senTree) to AstAlways that computes delayed values of the expression
|
||||||
std::unordered_map<VNRef<AstNodeExpr>, std::unordered_map<VNRef<AstSenTree>, AstAlways*>>
|
std::unordered_map<VNRef<AstNodeExpr>, std::unordered_map<VNRef<AstSenTree>, AstAlways*>>
|
||||||
m_modExpr2Sen2DelayedAlwaysp;
|
m_modExpr2Sen2DelayedAlwaysp;
|
||||||
|
|
@ -755,6 +759,28 @@ class AssertVisitor final : public VNVisitor {
|
||||||
|
|
||||||
//========== Case assertions
|
//========== Case assertions
|
||||||
void visit(AstCase* nodep) override {
|
void visit(AstCase* nodep) override {
|
||||||
|
// Introduce temporary variable for AstCase if needed - it is done here and not in V3Case
|
||||||
|
// because this phase is before V3Scope and V3Case is not. Doing it before V3Scope ensures
|
||||||
|
// that V3Scope will take care of a scope creation
|
||||||
|
// We also need to do it before V3Begin, co that pragmas like `unique0` also work correctly
|
||||||
|
if (!nodep->exprp()->isPure()) {
|
||||||
|
++m_statLiftedCaseExprs;
|
||||||
|
FileLine* const fl = nodep->exprp()->fileline();
|
||||||
|
AstVar* const varp = new AstVar{fl, VVarType::BLOCKTEMP, m_caseTempNames.get(nodep),
|
||||||
|
nodep->exprp()->dtypep()};
|
||||||
|
AstNodeExpr* const origp = nodep->exprp()->unlinkFrBack();
|
||||||
|
nodep->addHereThisAsNext(
|
||||||
|
new AstAssign{fl, new AstVarRef{fl, varp, VAccess::WRITE}, origp});
|
||||||
|
nodep->exprp(new AstVarRef{fl, varp, VAccess::READ});
|
||||||
|
if (m_ftaskp) {
|
||||||
|
varp->funcLocal(true);
|
||||||
|
varp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
|
||||||
|
m_ftaskp->stmtsp()->addHereThisAsNext(varp);
|
||||||
|
} else {
|
||||||
|
m_modp->stmtsp()->addHereThisAsNext(varp);
|
||||||
|
}
|
||||||
|
VIsCached::clearCacheTree();
|
||||||
|
}
|
||||||
iterateChildren(nodep);
|
iterateChildren(nodep);
|
||||||
if (!nodep->user1SetOnce()) {
|
if (!nodep->user1SetOnce()) {
|
||||||
bool has_default = false;
|
bool has_default = false;
|
||||||
|
|
@ -1180,6 +1206,7 @@ public:
|
||||||
V3Stats::addStat("Assertions, $past variables", m_statPastVars);
|
V3Stats::addStat("Assertions, $past variables", m_statPastVars);
|
||||||
V3Stats::addStat("Assertions, assertOn checks combined", m_statAssertOnCombined);
|
V3Stats::addStat("Assertions, assertOn checks combined", m_statAssertOnCombined);
|
||||||
V3Stats::addStat("Assertions, assertOn checks hoisted", m_statAssertOnHoisted);
|
V3Stats::addStat("Assertions, assertOn checks hoisted", m_statAssertOnHoisted);
|
||||||
|
V3Stats::addStat("Assertions, lifted impure case expressions", m_statLiftedCaseExprs);
|
||||||
// Rewrites can change purity, e.g. by compiling out assertion statements with --no-assert
|
// Rewrites can change purity, e.g. by compiling out assertion statements with --no-assert
|
||||||
VIsCached::clearCacheTree();
|
VIsCached::clearCacheTree();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -15,6 +15,7 @@ test.compile(verilator_flags2=['--stats'])
|
||||||
|
|
||||||
test.execute()
|
test.execute()
|
||||||
|
|
||||||
test.file_grep(test.stats, r'LiftExpr, lifted calls\s+(\d+)', 3)
|
test.file_grep(test.stats, r'LiftExpr, lifted calls\s+(\d+)', 2)
|
||||||
|
test.file_grep(test.stats, r'Assertions, lifted impure case expressions\s+(\d+)', 2)
|
||||||
|
|
||||||
test.passes()
|
test.passes()
|
||||||
|
|
|
||||||
|
|
@ -15,6 +15,7 @@ test.compile(verilator_flags2=['--stats'])
|
||||||
|
|
||||||
test.execute()
|
test.execute()
|
||||||
|
|
||||||
test.file_grep(test.stats, r'LiftExpr, lifted calls\s+(\d+)', 3)
|
test.file_grep(test.stats, r'LiftExpr, lifted calls\s+(\d+)', 2)
|
||||||
|
test.file_grep(test.stats, r'Assertions, lifted impure case expressions\s+(\d+)', 2)
|
||||||
|
|
||||||
test.passes()
|
test.passes()
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,20 @@
|
||||||
|
#!/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(verilator_flags2=["--stats"])
|
||||||
|
|
||||||
|
test.execute()
|
||||||
|
|
||||||
|
test.file_grep(test.stats, r"Assertions, lifted impure case expressions\s+(\d+)", 1)
|
||||||
|
|
||||||
|
test.passes()
|
||||||
|
|
@ -0,0 +1,39 @@
|
||||||
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
|
//
|
||||||
|
// This file ONLY is placed under the Creative Commons Public Domain.
|
||||||
|
// SPDX-FileCopyrightText: 2026 Antmicro
|
||||||
|
// 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='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
|
||||||
|
`define checkp(gotv,expv_s) do begin string gotv_s; gotv_s = $sformatf("%p", gotv); if ((gotv_s) != (expv_s)) begin $write("%%Error: %s:%0d: got='%s' exp='%s'\n", `__FILE__,`__LINE__, (gotv_s), (expv_s)); `stop; end end while(0);
|
||||||
|
// verilog_format: on
|
||||||
|
|
||||||
|
module t;
|
||||||
|
int x;
|
||||||
|
int y;
|
||||||
|
int z;
|
||||||
|
initial begin
|
||||||
|
y = 0;
|
||||||
|
x = 0;
|
||||||
|
z = 0;
|
||||||
|
unique0 case(increment_x())
|
||||||
|
1: begin
|
||||||
|
y = 1;
|
||||||
|
end
|
||||||
|
default: begin
|
||||||
|
z = 1;
|
||||||
|
end
|
||||||
|
endcase
|
||||||
|
`checkh(x, 32'h1);
|
||||||
|
`checkh(y, 32'h1);
|
||||||
|
`checkh(z, 32'h0);
|
||||||
|
$finish;
|
||||||
|
end
|
||||||
|
|
||||||
|
function automatic integer increment_x();
|
||||||
|
x = x + 1;
|
||||||
|
return x;
|
||||||
|
endfunction
|
||||||
|
endmodule
|
||||||
Loading…
Reference in New Issue