source: vis_dev/vis-2.1/examples/exampleS/exampleS.v @ 12

Last change on this file since 12 was 11, checked in by cecile, 13 years ago

Add vis

File size: 3.7 KB
Line 
1typedef enum { R, G, U, D } m_state;
2typedef enum { I, B } r_state;
3
4module resource(clk);
5input clk;
6wire req, grant, use, release;
7
8/* INSTANTIATION 0:  assert req implies (req until grant) then (use until release)
9*/
10        a0 a0(clk, req, grant, use, release);
11
12
13// RESOURCE REQUESTOR
14
15assign req = (m_st == R);
16assign use = (m_st == U);
17assign release = (m_st == D);
18m_state reg m_st;
19m_state wire r_m_st;
20initial m_st = R;
21
22assign r_m_st = $ND(U,D);
23
24always @(posedge clk) begin
25    case (m_st)
26        R: if (grant) m_st = G;
27        G: m_st = U;
28        U: begin
29                m_st = r_m_st;
30        end
31        D: m_st = R;
32    endcase;
33end
34
35// RESOURCE GRANTER
36
37r_state reg r_st;
38r_state wire r_r_st;
39initial r_st = I;
40
41assign grant = (r_st == B);
42assign r_r_st = $ND(B,I);
43
44always @(posedge clk) begin
45    case (r_st)
46        I: begin
47            if (req) r_st = r_r_st; 
48            else r_st = I;
49        end
50        B: if (release) r_st = I;
51    endcase;
52end
53endmodule
54
55
56/* TESLA ver 0.2: Sequence Detection FSMS: */
57
58typedef enum { S, D, X, T } state;
59
60/* DEFINITION 0: assert req implies (req until grant) then (use until release)
61*/
62module a0(clk, req, grant, use, release);
63input clk, req, grant, use, release;
64wire clk, trigger, failure, e0, r0, s0, f0, e3, r3, s3, f3, req, grant, use, release;
65        assign e0 = 1;
66        assign r0 = s3 || f0;
67        assign trigger = s0;
68        a0_seq0 a0_seq0(clk, e0, r0, s0, f0, req);
69        assign e3 = trigger;
70        assign r3 = 0;
71        a0_seq3 a0_seq3(clk, e3, r3, s3, f3, req, grant, use, release);
72endmodule
73
74module a0_seq0(clk, e, r, s, f, req);
75input clk, e, r, req;
76output s, f;
77//AP
78        state reg st;
79        initial st = S;
80        assign s = (((st == S) && e && (req)));
81        assign f = (((st == S) && e && ! (req)) || (st == T));
82        always @(posedge clk) begin
83                case (st)
84                        S: begin
85                                if (e && (req)) st = S;
86                                else if (e && !(req)) st = T;
87                        end
88                        default: if (r) st = S;
89                endcase;
90        end
91endmodule
92
93module a0_seq3(clk, e, r, s, f, req, grant, use, release);
94input clk, e, r, req, grant, use, release;
95output s, f;
96// THEN
97wire e1, r1, s1, f1, e2, r2, s2, f2, req, grant, use, release;
98        a0_seq1 a0_seq1(clk, e1, r1, s1, f1, req, grant);
99        a0_seq2 a0_seq2(clk, e2, r2, s2, f2, use, release);
100        assign r1 = r;
101        assign r2 = r;
102        then then(clk, s1, r, e2);
103        assign s = s2;
104        assign f = f1 || f2;
105        assign e1 = e;
106endmodule
107
108module then(clk, e, r, s);
109input clk, e, r;
110output s;
111//THEN_DEF
112        state reg st;
113        initial st = S;
114        assign s = (st == D);
115        always @(posedge clk) begin
116                case (st)
117                        S: if (e) st = X;
118                        X: st = D;
119                        default: if (r) st = S;
120                endcase;
121        end
122endmodule
123
124module a0_seq1(clk, e, r, s, f, req, grant);
125input clk, e, r, req, grant;
126output s, f;
127//UNTIL
128        state reg st;
129        initial st = S;
130        assign s = (((st == S) && e && (grant)) || ((st == X) && (! r) && (grant)));
131        assign f = (((st == S) && e && ! (req) && !(grant)) || ((st == X) && !(req) && !(grant)) || (st == T));
132        always @(posedge clk) begin
133                case (st)
134                        S: begin
135                                if (e && (grant)) st = S;
136                                else if (e && (req)) st = X;
137                                else if(e && !(req) && !(grant)) st = T;
138                        end
139                        X: begin
140                                if (r || (grant)) st = S;
141                                else if (!(req) && !(grant)) st = T;
142                        end
143                        default: if (r) st = S;
144                endcase;
145        end
146endmodule
147
148module a0_seq2(clk, e, r, s, f, use, release);
149input clk, e, r, use, release;
150output s, f;
151//UNTIL
152        state reg st;
153        initial st = S;
154        assign s = (((st == S) && e && (release)) || ((st == X) && (! r) && (release)));
155        assign f = (((st == S) && e && ! (use) && !(release)) || ((st == X) && !(use) && !(release)) || (st == T));
156        always @(posedge clk) begin
157                case (st)
158                        S: begin
159                                if (e && (release)) st = S;
160                                else if (e && (use)) st = X;
161                                else if(e && !(use) && !(release)) st = T;
162                        end
163                        X: begin
164                                if (r || (release)) st = S;
165                                else if (!(use) && !(release)) st = T;
166                        end
167                        default: if (r) st = S;
168                endcase;
169        end
170endmodule
171
Note: See TracBrowser for help on using the repository browser.