HPR L/S Project: Hardware and Embedded Software Synthesis from Executable Specifications.
Toy Bluespec Compiler.

Rudimentary/Toy Bluespec Compiler

The Bluespec System Verilog language is increasingly seen as a viable and productive alternative to conventional RTL coding for hardware design. For compiler writers like myself, the best way to learn a new language was to write a toy compiler for it. Also, where there's a lack of formal semantics for a language, writing a compiler is a good way to learn about the important and/or arbitrary decisions that have to be made. (These seem to be in the scheduler and in the way implicit guards of implicit guards are processed)

The user manual from Bluespec Inc may have restricted circulation, so this informal study was based on a couple of published studies: `HARDWARE LANGUAGES AND PROOF' by Dominic Richards of Manchester University and `A Unified Model for Hardware/Software Codesign' by Nirav Dave when at MIT.

This article gives the essence of a compiler for Bluespec. This toy compiler was coded in F Sharp using the HPR/LS library. This library provides various logic manipulation facilities and output functions for SMV, SystemC, Verilog and so on. Rather than initially writing a Bluespec parser, the test abstract-syntax trees were manually entered as separate F Sharp source files. This is actually an attractive approach but needs tidying up from what is here. The attraction is that Bluespec has a static elaborator which is basically a Haskel interpreter, but by embedding our constructs in F Sharp instead, we have the power of the ML dialect of F Sharp to do exactly the same kind of elaboration. All of the higher-order iterators and functors are exactly the same, modulo inserting 'fun () -> ' in a few places to get lazy behaviour. The good work needed is to use the domain-specific language (DSL) embedding facilities of F Sharp for the elaborated leaves. I might do this if I update this page.

I shall put a version of the Toy Bluespec Compiler on the following link for your own experiments: HERE.

Parser example run example run.

First simple test

The first test was a rule that has a single register incremented on every clock cycle:
let test_ast1 =
    (*     module test1();
              Reg#(#UInt(15)) ctr1 <- mk_register(0)

              rule test_ast1 (True) ;
                  ctr1.write(ctr1.read()+1)
              endrule
           endmodule
    *)
    Bsv_moduleDef("test1",
                  ([], [], Bsv_typen "Empty"),
                  [
                    Bsv_varDeclAssign("ctr1", [B_num [15]; B_num[1]], "mkReg", []);
                    Bsv_rule("test_ast1", B_true, [ g_write("ctr1", B_diadic(V_plus, g_read("ctr1"), B_num[1]))])
                  ],
                  [])

The first test generated the following output (which works fine: ctr is incremented on every clock cycle):

// CBG Orangepath HPR/LS System
//  /home/djg11/d320/hprls/bsvc/bsv.exe  -vnl test1.vnl test1
module test1(input clk, input RST_N);
  reg test_ast1_FIRE;
  reg [14:0] test1_ctr1_DREG;
  reg [14:0] test1_ctr1_Din;
  wire test1_ctr1_RDY;
  reg test1_ctr1_EN;
  always   @(posedge clk )  begin
      if (!RST_N || test1_ctr1_EN)  test1_ctr1_DREG <= (!RST_N ? 0: test1_ctr1_Din);
      end
  
  assign test_ast1_FIRE = 1;
  always @(*) test1_ctr1_EN =  test_ast1_FIRE;
  always @(*) test1_ctr1_Din =  1+test1_ctr1_DREG;
  
  // 2 vectors of width 1
  // 2 vectors of width 15
  // Total state bits in module = 32 bits.
  // 1 continuously assigned (wire/non-state) bits
endmodule
// eof (HPR/LS Verilog)

Second Test

The second test was to compile my Dining Philosophers example: Dining Philosophers in Bluespec Verilog.

Not originally having a parser, I had to manually enter the syntax tree for the example. Fortunately it is not too long.

The main part of the grammar is:

// Bluespec: Toy abstract syntax (may not be right!)
// Various modifiers for an interface:
type bsv_provisos_t =
    | Proviso_alwaysReady
    | Proviso_alwaysEnabled    
;

// Method prototype protocol has one of these three forms:
type bsv_protoprotocol_t =
    | BsvProtoValue of bsv_type_name_t
    | BsvProtoActionValue of bsv_type_name_t
    | BsvProtoAction 
   

and bsv_type_name_t =
    | Bsv_typen of string // for now - separate from bsv_if_t ... but can join.
    | Bsv_typen_uint_ns // Native/primitive run-time type
    | Bsv_typen_uint1 of int  // Native/primitive run-time type
    | Bsv_typen_action



// Method prototype: has name, provisio/pragmas, return type and method formals (pairs of formal and actuals so-far bound).
and bsv_methodProto_t = Bsv_methodProto of string * bsv_provisos_t list * bsv_protoprotocol_t * (bsv_type_name_t * string) list


and bsv_sigma_protocol_t =
    | BsvValue 
    | BsvAction of hexp_t option * (hbexp_t * hexp_t)  //  (en-net if needed) * (rdy-x, rdy-net)
and bsv_sigma_t = Bsv_current of string * bsv_sigma_protocol_t * (bsv_type_name_t * hexp_t option) * (hexp_t * hexp_t) list

and actuals_t = (string * (bsv_type_name_t * bsv_exp_t)) list

and formals_t = (bsv_exp_t * string) list


and bsv_moduleStmt_t = // Or actionValueStmt ?
    | Bsv_varDeclAssign  of string * bsv_exp_t list * string * string list
    | Bsv_rule           of string * bsv_bexp_t * bsv_moduleStmt_t list
    | Bsv_assignStmt     of string * bsv_exp_t
    | Bsv_eascActionStmt of bsv_exp_t
    | Bsv_pliStmt        of string * bsv_exp_t list      // for $display and so on
    | Bsv_beginEndStmt   of bsv_moduleStmt_t list
    | Bsv_ifThenStmt     of bsv_bexp_t * bsv_moduleStmt_t * bsv_moduleStmt_t option
    | Bsv_whileStmt     of bsv_bexp_t * bsv_moduleStmt_t * bsv_moduleStmt_t option      | Bsv_returnStmt    of bsv_exp_t // Only in actionvalue blocks.
    | Bsv_CaseStmt      of bsv_exp_t * (bsv_exp_t * bsv_moduleStmt_t) list *  bsv_moduleStmt_t option
    | Bsv_methodDef     of string * formals_t * bsv_bexp_t * bsv_moduleStmt_t list
    | Bsv_primBuffer    of bsv_exp_t * bsv_exp_t (* Only for internal implementation *)
  



// There are three lots of 'parameters' to the typical module as stored in this triple.
// They are the parametric type args of the exported interface, the parameters to the generate
// function and the list of interfaces, which consists of those used plus the single interface exported. 
and bsv_moduleParams_t = (bsv_type_name_t * string) list * (bsv_type_name_t * string) list * bsv_type_name_t

// The Bluespec interface definition: Generic parameters and list of methods:
and bsv_if_t = Bsv_if of (bsv_type_name_t * string) list *  bsv_methodProto_t list

// Boolean expressions
and bsv_bexp_t =
    | B_true
    | B_false
    | B_firing of string // Backdoor access to the composite guard for any rule.
    | B_not  of bsv_bexp_t
    | B_and  of bsv_bexp_t list
    | B_or   of bsv_bexp_t list        
    | B_bexp of hbexp_t // Pre-compiled forms
    | B_bdiop of x_bdiop_t * bsv_exp_t list // Equality, less than and orreduce where list is a singleton.
    | B_orred of bsv_exp_t

// Integer expressions    
and bsv_exp_t =
    | B_num of int list
    | B_blift of bsv_bexp_t
    | B_query of bsv_bexp_t * bsv_exp_t * bsv_exp_t
    | B_var of string
    | B_string of string    
    | B_hexp of hexp_t
    | B_fsmStmt of bsv_exprFsmStmt_t
    | B_ifcRef of string // Interface reference
    | B_diadic of x_diop_t * bsv_exp_t * bsv_exp_t
    | B_apply of string list * bsv_exp_t list

// Finite-state machine sub language.    
and bsv_exprFsmStmt_t =
 | Bsv_seqFsmStmt    of bsv_exprFsmStmt_t list
 | Bsv_parFsmStmt    of bsv_exprFsmStmt_t list
 | Bsv_ifFsmStmt     of bsv_bexp_t * bsv_exprFsmStmt_t * bsv_exprFsmStmt_t option 
 | Bsv_whileFsmStmt  of bsv_bexp_t * bsv_exprFsmStmt_t
 | Bsv_repeatFsmStmt of bsv_exprFsmStmt_t
 | Bsv_eascFsmStmt   of bsv_exp_t
 | Bsv_breakFsmStmt
 | Bsv_continueFsmStmt
;
The encoding of the spoon (really should be called a fork!) and the philosopher and the table of five of them look like this:
(* interface Spoon_if;
     method Action pickup();
     method Action putdown();
  endinterface
*)

      Bsv_ifDef("Spoon_if",
                Bsv_if([],
                       [
                         Bsv_methodProto("pickup", [], BsvProtoAction, []);
                         Bsv_methodProto("putdown", [], BsvProtoAction, []);              
                       ])
                )

(*
   module spoon (Spoon_if) ;

     Reg#(Bool) inuse <- mkReg(?);    

	method Action pickup() if (!inuse);
	 action
	   inuse <= True;
	 endaction
	endmethod

	method Action putdown();
	 action
	   inuse <= False;
	 endaction
	endmethod
   endmodule
*)

    Bsv_moduleDef("Spoon",
                  ([], [], Bsv_typen "Spoon_if"),
                  [
                    Bsv_varDeclAssign("inuse", [B_num[1]; B_num[0]], "mkReg", []);
                    Bsv_methodDef("pickup", [], B_bdiop(V_dned, [g_read "inuse"; B_num[1]]), [ g_write("inuse", B_num[1]); Bsv_pliStmt("$display", [B_string "pickup"]) ]);
                    Bsv_methodDef("putdown", [], B_true, [ g_write("inuse", B_num[0]); Bsv_pliStmt("$display", [B_string "putdown"]) ])
                  ],
                  [])


    (* interface Random_if;
       method ActionValue#(UInt#(15)) gen();
       endinterface
     *)
      Bsv_ifDef("Random_if",
                Bsv_if([],
                       [
                         Bsv_methodProto("gen", [], BsvProtoActionValue(Bsv_typen_uint1 15), []);
                       ])
                )


     (*  module mkRandom_gen #(UInt#(15) seed) (Random_if);
           Reg#(UInt#(15)) prbs <- mkReg(seed);
           method ActionValue#(UInt#(15)) gen();
             prbs <= (prbs << 1) | (((prbs >> 14) ^ (prbs >> 13)) & 1);
             return prbs;
           endmethod
         endmodule
     *)
    Bsv_moduleDef("mkRandom_gen",
                  ([(Bsv_typen "int", "seed")], [], Bsv_typen "Random_if"),
                  [
                    Bsv_varDeclAssign("prbs", [B_num[15]; B_var "seed"], "mkReg", []);
                    Bsv_methodDef("gen", [], B_true,
                                  [ g_write("prbs", B_diadic(V_bitor, B_diadic(V_lshift, g_read "prbs", B_num[1]), B_diadic(V_bitand, (B_diadic(V_bitor, B_diadic(V_rshift, g_read "prbs", B_num[14]), B_diadic(V_rshift, g_read "prbs", B_num[13]))), B_num[1])));
                                    Bsv_returnStmt(g_read "prbs");
                                  ])
                  ],
                  [])


    Bsv_moduleDef("Philo",
                  ([(Bsv_typen "int", "seed"); (Bsv_typen "int", "on")],
                   [(Bsv_typen "Spoon_if", "left"); (Bsv_typen "Spoon_if", "right")], Bsv_typen "Empty"),
                   [
                     Bsv_varDeclAssign("gen", [B_var "seed"], "mkRandom_gen", []);
                     Bsv_varDeclAssign("timer", [B_num[15]; B_num[0]], "mkReg", []);
                     Bsv_varDeclAssign("x", [B_num[15]; B_num[0]], "mkReg", []);
                     Bsv_rule("foo", B_bdiop(V_dned, [g_read("timer"); B_num[0]]), [ g_write("timer", B_diadic(V_minus, g_read "timer", B_num[1]))]);

                     Bsv_varDeclAssign("eating", [B_num[1]; B_num[0]], "mkReg", []);


                     Bsv_assignStmt("seq_behaviour",
                                B_fsmStmt(
                                          Bsv_whileFsmStmt(B_true,
                                                           Bsv_seqFsmStmt
                                                             [
                                                              fsm_write("x", g_actionVal("gen", "gen", []));
                                                              fsm_write("timer", B_diadic(V_bitand, g_read "timer", B_num[31]));
                                                              fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
                                                              fsm_action("left", "pickup", []);
                                                              fsm_noAction();
                                                              fsm_write("x", g_actionVal("gen", "gen", []));
                                                              fsm_write("timer", B_diadic(V_bitand, g_read "timer", B_num[31]));
                                                              fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
                                                              fsm_action("right", "pickup", []);
                                                              fsm_noAction();
                                                              fsm_write("eating", B_num[1]);
                                                              fsm_write("timer", B_var "on");
                                                              fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
                                                              fsm_write("eating", B_num[0]);
                                                              fsm_noAction();
                                                              fsm_action("left", "putdown", []);
                                                              fsm_noAction();
                                                              fsm_action("right", "putdown", []);
                                                              fsm_noAction();
                                                            ])));
                    Bsv_varDeclAssign("FSM", [B_var "seq_behaviour" ], "mkFSM", [ ]);                    

                    Bsv_rule("kickoff", B_true, [ g_action("FSM", "start", []) ]);
                   ],
                   [])


    Bsv_moduleDef("philoBENCH",
                  ([], [], Bsv_typen "Empty"),
                  [
                    Bsv_varDeclAssign("spoon0", [], "Spoon", []);
                    Bsv_varDeclAssign("spoon1", [], "Spoon", []);
                    Bsv_varDeclAssign("spoon2", [], "Spoon", []);
                    Bsv_varDeclAssign("spoon3", [], "Spoon", []);
                    Bsv_varDeclAssign("spoon4", [], "Spoon", []);


                    Bsv_varDeclAssign("philo0", [B_num[3]; B_num[7]  ], "Philo", [ "spoon0"; "spoon1" ]);                    
                    Bsv_varDeclAssign("philo1", [B_num[4]; B_num[4]  ], "Philo", [ "spoon1"; "spoon2" ]);                    
                    Bsv_varDeclAssign("philo2", [B_num[2]; B_num[9]  ], "Philo", [ "spoon3"; "spoon2" ]);                    
                    Bsv_varDeclAssign("philo3", [B_num[3]; B_num[6]  ], "Philo", [ "spoon3"; "spoon4" ]);                    
                    Bsv_varDeclAssign("philo4", [B_num[3]; B_num[6]  ], "Philo", [ "spoon4"; "spoon0" ]);                    
                  ],
                  [])
;

Note that I have reversed the spoons to philosopher number 2. This stops the system from deadlocking straightaway!

Verilog Output

The Verilog RTL output looks as follows (note: this was the very first run and there might be some bugs in this, but it seems to work!) HERE.

Modelsim simulation of Dining Philosophers using the Toy Bluespec Compiler

Does this deadlock? The HPR library can output also an NuSMV file of this design. We can give SMV the -ctt command line flag and it will check for deadlock (eventually?).

The above toy compiler has a default rule precedence based on the textual order of the rules in the source code. It's not hard to add priorities.

The above compiler does not have the interlock that BSV defaults to ON for each rule that stops it firing more than once per cycle. This can be added where the comment says.

Finally, the above compiler does not check alternate compositions of rule pairs to see if they have the same effect, but a simple approach based on textual equivalence of effect would work quite well because the expressions are all converted to a normal memoized form by the HPR library, so most minor artefacts arising from alternate compositions, such as operator association and operand interchange in commutative operators are eliminated.

SimpleProcessor.bsv Test

gtkwave plot of the Bluespec SimpleProcessor.bsv example

mono bsv.exe -incdir=/home/djg11/d320/hprls/bsvc/smalltests -cpp=disable -comb-assignment-delay=10  -vnl=dut.v  smalltests/SimpleProcessorTb.bsv
cver dut.v vsys.v
GPLCVER_2.11a of 07/05/05 (Linux-elf).
Copyright (c) 1991-2005 Pragmatic C Software Corp.
  All Rights reserved.  Licensed under the GNU General Public License (GPL).
  See the 'COPYING' file for details.  NO WARRANTY provided.
Today is Wed Nov  7 14:44:56 2012.
Compiling source file "dut.v"
Compiling source file "vsys.v"
Highest level modules:
SIMSYS

48: output regs[           1] = 3
49: Halt at pc13
  There were 0 error(s), 0 warning(s), and 24 inform(s).

The online Bluespec examples define a simple microprocessor that is provided with an assembly coding of Euclid's algorith. The above plot shows the toy compiler can now parse and correctly execute the processor and the example algorithm: the GCD of 27 and 15 is 3 which is printed from R1 at the end of the computation. The delay at the start is the download of the program into the processor by the testbench. Mind you, this hardly stretches the interesting parts of the Bluespec scheduler.

Listing ((C) Bluespec Inc):

Instruction code [14] =                                                               
   {                                                                                  
     tagged MovI { rd: R0, v: 0 },                // 0: The constant 0                
     tagged MovI { rd: R1, v: 15 },               // 1: x = 21                        
     tagged MovI { rd: R2, v: 27 },               // 2: y = 27                        
     // label_loop                                                                    
     tagged Brz { rs: R2, dest:label_done },      // 3: if (y == 0) goto done         
     tagged Gt  { rd: R3, rs1: R1, rs2: R2 },     // 4: tmp = (x > y)                 
     tagged Brz { rs: R3, dest: label_subtract }, // 5: if (x <= y) goto subtract     
     // swap                                                                          
     tagged Minus { rd: R3, rs1: R1, rs2: R0 },   // 6: tmp = x;                      
     tagged Minus { rd: R1, rs1: R2, rs2: R0 },   // 7: x = y;                        
     tagged Minus { rd: R2, rs1: R3, rs2: R0 },   // 8: y = tmp;                      
     tagged Br  label_loop,                       // 9: goto loop                     
     // label_subtract                                                                
     tagged Minus { rd: R2, rs1: R2, rs2: R1 },   // 10: y = y - x                    
     tagged Br  label_loop,                       // 11: goto loop                    
     // label_done                                                                    
     tagged Output R1,                            // 12: output x                     
     // label_last                                                                    
     tagged Halt                                  // 13: halt                         
   };                                                                                 

Verilog object file generated: dut.v.


Chuck Thacker's Tiny Computer

Simon Moore implemented Chuck Thacker's Tiny3 Processor in Bluespec. Simon's source files are here SWM Tiny3. This design now (Jan 2013) goes through the Toy Compiler and works!

The test program is coded in an assembly language entirely written in Bluespec. It is a simple program that writes the integers 9 down to 0 to the output FIFO.

   function List#(AsmLineT) my_program(function ImmT findaddr(String label)) =
/*0*/      cons(asmi("",    0, 0),  // Keep register 0 clear.
/*1*/      cons(asmi("",    1, 10), // put 10 in r1
/*2*/      cons(asmi("",    2, findaddr("loop")), // loop address in r2
/*3*/      cons(asm("loop", OpOut, FDECb, ShiftNone, SkipNever, 1, 0, 1), // r1-- and output
/*4*/      cons(asm("",     OpJump, FaORb, ShiftNone, SkipZero, 3, 2, 0), // jump r2 if not zero
/*5*/      cons(asm("",     OpReserved, Freserved, ShiftNone, SkipNever, 0, 0, 0), // stop processor
      tagged Nil))))));

Simulation output:

cver dut.v vsys.v
GPLCVER_2.12a of 05/16/07 (Linux-elf).
Copyright (c) 1991-2007 Pragmatic C Software Corp.
  All Rights reserved.  Licensed under the GNU General Public License (GPL).
  See the 'COPYING' file for details.  NO WARRANTY provided.
Today is Sun Jan 20 18:39:48 2013.
Compiling source file "dut.v"
Compiling source file "vsys.v"
Highest level modules:
SIMSYS
End of prog load
                2100: fetch 00 80000000: 
                2700: doSkip = False
                2700: r         0 = imm =          0
                2900: fetch 01 8100000a: 
                3500: doSkip = False
                3500: r         1 = imm =         10
                3700: fetch 02 82000003: 
                4300: doSkip = False
                4300: r         2 = imm =          3
                4500: fetch 03 01000583: 
                5100: doSkip = False
                5100: rd <-          1         9
Write out 00000009
                5300: fetch
                5300: output =          9 04 03040296: 
                5900: doSkip = False
                6100: fetch 03 01000583: 
                6700: doSkip = False
                6700: rd <-          1         8
Write out 00000008
                6900: fetch
                6900: output =          8 04 03040296: 
                7500: doSkip = False
                7700: fetch 03 01000583: 
                8300: doSkip = False
                8300: rd <-          1         7
Write out 00000007
                8500: fetch
                8500: output =          7 04 03040296: 
                9100: doSkip = False
                9300: fetch 03 01000583: 
                9900: doSkip = False
                9900: rd <-          1         6
Write out 00000006
               10100: fetch
               10100: output =          6 04 03040296: 
               10700: doSkip = False
               10900: fetch 03 01000583: 
               11500: doSkip = False
               11500: rd <-          1         5
Write out 00000005
               11700: fetch
               11700: output =          5 04 03040296: 
               12300: doSkip = False
               12500: fetch 03 01000583: 
               13100: doSkip = False
               13100: rd <-          1         4
Write out 00000004
               13300: fetch
               13300: output =          4 04 03040296: 
               13900: doSkip = False
               14100: fetch 03 01000583: 
               14700: doSkip = False
               14700: rd <-          1         3
Write out 00000003
               14900: fetch
               14900: output =          3 04 03040296: 
               15500: doSkip = False
               15700: fetch 03 01000583: 
               16300: doSkip = False
               16300: rd <-          1         2
Write out 00000002
               16500: fetch
               16500: output =          2 04 03040296: 
               17100: doSkip = False
               17300: fetch 03 01000583: 
               17900: doSkip = False
               17900: rd <-          1         1
Write out 00000001
               18100: fetch
               18100: output =          1 04 03040296: 
               18700: doSkip = False
               18900: fetch 03 01000583: 
               19500: doSkip = False
               19500: rd <-          1         0
Write out 00000000
               19700: fetch
               19700: output =          0 04 03040296: 
               20300: doSkip = True
               20500: fetch 06 6c697374: 
               21100: doSkip = False
               21100: rd <-        108         x
               21300: fetch 07 6c697374: 
               21900: doSkip = True
               21900: rd <-        108         x
               22100: fetch 09 xxxxxxxx: 
Halted at location **vsys.v(16) time 35000 from call to $finish.
  There were 0 error(s), 1 warning(s), and 63 inform(s).

Simulation of Simon Moore's Implementation of Chuck Thacker's Tiny3 Processor Design using the Toy Bluespec Compiler

See Also

  • TNDJG:0004: I converted my processor design to Bluespec and it went more than twice as fast!

  • Download the Toy Bluespec Compiler for your own experiments: HERE.

    (C) 2012-13 Orangepath Project. DJ Greaves.