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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
;Copyright (c) 2014 - 2016 The Regents of the University of
;California (Regents). All Rights Reserved. Redistribution and use in
;source and binary forms, with or without modification, are permitted
;provided that the following conditions are met:
; * Redistributions of source code must retain the above
; copyright notice, this list of conditions and the following
; two paragraphs of disclaimer.
; * Redistributions in binary form must reproduce the above
; copyright notice, this list of conditions and the following
; two paragraphs of disclaimer in the documentation and/or other materials
; provided with the distribution.
; * Neither the name of the Regents nor the names of its contributors
; may be used to endorse or promote products derived from this
; software without specific prior written permission.
;IN NO EVENT SHALL REGENTS BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT,
;SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, INCLUDING LOST PROFITS,
;ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF
;REGENTS HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
;REGENTS SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT
;LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
;A PARTICULAR PURPOSE. THE SOFTWARE AND ACCOMPANYING DOCUMENTATION, IF
;ANY, PROVIDED HEREUNDER IS PROVIDED "AS IS". REGENTS HAS NO OBLIGATION
;TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
;MODIFICATIONS.
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
|
