2020-11-22 07:42:30 +08:00
|
|
|
module top(input clk, rst, output [7:0] leds);
|
2021-02-11 19:10:32 +08:00
|
|
|
|
2020-11-29 10:08:09 +08:00
|
|
|
// TODO: Test miter circuit without reset value. SAT and SMT diverge without
|
|
|
|
|
// reset value (SAT succeeds, SMT fails). I haven't figured out the correct
|
|
|
|
|
// init set of options to make SAT fail.
|
|
|
|
|
// "sat -verify -prove-asserts -set-init-def -seq 1 miter" causes assertion
|
|
|
|
|
// failure in yosys.
|
2020-11-27 08:27:09 +08:00
|
|
|
reg [7:0] ctr = 8'h00;
|
2021-02-11 19:10:32 +08:00
|
|
|
always @(posedge clk)
|
|
|
|
|
if (rst)
|
|
|
|
|
ctr <= 8'h00;
|
|
|
|
|
else
|
|
|
|
|
ctr <= ctr + 1'b1;
|
|
|
|
|
|
|
|
|
|
assign leds = ctr;
|
|
|
|
|
|
|
|
|
|
endmodule
|
