From c10f59954ae174704997fd15ece67f51cb8c106a Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 25 May 2020 14:12:01 -0400 Subject: [PATCH] Minor cleanup of comments --- src/soc/fu/compunits/formal/proof_fu.py | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py index 0944fbaa..0644587b 100644 --- a/src/soc/fu/compunits/formal/proof_fu.py +++ b/src/soc/fu/compunits/formal/proof_fu.py @@ -45,17 +45,18 @@ class Driver(Elaboratable): with m.Else(): comb += Assume(rst == 0) - # Property One: Rd_rel should never be asserted before issue - # detect when issue has been raised and remember it with m.If(issue): sync += has_issued.eq(1) comb += Cover(has_issued) - # If issue has never been raised, then rd_rel should never be raised + + # Property One: Rd_rel should never be asserted before issue + + # If issue has never been raised, then rd_rel should never + # be raised with m.If(rd_rel != 0): comb += Assert(has_issued) - # Property Two: when rd_rel is asserted, it should stay # that way until a go_rd with m.If((Past(go_rd) == 0) & ~Past(go_die)): @@ -75,8 +76,6 @@ class Driver(Elaboratable): with m.If(Past(go_die)): comb += Assert(rd_rel == 0) - # Property - comb += Cover(Fell(rd_rel)) # Assume no instruction is issued until rd_rel is @@ -84,10 +83,6 @@ class Driver(Elaboratable): with m.If((rd_rel != 0) | (Past(rd_rel) != 0)): comb += Assume(issue == 0) - - - - return m -- 2.30.2