1// BUF from Chapter 4 of FoCs User's Manual (www.haifa.il.ibm.com/projects/verification/focs/) 2 3//---------------------------------- Sender ---------------------------------- 4// Send the sequence 0, 1, 2, ... , 99 5 6module Sender (BtoS_ACK, StoB_REQ, DI); 7 8input BtoS_ACK; 9output StoB_REQ; 10output [31:0] DI; 11reg StoB_REQ; 12reg [31:0] DI; 13 14initial 15 begin 16 DI = 0; 17 #10 18 while (DI < 100) 19 begin 20 StoB_REQ = 1; // Assert request 21 @(posedge BtoS_ACK) // Wait for ack to be asserted 22 #10 // Wait 10 time units 23 StoB_REQ = 0; // Deassert request 24 #10 // Wait 10 time units 25 @(negedge BtoS_ACK) // Wait for ack to be de-asserted 26 #10 // Wait 10 time units before incrementing data 27 DI = DI + 1; // Increment data to be sent next iteration 28 end 29 #10 $finish; 30 end 31 32endmodule 33 34//---------------------------------- BUF ------------------------------------- 35// Receive data from Sender and then send it to Receiver 36 37module BUF (clk,StoB_REQ, RtoB_ACK, DI, BtoS_ACK, BtoR_REQ, DO); 38 39input clk; 40input StoB_REQ; 41input RtoB_ACK; 42input [31:0] DI; 43output BtoS_ACK; 44output BtoR_REQ; 45output [31:0] DO; 46reg BtoS_ACK; 47reg BtoR_REQ; 48reg [31:0] DO; 49 50// BUF internal state registers 51reg free; // Flag to say if BUF is free to receive new data 52reg [31:0] data; // Data last read from Sender 53 54initial 55 begin 56 BtoS_ACK = 0; // Initially BtoS_ACK not asserted 57 BtoR_REQ = 0; // Initially BtoR_REQ not asserted 58 free = 1; // Initially free is true 59 end 60 61always @(posedge clk) 62 if (StoB_REQ && free) // Wait for StoB_REQ to be asserted and BUF free 63 begin 64 free = 0; // Set BUF to be not free 65 data = DI; // Read data 66 #10 BtoS_ACK = 1; // Tell Sender data is aquired 67 #10 DO = data; // Put dat on DO 68 #10 BtoR_REQ = 1; // Assert BtoR_REQ 69 @(posedge RtoB_ACK) // Wait for Receiver to acknowledge receipt of data 70 #10 BtoR_REQ = 0; // Deassert BtoR_REQ 71 #10 BtoS_ACK = 0; // Deassert BtoS_ACK 72 free = 1; // Set BUF to be free 73 end 74 else 75 #10 begin end 76 77endmodule 78 79 80 81//---------------------------------- Receiver -------------------- 82// Receive data from BUF 83 84module Receiver (BtoR_REQ, DO, RtoB_ACK); 85 86input BtoR_REQ; 87input [31:0] DO; 88output RtoB_ACK; 89reg RtoB_ACK; 90 91// Receiver internal state registers 92reg [31:0] data; // Data last read from BUF 93 94initial RtoB_ACK = 0; // Initially RtoB_ACK not asserted 95 96always 97 @(posedge BtoR_REQ) // Wait for BtoR_REQ to be asserted 98 begin 99 #10 data = DO; // Copy data from DO 100 #10 RtoB_ACK = 1; // Assert RtoB_ACK to say data aquired 101 #10 @(negedge BtoR_REQ) // Wait for BtoR_REQ to be deasserted 102 #10 RtoB_ACK = 0; // Deassert RtoB_ACK 103 end 104 105endmodule 106 107// ------------------------------- Checker ------------------------------------ 108// The following regular expression as a Verilog state machine 109// sere2regexp 110// (S_REPEAT S_TRUE ;; 111// S_BOOL (B_AND (B_NOT (B_PROP StoB_REQ),B_PROP BtoS_ACK)) ;; 112// S_BOOL (B_PROP StoB_REQ)) 113 114module Checker (StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK, state); 115 116input StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK; 117output [2:0] state; 118reg [2:0] state; 119 120initial state = 0; 121 122always @ (StoB_REQ or BtoS_ACK or BtoR_REQ or RtoB_ACK) 123begin 124 case (state) 125 0: 126 if (StoB_REQ) state = 1; 127 else 128 if (BtoS_ACK) state = 2; 129 else state = 1; 130 131 1: 132 if (StoB_REQ) state = 1; 133 else 134 if (BtoS_ACK) state = 2; 135 else state = 1; 136 137 2: 138 if (StoB_REQ) state = 3; 139 else 140 if (BtoS_ACK) state = 2; 141 else state = 1; 142 143 3: begin $display ("Checker: property violated!"); $finish; end 144 145 default: begin $display ("Checker: unknown state"); $finish; end 146 endcase 147end 148 149endmodule 150 151//---------------------------------- Test ------------------------------------ 152// Top level module linking Sender, BUF and Receiver 153 154module test (); 155 156wire StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK; 157wire [31:0] DI, DO; 158wire [2:0] state; 159reg clk; 160 161 162Sender M1(BtoS_ACK, StoB_REQ, DI); 163BUF M2(clk,StoB_REQ, RtoB_ACK, DI, BtoS_ACK, BtoR_REQ, DO); 164Receiver M3(BtoR_REQ, DO, RtoB_ACK); 165Checker M4(StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK, state); 166 167initial $monitor("State: %0d", state); 168 169// Make clock tick 170initial 171 forever 172 begin 173 #10 clk = 0; 174 #10 clk = 1; 175 end 176 177// Xtreme kludge to generate output that can be munged 178// into SimRun example in test (have eliminated strings) 179 180//initial 181// begin 182// $monitor 183// ("Time = %0d, clk = %0d, StoB_REQ = %0d, BtoS_ACK = %0d, DI = %0d, BtoR_REQ = %0d, RtoB_ACK = %0d, DO = %0d", 184// $time, clk, StoB_REQ, BtoS_ACK, DI, BtoR_REQ, RtoB_ACK, DO); 185// end 186 187// initial 188// begin 189// $monitor 190// ("((if %0d=1 then {\"StoB_REQ\"} else {}) UNION\ 191// (if %0d=1 then {\"BtoS_ACK\"} else {}) UNION\ 192// (if %0d=1 then {\"BtoR_REQ\"} else {}) UNION\ 193// (if %0d=1 then {\"RtoB_ACK\"} else {}));", 194// StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK); 195// end 196 197endmodule 198 199 200 201//initial 202// $monitor 203// ("val At_%0d = ``(StoB_REQ = %0d) /\\ (BtoS_ACK = %0d) /\\ (BtoR_REQ = %0d) /\\ (RtoB_ACK = %0d)``;", 204// $time, StoB_REQ, BtoS_ACK, BtoR_REQ, RtoB_ACK); 205 206 207 208//initial 209// begin 210// $monitor 211// ("Time = %0d, clk = %0d, StoB_REQ = %0d, BtoS_ACK = %0d, DI = %0d, BtoR_REQ = %0d, RtoB_ACK = %0d, DO = %0d", 212// $time, clk, StoB_REQ, BtoS_ACK, DI, BtoR_REQ, RtoB_ACK, DO); 213// end 214 215 216 217