mirror of https://github.com/llvm/circt.git
[FIRRTL] Fix folding of when conditions into LTL properties (#7760)
Make ExpandWhen's folding of the when condition into LTL properties work
for more inputs. This used to be very brittle and the condition would
be mapped to a new implication around the entire property:
when (a):
assert(@(posedge clock) b |-> c)
used to become
assert(a |-> @(posedge clock) b |-> c)
This commit improves on this by always pushing implications behind
clocks, and by merging implications like `a |-> b |-> c` into a single
`(a & b) |-> c`. As a result, ExpandWhens now produces the following
output, which is more in line with what users expect:
assert(@(posedge clock) a & b |-> c)
Also add a FIR-to-Verilog test to nail this behavior down and ensure we
don't regress on user expectations.
This commit is contained in:
Fabian Schuiki
GitHub
parent
c08df96a5a
commit
a7bd275fb9
|
|
@ -551,24 +551,82 @@ private:
|
|||
|
||||
/// Concurrent and of a property with the current condition. If we are in
|
||||
/// the outer scope, i.e. not in a WhenOp region, then there is no condition.
|
||||
Value ltlAndWithCondition(Operation *op, Value value) {
|
||||
// 'ltl.and' the value with the current condition.
|
||||
return OpBuilder(op).createOrFold<LTLAndIntrinsicOp>(
|
||||
condition.getLoc(), condition.getType(), condition, value);
|
||||
Value ltlAndWithCondition(Operation *op, Value property) {
|
||||
// Look through nodes.
|
||||
while (auto nodeOp = property.getDefiningOp<NodeOp>())
|
||||
property = nodeOp.getInput();
|
||||
|
||||
// Look through `ltl.clock` ops.
|
||||
if (auto clockOp = property.getDefiningOp<LTLClockIntrinsicOp>()) {
|
||||
auto input = ltlAndWithCondition(op, clockOp.getInput());
|
||||
auto &newClockOp = createdLTLClockOps[{clockOp, input}];
|
||||
if (!newClockOp) {
|
||||
newClockOp = OpBuilder(op).cloneWithoutRegions(clockOp);
|
||||
newClockOp.getInputMutable().assign(input);
|
||||
}
|
||||
return newClockOp;
|
||||
}
|
||||
|
||||
// Otherwise create a new `ltl.and` with the condition.
|
||||
auto &newOp = createdLTLAndOps[{condition, property}];
|
||||
if (!newOp)
|
||||
newOp = OpBuilder(op).createOrFold<LTLAndIntrinsicOp>(
|
||||
condition.getLoc(), property.getType(), condition, property);
|
||||
return newOp;
|
||||
}
|
||||
|
||||
/// Overlapping implication with the condition as its antecedent and a given
|
||||
/// property as the consequent. If we are in the outer scope, i.e. not in a
|
||||
/// WhenOp region, then there is no condition.
|
||||
Value ltlImplicationWithCondition(Operation *op, Value value) {
|
||||
// 'and' the value with the current condition.
|
||||
return OpBuilder(op).createOrFold<LTLImplicationIntrinsicOp>(
|
||||
condition.getLoc(), condition.getType(), condition, value);
|
||||
Value ltlImplicationWithCondition(Operation *op, Value property) {
|
||||
// Look through nodes.
|
||||
while (auto nodeOp = property.getDefiningOp<NodeOp>())
|
||||
property = nodeOp.getInput();
|
||||
|
||||
// Look through `ltl.clock` ops.
|
||||
if (auto clockOp = property.getDefiningOp<LTLClockIntrinsicOp>()) {
|
||||
auto input = ltlImplicationWithCondition(op, clockOp.getInput());
|
||||
auto &newClockOp = createdLTLClockOps[{clockOp, input}];
|
||||
if (!newClockOp) {
|
||||
newClockOp = OpBuilder(op).cloneWithoutRegions(clockOp);
|
||||
newClockOp.getInputMutable().assign(input);
|
||||
}
|
||||
return newClockOp;
|
||||
}
|
||||
|
||||
// Merge condition into `ltl.implication` left-hand side.
|
||||
if (auto implOp = property.getDefiningOp<LTLImplicationIntrinsicOp>()) {
|
||||
auto lhs = ltlAndWithCondition(op, implOp.getLhs());
|
||||
auto &newImplOp = createdLTLImplicationOps[{lhs, implOp.getRhs()}];
|
||||
if (!newImplOp) {
|
||||
auto clonedOp = OpBuilder(op).cloneWithoutRegions(implOp);
|
||||
clonedOp.getLhsMutable().assign(lhs);
|
||||
newImplOp = clonedOp;
|
||||
}
|
||||
return newImplOp;
|
||||
}
|
||||
|
||||
// Otherwise create a new `ltl.implication` with the condition on the LHS.
|
||||
auto &newImplOp = createdLTLImplicationOps[{condition, property}];
|
||||
if (!newImplOp)
|
||||
newImplOp = OpBuilder(op).createOrFold<LTLImplicationIntrinsicOp>(
|
||||
condition.getLoc(), property.getType(), condition, property);
|
||||
return newImplOp;
|
||||
}
|
||||
|
||||
private:
|
||||
/// The current wrapping condition. If null, we are in the outer scope.
|
||||
Value condition;
|
||||
|
||||
/// The `ltl.and` operations that have been created.
|
||||
SmallDenseMap<std::pair<Value, Value>, Value> createdLTLAndOps;
|
||||
|
||||
/// The `ltl.implication` operations that have been created.
|
||||
SmallDenseMap<std::pair<Value, Value>, Value> createdLTLImplicationOps;
|
||||
|
||||
/// The `ltl.clock` operations that have been created.
|
||||
SmallDenseMap<std::pair<LTLClockIntrinsicOp, Value>, LTLClockIntrinsicOp>
|
||||
createdLTLClockOps;
|
||||
};
|
||||
} // namespace
|
||||
|
||||
|
|
|
|||
|
|
@ -650,70 +650,62 @@ firrtl.module @ModuleWithObjectWire(in %in: !firrtl.class<@ClassWithInput(in in:
|
|||
firrtl.propassign %0, %in : !firrtl.class<@ClassWithInput(in in: !firrtl.string)>
|
||||
}
|
||||
|
||||
// Test all verif assert/assume/cover constructs
|
||||
// CHECK-LABEL: firrtl.module @verifassert
|
||||
firrtl.module @verifassert(
|
||||
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
|
||||
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
|
||||
// Conditions of when blocks should be folded into the LHS of implications in
|
||||
// assert/assume ops, or int othe LHS of ands in cover ops.
|
||||
// CHECK-LABEL: firrtl.module @WhenAroundPropertyAssertAssumeCover
|
||||
firrtl.module @WhenAroundPropertyAssertAssumeCover(
|
||||
in %clock: !firrtl.clock,
|
||||
in %a: !firrtl.uint<1>,
|
||||
in %b: !firrtl.uint<1>,
|
||||
in %c: !firrtl.uint<1>,
|
||||
in %d: !firrtl.uint<1>
|
||||
) {
|
||||
firrtl.when %cond : !firrtl.uint<1> {
|
||||
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.assert [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// b |-> c
|
||||
// CHECK: [[P0:%.+]] = firrtl.int.ltl.implication %b, %c :
|
||||
%0 = firrtl.int.ltl.implication %b, %c : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
%p0 = firrtl.node interesting_name %0 : !firrtl.uint<1>
|
||||
// @(posedge clock) b |-> c
|
||||
%1 = firrtl.int.ltl.clock %p0, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
%p1 = firrtl.node interesting_name %1 : !firrtl.uint<1>
|
||||
|
||||
firrtl.int.verif.assert %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
// CHECK-NOT: firrtl.when
|
||||
firrtl.when %a : !firrtl.uint<1> {
|
||||
// CHECK: [[TMP1:%.+]] = firrtl.int.ltl.and %a, %b
|
||||
// CHECK: [[TMP2:%.+]] = firrtl.int.ltl.implication [[TMP1]], %c
|
||||
// CHECK: [[TMP3:%.+]] = firrtl.int.ltl.clock [[TMP2]], %clock
|
||||
// CHECK: firrtl.int.verif.assert [[TMP3]], %d :
|
||||
// CHECK: firrtl.int.verif.assert [[TMP3]] :
|
||||
// CHECK: firrtl.int.verif.assume [[TMP3]], %d :
|
||||
// CHECK: firrtl.int.verif.assume [[TMP3]] :
|
||||
firrtl.int.verif.assert %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.assert %p1 : !firrtl.uint<1>
|
||||
firrtl.int.verif.assume %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.assume %p1 : !firrtl.uint<1>
|
||||
// CHECK: [[TMP1:%.+]] = firrtl.int.ltl.and %a, [[P0]]
|
||||
// CHECK: [[TMP2:%.+]] = firrtl.int.ltl.clock [[TMP1]], %clock
|
||||
// CHECK: firrtl.int.verif.cover [[TMP2]], %d :
|
||||
// CHECK: firrtl.int.verif.cover [[TMP2]] :
|
||||
firrtl.int.verif.cover %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.cover %p1 : !firrtl.uint<1>
|
||||
} else {
|
||||
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.assert [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
firrtl.int.verif.assert %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
}
|
||||
}
|
||||
|
||||
// CHECK-LABEL: firrtl.module @verifassume
|
||||
firrtl.module @verifassume(
|
||||
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
|
||||
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
|
||||
) {
|
||||
firrtl.when %cond : !firrtl.uint<1> {
|
||||
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.implication %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.assume [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
|
||||
firrtl.int.verif.assume %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
} else {
|
||||
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.implication [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.assume [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
firrtl.int.verif.assume %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
}
|
||||
}
|
||||
|
||||
// CHECK-LABEL: firrtl.module @verifcover
|
||||
firrtl.module @verifcover(
|
||||
in %clock : !firrtl.clock, in %cond : !firrtl.uint<1>, in %prop : !firrtl.uint<1>, in %prop1 : !firrtl.uint<1>,
|
||||
in %enable : !firrtl.uint<1>, in %enable1 : !firrtl.uint<1>, in %reset : !firrtl.uint<1>
|
||||
) {
|
||||
firrtl.when %cond : !firrtl.uint<1> {
|
||||
// CHECK: [[TMP2A:%.+]] = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP0A:%.+]] = firrtl.int.ltl.and %cond, [[TMP2A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.cover [[TMP0A]], %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
|
||||
firrtl.int.verif.cover %clk_prop, %enable : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
} else {
|
||||
// CHECK: [[TMP3A:%.+]] = firrtl.not %cond : (!firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP6A:%.+]] = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
// CHECK: [[TMP4A:%.+]] = firrtl.int.ltl.and [[TMP3A]], [[TMP6A]] : (!firrtl.uint<1>, !firrtl.uint<1>) -> !firrtl.uint<1>
|
||||
// CHECK: firrtl.int.verif.cover [[TMP4A]], %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
%clk_prop = firrtl.int.ltl.clock %prop1, %clock : (!firrtl.uint<1>, !firrtl.clock) -> !firrtl.uint<1>
|
||||
firrtl.int.verif.cover %clk_prop, %enable1 : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
// CHECK: [[NOTA:%.+]] = firrtl.not %a
|
||||
// CHECK: [[TMP1:%.+]] = firrtl.int.ltl.and [[NOTA]], %b
|
||||
// CHECK: [[TMP2:%.+]] = firrtl.int.ltl.implication [[TMP1]], %c
|
||||
// CHECK: [[TMP3:%.+]] = firrtl.int.ltl.clock [[TMP2]], %clock
|
||||
// CHECK: firrtl.int.verif.assert [[TMP3]], %d :
|
||||
// CHECK: firrtl.int.verif.assert [[TMP3]] :
|
||||
// CHECK: firrtl.int.verif.assume [[TMP3]], %d :
|
||||
// CHECK: firrtl.int.verif.assume [[TMP3]] :
|
||||
firrtl.int.verif.assert %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.assert %p1 : !firrtl.uint<1>
|
||||
firrtl.int.verif.assume %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.assume %p1 : !firrtl.uint<1>
|
||||
// CHECK: [[TMP1:%.+]] = firrtl.int.ltl.and [[NOTA]], [[P0]]
|
||||
// CHECK: [[TMP2:%.+]] = firrtl.int.ltl.clock [[TMP1]], %clock
|
||||
// CHECK: firrtl.int.verif.cover [[TMP2]], %d :
|
||||
// CHECK: firrtl.int.verif.cover [[TMP2]] :
|
||||
firrtl.int.verif.cover %p1, %d : !firrtl.uint<1>, !firrtl.uint<1>
|
||||
firrtl.int.verif.cover %p1 : !firrtl.uint<1>
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,59 @@
|
|||
; RUN: firtool %s | FileCheck %s
|
||||
FIRRTL version 4.0.0
|
||||
|
||||
circuit Foo :
|
||||
public module Foo :
|
||||
input clock : Clock
|
||||
input a : UInt<1>
|
||||
input b : UInt<1>
|
||||
input c : UInt<1>
|
||||
input d : UInt<1>
|
||||
|
||||
; b |-> c
|
||||
node p0 = intrinsic(circt_ltl_implication : UInt<1>, b, c)
|
||||
; @(posedge clock) b |-> c
|
||||
node p1 = intrinsic(circt_ltl_clock : UInt<1>, p0, clock)
|
||||
|
||||
when a :
|
||||
; CHECK: assert property (@(posedge clock) disable iff (d) a & b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) disable iff (d) a & b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) disable iff (d) a and (b |-> c));
|
||||
intrinsic(circt_verif_assert, p1, not(d))
|
||||
intrinsic(circt_verif_assume, p1, not(d))
|
||||
intrinsic(circt_verif_cover, p1, not(d))
|
||||
|
||||
; CHECK: assert property (@(posedge clock) a & b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) a & b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) a and (b |-> c));
|
||||
intrinsic(circt_verif_assert, p1)
|
||||
intrinsic(circt_verif_assume, p1)
|
||||
intrinsic(circt_verif_cover, p1)
|
||||
|
||||
else :
|
||||
; CHECK: assert property (@(posedge clock) disable iff (d) ~a & b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) disable iff (d) ~a & b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) disable iff (d) ~a and (b |-> c));
|
||||
intrinsic(circt_verif_assert, p1, not(d))
|
||||
intrinsic(circt_verif_assume, p1, not(d))
|
||||
intrinsic(circt_verif_cover, p1, not(d))
|
||||
|
||||
; CHECK: assert property (@(posedge clock) ~a & b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) ~a & b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) ~a and (b |-> c));
|
||||
intrinsic(circt_verif_assert, p1)
|
||||
intrinsic(circt_verif_assume, p1)
|
||||
intrinsic(circt_verif_cover, p1)
|
||||
|
||||
; CHECK: assert property (@(posedge clock) disable iff (d) b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) disable iff (d) b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) disable iff (d) b |-> c);
|
||||
intrinsic(circt_verif_assert, p1, not(d))
|
||||
intrinsic(circt_verif_assume, p1, not(d))
|
||||
intrinsic(circt_verif_cover, p1, not(d))
|
||||
|
||||
; CHECK: assert property (@(posedge clock) b |-> c);
|
||||
; CHECK: assume property (@(posedge clock) b |-> c);
|
||||
; CHECK: cover property (@(posedge clock) b |-> c);
|
||||
intrinsic(circt_verif_assert, p1)
|
||||
intrinsic(circt_verif_assume, p1)
|
||||
intrinsic(circt_verif_cover, p1)
|
||||
Loading…
Reference in New Issue