{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:16:13Z","timestamp":1754486173517,"version":"3.32.0"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,1]]},"DOI":"10.1007\/bf01383955","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T08:40:21Z","timestamp":1112431221000},"page":"5-31","source":"Crossref","is-referenced-by-count":15,"title":["A proof of the nonrestoring division algorithm and its implementation on an ALU"],"prefix":"10.1007","volume":"4","author":[{"given":"D.","family":"Verkest","sequence":"first","affiliation":[]},{"given":"L.","family":"Claesen","sequence":"additional","affiliation":[]},{"given":"H.","family":"De Man","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"CR1","first-page":"73","volume":"3","author":"H. Man De","year":"1986","unstructured":"H. De Man, J. Rabaey, P. Six, and L. Claesen. Cathedral-II: a silicon compiler for digital signal processing.IEEE Design & Test of Computers, 3(6):73?85, December 1986.","journal-title":"IEEE Design & Test of Computers"},{"key":"CR2","first-page":"213","volume-title":"Proceedings of IEEE 1985 Custom Integrated Circuits Conference, Portland Oregon, May","author":"P.N. Hilfinger","year":"1985","unstructured":"P.N. Hilfinger. A high level language and silicon compiler for digital signal processing. InProceedings of IEEE 1985 Custom Integrated Circuits Conference, Portland Oregon, May, IEEE, New York, pp. 213?216, 1985."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"P. Six, L. Claesen, J. Rabaey, and H. De Man. An intelligent module generation environment. InProceedings of the 23rd Design Automation Conference, Las Vegas, IEEE Computer Society Press, pp. 730?735, July 1986.","DOI":"10.1109\/DAC.1986.1586171"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-1-4613-2007-4_2","volume-title":"VLSI: Specification, Verification and Synthesis","author":"A. Cohn","year":"1988","unstructured":"A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. InVLSI: Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam (eds), Kluwer Academic Publishers, Boston, 1988, pp. 27?71."},{"key":"CR5","first-page":"85","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"W.A. Hunt","year":"1987","unstructured":"W.A. Hunt, FM8501: A verified microprocessor. InFrom HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, ed., pp. 85?114, Elsevier Science Publishers, Amsterdam, 1987."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"D. Verkest, L. Claesen, and H. De Man. Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environment. InProceedings of EDAC-90, pp. 62?66, Glasgow, Scotland, March 1990.","DOI":"10.1109\/EDAC.1990.136621"},{"key":"CR7","unstructured":"D. Verkest. Verification of parameterized modules using the Boyer-Moore theorem prover. Intermediate Report IMEC-2.A.2-01 of CHARME BRA 3216, July 1990."},{"key":"CR8","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore.A Computational Logic Handbook. Academic Press, New York, 1988."},{"key":"CR9","series-title":"Technical Report","volume-title":"A user's manual for an interactive enhancement to the Boyer-Moore theorem prover","author":"M. Kaufmann","year":"1988","unstructured":"M. Kaufmann. A user's manual for an interactive enhancement to the Boyer-Moore theorem prover. Technical Report 19. Computational Logic Inc., Austin, TX, May 1988."},{"key":"CR10","volume-title":"Introduction to Arithmetic for Digital System Designers","author":"Schlomo Waser","year":"1982","unstructured":"Schlomo Waser and Michael J. Flynn.Introduction to Arithmetic for Digital System Designers. Holt, Rinehart and Winston, New York, NY, 1982."},{"key":"CR11","first-page":"309","volume-title":"Formal VLSI Correctness Verification, VLSI Design Methods, II","author":"L. Pierre","year":"1990","unstructured":"L. Pierre. The formal proof of sequential circuits described in CASCADE using the Boyer-Moore theorem prover. InFormal VLSI Correctness Verification, VLSI Design Methods, II, L.J.M. Claesen (ed.). Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1990, pp. 309?328."},{"key":"CR12","series-title":"Internal report","volume-title":"The division operation on the IMEC ALU","author":"M. Pauwels","year":"1988","unstructured":"M. Pauwels. The division operation on the IMEC ALU. Internal report, IMEC, Kapeldreef 75, B-3001 Leuven, Belgium, March 1988."},{"key":"CR13","first-page":"52","volume-title":"Second Great Lakes Symposium on VLSI","author":"M. Pauwels","year":"1992","unstructured":"M. Pauwels, D. Lanneer, F. Catthoor, G. Goossens, and H. De Man. Models for bit-true simulation and high-level synthesis of DSP applications. InSecond Great Lakes Symposium on VLSI, pp. 52?59. Kalamazoo, Michigan USA, IEEE Computer Society Press, Los Alamos, CA, February 1992."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383955.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383955\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T06:01:35Z","timestamp":1735538495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,1]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994,1]]}},"alternative-id":["BF01383955"],"URL":"https:\/\/doi.org\/10.1007\/bf01383955","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1994,1]]}}}