| 1. |
- Björk, Magnus, 1977, et al.
(författare)
-
Exposed Datapath for Efficient Computing
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce FlexCore, which is the first exemplar of a processor based on the FlexSoC processor paradigm. TheFlexCore utilizes an exposed datapath for increased performance. Microbenchmarks yield a performance boost of a factor of two over a traditional five-stage pipeline with the same functional units as the FlexCore.We describe our approach to compiling for the FlexCore.A flexible interconnect allows the FlexCore datapath to bedynamically reconfigured as a consequence of code generation. Additionally, specialized functional units may be introduced and utilized within the same architecture and compilation framework. The exposed datapath requires a wide control word. The conducted evaluation of two micro benchmarks confirms that this increases the instruction bandwidth and memory footprint. This calls for an efficient instruction decoding as proposed in the FlexSoC paradigm.
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- Thuresson, Martin, 1977, et al.
(författare)
-
FlexCore: Utilizing Exposed Datapath Control for Efficient Computing
- 2009
-
Ingår i: Journal of Signal Processing Systems. - : Springer Science and Business Media LLC. - 1939-8115 .- 1939-8018. ; 57:1, s. 5-19
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce FlexCore, the first exemplar of an architecture based on the FlexSoC framework. Comprising the same datapath units found in a conventional five-stage pipeline, the FlexCore has an exposed datapath control and a flexible interconnect to allow the datapath to be dynamically reconfigured as a consequence of code generation. Additionally, the FlexCore allows specialized datapath units to be inserted and utilized within the same architecture and compilation framework.This study shows that, in comparison to a conventional five-stage general-purpose processor, the FlexCore is up to 40\% more efficient in terms of cycle count on a set of benchmarks from the embedded application domain. We show that both the fine-grained control and the flexible interconnect contribute to the speedup. Furthermore, our synthesized, placed and routed FlexCore offers savings both in energy and execution time.The exposed FlexCore datapath requires a wide control word. The conducted evaluation confirms that this increases the instruction bandwidth and memory footprint. This calls for efficient instruction decoding as proposed in the FlexSoC framework.
|
|
| 5. |
- Själander, Magnus, 1977, et al.
(författare)
-
A Flexible Datapath Interconnect for Embedded Applications
- 2007
-
Ingår i: IEEE Computer Society Annual Symposium on VLSI. ; , s. 15-20
-
Konferensbidrag (refereegranskat)abstract
- We investigate the effects of introducing a flexible interconnect into an exposed datapath. We define an exposed datapath as a traditional GPP datapath that has its normal control removed, leading to the exposure of a wide control word. For an FFT benchmark, the introduction of a flexible interconnect reduces the total execution time by 16%. Compared to a traditional GPP, the execution time for an exposed datapath using a flexible interconnect is 32% shorter whereas the energy dissipation is 29% lower. Our investigation is based on a cycleaccurate architectural simulator and figures on delay, power, and area are obtained from placed-and-routed layouts in a commercial 0.13-ìm technology. The results from our case studies indicate that by utilizing a flexible interconnect, significant performance gains can be achieved for generic applications.
|
|
| 6. |
- Axelsson, Emil, 1978, et al.
(författare)
-
Teaching Hardware Description and Verification
- 2005
-
Ingår i: 2005 International Conference on Microelectronic Systems Education. - 0769523749 ; , s. 119-120
-
Konferensbidrag (refereegranskat)abstract
- We outline the course "Hardware Description and Verification", taught at the department of computing science, and how the course and our research benefit from each other.
|
|
| 7. |
- Björk, Magnus, 1977
(författare)
-
A First Order Extension of Stålmarck's Method
- 2005
-
Ingår i: Logic for Programming, Artificial Intelligence, and Reasoning, 2005, Montego Bay, Jamaica. - 9783540305538 ; :LNAI 3835, s. 276-291
-
Konferensbidrag (refereegranskat)abstract
- We describe an extension of Stålmarck's method in First Order Logic. Stålmarck's method is a tableaux-like theorem proving method for propositional logic, that uses a branch-and-merge rule known as the dilemma rule. This rule opens two branches and later merges them, by retaining their common consequences. The propositional version does this with normal set intersection, while the FOL version searches for pairwise unifiable formulae from the two branches. The proof procedure attempts to find proofs with as few simultaneously open branches as possible. We present the proof system and a proof procedure, and show soundness and completeness. We also present benchmarks for an implementation of the proof procedure.
|
|
| 8. |
- Björk, Magnus, 1977
(författare)
-
A First Order Extension of Stålmarck's Method
- 2006
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Stålmarck's method is an algorithm that decides validity of formulae in propositional logic. It resembles many tableaux method, but uses a special branch-and-merge-rule, called the dilemma rule. The dilemma rule creates two branches, where a formula (called the dilemma formula) is assumed to be false in one branch and true in the other one. If neither of the branches turns out to be contradictory, then the branches are merged into one branch again, retaining the common consequences of the two branches. We present a first order version of Stålmarck's method. When branches are merged in first order logic, variables occurring in the respective branches are unified, to retain as much information as possible. We show that variables introduced in dilemma formulae must be treated rigidly in the branches of the dilemma where they were introduced, but that they are universal during and after the merge. Thus, the dilemma rule can be used to introduce lemmas with universal variables.We also present a proof procedure that searches for shallow dilemma proofs. It begins by searching for proofs not including the dilemma rule, then extends the search with non-nested dilemmas. After that, proofs with at most two simultaneously open dilemmas are found, then with three, and so on. The proof procedure does not substitute rigid variables destructively; instead it explores an instance of the current dilemma, after the branches have been merged. This is done to preserve as many generalized conclusions as possible, and to be able to find new dilemma formulae. We show that the calculus and proof procedure are sound and complete. We present encouraging benchmarks for the automated theorem prover Dilemma, that is based on the method.
|
|
| 9. |
- Björk, Magnus, 1977
(författare)
-
Adding Equivalence Classes to Stålmarck's Method in First Order Logic
- 2004
-
Ingår i: Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004). - 1613-0073.
-
Konferensbidrag (refereegranskat)abstract
- Stålmarck's method is a theorem proving method for propositional logic that has been known for more than a decade, and which has been successful in many industrial applications. During the last few years, a first order logic lifting of the method has been developed. This extended abstract presents the major features of the extension, and describes work in progress on how to lift the equivalence relations known from the propositional version of the method.
|
|
| 10. |
- Björk, Magnus, 1977
(författare)
-
Appendix to: A First Order Extension of Stålmarck's Method
- 2005
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This is an appendix to the paper "A First Order Extension of Stålmarck's Method", published at the LPAR 2005 conference in Montego Bay, Jamaica (Logic for Programming, Artificial Intelligence, and Reasoning). It contains the full proofs of all lemmas and theorems stated in the paper.
|
|
