Skip to content

Commit

Permalink
seq rule update
Browse files Browse the repository at this point in the history
  • Loading branch information
alaindargelas committed Oct 14, 2023
1 parent 43619fe commit e5dfc7f
Show file tree
Hide file tree
Showing 8 changed files with 7,839 additions and 272 deletions.
6,987 changes: 6,987 additions & 0 deletions tests/AssertTempError/AssertTempError.log

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions tests/AssertTempError/AssertTempError.sl
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
-parse -d uhdm -d coveruhdm -elabuhdm -d ast design.sv testbench.sv -nobuiltin
100 changes: 100 additions & 0 deletions tests/AssertTempError/design.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
// Code your design here
module UART(
input clk, // System Clock
input rst_n, // Active low reset
input rx, // RX line
output reg tx, // TX line
input [7:0] data, // Data to transmit
input send, // Signal to start transmission
output reg done // Signal to indicate transmission done
);

parameter IDLE = 0, START = 1, DATA = 2, STOP = 3;
reg [7:0] shift_reg;
reg [2:0] state, next_state;
reg [2:0] bit_counter;
reg tx_next;

always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
state <= IDLE;
tx <= 1'b1;
end else begin
state <= next_state;
tx <= tx_next;
end
end

always @(state, rx, shift_reg, bit_counter, send, data) begin
next_state = state;
tx_next = tx;
done = 1'b0;

case (state)
IDLE: begin
if (send) begin
tx_next = 1'b0; // Start bit
shift_reg = data;
bit_counter = 0;
next_state = START;
end
end
START: begin
bit_counter = bit_counter + 1;
if (bit_counter == 7) begin
tx_next = shift_reg[0];
shift_reg = shift_reg >> 1;
next_state = DATA;
end
end
DATA: begin
bit_counter = bit_counter + 1;
if (bit_counter == 15) begin
tx_next = 1'b1; // Stop bit
next_state = STOP;
end else begin
tx_next = shift_reg[0];
shift_reg = shift_reg >> 1;
end
end
STOP: begin
done = 1'b1;
next_state = IDLE;
end
endcase
end

endmodule


module UART_assertions (
input clk,
input rst_n,
input send,
input done

);

reg [2:0] state;
parameter IDLE = 0, START = 1, DATA = 2, STOP = 3;

// Property to check the send functionality
property p_send;
@(posedge clk)
send |=> (state == DATA);
endproperty

assert property (p_send) else $display("Send property violated");

// Property to check the done functionality
property p_done;
@(posedge clk)
done |=> (state == STOP);
endproperty

assert property (p_done) else $display("Done property violated");

endmodule


bind UART UART_assertions uut(.clk(clk),.rst_n(rst_n),.send(send),.done(done));
54 changes: 54 additions & 0 deletions tests/AssertTempError/testbench.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
// Code your testbench here
// or browse Examples
module tb_UART;
reg clk, rst_n, send;
reg rx; // Not used in this testbench
reg [7:0] data;
wire tx, done;

// Instantiate the UART module
UART uart_inst(
.clk(clk),
.rst_n(rst_n),
.rx(rx),
.tx(tx),
.data(data),
.send(send),
.done(done)
);


// Clock generator
always begin
#5 clk = ~clk;
end

// Test procedure
initial begin
// Start VCD dumping
$dumpfile("UART.vcd");
$dumpvars(0, tb_UART);
// Initial conditions
clk = 0;
rst_n = 0;
send = 0;
data = 8'b00000000;
rx = 1; // Assuming no data is received during the test
#10 rst_n = 1;
#10;



// Apply random inputs and observe the output
repeat(10) begin
data = $random & 8'b11111111;
send = 1;
#10 while(!done) #10; // Wait for transmission to complete
send = 0;
#10;
end

// Finish the simulation
$finish;
end
endmodule
Loading

0 comments on commit e5dfc7f

Please sign in to comment.