terapines
/
circt
mirror of https://github.com/llvm/circt.git
2
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[ImportVerilog] Add support for SVA declarations (#8656) 

Support `sequence` and `property` declarations. Slang already handles 
the references and variable ports. Make visiting of `AssertionInstance` 
legal. Those are part of `Expressions` of the `Simple` case. Adapt this 
visitor to handle the varied return types.
This commit is contained in:
Tobias Wölfel 2025-07-09 17:40:25 +02:00 committed by GitHub
parent 3df813fd7e
commit f91e77c509
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 122 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
lib/Conversion/ImportVerilog/AssertionExpr.cpp
View File

@ -78,18 +78,21 @@ struct AssertionExprVisitor {
}
Value visit(const slang::ast::SimpleAssertionExpr &expr) {
// A Simple Assertion expression has the following members:
// - Expression
// - Optional repetition
// The expression needs to have the type `i1` for the LTL operations.
// Convert first to a moore type and then add a conversion to `i1`.
// Handle expression
auto value = context.convertRvalueExpression(expr.expr);
if (!value)
return {};
auto loc = context.convertLocation(expr.expr.sourceRange);
value = context.convertToI1(value);
auto valueType = value.getType();
// For assertion instances the value is already the expected type, convert
// boolean value
if (!mlir::isa<ltl::SequenceType, ltl::PropertyType>(valueType)) {
value = context.convertToI1(value);
}
if (!value)
return {};
// Handle repetition
// The optional repetition is empty, return the converted expression
if (!expr.repetition.has_value()) {
return value;

4
lib/Conversion/ImportVerilog/Expressions.cpp
View File

@ -1065,6 +1065,10 @@ struct RvalueExprVisitor : public ExprVisitor {
return builder.create<moore::ConcatOp>(loc, slicedOperands);
}
Value visit(const slang::ast::AssertionInstanceExpression &expr) {
return context.convertAssertionExpression(expr.body, loc);
}
/// Emit an error for all other expressions.
template <typename T>
Value visit(T &&node) {

12
lib/Conversion/ImportVerilog/Structure.cpp
View File

@ -566,6 +566,18 @@ struct ModuleVisitor : public BaseVisitor {
return success();
}
// Ignore sequence declarations. The declarations are already evaluated by
// Slang and are part of an AssertionInstance.
LogicalResult visit(const slang::ast::SequenceSymbol &seqNode) {
return success();
}
// Ignore property declarations. The declarations are already evaluated by
// Slang and are part of an AssertionInstance.
LogicalResult visit(const slang::ast::PropertySymbol &propNode) {
return success();
}
// Handle functions and tasks.
LogicalResult visit(const slang::ast::SubroutineSymbol &subroutine) {
return context.convertFunction(subroutine);

96
test/Conversion/ImportVerilog/basic.sv
View File

@ -2570,6 +2570,102 @@ module ConcurrentAssert(input clk);
// CHECK: }
assert property (@(posedge clk) a);
// Sequence declaration
// CHECK: moore.procedure always {
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
// CHECK: [[RES:%.+]] = ltl.concat %6, %9 : !ltl.sequence, !ltl.sequence
// CHECK: verif.assert [[RES]] : !ltl.sequence
// CHECK: moore.return
// CHECK: }
sequence s1;
a ##1 b;
endsequence
assert property (s1);
// CHECK: moore.procedure always {
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[TRUE:%.+]] = hw.constant true
// CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
// CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
// CHECK: [[OP3:%.+]] = ltl.delay [[B]], 1, 0 : i1
// CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
// CHECK: [[RES:%.+]] = ltl.intersect [[OP4]], [[A]] : !ltl.sequence, i1
// CHECK: verif.assert [[RES]] : !ltl.sequence
// CHECK: moore.return
// CHECK: }
sequence s2(x, y);
x within y;
endsequence
assert property (s2(b, a));
// CHECK: moore.procedure always {
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[DA:%.+]] = ltl.delay [[A]], 0, 0 : i1
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[DB:%.+]] = ltl.delay [[B]], 1, 0 : i1
// CHECK: [[OP1:%.+]] = ltl.concat [[DA]], [[DB]] : !ltl.sequence, !ltl.sequence
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B2:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[RES:%.+]] = ltl.implication [[OP1]], [[B2]] : !ltl.sequence, i1
// CHECK: verif.assert [[RES]] : !ltl.property
// CHECK: moore.return
// CHECK: }
property p1;
s1 |-> b;
endproperty
assert property (p1);
// CHECK: moore.procedure always {
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A1:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A2:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B1:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[TRUE:%.+]] = hw.constant true
// CHECK: [[OP1:%.+]] = ltl.repeat [[TRUE]], 0 : i1
// CHECK: [[OP2:%.+]] = ltl.delay [[OP1]], 1, 0 : !ltl.sequence
// CHECK: [[OP3:%.+]] = ltl.delay [[A2]], 1, 0 : i1
// CHECK: [[OP4:%.+]] = ltl.concat [[OP2]], [[OP3]], [[TRUE]] : !ltl.sequence, !ltl.sequence, i1
// CHECK: [[OP5:%.+]] = ltl.intersect [[OP4]], [[B1]] : !ltl.sequence, i1
// CHECK: [[TRUE1:%.+]] = hw.constant true
// CHECK: [[OP6:%.+]] = ltl.repeat [[TRUE1]], 0 : i1
// CHECK: [[OP7:%.+]] = ltl.delay [[OP6]], 1, 0 : !ltl.sequence
// CHECK: [[OP8:%.+]] = ltl.delay [[A1]], 1, 0 : i1
// CHECK: [[OP9:%.+]] = ltl.concat [[OP7]], [[OP8]], [[TRUE1]] : !ltl.sequence, !ltl.sequence, i1
// CHECK: [[OP10:%.+]] = ltl.intersect [[OP9]], [[OP5]] : !ltl.sequence, !ltl.sequence
// CHECK: [[TMP:%.+]] = moore.read %a : <i1>
// CHECK: [[A3:%.+]] = moore.conversion [[TMP]] : !moore.i1 -> i1
// CHECK: [[DA3:%.+]] = ltl.delay [[A3]], 0, 0 : i1
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B2:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[DB2:%.+]] = ltl.delay [[B2]], 1, 0 : i1
// CHECK: [[OP11:%.+]] = ltl.concat [[DA3]], [[DB2]] : !ltl.sequence, !ltl.sequence
// CHECK: [[TMP:%.+]] = moore.read %b : <l1>
// CHECK: [[B3:%.+]] = moore.conversion [[TMP]] : !moore.l1 -> i1
// CHECK: [[OP12:%.+]] = ltl.implication [[OP11]], [[B3]] : !ltl.sequence, i1
// CHECK: [[TRUE2:%.+]] = hw.constant true
// CHECK: [[OP13:%.+]] = ltl.delay [[OP10]], 1, 0 : !ltl.sequence
// CHECK: [[OP14:%.+]] = ltl.concat [[OP13]], [[TRUE2]] : !ltl.sequence, i1
// CHECK: [[RES:%.+]] = ltl.implication [[OP14]], [[OP12]] : !ltl.sequence, !ltl.property
// CHECK: verif.assert [[RES]] : !ltl.property
// CHECK: moore.return
// CHECK: }
property p2(x, y);
s2(x, y) |=> p1;
endproperty
assert property (p2(a, s2(a, b)));
endmodule
// CHECK: [[TMP:%.+]] = moore.constant 42 : i32