[FIRRTL] Add Inline Formal Test ops

include/circt/Dialect/FIRRTL/FIRRTLDeclarations.td

@@ -36,8 +36,8 @@ class ReferableDeclOp<string mnemonic, list<Trait> traits = []> :
 /// located in a hardware-creating context, such as the body of a module.
 class HardwareDeclOp<string mnemonic, list <Trait> traits = []> :
   ReferableDeclOp<mnemonic, traits # [
-    ParentOneOf<[
-      "firrtl::FModuleOp", "firrtl::LayerBlockOp",
+    ParentOneOf<[ 
+      "firrtl::FormalOp", "firrtl::FModuleOp", "firrtl::LayerBlockOp",
       "firrtl::WhenOp", "firrtl::MatchOp", "sv::IfDefOp"]>]> {}
 
 def InstanceOp : HardwareDeclOp<"instance", [
@@ -336,6 +336,45 @@ def MemOp : HardwareDeclOp<"mem", [DeclareOpInterfaceMethods<CombDataflow>]> {
   }];
 }
 
+def SymbolicOp : FIRRTLOp<"symbolic", [
+  HasParent<"firrtl::FormalOp">, HasCustomSSAName
+]> {
+  let summary = "Produce a symbolic value (non-deterministic value)";
+  let description = [{
+    The symbolic operation produces a symbolic value of UInt Type. This 
+    is solely used in the context of formal verification in order to reason 
+    about module instance inputs in a symbolic manner.  
+    Example:  
+    ```mlir  
+    %foo.in = firrtl.symbolic : t1
+    %foo.out = firrtl.instance "foo" @Foo(in: %foo.in : t1) -> (t1)
+    %cond = firrtl.geq %foo.in, foo.out : (t1, t1) -> (t1)
+    firrtl.int.verif.assert %cond : t1
+    ```
+  }];
+
+  let arguments = (ins StrAttr:$name);
+  let results = (outs UIntType:$result);
+
+  let skipDefaultBuilders = true;
+
+  let builders = [
+    OpBuilder<(ins "::mlir::Type":$elementType,
+                   "::mlir::StringAttr":$name), [{
+      $_state.addAttribute(getNameAttrName($_state.name), name);
+      $_state.addTypes(elementType);
+    }]>,
+    OpBuilder<(ins "::mlir::Type":$elementType,
+                   "::llvm::StringRef":$name), [{
+      return build($_builder, $_state, elementType, $_builder.getStringAttr(name));
+    }]>
+  ];
+
+  let assemblyFormat = [{
+    custom<ImplicitSSAName>(attr-dict) `:`qualified(type($result))
+  }];
+}
+
 def NodeOp : HardwareDeclOp<"node", [
       AllTypesMatch<["input","result"]>,
       DeclareOpInterfaceMethods<InferTypeOpInterface, ["inferReturnTypes"]>,

include/circt/Dialect/FIRRTL/FIRRTLStructure.td

@@ -448,6 +448,42 @@ def LayerOp : FIRRTLOp<
   }];
 }
 
+def FormalOp : FIRRTLOp<"formal", [
+    IsolatedFromAbove,
+    Symbol,
+    NoTerminator,
+    HasParent<"firrtl::CircuitOp">
+]> {
+  let summary = "A formal test definition.";
+  let description = [{
+    The `firrtl.formal` operation defines a formal verification problem in the same 
+    context as the rest of the design. This problem is solved using bounded model 
+    checking and should be given a bound k, which represents the number of cycles considered 
+    during model checking.
+
+    Example:
+    ```mlir
+
+    firrtl.formal @formal1(k=20) {
+      %bar, %out = firrtl.instance foo @Foo(in bar: !firrtl.uint<8>, out out: !firrtl.uint<8>) 
+      %c42_8 = firrtl.constant 42 : !firrtl.uint<8>
+      firrtl.connect %bar, %c42_8: !firrtl.uint<8>, !firrtl.uint<8>
+      %c69_8 = firrtl.constant 69 : !firrtl.uint<8>
+      %cond = firrtl.eq %c69_8, %out : (!firrtl.uint<8>, !firrtl.uint<8>) -> !firrtl.uint<1>
+      firrtl.assert %cond
+    }
+}
+    ```
+  }];
+
+  let arguments = (ins SymbolNameAttr:$sym_name, UI64Attr:$k);
+  let results = (outs);
+  let regions = (region SizedRegion<1>:$body);
+  let assemblyFormat = [{
+    $sym_name `(` `k` `=` $k `)` attr-dict-with-keyword $body
+  }];
+}
+
 def OptionOp : FIRRTLOp<"option", [
     IsolatedFromAbove,
     Symbol,

include/circt/Dialect/FIRRTL/FIRRTLVisitors.h

@@ -304,7 +304,7 @@ class DeclVisitor {
     auto *thisCast = static_cast<ConcreteType *>(this);
     return TypeSwitch<Operation *, ResultType>(op)
         .template Case<InstanceOp, InstanceChoiceOp, ObjectOp, MemOp, NodeOp,
-                       RegOp, RegResetOp, WireOp, VerbatimWireOp>(
+                       RegOp, RegResetOp, SymbolicOp, WireOp, VerbatimWireOp>(
             [&](auto opNode) -> ResultType {
               return thisCast->visitDecl(opNode, args...);
             })
@@ -337,6 +337,7 @@ class DeclVisitor {
   HANDLE(NodeOp);
   HANDLE(RegOp);
   HANDLE(RegResetOp);
+  HANDLE(SymbolicOp);
   HANDLE(WireOp);
   HANDLE(VerbatimWireOp);
 #undef HANDLE

lib/Dialect/FIRRTL/Export/FIREmitter.cpp

@@ -60,6 +60,7 @@ struct Emitter {
   void emitModuleParameters(Operation *op, ArrayAttr parameters);
   void emitDeclaration(LayerOp op);
   void emitDeclaration(OptionOp op);
+  void emitDeclaration(FormalOp op);
   void emitEnabledLayers(ArrayRef<Attribute> layers);
 
   void emitParamAssign(ParamDeclAttr param, Operation *op,
@@ -70,6 +71,7 @@ struct Emitter {
   void emitStatementsInBlock(Block &block);
   void emitStatement(WhenOp op);
   void emitStatement(WireOp op);
+  void emitStatement(SymbolicOp op);
   void emitStatement(RegOp op);
   void emitStatement(RegResetOp op);
   void emitStatement(NodeOp op);
@@ -406,6 +408,7 @@ void Emitter::emitCircuit(CircuitOp op) {
           })
           .Case<LayerOp>([&](auto op) { emitDeclaration(op); })
           .Case<OptionOp>([&](auto op) { emitDeclaration(op); })
+          .Case<FormalOp>([&](auto op) { emitDeclaration(op); })
           .Default([&](auto op) {
             emitOpError(op, "not supported for emission inside circuit");
           });
@@ -623,6 +626,26 @@ void Emitter::emitDeclaration(OptionOp op) {
   ps << PP::newline << PP::newline;
 }
 
+/// Emit a formal test definition.
+void Emitter::emitDeclaration(FormalOp op) {
+  startStatement();
+  ps << "formal " << PPExtString(op.getSymName()) << ", "
+     << "k = ";
+  ps.addAsString(op.getK());
+
+  if (auto outputFile = op->getAttrOfType<hw::OutputFileAttr>("output_file")) {
+    ps << ", ";
+    ps.writeQuotedEscaped(outputFile.getFilename().getValue());
+  }
+
+  ps << " : ";
+  emitLocationAndNewLine(op);
+  ps.scopedBox(PP::bbox2, [&]() {
+    // Emit the test's body
+    emitStatementsInBlock(op.getBody().front());
+  });
+}
+
 /// Check if an operation is inlined into the emission of their users. For
 /// example, subfields are always inlined.
 static bool isEmittedInline(Operation *op) {
@@ -643,8 +666,8 @@ void Emitter::emitStatementsInBlock(Block &block) {
     if (isEmittedInline(&bodyOp))
       continue;
     TypeSwitch<Operation *>(&bodyOp)
-        .Case<WhenOp, WireOp, RegOp, RegResetOp, NodeOp, StopOp, SkipOp,
-              PrintFOp, AssertOp, AssumeOp, CoverOp, ConnectOp,
+        .Case<WhenOp, WireOp, SymbolicOp, RegOp, RegResetOp, NodeOp, StopOp,
+              SkipOp, PrintFOp, AssertOp, AssumeOp, CoverOp, ConnectOp,
               MatchingConnectOp, PropAssignOp, InstanceOp, InstanceChoiceOp,
               AttachOp, MemOp, InvalidValueOp, SeqMemOp, CombMemOp,
               MemoryPortOp, MemoryDebugPortOp, MemoryPortAccessOp, RefDefineOp,
@@ -699,6 +722,16 @@ void Emitter::emitStatement(WireOp op) {
   emitLocationAndNewLine(op);
 }
 
+void Emitter::emitStatement(SymbolicOp op) {
+  auto legalName = legalize(op.getNameAttr());
+  startStatement();
+  ps.scopedBox(PP::ibox2, [&]() {
+    ps << "symbolic " << PPExtString(legalName);
+    emitTypeWithColon(op.getResult().getType());
+  });
+  emitLocationAndNewLine(op);
+}
+
 void Emitter::emitStatement(RegOp op) {
   auto legalName = legalize(op.getNameAttr());
   addForceable(op, legalName);

lib/Dialect/FIRRTL/FIRRTLOps.cpp

@@ -3352,6 +3352,10 @@ void RegResetOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
   return forceableAsmResultNames(*this, getName(), setNameFn);
 }
 
+void SymbolicOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
+  setNameFn(getResult(), getName());
+}
+
 void WireOp::getAsmResultNames(OpAsmSetValueNameFn setNameFn) {
   return forceableAsmResultNames(*this, getName(), setNameFn);
 }

lib/Dialect/FIRRTL/Import/FIRParser.cpp

@@ -1747,6 +1747,7 @@ struct FIRStmtParser : public FIRParser {
   ParseResult parseRWProbe(Value &result);
   ParseResult parseLeadingExpStmt(Value lhs);
   ParseResult parseConnect();
+  ParseResult parseSymbolic();
   ParseResult parseInvalidate();
   ParseResult parseLayerBlockOrGroup(unsigned indent);
 
@@ -2666,6 +2667,8 @@ ParseResult FIRStmtParser::parseSimpleStmtImpl(unsigned stmtIndent) {
     return parseNode();
   case FIRToken::kw_wire:
     return parseWire();
+  case FIRToken::kw_symbolic:
+    return parseSymbolic();
   case FIRToken::kw_reg:
     return parseRegister(stmtIndent);
   case FIRToken::kw_regreset:
@@ -3797,6 +3800,28 @@ ParseResult FIRStmtParser::parseConnect() {
   return success();
 }
 
+ParseResult FIRStmtParser::parseSymbolic() {
+  auto startTok = consumeToken(FIRToken::kw_symbolic);
+
+  // If this was actually the start of a connect or something else handle
+  // that.
+  if (auto isExpr = parseExpWithLeadingKeyword(startTok))
+    return *isExpr;
+
+  StringRef id;
+  FIRRTLType type;
+  if (parseId(id, "expected symbolic value name") ||
+      parseToken(FIRToken::colon, "expected ':' in symbolic value") ||
+      parseType(type, "expected symbolic value type") || parseOptionalInfo())
+    return failure();
+
+  locationProcessor.setLoc(startTok.getLoc());
+
+  auto result = builder.create<SymbolicOp>(type, id);
+  return moduleContext.addSymbolEntry(id, result.getResult(),
+                                      startTok.getLoc());
+}
+
 /// propassign ::= 'propassign' expr expr
 ParseResult FIRStmtParser::parsePropAssign() {
   auto startTok = consumeToken(FIRToken::kw_propassign);
@@ -4585,6 +4610,7 @@ struct FIRCircuitParser : public FIRParser {
   ParseResult parseExtModule(CircuitOp circuit, unsigned indent);
   ParseResult parseIntModule(CircuitOp circuit, unsigned indent);
   ParseResult parseModule(CircuitOp circuit, bool isPublic, unsigned indent);
+  ParseResult parseFormal(CircuitOp circuit, unsigned indent);
 
   ParseResult parseLayerName(SymbolRefAttr &result);
   ParseResult parseOptionalEnabledLayers(ArrayAttr &result);
@@ -4890,6 +4916,7 @@ ParseResult FIRCircuitParser::skipToModuleEnd(unsigned indent) {
     case FIRToken::kw_extclass:
     case FIRToken::kw_extmodule:
     case FIRToken::kw_intmodule:
+    case FIRToken::kw_formal:
     case FIRToken::kw_module:
     case FIRToken::kw_public:
     case FIRToken::kw_layer:
@@ -5153,6 +5180,47 @@ ParseResult FIRCircuitParser::parseModule(CircuitOp circuit, bool isPublic,
   return success();
 }
 
+ParseResult FIRCircuitParser::parseFormal(CircuitOp circuit, unsigned indent) {
+  consumeToken(FIRToken::kw_formal);
+  StringRef id, kSpelling;
+  int64_t k = -1;
+  LocWithInfo info(getToken().getLoc(), this);
+
+  // Parse the formal operation
+  if (parseId(id, "expected a formal test name") ||
+      parseToken(FIRToken::comma, "expected ','") ||
+      parseGetSpelling(kSpelling) ||
+      parseToken(FIRToken::identifier, "expected parameter 'k' after ','") ||
+      parseToken(FIRToken::equal, "expected '=' after 'k'") ||
+      parseIntLit(k, "expected integer in k specification") ||
+      parseToken(FIRToken::colon,
+                 "expected ':' after option group definition") ||
+      info.parseOptionalInfo())
+    return failure();
+
+  // Check that the parameter is valid
+  if (kSpelling != "k" || k <= 0)
+    return emitError("Invalid parameter given to formal test: ") << kSpelling,
+           failure();
+
+  // Build out the firrtl mlir op
+  auto builder = circuit.getBodyBuilder();
+  auto formal = builder.create<firrtl::FormalOp>(info.getLoc(), id, k);
+  auto &body = formal.getBody().emplaceBlock();
+
+  // Create the statement parser
+  hw::InnerSymbolNamespace ns(circuit);
+  SymbolTable circuitSymTbl(circuit);
+  FIRModuleContext context(getConstants(), getLexer(), version);
+  FIRStmtParser stmtParser(body, context, ns, circuitSymTbl, version);
+
+  // If we've reached a new indentation, parse the internal region
+  if (getIndentation() > indent)
+    if (stmtParser.parseSimpleStmtBlock(indent))
+      return failure();
+  return success();
+}
+
 ParseResult FIRCircuitParser::parseToplevelDefinition(CircuitOp circuit,
                                                       unsigned indent) {
   switch (getToken().getKind()) {
@@ -5167,6 +5235,10 @@ ParseResult FIRCircuitParser::parseToplevelDefinition(CircuitOp circuit,
     return parseExtClass(circuit, indent);
   case FIRToken::kw_extmodule:
     return parseExtModule(circuit, indent);
+  case FIRToken::kw_formal:
+    if (requireFeature({4, 0, 0}, "inline formal tests"))
+      return failure();
+    return parseFormal(circuit, indent);
   case FIRToken::kw_intmodule:
     if (removedFeature({4, 0, 0}, "intrinsic modules"))
       return failure();
@@ -5514,6 +5586,7 @@ ParseResult FIRCircuitParser::parseCircuit(
     case FIRToken::kw_extmodule:
     case FIRToken::kw_intmodule:
     case FIRToken::kw_layer:
+    case FIRToken::kw_formal:
     case FIRToken::kw_module:
     case FIRToken::kw_option:
     case FIRToken::kw_public:

lib/Dialect/FIRRTL/Import/FIRTokenKinds.def

@@ -117,6 +117,7 @@ TOK_KEYWORD(extclass)
 TOK_KEYWORD(extmodule)
 TOK_KEYWORD(false)
 TOK_KEYWORD(flip)
+TOK_KEYWORD(formal)
 TOK_KEYWORD(group)
 TOK_KEYWORD(infer)
 TOK_KEYWORD(input)
@@ -151,6 +152,7 @@ TOK_KEYWORD(regreset)
 TOK_KEYWORD(reset)
 TOK_KEYWORD(skip)
 TOK_KEYWORD(smem)
+TOK_KEYWORD(symbolic)
 TOK_KEYWORD(true)
 TOK_KEYWORD(type)
 TOK_KEYWORD(undefined)

test/Dialect/FIRRTL/errors.mlir

@@ -279,7 +279,7 @@ firrtl.circuit "Foo" {
 
 firrtl.circuit "Foo" {
   firrtl.extmodule @Foo()
-  // expected-error @+1 {{'firrtl.instance' op expects parent op to be one of 'firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
+  // expected-error @+1 {{'firrtl.instance' op expects parent op to be one of 'firrtl.formal, firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
   firrtl.instance "" @Foo()
 }
 
@@ -1829,7 +1829,7 @@ firrtl.circuit "ClassCannotHaveHardwarePorts" {
 firrtl.circuit "ClassCannotHaveWires" {
   firrtl.module @ClassCannotHaveWires() {}
   firrtl.class @ClassWithWire() {
-    // expected-error @below {{'firrtl.wire' op expects parent op to be one of 'firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
+    // expected-error @below {{'firrtl.wire' op expects parent op to be one of 'firrtl.formal, firrtl.module, firrtl.layerblock, firrtl.when, firrtl.match, sv.ifdef'}}
     %w = firrtl.wire : !firrtl.uint<8>
   }
 }