Skip to content

Commit ceea5d2

Browse files
mikhailmoiseevmikhailmoiseev
committed
Version 1.4.38. Assertions updated, #27, #28 fixed
1 parent bf57c72 commit ceea5d2

25 files changed

+457
-213
lines changed

‎examples/dvcon20/dvcon_simple.sv

+21-10
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
//==============================================================================
22
//
3-
// The code is generated by Intel Compiler for SystemC, version 1.4.15
3+
// The code is generated by Intel Compiler for SystemC, version 1.4.38
44
// see more information at https://github.com/intel/systemc-compiler
55
//
66
//==============================================================================
@@ -90,20 +90,31 @@ endfunction
9090
always_ff @(posedge clk or negedge nrst)
9191
begin : thread_proc_ff
9292
if ( ~nrst ) begin
93+
94+
`ifndef INTEL_SVA_OFF
95+
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
96+
sctAssertLine70 : assert property ( enbl[i] |=> !enbl[i] );
97+
end
98+
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
99+
for (integer j = 0; j < 32; ++j) begin
100+
sctAssertLine72 : assert property ( actv[i][j] |-> ##2 actv[i][32 - j - 1] );
101+
end
102+
end
103+
`endif // INTEL_SVA_OFF
93104
end
94105
else begin
95-
end
96106

97-
`ifndef INTEL_SVA_OFF
98-
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
99-
sctAssertLine70 : assert property ( enbl[i] |=> !enbl[i] );
100-
end
101-
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
102-
for (integer j = 0; j < 32; ++j) begin
103-
sctAssertLine72 : assert property ( actv[i][j] |-> ##2 actv[i][32 - j - 1] );
107+
`ifndef INTEL_SVA_OFF
108+
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
109+
sctAssertLine70 : assert property ( enbl[i] |=> !enbl[i] );
104110
end
111+
for (integer i = 0; i < signed'({1'b0, N}); ++i) begin
112+
for (integer j = 0; j < 32; ++j) begin
113+
sctAssertLine72 : assert property ( actv[i][j] |-> ##2 actv[i][32 - j - 1] );
114+
end
115+
end
116+
`endif // INTEL_SVA_OFF
105117
end
106-
`endif // INTEL_SVA_OFF
107118
end
108119

109120
`ifndef INTEL_SVA_OFF

‎sc_tool/lib/sc_tool/SCToolFrontendAction.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -123,8 +123,8 @@ Object* getOuterArray(SCDesign& designDB, Object* memberObj)
123123
return arrayObj;
124124
}
125125

126-
const std::string SCElabASTConsumer::TOOL_VERSION = "1.4.37";
127-
const std::string SCElabASTConsumer::TOOL_DATE = "Aug 03,2022";
126+
const std::string SCElabASTConsumer::TOOL_VERSION = "1.4.38";
127+
const std::string SCElabASTConsumer::TOOL_DATE = "Aug 20,2022";
128128

129129
void SCElabASTConsumer::HandleTranslationUnit(clang::ASTContext &astCtx)
130130
{
@@ -149,7 +149,7 @@ void SCElabASTConsumer::HandleTranslationUnit(clang::ASTContext &astCtx)
149149
//const char* optNames[] = {doConstCfg, doConstLoop, doConstStmt, doConstBlock, doModuleBuilder};
150150
//const char* optNames[] = {doConstStmt, doGenStmt, doModuleBuilder};
151151
//const char* optNames[] = {doPortBind, doModuleBuilder};
152-
const char* optNames[] = {doModuleBuilder};
152+
const char* optNames[] = {doGenRTL, doGenStmt, doModuleBuilder};
153153
size_t optSize = sizeof(optNames)/sizeof(const char*);
154154
//DebugOptions::enable(optNames, optSize);
155155

‎sc_tool/lib/sc_tool/ScProcAnalyzer.cpp

+8-1
Original file line numberDiff line numberDiff line change
@@ -591,6 +591,7 @@ std::string ScProcAnalyzer::analyzeSvaProperties(
591591
auto constState = shared_ptr<ScState>(globalState->clone());
592592
ScTraverseConst travConst(astCtx, constState, modval,
593593
globalState, &elabDB, nullptr, nullptr, true);
594+
travConst.setModuleSctAssert();
594595

595596
// Add all used variable to state
596597
for (const FieldDecl* propDecl : properties) {
@@ -673,14 +674,20 @@ std::string ScProcAnalyzer::analyzeSvaProperties(
673674
auto procState = shared_ptr<ScState>(globalState->clone());
674675
ScTraverseProc travProc(astCtx, procState, modval, procWriter.get(),
675676
nullptr, nullptr, true);
677+
travProc.setTermConds(travConst.getTermConds());
676678

677679
// Generate all properties
678680
std::string propStr;
679681
for (const FieldDecl* propDecl : properties) {
680682
// Get actual parent class, required for assertion in base classes
681683
QualType partype(propDecl->getParent()->getTypeForDecl(), 0);
682684
SValue propmodval = getBaseClass(modval, partype);
683-
travProc.setModval(propmodval ? propmodval : modval);
685+
propmodval = propmodval ? propmodval : modval;
686+
travProc.setModval(propmodval);
687+
// Setup first non-MIF module value
688+
SValue synmodval = globalState->getSynthModuleValue(
689+
propmodval, ScState::MIF_CROSS_NUM);
690+
travProc.setSynModval(synmodval);
684691

685692
if (auto code = travProc.runSvaDecl(propDecl)) {
686693
propStr += *code;

‎sc_tool/lib/sc_tool/cfg/ScTraverseConst.cpp

+28-1
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ void ScTraverseConst::evaluateTermCond(Stmt* stmt, SValue& val)
178178

179179
// Use @checkRecOnly to have pointer null/not null value for record/MIF
180180
// array element accessed at unknown index, required for condition of
181-
// pointer initialized: if (p) p->f();
181+
// pointer initialized: if (p) p->f(); p ? p->f() : a;
182182
auto condvals = evaluateConstInt(const_cast<Expr*>(cond), false, true);
183183
//cout << "evaluateConstInt " << condvals.first << " " << condvals.second << endl;
184184
readFromValue(condvals.first);
@@ -190,6 +190,7 @@ void ScTraverseConst::evaluateTermCond(Stmt* stmt, SValue& val)
190190
if (!i.second) {
191191
i.first->second = condvals.first;
192192
}
193+
//cout << "condStoredValue " << hex << stmt << " " << condvals.first << dec << endl;
193194
}
194195
}
195196
}
@@ -234,6 +235,26 @@ llvm::Optional<unsigned> ScTraverseConst::evaluateIterNumber(const Stmt* stmt)
234235
return llvm::None;
235236
}
236237

238+
// Store ternary statement condition for SVA property
239+
void ScTraverseConst::putSvaCondTerm(const Stmt* stmt, SValue val)
240+
{
241+
auto callStack = contextStack.getStmtStack();
242+
callStack.push_back(stmt);
243+
// Add the same value for first iteration
244+
callStack.push_back(stmt);
245+
246+
auto i = termConds.emplace(callStack, val);
247+
if (!i.second) {
248+
if (i.first->second != val) {
249+
i.first->second = NO_VALUE;
250+
val = NO_VALUE;
251+
}
252+
}
253+
254+
//cout << "putSvaCondTerm " << hex << stmt << " stackSize " << callStack.size()
255+
// << " val " << val << dec << endl;
256+
}
257+
237258
// Prepare next block analysis
238259
void ScTraverseConst::prepareNextBlock(AdjBlock& nextBlock,
239260
vector<ConstScopeInfo>& scopeInfos)
@@ -518,6 +539,10 @@ void ScTraverseConst::parseMemberCall(CXXMemberCallExpr* expr, SValue& tval,
518539
if (isConstCharPtr(expr->getType())) {
519540
// Do nothing, all logic implemented in ScParseExprValue
520541

542+
} else
543+
if (state->getParseSvaArg()) {
544+
// Do nothing for function call in SVA, all done in ScParseExprValue
545+
521546
} else {
522547
// General method call
523548
// No user-define method call in constant evaluation mode
@@ -1175,6 +1200,8 @@ void ScTraverseConst::run()
11751200
i.first->second = NO_VALUE;
11761201
}
11771202
}
1203+
//cout << "putTermConds " << hex << term << " stackSize " << callStack.size()
1204+
// << " val " << termCondValue << dec << endl;
11781205

11791206
// Register terminator as live
11801207
liveTerms.insert(term);

‎sc_tool/lib/sc_tool/cfg/ScTraverseConst.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -264,7 +264,6 @@ class ScTraverseConst : public ScParseExprValue {
264264
dynmodval(modval_)
265265
{
266266
state->getMostDerivedClass(dynmodval, dynmodval);
267-
enableCheckAssert();
268267
}
269268

270269
/// @state deleted in @ScTraverse destructor
@@ -289,6 +288,9 @@ class ScTraverseConst : public ScParseExprValue {
289288
/// Evaluate loop iteration number from conditional expression
290289
llvm::Optional<unsigned> evaluateIterNumber(const clang::Stmt* stmt);
291290

291+
/// Store ternary statement condition for SVA property
292+
void putSvaCondTerm(const clang::Stmt* stmt, SValue val) override;
293+
292294
/// Prepare next block analysis
293295
void prepareNextBlock(AdjBlock& nextBlock, std::vector<ConstScopeInfo>& scopeInfos);
294296

‎sc_tool/lib/sc_tool/cfg/ScTraverseProc.cpp

+15-10
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ shared_ptr<CodeScope> ScTraverseProc::getScopeForBlock(AdjBlock block, unsigned
6868
llvm::Optional<std::string>
6969
ScTraverseProc::getSvaInLoopStr(const std::string& svaStr, bool isResetSection)
7070
{
71-
std::string tabStr = (isResetSection ? " " : " ");
71+
std::string tabStr = " ";
7272
std::string loopStr;
7373

7474
for (auto i = loopStack.begin(); i != loopStack.end(); ++i) {
@@ -126,15 +126,22 @@ void ScTraverseProc::getTermCondValue(const Stmt* stmt, SValue& val, SValue& fva
126126
i = termConds.find(callStack);
127127
bool firstIter = (i != termConds.end());
128128
fval = firstIter ? i->second : NO_VALUE;
129+
130+
// cout << "Call stack first iter " << hex;
131+
// for (auto i : callStack) cout << " " << i;
132+
// cout << " fval " << fval << endl;
129133

130-
if (firstIter && otherIters) {
134+
if (firstIter && otherIters) {
131135
// Join first iteration value to all other iterations value
132136
if (val != fval) val = NO_VALUE;
133137
} else
134138
if (firstIter && !otherIters) {
135139
// If there is only one loop iteration
136140
val = fval;
137141
}
142+
143+
//cout << "getTermConds " << hex << stmt << " stackSize " << callStack.size()
144+
// << " val " << val << dec << endl;
138145
//cout << "First iter " << fval.asString() << " " << firstIter
139146
// << ", other iters " << val.asString() << " " << otherIters << endl;
140147
}
@@ -386,7 +393,7 @@ void ScTraverseProc::parseMemberCall(CXXMemberCallExpr* expr, SValue& tval,
386393

387394
} else
388395
if (isConstCharPtr(expr->getType())) {
389-
// Do nothing, all logic implemented in ScParseExprValue
396+
// Do nothing, all logic implemented in ScGenerateExpr
390397

391398
} else
392399
if ( isAnyScCoreObject(thisType) ) {
@@ -400,6 +407,9 @@ void ScTraverseProc::parseMemberCall(CXXMemberCallExpr* expr, SValue& tval,
400407
} else {
401408
// Do nothing for other @sc_core methods
402409
}
410+
} else
411+
if (codeWriter->isParseSvaArg()) {
412+
// Do nothing for function call in SVA, all done in ScGenerateExpr
403413

404414
} else {
405415
// General method call
@@ -425,12 +435,6 @@ void ScTraverseProc::parseMemberCall(CXXMemberCallExpr* expr, SValue& tval,
425435
}
426436

427437
} else {
428-
// Normal processing of function call
429-
if (codeWriter->isParseSvaArg()) {
430-
ScDiag::reportScDiag(expr->getBeginLoc(),
431-
ScDiag::SYNTH_FUNC_IN_ASSERT);
432-
}
433-
434438
// Declare temporal variable if it is not a pointer
435439
if (!isVoidType(retType) && !isPointer(retType)) {
436440
codeWriter->putVarDecl(nullptr, retVal, retType, nullptr, false,
@@ -857,7 +861,8 @@ void ScTraverseProc::run()
857861
if (auto superStmtLevel = stmtInfo.getLevel(superStmt)) {
858862
level = *superStmtLevel;
859863
isCallSubStmt = isUserCallExpr(currStmt);
860-
isStmt = isCallSubStmt && !isIoStreamStmt(superStmt);
864+
isStmt = isCallSubStmt && !isIoStreamStmt(superStmt) &&
865+
!codeWriter->isParseSvaArg();
861866
}
862867
//cout << hex << "getSubStmtLevel " << currStmt << endl;
863868

‎sc_tool/lib/sc_tool/cthread/ScThreadBuilder.cpp

+3-5
Original file line numberDiff line numberDiff line change
@@ -476,8 +476,6 @@ sc_elab::VerilogProcCode ThreadBuilder::getVerilogCode(bool isSingleState)
476476
if (threadStates.hasWaitNState() && !threadStates.isFirstWaitN()) {
477477
vout << " " << waitNRegNames.first << " <= 0;\n";
478478
}
479-
480-
vout << "end\n";
481479
}
482480

483481
resetSection = verRawOS.str();
@@ -522,12 +520,12 @@ sc_elab::VerilogProcCode ThreadBuilder::getVerilogCode(bool isSingleState)
522520
}
523521

524522
// Get temporal assertions
525-
std::stringstream ss;
526-
travProc->printTemporalAsserts(ss, false);
527-
std::string tempAsserts = ss.str();
528523
std::stringstream ssr;
529524
travProc->printTemporalAsserts(ssr, true);
530525
std::string tempRstAsserts = ssr.str();
526+
std::stringstream ss;
527+
travProc->printTemporalAsserts(ss, false);
528+
std::string tempAsserts = tempRstAsserts + ss.str();
531529

532530
//std::cout << "Temporal asserts in proc:\n" << tempAsserts << std::endl;
533531

‎sc_tool/lib/sc_tool/diag/ScToolDiagnostic.h

+6-2
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,8 @@ class ScDiag {
208208
SYNTH_INCORRECT_FUNC_CALL = 236,
209209
SYNTH_PARENT_SAME_OBJECT = 237,
210210
SYNTH_NO_RESET_PROCESS = 238,
211-
211+
SYNTH_FUNC_TYPE_IN_ASSERT = 239,
212+
212213
SC_FATAL_ELAB_TYPES_NS = 300,
213214
SC_WARN_ELAB_UNSUPPORTED_TYPE,
214215
SC_WARN_ELAB_DANGLING_PTR,
@@ -410,7 +411,10 @@ class ScDiag {
410411
"Incorrect assert expression for : %0"};
411412
idFormatMap[SYNTH_FUNC_IN_ASSERT] =
412413
{clang::DiagnosticIDs::Error,
413-
"Function call in temporal assert not allowed"};
414+
"Non-trivial function call in temporal assert not allowed"};
415+
idFormatMap[SYNTH_FUNC_TYPE_IN_ASSERT] =
416+
{clang::DiagnosticIDs::Error,
417+
"Function called in temporal assert should return integral type"};
414418

415419

416420
idFormatMap[SC_FATAL_THREAD_NO_STATE] =

‎sc_tool/lib/sc_tool/elab/ScVerilogModule.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -1731,6 +1731,14 @@ void VerilogModule::serializeProcSplit(llvm::raw_ostream &os,
17311731
if (!procObj.resets().empty()) {
17321732
serializeResetCondition(os, procObj);
17331733
os << procCode.resetSection;
1734+
1735+
if (!procCode.tempRstAsserts.empty()) {
1736+
os << "\n `ifndef INTEL_SVA_OFF\n";
1737+
os << procCode.tempRstAsserts;
1738+
os << " `endif // INTEL_SVA_OFF\n";
1739+
}
1740+
1741+
os << " end\n";
17341742
os << " else ";
17351743
}
17361744
os << "begin\n";
@@ -1752,15 +1760,7 @@ void VerilogModule::serializeProcSplit(llvm::raw_ostream &os,
17521760
}
17531761

17541762
os << " end\n";
1755-
1756-
if (!procCode.tempRstAsserts.empty()) {
1757-
os << "\n`ifndef INTEL_SVA_OFF\n";
1758-
os << procCode.tempRstAsserts;
1759-
os << "`endif // INTEL_SVA_OFF\n";
1760-
}
1761-
17621763
os << "end\n\n";
1763-
17641764
}
17651765

17661766
void VerilogModule::serializeSensList(llvm::raw_ostream &os,

0 commit comments

Comments
 (0)