aboutsummaryrefslogtreecommitdiffstats
path: root/tests/asicworld/code_hdl_models_uart.v
blob: 40205250a27ac56b65def998bb092ada8817442b (plain)
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
//-----------------------------------------------------
// Design Name : uart 
// File Name   : uart.v
// Function    : Simple UART
// Coder       : Deepak Kumar Tala
//-----------------------------------------------------
module uart (
reset          ,
txclk          ,
ld_tx_data     ,
tx_data        ,
tx_enable      ,
tx_out         ,
tx_empty       ,
rxclk          ,
uld_rx_data    ,
rx_data        ,
rx_enable      ,
rx_in          ,
rx_empty
);
// Port declarations
input        reset          ;
input        txclk          ;
input        ld_tx_data     ;
input  [7:0] tx_data        ;
input        tx_enable      ;
output       tx_out         ;
output       tx_empty       ;
input        rxclk          ;
input        uld_rx_data    ;
output [7:0] rx_data        ;
input        rx_enable      ;
input        rx_in          ;
output       rx_empty       ;

// Internal Variables 
reg [7:0]    tx_reg         ;
reg          tx_empty       ;
reg          tx_over_run    ;
reg [3:0]    tx_cnt         ;
reg          tx_out         ;
reg [7:0]    rx_reg         ;
reg [7:0]    rx_data        ;
reg [3:0]    rx_sample_cnt  ;
reg [3:0]    rx_cnt         ;  
reg          rx_frame_err   ;
reg          rx_over_run    ;
reg          rx_empty       ;
reg          rx_d1          ;
reg          rx_d2          ;
reg          rx_busy        ;

// UART RX Logic
always @ (posedge rxclk or posedge reset)
if (reset) begin
  rx_reg        <= 0; 
  rx_data       <= 0;
  rx_sample_cnt <= 0;
  rx_cnt        <= 0;
  rx_frame_err  <= 0;
  rx_over_run   <= 0;
  rx_empty      <= 1;
  rx_d1         <= 1;
  rx_d2         <= 1;
  rx_busy       <= 0;
end else begin
  // Synchronize the asynch signal
  rx_d1 <= rx_in;
  rx_d2 <= rx_d1;
  // Uload the rx data
  if (uld_rx_data) begin
    rx_data  <= rx_reg;
    rx_empty <= 1;
  end
  // Receive data only when rx is enabled
  if (rx_enable) begin
    // Check if just received start of frame
    if (!rx_busy && !rx_d2) begin
      rx_busy       <= 1;
      rx_sample_cnt <= 1;
      rx_cnt        <= 0;
    end
    // Start of frame detected, Proceed with rest of data
    if (rx_busy) begin
       rx_sample_cnt <= rx_sample_cnt + 1;
       // Logic to sample at middle of data
       if (rx_sample_cnt == 7) begin
          if ((rx_d2 == 1) && (rx_cnt == 0)) begin
            rx_busy <= 0;
          end else begin
            rx_cnt <= rx_cnt + 1; 
            // Start storing the rx data
            if (rx_cnt > 0 && rx_cnt < 9) begin
              rx_reg[rx_cnt - 1] <= rx_d2;
            end
            if (rx_cnt == 9) begin
               rx_busy <= 0;
               // Check if End of frame received correctly
               if (rx_d2 == 0) begin
                 rx_frame_err <= 1;
               end else begin
                 rx_empty     <= 0;
                 rx_frame_err <= 0;
                 // Check if last rx data was not unloaded,
                 rx_over_run  <= (rx_empty) ? 0 : 1;
               end
            end
          end
       end 
    end 
  end
  if (!rx_enable) begin
    rx_busy <= 0;
  end
end

// UART TX Logic
always @ (posedge txclk or posedge reset)
if (reset) begin
  tx_reg        <= 0;
  tx_empty      <= 1;
  tx_over_run   <= 0;
  tx_out        <= 1;
  tx_cnt        <= 0;
end else begin
   if (ld_tx_data) begin
      if (!tx_empty) begin
        tx_over_run <= 0;
      end else begin
        tx_reg   <= tx_data;
        tx_empty <= 0;
      end
   end
   if (tx_enable && !tx_empty) begin
     tx_cnt <= tx_cnt + 1;
     if (tx_cnt == 0) begin
       tx_out <= 0;
     end
     if (tx_cnt > 0 && tx_cnt < 9) begin
        tx_out <= tx_reg[tx_cnt -1];
     end
     if (tx_cnt == 9) begin
       tx_out <= 1;
       tx_cnt <= 0;
       tx_empty <= 1;
     end
   end
   if (!tx_enable) begin
     tx_cnt <= 0;
   end
end

endmodule
is Res, Tmp : Node; begin Res := Create_Node (N_Star_Repeat_Seq); Tmp := Create_Node (N_Number); Set_Value (Tmp, 0); Set_Low_Bound (Res, Tmp); return Res; end Build_Empty; -- Return N[*] function Build_Star (N : Node) return Node is Res : Node; begin Res := Create_Node (N_Star_Repeat_Seq); Set_Sequence (Res, N); return Res; end Build_Star; -- Return N[+] function Build_Plus (N : Node) return Node is Res : Node; begin Res := Create_Node (N_Plus_Repeat_Seq); Set_Sequence (Res, N); return Res; end Build_Plus; -- Return N! function Build_Strong (N : Node) return Node is Res : Node; begin Res := Create_Node (N_Strong); Set_Property (Res, N); return Res; end Build_Strong; -- Return T[*] function Build_True_Star return Node is begin return Build_Star (True_Node); end Build_True_Star; function Build_Binary (K : Nkind; L, R : Node) return Node is Res : Node; begin Res := Create_Node (K); Set_Left (Res, L); Set_Right (Res, R); return Res; end Build_Binary; function Build_Concat (L, R : Node) return Node is begin return Build_Binary (N_Concat_SERE, L, R); end Build_Concat; function Build_Repeat (N : Node; Cnt : Uns32) return Node is Res : Node; begin if Cnt = 0 then raise Internal_Error; end if; Res := N; for I in 2 .. Cnt loop Res := Build_Concat (Res, N); end loop; return Res; end Build_Repeat; function Build_Overlap_Imp_Seq (S : Node; P : Node) return Node is Res : Node; begin Res := Create_Node (N_Overlap_Imp_Seq); Set_Sequence (Res, S); Set_Property (Res, P); return Res; end Build_Overlap_Imp_Seq; function Rewrite_Boolean (N : Node) return Node is Res : Node; begin case Get_Kind (N) is when N_Name => Res := Get_Decl (N); pragma Assert (Res /= Null_Node); return Res; when N_Not_Bool => Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); return N; when N_And_Bool | N_Or_Bool | N_Imp_Bool | N_Equiv_Bool => Set_Left (N, Rewrite_Boolean (Get_Left (N))); Set_Right (N, Rewrite_Boolean (Get_Right (N))); return N; when N_HDL_Expr => return Get_HDL_Hash (N); when N_HDL_Bool => return N; when others => Error_Kind ("rewrite_boolean", N); end case; end Rewrite_Boolean; function Rewrite_Star_Repeat_Seq (Seq : Node; Lo, Hi : Uns32) return Node is Res : Node; begin pragma Assert (Lo <= Hi); if Lo = Hi then if Lo = 0 then -- r[*0] --> [*0] return Build_Empty; elsif Lo = 1 then -- r[*1] --> r return Seq; end if; -- r[*c+] --> r;r;r...;r (c times) return Build_Repeat (Seq, Lo); end if; -- r[*0:1] --> [*0] | r -- r[*0:2] --> [*0] | r;{[*0]|r} -- r[*0:n] --> [*0] | r;r[*0:n-1] -- r[*l:h] --> r[*l] ; r[*0:h-l] Res := Build_Binary (N_Or_Seq, Build_Empty, Seq); for I in Lo + 2 .. Hi loop Res := Build_Concat (Seq, Res); Res := Build_Binary (N_Or_Seq, Build_Empty, Res); end loop; if Lo > 0 then Res := Build_Concat (Build_Repeat (Seq, Lo), Res); end if; return Res; end Rewrite_Star_Repeat_Seq; function Rewrite_Star_Repeat_Seq (Seq : Node; Lo, Hi : Node) return Node is Cnt_Lo : Uns32; Cnt_Hi : Uns32; begin -- r[*] must have been handled. pragma Assert (Lo /= Null_Node); Cnt_Lo := Get_Value (Lo); if Hi = Null_Node then Cnt_Hi := Cnt_Lo; elsif Get_Kind (Hi) = N_Inf then -- r[*N to inf] --> r[*N] ; r[*] if Cnt_Lo = 0 then return Build_Star (Seq); else return Build_Concat (Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Lo), Build_Star (Seq)); end if; else Cnt_Hi := Get_Value (Hi); end if; return Rewrite_Star_Repeat_Seq (Seq, Cnt_Lo, Cnt_Hi); end Rewrite_Star_Repeat_Seq; function Rewrite_Star_Repeat_Seq (N : Node) return Node is Seq : constant Node := Get_Sequence (N); Lo : constant Node := Get_Low_Bound (N); begin if Lo = Null_Node then -- r[*] --> r[*] return N; else return Rewrite_Star_Repeat_Seq (Seq, Lo, Get_High_Bound (N)); end if; end Rewrite_Star_Repeat_Seq; function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Node) return Node is Res : Node; begin -- b[->] --> {(~b)[*];b} Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B); if Lo = Null_Node then return Res; end if; -- b[->l:h] --> {b[->]}[*l:h] return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); end Rewrite_Goto_Repeat_Seq; function Rewrite_Goto_Repeat_Seq (B : Node; Lo, Hi : Uns32) return Node is Res : Node; begin -- b[->] --> {(~b)[*];b} Res := Build_Concat (Build_Star (Build_Bool_Not (B)), B); -- b[->l:h] --> {b[->]}[*l:h] return Rewrite_Star_Repeat_Seq (Res, Lo, Hi); end Rewrite_Goto_Repeat_Seq; function Rewrite_Equal_Repeat_Seq (N : Node) return Node is B : constant Node := Get_Boolean (N); Lo : constant Node := Get_Low_Bound (N); Hi : constant Node := Get_High_Bound (N); begin -- b[=l:h] --> {b[->l:h]};(~b)[*] return Build_Concat (Rewrite_Goto_Repeat_Seq (B, Lo, Hi), Build_Star (Build_Bool_Not (B))); end Rewrite_Equal_Repeat_Seq; function Rewrite_Within (N : Node) return Node is Res : Node; begin Res := Build_Concat (Build_Concat (Build_True_Star, Get_Left (N)), Build_True_Star); return Build_Binary (N_Match_And_Seq, Res, Get_Right (N)); end Rewrite_Within; function Rewrite_And_Seq (L : Node; R : Node) return Node is begin return Build_Binary (N_Or_Seq, Build_Binary (N_Match_And_Seq, L, Build_Concat (R, Build_True_Star)), Build_Binary (N_Match_And_Seq, Build_Concat (L, Build_True_Star), R)); end Rewrite_And_Seq; pragma Unreferenced (Rewrite_And_Seq); procedure Rewrite_Instance (N : Node) is Assoc : Node := Get_Association_Chain (N); begin while Assoc /= Null_Node loop case Get_Kind (Get_Formal (Assoc)) is when N_Const_Parameter => null; when N_Boolean_Parameter => Set_Actual (Assoc, Rewrite_Boolean (Get_Actual (Assoc))); when N_Sequence_Parameter => Set_Actual (Assoc, Rewrite_SERE (Get_Actual (Assoc))); when N_Property_Parameter => Set_Actual (Assoc, Rewrite_Property (Get_Actual (Assoc))); when others => Error_Kind ("rewrite_instance", Get_Formal (Assoc)); end case; Assoc := Get_Chain (Assoc); end loop; end Rewrite_Instance; function Rewrite_SERE (N : Node) return Node is S : Node; begin case Get_Kind (N) is when N_Star_Repeat_Seq => S := Get_Sequence (N); if S = Null_Node then S := True_Node; else S := Rewrite_SERE (S); end if; Set_Sequence (N, S); return Rewrite_Star_Repeat_Seq (N); when N_Plus_Repeat_Seq => S := Get_Sequence (N); if S = Null_Node then S := True_Node; else S := Rewrite_SERE (S); end if; Set_Sequence (N, S); return N; when N_Goto_Repeat_Seq => return Rewrite_Goto_Repeat_Seq (Rewrite_SERE (Get_Boolean (N)), Get_Low_Bound (N), Get_High_Bound (N)); when N_Equal_Repeat_Seq => Set_Boolean (N, Rewrite_SERE (Get_Boolean (N))); return Rewrite_Equal_Repeat_Seq (N); when N_Braced_SERE => return Rewrite_SERE (Get_SERE (N)); when N_Clocked_SERE => Set_SERE (N, Rewrite_SERE (Get_SERE (N))); Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); return N; when N_Within_SERE => Set_Left (N, Rewrite_SERE (Get_Left (N))); Set_Right (N, Rewrite_SERE (Get_Right (N))); return Rewrite_Within (N); -- when N_And_Seq => -- return Rewrite_And_Seq (Rewrite_SERE (Get_Left (N)), -- Rewrite_SERE (Get_Right (N))); when N_Concat_SERE | N_Fusion_SERE | N_Match_And_Seq | N_And_Seq | N_Or_Seq => Set_Left (N, Rewrite_SERE (Get_Left (N))); Set_Right (N, Rewrite_SERE (Get_Right (N))); return N; when N_Booleans => return Rewrite_Boolean (N); when N_Name => return Get_Decl (N); when N_Sequence_Instance => Rewrite_Instance (N); return N; when N_Endpoint_Instance => return N; when N_Boolean_Parameter | N_Sequence_Parameter | N_Const_Parameter => return N; when others => Error_Kind ("rewrite_SERE", N); end case; end Rewrite_SERE; function Rewrite_Until (N : Node) return Node is Res : Node; B : Node; L : Node; S : Node; begin if Get_Inclusive_Flag (N) then -- B1 until_ B2 --> {B1[+]:B2} Res := Build_Binary (N_Fusion_SERE, Build_Plus (Rewrite_Boolean (Get_Left (N))), Rewrite_Boolean (Get_Right (N))); if Get_Strong_Flag (N) then Res := Build_Strong (Res); end if; else -- P until B --> {(!B)[+]} |-> P B := Rewrite_Boolean (Get_Right (N)); L := Build_Plus (Build_Bool_Not (B)); Res := Build_Overlap_Imp_Seq (L, Rewrite_Property (Get_Left (N))); if Get_Strong_Flag (N) then -- p until! b --> (p until b) && ({b[->]}!) S := Build_Strong (Rewrite_Goto_Repeat_Seq (B, Null_Node, Null_Node)); Res := Build_Binary (N_And_Prop, Res, S); end if; end if; return Res; end Rewrite_Until; function Rewrite_Next_Event_A (B : Node; Lo, Hi : Uns32; P : Node; Strong : Boolean) return Node is Res : Node; begin Res := Rewrite_Goto_Repeat_Seq (B, Lo, Hi); Res := Build_Overlap_Imp_Seq (Res, P); if Strong then Res := Build_Binary (N_And_Prop, Res, Build_Strong (Rewrite_Goto_Repeat_Seq (B, Lo, Lo))); end if; return Res; end Rewrite_Next_Event_A; function Rewrite_Next_Event (B : Node; N : Uns32; P : Node; Strong : Boolean) return Node is begin return Rewrite_Next_Event_A (B, N, N, P, Strong); end Rewrite_Next_Event; function Rewrite_Next_Event (B : Node; Num : Node; P : Node; Strong : Boolean) return Node is N : Uns32; begin if Num = Null_Node then N := 1; else N := Get_Value (Num); end if; return Rewrite_Next_Event (B, N, P, Strong); end Rewrite_Next_Event; function Rewrite_Next (Num : Node; P : Node; Strong : Boolean) return Node is N : Uns32; begin if Num = Null_Node then N := 1; else N := Get_Value (Num); end if; return Rewrite_Next_Event (True_Node, N + 1, P, Strong); end Rewrite_Next; function Rewrite_Next_A (Lo, Hi : Uns32; P : Node; Strong : Boolean) return Node is begin return Rewrite_Next_Event_A (True_Node, Lo + 1, Hi + 1, P, Strong); end Rewrite_Next_A; function Rewrite_Next_Event_E (B1 : Node; Lo, Hi : Uns32; B2 : Node; Strong : Boolean) return Node is Res : Node; begin Res := Build_Binary (N_Fusion_SERE, Rewrite_Goto_Repeat_Seq (B1, Lo, Hi), B2); if Strong then Res := Build_Strong (Res); end if; return Res; end Rewrite_Next_Event_E; function Rewrite_Next_E (Lo, Hi : Uns32; B : Node; Strong : Boolean) return Node is begin return Rewrite_Next_Event_E (True_Node, Lo + 1, Hi + 1, B, Strong); end Rewrite_Next_E; function Rewrite_Before (N : Node) return Node is Res : Node; R : Node; B1, B2 : Node; N_B2 : Node; begin B1 := Rewrite_Boolean (Get_Left (N)); B2 := Rewrite_Boolean (Get_Right (N)); N_B2 := Build_Bool_Not (B2); Res := Build_Star (Build_Bool_And (Build_Bool_Not (B1), N_B2)); if Get_Inclusive_Flag (N) then R := B2; else R := Build_Bool_And (B1, N_B2); end if; Res := Build_Concat (Res, R); if Get_Strong_Flag (N) then Res := Build_Strong (Res); end if; return Res; end Rewrite_Before; function Rewrite_Or (L, R : Node) return Node is B, P : Node; begin if Get_Kind (L) in N_Booleans then if Get_Kind (R) in N_Booleans then return Build_Bool_Or (L, R); else B := L; P := R; end if; elsif Get_Kind (R) in N_Booleans then B := R; P := L; else -- Not in the simple subset. raise Program_Error; end if; -- B || P --> (~B) -> P return Build_Binary (N_Log_Imp_Prop, Build_Bool_Not (B), P); end Rewrite_Or; function Rewrite_Property (N : Node) return Node is begin case Get_Kind (N) is when N_Star_Repeat_Seq | N_Plus_Repeat_Seq | N_Equal_Repeat_Seq | N_Goto_Repeat_Seq | N_Sequence_Instance | N_Endpoint_Instance | N_Braced_SERE | N_And_Seq | N_Or_Seq => return Rewrite_SERE (N); when N_Imp_Seq | N_Overlap_Imp_Seq => Set_Sequence (N, Rewrite_Property (Get_Sequence (N))); Set_Property (N, Rewrite_Property (Get_Property (N))); return N; when N_Log_Imp_Prop => -- b -> p --> {b} |-> p return Build_Overlap_Imp_Seq (Rewrite_Boolean (Get_Left (N)), Rewrite_Property (Get_Right (N))); when N_Eventually => return Build_Strong (Build_Binary (N_Fusion_SERE, Build_Plus (True_Node), Rewrite_SERE (Get_Property (N)))); when N_Until => return Rewrite_Until (N); when N_Next => return Rewrite_Next (Get_Number (N), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Next_Event => return Rewrite_Next_Event (Rewrite_Boolean (Get_Boolean (N)), Get_Number (N), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Next_A => return Rewrite_Next_A (Get_Value (Get_Low_Bound (N)), Get_Value (Get_High_Bound (N)), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Next_Event_A => return Rewrite_Next_Event_A (Rewrite_Boolean (Get_Boolean (N)), Get_Value (Get_Low_Bound (N)), Get_Value (Get_High_Bound (N)), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Next_E => return Rewrite_Next_E (Get_Value (Get_Low_Bound (N)), Get_Value (Get_High_Bound (N)), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Next_Event_E => return Rewrite_Next_Event_E (Rewrite_Boolean (Get_Boolean (N)), Get_Value (Get_Low_Bound (N)), Get_Value (Get_High_Bound (N)), Rewrite_Property (Get_Property (N)), Get_Strong_Flag (N)); when N_Before => return Rewrite_Before (N); when N_Booleans => return Rewrite_Boolean (N); when N_Name => return Get_Decl (N); when N_Never | N_Always | N_Strong => -- Fully handled by psl.build Set_Property (N, Rewrite_Property (Get_Property (N))); return N; when N_Clock_Event => Set_Property (N, Rewrite_Property (Get_Property (N))); Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); return N; when N_And_Prop => Set_Left (N, Rewrite_Property (Get_Left (N))); Set_Right (N, Rewrite_Property (Get_Right (N))); return N; when N_Or_Prop => return Rewrite_Or (Rewrite_Property (Get_Left (N)), Rewrite_Property (Get_Right (N))); when N_Abort | N_Async_Abort | N_Sync_Abort => Set_Boolean (N, Rewrite_Boolean (Get_Boolean (N))); Set_Property (N, Rewrite_Property (Get_Property (N))); return N; when N_Property_Instance => Rewrite_Instance (N); return N; when N_Paren_Prop => -- Note: discard it. return Rewrite_Property (Get_Property (N)); when others => Error_Kind ("rewrite_property", N); end case; end Rewrite_Property; procedure Rewrite_Unit (N : Node) is Item : Node; begin Item := Get_Item_Chain (N); while Item /= Null_Node loop case Get_Kind (Item) is when N_Name_Decl => null; when N_Assert_Directive => Set_Property (Item, Rewrite_Property (Get_Property (Item))); when N_Property_Declaration => Set_Property (Item, Rewrite_Property (Get_Property (Item))); when others => Error_Kind ("rewrite_unit", Item); end case; Item := Get_Chain (Item); end loop; end Rewrite_Unit; end PSL.Rewrites;