Skip to content

Commit

Permalink
Bugfix
Browse files Browse the repository at this point in the history
  • Loading branch information
aferr committed Mar 25, 2018
1 parent ef0f932 commit 00433d9
Show file tree
Hide file tree
Showing 4 changed files with 22 additions and 10 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/firrtl/LoweringCompilers.scala
Original file line number Diff line number Diff line change
Expand Up @@ -113,11 +113,11 @@ class LabelChecking extends CoreTransform {
def outputForm = HighForm
def passSeq = Seq(
passes.PropNodes,
passes.LabelMPorts,
// passes.LabelMPorts,
passes.LabelExprs,
passes.DepsToWorkingIR,
passes.DepsResolveKinds,
passes.DepsInferTypes,
passes.LabelExprs,
passes.DeterminePC,
passes.NextCycleTransform,
passes.SeqPortGenNext,
Expand Down
18 changes: 16 additions & 2 deletions src/main/scala/firrtl/passes/labelchecking/ConstraintGen.scala
Original file line number Diff line number Diff line change
Expand Up @@ -273,8 +273,22 @@ object BVConstraintGen extends ConstraintGenerator {
val idx = CBVLit(ex.value, toBInt(vec_size(ex.exp.tpe)))
CASelect(refToIdent(ex.exp), idx).serialize
case ex: WSubAccess =>
val idx = exprToCons(ex.index, toBInt(vec_size(ex.exp.tpe)))
CASelect(refToIdent(ex.exp), idx).serialize
// try {
// toBInt(vec_size(ex.exp.tpe))
// } catch {
// case (t: Throwable) =>
// println(s"sub_access causing excp: ${ex.serialize}")
// println(s"sub_access.exp causing excp: ${ex.exp.serialize}")
// t
// }
try {
val idx = exprToCons(ex.index, toBInt(vec_size(ex.exp.tpe)))
CASelect(refToIdent(ex.exp), idx).serialize
} catch {
case (t: Exception) =>
val idx = exprToCons(ex.index)
CASelect(refToIdent(ex.exp), idx).serialize
}
case WRef(name,_,_,_,_) => name
case WSubField(exp,name,_,_,_) => s"(field_$name ${refToIdent(exp)})"
case ex: Mux =>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,18 +22,15 @@ object DepsToWorkingIR extends Pass with PassDebug {
}
def toLblComp(lc: LabelComp): LabelComp = lc map toExp map toLblComp

def toExp(e: Expression): Expression = e map toExp match {
def toExp(e: Expression): Expression = e map toExp map toLbl match {
case ex: Reference => WRef(ex.name, ex.tpe, ex.lbl, NodeKind, UNKNOWNGENDER)
case ex: SubField => WSubField(ex.expr, ex.name, ex.tpe, ex.lbl, UNKNOWNGENDER)
case ex: SubIndex => WSubIndex(ex.expr, ex.value, ex.tpe, ex.lbl, UNKNOWNGENDER)
case ex: SubAccess => WSubAccess(ex.expr, ex.index, ex.tpe, ex.lbl, UNKNOWNGENDER)
case ex => ex // This might look like a case to use case _ => e, DO NOT!
}

def toExpL(e: Expression): Expression =
toExp(e) map toExpL map toLbl

def toStmt(s: Statement): Statement = s map toExpL map toLbl match {
def toStmt(s: Statement): Statement = s map toExp map toLbl match {
case sx: DefInstance => WDefInstance(sx.info, sx.name, sx.module, UnknownType, UnknownLabel)
case sx => sx map toStmt
}
Expand Down
3 changes: 2 additions & 1 deletion src/main/scala/firrtl/passes/labelchecking/LabelCheck.scala
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,8 @@ object LabelCheck extends Pass with PassDebug {
emit(s"(assert (not (leqc ${ser(C(rhs) join C(pc))} ${ser(C(lhs))}) ) )\n")
} catch {
case (t: Exception) =>
throw new Exception(s"${info}: ${t.getMessage}")
println(s"Exception at source line ${info}")
throw t
}
emit("(check-sat)\n")
emit("(pop)\n")
Expand Down

0 comments on commit 00433d9

Please sign in to comment.