Start preparing assertions for sorting network

This commit is contained in:
Donald Sebastian Leung 2020-10-16 12:18:09 +08:00
parent ec957ad411
commit 036c91539b
4 changed files with 47 additions and 1 deletions

View File

@ -1,5 +1,6 @@
from nmigen import *
from nmigen.utils import *
from nmigen.asserts import *
from rtio.sed import layouts
@ -44,13 +45,23 @@ def cmp_wrap(a, b):
return Mux((a[-2] == a[-1]) & (b[-2] == b[-1]) & (a[-1] != b[-1]), a[-1], a < b)
class OutputNetwork(Elaboratable):
def __init__(self, lane_count, seqn_width, layout_payload):
def __init__(self, lane_count, seqn_width, layout_payload, *, fv_mode=False):
m = Module()
self.m = m
self.input = [Record(layouts.output_network_node(seqn_width, layout_payload))
for _ in range(lane_count)]
self.output = None
if fv_mode:
# Model arbitrary inputs for network nodes
for i in range(lane_count):
m.d.comb += self.input[i].valid.eq(AnySeq(1))
m.d.comb += self.input[i].seqn.eq(AnySeq(seqn_width))
m.d.comb += self.input[i].replace_occured.eq(AnySeq(1))
m.d.comb += self.input[i].nondata_replace_occured.eq(AnySeq(1))
for field, width in layout_payload:
m.d.comb += getattr(self.input[i].payload, field).eq(AnySeq(width))
step_input = self.input
for step in boms_steps_pairs(lane_count):
step_output = []
@ -98,5 +109,22 @@ class OutputNetwork(Elaboratable):
self.output = step_output
step_input = step_output
if fv_mode:
# Sanity checks
assert self.output is not None
assert len(self.input) == lane_count
assert len(self.output) == lane_count
# Indicator of when Past() is valid
f_past_valid = Signal()
m.d.sync += f_past_valid.eq(1)
# TODO: assert outputs is a permutation of inputs
# Channel numbers for outputs are sorted in increasing order
with m.If(f_past_valid):
# TODO: Get the below (bogus) assertion to fail
m.d.comb += Assert(self.output[7].payload.channel == 0)
def elaborate(self, platform):
return self.m

0
rtio/test/__init__.py Normal file
View File

View File

View File

@ -0,0 +1,18 @@
from nmigen import *
from nmigen.asserts import *
from nmigen.test.utils import *
from ...sed.output_network import *
"""
Verification tasks for OutputNetwork
"""
class OutputNetworkTestCase(FHDLTestCase):
def verify(self):
# Bounded model check
self.assertFormal(
OutputNetwork(16, 2, [("data", 32), ("channel", 3)], fv_mode=True),
mode="bmc", depth=10)
# TODO: unbounded proof
OutputNetworkTestCase().verify()