1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
defpackage firrtl/symbolic-value :
import core
import verse
import firrtl/ir2
import firrtl/ir-utils
; ======= Symbolic Value Library ==========
public definterface SymbolicValue
public defstruct SVExp <: SymbolicValue :
exp : Expression
public defstruct SVMux <: SymbolicValue :
pred : Expression
conseq : SymbolicValue
alt : SymbolicValue
public defstruct SVNul <: SymbolicValue
defmethod print (o:OutputStream, sv:SymbolicValue) :
match(sv) :
(sv: SVExp) : print(o, exp(sv))
(sv: SVMux) : print-all(o, ["(" pred(sv) " ? " conseq(sv) " : " alt(sv) ")"])
(sv: SVNul) : print(o, "SVNUL")
defn map (f: Expression -> Expression, sv:SymbolicValue) -> SymbolicValue :
match(sv) :
(sv:SVMux) : SVMux(f(pred(sv)),conseq(sv),alt(sv))
(sv:SVExp) : SVExp(f(exp(sv)))
(sv:SVNul) : sv
defmulti map<?T> (f: SymbolicValue -> SymbolicValue, sv:?T&SymbolicValue) -> T
defmethod map (f: SymbolicValue -> SymbolicValue, sv:SymbolicValue) -> SymbolicValue :
match(sv) :
(sv: SVMux) : SVMux(pred(sv),f(conseq(sv)),f(alt(sv)))
(sv) : sv
defn do (f:SymbolicValue -> ?, s:SymbolicValue) -> False :
defn f* (sv:SymbolicValue) -> SymbolicValue :
f(sv)
sv
map(f*,s)
false
defn dor (f:SymbolicValue -> ?, e:SymbolicValue) -> False :
do(f,e)
defn f* (x:SymbolicValue) -> SymbolicValue :
dor(f,x)
x
map(f*,e)
false
defmethod equal? (a:SymbolicValue,b:SymbolicValue) -> True|False :
match(a,b) :
(a:SVNul,b:SVNul) : true
(a:SVExp,b:SVExp) : exp(a) == exp(b)
(a:SVMux,b:SVMux) : pred(a) == pred(b) and conseq(a) == conseq(b) and alt(a) == alt(b)
(a,b) : false
;TODO add invert to primop
defn optimize (sv:SymbolicValue) -> SymbolicValue :
match(map(optimize,sv)) :
(sv:SVMux) :
if conseq(sv) == alt(sv) : conseq(sv)
else :
match(conseq(sv),alt(sv)) :
(c:SVExp,a:SVExp) :
if exp(c) == one and exp(a) == zero : SVExp(pred(sv))
else if exp(c) == zero and exp(a) == one : SVExp(NOT(pred(sv)))
else if exp(c) == exp(a) : c
else : sv
(c,a) : sv
(sv) : sv
|
