[/] [trunk/] [src/] [maketest/] [clkexprtrans.sml] -
Diff 62 ⟶ 72
Diff between revs
62
and
72
| Rev 62 |
Rev 72 |
|---|
| Line 1... |
Line 1... |
(* $Id: clkexprtrans.sml 62 2008-08-20 11:20:33Z tbourke $
|
(* $Id: clkexprtrans.sml 72 2009-03-14 11:44:10Z tbourke $
|
*
|
*
|
* Copyright (c) 2008 Timothy Bourke (University of NSW and NICTA)
|
* Copyright (c) 2008 Timothy Bourke (University of NSW and NICTA)
|
* All rights reserved.
|
* All rights reserved.
|
*
|
*
|
* This program is free software; you can redistribute it and/or modify it
|
* This program is free software; you can redistribute it and/or modify it
|
| Line 205... |
Line 205... |
(SOME true, SOME true) => (ClkE.trueExpr, false)
|
(SOME true, SOME true) => (ClkE.trueExpr, false)
|
| (SOME true, _) => (cinv, false)
|
| (SOME true, _) => (cinv, false)
|
| (_, SOME true) => (g', false)
|
| (_, SOME true) => (g', false)
|
| (NONE, NONE) => (ClkE.And (cinv,g'),false)
|
| (NONE, NONE) => (ClkE.And (cinv,g'),false)
|
| _ => (ClkE.falseExpr, true)
|
| _ => (ClkE.falseExpr, true)
|
val dnf = ClkE.toDNF e
|
val dnf = ClkE.clusterNonClocks (ClkE.toDNF e)
|
|
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
toString cet])
|
toString cet])
|
|
|
(* Check the assumption of disjointness: *)
|
(* Check the assumption of disjointness: *)
|
(* Check the assumption of disjointness: *)
|
(* Check the assumption of disjointness: *)
|