Page MenuHomePhorge
Files F386717

counter_comlex.v
No OneTemporary
Actions

Size
2 KB
Referenced Files
None
Subscribers
None

counter_comlex.v
View Options

module counter ( clk, rst, mode, cnt);
input wire clk;
input wire rst;
input wire mode;
output reg signed[10-1:0] cnt;
reg signed[10-1:0] add_val;
always @*
begin
add_val = 10'sd0;
if (mode) begin
if (cnt!=10'sd14) begin
if (cnt <=10'sd218) begin
add_val <= 10'sd5;
end
end else if (cnt <= 10'sd213 ) begin
add_val <= 10'sd10;
end
end else begin
if (cnt!=10'sd28) begin
if (cnt>=-10'sd233) begin
add_val<=-10'sd9;
end
end else if (cnt >= -10'sd224) begin
add_val <= -10'sd18;
end
end
end
always @(posedge clk) begin
if (rst)
cnt <= -10'sd62;
else begin
cnt<= cnt + add_val;
end
end
`ifdef FORMAL
reg init = 1;
always @(posedge clk) begin
if (init) assume(rst);
else assume(!rst);
init <= 0;
end
always @(posedge clk) begin
if (rst) begin
assert (cnt == -10'sd62);
end
if (!rst) begin
assert (cnt <= 10'sd223);
assert (cnt >= -10'sd242);
assert (cnt != 10'sd19);
if ($past(mode)) begin
if (!$past(rst)) begin
if ($past(cnt) == (10'sd19-10'sd5)) begin
assert ((cnt - $past(cnt)) == (10'sd10));
end else if ($past(cnt) <= 10'sd223 && $past(cnt) > (10'sd223-10'sd5)) begin
assert ((cnt - $past(cnt)) == 0);
end else begin
assert ((cnt - $past(cnt)) == 10'sd5);
end
end
end
// Counting down
if (!$past(mode)) begin
if (!$past(rst)) begin
if ($past(cnt) == (10'sd19+10'sd9)) begin
assert (($past(cnt) - cnt) == (10'sd18));
end else if ($past(cnt) >= -10'sd242 && $past(cnt) < (-10'sd242+10'sd9)) begin
assert (($past(cnt) - cnt) == 0);
end else begin
assert (($past(cnt) - cnt) == 10'sd9);
end
end
end
end
end
`endif
endmodule
/* Number of wires: 14
Number of wire bits: 59
Number of public wires: 5
Number of public wire bits: 23
Number of ports: 4
Number of port bits: 13
Number of memories: 0
Number of memory bits: 0
Number of processes: 0
Number of cells: 11
$add 1
$adff 1
$ge 2
$le 2
$mux 3
$ne 2*/

File Metadata

Mime Type
text/plain
Expires
Fri, Jul 4, 5:57 AM (5 h, 17 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
157481
Default Alt Text
counter_comlex.v (2 KB)

Event Timeline