https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/alu/formal;hb=HEAD * OP_ADD: done * OP_CMP: done however bug in 32 bit not done * OP_EXTS: done * OP_CMPEQB: done however setting RT out and CR out not properly detected
python3 alu/formal/proof_main_stage.py .. ---------------------------------------------------------------------- Ran 2 tests in 312.563s wooow :)
(In reply to Luke Kenneth Casson Leighton from comment #1) > python3 alu/formal/proof_main_stage.py .. > ---------------------------------------------------------------------- > Ran 2 tests in 312.563s > > wooow :) Yeah, adding shifts to the proof *really* slowed it down
* OP_EXTS proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=32d9da2bd849d3ae9b59bdec7a4add0c35908922 * OP_CMP and OP_CMPEQB proof https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=ca79ab18a7fa9bdabeca860448d79b5d11dc222f
hmm the same thing we noted in Branch, for CMPEQB is also not being picked up n the main_stage.py https://libre-soc.org/openpower/isa/comparefixed/ cmpeqb is only supposed to alter the CR, not the main register RT. the formal proof is not picking that up.
70 comb += Assume(a[32:64] == 0) 71 comb += Assume(b[32:64] == 0) michael in the alu proof should those be conditional? with m.If(op.is_32bit)?
(In reply to Luke Kenneth Casson Leighton from comment #5) > 70 comb += Assume(a[32:64] == 0) > 71 comb += Assume(b[32:64] == 0) > > michael in the alu proof should those be conditional? with m.If(op.is_32bit)? oh, yep. Fixed.
(In reply to Michael Nolan from comment #6) > (In reply to Luke Kenneth Casson Leighton from comment #5) > > 70 comb += Assume(a[32:64] == 0) > > 71 comb += Assume(b[32:64] == 0) > > > > michael in the alu proof should those be conditional? with m.If(op.is_32bit)? > > oh, yep. Fixed. star.
assigning to Samuel for review of formal_main_stage.py up to this point: # Assert that op gets copied from the input to output for rec_sig in rec.ports(): name = rec_sig.name dut_sig = getattr(dut.o.ctx.op, name) comb += Assert(dut_sig == rec_sig) https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;hb=HEAD#l56
from commit git diff 685b7 769a8, samuel did this: + # Output context is the same as the input context. + comb += Assert(dut.o.ctx != dut.i.ctx) this is the reasonable expectation: both are Records. should it be ok to Assert that one Record's contents equals the contents of another?
a bug in cmp was found https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py;h=b2d2279cf80dec3670d70e5b65359c92a9794acf;hb=29d0566fd104ab8b9ffd0c460fc7c588a72a340b#l50 the proof needs updating to match
(In reply to Luke Kenneth Casson Leighton from comment #10) > a bug in cmp was found > > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py; > h=b2d2279cf80dec3670d70e5b65359c92a9794acf; > hb=29d0566fd104ab8b9ffd0c460fc7c588a72a340b#l50 > > the proof needs updating to match Can you explain the bug? I see a link to line 50 of the main_stage.py file, but without more context, I don't know what I'm looking to fix in the proof. Thanks.
(In reply to Samuel A. Falvo II from comment #11) > Can you explain the bug? I see a link to line 50 of the main_stage.py file, > but without more context, I don't know what I'm looking to fix in the proof. > Thanks. ah sorry i should have recorded the diff-commit rather than a link to the line. the "L" field was previously being completely ignored. so where for example the pseudocode says this: * cmp BF,L,RA,RB if L = 0 then a <- EXTS((RA)[32:63] ) b <- EXTS((RB)[32:63]) else a <- (RA) b <- (RB) we were in fact simply doing this: * cmp BF,L,RA,RB a <- (RA) b <- (RB) because this was in the proof *and* the HDL and there was no corresponding unit test to catch it, the bug went unnoticed for several months.