1--  PSL - Nodes definition
2--  Copyright (C) 2002-2016 Tristan Gingold
3--
4--  This program is free software: you can redistribute it and/or modify
5--  it under the terms of the GNU General Public License as published by
6--  the Free Software Foundation, either version 2 of the License, or
7--  (at your option) any later version.
8--
9--  This program is distributed in the hope that it will be useful,
10--  but WITHOUT ANY WARRANTY; without even the implied warranty of
11--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12--  GNU General Public License for more details.
13--
14--  You should have received a copy of the GNU General Public License
15--  along with this program.  If not, see <gnu.org/licenses>.
16
17with Types; use Types;
18with PSL.Types; use PSL.Types;
19
20package PSL.Nodes is
21   type Nkind is
22     (
23      N_Error,
24
25      N_Vmode,
26      N_Vunit,
27      N_Vprop,
28
29      N_Hdl_Mod_Name,
30
31      N_Assert_Directive,
32      N_Property_Declaration,
33      N_Sequence_Declaration,
34      N_Endpoint_Declaration,
35
36      --  Formal parameters
37      N_Const_Parameter,
38      N_Boolean_Parameter,
39      N_Property_Parameter,
40      N_Sequence_Parameter,
41
42      N_Sequence_Instance,
43      N_Endpoint_Instance,
44      N_Property_Instance,
45      N_Actual,
46
47      N_Clock_Event,
48
49      --  Properties
50      N_Always,
51      N_Never,
52      N_Eventually,
53      N_Strong,          --  !
54      N_Imp_Seq,         --  |=>
55      N_Overlap_Imp_Seq, --  |->
56      N_Log_Imp_Prop,    --  ->
57      N_Log_Equiv_Prop,  --  <->
58      N_Next,
59      N_Next_A,
60      N_Next_E,
61      N_Next_Event,
62      N_Next_Event_A,
63      N_Next_Event_E,
64      N_Abort,
65      N_Until,
66      N_Before,
67      N_Or_Prop,
68      N_And_Prop,
69      N_Paren_Prop,
70
71      --  Sequences/SERE.
72      N_Braced_SERE,
73      N_Concat_SERE,
74      N_Fusion_SERE,
75      N_Within_SERE,
76      N_Clocked_SERE,
77
78      N_Match_And_Seq,  --  &&
79      N_And_Seq,
80      N_Or_Seq,
81
82      N_Star_Repeat_Seq,
83      N_Goto_Repeat_Seq,
84      N_Plus_Repeat_Seq, -- [+]
85      N_Equal_Repeat_Seq,
86
87      --  Boolean layer.
88      N_Paren_Bool,
89      N_Not_Bool,
90      N_And_Bool,
91      N_Or_Bool,
92      N_Imp_Bool,       -- ->
93      N_Equiv_Bool,     -- <->
94      N_HDL_Expr,
95      N_HDL_Bool,
96      N_False,
97      N_True,
98      N_EOS,
99
100      N_Name,
101      N_Name_Decl,
102      N_Number
103     );
104   for Nkind'Size use 8;
105
106   subtype N_Booleans is Nkind range N_Paren_Bool .. N_True;
107   subtype N_Sequences is Nkind range N_Braced_SERE .. N_Equal_Repeat_Seq;
108
109   subtype N_HDLs is Nkind range N_HDL_Expr .. N_HDL_Bool;
110
111   type PSL_Types is
112     (
113      Type_Unknown,
114      Type_Boolean,
115      Type_Bit,
116      Type_Bitvector,
117      Type_Numeric,
118      Type_String,
119      Type_Sequence,
120      Type_Property
121     );
122
123   --  Within CSE, it is useful to know which sub-expression already compose
124   --  an expression.
125   --  Eg: suppose we want to build A and B.
126   --  Each sub-expressions of B is marked either as Present_Pos or
127   --  Present_Neg.
128   --  If A is already present, return either B or FALSE.
129   --  Otherwise, build the node.
130   type PSL_Presence_Kind is
131     (
132      Present_Unknown,
133      Present_Pos,
134      Present_Neg
135     );
136
137   --  The next line marks the start of the node description.
138   -- Start of Nkind.
139
140   -- N_Error (Short)
141
142   -- N_Vmode (Short)
143   -- N_Vunit (Short)
144   -- N_Vprop (Short)
145   --
146   --   Get/Set_Identifier (Field1)
147   --
148   --   Get/Set_Chain (Field2)
149   --
150   --   Get/Set_Instance (Field3)
151   --
152   --   Get/Set_Item_Chain (Field4)
153
154   -- N_Hdl_Mod_Name (Short)
155   --
156   --   Get/Set_Identifier (Field1)
157   --
158   --   Get/Set_Prefix (Field2)
159
160   -- N_Assert_Directive (Short)
161   --
162   --   Get/Set_Label (Field1)
163   --
164   --   Get/Set_Chain (Field2)
165   --
166   --   Get/Set_String (Field3)
167   --
168   --   Get/Set_Property (Field4)
169   --
170   --   Get/Set_NFA (Field5)
171
172   -- N_Property_Declaration (Short)
173   --
174   --   Get/Set_Identifier (Field1)
175   --
176   --   Get/Set_Chain (Field2)
177   --
178   --   Get/Set_Global_Clock (Field3)
179   --
180   --   Get/Set_Property (Field4)
181   --
182   --   Get/Set_Parameter_List (Field5)
183
184   -- N_Sequence_Declaration (Short)
185   -- N_Endpoint_Declaration (Short)
186   --
187   --   Get/Set_Identifier (Field1)
188   --
189   --   Get/Set_Chain (Field2)
190   --
191   --   Get/Set_Sequence (Field3)
192   --
193   --   Get/Set_Parameter_List (Field5)
194
195   -- N_Const_Parameter (Short)
196   -- N_Boolean_Parameter (Short)
197   -- N_Property_Parameter (Short)
198   -- N_Sequence_Parameter (Short)
199   --
200   --   Get/Set_Identifier (Field1)
201   --
202   --   Get/Set_Chain (Field2)
203   --
204   --  --  Current actual parameter.
205   --   Get/Set_Actual (Field3)
206
207   -- N_Sequence_Instance (Short)
208   -- N_Endpoint_Instance (Short)
209   -- N_Property_Instance (Short)
210   --
211   --   Get/Set_Declaration (Field1)
212   --
213   --   Get/Set_Association_Chain (Field2)
214
215   -- N_Actual (Short)
216   --
217   --   Get/Set_Chain (Field2)
218   --
219   --   Get/Set_Actual (Field3)
220   --
221   --   Get/Set_Formal (Field4)
222
223   -- N_Clock_Event (Short)
224   --
225   --   Get/Set_Property (Field4)
226   --
227   --   Get/Set_Boolean (Field3)
228
229   -- N_Always (Short)
230   -- N_Never (Short)
231   -- N_Eventually (Short)
232   -- N_Strong (Short)
233   --
234   --   Get/Set_Property (Field4)
235
236   -- N_Next (Short)
237   --
238   --   Get/Set_Strong_Flag (Flag1)
239   --
240   --   Get/Set_Number (Field1)
241   --
242   --   Get/Set_Property (Field4)
243
244   -- N_Name (Short)
245   --
246   --   Get/Set_Identifier (Field1)
247   --
248   --   Get/Set_Decl (Field2)
249
250   -- N_Name_Decl (Short)
251   --
252   --   Get/Set_Identifier (Field1)
253   --
254   --   Get/Set_Chain (Field2)
255
256   -- N_Number (Short)
257   --
258   --   Get/Set_Value (Field1)
259
260   -- N_Braced_SERE (Short)
261   --
262   --   Get/Set_SERE (Field1)
263
264   -- N_Clocked_SERE (Short)
265   --
266   --   Get/Set_SERE (Field1)
267   --
268   --   Get/Set_Boolean (Field3)
269
270   -- N_Concat_SERE (Short)
271   -- N_Fusion_SERE (Short)
272   -- N_Within_SERE (Short)
273   --
274   --   Get/Set_Left (Field1)
275   --
276   --   Get/Set_Right (Field2)
277
278   -- N_Star_Repeat_Seq (Short)
279   -- N_Goto_Repeat_Seq (Short)
280   -- N_Equal_Repeat_Seq (Short)
281   --
282   --  Note: can be null_node for star_repeat_seq.
283   --   Get/Set_Sequence (Field3)
284   --
285   --   Get/Set_Low_Bound (Field1)
286   --
287   --   Get/Set_High_Bound (Field2)
288
289   -- N_Plus_Repeat_Seq (Short)
290   --
291   --  Note: can be null_node.
292   --   Get/Set_Sequence (Field3)
293
294   -- N_Match_And_Seq (Short)
295   -- N_And_Seq (Short)
296   -- N_Or_Seq (Short)
297   --
298   --   Get/Set_Left (Field1)
299   --
300   --   Get/Set_Right (Field2)
301
302   -- N_Imp_Seq (Short)
303   -- N_Overlap_Imp_Seq (Short)
304   --
305   --   Get/Set_Sequence (Field3)
306   --
307   --   Get/Set_Property (Field4)
308
309   -- N_Log_Imp_Prop (Short)
310   -- N_Log_Equiv_Prop (Short)
311   --
312   --   Get/Set_Left (Field1)
313   --
314   --   Get/Set_Right (Field2)
315
316   -- N_Next_A (Short)
317   -- N_Next_E (Short)
318   --
319   --   Get/Set_Strong_Flag (Flag1)
320   --
321   --   Get/Set_Low_Bound (Field1)
322   --
323   --   Get/Set_High_Bound (Field2)
324   --
325   --   Get/Set_Property (Field4)
326
327   -- N_Next_Event (Short)
328   --
329   --   Get/Set_Strong_Flag (Flag1)
330   --
331   --   Get/Set_Number (Field1)
332   --
333   --   Get/Set_Property (Field4)
334   --
335   --   Get/Set_Boolean (Field3)
336
337   -- N_Or_Prop (Short)
338   -- N_And_Prop (Short)
339   --
340   --   Get/Set_Left (Field1)
341   --
342   --   Get/Set_Right (Field2)
343
344   -- N_Paren_Prop (Short)
345   --
346   --   Get/Set_Property (Field4)
347
348   -- N_Until (Short)
349   -- N_Before (Short)
350   --
351   --   Get/Set_Strong_Flag (Flag1)
352   --
353   --   Get/Set_Inclusive_Flag (Flag2)
354   --
355   --   Get/Set_Left (Field1)
356   --
357   --   Get/Set_Right (Field2)
358
359   -- N_Next_Event_A (Short)
360   -- N_Next_Event_E (Short)
361   --
362   --   Get/Set_Strong_Flag (Flag1)
363   --
364   --   Get/Set_Low_Bound (Field1)
365   --
366   --   Get/Set_High_Bound (Field2)
367   --
368   --   Get/Set_Property (Field4)
369   --
370   --   Get/Set_Boolean (Field3)
371
372   -- N_Abort (Short)
373   --
374   --   Get/Set_Property (Field4)
375   --
376   --   Get/Set_Boolean (Field3)
377
378
379   -- N_HDL_Bool (Short)
380   --  An HDL expression of boolean type, that could be hashed.
381   --
382   --   Get/Set_Presence (State1)
383   --
384   --   Get/Set_HDL_Node (Field1)
385   --
386   --   Get/Set_HDL_Index (Field2)
387   --
388   --   Get/Set_Hash (Field5)
389   --
390   --   Get/Set_Hash_Link (Field6)
391
392   -- N_HDL_Expr (Short)
393   --  An HDL expression.  Just a proxy to the N_HDL_Bool.  The node
394   --  is removed when rewritten.  This node is present so that denoting
395   --  names are kept in the PSL tree.
396   --
397   --   Get/Set_HDL_Node (Field1)
398   --
399   --   Get/Set_HDL_Hash (Field5)
400
401   -- N_Paren_Bool (Short)
402   --
403   --   Get/Set_Presence (State1)
404   --
405   --   Get/Set_Boolean (Field3)
406   --
407   --   Get/Set_Hash (Field5)
408   --
409   --   Get/Set_Hash_Link (Field6)
410
411   -- N_Not_Bool (Short)
412   --
413   --   Get/Set_Presence (State1)
414   --
415   --   Get/Set_Boolean (Field3)
416   --
417   --   Get/Set_Hash (Field5)
418   --
419   --   Get/Set_Hash_Link (Field6)
420
421   -- N_And_Bool (Short)
422   -- N_Or_Bool (Short)
423   -- N_Imp_Bool (Short)
424   -- N_Equiv_Bool (Short)
425   --
426   --   Get/Set_Presence (State1)
427   --
428   --   Get/Set_Left (Field1)
429   --
430   --   Get/Set_Right (Field2)
431   --
432   --   Get/Set_Hash (Field5)
433   --
434   --   Get/Set_Hash_Link (Field6)
435
436   -- N_True (Short)
437   -- N_False (Short)
438
439   -- N_EOS (Short)
440   --  End of simulation.
441   --
442   --   Get/Set_HDL_Index (Field2)
443   --
444   --   Get/Set_Hash (Field5)
445   --
446   --   Get/Set_Hash_Link (Field6)
447
448   -- End of Nkind.
449
450   subtype Node is Types.PSL_Node;
451
452   Null_Node  : constant Node := 0;
453   False_Node : constant Node := 1;
454   True_Node  : constant Node := 2;
455   One_Node   : constant Node := 3;
456   EOS_Node   : constant Node := 4;
457
458   subtype NFA is Types.PSL_NFA;
459
460   subtype HDL_Node is Int32;
461   HDL_Null : constant HDL_Node := 0;
462
463   -- General methods.
464
465   procedure Init (Loc : Location_Type);
466
467   --  Get the number of the last node.
468   --  To be used to size lateral tables.
469   function Get_Last_Node return Node;
470
471   -- subtype Regs_Type_Node is Node range Reg_Type_Node .. Time_Type_Node;
472
473   function Create_Node (Kind : Nkind) return Node;
474   procedure Free_Node (N : Node);
475
476   --  Return the type of a node.
477   function Get_Psl_Type (N : Node) return PSL_Types;
478
479   --  Note: use field Location
480   function Get_Location (N : Node) return Location_Type;
481   procedure Set_Location (N : Node; Loc : Location_Type);
482   procedure Copy_Location (N : Node; Src : Node);
483
484   function Get_Kind (N : Node) return Nkind;
485   pragma Inline (Get_Kind);
486
487--   --  Disp: None
488--   --  Field: Field6
489--   function Get_Parent (N : Node) return Node;
490--   procedure Set_Parent (N : Node; Parent : Node);
491
492   --  Disp: Special
493   --  Field: Field1 (pos)
494   function Get_Identifier (N : Node) return Name_Id;
495   procedure Set_Identifier (N : Node; Id : Name_Id);
496
497   --  Disp: Special
498   --  Field: Field1 (pos)
499   function Get_Label (N : Node) return Name_Id;
500   procedure Set_Label (N : Node; Id : Name_Id);
501
502   --  Disp: Chain
503   --  Field: Field2 Chain
504   function Get_Chain (N : Node) return Node;
505   procedure Set_Chain (N : Node; Chain : Node);
506
507   --  Field: Field3
508   function Get_Instance (N : Node) return Node;
509   procedure Set_Instance (N : Node; Instance : Node);
510
511   --  Field: Field2
512   function Get_Prefix (N : Node) return Node;
513   procedure Set_Prefix (N : Node; Prefix : Node);
514
515   --  Field: Field4
516   function Get_Item_Chain (N : Node) return Node;
517   procedure Set_Item_Chain (N : Node; Item : Node);
518
519   --  Field: Field4
520   function Get_Property (N : Node) return Node;
521   procedure Set_Property (N : Node; Property : Node);
522
523   --  Field: Field3
524   function Get_String (N : Node) return Node;
525   procedure Set_String (N : Node; Str : Node);
526
527   --  Field: Field1
528   function Get_SERE (N : Node) return Node;
529   procedure Set_SERE (N : Node; S : Node);
530
531   --  Field: Field1
532   function Get_Left (N : Node) return Node;
533   procedure Set_Left (N : Node; S : Node);
534
535   --  Field: Field2
536   function Get_Right (N : Node) return Node;
537   procedure Set_Right (N : Node; S : Node);
538
539   --  Field: Field3
540   function Get_Sequence (N : Node) return Node;
541   procedure Set_Sequence (N : Node; S : Node);
542
543   --  Field: Flag1
544   function Get_Strong_Flag (N : Node) return Boolean;
545   procedure Set_Strong_Flag (N : Node; B : Boolean);
546
547   --  Field: Flag2
548   function Get_Inclusive_Flag (N : Node) return Boolean;
549   procedure Set_Inclusive_Flag (N : Node; B : Boolean);
550
551   --  Field: Field1
552   function Get_Low_Bound (N : Node) return Node;
553   procedure Set_Low_Bound (N : Node; S : Node);
554
555   --  Field: Field2
556   function Get_High_Bound (N : Node) return Node;
557   procedure Set_High_Bound (N : Node; S : Node);
558
559   --  Field: Field1
560   function Get_Number (N : Node) return Node;
561   procedure Set_Number (N : Node; S : Node);
562
563   --  Field: Field1 (uc)
564   function Get_Value (N : Node) return Uns32;
565   procedure Set_Value (N : Node; Val : Uns32);
566
567   --  Field: Field3
568   function Get_Boolean (N : Node) return Node;
569   procedure Set_Boolean (N : Node; B : Node);
570
571   --  Field: Field2
572   function Get_Decl (N : Node) return Node;
573   procedure Set_Decl (N : Node; D : Node);
574
575   --  Field: Field1 (uc)
576   function Get_HDL_Node (N : Node) return HDL_Node;
577   procedure Set_HDL_Node (N : Node; H : HDL_Node);
578
579   --  Field: Field5 (uc)
580   function Get_Hash (N : Node) return Uns32;
581   procedure Set_Hash (N : Node; E : Uns32);
582   pragma Inline (Get_Hash);
583
584   --  Field: Field6
585   function Get_Hash_Link (N : Node) return Node;
586   procedure Set_Hash_Link (N : Node; E : Node);
587   pragma Inline (Get_Hash_Link);
588
589   --  Field: Field2 (uc)
590   function Get_HDL_Index (N : Node) return Int32;
591   procedure Set_HDL_Index (N : Node; Idx : Int32);
592
593   --  Link the the hash-able node.
594   --  Field: Field5
595   function Get_HDL_Hash (N : Node) return Node;
596   procedure Set_HDL_Hash (N : Node; H : Node);
597
598   --  Field: State1 (pos)
599   function Get_Presence (N : Node) return PSL_Presence_Kind;
600   procedure Set_Presence (N : Node; P : PSL_Presence_Kind);
601
602   --  Field: Field5 (uc)
603   function Get_NFA (N : Node) return NFA;
604   procedure Set_NFA (N : Node; P : NFA);
605
606   --  Field: Field5
607   function Get_Parameter_List (N : Node) return Node;
608   procedure Set_Parameter_List (N : Node; E : Node);
609
610   --  Field: Field3
611   function Get_Actual (N : Node) return Node;
612   procedure Set_Actual (N : Node; E : Node);
613
614   --  Field: Field4
615   function Get_Formal (N : Node) return Node;
616   procedure Set_Formal (N : Node; E : Node);
617
618   --  Field: Field1 Ref
619   function Get_Declaration (N : Node) return Node;
620   procedure Set_Declaration (N : Node; Decl : Node);
621
622   --  Field: Field2
623   function Get_Association_Chain (N : Node) return Node;
624   procedure Set_Association_Chain (N : Node; Chain : Node);
625
626   --  Field: Field3
627   function Get_Global_Clock (N : Node) return Node;
628   procedure Set_Global_Clock (N : Node; Clock : Node);
629end PSL.Nodes;
630