Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

machine_concret1_Abs1.v @ 31

Last change on this file since 31 was 4, checked in by syed, 14 years ago
input files added
File size: 14.7 KB

Line
1	typedef enum{machine_concret1_Abs1_STATE_28,machine_concret1_Abs1_STATE_31,machine_concret1_Abs1_STATE_30,machine_concret1_Abs1_STATE_32,machine_concret1_Abs1_STATE_27,machine_concret1_Abs1_STATE_29,machine_concret1_Abs1_STATE_35,machine_concret1_Abs1_STATE_39,machine_concret1_Abs1_STATE_41,machine_concret1_Abs1_STATE_42,machine_concret1_Abs1_STATE_34,machine_concret1_Abs1_STATE_44,machine_concret1_Abs1_STATE_38,machine_concret1_Abs1_STATE_40,machine_concret1_Abs1_STATE_36,machine_concret1_Abs1_STATE_33,machine_concret1_Abs1_STATE_45,machine_concret1_Abs1_STATE_43,machine_concret1_Abs1_STATE_46,machine_concret1_Abs1_STATE_37} machine_concret1_Abs1_STATE;
2
3	module machine_concret1_Abs1(clk,i1,o1,o2,r_i1);
4
5	input clk;
6
7	input i1;
8
9
10
11	output r_i1;
12	output o1;
13	output o2;
14
15
16	reg r_i1;
17	reg o1;
18	reg o2;
19	machine_concret1_Abs1_STATE reg state;
20
21
22	wire nd_r_i1;
23	wire nd_o1;
24	wire nd_o2;
25	wire nd_aff0;
26	wire nd_aff1;
27
28
29	assign nd_r_i1 = $ND(0,1);
30	assign nd_o1 = $ND(0,1);
31	assign nd_o2 = $ND(0,1);
32	assign nd_aff0 = $ND(0,1);
33	assign nd_aff1 = $ND(0,1);
34
35	initial
36	begin
37
38	state = $ND(machine_concret1_Abs1_STATE_27,machine_concret1_Abs1_STATE_29,machine_concret1_Abs1_STATE_33,machine_concret1_Abs1_STATE_37);
39	if(state == machine_concret1_Abs1_STATE_27)
40	begin
41	r_i1 = 0;
42	o1 = 0;
43	o2 = 0;
44	end
45	else
46	begin
47	if(state == machine_concret1_Abs1_STATE_29)
48	begin
49	r_i1 = 0;
50	o1 = 0;
51	o2 = 0;
52	end
53	else
54	begin
55	if(state == machine_concret1_Abs1_STATE_33)
56	begin
57	r_i1 = 0;
58	o1 = 0;
59	o2 = 0;
60	end
61	else
62	begin
63	o1 = 0;
64	o2 = 0;
65	r_i1 = nd_r_i1;
66	end
67	end
68	end
69	end
70
71	always @(posedge clk)
72	begin
73
74	case(state)
75	machine_concret1_Abs1_STATE_28:
76	begin
77	state = machine_concret1_Abs1_STATE_28;
78	r_i1 = nd_r_i1;
79	o1 = nd_o1;
80	o2 = nd_o2;
81	end
82	machine_concret1_Abs1_STATE_31:
83	begin
84	state = machine_concret1_Abs1_STATE_31;
85	r_i1 = nd_r_i1;
86	o1 = nd_o1;
87	o2 = nd_o2;
88	end
89	machine_concret1_Abs1_STATE_30:
90	begin
91	state = machine_concret1_Abs1_STATE_31;
92	r_i1 = nd_r_i1;
93	o1 = nd_o1;
94	o2 = nd_o2;
95	end
96	machine_concret1_Abs1_STATE_32:
97	begin
98	if(nd_aff0 == 1)
99	begin
100	state = machine_concret1_Abs1_STATE_30;
101	o2 = 1;
102	r_i1 = nd_r_i1;
103	o1 = nd_o1;
104	end
105	else
106	begin
107	state = machine_concret1_Abs1_STATE_32;
108	r_i1 = nd_r_i1;
109	o1 = nd_o1;
110	o2 = nd_o2;
111	end
112	end
113	machine_concret1_Abs1_STATE_27:
114	begin
115	state = machine_concret1_Abs1_STATE_28;
116	r_i1 = nd_r_i1;
117	o1 = nd_o1;
118	o2 = nd_o2;
119	end
120	machine_concret1_Abs1_STATE_29:
121	begin
122	if(nd_aff0 == 1)
123	begin
124	state = machine_concret1_Abs1_STATE_30;
125	o2 = 1;
126	r_i1 = nd_r_i1;
127	o1 = nd_o1;
128	end
129	else
130	begin
131	state = machine_concret1_Abs1_STATE_32;
132	r_i1 = nd_r_i1;
133	o1 = nd_o1;
134	o2 = nd_o2;
135	end
136	end
137	machine_concret1_Abs1_STATE_35:
138	begin
139	state = machine_concret1_Abs1_STATE_35;
140	r_i1 = nd_r_i1;
141	o1 = nd_o1;
142	o2 = nd_o2;
143	end
144	machine_concret1_Abs1_STATE_39:
145	begin
146	state = machine_concret1_Abs1_STATE_39;
147	r_i1 = nd_r_i1;
148	o1 = nd_o1;
149	o2 = nd_o2;
150	end
151	machine_concret1_Abs1_STATE_41:
152	begin
153	state = machine_concret1_Abs1_STATE_39;
154	r_i1 = nd_r_i1;
155	o1 = nd_o1;
156	o2 = nd_o2;
157	end
158	machine_concret1_Abs1_STATE_42:
159	begin
160	if(nd_aff0 == 1)
161	begin
162	state = machine_concret1_Abs1_STATE_41;
163	o2 = 1;
164	r_i1 = nd_r_i1;
165	o1 = nd_o1;
166	end
167	else
168	begin
169	state = machine_concret1_Abs1_STATE_42;
170	r_i1 = nd_r_i1;
171	o1 = nd_o1;
172	o2 = nd_o2;
173	end
174	end
175	machine_concret1_Abs1_STATE_34:
176	begin
177	state = machine_concret1_Abs1_STATE_35;
178	r_i1 = nd_r_i1;
179	o1 = nd_o1;
180	o2 = nd_o2;
181	end
182	machine_concret1_Abs1_STATE_44:
183	begin
184	state = machine_concret1_Abs1_STATE_39;
185	r_i1 = nd_r_i1;
186	o1 = nd_o1;
187	o2 = nd_o2;
188	end
189	machine_concret1_Abs1_STATE_38:
190	begin
191	state = machine_concret1_Abs1_STATE_39;
192	r_i1 = nd_r_i1;
193	o1 = nd_o1;
194	o2 = nd_o2;
195	end
196	machine_concret1_Abs1_STATE_40:
197	begin
198	if(nd_aff0 == 1)
199	begin
200	state = machine_concret1_Abs1_STATE_41;
201	o2 = 1;
202	r_i1 = nd_r_i1;
203	o1 = nd_o1;
204	end
205	else
206	begin
207	state = machine_concret1_Abs1_STATE_42;
208	r_i1 = nd_r_i1;
209	o1 = nd_o1;
210	o2 = nd_o2;
211	end
212	end
213	machine_concret1_Abs1_STATE_36:
214	begin
215	if(nd_aff0 == 1)
216	begin
217	state = machine_concret1_Abs1_STATE_34;
218	o1 = 1;
219	r_i1 = nd_r_i1;
220	o2 = nd_o2;
221	end
222	else
223	begin
224	state = machine_concret1_Abs1_STATE_36;
225	r_i1 = nd_r_i1;
226	o1 = nd_o1;
227	o2 = nd_o2;
228	end
229	end
230	machine_concret1_Abs1_STATE_33:
231	begin
232	if(nd_aff0 == 1)
233	begin
234	state = machine_concret1_Abs1_STATE_34;
235	o1 = 1;
236	r_i1 = nd_r_i1;
237	o2 = nd_o2;
238	end
239	else
240	begin
241	state = machine_concret1_Abs1_STATE_36;
242	r_i1 = nd_r_i1;
243	o1 = nd_o1;
244	o2 = nd_o2;
245	end
246	end
247	machine_concret1_Abs1_STATE_45:
248	begin
249	if(nd_aff0 == 1)
250	begin
251	state = machine_concret1_Abs1_STATE_44;
252	o1 = 1;
253	r_i1 = nd_r_i1;
254	o2 = nd_o2;
255	end
256	else
257	begin
258	state = machine_concret1_Abs1_STATE_45;
259	r_i1 = nd_r_i1;
260	o1 = nd_o1;
261	o2 = nd_o2;
262	end
263	end
264	machine_concret1_Abs1_STATE_43:
265	begin
266	if(nd_aff0 == 1)
267	begin
268	state = machine_concret1_Abs1_STATE_44;
269	o1 = 1;
270	r_i1 = nd_r_i1;
271	o2 = nd_o2;
272	end
273	else
274	begin
275	state = machine_concret1_Abs1_STATE_45;
276	r_i1 = nd_r_i1;
277	o1 = nd_o1;
278	o2 = nd_o2;
279	end
280	end
281	machine_concret1_Abs1_STATE_46:
282	begin
283	if(nd_aff0 == 1)
284	begin
285	if(nd_aff1 == 1)
286	begin
287	state = machine_concret1_Abs1_STATE_38;
288	o1 = 1;
289	o2 = 1;
290	r_i1 = nd_r_i1;
291	end
292	else
293	begin
294	state = machine_concret1_Abs1_STATE_40;
295	o1 = 1;
296	r_i1 = nd_r_i1;
297	o2 = nd_o2;
298	end
299	end
300	else
301	begin
302	if(nd_aff1 == 1)
303	begin
304	state = machine_concret1_Abs1_STATE_43;
305	o2 = 1;
306	r_i1 = nd_r_i1;
307	o1 = nd_o1;
308	end
309	else
310	begin
311	state = machine_concret1_Abs1_STATE_46;
312	r_i1 = nd_r_i1;
313	o1 = nd_o1;
314	o2 = nd_o2;
315	end
316	end
317	end
318	machine_concret1_Abs1_STATE_37:
319	begin
320	if(nd_aff0 == 1)
321	begin
322	if(nd_aff1 == 1)
323	begin
324	state = machine_concret1_Abs1_STATE_38;
325	o1 = 1;
326	o2 = 1;
327	r_i1 = nd_r_i1;
328	end
329	else
330	begin
331	state = machine_concret1_Abs1_STATE_40;
332	o1 = 1;
333	r_i1 = nd_r_i1;
334	o2 = nd_o2;
335	end
336	end
337	else
338	begin
339	if(nd_aff1 == 1)
340	begin
341	state = machine_concret1_Abs1_STATE_43;
342	o2 = 1;
343	r_i1 = nd_r_i1;
344	o1 = nd_o1;
345	end
346	else
347	begin
348	state = machine_concret1_Abs1_STATE_46;
349	r_i1 = nd_r_i1;
350	o1 = nd_o1;
351	o2 = nd_o2;
352	end
353	end
354	end
355	endcase
356	end
357
358	endmodule

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: cegar_dev/cegar/abstract_model/machine_concret1_Abs1.v @ 31

Download in other formats: