Added formal verification and simulator framework

tutorial/formal_verification/adder.py

@@ -0,0 +1,17 @@
+from amaranth import Elaboratable, Module, Signal
+from amaranth.build import Platform
+from amaranth import * 
+
+
+class Adder(Elaboratable):
+    def __init__(self):
+        self.x = Signal(signed(16))
+        self.y = Signal(signed(16))
+        self.out = Signal(signed(32))
+
+    def ports(self):
+        return [self.x, self.y, self.out]
+
+    def elaborate(self, platform: Platform) -> Module:
+        m = Module()
+        return m

tutorial/formal_verification/adder.sby

@@ -0,0 +1,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

tutorial/formal_verification/adder_test.py

@@ -0,0 +1,19 @@
+from amaranth.asserts import Assert, Assume, Cover
+from amaranth.asserts import Past, Rose, Fell, Stable
+from amaranth.cli import main_parser, main_runner
+from amaranth import Module
+from adder 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())

tutorial/formal_verification/toplevel.il

@@ -0,0 +1,160 @@
+attribute \generator "Amaranth"
+attribute \amaranth.hierarchy "top.adder"
+module \adder
+  wire width 1 $empty_module_filler
+end
+attribute \generator "Amaranth"
+attribute \top 1
+attribute \amaranth.hierarchy "top"
+module \top
+  attribute \src "/home/ggangliu/first-riscv/tutorial/formal_verification/adder.py:8"
+  wire width 16 input 0 \x
+  attribute \src "/home/ggangliu/first-riscv/tutorial/formal_verification/adder.py:9"
+  wire width 16 input 1 \y
+  attribute \src "/home/ggangliu/first-riscv/tutorial/formal_verification/adder.py:10"
+  wire width 32 input 2 \out
+  cell \adder \adder
+  end
+  attribute \src "adder_test.py:14"
+  wire width 1 $assert$en
+  attribute \src "adder_test.py:14"
+  wire width 1 $assert$check
+  attribute \src "/home/ggangliu/.local/lib/python3.8/site-packages/amaranth/hdl/ast.py:254"
+  wire width 32 $1
+  attribute \src "adder_test.py:14"
+  wire width 17 $2
+  attribute \src "adder_test.py:14"
+  wire width 17 $3
+  attribute \src "adder_test.py:14"
+  cell $add $4
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 16
+    parameter \B_SIGNED 1
+    parameter \B_WIDTH 16
+    parameter \Y_WIDTH 17
+    connect \A \x
+    connect \B \y
+    connect \Y $3
+  end
+  connect $2 $3
+  attribute \src "/home/ggangliu/.local/lib/python3.8/site-packages/amaranth/hdl/ast.py:254"
+  cell $pos $5
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 8
+    parameter \Y_WIDTH 32
+    connect \A $2 [7:0]
+    connect \Y $1
+  end
+  attribute \src "adder_test.py:14"
+  wire width 1 $6
+  attribute \src "adder_test.py:14"
+  cell $eq $7
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 32
+    parameter \B_SIGNED 1
+    parameter \B_WIDTH 32
+    parameter \Y_WIDTH 1
+    connect \A \out
+    connect \B $1
+    connect \Y $6
+  end
+  attribute \src "adder_test.py:14"
+  cell $assert $8
+    connect \A $assert$check
+    connect \EN $assert$en
+  end
+  process $group_0
+    assign $assert$en 1'0
+    assign $assert$check 1'0
+    assign $assert$check $6
+    assign $assert$en 1'1
+    sync init
+  end
+  attribute \src "adder_test.py:17"
+  wire width 1 $cover$en
+  attribute \src "adder_test.py:17"
+  wire width 1 $cover$check
+  attribute \src "adder_test.py:16"
+  wire width 17 $9
+  attribute \src "adder_test.py:16"
+  cell $sshl $10
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 16
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 17
+    connect \A \y
+    connect \B 1'1
+    connect \Y $9
+  end
+  attribute \src "adder_test.py:16"
+  wire width 1 $11
+  attribute \src "adder_test.py:16"
+  cell $eq $12
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 16
+    parameter \B_SIGNED 1
+    parameter \B_WIDTH 17
+    parameter \Y_WIDTH 1
+    connect \A \x
+    connect \B $9
+    connect \Y $11
+  end
+  attribute \src "adder_test.py:17"
+  wire width 1 $13
+  attribute \src "adder_test.py:17"
+  cell $gt $14
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 32
+    parameter \B_SIGNED 1
+    parameter \B_WIDTH 32
+    parameter \Y_WIDTH 1
+    connect \A \out
+    connect \B 32'00000000000000000000000000000000
+    connect \Y $13
+  end
+  attribute \src "adder_test.py:17"
+  wire width 1 $15
+  attribute \src "adder_test.py:17"
+  cell $lt $16
+    parameter \A_SIGNED 1
+    parameter \A_WIDTH 32
+    parameter \B_SIGNED 1
+    parameter \B_WIDTH 32
+    parameter \Y_WIDTH 1
+    connect \A \out
+    connect \B 32'00000000000000000000000001000000
+    connect \Y $15
+  end
+  attribute \src "adder_test.py:17"
+  wire width 1 $17
+  attribute \src "adder_test.py:17"
+  cell $and $18
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A $13
+    connect \B $15
+    connect \Y $17
+  end
+  attribute \src "adder_test.py:17"
+  cell $cover $19
+    connect \A $cover$check
+    connect \EN $cover$en
+  end
+  process $group_2
+    assign $cover$en 1'0
+    assign $cover$check 1'0
+    attribute \src "adder_test.py:16"
+    switch { $11 }
+      attribute \src "adder_test.py:16"
+      case 1'1
+        assign $cover$check $17
+        assign $cover$en 1'1
+    end
+    sync init
+  end
+end
+

tutorial/simulator-framework/top-level.py

@@ -0,0 +1,39 @@
+from amaranth import Module
+from amaranth.sim import Simulator, Delay, Settle
+from your_module import YourModule
+
+if __name__ == "__main__":
+    m = Module()
+    m.submodules.yourmodule = yourmodule = YourModule()
+
+    sim = Simulator(m)
+	sim.add_clock(1e-6, domain="fast_clock")
+	sim.add_clock(0.91e-6, domain="faster_clock")
+
+    def process():
+        # To be defined
+		yield x.eq(0)
+		yield Delay(1e-6)
+		yield y.eq(0xff)
+		yield Settle()
+		got = yield yourmodel.sum
+		want = yield (x+y)[:8]
+		if got != want:
+			print("xx")
+
+    def process_sync():
+        # To be defined
+		yield x.eq(0)
+		yield Delay(1e-6)
+		yield y.eq(0xff)
+		yield Settle()
+		got = yield yourmodel.sum
+		want = yield (x+y)[:8]
+		if got != want:
+			print("xx")
+
+	sim.add_process(process) # or sim.add_sync_process(process), see below
+    sim.add_sync_process(process_sync, domain="name1")
+
+    with sim.write_vcd("test.vcd", "test.gtkw", traces=yourmodule.ports()):
+        sim.run()

tutorial/simulator-framework/your_module.py

@@ -0,0 +1,7 @@
+from amaranth import Elaboratable
+
+
+class YourModule(Elaboratable):
+    ...
+    def ports(self):
+        return [self.yourmodule.p1, self.yourmodule.p2, ...]