diff --git a/src/main/scala/firrtl/LoweringCompilers.scala b/src/main/scala/firrtl/LoweringCompilers.scala index f9475c7..04df711 100644 --- a/src/main/scala/firrtl/LoweringCompilers.scala +++ b/src/main/scala/firrtl/LoweringCompilers.scala @@ -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, diff --git a/src/main/scala/firrtl/passes/labelchecking/ConstraintGen.scala b/src/main/scala/firrtl/passes/labelchecking/ConstraintGen.scala index cad4d4a..0f00c0c 100644 --- a/src/main/scala/firrtl/passes/labelchecking/ConstraintGen.scala +++ b/src/main/scala/firrtl/passes/labelchecking/ConstraintGen.scala @@ -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 => diff --git a/src/main/scala/firrtl/passes/labelchecking/DepExprPasses.scala b/src/main/scala/firrtl/passes/labelchecking/DepExprPasses.scala index c520d7f..3017e0f 100644 --- a/src/main/scala/firrtl/passes/labelchecking/DepExprPasses.scala +++ b/src/main/scala/firrtl/passes/labelchecking/DepExprPasses.scala @@ -22,7 +22,7 @@ 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) @@ -30,10 +30,7 @@ object DepsToWorkingIR extends Pass with PassDebug { 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 } diff --git a/src/main/scala/firrtl/passes/labelchecking/LabelCheck.scala b/src/main/scala/firrtl/passes/labelchecking/LabelCheck.scala index c3a296d..fb79d9f 100644 --- a/src/main/scala/firrtl/passes/labelchecking/LabelCheck.scala +++ b/src/main/scala/firrtl/passes/labelchecking/LabelCheck.scala @@ -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")