git.libre-soc.org Git - soc.git/history - src/soc/regfile/formal/proof

2020-06-04	Luke Kenneth Casso...	use copy of FHDLTestCase	blob \| commitdiff \| raw
2020-06-01	Michael Nolan	Have regfile use AnySeq instead of AnyConst	blob \| commitdiff \| raw \| diff to current
2020-06-01	Michael Nolan	Enable k-induction for register file proof	blob \| commitdiff \| raw \| diff to current
2020-06-01	Michael Nolan	That was weird. For some reason it wasn't generating...	blob \| commitdiff \| raw \| diff to current
2020-06-01	Michael Nolan	Full BMC proof of Register	blob \| commitdiff \| raw \| diff to current
2020-06-01	Michael Nolan	Begin rewrite of proof_regfile.py	blob \| commitdiff \| raw \| diff to current
2020-05-28	Luke Kenneth Casso...	messing about with proof_regfile.py	blob \| commitdiff \| raw \| diff to current
2020-05-28	colepoirier	Added Initial() synchronous check with draft truth	blob \| commitdiff \| raw \| diff to current
2020-05-28	Luke Kenneth Casso...	hmm....	blob \| commitdiff \| raw \| diff to current
2020-05-28	colepoirier	Add sync Assert for _wrports 'wen' signal in proof_regf...	blob \| commitdiff \| raw \| diff to current
2020-05-27	Luke Kenneth Casso...	do not use range(0, x) - just range(x)	blob \| commitdiff \| raw \| diff to current
2020-05-27	colepoirier	Derive proof_regfile Driver from regfile.Register(...	blob \| commitdiff \| raw \| diff to current
2020-05-27	colepoirier	Fix indentation of regfile/formal/proof_regfile.py	blob \| commitdiff \| raw \| diff to current
2020-05-27	colepoirier	First commit of proof of regfile, not working yet	blob \| commitdiff \| raw \| diff to current