[Day06] Formal_verification

Assert, Assume, and Cover for fun and profit.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
from nmigen.asserts import Assert, Assume, Cover
from nmigen.cli import main_parser, main_runner
from somewhere import Adder

if __name__ == "__main__":
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    m.submodules.adder = adder = Adder()
    m.d.comb += Assert(adder.out == (adder.x + adder.y)[:8])
    with m.If(adder.x == (adder.y << 1)):
        m.d.comb += Cover((adder.out > 0x00) & (adder.out < 0x40))
    main_runner(parser, args, m, ports=[] + adder.ports())

Past, Rose, Fell, Stable

from nmigen.asserts import Assert, Assume, Cover
from nmigen.asserts import Past, Rose, Fell, Stable

Not ready yet.

updatedupdated2021-09-192021-09-19