From 555594f6b55a2c34b790c38e7252fe256e194f89 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Fri, 8 May 2020 14:59:45 -0400 Subject: [PATCH] Add assertions for output stage cr0 --- src/soc/alu/formal/proof_output_stage.py | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/soc/alu/formal/proof_output_stage.py b/src/soc/alu/formal/proof_output_stage.py index 50fc4e49..dc723acd 100644 --- a/src/soc/alu/formal/proof_output_stage.py +++ b/src/soc/alu/formal/proof_output_stage.py @@ -1,7 +1,7 @@ # Proof of correctness for partitioned equal signal combiner # Copyright (C) 2020 Michael Nolan -from nmigen import Module, Signal, Elaboratable, Mux, Cat +from nmigen import Module, Signal, Elaboratable, Mux, Cat, signed from nmigen.asserts import Assert, AnyConst, Assume, Cover from nmigen.test.utils import FHDLTestCase from nmigen.cli import rtlil @@ -64,6 +64,20 @@ class Driver(Elaboratable): with m.Else(): comb += Assert(dut.o.o == o) + cr_out = Signal.like(cr0) + comb += cr_out.eq(dut.o.cr0) + + o_signed = Signal(signed(64)) + comb += o_signed.eq(dut.o.o) + # Assert only one of the comparison bits is set + comb += Assert(cr_out[0] + cr_out[1] + cr_out[2] == 1) + with m.If(o_signed == 0): + comb += Assert(cr_out[2] == 1) + with m.Elif(o_signed > 0): + comb += Assert(cr_out[1] == 1) + with m.Elif(o_signed < 0): + comb += Assert(cr_out[0] == 1) + # Assert that op gets copied from the input to output for p in rec.ports(): -- 2.30.2