-
Notifications
You must be signed in to change notification settings - Fork 69
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #3904 from alainmarcel/alainmarcel-patch-1
File level binding
- Loading branch information
Showing
8 changed files
with
4,828 additions
and
16 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
-parse -d uhdm -d coveruhdm -elabuhdm -d ast left_rotate_assertions.sv left_rotate.sv tb_left_rotate.sv -nobuiltin |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
module left_rotation ( | ||
input wire clk, // Clock input | ||
input wire reset, // Active-high synchronous reset | ||
input wire [7:0] in_data, // 8-bit input data | ||
output reg [7:0] out_data // 8-bit output data after rotation | ||
); | ||
|
||
always @(posedge clk or posedge reset) begin | ||
if (reset) begin | ||
out_data <= 8'b0000_0000; // Reset value | ||
end else begin | ||
// Perform left rotation | ||
out_data <= {out_data[6:0], out_data[7]}; | ||
end | ||
end | ||
|
||
initial begin | ||
out_data = 8'b0000_0000; // Initial value | ||
end | ||
|
||
endmodule | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
module left_rotate_assertions ( | ||
input clk, | ||
input rst_n, | ||
input [31:0] word_in, | ||
input [4:0] rotate_by, // 5 bits can represent values from 0 to 31 | ||
input [31:0] rotated | ||
); | ||
|
||
// Initialization check | ||
initial begin | ||
@(posedge clk); | ||
if (!rst_n) begin | ||
assert(rotated == 0); | ||
end | ||
end | ||
|
||
// Valid Rotation | ||
property p_valid_rotation; | ||
@(posedge clk) (!rst_n) |-> (rotated == (word_in << rotate_by) | (word_in >> (32-rotate_by))); | ||
endproperty | ||
a_valid_rotation: assert property(p_valid_rotation); | ||
|
||
// Rotation Range | ||
property p_rotation_range; | ||
@(posedge clk) (!rst_n) |-> (rotate_by <= 5'd31); | ||
endproperty | ||
a_rotation_range: assert property(p_rotation_range); | ||
|
||
// No Rotation | ||
property p_no_rotation; | ||
@(posedge clk) (!rst_n && rotate_by == 0) |-> (rotated == word_in); | ||
endproperty | ||
a_no_rotation: assert property(p_no_rotation); | ||
|
||
endmodule | ||
|
||
bind left_rotation left_rotate_assertions u_left_rotate_assertions ( | ||
.clk(clk), | ||
.rst_n(reset), | ||
.word_in(in_data), | ||
.rotate_by(), | ||
.rotated(out_data) | ||
); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
|
||
module tb_left_rotation; | ||
reg clk, reset; | ||
reg [7:0] in_data; | ||
wire [7:0] out_data; | ||
|
||
// Instantiate the left_rotation module | ||
left_rotation left_rotation_inst( | ||
.clk(clk), | ||
.reset(reset), | ||
.in_data(in_data), | ||
.out_data(out_data) | ||
); | ||
|
||
// Clock generator | ||
always begin | ||
#5 clk = ~clk; | ||
end | ||
|
||
// Test procedure | ||
initial begin | ||
// Initial conditions | ||
clk = 0; | ||
reset = 1; | ||
in_data = 8'b0; | ||
#10 reset = 0; | ||
#10; | ||
|
||
// Start VCD dumping | ||
$dumpfile("left_rotation.vcd"); | ||
$dumpvars(0, tb_left_rotation); | ||
|
||
// Apply random inputs and observe the output | ||
repeat(20) begin | ||
in_data = $random & 8'b11111111; | ||
#10; | ||
end | ||
|
||
// Assert reset to observe reset behavior | ||
#10 reset = 1; | ||
#10 reset = 0; | ||
|
||
// Finish the simulation | ||
$finish; | ||
end | ||
endmodule | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters