[FIRRTL] Add support for new Verification statements (assert, assume,…

… cover) (#168) * [FIRRTL] Add "assert" verification statement * [FIRRTL] Add "assume" verification statement * [FIRRTL] Add "cover" verification statement Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
llvm · Oct 20, 2020 · 046eebb · 046eebb
1 parent 64dd773
commit 046eebb
Show file tree

Hide file tree

Showing 4 changed files with 131 additions and 0 deletions.
diff --git a/include/circt/Dialect/FIRRTL/OpStatements.td b/include/circt/Dialect/FIRRTL/OpStatements.td
@@ -125,6 +125,42 @@ def StopOp : FIRRTLOp<"stop", []> {
   }];
 }
 
+def AssertOp : FIRRTLOp<"assert", []> {
+  let summary = "Assert Verification Statement";
+
+  let arguments = (ins ClockType:$clock, UInt1Type:$predicate, UInt1Type:$enable,
+    StrAttr:$message);
+  let results = (outs);
+
+  let assemblyFormat = [{
+    $clock `,` $predicate `,` $enable `,` $message attr-dict
+  }];
+}
+
+def AssumeOp : FIRRTLOp<"assume", []> {
+  let summary = "Assume Verification Statement";
+
+  let arguments = (ins ClockType:$clock, UInt1Type:$predicate, UInt1Type:$enable,
+    StrAttr:$message);
+  let results = (outs);
+
+  let assemblyFormat = [{
+    $clock `,` $predicate `,` $enable `,` $message attr-dict
+  }];
+}
+
+def CoverOp : FIRRTLOp<"cover", []> {
+  let summary = "Cover Verification Statement";
+
+  let arguments = (ins ClockType:$clock, UInt1Type:$predicate, UInt1Type:$enable,
+    StrAttr:$message);
+  let results = (outs);
+
+  let assemblyFormat = [{
+    $clock `,` $predicate `,` $enable `,` $message attr-dict
+  }];
+}
+
 def WhenOp : FIRRTLOp<"when", [SingleBlockImplicitTerminator<"DoneOp">]> {
   let summary = "When Statement";
   let description = [{

diff --git a/lib/FIRParser/FIRParser.cpp b/lib/FIRParser/FIRParser.cpp
@@ -771,6 +771,9 @@ struct FIRStmtParser : public FIRScopedParser {
   ParseResult parsePrintf();
   ParseResult parseSkip();
   ParseResult parseStop();
+  ParseResult parseAssert();
+  ParseResult parseAssume();
+  ParseResult parseCover();
   ParseResult parseWhen(unsigned whenIndent);
   ParseResult parseLeadingExpStmt(Value lhs, SubOpVector &subOps);
 
@@ -1264,6 +1267,12 @@ ParseResult FIRStmtParser::parseSimpleStmt(unsigned stmtIndent) {
     return parseSkip();
   case FIRToken::lp_stop:
     return parseStop();
+  case FIRToken::lp_assert:
+    return parseAssert();
+  case FIRToken::lp_assume:
+    return parseAssume();
+  case FIRToken::lp_cover:
+    return parseCover();
   case FIRToken::kw_when:
     return parseWhen(stmtIndent);
   default: {
@@ -1489,6 +1498,78 @@ ParseResult FIRStmtParser::parseStop() {
   return success();
 }
 
+/// assert ::= 'assert(' exp exp exp StringLit ')' info?
+ParseResult FIRStmtParser::parseAssert() {
+  LocWithInfo info(getToken().getLoc(), this);
+  consumeToken(FIRToken::lp_assert);
+
+  SmallVector<Operation *, 8> subOps;
+
+  Value clock, predicate, enable;
+  StringRef message;
+  if (parseExp(clock, subOps, "expected clock expression in 'assert'") ||
+      parseExp(predicate, subOps, "expected predicate in 'assert'") ||
+      parseExp(enable, subOps, "expected enable in 'assert'") ||
+      parseGetSpelling(message) ||
+      parseToken(FIRToken::string, "expected message in 'assert'") ||
+      parseToken(FIRToken::r_paren, "expected ')' in 'assert'") ||
+      parseOptionalInfo(info, subOps))
+    return failure();
+
+  auto messageUnescaped = FIRToken::getStringValue(message);
+  builder.create<AssertOp>(info.getLoc(), clock, predicate, enable,
+                           builder.getStringAttr(messageUnescaped));
+  return success();
+}
+
+/// assume ::= 'assume(' exp exp exp StringLit ')' info?
+ParseResult FIRStmtParser::parseAssume() {
+  LocWithInfo info(getToken().getLoc(), this);
+  consumeToken(FIRToken::lp_assume);
+
+  SmallVector<Operation *, 8> subOps;
+
+  Value clock, predicate, enable;
+  StringRef message;
+  if (parseExp(clock, subOps, "expected clock expression in 'assume'") ||
+      parseExp(predicate, subOps, "expected predicate in 'assume'") ||
+      parseExp(enable, subOps, "expected enable in 'assume'") ||
+      parseGetSpelling(message) ||
+      parseToken(FIRToken::string, "expected message in 'assume'") ||
+      parseToken(FIRToken::r_paren, "expected ')' in 'assume'") ||
+      parseOptionalInfo(info, subOps))
+    return failure();
+
+  auto messageUnescaped = FIRToken::getStringValue(message);
+  builder.create<AssumeOp>(info.getLoc(), clock, predicate, enable,
+                           builder.getStringAttr(messageUnescaped));
+  return success();
+}
+
+/// cover ::= 'cover(' exp exp exp StringLit ')' info?
+ParseResult FIRStmtParser::parseCover() {
+  LocWithInfo info(getToken().getLoc(), this);
+  consumeToken(FIRToken::lp_cover);
+
+  SmallVector<Operation *, 8> subOps;
+
+  Value clock, predicate, enable;
+  StringRef message;
+  if (parseExp(clock, subOps, "expected clock expression in 'cover'") ||
+      parseExp(predicate, subOps, "expected predicate in 'cover'") ||
+      parseExp(enable, subOps, "expected enable in 'cover'") ||
+      parseGetSpelling(message) ||
+      parseToken(FIRToken::string, "expected message in 'cover'") ||
+      parseToken(FIRToken::r_paren, "expected ')' in 'cover'") ||
+      parseOptionalInfo(info, subOps))
+    return failure();
+
+  auto messageUnescaped = FIRToken::getStringValue(message);
+  builder.create<CoverOp>(info.getLoc(), clock, predicate, enable,
+                          builder.getStringAttr(messageUnescaped));
+  return success();
+}
+
 /// when  ::= 'when' exp ':' info? suite? ('else' ( when | ':' info? suite?)
 /// )? suite ::= simple_stmt | INDENT simple_stmt+ DEDENT
 ParseResult FIRStmtParser::parseWhen(unsigned whenIndent) {

diff --git a/lib/FIRParser/FIRTokenKinds.def b/lib/FIRParser/FIRTokenKinds.def
@@ -114,6 +114,9 @@ TOK_KEYWORD(write)
 // FIRToken::lp_foo enums.
 TOK_LPKEYWORD(printf)
 TOK_LPKEYWORD(stop)
+TOK_LPKEYWORD(assert)
+TOK_LPKEYWORD(assume)
+TOK_LPKEYWORD(cover)
 
 // These are for LPKEYWORD cases that correspond to a primitive operation.
 TOK_LPKEYWORD_PRIM(add, AddPrimOp)

diff --git a/test/FIRParser/basic.fir b/test/FIRParser/basic.fir
@@ -285,6 +285,17 @@ circuit MyModule :     ; CHECK: firrtl.circuit "MyModule" {
     ; CHECK: firrtl.attach(%a8, %a8, %a8) :
     attach (a8, a8, a8)
 
+    wire pred: UInt <1>
+    wire en: UInt <1>
+    pred <= eq(i8, i8)
+    en <= not(reset)
+    ; CHECK: firrtl.assert %clock, %pred, %en, "X equals Y when Z is valid"
+    assert(clock, pred, en, "X equals Y when Z is valid")
+    ; CHECK: firrtl.assume %clock, %pred, %en, "X equals Y when Z is valid"
+    assume(clock, pred, en, "X equals Y when Z is valid")
+    ; CHECK: firrtl.cover %clock, %pred, %en, "X equals Y when Z is valid"
+    cover(clock, pred, en, "X equals Y when Z is valid")
+
   ; CHECK-LABEL: firrtl.module @type_handling(
   module type_handling :
     wire _t_6 : { flip b : { bits : { source : UInt<7> } } }