mirror of https://github.com/llvm/circt.git
[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>
This commit is contained in:
parent
64dd773e18
commit
046eebb479
|
@ -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 = [{
|
||||
|
|
|
@ -771,6 +771,9 @@ private:
|
|||
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) {
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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> } } }
|
||||
|
|
Loading…
Reference in New Issue