Cycle accurate simulation

In previous session, we use combinational circuit design. Now, it is time for some sequential circuits!

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
from typing import List
from nmigen.asserts import Assert,Cover,Assume
from nmigen import Elaboratable, Module, Signal, Mux
from nmigen.back.pysim import Simulator, Delay
from nmigen.build import Platform
from nmigen.cli import main_parser, main_runner

class Clocky(Elaboratable):
    def __init__(self):
        self.x = Signal(7)
        self.load = Signal()
        self.value = Signal(7)
    def elaborate(self, platform: Platform) -> Module:
        m = Module()

        with m.If(self.load):
            m.d.sync += self.x.eq(Mux(self.value <= 100, self.value, 100))
        with m.Elif(self.x == 100):
            m.d.sync += self.x.eq(0)
        with m.Else():
            m.d.sync += self.x.eq(self.x + 1)
        return m
    def ports(self) -> List[Signal]:
        return [self.x, self.load, self.value]
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()

    #main_runner(parser, args, m, ports=[] + clocky.ports())

    load = Signal()
    value = Signal(7)
    m.d.comb += clocky.load.eq(load)
    m.d.comb += clocky.value.eq(value)

    sim = Simulator(m)
    sim.add_clock(1e-6)

    def process():
        yield
        yield load.eq(1)
        yield value.eq(95)
        yield
        yield load.eq(0)
        yield
        yield
        yield
        yield
        yield
        yield
        yield
        yield
        yield
    sim.add_sync_process(process)
    with sim.write_vcd("test.vcd", "test.gtkw", traces=[] + clocky.ports()):
        sim.run()

After simulation, here is the waveform. Imgur As you can see, x will be loaded when load is high and after the pulse, x will keep increasing each cycle until it reaches 100. Then x will be clear.

You might want to ask, why would x is not loaded at rising edge of load? That is becuase load is changing not simutanously with clock edge but infinitesimally close after clock rising edge. Which also applys to clock falling edge.

Formal verification

We remove simulator part and add main_runner into our clocky.py.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
from typing import List
from nmigen.asserts import Assert,Cover,Assume,Past
from nmigen import Elaboratable, Module, Signal, Mux
from nmigen.back.pysim import Simulator, Delay
from nmigen.build import Platform
from nmigen.cli import main_parser, main_runner

class Clocky(Elaboratable):
    def __init__(self):
        self.x = Signal(7)
        self.load = Signal()
        self.value = Signal(7)
    def elaborate(self, platform: Platform) -> Module:
        m = Module()

        with m.If(self.load):
            m.d.sync += self.x.eq(Mux(self.value <= 100, self.value, 100))
        with m.Elif(self.x == 100):
            m.d.sync += self.x.eq(0)
        with m.Else():
            m.d.sync += self.x.eq(self.x + 1)
        return m
    def ports(self) -> List[Signal]:
        return [self.x, self.load, self.value]
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()
    with m.If((clocky.x > 0)):
        m.d.sync += Assert(clocky.x == (Past(clocky.x) + 1)[:7])
    main_runner(parser, args, m, ports=[] + clocky.ports())

Generate toplevel iLang file and sby file.

1
python3 clocky.py generate -t il > toplevel.il

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
[tasks]
cover
bmc

[options]
bmc: mode bmc
cover: mode cover
depth 40
multiclock off

[engines]
smtbmc boolector

[script]
read_ilang toplevel.il
prep -top top

[files]
toplevel.il

1
sby -f clocky.sby

Note: use depth 40 which means to run 40 cycles. The result will be: It Failed on bmc test! Why? We can trace the bmc waveform.

gtkwave.exe clocky_bmc/engine_0/trace.vcd &

Imgur Yes, in formal verification, it found that Past(x) is 0x00 and x is 0x4A which violates the rule!

Here we change the condition into:

1
2
3
4
5
6
7
8
9
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()
    with m.If((clocky.x > 0) & (Past(clocky.load) == 0)):
        m.d.sync += Assert(clocky.x == (Past(clocky.x) + 1)[:7])
    main_runner(parser, args, m, ports=[] + clocky.ports())

Assertion will only applied if x > 0 & Past(load) == 0. After changing, it will pass the bmc test. Imgur

Here is another interesting case. We put a assertion like this:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()
    with m.If((clocky.x > 0) & (Past(clocky.load) == 0)):
        m.d.sync += Assert(clocky.x == (Past(clocky.x) + 1)[:7])
    with m.If(clocky.x == 0):
        m.d.sync += Assert(Past(clocky.x) == 100)
    main_runner(parser, args, m, ports=[] + clocky.ports())

This statement is not always true if x start with 0x00 at 0 ns. But who knows? Let’s fire formal verification up!

python3 clocky.py generate -t il > toplevel.il
sby -f clocky.sby

Imgur Oh, it discoverd our little secret! Let’s take a look into trace waveform.

gtkwave.exe clocky_bmc/engine_0/trace.vcd &

Imgur Wow! It actually discovers a specific case that we just talked about. x begins with 0 initial value!

Okie, how about we say only checks this condition under Past(rst) == 0?

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()

    rst = ResetSignal()
    with m.If((clocky.x > 0) & (Past(clocky.load) == 0)):
        m.d.sync += Assert(clocky.x == (Past(clocky.x) + 1)[:7])
    with m.If((clocky.x == 0) & (Past(rst) == 0) ):
        m.d.sync += Assert(Past(clocky.x) == 100)
    main_runner(parser, args, m, ports=[] + clocky.ports())

The answer is …still no!

Imgur

As you can see, you must be very careful about condtion in formal verification especially in a complex design.

Here is the correct condition:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.clocky = clocky = Clocky()

    rst = ResetSignal()
    with m.If((clocky.x > 0) & (Past(clocky.load) == 0)):
        m.d.sync += Assert(clocky.x == (Past(clocky.x) + 1)[:7])
    with m.If((clocky.x == 0) & (Past(rst) == 0) & (Past(clocky.load) == 0)):
        m.d.sync += Assert(Past(clocky.x) == 100)
    main_runner(parser, args, m, ports=[] + clocky.ports())

And here is the result: Imgur

[Day10] Clock domain simulation!

Cycle accurate simulation

Formal verification